Foundation Circle Param Trig Circle Point Two Pi

The once-around circle

The unit circle in the plane is the set of points at distance exactly 1 from the origin. Its standard trigonometric parametrization sends a real number t to the point (cos t, sin t). This is the familiar wrapping of the real line around the circle: as t increases from 0, the point moves counterclockwise, and after t reaches 2π it has completed one full circuit. The statement trigCirclePoint_two_pi in the framework's machine-checked library of formal theorems records precisely this fact: the point obtained at t = 2π is the same as the point at t = 0, namely the basepoint (1, 0).

The declaration does not merely assert the identity informally. It proves it for the exact topological sphere object used in the library, the metric unit circle embedded in the Euclidean plane. The proof checks, coordinate by coordinate, that cos(2π) = 1 and sin(2π) = 0, using the defining properties of the real trigonometric functions. This is a theorem in the formal sense: it follows from the definitions by a chain of verified steps, with no additional assumptions about the circle or the parametrization.

In Recognition Science, this result is a foundation stone. The framework models physical structure from a discrete ledger of recognition events, and it seeks to derive the circle and its topology from first principles. The parametrization (cos t, sin t) is the bridge between the real line and the circle, and the fact that one full turn closes the loop is what makes the circle a circle rather than an open spiral. The theorem establishes that the standard parametrization is a genuine once-around map into the exact sphere object, not merely a formal expression.

The declaration does not claim that the trigonometric parametrization is the only way to go around the circle, nor that it is the fundamental generator of the circle's topology. It does not assert that the circle itself is derived from the framework's ledger; the circle is taken as a standard mathematical object, and the theorem concerns the parametrization of that object. It also does not claim that the value 2π is special beyond the periodicity of sine and cosine; the same identity would hold at any integer multiple of 2π.

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

The trigonometric parametrization is the only once-around map of the circle. The circle itself is derived from the framework's ledger; it is a standard mathematical object. The value 2π is special beyond the periodicity of sine and cosine.

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: