t0t8_clause_is_complete_forcing_chain
plain-language theorem explainer
Definitional equality: the master theorem's T0–T8 atom is exactly the concrete conjunction of the UnifiedForcingChain theorem surfaces T0 through T8, not True or a self-referential package. Auditors of rs_quantum_gravity_master_unconditional cite this to confirm the substrate-forcing slot is non-vacuous and non-circular. Proof is pure rfl from the def of T0_T8_holds.
Claim. By definition, the proposition "the T0–T8 forcing chain holds" is identical to the concrete carried conjunction $T0\_\mathrm{Logic}\_\mathrm{Forced} \land T1\_\mathrm{MP}\_\mathrm{Forced} \land \cdots \land T8$ (spatial dimension forced), i.e. the full UnifiedForcingChain theorem-surface package rather than a placeholder.
background
This module is a field-by-field non-circularity audit of the quantum-gravity master theorem. A referee objection is that witness slots of shape $\Sigma(P:\mathrm{Prop}), P$ can be inhabited by $\langle\mathrm{True},\mathrm{trivial}\rangle$, so "unconditional" strength depends entirely on which propositions are plugged in. For each atom the audit therefore discloses, by definitional equality, what proposition the field actually is, and separately proves that field holds without assuming the master conclusion.
Upstream, T0_T8_carried_prop is the concrete conjunction of the Foundation.UnifiedForcingChain surfaces (T0 logic forced through T8, $D=3$), chosen to avoid universe metavariables from the larger CompleteForcingChain package while still transitively carrying those theorem surfaces. T0_T8_holds is defined to be exactly that carried proposition: the substrate-forcing piece of D1.
The forcing chain itself is the RS landmark spine: J-uniqueness (T5), $\varphi$ as self-similar fixed point (T6), eight-tick octave (T7), and three spatial dimensions (T8).
proof idea
One-line term proof by rfl. Because T0_T8_holds is defined as T0_T8_carried_prop, the equality of the two propositions is definitional; no lemmas are applied and no hypotheses are opened.
why it matters
Feeds directly into master_theorem_non_circularity_certificate, whose first conjunct is this equality together with the claim that the T0–T8 clause holds. That certificate is the peer-review answer to findings F1 / Rec 2: after M1 the T0–T8 slot is no longer a True placeholder but carries the named forcing-chain conjunction, assembled from independently proved, non-self-referential surfaces.
In framework terms this locks the master theorem's substrate atom to the T0–T8 forcing chain (J-cost uniqueness, $\varphi$, eight-tick period $2^3$, $D=3$). Without this disclosure, the unconditional QG master statement could silently weaken to a vacuous witness. The audit records the honest upgrade path: carried concrete props, then standalone holds proofs, then the bundled non-circularity certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.