T7_OperatorCore_RouteEquivalence
plain-language theorem explainer
Packages agreement between two routes from forced eight-tick and D=3 to the operator core: the canonical carrier bridge and the direct T7/T8 operator-core bridge. They must match on complexification, quarter-turn core neutrality, and the eight-tick equation. Cited when assembling the complete forcing chain. Definitional Prop structure plus a Subsingleton instance; no deep proof content here.
Claim. Given certificates that the eight-tick period is forced ($8=2^3$ from $D=3$) and that spatial dimension $D=3$ is forced, a route-equivalence certificate consists of (i) a T7-to-canonical-carrier bridge and (ii) a T7/T8-to-operator-core bridge, together with equalities asserting that both routes yield the same complexification witness, the same quarter-turn core neutrality, and the same eight-tick equation. For fixed T7 and T8 certificates such route equivalences are propositionally unique.
background
The Unified Forcing Chain module aims to show T0–T8 as inevitabilities from the Recognition Composition Law plus normalization and calibration. T7 asserts that the minimal ledger-compatible cycle is $2^D$, hence eight-tick once $D=3$. T8 asserts $D=3$ is the unique dimension compatible with nontrivial linking, eight-tick sync, and gap-45 synchronization.
Two bridges sit above those layers. The T7-to-canonical-carrier bridge names Signal8 = Fin 8 → ℂ as the recognition carrier, records that the cyclic shift has period 8 with Complex.I in its spectrum, and packages the algebraic obstruction forcing ℂ over ℝ. The T7/T8-to-operator-core bridge surfaces the forced eight-tick equation, inhabitance of Signal8, complexification (an eigenvalue equal to $i$, and $x^2+1\neq 0$ on ℝ), and quarter-turn core neutrality, building the operator-core surface from the carrier data.
This declaration is the agreement interface between those two routes: same universal construction, not two competing cores.
proof idea
This is a Prop-valued structure definition, not a proved theorem. It simply bundles five fields: a carrier-route certificate, an operator-route certificate, and three propositional equalities (complexification witness, quarter-core neutrality, eight-tick equation).
A companion Subsingleton instance proves propositional uniqueness for fixed T7 and T8 inputs by rfl on allEq, so any two such certificates are definitionally equal as Props.
The inhabiting theorem t7_operator_core_route_equivalence (downstream) fills the fields by applying t7_to_canonical_carrier_bridge_holds and t7_t8_to_operator_bridge_holds, then discharges the three agreements by rfl.
why it matters
In the forcing chain, T7 (eight-tick octave, period $2^3$) and T8 ($D=3$) must feed a single operator-core surface rather than two divergent constructions. This structure is the certificate type that enforces that uniqueness of routing: carrier path and direct T7/T8 path agree on complexification, quarter-turn neutrality, and the eight-tick equation.
It is consumed by CompleteForcingChain, the top-level package that all of T0–T8 are forced from the cost foundation and that quarter-turn, Hamiltonian, projective, coupled-core, variational, and measurement layers are available in-namespace. The inhabiting theorem t7_operator_core_route_equivalence is the concrete witness used there.
Framework landmarks: T7 eight-tick octave and T8 dimension forcing; the operator core is the algebraic home for the subsequent dynamics layers once the octave and $D=3$ are locked.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.