v0
plain-language theorem explainer
The unique vertex of the standard 0-simplex Δ⁰, realized as the barycentric coordinate vector with sole entry 1. Anyone working with singular 0-chains, constant simplices, or face maps out of a point cites this basepoint. The definition is the Dirac mass at index 0, with Mathlib's membership lemma for the standard simplex.
Claim. Let $v_0$ denote the unique point of the standard $0$-simplex $\Delta^0 \subset \mathbb{R}^{\{0\}}$, given in barycentric coordinates by the vector with sole entry $1$ (equivalently $\mathrm{Pi.single}\,0\,1$).
background
In singular homology one works with continuous maps $\sigma:\Delta^n\to X$ from the standard $n$-simplex. The $0$-simplex $\Delta^0$ is a single point: the set of maps $\mathrm{Fin},1\to\mathbb{R}_{\ge 0}$ summing to $1$. That set is a singleton, so there is a canonical basepoint $v_0$.
The ambient module SingularSphere builds singular chains and Mayer–Vietoris data for spheres from prism and pair constructions. The 0-simplex vertex is the seed for extracting the underlying point of a singular 0-simplex and for evaluating face maps of prisms at the base of a 1-simplex.
Uniqueness is recorded immediately after the definition by a Subsingleton instance on $\mathrm{stdSimplex},\mathbb{R},(\mathrm{Fin},(0+1))$, obtained by reducing the sum-to-one constraint via Fin.sum_univ_succ and add_zero.
proof idea
Definitional construction, not a tactic proof. The term is the subtype pair whose first component is Pi.single 0 1 (value 1 at the unique index, 0 elsewhere) and whose second component is Mathlib's single_mem_stdSimplex ℝ 0, which checks nonnegativity and sum-one. The following Subsingleton instance separately proves any two points of $\Delta^0$ agree by forcing both coordinates at index 0 to equal 1.
why it matters
This is the canonical basepoint for all 0-dimensional singular data in the module. Downstream, pointOf evaluates a singular 0-simplex at $v_0$ to recover its underlying point in $X$; idx0_ext uses Subsingleton.elim z v0 to show 0-simplices are determined by that point. Face lemmas coord_face_v0 and simplexToI_face_v0 evaluate prism faces of $v_0$ when building interval and sphere maps. Outside the module it appears in Freudenthal-axis stencil coefficient certificates as a named local vertex coordinate. It sits in the singular-homology scaffolding that supports Recognition foundation geometry (contractible simplices, Mayer–Vietoris), not in the T0–T8 forcing chain itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.