inhabitedCertClauseCount
plain-language theorem explainer
After the M3 audit pass, exactly nine atoms of the quantum-gravity master conjunction are classified as carried or certificate-closed clauses (not True placeholders and not raw witness fields). Gravity auditors cite this constant when tallying the master statement’s non-circular content. The body is the literal natural number nine.
Claim. The number of carried or certificate-closed clauses among the atoms of the unconditional quantum-gravity master conjunction, after the M3 non-circularity audit, equals $9$.
background
The module audits rs_quantum_gravity_master_unconditional against a formal-methods objection: witness slots of shape $\Sigma(P:\mathrm{Prop}),P$ are inhabited by $\langle\mathrm{True},\mathrm{trivial}\rangle$ and carry no physics unless the plugged-in propositions are genuine, independently proved, and non-self-referential.
Classification key (module header): trivialPlaceholder means the clause is definitionally True and the cited theorem is not transitively carried; inhabitedCert means the clause is Nonempty C for an explicit certificate structure $C$. After M1–M3 the T0–T8, cost-uniqueness, and BMV-positivity slots are carried propositions rather than True.
Sibling counters track placeholders and witness-field atoms. Downstream, the three counts must sum to the fifteen atoms of the master conjunction.
proof idea
Pure definition: the constant is the natural number literal $9$. No tactic proof, no lemma application. The value is the audited tally of inhabitedCert atoms after M3, consumed by equality checks in the clause-classification record.
why it matters
Feeds masterClauseClassification, which records the post-M3 split of the fifteen master atoms: zero True placeholders, nine carried/certificate clauses, six witness-field clauses (total fixed by decide). That classification is the quantitative answer to peer-review finding F1 / Rec 2: the unconditional master theorem is only as strong as the concrete propositions in its slots, and nine of those slots are now certificate-backed rather than vacuous.
In the broader Recognition gravity stack this supports the claim that the master conjunction is assembled from independently discharged, named physics (Regge–EH product-filter content, hinge-aware zero modes, gap-layer structure, and related certificates) rather than from a circular packaging of its own conclusion. It does not itself invoke T0–T8, RCL, or the phi ladder; it only counts how many master atoms have been closed at the certificate level.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.