You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
{{ message }}
Repository navigation
applied: Agda proofs of APP-1 to APP-4 (WO 4.2, 2 of 3) - #83
This is the second of three pull requests for WO 4.2. It proves the four obligations of the cohort model in Agda, for the model as it runs. Following your ruling of 2026-11-12, the PR also proves that the integer instance of the worked examples satisfies the laws that APP-2 and APP-3 need.
Every new module is gated in the Agda manifest, and the gate finds no postulate in any import cone. The Rocq and Lean re-proofs are the third pull request.
Changes
Applied/Status.agda: the order of evidence statuses, and Covers u v: the value v is given, with a status at least u. zipWith and map pass it to their arguments.
Applied/Missing.agda: APP-1 and APP-4, for any number structure. One statement carries both. If an output is given with status u, then every input that it depends on is given with a status at least u. This holds for:
each output of a period: members, receipts, payments, closing cash, shortfall, support minutes, and both tests;
each kind of cohort.
Also proved:
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 a verdict;
the funding gap needs every shortfall.
Applied/Cash.agda: APP-2 and APP-3, for any ordered abelian group (Laws).
cash-identity: the last closing balance is the opening balance plus, summed over the periods, receipts minus payments. When a value is missing, both sides are missing together.
gap-sound: adding the gap to the previous balance meets every floor.
gap-least: any non-negative amount that meets every floor is at least the gap.
Applied/IntLaws.agda: the integer instance satisfies Laws. It uses Agda.Builtin only.
Every integer is written as P i ⊖ Q i.
Sums reduce to (a ⊖ b) + (c ⊖ d) = (a + c) ⊖ (b + d).
The order reduces to a natural-number comparison, with cancellation.
So the theorems apply to the arithmetic that the examples use, and the laws are shown to be satisfiable.
Applied/Cohort.agda: the two local helpers of cohortAt are now top-level functions (joined, renewed), so that the proofs can name them. The worked examples check unchanged.
Documents:PROOF-NEEDS, PROOF-STATUS, the EXPLAINME ledger ("7 proven of 17 legs; 1 argued, 9 open"), the README, the ROADMAP and the applied documents now say that the Agda leg is proved and the Rocq and Lean legs are open.
Updated the cohort model documentation and proof-status records to show that its four general properties are proved in Agda. Re-proofs in Rocq and Lean remain open.
Clarified that the proofs apply to the model, not to real-world organisations or inputs, and documented the scope and assumptions of the properties.
The second of three pull requests for WO 4.2 (owner rulings
2026-11-12). Every new module is gated in the Agda manifest; the gate
finds no postulate in any import cone.
- Applied/Status.agda: the order of evidence statuses, and `Covers u v`:
v is given with a status at least u. zipWith and map pass it to their
arguments.
- Applied/Missing.agda: APP-1 and APP-4, for any number structure. For
each output of a period (members, receipts, payments, closing cash,
shortfall, support minutes, both tests) and for each cohort kind: if
the 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 a verdict; the funding gap needs
every shortfall.
- Applied/Cash.agda: APP-2 (`cash-identity`: the last closing balance is
the opening balance plus, summed over the periods, receipts minus
payments; both sides are missing together) and APP-3 (`gap-sound`,
`gap-least`), for any ordered abelian group (`Laws`).
- Applied/IntLaws.agda: the integer instance of the worked examples
satisfies `Laws` (owner ruling 2026-11-12), built on Agda.Builtin
only, so APP-2 and APP-3 hold for the model as it runs.
- Applied/Cohort.agda: the local helpers of cohortAt are now top-level
(`joined`, `renewed`) so that the proofs can name them; the worked
examples check unchanged.
- PROOF-NEEDS, PROOF-STATUS, EXPLAINME, README, ROADMAP and the applied
documents: the Agda leg is proved; the Rocq and Lean legs are open.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_0136P7Zo9dheFQzYYWV49hAk
No actionable comments were generated in the recent review.
Walkthrough
The PR adds Agda proofs for APP-1 through APP-4, including cash and funding-gap properties and the integer laws used by the cash proofs. It registers the proof modules and updates documentation to record the Agda results and the remaining Rocq and Lean re-proofs.
Changes: Applied model proofs
Layer / File(s)
Summary
Evidence status and coverage foundations verification/proofs/agda/Applied/Status.agda
Defines the evidence-status ordering and coverage evidence. Adds proofs for status meets and for coverage requirements of map and zipWith results.
Cohort model and missing-value proofs verification/proofs/agda/Applied/Cohort.agda, verification/proofs/agda/Applied/Missing.agda
Moves joined and renewed to top-level helpers. Adds proofs that cohort and row outputs require covered inputs, and proves properties for missing closing cash, verdicts, and worst shortfall coverage.
Cash identity and funding-gap proofs verification/proofs/agda/Applied/Cash.agda
Defines ordered abelian group laws. Proves the cash identity, that the worst shortfall is sufficient to meet every floor, and that no smaller non-negative addition can meet every floor.
Integer laws and cash-proof instance verification/proofs/agda/Applied/IntLaws.agda
Proves arithmetic and order laws for integers, constructs the intLaws record, and exposes the cash proofs for integers through OnIntegers.
Proof registration and status verification/proofs/agda/MANIFEST, EXPLAINME.adoc, README.adoc, applied-systems/finance/cohort-economics/*, applied-systems/methods/types-and-assurance.adoc, docs/status/*
Adds gated manifest entries for the proof modules. Updates proof ledgers, status pages, and project documentation to record the Agda proofs and the open Rocq and Lean re-proofs.
hyperpolymath/mathesis#81: Adds the Applied.Cohort model and the APP-1 to APP-4 obligations that this PR proves.
Suggested reviewers:claude
Merge Risk: Minimal · up to 13b7c
This change adds Agda proofs and updates proof-status documentation. The documented claims match what the proofs state, and no merge-blocking issue remains.
Pre-merge checks: 4
Check name
Status
Explanation
Title check
The title names the main change: Agda proofs of APP-1 to APP-4 for the WO 4.2 work, part 2 of 3. The changeset adds Agda modules (Status, Missing, Cash, IntLaws) that prove these obligations, and the …
Description check
The description follows the repository template's main sections: Summary, Changes, RSR Quality Checklist, and Testing. It explains the purpose, lists the key Agda modules and document updates, and rep…
Linked Issues check
Check skipped because no linked issues were found for this pull request.
Out of Scope Changes check
Check skipped because no linked issues were found for this pull request.
Full details: Title check
Explanation
The title names the main change: Agda proofs of APP-1 to APP-4 for the WO 4.2 work, part 2 of 3. The changeset adds Agda modules (Status, Missing, Cash, IntLaws) that prove these obligations, and the title matches that main point. The title is 55 characters, within a short single-sentence form.
Full details: Description check
Explanation
The description follows the repository template's main sections: Summary, Changes, RSR Quality Checklist, and Testing. It explains the purpose, lists the key Agda modules and document updates, and reports the checks run with their Agda version and CI caveat. Some template items are not addressed. The Screenshots section is marked not applicable. The checklist also leaves some Required items unchecked, though the author marks most as done. The template's HTML comments and the Closes #N linking guidance are not used, and no issue is linked. These gaps are non-critical, so the description is mostly complete.
Finishing Touches
Generate unit tests (beta)
Commit to this branch
Create a new PR
Autofix · Keep fixing CodeRabbit findings and required CI, and resolving merge conflicts
Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out.
Included review availability: This review used your included allowance. Your plan provides up to 1 included review per hour; 0 remain after this review.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
This is the second of three pull requests for WO 4.2. It proves the four obligations of the cohort model in Agda, for the model as it runs. Following your ruling of 2026-11-12, the PR also proves that the integer instance of the worked examples satisfies the laws that APP-2 and APP-3 need.
Every new module is gated in the Agda manifest, and the gate finds no postulate in any import cone. The Rocq and Lean re-proofs are the third pull request.
Changes
Applied/Status.agda: the order of evidence statuses, andCovers u v: the value v is given, with a status at least u.zipWithandmappass it to their arguments.Applied/Missing.agda: APP-1 and APP-4, for any number structure. One statement carries both. If an output is given with status u, then every input that it depends on is given with a status at least u. This holds for:Also proved:
Applied/Cash.agda: APP-2 and APP-3, for any ordered abelian group (Laws).cash-identity: the last closing balance is the opening balance plus, summed over the periods, receipts minus payments. When a value is missing, both sides are missing together.gap-sound: adding the gap to the previous balance meets every floor.gap-least: any non-negative amount that meets every floor is at least the gap.Applied/IntLaws.agda: the integer instance satisfiesLaws. It usesAgda.Builtinonly.So the theorems apply to the arithmetic that the examples use, and the laws are shown to be satisfiable.
Applied/Cohort.agda: the two local helpers ofcohortAtare now top-level functions (joined,renewed), so that the proofs can name them. The worked examples check unchanged.Documents:
PROOF-NEEDS,PROOF-STATUS, the EXPLAINME ledger ("7 proven of 17 legs; 1 argued, 9 open"), the README, the ROADMAP and the applied documents now say that the Agda leg is proved and the Rocq and Lean legs are open.RSR Quality Checklist
Required
As Applicable
docs/status/ROADMAP.adocupdatedPROOF-NEEDSAPP-1 to APP-4: Agda leg proved)Testing
I ran these in this session on
main0c624b8plus this change:bash scripts/check-proofs.sh agda: all 10 gated modules pass, and the axiom audit finds no postulate in any import cone. Manifest coverage passes.bash tests/golden/check_controls_test.sh: stale catalogue, failing proof and missing read as zero all fail as they should.just check-viewspasses, and so dovalidate-claude-md,validate-coapt,validate-state,validate-rsrandvalidate-repo-map.Screenshots
Not applicable.
Generated by Claude Code
Summary by CodeRabbit
Documentation
Verification