Pith. sign in
module module moderate

IndisputableMonolith.Foundation.LinkingVanishingHighDim

show as:
view Lean formalization →

Mathlib-facing leaf that restates the content-typed linking object and detector from PublicSpine, then treats the high-dimensional regime. It supplies sphere-point and arc constructions used to show that the nontrivial-linking detector fails once dimension is large enough that arc complements are acyclic in H1. Downstream assembly and arc-complement modules import it as the high-D half of the low/high vanishing pair that isolates D = 3.

claimIn high ambient dimension, the first homology of the complement of a tame arc in the singular sphere vanishes, so the detector $\mathrm{DetectsNontrivialLinking}$ fails: there is no class in $H_1$ of the complement that witnesses nontrivial linking. The module also packages the restated linking object $\mathrm{linkingComplementH}_1$ and elementary sphere geometry (coordinate points on $S^{n}$, squared-coordinate bounds, arc parameterizations).

background

Recognition Science forces spatial dimension $D = 3$ (forcing step T8) by a linking argument on spheres: nontrivial $S^1$--$S^{1}$ linking lives only in $S^3$. The PublicSpine content types linkingComplementH1 (the $H_1$ of a link complement, as a Prop-level witness) and DetectsNontrivialLinking (a detector that a homology class sees nontrivial linking). The sibling leaf LinkingVanishingLowDim already shows the detector fails for $D = 0,1$ because the $0$-sphere is finite and low-dimensional spheres cannot carry the required dual cycles.

This module is the matching high-dimensional leaf. It imports SingularSphereGeometry for the singular-sphere model and coordinate calculus, and restates the same PublicSpine linking object so both vanishing leaves share a single content type. Local definitions include concrete points pt2 on the sphere, norm and membership lemmas, squared-coordinate inequalities, and an arc map arcFun used to build tame arcs whose complements are the test spaces for $H_1$.

proof idea

Structural twin of the low-dimensional vanishing leaf, not a single theorem. It (1) restates linkingComplementH1 and DetectsNontrivialLinking verbatim from PublicSpine so the content types match across dimension regimes; (2) builds elementary sphere geometry (points, norms, coordinate square sums, arc parameterizations) on top of SingularSphereGeometry; (3) packages the high-D acyclicity claim for arc complements (ArcComplementsAcyclic and related lemmas) that makes the detector fail when dimension is large enough for the complement to be $H_1$-acyclic. No deep algebraic topology is reinvented here: the work is Mathlib-facing geometry plus the content-type bridge.

why it matters in Recognition Science

Closes the high-dimensional side of the linking-vanishing sandwich that isolates $D = 3$ in the T8 forcing step. Low dimensions kill the detector by scarcity of cycles; high dimensions kill it by acyclicity of arc complements. Only the three-dimensional case remains open for a positive linking witness. Downstream, ArcComplementAcyclic consumes the arc and acyclicity material, and PublicSpineLinkingAssembly imports both vanishing leaves to assemble the public spine statement that nontrivial linking detection is dimension-selective. Without this module the assembly would lack a uniform high-D failure mode stated against the same linkingComplementH1 content type as the low-D leaf.

scope and limits

used by (2)

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 (43)