Encyclopedia Foundation Foundation Arc Complement Acyclic

ARTICLE 1 claim 1 theorem

Foundation Arc Complement Acyclic

A theorem in the Recognition Science library proves that removing a single arc from a high-dimensional sphere leaves a space with no topological holes, a result that underpins the framework's account of spatial structure.

Verify this page

The acyclic complement

In topology, a circle is a one-dimensional loop. Remove a single point from it, and you get an interval, which can be continuously shrunk to a point. The space has no holes. The same idea applies in higher dimensions: a sphere in any dimension, with one arc removed, leaves a space that is topologically featureless. This property, called being acyclic, means every closed loop or higher-dimensional cycle in the space can be filled in, so the space carries no independent topological information.

This property is a standard fact in algebraic topology. The Recognition Science framework, which derives physical structure from a discrete record of events called a ledger, builds its account of space on such results. The framework's machine-checked library of formal theorems contains a proof that the complement of an arc in a sphere of any dimension is acyclic. The theorem, named arcComplementsAcyclic, is stated for all natural numbers D, meaning it holds for spheres of every dimension, not just the familiar two-dimensional surface.

The proof in the library works by constructing the complement as a union of two overlapping pieces, each of which is itself acyclic, and then showing their intersection is also acyclic. This is a standard technique in algebraic topology, using the Mayer-Vietoris sequence. The library formalizes this argument in the Lean proof assistant, checking every step against the kernel's rules. The result is a theorem that is guaranteed to follow from the axioms, with no gaps in the reasoning.

For the Recognition Science framework, this theorem is a building block. The framework's account of three-dimensional space derives from a chain of forced consequences, and this acyclicity result is part of the topological groundwork. It ensures that certain spaces, when an arc is removed, do not introduce spurious topological features that would complicate the framework's structural claims. The theorem is a formal guarantee that this particular piece of the foundation is sound.

The practical upshot is that the framework's library can rely on this topological fact without hand-waving. When the framework's arguments require that a sphere with an arc removed is acyclic, the library has a checked proof. This is one small piece of the larger project of building a fully formalized foundation for physics, where every step is verified by a computer.

THEOREM arcComplementsAcyclic · IndisputableMonolith/Foundation/ArcComplementAcyclic.lean
arcComplementsAcyclic · IndisputableMonolith/Foundation/ArcComplementAcyclic.lean:758 
/-- **Arc-complement acyclicity** (Hatcher 2B.1, arc case, formal):
every topological embedding of the unit interval into `S^D` has
`H₁`-acyclic complement, in every dimension `D`. -/
theorem arcComplementsAcyclic (D : ℕ) :
    LinkingVanishingHighDim.ArcComplementsAcyclic D := by
  intro a hemb
  by_contra hH
  haveI : T2Space ↥(Sph D) :=
    inferInstanceAs (T2Space (sphere (0 : Esp D) 1))
  obtain ⟨z, hz, hznb⟩ := exists_nonbounding hH
  have hinj : Function.Injective ⇑a := hemb.injective
  -- the initial bad interval
  have h0 : Bad a z 0 1 := by
    refine ⟨le_refl 0, le_refl 1, zero_le_one, ?_⟩
    intro hb
    apply hznb
    refine bounds_of_retract (cInc (seg_subset_range a 0 1))
      (cInc (range_subset_seg a)) (cInc_cInc_id _ _) z ?_
    exact hb
  -- the nested bad intervals and their limit point
  set s : ℕ → ℝ := fun k => (badSeq a z hinj hz h0 k).1.1 with hs
  set t : ℕ → ℝ := fun k => (badSeq a z hinj hz h0 k).1.2 with ht
  have hbdd : BddAbove (Set.range s) := by
    refine ⟨1, ?_⟩
    rintro _ ⟨k, rfl⟩
    exact ((badSeq a z hinj hz h0 k).2.2.2.1).trans (badSeq a z hinj hz h0 k).2.2.1
  set tstar : ℝ := ⨆ k, s k with htstar
  have hst : ∀ k, s k ≤ tstar := fun k => le_ciSup hbdd k
  have hts : ∀ k, tstar ≤ t k := fun k =>
    ciSup_le fun j => badSeq_le a z hinj hz h0 j k
  have h0t : (0 : ℝ) ≤ tstar := by
    have h := hst 0
    rw [show s 0 = 0 from congrArg Prod.fst (badSeq_zero a z hinj hz h0)] at h
    exact h
  have ht1 : tstar ≤ 1 := by
    have h := hts 0
    rw [show t 0 = 1 from congrArg Prod.snd (badSeq_zero a z hinj hz h0)] at h
    exact h
  set tI : unitInterval := ⟨tstar, h0t, ht1⟩ with htI
  set p : ↥(Sph D) := a tI with hp
  -- the point complement is contractible, so the pushforward bounds there
  have hpr : ({p} : Set ↥(Sph D)) ⊆ Set.range ⇑a := by
    intro x hx
    rw [Set.mem_singleton_iff] at hx
    exact ⟨tI, hx.symm⟩
  haveI hcontr : ContractibleSpace
      ↥((({p} : Set ↥(Sph D))ᶜ : Set ↥(Sph D))) :=
    contractibleSpace_compl_singleton_sphere p
  have hzero : IsZero (Hgrp (TopCat.of
      {y : ↥(Sph D) // y ∉ ({p} : Set ↥(Sph D))}) 1) := by
    have h := isZero_homology_of_contractible
      (TopCat.of ((({p} : Set ↥(Sph D))ᶜ : Set ↥(Sph D)))) one_ne_zero
    exact h
  obtain ⟨w, hw⟩ := bounds_of_isZero hzero (chainMap (cInc hpr) 1 z)
    (chainMap_cycle _ z hz)
  -- the compact support of the bounding chain misses `a(t*)`
  set Kc : Set ↥(Sph D) :=
    ⋃ i ∈ suppOf w, Set.range ⇑(simplexEquiv (Sph D) 2 (cPush i)) with hKc
  have hKc_compact : IsCompact Kc := by
    rw [hKc]
    exact (suppOf w).isCompact_biUnion fun i _ => isCompact_range (map_continuous _)
  have hKc_closed : IsClosed Kc := hKc_compact.isClosed
  have hKc_avoids : ∀ x ∈ Kc, x ∉ ({p} : Set ↥(Sph D)) := by
    intro x hx
    rw [hKc, Set.mem_iUnion₂] at hx
    obtain ⟨i, _, hxi⟩ := hx
    exact range_cPush i x hxi
  -- an ε-neighbourhood of `t*` avoids the support
  have hA_closed : IsClosed (⇑a ⁻¹' Kc) := hKc_closed.preimage (map_continuous a)
  have htA : tI ∈ (⇑a ⁻¹' Kc)ᶜ := by
    intro hmem
    exact hKc_avoids (a tI) hmem (by rw [hp]; exact Set.mem_singleton _)
  obtain ⟨ε, hε, hball⟩ := Metric.isOpen_iff.mp hA_closed.isOpen_compl tI htA
  obtain ⟨k, hk⟩ := exists_pow_lt_of_lt_one hε (by norm_num : (1 / 2 : ℝ) < 1)
  -- the k-th interval's arc image avoids the support
  have hclaim : ∀ x ∈ seg a (s k) (t k), x ∉ Kc := by
    rintro _ ⟨q, ⟨hq1, hq2⟩, rfl⟩ hxK
    have hqball : q ∈ Metric.ball tI ε := by
      rw [Metric.mem_ball, Subtype.dist_eq, Real.dist_eq]
      have hwidth : t k - s k = (1 / 2 : ℝ) ^ k := badSeq_width a z hinj hz h0 k
      have h1 : s k ≤ tstar := hst k
      have h2 : tstar ≤ t k := hts k
      have habs : |(q : ℝ) - tstar| ≤ (1 / 2 : ℝ) ^ k := by
        rw [abs_le]
        constructor
        · linarith
        · linarith
      show |(q : ℝ) - tstar| < ε
      exact lt_of_le_of_lt habs hk
    exact hball hqball hxK
  -- lift the bounding chain below the k-th arc complement
  obtain ⟨w', hw'⟩ := exists_chain_lift (S := ({p} : Set ↥(Sph D)))
    (T := seg a (s k) (t k)) w
    (fun i hi x hx hxT => hclaim x hxT (Set.mem_biUnion hi hx))
  -- contradiction with the k-th bad interval
  apply (badSeq a z hinj hz h0 k).2.2.2.2
  refine ⟨w', ?_⟩
  apply chainMap_injective (cVal (seg a (s k) (t k))) (cVal_injective _) 1
  have hL : chainMap (cVal (seg a (s k) (t k))) 1 (zSeg a z (s k) (t k)) =
      chainMap (cVal (Set.range ⇑a)) 1 z := by
    unfold zSeg
    rw [chainMap_chainMap, cInc_comp_cVal]
  have hR : chainMap (cVal (seg a (s k) (t k))) 1
      (bnd (TopCat.of {y : ↥(Sph D) // y ∉ seg a (s k) (t k)}) 1 w') =
      chainMap (cVal (Set.range ⇑a)) 1 z := by
    rw [← chainMap_bnd (cVal (seg a (s k) (t k))) 1 w', hw',
      chainMap_bnd (cVal ({p} : Set ↥(Sph D))) 1 w, ← hw,
      chainMap_chainMap, cInc_comp_cVal]
  rw [hL, hR]

What this page does not claim

The theorem does not claim that the framework's derivation of three dimensions is complete or that this result alone forces three-dimensionality. The theorem does not claim that the complement of an arc is contractible, only that it is acyclic. The theorem does not establish any physical fact about the actual universe; it is a purely topological statement.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Foundation/ArcComplementAcyclic.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND