masterClauseClassification
plain-language theorem explainer
After M3, the fifteen atoms of the RS quantum gravity master conjunction split as zero True placeholders, nine carried or certificate clauses, and six witness-field clauses. Gravity auditors cite this aggregate when checking that the master statement is not secretly self-referential. The definition is a structure instance that plugs in the three count constants and discharges the sum by decide.
Claim. The master clause classification is the triple of natural numbers $(0, 9, 6)$ with total $15$, satisfying $0 + 9 + 6 = 15$: zero definitional-$\mathrm{True}$ placeholders, nine inhabited-certificate (carried) clauses, and six witness-field clauses among the fifteen atoms of the RS quantum gravity master conjunction after M3.
background
The module is a field-by-field non-circularity audit of the unconditional RS quantum gravity master theorem. A formal-methods referee objected that witness slots of shape $\Sigma(P:\mathrm{Prop}), P$ can be filled by $\langle\mathrm{True}, \mathrm{trivial}\rangle$, so the master claim is only as strong as the concrete propositions in those slots. The audit discloses each atom and proves it holds without assuming the master conclusion.
Classification key: trivial placeholders are definitionally True (weaker than prose may suggest); inhabited certificates are Nonempty of an explicit certificate structure; witness-field clauses are the concrete continuum or lattice field propositions (e.g. the fixed nonconstant $C^2$ field $f(p)=\sin(2\pi p_0)$ on $\mathbb{R}^3$).
ClauseClassification packages three counts plus a decide-checked total. Sibling counts fix placeholders at 0, inhabited certificates at 9, and witness-field atoms at 6 (D2 twice, D3, D4, D5 twice).
proof idea
Pure structure instance: assign the three named count definitions (0, 9, 6), set total to 15, and prove the additive identity by decide. No lemmas beyond the count defs and decidable arithmetic on naturals.
why it matters
This is the single aggregate snapshot the audit uses to answer the referee: after M1–M3, T0–T8, cost-uniqueness, and BMV-positivity are no longer True placeholders; they are carried propositions, and the remaining atoms are either explicit certificates or named witness fields. Downstream, masterClauseClassification_total re-exports the equality $0+9+6=15$ as a one-line decide theorem, feeding the module’s one-statement non-circularity certificate. In framework terms it records that the gravity master conjunction is assembled from independently proved, non-self-referential pieces rather than from vacuous witnesses, closing the circularity objection without touching the T0–T8 forcing content itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.