T6_To_T7_RouteEquivalence
plain-language theorem explainer
Given φ forced at T6, the direct canonical-period path to the eight-tick (T7) and the indirect path through dimensional forcing (T6→T8→T7) yield identical T7 surfaces. Anyone assembling the complete T0–T8 inevitability chain cites this certificate to collapse the two constructions into one. The structure packages both bridges plus three agreement equalities; propositional uniqueness is immediate by rfl.
Claim. Fix a witness that $\varphi$ is forced ($\varphi^2=\varphi+1$, $\varphi>0$, unique positive root). A route-equivalence certificate consists of: (i) the direct T6$\to$T7 canonical-period bridge; (ii) the T6$\to$T8 dimension bridge; (iii) the T8$\to$T7 eight-tick bridge; (iv) equality of the two resulting T7 surfaces on the fields ``eight is $2^3$'' and ``from dimension''; (v) the identity $\mathrm{PeriodFromDimension}(3)=\mathrm{EightTickFromDimension}(3)$. Any two such certificates are propositionally equal.
background
The Unified Forcing Chain module derives T0–T8 as inevitabilities from the Recognition Composition Law plus normalization and calibration. T6 asserts that in a discrete ledger with self-similar cost, the only positive scaling ratio is $\varphi=(1+\sqrt{5})/2$, the unique solution of $x^2=x+1$. T7 is the eight-tick octave (period $2^3$); T8 is the forcing of spatial dimension $D=3$.
Two constructions reach T7 from T6. The canonical-period bridge builds the cycle as $\Pi(D)=2^D$ evaluated at the Alexander-duality dimension $D=3$, independently of $\varphi$. The dimension bridge first packages T8 (linking forces $D=3$), then the T8$\to$T7 bridge reads the eight-tick as a consequence of that dimension rather than a premise for it.
Upstream constants fix the ambient units: the fundamental tick $\tau_0=1$, spatial dimension $D=3$, and the hypercube vertex count $2^D$. The period constructions PeriodFromDimension and EightTickFromDimension are the two faces of the same $2^D$ law at $D=3$.
proof idea
This declaration is a structure (Prop bundle), not a proved theorem. Its fields name the two bridges and the three agreement identities that make the routes equivalent. The companion theorem t6_to_t7_route_equivalence fills the fields by applying t6_to_t7_canonical_bridge_holds, t6_to_t8_dimension_bridge_holds, and t8_to_t7_bridge_holds on the T8 surface of the dimension bridge, then discharging the agreement equalities by the shared canonical constructions. The Subsingleton instance is a one-line rfl: all fields are propositions, so any two inhabitants are definitionally equal.
why it matters
In the forcing chain, T6 pins $\varphi$, T7 the eight-tick octave, and T8 the dimension $D=3$. Without route equivalence, the complete chain would carry two potentially distinct T7 surfaces—one from the direct period law, one from the dimension detour. This certificate collapses them, so CompleteForcingChain can cite a single T7 without choosing a preferred path.
The design matches the module's stronger claim: every level is forced, not merely compatible. Dimension is primary (Alexander linking pins $D=3$); the eight-tick is $2^D$ at that $D$, not an independent postulate used to prove dimension. The agreement PeriodFromDimension 3 = EightTickFromDimension 3 is exactly the T7 landmark $2^3=8$ read two ways. Downstream, t6_to_t7_route_equivalence inhabits the structure and feeds the top-level complete chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.