t8_to_canonical_dimension_bridge_holds
plain-language theorem explainer
From a T8 certificate that spatial dimension is forced, this builds the canonical dimension bridge naming $D_{\mathrm{physical}}=3$ and recording bidirectional RS-compatibility plus the linking, eight-tick, and spinor forcing routes. Anyone wiring the complete forcing chain or the extended ultimate-inevitability surface cites it. The proof is a structure constructor: reflexivity for the named equalities, DimensionForcing lemmas for compatibility and uniqueness routes, and the T8 uniqueness field passed through.
Claim. Given a certificate that spatial dimension is forced (nontrivial linking implies $D=3$, eight-tick synchronization implies $D=3$, and there is a unique RS-compatible dimension), there is a canonical dimension bridge asserting $D_{\mathrm{physical}}=3$, that both $D_{\mathrm{physical}}$ and $3$ are RS-compatible, that every RS-compatible dimension equals $3$, that the period at $D_{\mathrm{physical}}$ and the eight-tick period at three agree, and that linking, eight-tick, and spinor routes each force $D=3$.
background
The Unified Forcing Chain module shows T0–T8 as inevitabilities from the Recognition Composition Law plus normalization and calibration. T8 is the dimension step: spatial dimension is not a free parameter. The structure T8_Dimension_Forced packages three claims: nontrivial linking (ledger conservation) forces $D=3$; the eight-tick identity $2^D=8$ forces $D=3$; and there is a unique RS-compatible dimension.
The bridge structure is the bookkeeping layer between that abstract uniqueness and the named constant $D_{\mathrm{physical}}=3$. Its fields surface bidirectional characterization ($\mathrm{RSCompatibleDimension},D\leftrightarrow D=3$), the canonical period identity $\mathrm{PeriodFromDimension},3=8$, and four independent forcing routes (Alexander-duality linking, eight-tick, gap-sync, spinor). Downstream assembly of the full chain needs this named $D=3$ surface rather than a bare existence statement.
Local setting: after T7 fixes the eight-tick octave, T8 closes the dimension loop so that $2^D=8$ is not an extra assumption but a forced identity at $D=3$.
proof idea
Term-mode structure construction for T8_To_CanonicalDimension_Bridge. The equality $D_{\mathrm{physical}}=3$ and the two period identities are rfl. Compatibility of $D_{\mathrm{physical}}$ and of $3$ are the imported lemmas DimensionForcing.D_physical_compatible and DimensionForcing.D3_compatible. The forward uniqueness arrow is DimensionForcing.dimension_unique. Linking, eight-tick, and spinor forcing routes are filled by DimensionForcing.linking_requires_D3, DimensionForcing.eight_tick_forces_D3, and DimensionForcing.spinor_eight_tick_forces_D3. The legacy uniqueness field is projected from the input T8 certificate as h8.unique_dimension. No new arithmetic is proved here; the bridge only packages existing DimensionForcing facts under the T8 hypothesis.
why it matters
This is the T8-to-canonical surface step in the complete inevitability chain. The module's forcing ladder ends at T8 ($D=3$ via linking and gap-45 sync); the bridge makes that conclusion usable as the named constant $D_{\mathrm{physical}}=3$ rather than a bare $\exists!$. Downstream, complete_forcing_chain threads this bridge into the unconditional CompleteForcingChain record, and ultimate_inevitability_extended exposes "the canonical dimension $D=3$" on the extended canonical surface alongside Gap-45 and the cyclic-shift universal property.
Framework landmark: primer T8 (spatial dimensions forced to three) and the T7 eight-tick octave ($2^3$), which become consistent only when this bridge identifies the unique RS-compatible dimension with three. Without it, later constant derivations that assume $D=3$ would sit on an unlinked uniqueness lemma rather than a named physical dimension.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.