Foundation Circle Lifting Trig Circle Point Eq Iff Exp

The covering map's fiber

The circle is the set of points at a fixed distance from a center. A standard way to label its points is by an angle: the point at angle a is the position reached by starting at the rightmost point and traveling counterclockwise by a radians. Because a full turn is 2π radians, the angle a and the angle a + 2π describe the same point. The declaration trigCirclePoint_eq_iff_exp states this identification precisely: two real numbers a and b name the same point of the circle if and only if the complex exponential function Circle.exp sends them to the same value.

The complex exponential, written exp(a) = cos a + i sin a, wraps the real line around the unit circle in the complex plane. The theorem says that this wrapping is injective modulo the period: exp(a) = exp(b) exactly when a − b is an integer multiple of 2π. This is the algebraic heart of the winding number, the integer count of how many times a loop goes around a point. The declaration is proved in the framework's machine-checked library of formal theorems, with no axioms beyond the standard logical ones.

In Recognition Science, this fact appears as a recognition event, a discrete record of when two angles are perceived as the same point. The theorem does not claim that every real number is a distinct point on the circle; it claims the opposite, that infinitely many real numbers collapse to the same circle point. It also does not claim that the exponential map is onto, that every point of the circle is hit, though that is true. Nor does it claim anything about the winding number's value for a specific loop; it only provides the fiber structure on which that value is built.

/-- Two real parameters hit the same point of `TopCat.sphere 1` under the
trigonometric covering iff they have the same `Circle.exp`. -/
theorem trigCirclePoint_eq_iff_exp (a b : ℝ) :
    trigCirclePoint a = trigCirclePoint b ↔ Circle.exp a = Circle.exp b := by
  rw [← ulift_carrierCovering_eq_trig]
  simp only [Function.comp_apply, carrierCovering]
  refine ⟨fun h => ?_, fun h => ?_⟩
  · exact circleHomeoCarrier.injective (Homeomorph.ulift.symm.injective h)
  · rw [h]

/-- **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]

What this page does not claim

The theorem does not claim that the exponential map is surjective onto the circle. It does not assign a winding number to any particular loop. It does not introduce any RS-specific axiom or replacement for the standard circle.

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: