Foundation Circle Winding Trig Circle Point Add Int Mul Period

The period of the circle map

The circle is the set of points at a fixed distance from a center, and its most important feature is that you can travel around it and return to where you started. The map trigCirclePoint sends a real number, thought of as an angle or a distance along a line, to a point on the circle. The theorem trigCirclePoint_add_intMul_period states a precise periodicity: adding any integer multiple of 2π to the input leaves the output unchanged. In symbols, for any real number x and any integer k, trigCirclePoint(x + k·2π) = trigCirclePoint(x). This is the formal, machine-checked statement that the circle's fundamental period is exactly 2π, and it is the reason that angles are measured modulo 2π.

This periodicity is not just a convenient convention; it is the foundation for the concept of winding number. The framework's library defines the displacement of a path on the circle by lifting the path to the real line and measuring how far the lift travels. The theorem pathDisplacement_loop_intMul uses the periodicity to show that for any closed loop, the displacement is an integer multiple of 2π. Dividing by 2π gives the winding number, an integer that counts how many times the loop goes around the circle. The theorem pathWinding_fundamentalLoop then shows that the simplest loop, which goes around once, has winding number 1. This chain of results makes the winding number a rigorous, computable invariant of a loop.

The theorem itself is a simple consequence of the definition of trigCirclePoint, which is built from the complex exponential function. The proof in the library is a direct application of the definition, using the fact that e^(i(x + 2πk)) = e^(ix). The statement is an axiom-clean theorem in the machine-checked library, meaning it is proved from the standard axioms of the underlying type theory with no additional assumptions. It is a basic but essential building block: without this precise period, the entire theory of winding numbers and the recognition of loops would lack its fundamental measure.

What the theorem does not claim is that 2π is the only period, or that the map is injective on any interval of length less than 2π. It only states that integer multiples of 2π are periods. It also does not claim anything about the behavior of the map for non-integer multiples of 2π, nor does it address the winding of paths that are not closed. The theorem is a statement about the map itself, not about the paths on the circle. It is the first step in a larger theory, not the whole theory.

/-- Period invariance of the covering: shifting the angle by an integer number of
full turns `2π` does not change the point. -/
theorem trigCirclePoint_add_intMul_period (x : ℝ) (k : ℤ) :
    trigCirclePoint (x + (k : ℝ) * (2 * Real.pi)) = trigCirclePoint x := by
  rw [trigCirclePoint_eq_iff]
  exact ⟨k, rfl⟩

/-- A closed path has displacement equal to an integer number of full turns. -/
theorem pathDisplacement_loop_intMul (γ : C(I, SphereOne)) (hloop : γ 1 = γ 0) :
    ∃ k : ℤ, pathDisplacement γ = (k : ℝ) * (2 * Real.pi) := by
  have hfib : trigCirclePoint (pathLift γ 1) = trigCirclePoint (pathLift γ 0) := by
    have h1 : trigCirclePoint (pathLift γ 1) = γ 1 := congrFun (pathLift_lifts γ) 1
    have h0 : trigCirclePoint (pathLift γ 0) = γ 0 := congrFun (pathLift_lifts γ) 0
    rw [h1, h0, hloop]
  obtain ⟨k, hk⟩ := (trigCirclePoint_eq_iff (pathLift γ 1) (pathLift γ 0)).1 hfib
  refine ⟨k, ?_⟩
  rw [pathDisplacement_self, hk]
  ring

/-- **The winding number of the fundamental loop is `1`.**  The winding invariant
is therefore a left inverse to the fundamental loop class on the nose: it sends
the canonical generator to `1`. -/
theorem pathWinding_fundamentalLoop : pathWinding fundamentalLoop = 1 := by
  rw [pathWinding, pathDisplacement_fundamentalLoop]
  have hpi : (2 : ℝ) * Real.pi ≠ 0 := by positivity
  field_simp

What this page does not claim

The theorem does not claim that 2π is the only period, only that integer multiples of it are periods. The theorem does not claim anything about the behavior of the map for non-integer multiples of 2π. The theorem does not address the winding of paths that are not closed loops.

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/CircleWinding.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: