docs: add AFFIRMATION.adoc anchored at 53600326

[hyperpolymath]

Summary

Adds AFFIRMATION.adoc, the third file of the README / EXPLAINME / AFFIRMATION trio. It is a dated snapshot, open to refutation, of what proven can honestly claim at main 5360032. It also lists what proven does not claim.

• Affirmed:
  • proven.ipkg builds 305/305 modules in CI;
  • proof-check (0.8.0) passes;
  • there is no believe_me or idris_crash in code;
  • the false postulates are gone (fix(soundness): remove false postulates in SafeFiniteField, SafePipe, SafeTerminal #228, fix(SafeFiniteField): reject irreducibles not of degree n before reduction #229);
  • gitleaks is clean (chore(secrets): ignore three gitleaks test-fixture false positives #231).
• Not claimed:
  • the README's "Mathematically proven" (PROOF-NEEDS samples about 3%);
  • the bodyless declarations that act as postulates;
  • 22 escape hatches;
  • the stubbed hash FFI;
  • tests.ipkg (it does not build);
  • about 79 unbuilt modules;
  • the weak or empty theorems;
  • the red checks on CI: seven checks red on main independent of PR content (tests.ipkg, assert_total, SPDX, 4 governance/scan) #230;
  • a pinned CI image.

Where the README says more than this file, this file wins.

Refs #230

Type of change

• 🐛 Bug fix: no
• ✨ New feature: no
• 💥 Breaking change: no
• 🕳️ Soundness fix: no
• 📖 Documentation
• 🧹 Refactor / tech debt: no
• ⚡ Performance: no
• 🔧 Build / CI / tooling: no

📌 New pins

Head SHA: c25c3b5

None. This PR changes no action uses:, actions.lock, lockfile or container digest.

How has this been verified?

Every claim cites its evidence in the file:

• The build: CI job verify-idris-build (id 112464109461) at 5360032 ends with 305/305: Building Proven.
• The test build: idris2-ci.yml at a32c3b6 gave proof-check success and build failure. The failure comes from the tests.ipkg renames in bdb1863.
• The escape-hatch counts: grep -rnw --include=*.idr <word> src, with comment and doc-comment lines removed:
  • believe_me 0 (the 48 raw matches are all comments);
  • idris_crash 0;
  • assert_total 20;
  • assert_smaller 2.
• The hash stubs: Hash.idr has 9 %foreign lines, all commented out.
• The recon figures (383 bodyless, 79 unbuilt, 52 warnings, 71 () theorems) are labelled as measured at 8542e84 and not re-counted here.
• The 3% is quoted from PROOF-NEEDS.adoc (1 of 32 sampled modules).
• Placeholder check: the file contains no {{, TODO: update, <PROJECT or example.com. It has 103 substantive lines.

Checklist

• My commits are signed (git log --format=%G? → G).
• I ran the project's own checks: no Idris source changed, so there was nothing to rebuild. The evidence is CI's at the anchor.
• New files carry the correct SPDX-License-Identifier: CC-BY-SA-4.0, as for the repo's other .adoc docs, with the attribution line from .claude/CLAUDE.md.
• Docs: this is the docs change. Correcting the README overclaim is item C4 of the follow-up and is not done here.
• No soundness hole: no .idr file is touched.

Notes for reviewers

• The anchor is the parent of this commit. A squash merge changes the commit SHA but keeps 5360032 as the parent, so the anchor stays valid only if nothing else lands on main first. If something does, rebase this branch and re-check the anchor row.
  Pre-existing red checks (red on main too; this PR does not touch them):

• governance / Workflow security linter: deferred to CI: seven checks red on main independent of PR content (tests.ipkg, assert_total, SPDX, 4 governance/scan) #230 (dead OCaml pin)

• governance / Trusted-base reduction policy: deferred to CI: seven checks red on main independent of PR content (tests.ipkg, assert_total, SPDX, 4 governance/scan) #230 (undocumented escape hatches)

• governance / Validate Hypatia Baseline: deferred to CI: seven checks red on main independent of PR content (tests.ipkg, assert_total, SPDX, 4 governance/scan) #230 (--argjson crash in standards)

• Enforce Trustfile Policies: deferred to CI: seven checks red on main independent of PR content (tests.ipkg, assert_total, SPDX, 4 governance/scan) #230 (Palimpsest licence headers)

• Aspect — Safety Invariants: deferred to CI: seven checks red on main independent of PR content (tests.ipkg, assert_total, SPDX, 4 governance/scan) #230

• Emerged, not yet on CI: seven checks red on main independent of PR content (tests.ipkg, assert_total, SPDX, 4 governance/scan) #230: GitHub Pages / build is blocked by the action allowlist on actions/upload-artifact@v4. The mirror-* ×3 jobs have an empty host variable. Both are recorded in dev-notes/inbox/findings.md.

• There are no required checks on main, so automerge is deliberately not armed. This waits for a human squash merge.

🤖 Generated with Claude Code

https://claude.ai/code/session_01HZc76cZKg5tUgduxXGLQkD

[coderabbitai]

Note

Currently processing new changes in this PR. This may take a few minutes, please wait...

⚙️ Run configuration

• Configuration used: Organization UI
• Review profile: ASSERTIVE
• Plan: Advanced
• Run ID: 7550e806-bbad-497b-8bf5-34d5e82d3116

📥 Commits

Reviewing files that changed from the base of the PR and between 5360032 and c25c3b5.

📒 Files selected for processing (1)

• AFFIRMATION.adoc

 __________________________________________________________________________________________________________
< Minimize coupling between modules. Avoid coupling by writing 'shy' code and applying the Law of Demeter. >
 ----------------------------------------------------------------------------------------------------------
  \
   \   (\__/)
       (•ㅅ•)
       / 　 づ

• Autopilot · Keep fixing CodeRabbit findings and required CI, and resolving merge conflicts

---

Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out.

❤️ Share

• X
• Mastodon
• Reddit
• LinkedIn

_{Comment @coderabbitai help to get the list of available commands.}

[sonarqubecloud]

Quality Gate passed

Issues
0 New issues
0 Accepted issues

Measures
0 Security Hotspots
0.0% Coverage on New Code
0.0% Duplication on New Code

See analysis details on SonarQube Cloud