applied: input schema, cohort model in Agda, three worked examples (WO 4.2, 1 of 3)

EXPLAINME.adoc

@@ -132,15 +132,27 @@ resolution is argued, not proved.
 [quote, README.adoc]
 ____
 Methods that apply mathematics to decisions, starting
-with accounting and finance. Design documents only so far.
+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.
 ____
 
 How this is implemented::
 `link:applied-systems/README.adoc[]` and its subdirectories: a management
-accounting design, a decision record, an event map and evidence guidance.
+accounting design, a decision record, an event map and evidence guidance. The
+input schema (`link:applied-systems/methods/input-schema.adoc[]`, enforced by
+`scripts/applied/inputs.mjs`) gives each input an evidence status and keeps
+missing apart from zero. The cohort model
+(`verification/proofs/agda/Applied/Cohort.agda`) has three number modes and
+three synthetic worked examples; the Agda gate checks every expected output of
+each, missing ones included, and a control in
+`tests/golden/check_controls_test.sh` shows that a missing value read as zero
+fails it.
 
 Caveat::
-No executable model, data schema or worked example exists yet (WO 4.2).
+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
+organisation. The management-accounting design has no model yet.
 
 == Privacy by count
 
@@ -267,8 +279,16 @@ and `_⊔_` as builtins.
 |-
 |`docs/proposals/mathesis-research-programme.adoc`
 |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)
+|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
 |===
 
-Proofs: 3 proven of 5; 1 argued, 1 open. The registry derives `PWG-1` for
+Proofs: 3 proven of 9; 1 argued, 5 open (the token-lattice theorems count as
+one). 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).

Justfile

@@ -710,8 +710,9 @@ uncloak:
 check: check-views check-proofs
 
 # Needs bun, network for the receipts, and MATHESIS_STANDARDS (see `registry`).
-# Views current: catalogue, census tests, atlas, claims registry and bridges
-check-views: catalogue-check census-test atlas-check registry-check
+# Views current: catalogue, census tests, atlas, claims registry, bridges and
+# the worked cohort examples
+check-views: catalogue-check census-test atlas-check registry-check applied-check
 
 # Needs agda, coqc and lean, e.g. in the pinned Guix:
 #   guix time-machine -C build/channels.scm -- shell -m build/manifest.scm -- just check-proofs
@@ -776,3 +777,14 @@ registry-check:
 # story: just theory-ledger "THY-2 admitted after its Lean leg landed"
 theory-ledger note="":
     bun scripts/registry/claims-registry.mjs ledger {{ if note == "" { "" } else { "--note " + quote(note) } }}
+
+# Regenerate the Agda checks and the view of the worked cohort examples
+# (applied shelf, re-anchoring plan WO 4.2) from their JSON Lines
+applied-build:
+    bun scripts/applied/cohort.mjs build
+
+# Fail if a generated file of the cohort examples is stale; test the input
+# schema and the example validator. Agda checks the examples in check-proofs.
+applied-check:
+    bun scripts/applied/cohort.mjs check
+    bun test tests/applied/

README.adoc

@@ -33,15 +33,17 @@ describes what is proved, where, and how strongly.
   pinned Guix shell. A theorem enters the theory shelf only under a stated
   admission rule, and a generated index lists each one with its dependant.
 * *Applied systems.* Methods that apply mathematics to decisions, starting
-  with accounting and finance. Design documents only so far.
+  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.
 * *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 applied
-shelf tied to the evidence rules, a published atlas, receipts in more home
+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
 repositories, and a scheduled census. See
 link:docs/status/ROADMAP.adoc[the roadmap].
 ====

applied-systems/README.adoc

@@ -23,6 +23,7 @@ Do not copy a private case here merely by changing its name.
 |link:decision-science/README.adoc[Decision science] |Event chains, uncertainty and the value of additional information.
 |link:organisational-design/README.adoc[Organisational design] |Capacity, role design, service safeguards and implementation constraints.
 |link:methods/evidence-and-assumptions.adoc[Evidence and assumptions] |Shared conventions for status, provenance, units and uncertainty.
+|link:methods/input-schema.adoc[Input schema] |One record for each model input, with its evidence status; missing is never zero.
 |link:methods/types-and-assurance.adoc[Types and assurance] |Research questions connecting types to reliable applied models.
 |===
 

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

@@ -27,3 +27,19 @@ Sensitivity analysis should report conversion, renewal retention and workload
 together with minimum cash, the period of cumulative payback (if reached),
 full-cost result and capacity excess. Do not call an infeasible workload case
 viable merely because its financial column is positive.
+
+== Model and worked examples
+
+The cohort model is `verification/proofs/agda/Applied/Cohort.agda`: active
+members, receipts, payments, closing cash, the shortfall below the cash floor,
+support minutes, the floor and capacity verdicts, and the funding gap. Every
+value can be missing and carries an evidence status. The model has three number
+modes; link:modes.adoc[Number modes] says which one to use.
+
+Each file in `examples/` is one synthetic worked example: its inputs, in the
+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
+`docs/status/PROOF-NEEDS.adoc`.

applied-systems/finance/cohort-economics/examples/approximate.jsonl

@@ -0,0 +1,60 @@
+{"description":"Rates are whole numbers per 1000. Each step counts whole members and rounds down. The retention rate of cohort B is missing. Cohort B in P3 needs no retention, so it is known. Every value in P4 that depends on it stays missing, and so does the cash verdict. The capacity verdict is known: P3 is above capacity.","kind":"example","mode":"approximate","name":"approximate","period_length":"one month; each month end is a renewal date","periods":["P1","P2","P3","P4"],"synthetic":true,"title":"Rates per 1000, one input missing (mode approximate)"}
+{"description":"The first recruitment campaign.","id":"A","kind":"cohort","start":"P1"}
+{"description":"A second, smaller campaign two months later.","id":"B","kind":"cohort","start":"P3"}
+{"access":"public","depends_on":[],"description":"Cash at the start of P1","evidence_status":"illustrative","id":"opening_cash","kind":"input","owner":"mathesis","period":null,"source":"synthetic","unit":"pence","value":600000,"verified_on":null}
+{"access":"public","depends_on":[],"description":"Cash received from each active member in each period","evidence_status":"illustrative","id":"price","kind":"input","owner":"mathesis","period":null,"source":"synthetic","unit":"pence per member per period","value":1500,"verified_on":null}
+{"access":"public","depends_on":[],"description":"Avoidable cost of each active member in each period","evidence_status":"illustrative","id":"unit_cost","kind":"input","owner":"mathesis","period":null,"source":"synthetic","unit":"pence per member per period","value":400,"verified_on":null}
+{"access":"public","depends_on":[],"description":"Support time that each active member needs in each period","evidence_status":"illustrative","id":"support_minutes","kind":"input","owner":"mathesis","period":null,"source":"synthetic","unit":"minutes per member per period","value":30,"verified_on":null}
+{"access":"public","depends_on":[],"description":"Fixed payments in the period","evidence_status":"illustrative","id":"fixed_cost","kind":"input","owner":"mathesis","period":"P1","source":"synthetic","unit":"pence","value":350000,"verified_on":null}
+{"access":"public","depends_on":[],"description":"Fixed payments in the period","evidence_status":"illustrative","id":"fixed_cost","kind":"input","owner":"mathesis","period":"P2","source":"synthetic","unit":"pence","value":350000,"verified_on":null}
+{"access":"public","depends_on":[],"description":"Fixed payments in the period","evidence_status":"illustrative","id":"fixed_cost","kind":"input","owner":"mathesis","period":"P3","source":"synthetic","unit":"pence","value":350000,"verified_on":null}
+{"access":"public","depends_on":[],"description":"Fixed payments in the period","evidence_status":"illustrative","id":"fixed_cost","kind":"input","owner":"mathesis","period":"P4","source":"synthetic","unit":"pence","value":350000,"verified_on":null}
+{"access":"public","depends_on":[],"description":"Agreed minimum cash at the end of the period","evidence_status":"illustrative","id":"cash_floor","kind":"input","owner":"mathesis","period":"P1","source":"synthetic","unit":"pence","value":200000,"verified_on":null}
+{"access":"public","depends_on":[],"description":"Agreed minimum cash at the end of the period","evidence_status":"illustrative","id":"cash_floor","kind":"input","owner":"mathesis","period":"P2","source":"synthetic","unit":"pence","value":200000,"verified_on":null}
+{"access":"public","depends_on":[],"description":"Agreed minimum cash at the end of the period","evidence_status":"illustrative","id":"cash_floor","kind":"input","owner":"mathesis","period":"P3","source":"synthetic","unit":"pence","value":200000,"verified_on":null}
+{"access":"public","depends_on":[],"description":"Agreed minimum cash at the end of the period","evidence_status":"illustrative","id":"cash_floor","kind":"input","owner":"mathesis","period":"P4","source":"synthetic","unit":"pence","value":200000,"verified_on":null}
+{"access":"public","depends_on":[],"description":"Support time available in the period","evidence_status":"illustrative","id":"capacity_minutes","kind":"input","owner":"mathesis","period":"P1","source":"synthetic","unit":"minutes","value":7500,"verified_on":null}
+{"access":"public","depends_on":[],"description":"Support time available in the period","evidence_status":"illustrative","id":"capacity_minutes","kind":"input","owner":"mathesis","period":"P2","source":"synthetic","unit":"minutes","value":7500,"verified_on":null}
+{"access":"public","depends_on":[],"description":"Support time available in the period","evidence_status":"illustrative","id":"capacity_minutes","kind":"input","owner":"mathesis","period":"P3","source":"synthetic","unit":"minutes","value":7500,"verified_on":null}
+{"access":"public","depends_on":[],"description":"Support time available in the period","evidence_status":"illustrative","id":"capacity_minutes","kind":"input","owner":"mathesis","period":"P4","source":"synthetic","unit":"minutes","value":7500,"verified_on":null}
+{"access":"public","depends_on":[],"description":"People that the campaign of cohort A reaches","evidence_status":"illustrative","id":"A.contacts","kind":"input","owner":"mathesis","period":null,"source":"synthetic","unit":"people","value":2000,"verified_on":null}
+{"access":"public","depends_on":[],"description":"Contacts of cohort A who join","evidence_status":"illustrative","id":"A.conversion","kind":"input","owner":"mathesis","period":null,"source":"synthetic","unit":"per 1000","value":100,"verified_on":null}
+{"access":"public","depends_on":[],"description":"Members of cohort A who renew at each renewal date","evidence_status":"illustrative","id":"A.retention","kind":"input","owner":"mathesis","period":null,"source":"synthetic","unit":"per 1000","value":850,"verified_on":null}
+{"access":"public","depends_on":[],"description":"People that the campaign of cohort B reaches","evidence_status":"illustrative","id":"B.contacts","kind":"input","owner":"mathesis","period":null,"source":"synthetic","unit":"people","value":1500,"verified_on":null}
+{"access":"public","depends_on":[],"description":"Contacts of cohort B who join","evidence_status":"illustrative","id":"B.conversion","kind":"input","owner":"mathesis","period":null,"source":"synthetic","unit":"per 1000","value":80,"verified_on":null}
+{"access":"public","depends_on":[],"description":"Members of cohort B who renew at each renewal date","evidence_status":"missing","id":"B.retention","kind":"input","owner":"mathesis","period":null,"source":"synthetic","unit":"per 1000","value":null,"verified_on":null}
+{"evidence_status":"illustrative","id":"members","kind":"expected","period":"P1","value":200}
+{"evidence_status":"illustrative","id":"receipts","kind":"expected","period":"P1","value":300000}
+{"evidence_status":"illustrative","id":"payments","kind":"expected","period":"P1","value":430000}
+{"evidence_status":"illustrative","id":"closing","kind":"expected","period":"P1","value":470000}
+{"evidence_status":"illustrative","id":"shortfall","kind":"expected","period":"P1","value":-270000}
+{"evidence_status":"illustrative","id":"hours","kind":"expected","period":"P1","value":6000}
+{"evidence_status":"illustrative","id":"cash_ok","kind":"expected","period":"P1","value":true}
+{"evidence_status":"illustrative","id":"capacity_ok","kind":"expected","period":"P1","value":true}
+{"evidence_status":"illustrative","id":"members","kind":"expected","period":"P2","value":170}
+{"evidence_status":"illustrative","id":"receipts","kind":"expected","period":"P2","value":255000}
+{"evidence_status":"illustrative","id":"payments","kind":"expected","period":"P2","value":418000}
+{"evidence_status":"illustrative","id":"closing","kind":"expected","period":"P2","value":307000}
+{"evidence_status":"illustrative","id":"shortfall","kind":"expected","period":"P2","value":-107000}
+{"evidence_status":"illustrative","id":"hours","kind":"expected","period":"P2","value":5100}
+{"evidence_status":"illustrative","id":"cash_ok","kind":"expected","period":"P2","value":true}
+{"evidence_status":"illustrative","id":"capacity_ok","kind":"expected","period":"P2","value":true}
+{"evidence_status":"illustrative","id":"members","kind":"expected","period":"P3","value":264}
+{"evidence_status":"illustrative","id":"receipts","kind":"expected","period":"P3","value":396000}
+{"evidence_status":"illustrative","id":"payments","kind":"expected","period":"P3","value":455600}
+{"evidence_status":"illustrative","id":"closing","kind":"expected","period":"P3","value":247400}
+{"evidence_status":"illustrative","id":"shortfall","kind":"expected","period":"P3","value":-47400}
+{"evidence_status":"illustrative","id":"hours","kind":"expected","period":"P3","value":7920}
+{"evidence_status":"illustrative","id":"cash_ok","kind":"expected","period":"P3","value":true}
+{"evidence_status":"illustrative","id":"capacity_ok","kind":"expected","period":"P3","value":false}
+{"evidence_status":"missing","id":"members","kind":"expected","period":"P4","value":null}
+{"evidence_status":"missing","id":"receipts","kind":"expected","period":"P4","value":null}
+{"evidence_status":"missing","id":"payments","kind":"expected","period":"P4","value":null}
+{"evidence_status":"missing","id":"closing","kind":"expected","period":"P4","value":null}
+{"evidence_status":"missing","id":"shortfall","kind":"expected","period":"P4","value":null}
+{"evidence_status":"missing","id":"hours","kind":"expected","period":"P4","value":null}
+{"evidence_status":"missing","id":"cash_ok","kind":"expected","period":"P4","value":null}
+{"evidence_status":"missing","id":"capacity_ok","kind":"expected","period":"P4","value":null}
+{"evidence_status":"missing","id":"cash_verdict","kind":"expected","period":null,"value":null}
+{"evidence_status":"illustrative","id":"capacity_verdict","kind":"expected","period":null,"value":false}
+{"evidence_status":"missing","id":"gap","kind":"expected","period":null,"value":null}