T0_T8_carried_prop
plain-language theorem explainer
Defines the substrate-forcing clause of the gravity master theorem as the bare conjunction of the nine T0–T8 forcing surfaces (logic, meta-principle, discreteness, ledger, recognition, J-uniqueness, φ, eight-tick, D=3). Gravity and audit modules cite it as the concrete D1 atom. It is a pure Prop abbreviation, not a proof.
Claim. Let $P_{T0\text{–}T8}$ be the proposition that logic is forced as the zero/positive split of recognition work, the meta-principle is forced, discreteness of the Boolean floor is forced, the ledger is forced, recognition is forced, the cost $J$ is unique, $\varphi$ is the self-similar fixed point, the eight-tick octave is forced, and spatial dimension $D=3$ is forced. Then $P_{T0\text{–}T8}$ is exactly that nine-fold conjunction.
background
Track 7.A authors the quantum-gravity master statement as a twelve-clause conjunction. Eight clauses are closed; five remain hypothesis inputs. The first closed piece is the substrate-forcing spine T0–T8 from the unified forcing chain.
T0 identifies logic with the zero/positive split of recognition cost on Bool. T1 forces the meta-principle. T2 forces discreteness of the normalized two-point Boolean floor. T3–T4 force the ledger and recognition structure. T5 forces uniqueness of the J-cost $J(x)=(x+x^{-1})/2-1$. T6 forces $\varphi$ as the self-similar fixed point. T7 forces the eight-tick octave (period $2^3$). T8 forces $D=3$ spatial dimensions.
The larger CompleteForcingChain package introduces universe metavariables. This definition packages only the nine concrete theorem surfaces so the master atom can carry them transitively without that baggage.
proof idea
No proof: this is a definitional abbreviation. The body is the nine-fold And of the named forcing surfaces T0_Logic_Forced through T8_Dimension_Forced from Foundation.UnifiedForcingChain (via the TMinus1–T8 bridge abbrevs). Inhabitation is deferred to the sibling T0_T8_holds / T0_T8_holds_proven layer, which cites the concrete chain theorems.
why it matters
This is the concrete Prop behind the D1 substrate-forcing clause of rs_quantum_gravity_master. Downstream, T0_T8_holds is definitionally equal to it; the non-circularity audit proves T0_T8_holds = T0_T8_carried_prop by rfl and records that the clause carries the full T0–T8 theorem-surface conjunction. That audit also certifies the master theorem does not smuggle circular assumptions through this atom.
Framework landmarks: the whole forcing chain T0–T8 (J-uniqueness, φ, eight-tick octave, D=3) is exactly what this Prop packages. It does not close the five open master hypotheses (classical continuum/Bianchi, unconditional amplitude linearity, Page curve, PTA stochastic GW, strong-field tests); those remain separate inputs to the conditional master theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.