Say what verification/proofs/ actually contains

CHANGELOG.adoc

@@ -8,6 +8,27 @@ https://semver.org/spec/v2.0.0.html[Semantic Versioning].
 
 === [Unreleased]
 
+==== Fixed
+
+* *`+docs/status/PROOF-STATUS.adoc+` published a percentage, which PROOF-POLICY
+forbids (2026-11-09).* The summary read `+*Overall*: 0% proven+`. §8.4 rule 7 is
+explicit — "Never publish 'X% proved', an average grade, or a single confidence
+score" — and asks for a count per category with the denominator instead. The
+figure was accurate; the form was the forbidden one. It now reads as a census,
+with a note recording why. The same line ships in `+rsr-template-repo+`'s
+`+PROOF-STATUS.adoc+`, so every repository minted from it carries the same
+breach; fixing it there is the solution at source.
+
+==== Added
+
+* *A note saying what `+verification/proofs/+` actually contains (2026-11-09).*
+`+docs/status/PROOF-STATUS.adoc+` now records that the directory is the unmodified
+mint set, that none of it states a property of HERMENEIA, and that the 0%-proven summary
+is therefore the accurate count rather than a backlog against those files. Also
+records that nothing there supports a Proof Witness Grade under PROOF-POLICY §8.1,
+and that removing the templates (as trope-checker did under ADR 0005 D5) is an
+owner decision.
+
 ==== Added
 
 - `coaptation`: `just check-coapt-identity` (`.machine_readable/coaptation/check-identity.sh`)

docs/status/PROOF-STATUS.adoc

@@ -20,7 +20,16 @@
 | *Total* | *7* | *0* | *0* | *0* | *7*
 |===
 
-*Overall*: 0% proven
+*Census.* Of 7 recorded obligations: 0 done, 0 in progress, 0 blocked, 7
+remaining. No obligation here carries a Proof Witness Grade, because none is a
+theory obligation of this repository under PROOF-POLICY §8.1.
+
+NOTE: this line used to read "*Overall*: 0% proven". PROOF-POLICY §8.4 rule 7 is
+explicit — "Never publish 'X% proved', an average grade, or a single confidence
+score" — and requires a count per category with the denominator instead. The
+figure was accurate; the *form* was the one the policy forbids. The same line
+ships in `rsr-template-repo`'s `PROOF-STATUS.adoc`, so every repository minted
+from it carries it; fixing it there is the solution at source.
 
 == Proofs Done
 
@@ -68,6 +77,39 @@
 | TP-2 | Public API type safety | TP | Lean4 | P2 | 4h
 |===
 
+== What `verification/proofs/` currently contains
+
+NOTE: as of 2026-11-09 the whole of `verification/proofs/` is the *unmodified mint
+set*. Five files still carry an explicit marker — `coq/TypeSafety.v`,
+`agda/Properties.agda`, `lean4/ApiTypes.lean`, `idris2/Types.idr` and
+`tlaplus/StateMachine.tla` all say "Replace with your project's …" — and the
+`idris2/ABI/` modules are from the same mint (`ABI/Pointers.idr`: "Template proof
+— customise for your project's pointer types"). None of them states a property of
+HERMENEIA: the Agda proves `length (xs ++ ys) ≡ length xs + length ys`, the Lean proves
+the functor laws for a template `ApiResult`, the Coq is a toy expression language,
+and the TLA+ models a placeholder request pipeline.
+
+They are therefore not evidence for anything, which is why the census above
+correctly reads 0 done of 7: that count is accurate, not a backlog against these
+files. No escape hatch is present either: no `believe_me`, `assert_total`,
+`postulate`, `sorry`, `Axiom` or `Admitted` occurs in any body — verified by
+`hyperpolymath/mathesis`, `scripts/census/proof-holes.sh`, run over this tree on
+2026-11-09, which reports no hole, axiom or unsafe record.
+
+One policy finding does come back from that same scan, and it is real:
+`verification/proofs/agda/Properties.agda` carries *no* `OPTIONS` pragma at all, so
+it does not set `--safe`, let alone the PROOF-POLICY §2.1 invocation
+`--safe --without-K --cubical-compatible`. Since §2.1 binds first-party Agda theory
+entrypoints and this file is not a theory entrypoint of this repository but mint
+boilerplate, the defensible fix is removal rather than adding flags to a template —
+which is the owner decision noted below. Until then the finding stands.
+
+Under PROOF-POLICY §8.1 none of this supports a Proof Witness Grade, because none of
+it is a theory obligation of this repository. `hyperpolymath/trope-checker` removed
+the identical never-instantiated templates under ADR 0005 D5; whether HERMENEIA does the
+same is an owner decision (doctrine 7: cold is not disposable), so nothing is
+deleted here. The real obligations are the ones named in `PROOF-NEEDS.adoc`.
+
 == Verification Commands
 
 [source,bash]