stdSimplex_contractibleSpace
plain-language theorem explainer
For every positive integer n, the standard topological n-simplex in real coordinates is contractible. Singular-homology and covering-space arguments that need path-homotopy on simplex domains cite this. The proof is a one-line appeal to Mathlib convexity of the simplex, with the Dirac mass at a vertex as the nonempty base point.
Claim. For every natural number $n \ge 1$, the standard simplex $\{ x \in \mathbb{R}^n : x_i \ge 0,\ \sum_i x_i = 1 \}$ is a contractible topological space.
background
This module supplies lifting prerequisites for the circle winding invariant on singular 1-chains of the topological circle. Singular simplices realize on the standard simplex stdSimplex ℝ (Fin n): nonnegative real n-tuples summing to one. Mathlib already records that this set is convex.
A nonempty convex subset of a real topological vector space is contractible by the straight-line homotopy to any chosen point of the set. Contractibility immediately yields simple connectedness, which is the exact hypothesis consumed by path-lifting monodromy invariance for covering maps (IsCoveringMap.liftPath_apply_one_eq_of_homotopicRel together with path-homotopy in a simply connected space).
The covering in play is the trigonometric cover of the circle; once monodromy is path-homotopy invariant, the winding number vanishes on boundaries. No project-local circle replacement or axioms are used.
proof idea
One-line wrapper. Apply the Mathlib lemma that a convex set is a contractible space, instantiated at convex_stdSimplex ℝ (Fin n). Nonemptiness is witnessed by the standard basis mass at coordinate 0, which lies in the simplex by single_mem_stdSimplex. The NeZero n instance guarantees Fin n is inhabited so that vertex exists.
why it matters
Infrastructure for the foundation layer that builds the winding/degree invariant via lifts through the trigonometric circle covering. The module doc states the purpose explicitly: register contractibility once so that the simplex is simply connected and monodromy invariance makes winding kill boundaries.
The immediate sibling records simple connectedness for discoverability; both feed the covering-space side of the circle story used elsewhere in the monolith. No downstream theorem currently lists this instance as a named dependency (instance resolution is silent), but without it the path-lifting route to a well-defined winding number on chains would not typecheck against Mathlib's covering API. It is pure topology: no Recognition-cost functional, no forcing-chain step T0–T8, and no physical constant is touched here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.