CompleteForcingChainTMinus2ToT8
plain-language theorem explainer
Packages the full public forcing certificate from the T-2 absolute-nothing floor through T8 (D=3), together with the Mathlib circle-homology nonvanishing and isomorphism witnesses needed for the linking argument. Anyone citing the end-to-end foundation spine from Empty to spatial dimension uses this record. It is a pure Prop structure: five named fields, no proof body.
Claim. A proposition holding exactly when (i) the nothing-to-distinction certificate is inhabited (universe populated; type, propositional, object, and Boolean distinctions), (ii) the T-1 through T8 forcing spine is nonempty, (iii) $H_1(S^1;\mathbb{Z})$ is nonvanishing, (iv) $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ as $\mathbb{Z}$-modules, and (v) a Mathlib circle-linking backend exists.
background
The module exposes the public, theory-only T-1 through T8 forcing spine and deliberately stops before private operator or measurement layers. Landmarks on that spine: T-1 absolute distinguishability floor; T0 Boolean recognition-work split; T1 cost-form Meta-Principle; T2 two-state discreteness; T3 additive ledger; T4 recognition witness; T5 uniqueness of the canonical reciprocal cost $J$; T6 $\varphi$ forced by self-similar hierarchy; T7 eight-tick cadence; T8 $D=3$ from linking, eight-tick, and gap-sync compatibility.
The T-2 floor is discharged by NothingToDistinctionCert: from the Lean encoding of Empty, the universe is populated and type, propositional, object, and Boolean distinctions all hold. The inner spine is the nonempty record CompleteForcingChainT8, which chains T-1 through T8 with the successive bridges between them.
T8's dimensional argument needs circle homology. The Mathlib bridge supplies three props: nonvanishing of $H_1(S^1;\mathbb{Z})$, the isomorphism $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$, and a linking backend that routes dimension-forcing through that computation rather than a project-local $S^1$ encoding.
proof idea
No proof body: this is a five-field Prop structure. Inhabitation is supplied downstream by complete_forcing_chain_tminus2_to_t8, which fills the fields by nothingToDistinctionCert, complete_forcing_chain_t8_nonempty, and the unconditional circle-homology witnesses circleH1ZNonzero_unconditional and circleH1ZIsoInt_holds from the circle-winding chain. The structure itself only names the certificate interface.
why it matters
This is the public end-to-end foundation certificate: T-2 absolute nothing through T8 ($D=3$). Downstream, complete_forcing_chain_tminus2_to_t8 is the theorem that inhabits it and re-exports the circle $H_1$ facts used by Foundation-level wrappers (circle_h1_nonzero, circle_h1_iso_int).
In the Recognition forcing chain it closes the public spine from the Empty encoding up through J-uniqueness (T5), $\varphi$ as self-similar fixed point (T6), the eight-tick octave (T7), and three spatial dimensions (T8). The bundled Mathlib circle-linking backend is the honest interface for replacing any remaining project-local $S^1$ cohomology with a pinned Mathlib computation of $H_1(S^1;\mathbb{Z})$.
It does not touch the private operator or measurement layers in /reality; those sit strictly above this certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.