applied: Rocq and Lean re-proofs of APP-1 to APP-4 (WO 4.2, 3 of 3)

EXPLAINME.adoc

@@ -135,7 +135,7 @@ Methods that apply mathematics to decisions, starting
 with accounting and finance. A shared input schema keeps missing apart from
 zero. A cohort model in Agda has three number modes and three synthetic
 worked examples, each checked by Agda. Its four general properties are proved
-in Agda; the Rocq and Lean re-proofs are next.
+in Agda and re-proved in Rocq and Lean.
 ____
 
 How this is implemented::
@@ -152,7 +152,7 @@ fails it.
 
 Caveat::
 Its four general properties (APP-1 to APP-4) are proved in Agda for the
-model as it runs; the Rocq and Lean re-proofs are open. The examples are synthetic and say nothing about any
+model as it runs, and re-proved in Rocq and Lean. The examples are synthetic and say nothing about any
 organisation. The management-accounting design has no model yet.
 
 == Privacy by count
@@ -289,14 +289,20 @@ cash identity, the funding gap, status never upgrades), Agda leg
 |The model only. APP-2 and APP-3 rest on the laws that `IntLaws.agda`
 proves for the integer instance
 
-|APP-1 to APP-4, Rocq and Lean legs
-|open
-|-
-|-
-|Not yet re-proved (WO 4.2, third pull request)
+|APP-1 to APP-4, Rocq leg (re-proved)
+|proven
+|Rocq 8.18.0, `coqc`; `Print Assumptions` closed
+|`verification/proofs/coq/Cohort.v`
+|The model only, as in Agda
+
+|APP-1 to APP-4, Lean leg (re-proved)
+|proven
+|Lean 4.29.0, `lean`; no axiom
+|`verification/proofs/lean4/Cohort.lean`
+|The model only, as in Agda
 |===
 
-Proofs, counted by leg: 7 proven of 17; 1 argued, 9 open (the token-lattice
+Proofs, counted by leg: 15 proven of 17; 1 argued, 1 open (the token-lattice
 theorems count as one; APP-1 to APP-4 count one for each prover). The registry derives `PWG-1` for
 THY-1 from the receipt. The checker versions are those that CI asserts in the
 Guix shell (CI run 43057783538).

README.adoc

@@ -36,15 +36,15 @@ describes what is proved, where, and how strongly.
   with accounting and finance. A shared input schema keeps missing apart from
   zero. A cohort model in Agda has three number modes and three synthetic
   worked examples, each checked by Agda. Its four general properties are proved
-  in Agda; the Rocq and Lean re-proofs are next.
+  in Agda and re-proved in Rocq and Lean.
 * *Privacy by count.* The frame names public repositories only. The number of
   private repositories in the listing is kept as one number.
 
 [NOTE]
 .Planned
 ====
-The token-lattice theorems of the theory shelf, the Rocq and Lean re-proofs
-of the cohort model (APP-1 to APP-4), a published atlas, receipts in more home
+The token-lattice theorems of the theory shelf, receipts for the cohort model
+proofs (APP-1 to APP-4), a published atlas, receipts in more home
 repositories, and a scheduled census. See
 link:docs/status/ROADMAP.adoc[the roadmap].
 ====

applied-systems/finance/cohort-economics/README.adoc

@@ -41,6 +41,6 @@ link:../../methods/input-schema.adoc[input schema], and its expected outputs.
 `just applied-build` writes link:generated/examples.adoc[the worked examples]
 and one Agda module for each example. Agda accepts that module only if the
 model computes every expected output, missing ones included. The general
-properties of the model, APP-1 to APP-4, are proved in Agda (Rocq and Lean
-re-proofs open); see
+properties of the model, APP-1 to APP-4, are proved in Agda and re-proved in
+Rocq and Lean; see
 `docs/status/PROOF-NEEDS.adoc`.

applied-systems/finance/cohort-economics/modes.adoc

@@ -66,4 +66,4 @@ costs and floors in each mode, so you can compare the results.
   different rates.
 * The model checks each worked example exactly. The general properties
   (obligations APP-1 to APP-4 in `docs/status/PROOF-NEEDS.adoc`) are proved
-  in Agda for every mode; the Rocq and Lean re-proofs are open.
+  in Agda for every mode, and re-proved in Rocq and Lean.

applied-systems/methods/types-and-assurance.adoc

@@ -31,5 +31,5 @@ The cohort model (`verification/proofs/agda/Applied/Cohort.agda`) is the first
 test of these ideas. Each value carries its evidence status, a missing value
 stays missing, and every worked example is checked by Agda. Its general
 properties (obligations APP-1 to APP-4 in `docs/status/PROOF-NEEDS.adoc`) are
-proved in Agda; the Rocq and Lean re-proofs are open. A check of a model on an example is not a proof of the model, and neither
+proved in Agda and re-proved in Rocq and Lean. A check of a model on an example is not a proof of the model, and neither
 establishes the truth of real inputs.

docs/status/PROOF-NEEDS.adoc

@@ -42,31 +42,31 @@ missing input is missing, in every period after it too, and never zero. A
 verdict is "no" on a known breach and otherwise missing when any value it
 depends on is missing; it is never "yes" then
 |Agda, re-checked in Rocq and Lean
-|Agda leg proved; Rocq and Lean legs open (WO 4.2)
-|`verification/proofs/agda/Applied/Missing.agda`
+|Proved in Agda, Rocq and Lean; no receipt yet (WO 4.2)
+|`verification/proofs/agda/Applied/Missing.agda`; Rocq and Lean: `Cohort.v`, `Cohort.lean`
 
 |APP-2
 |Cash identity: the closing cash of the last period equals the opening cash
 plus, summed over the periods, receipts minus payments; when a value is
 missing, both sides are missing
 |Agda, re-checked in Rocq and Lean
-|Agda leg proved; Rocq and Lean legs open (WO 4.2)
-|`verification/proofs/agda/Applied/Cash.agda` (`cash-identity`)
+|Proved in Agda, Rocq and Lean; no receipt yet (WO 4.2)
+|`verification/proofs/agda/Applied/Cash.agda` (`cash-identity`); Rocq and Lean: `cash_identity`
 
 |APP-3
 |The funding gap is sound and least: adding the gap to the opening cash
 keeps every closing balance at or above its floor, and no smaller
 non-negative amount does
 |Agda, re-checked in Rocq and Lean
-|Agda leg proved; Rocq and Lean legs open (WO 4.2)
-|`verification/proofs/agda/Applied/Cash.agda` (`gap-sound`, `gap-least`)
+|Proved in Agda, Rocq and Lean; no receipt yet (WO 4.2)
+|`verification/proofs/agda/Applied/Cash.agda` (`gap-sound`, `gap-least`); Rocq and Lean: `gap_sound`, `gap_least`
 
 |APP-4
 |Status never upgrades: the evidence status of an output is never stronger
 than the weakest status of the inputs that it depends on
 |Agda, re-checked in Rocq and Lean
-|Agda leg proved; Rocq and Lean legs open (WO 4.2)
-|`verification/proofs/agda/Applied/Missing.agda`
+|Proved in Agda, Rocq and Lean; no receipt yet (WO 4.2)
+|`verification/proofs/agda/Applied/Missing.agda`; Rocq and Lean: `Cohort.v`, `Cohort.lean`
 |===
 
 APP-1 to APP-4 are about the cohort model of the applied shelf (re-anchoring
@@ -79,8 +79,12 @@ The Agda leg holds for the model as it runs. APP-1 and APP-4 hold for any
 number structure: one statement carries both (`Covers`, in
 `Applied/Status.agda`). APP-2 and APP-3 hold for any ordered abelian group
 (`Laws`, in `Applied/Cash.agda`), and `Applied/IntLaws.agda` proves that
-the integer instance of the worked examples is one. Every module is in the
-gated Agda manifest, with no postulate in its import cone.
+the integer instance of the worked examples is one. The Rocq and Lean legs
+(`verification/proofs/coq/Cohort.v`, `verification/proofs/lean4/Cohort.lean`)
+restate the same definitions and re-prove every theorem, the integer laws
+included. Every module is gated: no postulate in an Agda import cone, every
+Rocq theorem closed under the global context, and no axiom in any Lean
+theorem. No receipt records these legs yet, so no grade is derived.
 
 No Mathesis obligation concerns an ABI or an FFI: since WO 3.2 the deed
 declares neither capability.

docs/status/PROOF-STATUS.adoc

@@ -24,15 +24,14 @@ reader of PROOF-POLICY §8.5.1.
 |Not yet stated in a prover
 
 |APP-1 to APP-4, the cohort model of the applied shelf (WO 4.2)
-|Agda leg proved; Rocq and Lean legs open
+|Proved in Agda, Rocq and Lean
 |-
-|`verification/proofs/agda/Applied/Missing.agda`, `Cash.agda` and
-`IntLaws.agda`, gated in CI. No receipt yet: a grade needs all three legs
+|The record below. No receipt yet, so no grade is derived
 |===
 
-*Overall*: 1 of 6 obligations discharged; 5 open (the token-lattice theorems
-count as one). APP-1 to APP-4 have their Agda leg; each stays open until its
-Rocq and Lean legs land. These are counts, not a
+*Overall*: 5 of 6 obligations are proved in all three provers; THY-1 alone has
+a receipt and a derived grade. The token-lattice theorems (counted as one) are
+open. These are counts, not a
 percentage: PROOF-POLICY §8 grades are derived from receipts and are never
 flattened. The template example proofs were removed in WO 4.1.
 
@@ -211,6 +210,62 @@ dependency units unify features separately, and the theorem applies to
 each unit's graph.
 |===
 
+== Applied obligations
+
+=== APP-1 to APP-4: the cohort model of the applied shelf
+
+[cols="1,3"]
+|===
+|Statements
+|`docs/status/PROOF-NEEDS.adoc`, rows APP-1 to APP-4.
+
+|Agda (source of truth)
+|`verification/proofs/agda/Applied/`: `Cohort` (the model), `Status` and
+`Missing` (APP-1, APP-4), `Cash` (APP-2, APP-3, for any ordered abelian
+group), `IntNumber` and `IntLaws` (the integer instance and its laws).
+`--safe --without-K --cubical-compatible`; no postulate in any import cone.
+
+|Rocq leg
+|`PROVEN`, route `re-proved`. `verification/proofs/coq/Cohort.v`, Rocq
+8.18.0. The gate's `Print Assumptions` finds all 82 theorems closed under
+the global context. The standard library's `PeanoNat` and `Lia` prove the
+natural-number arithmetic; `Unset Lia Cache` keeps `lia` from writing a
+file.
+
+|Lean leg
+|`PROVEN`, route `re-proved`. `verification/proofs/lean4/Cohort.lean`,
+Lean 4.29.0, core only. The gate's audit finds no axiom in any of the 95
+theorems. No `simp`, `omega` or `ac_rfl`: each brings `propext` in.
+
+|Statement correspondence (§2.2)
+|Compared by reading, item by item. Each target restates every Agda
+definition with the same constructors, fields and clauses, and states every
+Agda theorem with the same hypotheses and conclusions (Agda `cash-identity`
+is `cash_identity`, and so on). The differences are encoding only:
+
+* Agda's `_<_` and `_-_` on Nat are `natLt` and `monus`, with the same
+  clauses, recursive on the second argument as Agda's are, so that the
+  same terms reduce.
+* Lean compiles overlapping patterns with `propext`, so `meet`,
+  `zipWith`, `kand` and `denominator` list their cases without overlap;
+  `zipWith` and `kand` split their first argument first, as Agda's do.
+  Each is the same function.
+* Agda's `n div suc m` is `Nat.div` (Rocq) or `/` (Lean): each rounds
+  down and gives 0 for a zero divisor.
+* `T b` is `b = true`. The proof-relevant records `Covers`, `Bounded`
+  and `Yes` are existential propositions, so every result is a theorem
+  that the axiom audit inspects. `All` and `Any` stay functions on lists.
+* The integers are Agda's (`pos`, `negsuc` and the same operations), not
+  the standard `Z` or `Int`: Lean's `Int` lemmas use `propext`.
+
+Residual assumptions: none in any leg.
+
+|Machine receipt (§8.5.1)
+|None yet. The receipt `verification/receipts/theory_praxis.deed` records
+THY-1 only. Adding APP-1 to APP-4 needs receipts from a CI run on the merged
+commit, so no grade is derived for them yet.
+|===
+
 == Verification commands
 
 [source,bash]
@@ -233,6 +288,10 @@ bash tests/proofs/gate_controls_test.sh agda
 |THY-1 receipts earned again at Agda 2.7.0.1 and Lean 4.29.0 in the pinned
 Guix shell; the receipt derives `PWG-1`.
 
+|2026-11-12
+|APP-1 to APP-4 proved in Agda (with the laws of the integer instance), then
+re-proved in Rocq and Lean (re-anchoring plan WO 4.2). No receipt yet.
+
 |2026-11-11
 |The template obligations ABI-1 to ABI-5, TP-1 and TP-2 leave the lists:
 they never applied to Mathesis (re-anchoring plan WO 3.4, owner ruling

docs/status/ROADMAP.adoc

@@ -191,7 +191,14 @@ One pull request that changes census rows is open at a time (atlas README,
    for the model as it runs.
 ** The two local helpers of `cohortAt` became top-level functions, so that
    the proofs can name them. The worked examples are unchanged.
-** Next: the Rocq and Lean re-proofs (third pull request).
+** Merged (pull request 83).
+* WO 4.2, third pull request: the Rocq and Lean re-proofs of APP-1 to APP-4,
+  with the integer laws: `verification/proofs/coq/Cohort.v` (82 theorems,
+  `Print Assumptions` closed) and `verification/proofs/lean4/Cohort.lean`
+  (95 theorems, no axiom). Each restates the Agda definitions clause for
+  clause; `docs/status/PROOF-STATUS.adoc` records the comparison. WO 4.2 is
+  then done. Next: receipts for APP-1 to APP-4, from a CI run on the merged
+  commit, then WO 4.3 (needs a ruling).
 * Open item for the owner (ruling 2026-11-12): none of the JSON Lines data
   files declares a licence; JSON has no comment syntax. The owner will write
   one `REUSE.toml` rule at the root that covers all of them (doctrine 6: a
@@ -237,8 +244,8 @@ anchors `c81cb84`
 |The three shelves: the theory admission rule and the token-lattice
 theorems, the applied shelf tied to the evidence spine, the published atlas
 (needs a ruling)
-|In progress: WO 4.1, the theory ledger and WO 4.2 (1 of 3) merged; the
-Agda proofs of WO 4.2 in review
+|In progress: WO 4.1, the theory ledger and WO 4.2 (2 of 3) merged; the
+Rocq and Lean re-proofs of WO 4.2 in review
 
 |5
 |Scale: receipts in the home repositories, the bridge lock pilot, a

mathesis_chora.deed

@@ -1021,6 +1021,7 @@
               "verification/proofs/agda/FeatureReachability.agda"
               "verification/proofs/coq/FeatureReachability.v"
               "verification/proofs/lean4/FeatureReachability.lean"
+              "verification/proofs/coq/Cohort.v" "verification/proofs/lean4/Cohort.lean"
               "EXPLAINME.adoc"
               "docs/theory/admissions.jsonl" "docs/theory/ledger.jsonl" "docs/theory/generated/"
               "scripts/applied/" "tests/applied/" "verification/proofs/agda/Applied/")