t8_triple_route_unique_via_routes
plain-language theorem explainer
Under any T8 witness that spatial dimension is forced, the unique-dimension field equals the canonical dimension-forcing theorem (unique RS-compatible $D$). Citers of the three-route T8 surface can treat that field as interchangeable with the direct Alexander-duality uniqueness result. Proof is one-line Subsingleton elimination on Prop.
Claim. If $h_8$ is a witness that spatial dimension is forced (nontrivial linking forces $D=3$, eight-tick forces $D=3$, and there is a unique RS-compatible dimension), then the unique-existence component of $h_8$ is equal, as a proposition, to the theorem that there exists a unique dimension $D$ with the RS-compatible-dimension property.
background
The Unified Forcing Chain module derives T0–T8 as inevitabilities from the Recognition Composition Law plus normalization and calibration. T8 is the claim that spatial dimension is not free: $D=3$ is the only value compatible with ledger conservation via nontrivial linking, the eight-tick period $2^D=8$, and gap-45 synchronization.
The T8 surface packages three force statements, including a unique-existence field: there is a unique $D$ satisfying the RS-compatible-dimension predicate. Upstream, dimension_forced is the direct theorem of the same shape, proved by exhibiting $D=3$ and uniqueness from Alexander duality (linking exists iff $D=3$, Hatcher 3.44), with eight-tick and lcm$(8,45)=360$ as consequences.
Both sides are therefore propositions of type $\exists! D,,\mathrm{RSCompatibleDimension}(D)$. In Lean, proofs of a fixed proposition form a subsingleton, so any two such proofs are equal.
proof idea
Term proof by Subsingleton.elim. The left side is the unique-dimension field of the T8 witness; the right side is the canonical dimension-forcing uniqueness theorem. Both inhabit the same proposition type (unique existence of an RS-compatible dimension). Prop is a subsingleton, so the two proof terms are definitionally interchangeable; no case analysis on linking, eight-tick, or gap-sync is required.
why it matters
Closes the three-route compatibility bridge for T8 inside the Complete Inevitability Chain: routing dimension forcing through topology (Alexander duality / linking), Bott-period structure, and gap-sync is propositionally the same as citing the direct dimension-forcing theorem. That aligns with the framework landmark T8 ($D=3$ forced) and the stated priority that dimension forcing is primary, with the eight-tick identity ($2^3=8$, T7) a consequence rather than a premise.
No downstream dependents are recorded yet; the lemma is a surface-coherence certificate so later T8 consumers need not choose between the packaged unique-dimension field and the DimensionForcing uniqueness theorem. It does not itself re-prove $D=3$; it only equates the two uniqueness statements once a T8 witness is in hand.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.