ClauseClassification
plain-language theorem explainer
A four-field tally that partitions the fifteen atomic clauses of the quantum-gravity master statement into placeholders, inhabited certificates, and witness-field propositions, with an equality forcing the three counts to sum to the total. Auditors of the non-circularity claim cite it to record how much of the master conjunction is genuine content versus trivial True. The structure is pure data plus a decidable arithmetic identity.
Claim. A clause classification is a record of four natural numbers $p$, $c$, $w$, $T$ together with a proof that $p + c + w = T$, where $p$ counts trivial $\mathsf{True}$ placeholders, $c$ counts inhabited certificate clauses, and $w$ counts witness-field clauses among the atoms of the quantum-gravity master conjunction.
background
The ambient module is a field-by-field non-circularity audit of the unconditional quantum-gravity master theorem. A formal-methods referee objected that witness structures of shape $\Sigma(P:\mathrm{Prop}),P$ can be inhabited by $\langle\mathsf{True},\mathrm{trivial}\rangle$, so the master statement is only as strong as the concrete propositions in its slots. The audit answers by disclosing each atom and proving it holds without assuming the master conclusion.
Classification key (from the module): a trivial placeholder is definitionally $\mathsf{True}$ and does not transitively carry the cited physics; an inhabited certificate is $\mathrm{Nonempty},C$ for an explicit certificate structure $C$; a witness-field clause packages a concrete analytic or geometric witness (for example the fixed nonconstant $C^2$ field $f(p)=\sin(2\pi p_0)$ used in continuum energy limits).
The master statement itself is the large conjunction matching the Track 7.A template: T0–T8 and cost uniqueness, Lorentzian signature, Regge-to-Einstein–Hilbert continuum limit with discrete Bianchi, amplitude linearity and BMV positivity, Hawking temperature, and several observational distinctness clauses. After M1–M3 the T0–T8, cost-uniqueness, and BMV clauses are carried propositions rather than $\mathsf{True}$.
proof idea
No proof body: this is a structure declaration. It packages three category counts and a total, plus a single equality field total_eq asserting that the three summands equal the total. Downstream instances discharge that equality by decide on concrete numerals (for the master audit: $0+9+6=15$).
why it matters
This structure is the type of the audit's headline tally masterClauseClassification, which records that after M3 the fifteen atoms of the quantum-gravity master statement split as zero True placeholders, nine carried or certificate clauses, and six witness-field clauses. That split is the quantitative answer to peer-review findings F1 / Rec 2: non-circularity follows once every atom is independently proved and none is the master conclusion itself.
In the Recognition framework the master conjunction is the gravity-side packaging of the forcing chain (T0–T8, including J-uniqueness, $\varphi$, the eight-tick octave, and $D=3$) together with continuum and observational closures. The classification does not prove those physics results; it certifies that the master theorem's logical surface area is honest about what it carries.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.