T7_To_CanonicalCarrier_Bridge
plain-language theorem explainer
Given a forced eight-tick period (T7), this certificate packages the canonical complex recognition carrier: functions from eight discrete ticks into the complexes. It records period-8 cyclic shift, eigenvalues ±i at modes 2 and 6, the real obstruction to an imaginary unit, DFT-8 unitarity with U(1)⁸ phase-invariant cost, and quarter-turn neutrality. Cited by the operator-core route and the complete forcing chain. Pure Prop structure (definitional interface), discharged later by a companion existence theorem.
Claim. Assume the eight-tick layer is forced, so the minimal ledger-compatible cycle equals $2^3$. The bridge asserts: the eight-tick identity holds for spatial dimension $3$; the canonical carrier is $\mathrm{Signal}_8=(\mathrm{Fin}\,8\to\mathbb{C})$ and is inhabited; the cyclic shift $S$ satisfies $S^8=\mathrm{id}$ on that carrier; the spectrum contains $i$ at mode $2$ and $-i$ at mode $6$; no real $x$ obeys $x^2+1=0$; the DFT-8 is unitary and norm-preserving (Parseval); total mode cost is invariant under $U(1)^8$ phase multiplications; the quarter-turn core sits inside the neutral register; and a single complex-structure certificate sources complexification, DFT unitarity, and phase invariance.
background
The Unified Forcing Chain module treats T0–T8 as inevitabilities from the Recognition Composition Law with normalization and calibration. T7 states that the minimal ledger-compatible cycle is $2^D$; with $D=3$ this forces the eight-tick octave (period $2^3$). In RS-native units the fundamental time quantum is one tick $\tau_0=1$, and one octave is eight ticks.
With the period fixed at eight, recognition dynamics need a carrier that faithfully represents a cyclic shift of order eight. The regular representation space is functions on eight ticks valued in $\mathbb{C}$. On that space the shift spectrum includes the primitive fourth roots $i$ and $-i$, which cannot live in a purely real carrier: no real squares to $-1$. The DFT-8 is the canonical unitary diagonalizing the shift; cost is phase-invariant in the mode basis.
Upstream T7 is the structure asserting the eight-tick equals $2^3$ and the dimension-forcing identity for $D=3$. This bridge sits between that discrete-period fact and the complex operator core used later in the chain.
proof idea
Definitional Prop structure, not a tactic proof. Fields name what the bridge must supply: the eight-tick equation (from T7's dimension identity); definitional equality of the eight-tick signal space with $\mathrm{Fin},8\to\mathbb{C}$; inhabitation of the carrier; the universal $S^8=\mathrm{id}$ law for the cyclic shift; eigenvalue identities at modes 2 and 6; the algebraic obstruction $\forall x\in\mathbb{R},,x^2+1\neq 0$; DFT-8 unitarity and Parseval; phase invariance of total mode cost; a complexification witness pairing existence of eigenvalue $i$ with the real obstruction; quarter-turn core inside the neutral register; and the master complex-structure certificate.
A Subsingleton instance records that any two certificates for fixed T7 are propositionally equal (rfl on Prop). The companion theorem t7_to_canonical_carrier_bridge_holds fills every field from T7, rfl, a zero witness, and the complex-structure forcing lemmas.
why it matters
T7 pins the eight-tick octave (primer landmark: period $2^3$ with $D=3$). This bridge converts that discrete period into the canonical complex carrier on which recognition operators act, and makes precise why $\mathbb{C}$ rather than $\mathbb{R}$ is forced: the shift spectrum demands an imaginary unit.
Downstream, the companion existence theorem shows the certificate is inhabited whenever T7 holds. The T7 operator-core route equivalence takes the carrier route as one of two equivalent paths to the operator core; the operator-core package records quarter-core neutrality and Hamiltonian evolution on that core. The complete forcing chain structure includes the full T0–T8 stack plus operator, projective, and measurement layers.
It does not itself force $D=3$ (T8) or derive constants; it is the T7-to-carrier hinge inside the inevitability chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.