T8_DimensionFourRoute_Equivalence
plain-language theorem explainer
Under the T8 hypothesis that spatial dimension is forced, this certificate packages four independent routes to D = 3 (linking, eight-tick, gap-sync, spinor) and records that every pair agrees on the same value. Anyone citing multi-route uniqueness of three-space in the forcing chain uses it. It is a Prop-valued structure (definitional certificate), not a proved theorem; the inhabiting instance is built separately.
Claim. Given a proof that spatial dimension is forced ($T8$), a four-route equivalence certificate is a proposition asserting: the physical dimension equals $3$; nontrivial linking forces $D=3$; matching the eight-tick period forces $D=3$; divisibility of the sync period by $2^D$ forces $D\le 3$; an RS spinor structure plus eight-tick forces $D=3$; each pairwise combination of linking, eight-tick, and spinor forces $D=3$; and full RS-compatibility of $D$ forces $D=3$.
background
The module UnifiedForcingChain assembles the complete inevitability chain from the cost foundation (Recognition Composition Law plus normalization and calibration) through T-1 and T0–T8. In that ladder, T7 is the eight-tick octave ($2^D$ with period 8) and T8 is the claim that spatial dimension is not free: $D=3$ is the unique value compatible with the ledger.
Upstream, T8_Dimension_Forced already states the core forcings: nontrivial linking implies $D=3$, eight-tick matching implies $D=3$, and there is a unique RS-compatible dimension. DimensionForcing supplies the predicates used here: SupportsNontrivialLinking (ledger conservation via nontrivial linking), EightTickFromDimension versus the fixed eight_tick period, sync_period for the gap-sync bound $2^D \mid$ sync_period, HasRSSpinorStructure, and the conjunction RSCompatibleDimension.
Constants fix the RS tick $\tau_0=1$ and the derived spatial dimension $D:=3$. This structure does not re-derive those facts; it organizes route agreement once T8 is assumed.
proof idea
No proof body: the declaration is a Prop-valued structure (certificate interface). Fields are named hypotheses about DimensionForcing predicates, not tactics. Propositional uniqueness of certificates for fixed T8 is immediate (Subsingleton via rfl). The separate theorem t8_dimension_four_route_equivalence inhabits the structure from a T8 instance by assigning D_physical_eq_three by rfl and wiring each route field to the corresponding DimensionForcing lemma (linking_requires_D3, eight_tick_forces_D3, and the gap-sync and spinor arguments).
why it matters
In the primer chain, T8 is "$D=3$ ← linking + gap-45 sync," with T7 the eight-tick octave $2^3$. This certificate is the bookkeeping layer that makes multi-route agreement explicit: linking, eight-tick, gap-sync, and spinor are not four independent numerology hits but pairwise-coherent forcings of the same $D=3$.
Downstream, t8_dimension_four_route_equivalence builds an instance from any T8_Dimension_Forced, and CompleteForcingChain consumes the T8 layer inside the full T-1…T8 package ("all of T0–T8 are forced from the cost foundation"). Without route equivalence, a referee could treat the four arguments as alternative models rather than one forced dimension. The structure closes that gap at the interface level so the complete chain can cite a single certificate shape.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.