Foundation Circle Lifting Std Simplex Simply Connected Space

The simplex's simple loops

A standard simplex is the simplest solid shape in any dimension: a point in dimension zero, a line segment in dimension one, a triangle in dimension two, a tetrahedron in dimension three, and so on. Topologists use these shapes as building blocks to assemble more complicated spaces. The declaration stdSimplex_simplyConnectedSpace states a basic property of these building blocks: for any dimension n, the standard n-simplex is simply connected. A space is simply connected when it is connected and every loop in it can be continuously shrunk to a single point without leaving the space. A circle is not simply connected, because a loop that goes all the way around cannot shrink to a point without breaking; a disk is simply connected, because any loop drawn on it can be pulled tight to its center.

The reason a standard simplex has this property is that it is a convex set: if two points lie in it, the entire straight line segment between them also lies in it. In a convex set, any loop can be shrunk to a point by pulling each point of the loop along a straight line toward a fixed point of the set. This argument works in every dimension, so the result holds for all n. The machine-checked library of formal theorems records this as a theorem, derived by applying the convexity of the simplex to the standard topological definition of simple connectivity.

In Recognition Science, this theorem plays a supporting role in a larger construction. The framework builds a winding number, a count of how many times a path winds around a circle, by lifting paths through a covering map. The lifting process requires that the domain of each simplex, which is a standard simplex, be simply connected. The theorem supplies exactly that condition, so the winding number is well defined and kills boundaries as needed. The declaration does not itself define the winding number, nor does it prove that the winding number has any particular value; it only establishes the topological property that the construction relies on.

/-- Consequently the standard simplex is simply connected; this is the precise
hypothesis consumed by the path-lifting monodromy invariance used to show the
winding number kills boundaries.  (Stated explicitly for discoverability; it is
also available by instance resolution.) -/
theorem stdSimplex_simplyConnectedSpace (n : ℕ) [NeZero n] :
    SimplyConnectedSpace (stdSimplex ℝ (Fin n)) :=
  inferInstance

/-- The topological standard `n`-simplex (the realization domain of a singular
`(n-1)`-simplex) is contractible: it is a nonempty convex set. -/
instance stdSimplex_contractibleSpace (n : ℕ) [NeZero n] :
    ContractibleSpace (stdSimplex ℝ (Fin n)) :=
  (convex_stdSimplex ℝ (Fin n)).contractibleSpace
    ⟨_, single_mem_stdSimplex ℝ (0 : Fin n)⟩

/-- The covering map of `TopCat.sphere 1`, repackaged as an
`IsCoveringMap` term for direct use with the path-lifting API. -/
theorem isCoveringMap_trig : IsCoveringMap CircleParam.trigCirclePoint :=
  isCoveringMap_trigCirclePoint

What this page does not claim

The declaration does not define the winding number. The declaration does not prove that the winding number of the fundamental loop is one. The declaration does not apply to spaces that are not standard simplices.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Foundation/CircleLifting.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: