Foundation Singular Subdivision

Subdivision as a structural tool

Subdivision is a classical geometric operation: cut a triangle into smaller triangles, a cube into smaller cubes, or an interval into shorter intervals. In algebraic topology, the singular chain complex of a space is built from continuous maps of standard simplices into that space, and subdivision is the process of replacing each such map with a formal sum of maps on finer simplices. The operation is central because it preserves the essential shape of the space while making its structure finer, a technique used in proofs of invariance and in computations of homology.

The standard barycentric subdivision of a simplex is the classical example. Given a simplex with vertices, its barycentric subdivision introduces a new vertex at the average of any subset of the original vertices, then forms all smaller simplices from these new points. The operation is iterable: subdivide again to get an even finer triangulation. A key classical fact is that the boundary of a subdivided simplex is the subdivided boundary, a compatibility that makes subdivision a chain map on the singular complex.

In Recognition Science, the framework models this same operation inside its discrete ledger: a record of events where each entry is a formal integer combination of vertex tuples. The module defines an affine chain complex, where a chain is a finite integer combination of tuples of points. Subdivision appears as an operator on these chains, and the central result is that the boundary operator commutes with subdivision: subdividing then taking the boundary gives the same result as taking the boundary then subdividing. This compatibility is proved as a theorem in the machine-checked library of formal theorems, along with the naturality of subdivision under continuous maps.

The framework also introduces a cone construction, which adds a new point to every simplex in a chain, and an augmentation map that counts the total coefficient of a zero-dimensional chain. Iterating subdivision yields a sequence of finer approximations, and the framework proves that the boundary of the iterated subdivision remains compatible at every stage. These results establish that subdivision is a well-behaved structural operation inside the ledger, not merely a geometric convenience.

What this establishes in plain language is that the discrete record can be refined without losing its algebraic coherence. The boundary of a refined chain is the refined boundary, so the ledger's structure is stable under subdivision. This is a necessary foundation for any later claim that the ledger's geometry is independent of how finely it is cut, a property that any sound theory of space would require.

/-- The singular subdivision operator is a chain map: `∂ ∘ S = S ∘ ∂`. -/
theorem sdOp_comp_bnd (X : TopCat.{0}) (n : ℕ) :
    sdOp X (n + 1) ≫ bnd X n = bnd X n ≫ sdOp X n := by
  apply Sigma.hom_ext
  intro s
  rw [← Category.assoc, ← Category.assoc, gen_sdOp, gen_d]
  have hL : sdGen X (n + 1) s ≫ bnd X n =
      toChain (simplexEquiv X (n + 1) s) n
        (asub (baryFn (n + 1)) n (abnd n (asimplex (idTuple (n + 1))))) := by
    have h := LinearMap.congr_fun
      (toChain_comp_abnd (simplexEquiv X (n + 1) s) n)
      (asub (baryFn (n + 1)) (n + 1) (asimplex (idTuple (n + 1))))
    rw [LinearMap.comp_apply, LinearMap.comp_apply] at h
    have hcomm := LinearMap.congr_fun (abnd_comp_asub (baryFn (n + 1)) n)
      (asimplex (idTuple (n + 1)))
    rw [LinearMap.comp_apply, LinearMap.comp_apply] at hcomm
    rw [← hcomm]
    exact h
  rw [hL, abnd_asimplex, map_sum, map_sum, Preadditive.sum_comp]
  refine Finset.sum_congr rfl fun k _ => ?_
  rw [map_smul, map_smul, Preadditive.zsmul_comp]
  congr 1
  rw [δ_eq_pushSimplex, gen_pushSimplex_comp_sdOp]

/-- Naturality of the singular subdivision operator. -/
theorem sdOp_natural (f : X ⟶ Y) (n : ℕ) :
    chainMap f n ≫ sdOp Y n = sdOp X n ≫ chainMap f n := by
  apply Sigma.hom_ext
  intro s
  rw [← Category.assoc, ← Category.assoc, gen_map, gen_sdOp, gen_sdOp]
  have hR := LinearMap.congr_fun
    (toChain_comp_chainMap (simplexEquiv X n s) f n)
    (asub (baryFn n) n (asimplex (idTuple n)))
  rw [LinearMap.comp_apply] at hR
  have hL : sdGen Y n ((TopCat.toSSet.map f).app (op ⦋n⦌) s) =
      toChain (f.hom.comp (simplexEquiv X n s)) n
        (asub (baryFn n) n (asimplex (idTuple n))) := by
    show toChain (simplexEquiv Y n ((TopCat.toSSet.map f).app (op ⦋n⦌) s)) n
        (asub (baryFn n) n (asimplex (idTuple n))) = _
    rw [simplexEquiv_map]
  rw [hL, ← hR]
  rfl

/-- The cone with apex `b`, `AC α n → AC α (n+1)`: prepend `b` to every
vertex tuple. -/
noncomputable def acone (b : α) : AC α n →ₗ[ℤ] AC α (n + 1) :=
  Finsupp.lmapDomain ℤ ℤ (fun w => Fin.cons b w)

/-- The augmentation `ε : AC α 0 → ℤ` (sum of coefficients). -/
noncomputable def eps (α : Type) : AC α 0 →ₗ[ℤ] ℤ :=
  Finsupp.linearCombination ℤ (fun _ : Fin 1 → α => (1 : ℤ))

What this page does not claim

This module does not prove that subdivision produces a unique or canonical refinement of a chain. This module does not establish any physical interpretation of subdivision as a process in spacetime. This module does not derive the golden ratio or any specific dimension from the subdivision operation.

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: