coord_face_v0
plain-language theorem explainer
The first barycentric coordinate of the image of the unique 0-simplex vertex under the k-th face inclusion into the standard 1-simplex equals 1 when k skips vertex 0 and equals 0 when k skips vertex 1. Algebraic topologists computing singular chains on spheres cite it when reducing face maps of constant simplices to endpoint values. The proof reindexes a filtered coordinate sum along succAbove and case-splits on k.
Claim. For each $k \in \{0,1\}$, if $v_0$ is the unique point of the standard $0$-simplex and $\partial_k$ is the $k$-th face inclusion $\Delta^0 \to \Delta^1$ induced by skipping vertex $k$, then the barycentric coordinate of $\partial_k(v_0)$ at index $1$ equals $1$ if $k=0$ and equals $0$ otherwise.
background
The module builds singular-sphere infrastructure used by Recognition Science foundation arguments: standard simplices, face inclusions, and maps from $0$-simplices into the unit interval. The unique point $v_0$ of $\Delta^0 = \mathrm{stdSimplex},\mathbb{R},(\mathrm{Fin},1)$ is the Dirac mass $\mathrm{Pi.single},0,1$.
Face inclusions come from SingularPrism: the $j$-th topological face $\Delta^n \to \Delta^{n+1}$ is continuous realization of $\mathrm{Fin.succAbove},j$, the vertex map that skips index $j$. Coordinate extraction on the image therefore reduces to how mass is pushed forward under that skip map.
The key upstream identity is sum_filter_map_apply: a filtered sum of coordinates of $\mathrm{stdSimplex.map},f,x$ reindexes to a filtered sum of coordinates of $x$ along $f$. Together with the explicit formula for the natural-number value of $\mathrm{succAbove}$, this turns face-coordinate questions into finite case analysis on $\mathrm{Fin},2$.
proof idea
Apply sum_filter_map_apply with $f = k.\mathrm{succAbove}$ and predicate "equals index $1$" to rewrite the target coordinate as a filtered sum of $v_0$ over preimages of $1$. The left filtered sum collapses to the single term at index $1$ by Finset.filter_eq'.
Compute $((k.\mathrm{succAbove},0):\mathbb{N})$ via coe_succAbove and fin_cases k: it is $1$ when $k=0$ and $0$ when $k=1$. For the right-hand filtered sum, case on $k=0$. If $k=0$, the filter is the singleton ${0}$ and $v_0$ evaluates to $1$ by Pi.single_eq_same. If $k\neq 0$, the filter is empty: any purported preimage would force $1=0$ after substituting the coe_succAbove value, contradicting one_ne_zero. Chain the three equalities.
why it matters
This is a coordinate lemma feeding simplexToI_face_v0, which identifies the unit-interval image of each face of $v_0$ with the corresponding endpoint $0$ or $1$. That identification is the base case for relating singular $1$-simplices on the circle (or sphere) to winding data: constant $0$-simplices pushed along faces land on the two endpoints of $I$.
In the broader SingularSphere development (with Mayer–Vietoris, prisms, and pair exact sequences imported), endpoint control on faces is needed before one can compute reduced homology generators and connect geometric spheres to the Recognition forcing chain's dimensional and periodic structure (eight-tick octave, $D=3$). The lemma itself is pure simplicial linear algebra; its value is that it discharges the first nontrivial face-coordinate obligation without sorry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.