module module moderate

`IndisputableMonolith.Foundation.LinkingVanishingHighDim`

Foundation module that restates the content-typed first homology of a linking complement and the nontrivial-linking detector, then develops the high-dimensional geometric side (sphere points, coordinate bounds, arc parametrizations). Complements the low-dimensional vanishing leaf. Downstream assembly and arc-complement acyclicity import it. Argument shape is restatement plus elementary sphere/arc lemmas rather than a single theorem.

claimIn the high-dimensional regime, the module packages the first homology $H_1$ of a linking complement, a predicate that a class detects nontrivial linking, and supporting geometry on the unit sphere (distinguished points, coordinate square-sum identities, and an arc map whose $0$-coordinate is controlled). It is the high-dim counterpart of the low-dim linking-vanishing leaf.

background

Recognition Science forces spatial dimension $D=3$ (forcing step T8) partly by topological linking constraints: nontrivial linking of complementary spheres or arcs is dimension-sensitive, and the first homology of the complement is the natural detector.

The low-dimensional sibling module is Mathlib-only: it restates the content-typed object linkingComplementH1 and the detector DetectsNontrivialLinking from the public spine, and proves the detector fails for $D=0$ and $D=1$ (the $0$-sphere is finite, etc.). This module is the matching high-dimensional leaf: same restated linking/$H_1$ interface, plus singular-sphere geometry (unit sphere membership, squared-coordinate bounds, an arc parametrization).

Local setting is Foundation geometry feeding the public spine assembly of linking facts, not continuum physics constants.

proof idea

Not a single theorem. The module (i) restates the spine's content-typed linking complement $H_1$ and the nontrivial-linking detector, and (ii) builds elementary sphere/arc infrastructure: distinguished points on $S^n$, norm and membership lemmas, $x_0^2+x_1^2$ identities, bounds $x_0^2\le 1$, and an arc map with controlled $0$-coordinate. Those lemmas support later acyclicity and assembly arguments rather than closing the dimension force alone. Overall structure mirrors the low-dim vanishing leaf, with geometry imported from singular sphere geometry.

why it matters in Recognition Science

Closes the high-dimensional half of the Foundation linking package. Imported by ArcComplementAcyclic (arc complements have vanishing $H_1$) and by PublicSpineLinkingAssembly (public assembly of linking facts for the spine). Together with the low-dim leaf (detector fails in $D=0,1$), it supplies the geometric substrate for dimension-sensitive linking used in the T8 forcing of three spatial dimensions. Without the restated $H_1$/detector interface and the sphere-arc lemmas, the assembly cannot cite a uniform content-typed linking object across dimensions.

scope and limits

Does not by itself prove $D=3$; only supplies high-dim linking/$H_1$ restatement and sphere-arc lemmas.
Does not re-prove low-dim vanishing; that lives in the low-dim sibling module.
Does not define continuum physics constants ($c$, $\hbar$, $G$, $\alpha$).
Does not claim a full singular homology theory beyond the restated $H_1$ linking interface.
Does not discharge PublicSpine obligations outside what assembly imports.

used by (2)

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

IndisputableMonolith.Foundation.ArcComplementAcyclic module_import
IndisputableMonolith.Foundation.PublicSpineLinkingAssembly module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Foundation.LinkingVanishingLowDim module_import
IndisputableMonolith.Foundation.SingularSphereGeometry module_import

declarations in this module (43)

def linkingComplementH1 L69
def DetectsNontrivialLinking L76
def ArcComplementsAcyclic L88
def pt2 L96
lemma pt2_zero L99
lemma pt2_one L101
lemma pt2_norm L103
lemma pt2_mem_sphere L109
lemma coord_sq_add_sq L114
lemma sq_coord0_le_one L120
def arcFun L125
lemma arcFun_coord0 L135
lemma arcFun_coord1 L138
lemma continuous_arcFun L141
def arcMap L155
lemma arcMap_injective L159
lemma isEmbedding_arcMap L167
def arcPlus L175
def arcMinus L179
lemma isEmbedding_arcPlus L182
lemma isEmbedding_arcMinus L185
def arcParam L189
lemma arcFun_arcParam L199
lemma range_arcPlus L218
lemma range_arcMinus L231
lemma range_arcPlus_union_arcMinus L245
lemma range_arcPlus_inter_arcMinus L253
lemma eastP_ne_westP L301
def perpIsometry L312
lemma stereographic_source_pt L320
def twoPunctHomeo L329
def punctTranslateHomeo L385
def twoPointComplHEquiv L396
theorem isZero_h2_twoPointCompl L408
theorem isZero_h1_inter L420
def flattenComplHomeo L434
theorem isZero_h1_unionCompl L452
theorem isZero_h1_complement_of_embedding L518
def toSphMap L565
lemma isEmbedding_toSphMap L573
def complDownHomeo L582
theorem not_detects_of_arcAcyclic L603
theorem forces_D3_of_arcAcyclic L615