simplexEdge_apply
plain-language theorem explainer
The i-th geometric edge of the standard 2-simplex, evaluated at a unit-interval point t, equals the i-th affine face map applied to the standard reparameterization of t onto Δ¹. Anyone simplifying cone-lift or face-displacement calculations on singular simplices of S¹ cites this. The proof is pure definitional equality (rfl) from the composition that defines the edge.
Claim. For each face index $i \in \{0,1,2\}$ and each $t \in I = [0,1]$, the $i$-th geometric edge of $\Delta^2$ at $t$ equals the $i$-th affine face map $\Delta^1 \to \Delta^2$ applied to the standard reparameterization $t \mapsto (1-t,\, t)$ of the unit interval onto $\Delta^1$.
background
This module lifts the path-level winding and displacement invariant of the circle to singular simplices of $S^1$, and proves that displacement kills boundaries: for every singular 2-simplex $F$, the alternating face sum of displacements vanishes. That identity is the chain-level reason winding descends to a homology invariant, and with the generator evaluation it supplies the split-injective half of $H_1(S^1;\mathbb{Z}) \cong \mathbb{Z}$.
The standard 1-simplex is reparameterized from the unit interval by $t \mapsto (1-t, t)$, the inverse of Mathlib's homeomorphism to $I$. Face maps $\Delta^1 \to \Delta^2$ are the continuous affine maps induced by the cofaces $\delta_i : [1] \to [2]$ in the simplex category. The geometric edge selected by index $i$ is defined as the composition of that face map with the interval reparameterization, so it is a continuous path $I \to \Delta^2$ along the corresponding edge of the 2-simplex.
proof idea
One-line term proof by rfl. The edge is defined as the composition of the $i$-th face map with the interval-to-simplex reparameterization, so evaluating the edge at $t$ is definitionally the face map at the reparameterized point. No lemmas are applied beyond unfolding that definition.
why it matters
This simp lemma is the standard unfolding step for every computation that restricts cone data or lifted angles to an edge of $\Delta^2$. Downstream it is rewritten in the endpoint identities (edge at $0$ and $1$ land on the corresponding vertices of the face), in the base-parameter identity along the geometric base edge $v_0 \to v_1$, and in the three cone-lift-angle evaluations on faces $\delta_0$, $\delta_1$, and $\delta_2$. Those cone identities are the concrete bookkeeping behind the 2-simplex telescoping that proves displacement kills boundaries.
In the Recognition foundation stack this sits inside the singular-homology half of the circle winding story: once boundaries are killed and the fundamental loop has winding one, winding is a left inverse to the fundamental class. The module notes that the converse generation half still needs a simplicial prism or subdivision operator not yet in Mathlib. The lemma itself is pure simplex geometry and does not invoke the forcing chain (T0–T8) or the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.