twoSimplexCoordOneParam_face_two
plain-language theorem explainer
On the base face δ₂ : Δ¹ → Δ², the second barycentric coordinate of the image equals the standard Δ¹ ≃ I homeomorphism. Anyone building singular chains or face restrictions for the S¹ winding invariant cites this. The proof is a one-line coordinate comparison after extensionality.
Claim. For every point $x$ of the standard $1$-simplex $\Delta^1 = \mathrm{stdSimplex}\,\mathbb{R}\,(\mathrm{Fin}\,2)$, the second barycentric coordinate of its image under the face map $\delta_2:\Delta^1\to\Delta^2$, read as a unit-interval parameter, equals the image of $x$ under the canonical homeomorphism $\Delta^1\simeq I$.
background
The module lifts path-level winding on $S^1$ to singular simplices and proves that displacement kills boundaries: for every singular $2$-simplex $F$, $\mathrm{disp}(\partial_0 F)-\mathrm{disp}(\partial_1 F)+\mathrm{disp}(\partial_2 F)=0$. That identity is the chain-level half of the split injection $H_1(S^1;\mathbb{Z})\hookrightarrow\mathbb{Z}$.
Here $\mathrm{faceMap},i$ is the continuous affine map $\Delta^1\to\Delta^2$ induced by the coface $\delta i:,[1]\to,[2]$. The base face $i=2$ is the edge opposite the last vertex. The map $\mathrm{twoSimplexCoordOneParam}$ reads the second barycentric coordinate $x_1$ of a point of $\Delta^2$ as an element of the unit interval $I$. The companion homeomorphism $\mathrm{stdSimplexHomeomorphUnitInterval}$ identifies $\Delta^1$ with $I$ by the same coordinate.
Upstream, $\mathrm{faceMap_two_coord_one}$ records that $\delta_2$ preserves the second barycentric coordinate, and $\mathrm{stdSimplexHomeomorphUnitInterval_coe}$ identifies that homeomorphism with evaluation of coordinate $1$.
proof idea
Term-mode after ext on the unit-interval value. Both sides are real numbers in $[0,1]$; the goal reduces to equality of the second barycentric coordinate of $\mathrm{faceMap},2,x$ with the real underlying the homeomorphism image of $x$. Rewrite by $\mathrm{faceMap_two_coord_one}$ (base face preserves coordinate $1$) and $\mathrm{stdSimplexHomeomorphUnitInterval_coe}$ (homeomorphism coe is coordinate $1$). Done.
why it matters
Feeds $\mathrm{pathBacktrackMap_face_two}$, which identifies the $\delta_2$ face of the path-backtrack $2$-simplex with the singular $1$-simplex of the original path. That face identity is part of the $2$-simplex telescoping used for $\mathrm{simplexDisplacement_boundary}$: the alternating face sum of displacement vanishes because the boundary walk is homotopic rel endpoints inside the convex $\Delta^2$.
In the module's program this is scaffolding for the "kills boundaries" half of the winding homomorphism on $1$-cycles, the left inverse to the fundamental class that gives split-injectivity of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. It does not touch the generation/surjectivity half (prism subdivision), which remains open relative to Mathlib singular homology. No direct link to the T0–T8 forcing chain; the landmark is the circle homology computation supporting Recognition's topological invariants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.