Pith. sign in
module module moderate

IndisputableMonolith.Foundation.PublicSpineLinkingAssembly

show as:
view Lean formalization →

Assembly module for the binder uniqueness half of the public dual spine, conditioned on the arc-complement frontier. Low dimensions 0 and 1 are taken unconditionally from the low-dim linking vanishing results; dimensions 2 and at least 4 come from the Mayer-Vietoris reduction in the high-dim linking module. Downstream closure packages cite it to force spatial dimension three under arc-acyclicity.

claimOn the public dual spine, the uniqueness half of the binder is assembled as follows: for dimensions $0$ and $1$, linking vanishes unconditionally; for dimension $2$ and all dimensions $\ge 4$, linking vanishes by the Mayer-Vietoris reduction of the high-dimensional vanishing theorem, conditional on the arc-complement frontier. The resulting package yields the forcing statements that arc-acyclicity selects $D=3$ and identifies the corresponding target.

background

PublicSpine is the public dual of the UnifiedForcingChain. It keeps the Boolean certificate spine for compatibility and pedagogy, while exposing an honest $\delta$-stratified map: a $\delta$-only tower over $\mathbb{N}/\mathbb{Z}/\mathbb{Q}$ via forced_tower_holds, with continuum cut handled by classicalExtension (panel K2: do not place $\neg\mathbb{R}$ under $\delta$-only).

Linking vanishing is the geometric input that kills nontrivial linking outside dimension three. Low dimensions $0,1$ are unconditional. High dimensions $2$ and $\ge 4$ are reduced by Mayer-Vietoris arguments in LinkingVanishingHighDim. The arc-complement frontier is the residual hypothesis that keeps the uniqueness half conditional until the frontier is discharged.

This module sits between those two imports and the closure layer: it does not re-prove vanishing, it wires the low-dim unconditional facts and the high-dim MV reduction into the public spine's uniqueness half.

proof idea

Structural assembly, not a single deep proof. Import PublicSpine for the dual $\delta$-stratified surface and LinkingVanishingHighDim for the Mayer-Vietoris high-dim vanishing. Wire dimensions $0,1$ from the unconditional low-dim linking results; wire dimensions $2$ and $\ge 4$ from the high-dim MV reduction, retaining the arc-complement frontier hypothesis. Expose the packaged predicates (membership in the assembled uniqueness half, forcing of $D=3$ from arc-acyclicity, and the associated target) for the closure module to consume.

why it matters in Recognition Science

Fills the uniqueness half of the binder on the public dual spine, the counterpart to the T0-T8 forcing chain's dimension step (T8: $D=3$ spatial dimensions). Downstream, PublicSpineLinkingClosure imports this assembly to close the linking argument under arc-acyclicity. Without the split (unconditional low-dim vs MV high-dim), the public surface could not honestly claim that only $D=3$ survives while keeping the arc-complement frontier explicit. It is the linking-side twin of the $\delta$-stratified tower in PublicSpine, and the place where high-dim vanishing becomes usable for the dual forcing surface.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (3)