t8_topology_dependency_audit_bridge_holds
plain-language theorem explainer
Given the T8 surface that spatial dimension three is forced, this packages a topology dependency audit: circle reduced cohomology is nontrivial only in degree one, sphere–circle linking holds exactly at D=3, and non-linking is recorded outside three dimensions. Citers are those assembling the complete T0–T8 inevitability chain. The proof is a structure constructor wiring Alexander-duality theorems and dimension-forcing lemmas into the audit fields.
Claim. Assume spatial dimension is forced to $D=3$ by nontrivial linking, the eight-tick condition $2^D=8$, and uniqueness of an RS-compatible dimension. Then the topology audit holds: reduced cohomology $\tilde H^k(S^1;\mathbb{Z})$ is nontrivial iff $k=1$; a sphere admits nontrivial circle linking iff $D=3$; the T8 linking route forces $D=3$; that dimension is unique; and dimensions $1$, $2$, and $D>3$ admit no nontrivial linking.
background
The module Unified Forcing Chain proves that T-1 through T8 are forced from the Recognition Composition Law plus normalization and calibration, rather than merely compatible. T8 is the dimension step: spatial $D$ is not a free parameter. The structure T8_Dimension_Forced records three routes: nontrivial linking forces $D=3$, the eight-tick identity $2^D=8$ forces $D=3$, and there is a unique RS-compatible dimension.
The audit bridge sits on Alexander duality for circle linking. Upstream, reduced cohomology of the circle is nontrivial exactly in degree one (Hatcher §2.2), now a closed theorem rather than an axiom. Sphere–circle linking is defined so that $S^D$ admits nontrivial closed-curve linking iff that cohomology group in degree $D-2$ is nontrivial, which forces $D=3$. Dimension-forcing lemmas separately record that $D=1$, $D=2$, and high $D$ support no nontrivial linking.
Locally this certificate is the topology half of the T8 surface before gauge and Standard Model routing consume $D=3$.
proof idea
Tactic-mode structure constructor for the audit certificate under hypothesis h8.
- Circle cohomology field: direct application of
AlexanderDuality.circle_reduced_cohomology_iff(definitionalIff.rflafter the concrete predicate). - Sphere-linking field:
AlexanderDuality.alexander_duality_circle_linking, which rewrites linking to the cohomology criterion and finishes withomegato get $D=3$. - Unfolding field:
intro D; rfl(definitional agreement of the supports-linking predicate with sphere linking). - Topological route and uniqueness: project
h8.linking_forces_D3andh8.unique_dimension. - Non-linking outside three: pair
DimensionForcing.D1_no_linking,D2_no_linking, andhigh_D_no_linking.
No new topology is proved here; the bridge only closes the dependency audit surface.
why it matters
T8 is the landmark that spatial dimension equals three in the forcing chain (linking plus gap-45 sync, with the eight-tick octave $2^3$ already on the table). This declaration does not re-derive $D=3$; it certifies that the topological dependencies the T8 surface cites are closed theorems (circle cohomology, Alexander duality linking) and that non-linking outside three dimensions is on record.
Downstream it is consumed by complete_forcing_chain, the unconditional assembly of T-1 through T8. Without this bridge the chain would still carry an open topology-audit hole on the T8 surface. The module comment after the proof routes gauge and SM structure through the forced cube/dimension skeleton; this audit is the topology gate for that routing. It does not touch $\varphi$, $\alpha$, or mass-ladder claims; those live elsewhere in the chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.