placeholderClauseCount
plain-language theorem explainer
Records that after the M3 upgrade the quantum-gravity master conjunction contains zero definitionally-True placeholder clauses. Auditors and anyone citing the non-circularity classification use this constant. The body is the numeral 0; no proof work is involved.
Claim. The number of trivial $\mathrm{True}$ placeholder atoms remaining in the quantum-gravity master conjunction after the M3 upgrade equals $0$.
background
The module audits rs_quantum_gravity_master_unconditional field by field against a referee objection: witness slots of shape $\Sigma(P:\mathrm{Prop}), P$ can be filled by $\langle\mathrm{True},\mathrm{trivial}\rangle$ and then carry no physics. Each atom of the master conjunction is therefore classified as a trivial placeholder, an inhabited certificate, or a carried proposition, and each is shown to hold without assuming the master conclusion.
After M1–M3 the T0–T8 forcing chain, cost-uniqueness, and BMV-positivity slots are no longer True; they are the named carried propositions T0_T8_carried_prop, CostUniqueness_carried_prop, and bmv_positive_unconditional_carried_prop. This definition is the residual count of any still-trivial atoms under that classification key.
proof idea
Pure definitional binding: the natural-number constant is set to the numeral 0. No tactics, lemmas, or reduction steps appear. Downstream code treats the value as the placeholder field of the clause-classification record.
why it matters
Feeds masterClauseClassification, which packages the fifteen atoms of RSQuantumGravityMaster after M3 as 0 True placeholders, 9 carried/certificate clauses, and 6 witness-field clauses (total fixed by decide). The zero count is the quantitative half of the non-circularity claim: the master conclusion is assembled only from independently proved, concretely named, non-self-referential propositions, not from hidden True fillers. It closes the peer-review finding that earlier master statements overstated what they carried relative to the T0–T8 chain and related gravity certificates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.