masterClauseClassification_total
plain-language theorem explainer
The master-clause audit partitions every atom of the quantum-gravity master conjunction into exactly three buckets (trivial placeholders, inhabited certificates, witness fields), and those three Nat counters sum to 15. Anyone checking that the non-circularity audit is exhaustive cites this equality. The proof is a one-line `decide` on the concrete classification record.
Claim. In the master-clause classification record, the number of trivial-placeholder clauses plus the number of inhabited-certificate clauses plus the number of witness-field clauses equals $15$.
background
This module is a field-by-field non-circularity audit of the unconditional RS quantum-gravity master theorem. A formal-methods referee objected that witness structures of shape $\Sigma(P:\mathrm{Prop}), P$ carry no content unless the plugged-in propositions are named, independently proved, and free of the master conclusion itself.
The audit therefore classifies every atom of the master conjunction under a three-way key drawn from the module doc: trivial placeholders (definitionally True, real content living elsewhere), inhabited certificates (Nonempty C discharged by an explicit construction), and witness fields (unconditional inputs that do not assume any master clause). Sibling lemmas disclose and discharge the T0–T8, cost-uniqueness, and BMV-positivity carried propositions, the closed certificate clauses, and the five witness inputs.
The classification record exposes three Nat counters for those buckets. Totality of the partition is the claim here: nothing in the 15-atom conjunction is left unclassified.
proof idea
One-line computational proof. The three fields of the classification record are concrete natural numbers fixed by the audit definitions; decide evaluates the sum and checks equality with 15. No lemmas are invoked beyond the decidability instance on Nat equality.
why it matters
Without a total count, a referee could still ask whether some master atom escaped the audit and quietly reintroduced circularity. This equality closes that gap: every clause is in exactly one of the three disclosed buckets, matching the non-circularity certificate's inventory (carried T0–T8 / cost-uniqueness / BMV clauses, six closed certificates, five unconditional witnesses, and the remaining named fields that bring the total to 15).
It sits at the end of the Gravity non-circularity audit chain that answers peer-review finding F1: the unconditional master theorem is assembled from independently proved, concretely named, non-self-referential propositions rather than from a vacuous $\Sigma(P),P$ shell. No downstream theorem currently depends on it; it is a referee-facing completeness check, not a physics derivation step. Framework landmarks T0–T8 and J-cost uniqueness appear only as named carried clauses elsewhere in the module, not inside this arithmetic identity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.