SubstrateCert
plain-language theorem explainer
Preferred alias for the dual-surface public-spine certificate: the inhabited package of δ-stratified forcing pieces (tower, continuum purchase, cost selection, φ from reciprocal involution, circle H₁, and named linking encoding). Papers and loops that mean “what is forced” cite this name rather than the UFC Boolean spine. The body is a one-line abbreviation of the certificate structure.
Claim. Write $\mathsf{SubstrateCert}$ as a synonym for the dual-surface certificate proposition whose inhabitants package: a $\delta$-only forced tower $\mathbb{N}/\mathbb{Z}/\mathbb{Q}$; a classical-extension purchase that $\mathbb{R}$ is not $\delta$-forced; a trace-closure cost-selection package; $\varphi$ obtained from the reciprocal involution; the classical isomorphism $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$; and the named linking-encoding equivalence for each dimension $D$.
background
PublicSpine is the public dual of UnifiedForcingChain. It keeps the Boolean/certificate spine for loop compatibility but exposes an honest δ-stratified map: δ-only tower on ℕ/ℤ/ℚ, continuum cut as a classical extension (not under δ-only), cost form versus unit calibration as purchases/gauges, φ from the reciprocal involution, and H₁(S¹;ℤ) ≅ ℤ as a theorem. The D=3 / eight-tick bridge target is closed via AlexanderLinkingBridge in PublicSpineLinkingClosure.
The underlying certificate structure packages tagged pieces: forced tower under StrengthTag.deltaOnly; continuum purchase under classicalExtension that ℝ is not DeltaForced; cost selection and φ-from-ι under traceClosure; circle H₁ under classicalExtension; plus a named linking-encoding binder ∀ D, SphereAdmitsCircleLinking D ↔ (D : ℤ) − 2 = 1. Contract: papers meaning “what is forced” cite this module; UFC names remain floor witnesses, not the architecture claim.
proof idea
One-line definitional abbreviation: the name is definitionally equal to the dual-surface certificate structure. No tactics, no lemmas, no proof obligations beyond the structure’s field types.
why it matters
Gives the preferred Channel-B name for the inhabited public substrate so downstream citations avoid UFC Boolean packaging. The immediate consumer is substrateCert_holds, which inhabits the alias by forwarding publicSpineCert_holds and discloses that the D=3 / eight-tick public targets are exactly the content-typed binders (both proved in PublicSpineLinkingClosure). Citing this is the honest replacement for Nonempty T7_EightTick_Forced / Nonempty T8_Dimension_Forced. Framework landmarks: T6 φ from reciprocal generator, T7 eight-tick octave and T8 D=3 via the closed Alexander linking bridge, without encoding predicates or DimensionForcing.linking_requires_D3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.