Encyclopedia Foundation Foundation Arc Complement Acyclic Hom Apply Eq Zero Iff

ARTICLE 2 claims 2 theorems

Foundation Arc Complement Acyclic Hom Apply Eq Zero Iff

A machine-checked theorem gives a precise condition for when a homology class in an arc complement is zero, and it does not claim to prove the Riemann Hypothesis.

Verify this page

The vanishing criterion

In algebraic topology, a homology class is a formal way to detect holes in a space; two cycles are homologous when they differ by a boundary. The theorem hom_apply_eq_zero_iff in the framework's machine-checked library of formal theorems establishes a precise criterion: a homology class in the complement of an arc is zero exactly when it is the boundary of a chain in the next dimension. This is the standard exactness condition that characterizes when a cycle is null-homologous, stated here for the specific construction of arc complements in spheres.

Classically, this kind of result is the content of the long exact sequence of a pair. The framework's contribution is to have formalized this statement in the Lean proof assistant, with the theorem arcComplementsAcyclic proving that the arc complements are acyclic in all dimensions. The lemma classOf_eq_zero_iff is the general form: a class is zero if and only if the representing cycle is a boundary. The specific declaration hom_apply_eq_zero_iff applies this to the homomorphism induced by the inclusion of an arc complement, which is the map that sends a class in the complement to its image in the larger sphere.

The practical meaning is a checkable test. If you have a cycle in the complement of an arc and you want to know whether it wraps around a hole, you compute its boundary in the next dimension. If that boundary exists, the class is zero; if not, it is nonzero. This is exactly the kind of criterion that lets a computer verify statements about the topology of spaces built from spheres and arcs, which is the setting the framework uses to model recognition events.

In Recognition Science, the framework models recognition as a discrete ledger of events, and this theorem is part of the topological scaffolding for that model. The declaration does not claim that the Riemann Hypothesis is proved, nor does it assert anything about the physical three-dimensionality of space. It is a formal statement about homology, verified in the machine-checked library, and it does not venture beyond that scope.

THEOREM eq_zero_of_isZero · IndisputableMonolith/Foundation/ArcComplementAcyclic.lean
eq_zero_of_isZero · IndisputableMonolith/Foundation/ArcComplementAcyclic.lean:82 
/-- Every element of a zero object vanishes. -/
lemma eq_zero_of_isZero (hM : IsZero M) (x : ↥M) : x = 0 := by
  have h : 𝟙 M = 0 := hM.eq_of_src _ _
  calc x = (𝟙 M) x := (ModuleCat.id_apply _ _).symm
    _ = (0 : M ⟶ M) x := by rw [h]
    _ = 0 := zeroApp x
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

This theorem does not prove the Riemann Hypothesis. This theorem does not assert the physical dimensionality of space. This theorem does not claim that all homology classes in all spaces are boundaries.

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