Foundation Circle Winding Chain

The winding invariant

The winding number answers a simple question: how many times does a closed loop wrap around a circle? Draw a curve on a flat surface that ends where it began, and count how many full turns it makes around a fixed point. The answer is always an integer, and it cannot change unless the curve is torn or passes through the point itself. This invariant, known since the nineteenth century, is one of the first tools mathematicians use to tell spaces apart.

In the framework's machine-checked library of formal theorems, the module foundation circle winding chain builds this classical idea from the ground up. It assigns to every continuous map from a line segment into the circle a real number called the displacement, equal to 2π times the winding. The central theorem proves a cancellation law: when three such segments form the boundary of a triangle, the alternating sum of their displacements is exactly zero. This is the chain-level statement that winding kills boundaries, the property that makes the invariant survive when shapes are deformed.

The proof works by a geometric telescoping argument. A path from one corner of a triangle to another along two edges is homotopic, meaning it can be continuously deformed without moving its endpoints, to the direct edge. Pushing this deformation through the map to the circle, additivity and homotopy invariance of the displacement combine to give the vanishing alternating sum. This is the same reasoning that underlies Stokes' theorem in calculus, where the integral of a derivative over a region equals the integral over its boundary.

Together with the fact that the once-around generator has winding one, this yields a homomorphism on 1-cycles that is a left inverse to the fundamental class. The module proves the split-injective half of the isomorphism H₁(S¹; ℤ) ≅ ℤ, showing that every integer winding number is realized by some cycle. The converse, that every 1-cycle is homologous to an integer multiple of the fundamental cycle, remains open in the library because it requires a subdivision operator that Mathlib's singular homology does not yet provide.

What this establishes in plain language is that the winding number is not an artifact of a particular drawing or coordinate system. It is a stable feature of the circle itself, preserved under continuous deformation, and it can be computed from any triangulation of the space. The module provides a formal guarantee, checked by the machine, that the alternating sum of displacements around any triangle vanishes, which is the local condition that makes the global invariant well-defined.

/-- **The displacement of a singular `1`-simplex**: the lift-independent angular
travel `2π × (winding number)`, obtained from the path-level displacement. -/
def simplexDisplacement (f : OneSimplex) : ℝ := pathDisplacement (oneSimplexPath f)

/-- Boundary coefficient of any finite free edge-flow is the finite incidence sum
over its support. -/
theorem vertexBoundaryCoeff_eq_incidenceSum_holds :
    vertexBoundaryCoeff_eq_incidenceSum := by
  intro _ c v
  induction c using Finsupp.induction_linear with
  | zero =>
      rw [boundaryIncidenceSum_zero]
      unfold vertexBoundaryCoeff vertexCoeff
      change (0 : singularZeroChainFree).toFun v = 0
      rfl
  | add f g hf hg =>
      rw [boundaryIncidenceSum_add]
      have hadd : vertexBoundaryCoeff (f + g) v =
          vertexBoundaryCoeff f v + vertexBoundaryCoeff g v := by
        unfold vertexBoundaryCoeff vertexCoeff
        rw [map_add]
        rfl
      rw [hadd, hf, hg]
  | single e n =>
      rw [boundaryIncidenceSum_single]
      have hsingle : (Finsupp.single e n : singularOneChainFree) =
          n • ModuleCat.freeMk e := by
        rw [ModuleCat.freeMk]
        rw [Finsupp.smul_single]
        simp
      rw [hsingle]
      unfold vertexBoundaryCoeff vertexCoeff
      rw [map_zsmul]
      change (n • (ModuleCat.Hom.hom singularOneBoundaryFree (ModuleCat.freeMk e) :
          singularZeroChainFree)).toFun v =
        n * incidenceCoeff e v
      change n * ((ModuleCat.Hom.hom singularOneBoundaryFree (ModuleCat.freeMk e) :
          singularZeroChainFree).toFun v) =
        n * incidenceCoeff e v
      rw [show (ModuleCat.Hom.hom singularOneBoundaryFree (ModuleCat.freeMk e) :
            singularZeroChainFree).toFun v =
          vertexBoundaryCoeff (ModuleCat.freeMk e) v by rfl]
      rw [vertexBoundaryCoeff_freeMk]

/-- The exact remaining generation statement, in homology-level form.  It says
that every degree-`1` homology class is an integer multiple of the fundamental
circle class.  This is deliberately stated as surjectivity of the already-built
comparison morphism `fundamentalHomologyClass`; proving this is the remaining
surjective half of `H₁(S¹;ℤ) ≅ ℤ`.

Note: this is **not** needed for the strict T-1-to-T8 frontier closure, which only
requires nonvanishing (`circleH1ZNonzero_unconditional`).  Surjectivity is the
stronger statement that upgrades nonvanishing to the full isomorphism. -/
def fundamentalHomologyClass_surjective : Prop :=
  Function.Surjective (ModuleCat.Hom.hom fundamentalHomologyClass)

/-- The exact remaining generation statement, in homology-level form.  It says
that every degree-`1` homology class is an integer multiple of the fundamental
circle class.  This is deliberately stated as surjectivity of the already-built
comparison morphism `fundamentalHomologyClass`; proving this is the remaining
surjective half of `H₁(S¹;ℤ) ≅ ℤ`.

Note: this is **not** needed for the strict T-1-to-T8 frontier closure, which only
requires nonvanishing (`circleH1ZNonzero_unconditional`).  Surjectivity is the
stronger statement that upgrades nonvanishing to the full isomorphism. -/
def fundamentalHomologyClass_surjective : Prop :=
  Function.Surjective (ModuleCat.Hom.hom fundamentalHomologyClass)

What this page does not claim

This module does not prove the full isomorphism H₁(S¹; ℤ) ≅ ℤ, only the split-injective half. The module does not construct a subdivision operator for singular homology. This page does not claim the winding invariant is derived from the framework's cost function or forcing chain.

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