T8_To_T7_EightTick_Bridge
plain-language theorem explainer
Packages the reverse bridge from forced spatial dimension D = 3 back to the eight-tick cadence: every RS-compatible dimension equals 3, satisfies 2^D = 8, and the concrete identity 2^3 = 8 holds. Cited by the complete T−1..T8 forcing spine and by the T6→T7 route-equivalence certificate that equates the direct and via-dimension paths. It is a Prop-structure of three fields, not a proved theorem; the inhabitant is built separately from T8's linking and eight-tick forcing clauses.
Claim. Given that spatial dimension is forced ($D = 3$ from linking, eight-tick, and uniqueness of an RS-compatible dimension), the T8-to-T7 bridge asserts: (i) every RS-compatible dimension equals $3$; (ii) every RS-compatible dimension satisfies $2^D = 8$; (iii) the concrete identity $2^3 = 8$ holds. Here RS-compatible means the dimension supports nontrivial linking, carries the eight-tick equation, gap-sync divisibility, and the cellular/one-acyclic substrate package.
background
The module exposes the public T−1 through T8 forcing spine and stops before private operator/measurement layers. T7 is the eight-tick cadence from dimension; T8 is $D = 3$ from linking, eight-tick, and gap-sync compatibility.
In DimensionForcing, spatial dimension is a natural number, eight_tick is the constant $8$, and EightTickFromDimension D := 2^D. An RS-compatible dimension must support nontrivial linking (ledger conservation), satisfy $2^D = 8$, divide the gap-sync period, and carry the cellular-completion / one-acyclic substrate package used by the realization route.
The hypothesis T8_Dimension_Forced already records three facts: linking forces $D = 3$, the eight-tick equation forces $D = 3$, and there is a unique RS-compatible dimension. This bridge structure is the interface that re-exports those consequences in the form T7 consumers expect: compatibility implies $D = 3$ and $2^D = 8$, plus the bare identity at $D = 3$.
proof idea
No proof body: this is a Prop-valued structure definition with three fields. Inhabitants are constructed elsewhere (e.g. t8_to_t7_bridge_holds). That theorem fills the fields by: (1) reducing compatible-dimension-three to T8's linking_forces_D3 on the linking component of RS-compatibility; (2) reducing compatible-dimension-eight-tick to the eight-tick field already present in RS-compatibility; (3) discharging dimension-three-eight-tick by direct evaluation of $2^3 = 8$. The structure itself only names the certificate surface.
why it matters
Closes the T8 → T7 arrow on the public forcing spine. Downstream, CompleteForcingChainT8 and UnifiedForcingChain.CompleteForcingChain include this bridge so the full T−1..T8 chain can cite eight-tick as a consequence of forced dimension rather than an independent axiom. T6_To_T7_RouteEquivalence uses it to show the indirect route T6 → T8 → T7 matches the direct canonical-period T6 → T7 route.
Framework landmarks: T8 ($D = 3$) and T7 (eight-tick octave, period $2^3$). The UnifiedForcingChain copy of this bridge stresses the intended logical order: Alexander-duality linking pins $D = 3$ first; the eight-tick identity is then a consequence of the dimension, not a premise used to prove the dimension. That ordering matters for anyone auditing whether the octave is forced or assumed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.