Foundation Circle Lifting Is Covering Map Trig

The circle covering

The circle is one of the oldest objects in mathematics, and the map from the real line onto it is one of the oldest pictures: roll the real line around a unit circle, and every point on the circle gets hit by infinitely many real numbers, one for each full turn. The map is usually written as t ↦ (cos t, sin t), or in complex form as t ↦ e^(it). The declaration isCoveringMap_trig establishes, in the framework's machine-checked library of formal theorems, that this familiar map is a covering map: a continuous surjection with the special property that every point on the circle has a small neighborhood whose preimage is a disjoint union of open intervals, each mapped homeomorphically onto that neighborhood. In plain terms, the real line is the universal cover of the circle, and the declaration records that fact as a formal theorem ready for use.

Why does this matter? A covering map is the tool that lets you lift paths: if you have a path on the circle, you can follow it continuously upward into the real line, and the lift is unique once you choose a starting point. This lifting property is what makes the winding number well defined. The winding number counts how many times a loop goes around the circle, and to compute it you lift the loop to the real line and measure how far the lifted endpoint has traveled. The declaration isCoveringMap_trig is the prerequisite that makes that lifting possible in the framework's formal development. The machine-checked library uses it to build the winding invariant on singular 1-chains of the circle, and the value of the winding number on the fundamental loop comes out as 1.

The declaration also pins down the fiber structure of the covering. Two real parameters a and b hit the same point on the circle exactly when they differ by an integer multiple of 2π. That is the deck-transformation group 2πℤ, and it is the algebraic heart of the winding number: the lift of a closed loop can end only at a point shifted by an integer number of full turns, and that integer is the winding number. The formal theorem states this equivalence precisely: trigCirclePoint a = trigCirclePoint b if and only if there exists an integer m such that a = b + m * (2 * Real.pi).

In Recognition Science, this declaration is a small but load-bearing step in a larger chain. The framework derives physical structure from a forced cost function, and part of that derivation involves topological invariants on the circle. The covering map is the bridge between the local trigonometric description and the global winding invariant, and the declaration makes that bridge formally explicit. It is not a claim about physics; it is a claim about the topology of the circle, and the framework uses it as a tool.

What the declaration does not claim is just as important. It does not claim that the real line is the only cover of the circle, nor does it claim that the winding number is defined for all maps into the circle without further hypotheses. It does not claim that the trigonometric covering map is the same as any other covering map, only that this particular map, defined by the framework's CircleParam.trigCirclePoint, satisfies the IsCoveringMap property. It also does not claim that the framework's derivation of physical constants depends on this declaration; the declaration is a topological foundation, not a physical law.

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

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

What this page does not claim

This declaration does not claim that the real line is the only cover of the circle. It does not claim that the winding number is defined for all maps into the circle without further hypotheses. It does not claim that the framework's physical derivations depend on this topological declaration.

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: