Pith. sign in
module module moderate

IndisputableMonolith.Foundation.ArcComplementAcyclic

show as:
view Lean formalization →

Module establishing that complements of arcs in the ambient space are acyclic: their homology vanishes in the relevant degrees. Homological algebraists and RS foundation readers cite it when reducing linking obstructions to zero-object vanishing. The argument packages chain-map naturality, homology class functors, and zero-object lemmas imported from high-dimensional linking vanishing.

claimIn the homological setting of the Recognition foundation, the complement of an arc is acyclic: every homology class of the complement is zero. Equivalently, the relevant chain complexes of the arc complement are quasi-isomorphic to the zero complex, so every cycle is a boundary and every element of a zero object vanishes.

background

Recognition Science foundation work reduces geometric linking and spine-closure questions to vanishing statements in homology. An arc complement is the ambient space with a tame arc removed; acyclicity means its homology groups (in the degrees that carry linking data) are trivial.

The module sits on LinkingVanishingHighDim, which supplies high-dimensional vanishing for linking classes. Local vocabulary includes homology class maps (classOf), the criterion that a class is zero iff it comes from a zero object, short-complex isomorphisms, and the usual chain-map identities (boundaries, cycles, composition). The module doc fixes the elementary zero-object fact: every element of a zero object vanishes.

Notation is Mathlib-style homological algebra: chain maps preserve boundaries and cycles; naturality of class maps lets vanishing transport along quasi-isomorphisms.

proof idea

Definition-and-lemma module, not a single monolithic theorem. It assembles standard zero-object and homology-class lemmas (elements of zero objects vanish; a class is zero iff the object is zero; existence and naturality of classOf) with chain-map calculus (boundary and cycle preservation, functoriality of composition). Acyclicity of the arc complement is obtained by identifying its complex with a zero object up to the imported high-dimensional linking vanishing, then pushing vanishing of classes through the naturality squares.

why it matters in Recognition Science

Feeds the public spine linking-closure stack: PublicSpineLinkingClosure imports this module to discharge residual linking obstructions once high-dimensional vanishing is in hand. In the RS foundation layer, arc-complement acyclicity clears topological noise so that forcing-chain geometry (octave period, spatial dimension, self-similar fixed point) is not contaminated by nontrivial linking in the complement. It is infrastructure rather than a named T0–T8 step, but without it the spine-closure theorems cannot quote clean vanishing.

scope and limits

used by (1)

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

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (60)