twoSimplexCoordOneParam
plain-language theorem explainer
Extracts the middle barycentric coordinate of a point in the standard 2-simplex and packages it as a unit-interval parameter. Anyone building singular prism maps or face restrictions for the S¹ winding chain cites this coordinate projection. The body is a one-line subtype package: the Fin-3 coordinate at index 1, with the standard-simplex membership proof that it lies in [0,1].
Claim. For $x$ in the standard $2$-simplex $\Delta^2 = \mathrm{stdSimplex}\,\mathbb{R}\,(\mathrm{Fin}\,3)$, return the middle barycentric coordinate $x_1$ as an element of the closed unit interval $I=[0,1]$.
background
The module lifts path-level winding and displacement on the circle to singular simplices of $S^1$, and proves that displacement vanishes on boundaries of $2$-simplices. That identity is the chain-level fact making winding a homology invariant, and with the once-around generator it supplies the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
The standard $2$-simplex consists of triples $(x_0,x_1,x_2)$ of nonnegative reals summing to $1$. Its three faces are the usual face maps omitting one vertex. Paths on $S^1$ are continuous maps from the unit interval $I$; to push a path through a $2$-simplex one needs a continuous $I$-valued coordinate on $\Delta^2$.
This definition supplies exactly that coordinate: the middle barycentric weight, read as a time parameter. Sibling constructions reparameterize $\Delta^1$ to $I$ and define simplex displacement via path displacement; the present map is the $2$-dimensional analogue used for prisms and face comparisons.
proof idea
Definition, not a proof. The body packages the evaluation of the underlying Fin-3 coordinate function at index $1$ into the subtype $I$, using the library fact that every barycentric coordinate of a standard-simplex point lies in $[0,1]$. No further algebraic work.
why it matters
This coordinate is the parameter map inside the triangular backtrack prism: that prism sends $x\in\Delta^2$ to $\gamma(x_1)$ for a path $\gamma$, so its three faces become the reversed path, a constant edge, and the original path. Continuity of the coordinate is proved immediately downstream and is composed into the prism's continuity.
The three face lemmas pin the coordinate on each face of $\Delta^2$: face $1$ collapses it to $0$, face $2$ recovers the standard $\Delta^1\simeq I$ homeomorphism, and face $0$ recovers the reversed interval parameter. Those identities are the concrete face computations needed when checking that displacement of the alternating boundary of a $2$-simplex vanishes (the telescoping argument in the module doc).
In the broader Recognition foundation this sits in the singular-homology half of the circle winding story, not in the T0–T8 forcing chain itself; it is infrastructure for the $H_1(S^1)\cong\mathbb{Z}$ comparison that underwrites topological consistency of the eight-tick and winding picture.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.