complete_tminus2_to_t8
plain-language theorem explainer
Public re-export of the Recognition Science forcing certificate from T-2 (nothing-to-distinction) through T8 (three spatial dimensions plus circle H¹ closure). Foundation consumers cite this single name instead of the bridge module. It is a one-line abbreviation of the theorem-backed structure that packs the T-2→T-1 certificate, the T-1→T8 chain, and the unconditional Mathlib circle-H¹ facts.
Claim. The public certificate that the forcing chain from the nothing-to-distinction step ($T_{-2}$) through the eight-tick octave and three-dimensional closure ($T_8$) is fully assembled, including unconditional nonvanishing of $H^1(S^1;\mathbb{Z})$ and its isomorphism with $\mathbb{Z}$.
background
The Foundation module is a narrow public aggregator: it exposes only the $T_{-2}$ through $T_8$ core and the Mathlib circle-$H^1$ closure for $T_8$, and deliberately does not re-export later physics layers.
In the Recognition forcing chain, $T_{-2}$ is the nothing-to-distinction step, $T_{-1}$ opens the ledger floor, and $T_0$–$T_8$ force the cost functional $J$, the golden ratio $\varphi$, the eight-tick octave (period $2^3$), and $D=3$ spatial dimensions. The bridge theorem that this abbreviation names packages four fields: the $T_{-2}\to T_{-1}$ certificate from NothingToDistinction, a nonempty $T_{-1}\to T_8$ forcing chain, unconditional nonvanishing of circle $H^1$ with integer coefficients, and the isomorphism of that group with $\mathbb{Z}$.
Upstream doc-comment on the bridge theorem: "The public T-2 through T8 forcing certificate is theorem-backed." Adjacent module notes call the result the carrier-threaded $T_0$–$T_8$ spine from one object-level distinction, with $T_8$'s Mathlib circle-$H^1$ replacement closed unconditionally.
proof idea
One-line abbreviation. The body is exactly the bridge theorem complete_forcing_chain_tminus2_to_t8, which inhabits the structure CompleteForcingChainTMinus2ToT8 by supplying four already-proved components: the nothing-to-distinction certificate, the nonempty $T_{-1}\to T_8$ chain, unconditional circle-$H^1$ nonvanishing, and the integer isomorphism. No new proof work occurs at this site.
why it matters
This is the public face of the Recognition forcing spine from object-level distinction through $T_8$. Anyone citing the closed $T_{-2}$–$T_8$ package (including $J$-uniqueness at $T_5$, $\varphi$ at $T_6$, the eight-tick octave at $T_7$, and $D=3$ at $T_8$) is meant to land here rather than on internal bridge names.
The module doc states the aggregator is intentionally narrow: core theory plus Mathlib circle-$H^1$ $T_8$ closure only. That matches the primer landmarks $T_0$–$T_8$ and keeps later physics out of the Foundation surface. No downstream consumers are wired yet in the graph; the declaration exists so external and paper-facing citations have a stable, theorem-backed handle.
Upstream still flags ledger-floor work from the floor upward as an open task in places; this certificate does not claim to close those residual gaps, only the packaged $T_{-2}$–$T_8$ chain and the unconditional circle-$H^1$ facts.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.