Verification Dimension Kepler

The Kepler selector

In classical mechanics, a planet orbiting a central mass does not generally return to its starting point after one loop. The apsidal angle is the angle, measured at the central body, between one closest approach (periapsis) and the next. For an inverse-square force law, that angle is exactly 2π, meaning the orbit closes into an ellipse and repeats itself precisely.

The Kepler specialization in the Recognition Science library isolates the algebraic core of this fact. It defines a closed-form expression for the apsidal angle as a function of the spatial dimension D: Δθ(D) = 2π / √(4 − D). The library then proves, as a machine-checked theorem, that this expression equals 2π if and only if D = 3. In plain language: only in three spatial dimensions does the inverse-square orbit close.

This result is a verification-layer endpoint. The module deliberately starts from the reduced-form expression, after the classical mechanics derivation, so the verification layer can reference it cleanly. It does not re-derive the physics; it isolates the algebraic statement that the apsidal angle closes exactly at D = 3, and proves that statement in the framework's machine-checked library of formal theorems.

In Recognition Science, this algebraic selector connects the framework's forcing chain to a classical, independently checkable fact. The framework models spatial structure through its own recognition ledger, a discrete record of events, and the Kepler selector provides a cross-check: the same dimension that the framework's internal chain forces is the one classical orbital mechanics singles out. The module thus acts as a bridge between the framework's derived structure and a familiar physical result.

What the module changes is the status of the dimensional claim. The apsidal-angle closure at D = 3 is not merely a known fact from textbooks; it is a proved theorem in the library, with the algebraic core isolated for direct reference. Any downstream verification layer can now cite this selector without re-deriving the mechanics.

/-- Algebraic Kepler selector: `Δθ = 2π` holds exactly at `D = 3`. -/
theorem kepler_selection_principle (D : ℕ) :
    apsidalAngle D = 2 * Real.pi ↔ D = 3 := by
  constructor
  · intro h
    have hpi : (2 * Real.pi) ≠ 0 := by
      exact mul_ne_zero (by norm_num) Real.pi_ne_zero
    set x : ℝ := Real.sqrt (4 - (D : ℝ))
    have hx : x ≠ 0 := by
      intro hx0
      have : apsidalAngle D = 0 := by
        simp [apsidalAngle, x, hx0]
      have h0 : 0 = 2 * Real.pi := by
        simpa [this] using h
      exact hpi h0.symm
    have h' : (2 * Real.pi) * x⁻¹ = 2 * Real.pi := by
      simpa [apsidalAngle, x, div_eq_mul_inv] using h
    have hmul : (2 * Real.pi) * (x⁻¹ * x) = (2 * Real.pi) * x := by
      simpa [mul_assoc] using congrArg (fun t => t * x) h'
    have hmul' : (2 * Real.pi) = (2 * Real.pi) * x := by
      simpa [mul_assoc, inv_mul_cancel₀ hx, mul_one] using hmul
    have hx1 : x = 1 := by
      have hcancel : (2 * Real.pi) * x = (2 * Real.pi) * 1 := by
        calc
          (2 * Real.pi) * x = (2 * Real.pi) := by simpa [mul_assoc] using hmul'.symm
          _ = (2 * Real.pi) * 1 := by simp
      exact mul_left_cancel₀ hpi hcancel
    have hnonneg : 0 ≤ 4 - (D : ℝ) := by
      by_contra hneg
      have hle : 4 - (D : ℝ) ≤ 0 := le_of_not_ge hneg
      have : Real.sqrt (4 - (D : ℝ)) = 0 := Real.sqrt_eq_zero_of_nonpos hle
      have : (1 : ℝ) = 0 := by simpa [x, hx1] using this
      exact one_ne_zero this
    have hsq : x ^ 2 = 4 - (D : ℝ) := by
      simpa [x, pow_two] using (Real.sq_sqrt hnonneg)
    have hreal : (D : ℝ) = 3 := by
      have : (1 : ℝ) ^ 2 = 4 - (D : ℝ) := by simpa [hx1] using hsq
      nlinarith
    exact (Nat.cast_injective (R := ℝ) (by simpa using hreal))
  · intro hD
    subst hD
    have : (4 - (3 : ℝ)) = (1 : ℝ) := by norm_num
    simp [apsidalAngle, this]

/-- Closed-form apsidal angle used in the Kepler specialization. -/
noncomputable def apsidalAngle (D : ℕ) : ℝ :=
  (2 * Real.pi) / Real.sqrt (4 - (D : ℝ))

What this page does not claim

The module does not derive the apsidal-angle formula from classical mechanics; it starts from the reduced-form expression. The theorem does not prove that physical space is three-dimensional; it proves an algebraic equivalence for the apsidal angle. The module does not establish the inverse-square force law itself.

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/Verification/DimensionKepler.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: