linearTwoSimplexMap_apply
plain-language theorem explainer
Evaluating the lift-affine singular 2-simplex at a barycentric point equals the trigonometric circle point of the corresponding affine combination of three real lifts. Anyone computing faces or displacements of geodesic 2-simplices on S¹ cites this. The proof is pure definitional equality (rfl), exposed as a simp lemma.
Claim. For real lifts $p,q,r$ and any point $x$ of the standard $2$-simplex $\Delta^2$, the lift-affine singular $2$-simplex built from $(p,q,r)$ sends $x$ to the trigonometric point on $S^1$ at angle $(1-x_1-x_2)p + x_1 q + x_2 r$.
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}(\delta_0 F)-\mathrm{disp}(\delta_1 F)+\mathrm{disp}(\delta_2 F)=0$. That identity, with the generator evaluation, supplies the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
A lift-affine (geodesic) singular $2$-simplex is the continuous map $\Delta^2\to S^1$ that sends barycentric coordinates to the once-around trigonometric parametrization of the affine combination of three real lifts $p,q,r$. The trigonometric point map is the standard embedding $t\mapsto(\cos t,\sin t)$ into the exact TopCat.sphere 1 object. Faces of a singular $2$-simplex are compositions with the standard face maps of $\Delta^2$.
This evaluation lemma is the pointwise unfolding of that construction, so face computations reduce to algebra on barycentric coordinates.
proof idea
One-line term proof by rfl: the right-hand side is exactly the toFun field of the lift-affine $2$-simplex definition. Marked @[simp] so later face identities can rewrite the composition automatically.
why it matters
Feeds the three face lemmas: $\delta_0$ of the lift-affine simplex is the geodesic from $q$ to $r$, $\delta_1$ from $p$ to $r$, and $\delta_2$ from $p$ to $q$. Those identities are the concrete edges needed when checking that geodesic $2$-simplices realize the telescoping homotopy behind simplex-displacement killing boundaries.
In the broader Recognition foundation, the circle winding chain is the singular-homology half of identifying $H_1(S^1)$ with $\mathbb{Z}$, which underwrites period and octave bookkeeping (eight-tick structure) once the generator is normalized. The module notes that the converse generation half still needs a simplicial prism or subdivision operator not yet in Mathlib; this lemma is only on the evaluation side of the existing kills-boundaries argument.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.