witnessFieldClauseCount
plain-language theorem explainer
Defines the integer count of witness-field clauses in the QG master-theorem non-circularity audit as six: two D2 fields, one D3, one D4, and two D5. Auditors and anyone citing the post-M3 clause census use this constant. The body is a bare natural-number definition, not a proof.
Claim. The number of witness-field clauses among the atoms of the unconditional RS quantum-gravity master statement is $6$, namely two D2 clauses, one D3 clause, one D4 clause, and two D5 clauses.
background
The module audits rs_quantum_gravity_master_unconditional field by field. A referee objection is that witness slots of shape $\Sigma(P:\mathrm{Prop}), P$ are inhabited by $\langle\mathrm{True},\mathrm{trivial}\rangle$, so the master theorem is only as strong as the concrete propositions in those slots. The audit classifies every atom as a trivial placeholder, an inhabited certificate, or a genuine witness-field clause, and proves each non-placeholder holds without assuming the master conclusion.
Witness-field clauses are the non-vacuous physics-bearing conjuncts (D2 through D5 in the audit numbering). The doc-comment fixes the census as D2 twice, D3, D4, and D5 twice. Downstream, the full 15-atom classification records zero placeholders, nine carried or certificate clauses, and these six witness-field clauses.
proof idea
Pure definition: the constant is the natural number $6$. No tactics, no lemmas, no reduction. Sibling counts (placeholderClauseCount, inhabited-cert counts) play the same role for the other classification bins.
why it matters
Feeds masterClauseClassification, which packages the post-M3 census of the fifteen atoms of RSQuantumGravityMaster: zero True placeholders, nine carried or certificate clauses, and six witness-field clauses, with a decide proof that the three bins sum to 15. That census is the quantitative answer to peer-review finding F1 / Rec 2: after M1–M3 the master conjunction is assembled from independently proved, named, non-self-referential propositions rather than vacuous placeholders. The count itself does not touch T0–T8, RCL, or the phi ladder; it only tallies how many master atoms sit in the witness-field bin of the gravity audit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.