IndisputableMonolith.Foundation.CircleFundamentalSimplex
Defines the fundamental singular 1-simplex on the exact topological circle S¹: the continuous once-around map from the standard 1-simplex, parameterized by the second barycentric coordinate so endpoints land at angles 0 and 2π. Downstream H₁ and winding modules treat this as the generator. Construction is definitional, assembling CircleParam primitives into an explicit singular simplex and its face identities.
claimThe module supplies the continuous once-around path $\gamma:\Delta^1\to S^1$ and the induced singular 1-simplex in $\operatorname{Sing}(S^1)$, with parameter the second barycentric coordinate so the two faces evaluate at angles $0$ and $2\pi$.
background
Recognition Science needs a by-hand computation of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ against Mathlib's imported TopCat.sphere 1, not a stand-in model. Upstream CircleParam fixes the exact carrier, a checked basepoint, and the constant singular 1-simplex face identities in TopCat.toSSet.obj (TopCat.sphere 1). That constant simplex is only API scaffolding; it is not the fundamental generator.
This module introduces the genuine once-around path. The domain is the topological standard 1-simplex $\Delta^1$; the codomain is the exact sphere object. Parameterization uses the second barycentric coordinate, forcing the two endpoints to the angles $0$ and $2\pi$ on the circle. Face maps of the resulting singular 1-simplex are then elementary evaluations of that path.
proof idea
Definition module, not a theorem package. It assembles a continuous path map from $\Delta^1$ into $S^1$, promotes it to a singular 1-simplex, and records the two face identities (face 0 and face 1) together with their equality statement. All content is definitional wiring of the CircleParam carrier and angle conventions; no deep algebraic argument appears here.
why it matters in Recognition Science
Supplies the concrete generator that later modules promote to a homology class. CircleH1Computation imports it as the local workbench atom toward $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ (still short of a strict T8 bridge until equivalence with Mathlib singular homology is proved). CircleWindingChain lifts path-level winding to singular 1-simplices of TopCat.sphere 1 and needs this simplex so that simplexDisplacement can be evaluated on the fundamental loop and shown to kill boundaries. Without an explicit once-around simplex pinned to the real sphere object, both the H₁ computation and the winding invariant remain formal.
scope and limits
- Does not prove $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
- Does not show winding is a homology invariant or kills boundaries.
- Does not replace or equate Mathlib's singular homology object.
- Does not feed the strict T8 dimensional bridge by itself.
- Does not treat higher simplices or the full singular chain complex.