module module moderate

`IndisputableMonolith.Foundation.CircleWindingChain`

Assembles the singular-simplex layer of the circle winding invariant: continuous maps from the standard 1-simplex into S¹, conversion to paths, and the induced real displacement and integer winding. Cited by the public T-1–T8 forcing spine and the T6–T8 honesty audit. Mostly definitional glue plus transport lemmas that pull path-lifting results onto singular 1-simplices.

claimSingular $1$-simplices $\sigma:\Delta^1\to S^1$ (continuous maps from the standard topological $1$-simplex $\Delta^1=\mathrm{stdSimplex}\,\mathbb{R}(\mathrm{Fin}\,2)$) are equipped with a real displacement and an integer winding by converting $\sigma$ to a path, lifting through the covering $\mathbb{R}\to S^1$, and measuring travel in $\mathbb{R}$. The once-around fundamental $1$-simplex has both faces at the chosen basepoint.

background

Recognition Science foundation work builds topological invariants on the exact Mathlib object TopCat.sphere 1, not a custom model. Upstream, the path winding module defines displacement of a path by lifting through the trigonometric covering map and proves the displacement is independent of lift choice once the start height is fixed. The lifting module supplies contractibility of simplex realization domains so unique lifts exist. The fundamental-simplex module constructs the once-around singular 1-simplex whose two faces coincide at the basepoint. The H₁ workbench targets the missing computation $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ without yet feeding the strict T8 bridge.

This module is the chain-level glue. It presents a singular 1-simplex as a continuous map out of the standard topological 1-simplex, records the analogous 2-simplex, and identifies the unit interval with $\Delta^1$ via a homeomorphism. Paths and 1-simplices are interconverted with round-trip identities, so the path displacement and winding invariants transport cleanly to singular 1-simplices.

proof idea

Definitional module with transport lemmas, not a single deep theorem. The interval-to-simplex map identifies $I$ with $\Delta^1$ and is checked at the endpoints. Conversion functors between paths and 1-simplices are shown mutually inverse by direct evaluation. Simplex displacement and winding are defined by converting the simplex to a path and applying the upstream path-displacement equality (the central technical result of the path winding module). Face agreement for the fundamental simplex is inherited from the fundamental-simplex construction. No new covering-space analysis is performed here.

why it matters in Recognition Science

Imported by the public dual forcing surface (δ-stratified map parallel to the unified forcing chain), by the public T-1 through T8 forcing spine, and by the T6–T8 spine honesty audit. Those parents need a well-defined integer winding on singular 1-chains of the exact $S^1$ object before the eight-tick octave (T7) and the $D=3$ dimensional step (T8) can be stated without a custom circle model. The module closes the gap between path-level lifting and the singular-simplicial set, so the H₁ workbench and the T-bridge can cite a single chain-level invariant rather than ad-hoc path data.

scope and limits

Does not prove $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$; that stays in the H₁ workbench.
Does not replace Mathlib singular homology objects; works directly on TopCat.sphere 1.
Does not by itself force T6–T8; only supplies the winding-chain layer.
Does not treat higher simplices beyond the 2-simplex data needed for faces.
Does not strengthen covering uniqueness beyond the upstream lifting lemmas.

used by (3)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Foundation.PublicSpine module_import
IndisputableMonolith.Foundation.TMinus1ToT8Bridge module_import
IndisputableMonolith.Verification.T6T8SpineAudit module_import

depends on (4)

Lean names referenced from this declaration's body.

IndisputableMonolith.Foundation.CircleFundamentalSimplex module_import
IndisputableMonolith.Foundation.CircleH1Computation module_import
IndisputableMonolith.Foundation.CircleLifting module_import
IndisputableMonolith.Foundation.CircleWinding module_import

declarations in this module (465)

abbrev OneSimplex L64
abbrev TwoSimplex L68
def intervalToSimplex L73
theorem intervalToSimplex_apply L76
theorem intervalToSimplex_zero L79
theorem intervalToSimplex_one L86
def oneSimplexPath L94
def oneSimplexOfPath L98
theorem oneSimplexPath_ofPath L103
theorem oneSimplexOfPath_oneSimplexPath L111
def simplexDisplacement L119
def simplexWinding L123
def faceMap L127
theorem faceMap_apply L131
theorem faceMap_two_coord_one L138
theorem faceMap_two_coord_two L159
theorem faceMap_zero_coord_one L177
theorem faceMap_zero_coord_two L199
theorem faceMap_one_coord_one L220
theorem faceMap_one_coord_two L238
def face L258
def simplexEdge L262
theorem simplexEdge_apply L264
abbrev V L268
theorem simplexEdge_zero L270
theorem simplexEdge_one L274
def edge01 L279
def edge12 L285
def edge02 L291
theorem oneSimplexPath_face L298
theorem simplexDisplacement_face L305
theorem simplexDisplacement_boundary L318
theorem simplexWinding_boundary L355
theorem intervalToSimplex_coord_one L363
def coneBaseParam L371
theorem coneBaseParam_coe_of_coord_two_ne_one L391
theorem continuousAt_coneBaseParam_coe_of_coord_two_ne_one L400
theorem continuousAt_coneBaseParam_of_coord_two_ne_one L422
theorem coneBaseParam_faceMap_two_coe L431
theorem coneBaseParam_simplexEdge_two_coe L441
theorem coneBaseParam_faceMap_zero_coe_of_not_apex L448
theorem coneBaseParam_faceMap_one_coe_of_not_apex L465
def coneLiftAngle L478
theorem coneLiftAngle_sub_start L483
theorem norm_coneLiftAngle_sub_start_le L494
theorem coneLiftAngle_tendsto_apex L509
theorem continuousAt_coneLiftAngle_of_coord_two_ne_one L538
theorem coneLiftAngle_simplexEdge_two L553
theorem coneLiftAngle_simplexEdge_one L566
theorem coneLiftAngle_simplexEdge_zero_of_lift_endpoint_eq L595
def coneCirclePoint L625
theorem coneCirclePoint_tendsto_apex L629
theorem continuousAt_coneCirclePoint_apex L641
theorem continuousAt_coneCirclePoint_of_coord_two_ne_one L657
theorem stdSimplex_eq_vertex_two_of_coord_two_eq_one L666
theorem continuous_coneCirclePoint L693
theorem coneCirclePoint_simplexEdge_two L703
theorem coneCirclePoint_simplexEdge_one L710
theorem coneCirclePoint_simplexEdge_zero_of_lift_endpoint_eq L718
theorem coneLiftAngle_faceMap_two_of_oneSimplex L728
theorem coneLiftAngle_faceMap_two L743
theorem coneCirclePoint_faceMap_two_of_oneSimplex L758
theorem coneCirclePoint_faceMap_two L773
theorem coneLiftAngle_faceMap_one L782
theorem coneLiftAngle_faceMap_zero_of_lift_endpoint_eq L802
theorem coneLiftAngle_faceMap_zero L824
def coneTerminalSide L843
def constantOneSimplex L852
theorem coneTerminalSide_eq_constantOneSimplex_of_lift_endpoint_eq L857
theorem coneTerminalSide_eq_constantOneSimplex_of_simplexWinding_zero L870
theorem coneCirclePoint_faceMap_one L880
theorem coneCirclePoint_faceMap_zero_of_lift_endpoint_eq L888
theorem coneCirclePoint_faceMap_zero L898
theorem coneCirclePoint_side_faces_eq_of_lift_endpoint_eq L908
theorem coneCirclePoint_side_faces_eq_of_winding_zero L917
def coneCircleMapOfContinuous L928
theorem coneCircleMapOfContinuous_face_two L935
theorem coneCircleMapOfContinuous_face_two_path L942
theorem coneCircleMapOfContinuous_face_zero L951
theorem coneCircleMapOfContinuous_face_one L958

… and 385 more