coneCirclePoint_faceMap_one
plain-language theorem explainer
On the middle face δ₁ of the standard 2-simplex, the pointwise S¹-cone of a continuous path γ is constantly the path start γ(0). Homology and cone-packaging arguments cite this when the continuous cone map is assembled and when side faces are compared under lifted-endpoint equality. The proof unfolds the cone, applies the constant lifted-angle face lemma, and projects through the covering identity.
Claim. For every continuous path $\gamma : I \to S^1$ and every point $x \in \Delta^1$, the pointwise cone evaluated on the image of $x$ under the coface face map $\delta_1 : \Delta^1 \to \Delta^2$ equals the path start $\gamma(0)$.
background
The module lifts the path-level winding/displacement invariant of the circle covering to singular simplices of $S^1$, aiming at the chain-level identity that winding kills boundaries: for every singular 2-simplex $F$, the alternating face sum of displacements vanishes. That identity, with the generator evaluation on the once-around loop, supplies the split-injective half of $H_1(S^1;\mathbb{Z}) \cong \mathbb{Z}$.
Here $S^1$ is the carrier of TopCat.sphere 1. The trigonometric covering sends a real angle to a circle point; pathLift is a continuous real lift of a path $\gamma$, and the covering identity states that projecting the lift recovers $\gamma$. The face map $\delta_i$ is the affine coface embedding $\Delta^1 \hookrightarrow \Delta^2$. The pointwise cone is defined by projecting a lifted cone angle through the covering: cone point of $\gamma$ at $x$ is the cover of the lifted cone angle at $x$.
Upstream, the lifted-angle face lemma already shows that on the middle face the lifted cone angle is constantly the lift value at time 0. This declaration is the $S^1$-valued shadow of that constancy.
proof idea
Term-mode, three steps. Unfold the pointwise cone definition so the goal is equality of cover-projections of angles. Rewrite by the upstream face lemma: the lifted cone angle on $\delta_1(x)$ equals the path lift at time 0. Finish by functional congruence of the covering identity trigCirclePoint ∘ pathLift γ = γ evaluated at 0, which yields $\gamma(0)$.
why it matters
This is the pointwise $\delta_1$ side restriction needed to package the cone as a continuous singular 2-simplex and to control its faces. Downstream, it is the exact pointwise step in the continuous-cone face theorem: under a continuity hypothesis, the $\delta_1$ face of the packaged cone is the constant 1-simplex at the apex $\gamma(0)$. It is also rewritten into the side-face comparison that equates the two lateral faces once the lifted endpoints of the base path agree (the pointwise form of a future face equation face $F,0 =$ face $F,1$).
In the module narrative those face controls feed the 2-simplex telescoping that proves displacement kills boundaries, the chain-level fact behind the winding homomorphism on 1-cycles. Within Recognition Science this sits in the Foundation layer that makes the circle's first homology available without axioms or local $S^1$ replacements; it does not itself touch the forcing chain T0–T8, but it underwrites the topological bookkeeping those later steps rely on when periods and windings appear.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.