Foundation Circle Fundamental Simplex

The once-around loop

The circle is the shape you get by taking a line segment and gluing its two ends together. Its most basic feature is the loop that starts at the glued point, travels all the way around, and comes back to where it began. In topology, this is called the fundamental 1-simplex of the circle: the once-around path that generates every other loop, up to continuous deformation. The module CircleFundamentalSimplex constructs exactly this path in the framework's machine-checked library of formal theorems, using the standard topological definition of the circle as the set of points at distance one from the origin in the plane.

The construction works by parameterizing the path with a number between 0 and 1, mapping that number to the angle it sweeps out on the circle. The point at parameter 0 sits at angle 0, and the point at parameter 1 sits at angle 2π, which is the same physical point on the circle. The path is continuous: small changes in the parameter produce small changes in the point on the circle. This is the geometric generator candidate for the later computation of the circle's first homology group, the algebraic measure of how many independent loops the circle has.

What is proved is that this once-around path is genuinely a loop. A loop in topology is a path whose starting point and ending point coincide. The two faces of the 1-simplex, its two endpoints, are shown to be equal in the actual singular simplicial set of the circle. Both faces evaluate to the chosen basepoint, the point where the segment's ends were glued. The proof is direct: it rewrites each face using the definition of the path and the fact that angles 0 and 2π correspond to the same point on the circle.

In Recognition Science, this formal loop is the first concrete instance of a recognition cycle. The framework models reality as a ledger, a discrete record of recognition events, and the cost of recognition is forced by a proved functional equation. The circle's once-around path is the continuous geometric shadow of that discrete cycle: a closed structure that returns to its starting state. The construction establishes, in the framework's own terms, that the simplest closed path on the circle exists as a formal object, with its two endpoints provably identified. This is the foundation on which later claims about the eight-tick recognition cycle and the golden ratio as the unique self-similar scaling are built.

The consequence is that the framework's discrete ledger and the classical continuous circle are not separate worlds. The once-around loop is the bridge: it is a topological object, fully defined in the standard singular simplicial set, and it is also the geometric generator that the framework's later homology computations will use. The reader can now see that the framework's claims about cycles and recognition are anchored in a precise, machine-checked construction of the circle's most basic loop.

/-- The once-around singular 1-simplex in `TopCat.toSSet.obj (TopCat.sphere 1)`.
This is the geometric generator candidate for the later H1 computation. -/
def fundamentalSphereOneSingularOneSimplex :
    (TopCat.toSSet.obj (TopCat.sphere 1)).obj (op (SimplexCategory.mk 1)) :=
  (TopCat.toSSetObjEquiv (TopCat.sphere 1) (op (SimplexCategory.mk 1))).symm
    fundamentalCirclePathMap

/-- 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]

/-- 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 `δ 1` face of the fundamental singular 1-simplex is the chosen
basepoint.  This endpoint evaluates the second barycentric coordinate at `0`,
hence the angle `0`. -/
theorem fundamentalSphereOneSingularOneSimplex_face_one :
    (TopCat.toSSet.obj (TopCat.sphere 1)).δ (1 : 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.δ (1 : Fin 2))) x :
            stdSimplex ℝ (Fin 2)) : Fin 2 → ℝ) 1) =
    sphereOneBasepoint
  rw [show
      ((stdSimplex.map (S := ℝ) ⇑(ConcreteCategory.hom (SimplexCategory.δ (1 : Fin 2))) x :
          stdSimplex ℝ (Fin 2)) : Fin 2 → ℝ) 1 = 0 by
    rw [stdSimplex.map_coe, FunOnFinite.linearMap_apply_apply]
    simp [SimplexCategory.δ]]
  simpa using trigCirclePoint_zero

What this page does not claim

This module does not compute the first homology group of the circle; it only constructs the generator candidate. The framework's discrete ledger is not shown to be equivalent to the continuous circle; the loop is a geometric shadow, not a proof of identity. No claim is made about the golden ratio or the eight-tick cycle in this module; those are established elsewhere in the framework.

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: