applied: Agda proofs of APP-1 to APP-4 (WO 4.2, 2 of 3)

EXPLAINME.adoc

@@ -134,7 +134,8 @@ ____
 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 general properties are open.
+worked examples, each checked by Agda. Its four general properties are proved
+in Agda; the Rocq and Lean re-proofs are next.
 ____
 
 How this is implemented::
@@ -150,8 +151,8 @@ each, missing ones included, and a control in
 fails it.
 
 Caveat::
-The examples are checked, not the model: its general properties (APP-1 to
-APP-4) are open. The examples are synthetic and say nothing about any
+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
 organisation. The management-accounting design has no model yet.
 
 == Privacy by count
@@ -281,14 +282,21 @@ and `_⊔_` as builtins.
 |Not yet stated in a prover (next on the theory shelf)
 
 |APP-1 to APP-4: the cohort model of the applied shelf (missing propagates,
-cash identity, the funding gap, status never upgrades)
+cash identity, the funding gap, status never upgrades), Agda leg
+|proven
+|Agda, `--safe --without-K --cubical-compatible`
+|`verification/proofs/agda/Applied/Missing.agda`, `Cash.agda`, `IntLaws.agda`
+|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
 |-
-|`docs/status/PROOF-NEEDS.adoc`; model `verification/proofs/agda/Applied/Cohort.agda`
-|Stated in prose; the worked examples are checked, the properties are not
+|-
+|Not yet re-proved (WO 4.2, third pull request)
 |===
 
-Proofs: 3 proven of 9; 1 argued, 5 open (the token-lattice theorems count as
-one). The registry derives `PWG-1` for
+Proofs, counted by leg: 7 proven of 17; 1 argued, 9 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

@@ -35,15 +35,16 @@ describes what is proved, where, and how strongly.
 * *Applied systems.* 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 general properties are open.
+  worked examples, each checked by Agda. Its four general properties are proved
+  in Agda; the Rocq and Lean re-proofs are next.
 * *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, 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, the Rocq and Lean re-proofs
+of the cohort model (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,5 +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 are open proof obligations APP-1 to APP-4 in
+properties of the model, APP-1 to APP-4, are proved in Agda (Rocq and Lean
+re-proofs open); see
 `docs/status/PROOF-NEEDS.adoc`.

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

@@ -65,4 +65,5 @@ costs and floors in each mode, so you can compare the results.
 * Rates do not carry uncertainty. To explore it, write two examples with
   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 open.
+  (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.

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
-open. A check of a model on an example is not a proof of the model, and neither
+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
 establishes the truth of real inputs.

docs/status/PROOF-NEEDS.adoc

@@ -42,40 +42,45 @@ 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
-|Open: stated here, not yet in Agda (WO 4.2)
-|`verification/proofs/agda/Applied/Cohort.agda`
+|Agda leg proved; Rocq and Lean legs open (WO 4.2)
+|`verification/proofs/agda/Applied/Missing.agda`
 
 |APP-2
-|Cash identity: when every input is present, the closing cash of the last
-period equals the opening cash plus all receipts minus all payments
+|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
-|Open: stated here, not yet in Agda (WO 4.2)
-|`verification/proofs/agda/Applied/Cohort.agda`
+|Agda leg proved; Rocq and Lean legs open (WO 4.2)
+|`verification/proofs/agda/Applied/Cash.agda` (`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
-|Open: stated here, not yet in Agda (WO 4.2)
-|`verification/proofs/agda/Applied/Cohort.agda`
+|Agda leg proved; Rocq and Lean legs open (WO 4.2)
+|`verification/proofs/agda/Applied/Cash.agda` (`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
-|Open: stated here, not yet in Agda (WO 4.2)
-|`verification/proofs/agda/Applied/Cohort.agda`
+|Agda leg proved; Rocq and Lean legs open (WO 4.2)
+|`verification/proofs/agda/Applied/Missing.agda`
 |===
 
 APP-1 to APP-4 are about the cohort model of the applied shelf (re-anchoring
 plan WO 4.2, owner rulings 2026-11-12). Each statement would be true of any
 implementation of the model, so each is theory by PROOF-POLICY §1: proved in
-Agda and re-checked in Rocq and Lean. The model is written over an abstract
-number structure, so APP-2 and APP-3 need only its laws, not the laws of one
-number type. They are not theory-shelf admissions: no estate rule depends on
-them yet. Each worked example is already checked by Agda; a checked example is
-not a proof of the property.
+Agda and re-checked in Rocq and Lean. They are not theory-shelf admissions:
+no estate rule depends on them yet.
+
+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.
 
 No Mathesis obligation concerns an ABI or an FFI: since WO 3.2 the deed
 declares neither capability.

docs/status/PROOF-STATUS.adoc

@@ -24,14 +24,15 @@ 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)
-|Open
+|Agda leg proved; Rocq and Lean legs open
 |-
-|Stated in `docs/status/PROOF-NEEDS.adoc`; the model and its three worked
-examples check in Agda, but no theorem is stated in Agda yet
+|`verification/proofs/agda/Applied/Missing.agda`, `Cash.agda` and
+`IntLaws.agda`, gated in CI. No receipt yet: a grade needs all three legs
 |===
 
 *Overall*: 1 of 6 obligations discharged; 5 open (the token-lattice theorems
-count as one). These are counts, not a
+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
 percentage: PROOF-POLICY §8 grades are derived from receipts and are never
 flattened. The template example proofs were removed in WO 4.1.
 

docs/status/ROADMAP.adoc

@@ -176,7 +176,22 @@ One pull request that changes census rows is open at a time (atlas README,
    that depends on it stays missing. A golden-path control shows that the
    gate fails when a missing output is read as zero.
 ** APP-1 to APP-4 are recorded as open in `docs/status/PROOF-NEEDS.adoc`.
-   Next: the Agda proofs, then the Rocq and Lean re-proofs.
+   Merged (pull request 81).
+* WO 4.2, second pull request: the Agda proofs of APP-1 to APP-4, gated in
+  CI with no postulate in any import cone.
+** `Applied/Status.agda` and `Applied/Missing.agda`: APP-1 and APP-4, for any
+   number structure. If an output is given with status u, every input that it
+   depends on is given with a status at least u. Once a closing balance is
+   missing, every later one is missing; a "yes" verdict needs every period to
+   be a known "yes"; a known breach decides the verdict.
+** `Applied/Cash.agda`: APP-2 (cash identity) and APP-3 (the funding gap is
+   sound and least), for any ordered abelian group (`Laws`).
+** `Applied/IntLaws.agda`: the integer instance of the worked examples is an
+   ordered abelian group (owner ruling 2026-11-12), so APP-2 and APP-3 hold
+   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).
 * 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
@@ -222,8 +237,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 and the theory ledger merged; WO 4.2 in review (1 of
-3 pull requests)
+|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
 
 |5
 |Scale: receipts in the home repositories, the bridge lock pilot, a
@@ -253,4 +268,5 @@ scheduled census, a view of what each repository owes
   example; the model in Agda, proved; all four invariants recorded; a shared
   schema; three number modes for different users, with guidance; JSON Lines as
   the source of generated Agda; proofs in Agda, Rocq and Lean; three pull
-  requests.
+  requests; the laws of the integer instance proved in the second pull
+  request.