Foundation Circle Param Continuous Trig Circle Vector

The continuous circle map

The unit circle in the plane is the set of points at distance exactly 1 from the origin. Its standard parametrization sends a real number t to the point (cos t, sin t). This is the map that draws the circle as t runs from 0 to 2π, starting at (1, 0) and returning there after one full turn. The map is continuous: if t changes by a tiny amount, the point (cos t, sin t) changes by a tiny amount too. This is a basic fact of calculus, since cosine and sine are continuous functions.

The framework's machine-checked library of formal theorems records this fact for its own exact model of the circle. It defines the vector (cos t, sin t) in the two-dimensional Euclidean plane, proves that this vector lies on the unit circle for every t, and then proves the continuity statement as a formal theorem. The declaration continuous_trigCircleVector is precisely that theorem: the map t ↦ (cos t, sin t) is continuous. The library also proves the companion facts that the parametrization starts at the chosen basepoint (1, 0) and returns to it after t = 2π.

In Recognition Science, this is groundwork for a larger project. The framework treats the circle as a geometric object whose structure should be derived from its own principles, and this theorem is a first step in that derivation. It establishes that the standard trigonometric parametrization is a continuous map into the exact circle object the framework uses. This matters because later steps in the framework's program, such as defining loops or analyzing the circle's topology, will rely on having a continuous parametrization available.

The theorem does not claim that this parametrization is the only continuous one, nor that it is the fundamental generator of the circle's topology. The library explicitly notes that the constant simplex, not this map, is the first API anchor for later work. The theorem also does not establish any property about the circle's fundamental group, winding numbers, or any deeper topological invariant. It is a single, clean fact: the standard circle parametrization is continuous.

/-- The ambient trigonometric circle parametrization is continuous. -/
theorem continuous_trigCircleVector :
    Continuous trigCircleVector := by
  change Continuous fun t : ℝ =>
    (WithLp.toLp 2 (fun i : Fin 2 => ![Real.cos t, Real.sin t] i) : SphereOneAmbient)
  exact (PiLp.continuous_toLp (p := 2) (β := fun _ : Fin 2 => ℝ)).comp
    (continuous_pi fun i => by
      fin_cases i
      · simpa using Real.continuous_cos
      · simpa using Real.continuous_sin)

/-- The vector `(cos t, sin t)` lies on the exact metric unit circle used by
`TopCat.sphere 1`. -/
theorem trigCircleVector_mem_sphere (t : ℝ) :
    trigCircleVector t ∈ Metric.sphere (0 : SphereOneAmbient) 1 := by
  change dist (trigCircleVector t) 0 = 1
  rw [dist_zero_right]
  have hsq : ‖trigCircleVector t‖ ^ 2 = 1 := by
    rw [EuclideanSpace.norm_sq_eq]
    simp [trigCircleVector, Fin.sum_univ_two, Real.cos_sq_add_sin_sq]
  have hnonneg : 0 ≤ ‖trigCircleVector t‖ := norm_nonneg _
  nlinarith

/-- The trigonometric parametrization starts at the chosen basepoint. -/
theorem trigCirclePoint_zero :
    trigCirclePoint 0 = sphereOneBasepoint := by
  apply ULift.ext
  apply Subtype.ext
  ext i
  fin_cases i <;>
    simp [trigCirclePoint, trigCircleVector, sphereOneBasepoint, sphereOneBaseVector]

/-- The trigonometric parametrization returns to the basepoint after one full
turn. -/
theorem trigCirclePoint_two_pi :
    trigCirclePoint (2 * Real.pi) = sphereOneBasepoint := by
  apply ULift.ext
  apply Subtype.ext
  ext i
  fin_cases i <;>
    simp [trigCirclePoint, trigCircleVector, sphereOneBasepoint, sphereOneBaseVector]

What this page does not claim

This parametrization is the unique continuous map onto the circle. This theorem establishes any property of the circle's fundamental group or winding number. The constant simplex, not the trigonometric map, is the fundamental generator for the framework's circle topology.

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