Foundation Circle Fundamental Simplex Fundamental Sphere One Singular One Simple

The once-around loop

A circle has a simple, familiar feature: a path that starts at a point, goes once around, and returns to that same point. In algebraic topology, this idea is made precise with singular simplices, which are continuous maps from standard triangles or intervals into a space. The declaration fundamentalSphereOneSingularOneSimplex_face_zero concerns one specific such map: the once-around path on the circle, parameterized so that it starts at angle 0 and ends at angle 2π.

The theorem states that the first face of this singular 1-simplex, the endpoint at angle 2π, is exactly the constant zero-simplex at the chosen basepoint. In plainer terms, it proves that the end of the loop lands precisely on the basepoint, no more and no less. This is one half of the statement that the path is a loop; its companion declaration proves the other end, at angle 0, also lands on the basepoint. Together, the two declarations establish that the once-around path is a genuine closed loop in the circle's singular simplicial set.

In Recognition Science, this declaration is a building block. The framework models physical structure through recognition events, and here it constructs a fundamental loop in the circle, the geometric generator candidate for later homology computations. The declaration is a theorem in the machine-checked library of formal theorems, meaning its proof has been verified by a computer. It does not, however, claim that this loop generates the entire first homology group, nor does it assert anything about the circle's higher-dimensional structure. Those are separate, later steps.

What the declaration does not claim is equally precise. It does not prove that the once-around path is unique, nor that it is non-contractible. It merely fixes one endpoint of a specific loop. The power of the declaration lies in its exactness: it gives a formal, checkable guarantee that a chosen geometric object behaves as expected, a necessary first step before any deeper topological or physical conclusions can be drawn.

/-- The `δ 0` face of the fundamental singular 1-simplex is the chosen
basepoint.  In Mathlib's simplex convention this endpoint evaluates the second
barycentric coordinate at `1`, hence the angle `2π`. -/
theorem fundamentalSphereOneSingularOneSimplex_face_zero :
    (TopCat.toSSet.obj (TopCat.sphere 1)).δ (0 : Fin 2)
      fundamentalSphereOneSingularOneSimplex =
        constantSphereOneSingularZeroSimplex := by
  apply (TopCat.toSSetObjEquiv (TopCat.sphere 1) (op (SimplexCategory.mk 0))).injective
  ext x
  dsimp [TopCat.toSSetObjEquiv, TopCat.toSSet,
    CategoryTheory.Presheaf.restrictedULiftYoneda,
    CategoryTheory.SimplicialObject.δ,
    CategoryTheory.ConcreteCategory.homEquiv,
    Homeomorph.continuousMapCongr,
    fundamentalSphereOneSingularOneSimplex, fundamentalCirclePathMap,
    constantSphereOneSingularZeroSimplex]
  change trigCirclePoint
      (2 * Real.pi *
        ((stdSimplex.map (S := ℝ) ⇑(ConcreteCategory.hom (SimplexCategory.δ (0 : Fin 2))) x :
            stdSimplex ℝ (Fin 2)) : Fin 2 → ℝ) 1) =
    sphereOneBasepoint
  rw [show
      ((stdSimplex.map (S := ℝ) ⇑(ConcreteCategory.hom (SimplexCategory.δ (0 : Fin 2))) x :
          stdSimplex ℝ (Fin 2)) : Fin 2 → ℝ) 1 = 1 by
    rw [stdSimplex.map_coe, FunOnFinite.linearMap_apply_apply]
    simp [SimplexCategory.δ]
    decide]
  simpa using trigCirclePoint_two_pi

/-- The fundamental once-around singular 1-simplex is a loop: its two faces are
equal in the actual singular simplicial set of `TopCat.sphere 1`. -/
theorem fundamentalSphereOneSingularOneSimplex_faces_eq :
    (TopCat.toSSet.obj (TopCat.sphere 1)).δ (0 : Fin 2)
      fundamentalSphereOneSingularOneSimplex =
        (TopCat.toSSet.obj (TopCat.sphere 1)).δ (1 : Fin 2)
          fundamentalSphereOneSingularOneSimplex := by
  rw [fundamentalSphereOneSingularOneSimplex_face_zero,
    fundamentalSphereOneSingularOneSimplex_face_one]

What this page does not claim

The declaration does not prove that the once-around loop generates the first homology group. It does not claim the loop is non-contractible or unique. It says nothing about the circle's higher-dimensional simplices or its fundamental group.

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