Skip to content

Commit f496d44

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
committed
docs: seed proof-debt.md per standards#203 schema (all markers §(e) vendored)
Add docs/proof-debt.md conforming to the trusted-base reduction policy schema from hyperpolymath/standards#203 (canonical) + standards#211 (check-trusted-base.sh CI gate). Triage result: all 150 syntactic markers (13 files) live under the absolute-zero/ subtree, which is an in-tree copy of the sibling estate repo hyperpolymath/absolute-zero. Canonical disposition is delegated upstream. Per standards#203 guidance ("extend the schema; document the extension at the top of the file as a repo-specific note"), this seed introduces disposition §(e) VENDORED — estate-sibling, for markers whose close-out path is in another estate repo. §(a)/(b)/(c)/(d) are all empty because maa-framework itself contains no proof-bearing source outside the vendored subtree. Breakdown by file group: - absolute-zero/proofs/coq/ : 7 files, 91 markers - absolute-zero/proofs/lean4/ : 4 files, 54 markers - absolute-zero/proofs/agda/ : 1 file, 1 marker (grep false positive) Vendored-ratio: 13/13 files vendored, 0/13 estate-owned-by-this-repo. PROOF-NEEDS.md's known gap (`y_not_cno` Admitted in proofs/coq/lambda/LambdaCNO.v) is recorded as a §(e) entry deferred to the sibling repo, consistent with the policy's "vendored markers go in §(e)" rule. Two owner-decision questions filed inline: 1. Should absolute-zero/ become a git submodule rather than a vendored copy? 2. Re-sync cadence until that decision lands. Refs hyperpolymath/standards#203 hyperpolymath/standards#211 Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
1 parent f4ba523 commit f496d44

1 file changed

Lines changed: 177 additions & 0 deletions

File tree

‎docs/proof-debt.md‎

Lines changed: 177 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,177 @@
1+
<!--
2+
SPDX-License-Identifier: MPL-2.0
3+
SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath)
4+
-->
5+
6+
# Proof Debt — maa-framework
7+
8+
**Schema**: `hyperpolymath/standards`
9+
[`docs/TRUSTED-BASE-REDUCTION-POLICY.adoc`](https://github.com/hyperpolymath/standards/blob/main/docs/TRUSTED-BASE-REDUCTION-POLICY.adoc)
10+
— the canonical policy, landed via standards#203.
11+
**Enforcement**: standards#211 (`scripts/check-trusted-base.sh`).
12+
13+
This file is the schema-conformant per-repo proof-debt index for
14+
`hyperpolymath/maa-framework`. The broader strategic proof goals across
15+
the repo live in [`PROOF-NEEDS.md`](../PROOF-NEEDS.md); this file
16+
enumerates the *specific* soundness-relevant escape hatches that the
17+
[`check-trusted-base.sh`](https://github.com/hyperpolymath/standards/blob/main/scripts/check-trusted-base.sh)
18+
CI gate detects in source.
19+
20+
## Schema extension for maa-framework: §(e) VENDORED
21+
22+
maa-framework carries an in-tree copy of the sibling estate repo
23+
`hyperpolymath/absolute-zero` at `absolute-zero/`. The canonical home of
24+
those proof files is the standalone `absolute-zero` repo, which has its
25+
own `docs/proof-debt.md` (seeded under the same standards#203 chain).
26+
27+
To avoid double-counting (and double-discharging) the same markers, we
28+
extend the schema with a fifth disposition:
29+
30+
| Disposition | Marker | Definition |
31+
| --- | --- | --- |
32+
| **(e) VENDORED — estate-sibling** | `// VENDORED: <canonical-repo>` | The marker lives in an in-tree copy of another estate repository. Disposition is **delegated** to the canonical repo's `docs/proof-debt.md`. Closing the marker upstream + re-vendoring is the close-out path. |
33+
34+
`(e)` is **out of scope** for maa-framework's own proof-debt close-out
35+
budget. The maintainers' obligation is just to keep the vendored copy
36+
fresh (re-sync periodically) and to flag if a marker disappears upstream
37+
but persists here.
38+
39+
The `(e)` extension is documented inline here per the standards#203
40+
policy's guidance: "extend the schema; document the extension at the
41+
top of the file as a repo-specific note." If the pattern recurs across
42+
other estate repos, it will be promoted into the central policy.
43+
44+
## Marker count (2026-05-27)
45+
46+
`scripts/check-trusted-base.sh`-style grep over `*.v / *.lean / *.agda /
47+
*.idr / *.fst / *.dfy / *.rs / *.hs`:
48+
49+
- **150 syntactic matches across 13 files** (the higher number vs the
50+
audit's "134" reflects a more inclusive regex; the audit excluded
51+
some comment/import false positives).
52+
- **All 13 files** live under `absolute-zero/proofs/{coq,lean4,agda}/`.
53+
- **All 13 files** are vendored from `hyperpolymath/absolute-zero` (the
54+
sibling estate repo). File-header comparison + author/license headers
55+
("Author: Jonathan D. A. Jewell; Project: Absolute Zero") confirm
56+
these are estate-owned but with canonical home in the sibling repo.
57+
- The two trees have drifted (e.g.
58+
`proofs/coq/lambda/LambdaCNO.v` differs from the sibling-repo copy);
59+
re-syncing is a follow-up.
60+
61+
Disposition split:
62+
63+
| Disposition | Files | Marker count | Notes |
64+
| --- | --- | --- | --- |
65+
| (a) DISCHARGED | 0 | 0 | — |
66+
| (b) BUDGETED | 0 | 0 | — |
67+
| (c) NECESSARY AXIOM | 0 | 0 | (See §(e). The axioms in those files are mostly genuine §(c)-class — physical constants, no-cloning, function-extensionality — but the canonical home is the sibling repo.) |
68+
| (d) DEBT | 0 | 0 | (PROOF-NEEDS.md flags `y_not_cno` `Admitted` as a known gap — that's also (e) since it lives in the vendored subtree.) |
69+
| **(e) VENDORED — estate-sibling** | **13** | **150** | All under `absolute-zero/`; canonical home `hyperpolymath/absolute-zero`. |
70+
71+
## (a) DISCHARGED in this repo
72+
73+
*(None — maa-framework itself contains no proof-bearing source outside
74+
the vendored `absolute-zero/` subtree.)*
75+
76+
## (b) BUDGETED — tested with a refutation budget
77+
78+
*(None — same reason as §(a).)*
79+
80+
## (c) NECESSARY AXIOM
81+
82+
*(None — same reason as §(a). Note: the axioms inside `absolute-zero/`
83+
(`kB_positive`, `temperature_positive`, `no_cloning`, the unitary-gate
84+
postulates, Shannon-entropy axioms, function-extensionality, etc.) are
85+
genuine §(c)-class candidates, but their canonical disposition lives in
86+
the sibling repo. See §(e).)*
87+
88+
## (d) DEBT — actively to be closed
89+
90+
*(None — same reason as §(a). `PROOF-NEEDS.md` notes a known `Admitted`
91+
on `y_not_cno` in `proofs/coq/lambda/LambdaCNO.v`; that file is in the
92+
vendored subtree (§(e)), so the discharge happens upstream in
93+
`hyperpolymath/absolute-zero`.)*
94+
95+
## (e) VENDORED — estate-sibling
96+
97+
All entries below have the form: `<vendored path> — <marker count> —
98+
<brief disposition rationale>`. The **canonical home** for every entry
99+
is `hyperpolymath/absolute-zero`; this file does not duplicate that
100+
repo's proof-debt classification.
101+
102+
### `absolute-zero/proofs/coq/` (7 files, 91 markers)
103+
104+
| File | Markers | Sample disposition (in sibling repo) |
105+
| --- | ---: | --- |
106+
| `absolute-zero/proofs/coq/quantum/QuantumCNO.v` | 35 | Mostly §(c): physical constants (`kB_positive`, `temperature_positive`), gate-unitarity (`X_gate_unitary`, `H_gate_unitary`, `CNOT_gate_unitary`), inner-product / `Cexp` algebra, `no_cloning`, `unitary_preserves_entropy`. |
107+
| `absolute-zero/proofs/coq/physics/StatMech.v` | 17 | §(c): Shannon-entropy non-negativity / maximum / point-zero, `landauer_principle`, `reversible_zero_dissipation`, physical constants. |
108+
| `absolute-zero/proofs/coq/physics/LandauerDerivation.v` | 14 | §(c): same family as `StatMech.v` plus `second_law`, `isothermal_work_bound`, `entropy_change_erasure`, `cno_preserves_shannon_entropy`. |
109+
| `absolute-zero/proofs/coq/filesystem/FilesystemCNO.v` | 13 | §(c): syscall semantics (`mkdir_rmdir_inverse`, `create_unlink_inverse`, `read_write_identity`, `chmod_identity`, `chown_identity`, `rename_inverse`, `snapshot_restore_identity`) — POSIX-spec assumptions standard in filesystem formalisations. |
110+
| `absolute-zero/proofs/coq/common/CNO.v` | 5 | §(c)+(d) mix: `eval_deterministic` (operational-semantics assumption), `cno_decidable` (decidability postulate), `eval_respects_state_eq_left/right` (one has a "TODO: Prove this axiom by induction on eval structure" comment — that's a (d) entry upstream). |
111+
| `absolute-zero/proofs/coq/lambda/LambdaCNO.v` | 5 | §(c): `y_not_cno` (Y-combinator non-termination — well-established but not derivable in pure Coq), `eta_equivalence`. **Note: PROOF-NEEDS.md targets `y_not_cno` for discharge; close upstream.** |
112+
| `absolute-zero/proofs/coq/quantum/QuantumMechanicsExact.v` | 4 | §(c): `X_gate_unitary`, `unitary_preserves_entropy`, `no_cloning` (subset of QuantumCNO.v). |
113+
| `absolute-zero/proofs/coq/category/CNOCategory.v` | 2 | §(c): `hom_functor` (Hom-functor functoriality, standard category-theory result). |
114+
115+
### `absolute-zero/proofs/lean4/` (4 files, 54 markers)
116+
117+
| File | Markers | Sample disposition (in sibling repo) |
118+
| --- | ---: | --- |
119+
| `absolute-zero/proofs/lean4/FilesystemCNO.lean` | 22 | §(c): Lean4 port of `FilesystemCNO.v` axioms — same family of syscall-semantics postulates plus `mkdir_test_not_identity`, `mkdir_idempotent`. |
120+
| `absolute-zero/proofs/lean4/StatMech.lean` | 15 | §(c): Lean4 port of `StatMech.v` plus `programState_eq_eval_fixpoint`, `state_preserving_dist`. |
121+
| `absolute-zero/proofs/lean4/QuantumCNO.lean` | 14 | §(c): Lean4 port of `QuantumCNO.v`. |
122+
| `absolute-zero/proofs/lean4/LambdaCNO.lean` | 3 | §(c): `subst_closed_term`, `y_combinator_not_identity`, `eta_equivalence`. |
123+
124+
### `absolute-zero/proofs/agda/` (1 file, 1 marker)
125+
126+
| File | Markers | Disposition |
127+
| --- | ---: | --- |
128+
| `absolute-zero/proofs/agda/EchoBridgeCNO.agda` | 1 | False positive on the strict grep — the single hit is `open import Axiom.Extensionality.Propositional`, which is a **module import** (the agda-stdlib path), not a `postulate`. Treat as resolved on close inspection. |
129+
130+
### One outlier on close inspection
131+
132+
The `EchoBridgeCNO.agda` count is a grep false positive
133+
(`Axiom.Extensionality.Propositional` is the agda-stdlib module path,
134+
not an axiom declaration). The real "load-bearing escape hatches" count
135+
across `absolute-zero/` is therefore **149**, not 150. Schema preserves
136+
the grep number for CI parity with `check-trusted-base.sh`.
137+
138+
## How to update this file
139+
140+
1. Re-run `bash scripts/check-trusted-base.sh .` (from standards#211)
141+
from the repo root.
142+
2. If markers in `absolute-zero/` change, the close-out path is to fix
143+
the canonical `hyperpolymath/absolute-zero` repo and re-sync into
144+
this subtree.
145+
3. If a **new** proof-bearing file appears **outside** `absolute-zero/`
146+
(e.g. under `aletheia/` for the Rust verification pipeline, or under
147+
`contractiles/`), classify it into §(a)/(b)/(c)/(d) per the canonical
148+
schema. That would be load-bearing maa-framework debt.
149+
150+
## Open owner question
151+
152+
1. **Vendoring policy**: should the `absolute-zero/` subtree be a git
153+
submodule (so the canonical proof-debt.md is the single source of
154+
truth) instead of a vendored copy? Current state is "in-tree copy
155+
that has drifted from the sibling repo's main branch". Filed for
156+
maintainer decision; this PR does not resolve it.
157+
2. **Re-sync cadence**: until the vendoring question is resolved,
158+
maa-framework's vendored copies should be diffed against the
159+
sibling repo before each minor release, and the diff annotated in
160+
`CHANGELOG.adoc`.
161+
162+
## Companion documents
163+
164+
- [`PROOF-NEEDS.md`](../PROOF-NEEDS.md) — the broader strategic proof
165+
narrative for maa-framework as a whole.
166+
- `hyperpolymath/standards`
167+
[`docs/TRUSTED-BASE-REDUCTION-POLICY.adoc`](https://github.com/hyperpolymath/standards/blob/main/docs/TRUSTED-BASE-REDUCTION-POLICY.adoc)
168+
— the canonical schema.
169+
- `hyperpolymath/standards`
170+
[`scripts/check-trusted-base.sh`](https://github.com/hyperpolymath/standards/blob/main/scripts/check-trusted-base.sh)
171+
— the CI gate.
172+
- `hyperpolymath/absolute-zero` `docs/proof-debt.md` — the canonical
173+
per-marker disposition for everything in §(e).
174+
175+
---
176+
177+
Initial seed under standards#203 + standards#211, 2026-05-27.

0 commit comments

Comments
 (0)