all_witness_fields_hold
plain-language theorem explainer
The five canonical gravity-master witnesses hold as standalone propositions: Regge-to-EH continuum plus contracted discrete Bianchi, amplitude linearity, nontrivial Page curve, PTA-vs-inflation separation, and strong-field GR-distinct signals. Non-circularity auditors cite this to show the unconditional master theorem consumes only independently proved physics. The proof is a six-component product of each witness's own holds field.
Claim. The six propositions carried by the five canonical master-theorem witnesses all hold: the Regge continuum limit to the Einstein-Hilbert action, the contracted discrete Bianchi identity, unconditional many-body amplitude linearity, the derived nontrivial Page curve, PTA stochastic gravitational-wave distinctness from inflation, and strong-field observation-channel distinctness from pure GR.
background
This module answers a formal-methods referee objection to the unconditional quantum-gravity master theorem. Witness structures of shape $\Sigma(P:\mathrm{Prop}),P$ are inhabited even by $\langle\mathrm{True},\mathrm{trivial}\rangle$, so the master statement is only as strong as the concrete propositions in its five witness slots. The audit discloses each field by inspection and proves it holds without assuming any master clause.
The five canonical witnesses live in the unconditional master module. The primary D2 witness packages a physical product-filter Regge-to-Einstein-Hilbert continuum theorem with a Schläfli-based contracted discrete Bianchi identity. D3 is the theorem-built amplitude-linearity witness. D4 is the nontrivial Page process on $\mathrm{Fin},2\otimes\mathrm{Fin},2$ (interior peak $S_{BH}/2$, monotone rise and fall), superseding the degenerate $\mathrm{Fin},1$ route. PTA and strong-field witnesses are typed observation-channel signal models with formula-level separation from inflation and pure GR respectively.
Local classification distinguishes trivial placeholders (definitionally $\mathrm{True}$) from inhabited certificates and carried theorem-surface propositions. This declaration covers only the five witness inputs.
proof idea
Term-mode six-tuple. Each conjunct is the corresponding field of a canonical witness structure, discharged by that witness's own proof field: regge_holds and bianchi_holds from the Regge/EH+Bianchi witness, then holds from the amplitude-linearity, Page-curve, PTA, and strong-field witnesses in order. No rewriting, no master clause, no extra lemmas beyond those already sealed inside the canonical constructions.
why it matters
This is the non-circularity core for the witness half of the QG master theorem. Downstream, master_theorem_non_circularity_certificate conjoins it with carried T0-T8, cost-uniqueness (J-uniqueness from the forcing chain), BMV-positivity, six closed certificate inhabitations, and a non-vacuous D4 Page field. The parent certificate's clause 5 is exactly this result: the five witness inputs hold unconditionally, with no master clause assumed.
Peer-review findings F1/Rec 2 demanded proof that witness slots are genuine physics rather than conclusion-bearing or trivial. By routing only through standalone holds fields of named canonical witnesses, the assembly of the master conjunction cannot smuggle RSQuantumGravityMaster into its hypotheses. Framework landmarks touched indirectly via the carried T0-T8 side of the parent certificate include the forcing chain through D=3 and J-cost uniqueness; this declaration itself stays on the gravity-witness side (Regge/EH, Bianchi, Page, PTA, strong field).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.