Foundation Singular Subdivision Abnd Comp Acone Zero

The boundary of a cone

In algebraic topology, a cone is a geometric construction that takes a shape and adds a new point, then draws every line from that point to the original shape. For a triangle, the cone is a pyramid; for a circle, it is an ordinary cone. The boundary of a cone has a simple and famous description: for a simplex, the boundary of its cone is the original simplex, with no leftover pieces. The formal statement abnd_comp_acone_zero in the framework's machine-checked library of formal theorems records exactly this fact for a class of objects called affine chains.

An affine chain is a formal sum of simplices, where each simplex is a list of points. The framework defines a boundary operator, written abnd, which sends an n-dimensional chain to its (n-1)-dimensional boundary, and a cone operator, written acone, which sends an n-dimensional chain to an (n+1)-dimensional cone. The theorem states that applying the boundary operator after the cone operator always gives zero: abnd (acone c) = 0 for any chain c. This is the algebraic way of saying that the boundary of a cone has no boundary of its own, a property that holds for every geometric cone.

This result is a standard lemma in homology theory, where it appears as part of the proof that the cone construction is acyclic. The framework's contribution is not the discovery of the fact, which has been known for over a century, but the verification that it follows from the definitions using only the axioms of the ambient type theory. The declaration is a theorem, meaning a statement proved in the machine-checked library, and it is used as a building block for larger results about subdivision and chain homotopies in the same file.

The theorem does not claim that every cone has zero boundary in a geometric sense, only that the algebraic boundary operator defined in the framework annihilates the algebraic cone operator. It does not establish anything about the physical world, such as the number of spatial dimensions or the value of any constant. It is a purely formal statement about the interaction of two definitions, and its significance lies in what it enables: a fully verified foundation for the framework's treatment of singular subdivision.

/-- `∂∂ = 0` on affine chains. -/
theorem abnd_comp_abnd (n : ℕ) :
    (abnd n).comp (abnd (n + 1)) = (0 : AC α (n + 2) →ₗ[ℤ] AC α n) := by
  classical
  refine AC.hom_ext fun w => ?_
  rw [LinearMap.comp_apply, abnd_asimplex, map_sum, LinearMap.zero_apply]
  have hexp : ∀ i : Fin (n + 3),
      abnd n ((-1 : ℤ) ^ (i : ℕ) • asimplex (w ∘ i.succAbove)) =
        ∑ j : Fin (n + 2), (-1 : ℤ) ^ ((i : ℕ) + (j : ℕ)) •
          asimplex (w ∘ i.succAbove ∘ j.succAbove) := by
    intro i
    rw [map_smul, abnd_asimplex, Finset.smul_sum]
    refine Finset.sum_congr rfl fun j _ => ?_
    rw [smul_smul, ← pow_add]
    rfl
  simp only [hexp]
  rw [← Finset.sum_product', Finset.univ_product_univ]
  have hsplit := Finset.sum_filter_add_sum_filter_not
    (Finset.univ : Finset (Fin (n + 3) × Fin (n + 2)))
    (fun p => (p.2 : ℕ) < (p.1 : ℕ))
    (fun p => (-1 : ℤ) ^ ((p.1 : ℕ) + (p.2 : ℕ)) •
      asimplex (w ∘ p.1.succAbove ∘ p.2.succAbove))
  rw [← hsplit]
  have hcancel : (∑ p ∈ Finset.univ.filter
        (fun p : Fin (n + 3) × Fin (n + 2) => (p.2 : ℕ) < (p.1 : ℕ)),
        (-1 : ℤ) ^ ((p.1 : ℕ) + (p.2 : ℕ)) •
          asimplex (w ∘ p.1.succAbove ∘ p.2.succAbove)) =
      -∑ p ∈ Finset.univ.filter
        (fun p : Fin (n + 3) × Fin (n + 2) => ¬ (p.2 : ℕ) < (p.1 : ℕ)),
        (-1 : ℤ) ^ ((p.1 : ℕ) + (p.2 : ℕ)) •
          asimplex (w ∘ p.1.succAbove ∘ p.2.succAbove) := by
    rw [← Finset.sum_neg_distrib]
    refine Finset.sum_bij'
      (i := fun p hp => ((⟨(p.2 : ℕ), by
          simp only [Finset.mem_filter_univ] at hp
          omega⟩ : Fin (n + 3)),
        (⟨(p.1 : ℕ) - 1, by
          have := p.1.isLt
          omega⟩ : Fin (n + 2))))
      (j := fun q hq => ((⟨(q.2 : ℕ) + 1, by
          have := q.2.isLt
          omega⟩ : Fin (n + 3)),
        (⟨(q.1 : ℕ), by
          simp only [Finset.mem_filter_univ] at hq
          have := q.2.isLt
          omega⟩ : Fin (n + 2))))
      ?_ ?_ ?_ ?_ ?_
    · intro p hp
      simp only [Finset.mem_filter_univ] at hp ⊢
      omega
    · intro q hq
      simp only [Finset.mem_filter_univ] at hq ⊢
      omega
    · intro p hp
      simp only [Finset.mem_filter_univ] at hp
      ext
      all_goals (try dsimp only)
      all_goals omega
    · intro q hq
      simp only [Finset.mem_filter_univ] at hq
      ext
      all_goals (try dsimp only)
      all_goals omega
    · intro p hp
      simp only [Finset.mem_filter_univ] at hp
      have htuple : w ∘ p.1.succAbove ∘ p.2.succAbove =
          w ∘ (⟨(p.2 : ℕ), by omega⟩ : Fin (n + 3)).succAbove ∘
            (⟨(p.1 : ℕ) - 1, by have := p.1.isLt; omega⟩ : Fin (n + 2)).succAbove := by
      -- faces commute: δ_i δ_j = δ_j δ_{i-1} for j < i
        funext k
        apply congrArg w
        apply Fin.ext
        have hk := k.isLt
        simp only [Function.comp_apply, SingularPrism.coe_succAbove]
        split_ifs <;> omega
      rw [htuple]
      have hsign : ((p.1 : ℕ) + (p.2 : ℕ)) =
          (((⟨(p.2 : ℕ), by omega⟩ : Fin (n + 3)) : ℕ) +
            ((⟨(p.1 : ℕ) - 1, by have := p.1.isLt; omega⟩ : Fin (n + 2)) : ℕ)) + 1 := by
        dsimp only
        omega
      rw [hsign, pow_succ, mul_neg_one, neg_smul]
  rw [hcancel, neg_add_cancel]

What this page does not claim

The theorem does not claim that every geometric cone has zero boundary, only the algebraic boundary operator annihilates the algebraic cone operator. The declaration does not establish any physical fact about dimensions or constants. The result is not a new mathematical discovery, but a machine-checked verification of a classical lemma.

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/SingularSubdivision.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: