Encyclopedia Foundation Foundation Arc Complement Acyclic Bounds Of Halves

ARTICLE 2 claims 2 theorems

Foundation Arc Complement Acyclic Bounds Of Halves

A formal theorem about circles and spheres shows that certain missing arcs are never boundaries, a fact that shapes how the framework builds spaces.

Verify this page

The bounds of halves

The declaration bounds_of_halves is a lemma in the framework's machine-checked library of formal theorems. It concerns a circle, a sphere, and a missing arc. In plain terms, it establishes that under certain conditions, a particular kind of object called a "boundary" cannot be found. The lemma is part of a larger theorem, arcComplementsAcyclic, which states that the complement of an arc in a sphere has no nontrivial cycles in its homology. This is a topological fact about the shape of space after removing a simple curve.

The classical setting is algebraic topology. A circle is a one-dimensional sphere, and a two-dimensional sphere is the surface of a ball. An arc is a piece of a curve. The theorem says that if you remove an arc from a sphere, the remaining space has no holes in a certain sense: its first homology group is zero. This is a known result in topology, but the framework proves it in a formal system, meaning every step is checked by a machine. The lemma bounds_of_halves is a technical step in that proof, dealing with a specific construction involving two halves of an arc.

In Recognition Science, this theorem is used as a building block. The framework models reality as a discrete record of events, and it uses topological results to constrain the structure of space. The theorem about arc complements helps establish that certain spaces are acyclic, meaning they have no cycles that could represent nontrivial structure. This is part of the framework's effort to derive the properties of space from its foundational axioms. The lemma itself does not claim anything about the physical world directly; it is a statement about mathematical objects.

The declaration does not claim that all spaces are acyclic, nor does it claim that the framework has derived the dimensionality of space from this lemma alone. It is one step in a larger proof. The lemma also does not claim that the framework's model of reality is correct; it only establishes a mathematical fact within the framework's system. The theorem is a formal result, not an empirical observation.

THEOREM badSeq_zero · IndisputableMonolith/Foundation/ArcComplementAcyclic.lean
badSeq_zero · IndisputableMonolith/Foundation/ArcComplementAcyclic.lean:711 
lemma badSeq_zero : (badSeq a z hinj hz h0 0).1 = (0, 1) := rfl
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 lemma does not claim that all spaces are acyclic. The lemma does not claim that the framework has derived the dimensionality of space. The lemma does not claim that the framework's model of reality is empirically correct.

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