master_theorem_non_circularity_certificate
plain-language theorem explainer
Field-by-field non-circularity certificate for the unconditional RS quantum-gravity master theorem: every atom is either a carried T0–T8 / J-cost / BMV proposition, an inhabited closed certificate, or an independently proved witness, and none equals the master conclusion. Referees auditing circularity objection F1 cite this. Term proof packages clause disclosures, carried holds, closed certs, witness fields, and the master assembly.
Claim. The T0–T8 forcing-chain clause equals its carried proposition and holds; J-cost uniqueness equals its carried proposition and holds; BMV two-qubit entropy positivity equals its carried proposition and holds; the six closed certificates (Lorentzian $1{+}3$, Hawking temperature in SI, $c_{\mathrm{RS}}$ distinctness, $\omega_\Lambda$ from $\varphi$, QNM distinct from LQG/string, gravity sector with zero free parameters) hold; the five witness fields (Regge–EH continuum and discrete Bianchi, amplitude linearity forced, Page curve derived, PTA distinct from inflation, strong-field distinct from GR-only) hold unconditionally; therefore the RS quantum-gravity master theorem holds on those witnesses.
background
This module answers a formal-methods referee objection (F1) to the unconditional quantum-gravity master theorem. Witness structures of shape $\Sigma(P:\mathrm{Prop}),P$ are content-free if $P$ is True or secretly the master conclusion. The audit therefore discloses, for every atom, what proposition the field definitionally is, and proves each atom holds without assuming any master clause.
After prior repairs, three formerly placeholder clauses now carry real content: T0–T8 is the complete forcing-chain conjunction (through J-uniqueness, $\varphi$, the eight-tick octave, and $D=3$); cost uniqueness is universal J-cost uniqueness from the Recognition Composition Law (T5 / d'Alembert forcing); BMV positivity is pure two-qubit von Neumann entropy positivity under unit Frobenius norm and positive concurrence.
Closed certificates include the SI Hawking law $T=\hbar c^3/(8\pi G k_B M)$, the ringdown coefficient $c_{\mathrm{RS}}=-\log\varphi/2$ separated from LQG $-1/2$ and string $-3/2$, and zero free parameters in the gravity sector. Five witness bundles supply continuum Regge–EH plus discrete Bianchi, forced linear amplitudes, a derived Page curve, and PTA / strong-field discriminators.
proof idea
Pure term-mode quadruple product. First conjunct: t0t8_clause_is_complete_forcing_chain and the two analogous *_clause_is_carried lemmas give definitional equality of each master clause to its carried proposition; carried_clauses_hold supplies the three truth proofs. Second: closed_certs_hold packages the six inhabited certificates (Lorentzian, Hawking SI, $c_{\mathrm{RS}}$, $\omega_\Lambda(\varphi)$, QNM discriminator, zero free parameters). Third: all_witness_fields_hold discharges the five witness-structure fields unconditionally. Fourth: rs_quantum_gravity_master_unconditional assembles the master theorem on the canonical witnesses. No tactics beyond pairing.
why it matters
Discharges peer-review finding F1 / Rec 2 at field granularity: a referee can read each field's definition and confirm none is the master conclusion, then check each holds by an independent proof. This is the audit capstone for the gravity-sector master theorem, tying the forcing chain (T0–T8), J-cost uniqueness via the Recognition Composition Law, and BMV entropy positivity into one non-self-referential package alongside Hawking SI, $c_{\mathrm{RS}}$ spectroscopy margins, and zero free parameters.
Downstream use is presently empty (certificate endpoint). Upstream it rests on rs_qnm_distinct_LQG_string, hawking_temperature_SI, the carried BMV and CostUniqueness props, and the unconditional master assembly. Framework landmarks hit directly: T5 J-uniqueness, T6 $\varphi$, T7 eight-tick, T8 $D=3$, and the gravity master plan tracks for QNM, Page curve, and PTA discriminators.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.