Foundation Circle Lifting Trig Circle Point Eq Iff

The circle's fiber

The declaration trigCirclePoint_eq_iff is a theorem about the standard trigonometric covering of the circle. In plain language, it states that two real numbers a and b map to the same point on the unit circle under the map t ↦ (cos t, sin t) if and only if they differ by an integer multiple of 2π. That is, the condition a = b + 2πm for some integer m is exactly equivalent to the two inputs wrapping around to the same location on the circle.

This equivalence is the algebraic heart of the circle's fiber structure. It describes the deck-transformation group of the universal cover ℝ → S¹: the group of translations by 2πℤ that leave the circle point unchanged. The theorem is proved in the machine-checked library of formal theorems, and it relies on two established ingredients. First, the topological standard simplex, the domain of a singular simplex, is contractible and therefore simply connected. Second, the path-lifting monodromy invariance from Mathlib, combined with simple connectivity, is what makes the winding number kill boundaries. The declaration itself is a theorem, not a definition, and it carries no axioms, sorry, or project-local S¹ replacements.

The practical consequence is that the winding number, the integer that counts how many times a loop winds around the circle, is well-defined. The value of the winding number on the fundamental loop is exactly 1, because the loop lifts to a path that changes the real parameter by 2π. This theorem is the precise algebraic condition that makes that integer invariant under homotopy. It does not, however, claim anything about the winding number's value on arbitrary loops, nor does it establish the existence of the covering map itself. It only provides the fiber structure that the winding number requires.

/-- **Fiber of the trigonometric covering.**  `trigCirclePoint a = trigCirclePoint b`
exactly when `a` and `b` differ by an integer number of full turns `2π`.  This is
the deck-transformation group `2π ℤ` of the universal cover `ℝ → S¹`. -/
theorem trigCirclePoint_eq_iff (a b : ℝ) :
    trigCirclePoint a = trigCirclePoint b ↔ ∃ m : ℤ, a = b + (m : ℝ) * (2 * Real.pi) := by
  rw [trigCirclePoint_eq_iff_exp, Circle.exp_eq_exp]

/-- **Fiber of the trigonometric covering.**  `trigCirclePoint a = trigCirclePoint b`
exactly when `a` and `b` differ by an integer number of full turns `2π`.  This is
the deck-transformation group `2π ℤ` of the universal cover `ℝ → S¹`. -/
theorem trigCirclePoint_eq_iff (a b : ℝ) :
    trigCirclePoint a = trigCirclePoint b ↔ ∃ m : ℤ, a = b + (m : ℝ) * (2 * Real.pi) := by
  rw [trigCirclePoint_eq_iff_exp, Circle.exp_eq_exp]

/-- 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 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 theorem does not establish the existence or uniqueness of the covering map itself. It does not compute the winding number for any specific loop beyond the fundamental one. It does not address the winding number's behavior under arbitrary continuous deformations.

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: