fix(a-sounder-constitution): make the Idris2 proof compile + machine-check it (Idris2 0.7.0)

a-sounder-constitution/README.adoc

@@ -103,9 +103,9 @@ executable mirror, exercised by `tests/`.
 
 Pre-alpha research artefact (2026-06-19). The JavaScript engine, tests, headless
 comparison, and web UI run today (Node 22 / any modern browser, zero
-dependencies). The Idris2 module is written to compile clean but has *not* been
-run through `idris2` in this environment — see `formal/README.adoc` for the
-verification status and graduation criteria.
+dependencies). The Idris2 module type-checks cleanly under Idris2 0.7.0
+(`idris2 --check formal/Constitution.idr`, exit 0) — see `formal/README.adoc`
+for the verification details and graduation criteria.
 
 == License
 

a-sounder-constitution/formal/Constitution.idr

@@ -30,11 +30,10 @@
 -- Contrast: in the unsound world `Property` is an ordinary constructor and
 -- reclassification is a total function any human can be fed to.
 --
--- VERIFICATION STATUS: written to compile under Idris2 with `%default total`
--- and zero `believe_me` / `assert_total`. It has NOT yet been run through
--- Idris2 in this environment (no idris2 on PATH); treat the "proved" claims as
--- pending CI, in line with this repo's blocker-tracking convention. The JS
--- mirror in ../src/constitution.js IS exercised by the test suite.
+-- VERIFICATION STATUS: type-checks cleanly under Idris2 0.7.0 with
+-- `%default total` and zero `believe_me` / `assert_total` / `postulate`
+-- (verified 2026-06-27 via `idris2 --check Constitution.idr`, exit 0). The JS
+-- mirror in ../src/constitution.js is exercised by the test suite.
 
 module Constitution
 
@@ -132,11 +131,21 @@ data SoundStep : Person -> Person -> Type where
 ||| Theorem: every sound step is rank-monotone. Standing is never reduced.
 ||| (The Reconstruction-style rights patch — only ever upward — is exactly the
 ||| set of moves this type admits.)
+|||
+||| `lteRefl` is reflexivity of `LTE`, inlined by induction on the index so the
+||| module needs only `import Data.Nat`. (Idris2 0.7.0's base supplies the same
+||| proof through the `Reflexive` interface as `reflexive`.)
+lteRefl : {n : Nat} -> LTE n n
+lteRefl {n = Z}   = LTEZero
+lteRefl {n = S k} = LTESucc lteRefl
+
+||| `a` is bound explicitly (hence relevant, not erased) so that `rank a` is
+||| available to `lteRefl` in the `Keep` case.
 public export
-soundMonotone : SoundStep a b -> LTE (rank a) (rank b)
-soundMonotone Keep       = lteRefl          -- rank p <= rank p
-soundMonotone Recognise  = LTESucc LTEZero  -- 1 <= 2
-soundMonotone Naturalise = LTEZero          -- 0 <= 2
+soundMonotone : {a : Person} -> SoundStep a b -> LTE (rank a) (rank b)
+soundMonotone {a} Keep   = lteRefl {n = rank a}  -- rank p <= rank p
+soundMonotone Recognise  = LTESucc LTEZero       -- 1 <= 2
+soundMonotone Naturalise = LTEZero               -- 0 <= 2
 
 -- ─────────────────────────────────────────────────────────────────────────────
 -- (3) PROOF OBLIGATION — coercion that is admissible-but-constrained.

a-sounder-constitution/formal/README.adoc

@@ -52,23 +52,21 @@ downstream of exactly this one distinction. The JS side is exercised by
 
 == Verification status
 
-[WARNING]
+[NOTE]
 ====
-This module is written to compile under Idris2 with `%default total` and zero
-`believe_me` / `assert_total`, but it has *not yet been run through Idris2 in
-this environment* (no `idris2` on `PATH`). Per this repo's convention, treat the
-"proved" claims as pending CI until the check below passes.
+*Machine-checked.* This module type-checks cleanly under *Idris2 0.7.0* with
+`%default total` and zero `believe_me` / `assert_total` / `postulate` (verified
+2026-06-27). The `Reflexive`-interface dependency for `LTE` is avoided by
+inlining a small `lteRefl` lemma, so the module needs only `import Data.Nat`.
 ====
 
-To check it locally:
+To reproduce:
 
 [source,sh]
 ----
-idris2 --check formal/Constitution.idr
+idris2 --check formal/Constitution.idr     # exit 0, no holes, no errors
 ----
 
-Expected: type-checks with no holes, no errors, no `believe_me`.
-
 == Graduation criteria (per `research/README.adoc`)
 
 . `idris2 --check` passes with zero `believe_me`/`assert_total`.