substrateCert_holds
plain-language theorem explainer
Preferred public name for the inhabited dual-spine certificate: δ-stratified tower, continuum as purchase, cost selection, φ from reciprocal involution, and circle H₁. Papers and loops that mean "what is forced" should cite this instead of UFC certificate emptiness wrappers. One-line definitional alias of the assembled public spine certificate; D=3 and eight-tick targets are the content-typed binders closed via Alexander linking.
Claim. The public substrate certificate holds: the $\delta$-only forcing tower on $\mathbb{N}/\mathbb{Z}/\mathbb{Q}$, continuum as a classical purchase, the cost-selection package, $\varphi$ from the reciprocal involution, and $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ are all inhabited on the public dual spine.
background
PublicSpine is the public dual of UnifiedForcingChain. It does not delete UFC; the Boolean certificate spine stays for loop compatibility. This surface is the honest δ-stratified map: papers that mean "what is forced" cite here, while UFC names remain certificate or floor witnesses only.
SubstrateCert is the preferred Channel-B name for PublicSpineCert. That package bundles the δ-only tower (ℕ/ℤ/ℚ), continuum cut as classicalExtension (panel K2: do not put ¬ℝ under deltaOnly), cost form versus unit calibration as purchases or gauges, φ from ReciprocalGenerator, and the theorem $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. The D=3 / eight-tick bridge target is closed in PublicSpineLinkingClosure via AlexanderLinkingBridge (unknot-complement retract, CubePeriodEight pigeonhole, vanishing in low dimension, forces_D3 off D=3), with no encoding predicates.
Framework constants in view: spatial dimension D=3 (T8) and the fundamental tick τ₀=1, with one octave equal to eight ticks (T7).
proof idea
One-line term proof. SubstrateCert is an abbrev for PublicSpineCert, so the already-proved publicSpineCert_holds inhabits it by definitional equality. That upstream structure packs forced_tower_holds, continuum_is_purchase, cost_selection_holds, phi_from_iota_holds, and circle_H1_holds. No new mathematics; pure retarget alias for honest public citation.
why it matters
Citation surface for the dual forcing map. Module contract: this is the honest replacement for Nonempty wrappers around T7_EightTick_Forced and T8_Dimension_Forced; the content-typed binder (panel K1) blocks encoding cheats such as SphereAdmitsCircleLinking. Lands the closed D=3 / eight-tick bridge (forcing-chain landmarks T7 eight-tick octave and T8 spatial dimension three) without appealing to DimensionForcing.linking_requires_D3 or arithmetic encoding. Also exposes T6-adjacent φ-from-iota and the cost-selection package on the public side. No downstream used_by edges yet; the declaration is itself the public export. FOP and unique-cost results are untouched.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.