Foundation Singular Sphere Geometry Abs Eq One Of Sq Eq One

The sphere and its poles

A circle in the plane has a natural pair of opposite points, its poles. In the Recognition Science framework, the declaration abs_eq_one_of_sq_eq_one proves a precise fact about these poles: on a circle of radius one, a point whose first coordinate squares to one must be exactly one of the two poles. The poles are the points where the circle meets the vertical axis, and the result states that no other point on the circle has a coordinate whose square equals one. This is a statement about the geometry of the circle, not about any physical system.

The proof lives in a machine-checked library of formal theorems, a collection of mathematical results verified by a computer. The library defines the circle as the set of points at distance one from the origin in a two-dimensional Euclidean space. It then defines the north pole as the point with coordinates (0,1) and the south pole as (0,-1). The result abs_eq_one_of_sq_eq_one says that if a point on the circle has a first coordinate whose square is one, then that point is either the north pole or the south pole. The library also proves related facts, such as that the two poles are distinct and that the circle's homology groups vanish except in the expected dimension.

The result is a formal consequence of the definitions. The library proves that the only points on the circle with a first coordinate whose square is one are the two poles. This is not a physical claim; it is a mathematical fact about the circle. It does not say anything about the cost function, the golden ratio, or the forcing chain. It is a standalone result about the geometry of the circle, proved in the framework's library as a step toward understanding the sphere model.

In Recognition Science, the sphere model is a tool for studying recognition events, which are discrete records of comparisons. The framework uses the circle and its poles to build a model of how a recognition event can be represented geometrically. The result abs_eq_one_of_sq_eq_one is a small but necessary piece of that model: it pins down which points on the circle can serve as the poles. Without it, the model would be ambiguous about which points are the poles. The result does not, by itself, prove anything about the physical world; it is a lemma in a larger formal development.

/-- The right (east) arc of the doubly punctured circle. -/
noncomputable def arcA : Set ↥Wc := {w | 0 < coordW w}

lemma northP_ne_southP (n : ℕ) : northP n ≠ southP n := by
  intro h
  have h1 : (northP n : Esp n) = -(northP n : Esp n) := by
    calc (northP n : Esp n) = (southP n : Esp n) := congrArg _ h
      _ = -(northP n : Esp n) := coe_neg_sphere (northP n)
  have h2 : (northP n : Esp n) = 0 := by
    have hsum : (northP n : Esp n) + (northP n : Esp n) = 0 := by
      nth_rewrite 2 [h1]
      exact add_neg_cancel _
    have h2' : (2 : ℝ) • (northP n : Esp n) = 0 := by
      rw [two_smul]
      exact hsum
    rcases smul_eq_zero.mp h2' with h | h
    · exact absurd h (by norm_num)
    · exact h
  have h3 : ‖(northP n : Esp n)‖ = 1 := norm_eq_of_mem_sphere (northP n)
  rw [h2, norm_zero] at h3
  exact zero_ne_one h3

/-- The south pole, as a point of the sphere. -/
noncomputable def southP (n : ℕ) : sphere (0 : Esp n) 1 := -northP n

lemma northP_ne_southP (n : ℕ) : northP n ≠ southP n := by
  intro h
  have h1 : (northP n : Esp n) = -(northP n : Esp n) := by
    calc (northP n : Esp n) = (southP n : Esp n) := congrArg _ h
      _ = -(northP n : Esp n) := coe_neg_sphere (northP n)
  have h2 : (northP n : Esp n) = 0 := by
    have hsum : (northP n : Esp n) + (northP n : Esp n) = 0 := by
      nth_rewrite 2 [h1]
      exact add_neg_cancel _
    have h2' : (2 : ℝ) • (northP n : Esp n) = 0 := by
      rw [two_smul]
      exact hsum
    rcases smul_eq_zero.mp h2' with h | h
    · exact absurd h (by norm_num)
    · exact h
  have h3 : ‖(northP n : Esp n)‖ = 1 := norm_eq_of_mem_sphere (northP n)
  rw [h2, norm_zero] at h3
  exact zero_ne_one h3

What this page does not claim

The result does not claim anything about the cost function J(x) or the golden ratio phi. The result does not claim that the circle itself is a physical object or that recognition events occur on a circle. The result does not claim that the first coordinate is the only coordinate that can square to one; the second coordinate can also square to one at the poles.

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