carried_clauses_hold
plain-language theorem explainer
The three carried clauses of the quantum-gravity master theorem hold: the T0–T8 forcing chain, uniqueness of the recognition cost J, and unconditional BMV positivity. Anyone auditing non-circularity of the master statement cites this packaging lemma. The proof is a pure term constructor that pairs the three independently proved theorems.
Claim. The T0–T8 forcing chain holds, the recognition cost functional is uniquely $J$ (under the standard reciprocity, normalization, composition, calibration, and continuity hypotheses), and the pure two-qubit BMV entropy-concurrence positivity statement holds unconditionally.
background
This module is a field-by-field non-circularity audit of the unconditional quantum-gravity master theorem. A referee objection was that witness slots of shape $\Sigma(P:\mathrm{Prop}),P$ can be filled by trivial placeholders. After M1–M3 the master statement carries three concrete propositions rather than True: the T0–T8 substrate-forcing conjunction, the universal J-cost uniqueness theorem, and the pure two-qubit entropy positivity theorem.
T0–T8 is the Foundation forcing chain (J-uniqueness, $\varphi$ as self-similar fixed point, eight-tick octave, $D=3$, and the earlier T0–T4 steps). Cost uniqueness is the statement that any $F$ satisfying reciprocity, normalization, the Recognition Composition Law, calibration, and continuity equals the J-cost $J(x)=(x+x^{-1})/2-1$. BMV positivity is the unconditional pure-two-qubit entropy-concurrence theorem from the Quantum layer.
Each clause is exposed both as a named proposition and as a standalone proof that does not assume any master-theorem conjunct.
proof idea
Term-mode triple constructor. The goal is the conjunction of the three carried propositions. It is inhabited by pairing T0_T8_holds_proven (itself the eight-component package of Foundation.UnifiedForcingChain.t0_holds through t8_holds), CostUniqueness_proven (which applies Cost.FunctionalEquation.law_of_logic_forces_jcost under the reciprocity/normalization/composition/calibration/continuity hypotheses), and bmv_positive_unconditional_proven (which is pure_two_qubit_entropy_positive_unconditional). No further tactics or rewriting.
why it matters
This is the atomic conjunction that the non-circularity certificate consumes. Downstream, master_theorem_non_circularity_certificate records that the three carried clauses equal their concrete proposition surfaces, that they hold, that the six closed certificate clauses hold by inhabitation, and that the five witness inputs are unconditional. Without this packaging step the audit cannot assert that the master conclusion is assembled from independently proved, non-self-referential atoms.
Framework landmarks touched: the full T0–T8 forcing chain (including T5 J-uniqueness, T6 $\varphi$, T7 eight-tick octave, T8 $D=3$), the Recognition Composition Law underlying cost uniqueness, and the BMV positivity input used in the holographic/entropy side of the master theorem. It closes the peer-review finding that those three slots were formerly trivial placeholders.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.