Coq: 73 of 182 theorems rest on axioms and the 38 Axiom/Parameter declarations use four tag forms — unify the tag grammar, generate the census

[hyperpolymath]

Finding (measured 2026-09-23 on main @ dd87b48, Coq 8.18, Print Assumptions over every top-level theorem)

The 17 theorems PROOF-STATUS.adoc names in backticks are all Closed under the global context — that is now CI-gated by proofs/coq/check-assumptions.sh (PR for phase 4b–4d). The rest of the tree is not closed, and the prose in PROOF-STATUS.adoc ("Remaining axioms are exactly: (a) tagged physical postulates … (b) the class-A items listed above") cannot be checked because the axiom declarations do not share a tag grammar.

Census: 182 top-level Theorem/Lemma/Corollary/Proposition across the 14 theories — 109 closed, 73 rest on at least one axiom.

theory	theorems	closed	axiom-dependent
CNO	26	26	0
CNOCategory	7	6	1
Complex	18	1	17
FilesystemCNO	33	33	0
LambdaCNO	13	13	0
LandauerDerivation	5	0	5
MalbolgeCore	7	7	0
OND	17	17	0
QuantumCNO	39	2	37
QuantumMechanicsExact	5	0	5
StatMech	9	1	8
StatMech_helpers	3	3	0

Axioms that appear in the 73 non-closed blocks (count = number of theorems depending on it):

axiom	theorems
ClassicalDedekindReals.sig_forall_dec	68
FunctionalExtensionality.functional_extensionality_dep	60
ClassicalDedekindReals.sig_not_dec	32
StatMechBasis.shannon_entropy	12
PhysicsConstants.kB	8
Classical_Prop.classic	8
StatMechBasis.state_dec	4
PhysicsConstants.temperature	4
StatMechBasis.shannon_entropy_point_zero	3
PhysicsConstants.kB_positive	3
LandauerDerivation.shannon_entropy_uniform_max	3
StatMech.reversible_zero_dissipation	2
StatMech.energy_dissipated_phys	2
StatMechBasis.shannon_entropy_nonneg	2
QuantumCNO.unitary_inverse_property	2
QuantumCNO.unitary_inverse	2
LandauerDerivation.isothermal_work_bound	2
LandauerDerivation.internal_energy	2
QuantumCNO.reversible_quantum_zero_dissipation	1
QuantumCNO.quantum_energy_dissipated	1
QuantumCNO.measure	1
ProofIrrelevance.proof_irrelevance	1
PhysicsConstants.temperature_positive	1
LandauerDerivation.eval_to_dec	1
LandauerDerivation.cno_preserves_shannon_entropy	1
LandauerDerivation.all_states	1

The 38 Axiom/Parameter declarations (QuantumCNO.v 12, LandauerDerivation.v 11, StatMechBasis.v 6, StatMech.v 4, PhysicsConstants.v 4, LambdaCNO.v 1) are annotated in at least four different forms within the three lines above the declaration — (* TRUSTED: unsound class-A debt …, (* TRUSTED: class-A debt …, (* METAL-BOUNDARY (kept): …, (* METAL-BOUNDARY AXIOM (kept): …, (* Opaque [Parameter]: …, (* AXIOM: … — and grep -B3 finds a recognisable tag on only 10 of the 38. Nothing machine-checks that a declaration is tagged at all.

Two declarations (prob_nonneg, prob_normalized in common/StatMechBasis.v) are tagged "TRUSTED: unsound class-A debt" while PROOF-STATUS.adoc says every class-A item is "true, provable in principle". The census shows zero theorems depend on either today, so they are dead weight rather than a soundness hole — but the tag and the prose contradict each other.

Acceptance criteria

1. One tag grammar. Every top-level Axiom/Parameter/Hypothesis is immediately preceded by exactly one tag of a fixed form, e.g. (* AXIOM[METAL-BOUNDARY|CLASS-A|STDLIB-CLASSICAL]: <reason> *). A checker (proofs/coq/check-axiom-tags.sh, bash/awk — no Python/Deno) fails on any untagged declaration or unknown class and runs in the Coq CI job. Its positive control: a scratch file with an untagged Axiom must turn it red.
2. The two "unsound" declarations are discharged, deleted, or retagged with a written reason; the prose in PROOF-STATUS.adoc and the tag must agree.
3. The census is generated, not hand-written. proofs/coq/census-assumptions.sh emits the per-theory table and axiom tally above from the tree; PROOF-STATUS.adoc "Honest scope" cites those numbers (109/182 closed today) instead of "remaining axioms are exactly …".
4. Advisory first, gate second. The Coq CI job runs the census as a logged artefact until 1–3 land; then it becomes a gate that allow-lists the Coq stdlib axioms (ClassicalDedekindReals.*, FunctionalExtensionality.*, Classical_Prop.classic, ProofIrrelevance.*) plus the tagged project parameters and fails on anything else.

Evidence: the census run (coqc on a generated file of 182 Print Assumptions lines, exit 0) is reproducible from the script in AC3; the 17-theorem gate and its --control (which proves the gate rejects landauer_limit_positive via PhysicsConstants.kB_positive) are in the 4b–4d PR.

🤖 Generated with Claude Code