Foundation Dalembert Curvature Gate Gspher Negative At Pi

The spherical candidate

In the Recognition Science framework, the cost of a recognition event is encoded in a function G(t), and the geometry of that cost is read from its second derivative. Three candidate geometries are considered: flat, where the second derivative is constant; hyperbolic, where it equals G plus one; and spherical, where it equals minus G minus one. The spherical candidate is G(t) = cos(t) − 1, a periodic function that swings between zero and negative values.

The declaration Gspher_negative_at_pi is a formal theorem in the framework's machine-checked library. It states that at t = π, the spherical candidate G(π) = cos(π) − 1 = −2, which is less than zero. This single negative value is enough to violate the framework's non-negativity requirement, which demands that the cost function never dip below zero. The theorem Gspher_violates_nonnegativity uses this fact to formally rule out the spherical geometry as a valid cost metric.

This is one step in the curvature gate, which forces the cost metric to have constant nonzero curvature. The gate's main theorem, curvature_gate_main, takes smoothness, normalization, calibration, evenness, non-negativity, and constant curvature as premises, and concludes that only the flat or hyperbolic candidates survive. The spherical candidate is eliminated not by a deep argument but by a direct calculation: cos(π) = −1, so the function goes negative.

In Recognition Science, this matters because the surviving hyperbolic geometry, G(t) = cosh(t) − 1, is the one that leads to the framework's derived constants and the golden ratio. The spherical candidate, with its periodic comparisons, cannot serve as a cost ledger because it would sometimes assign negative cost. The theorem is a small but necessary gate: it closes off one branch of the geometric path.

What the declaration does not claim is broader. It does not prove that the spherical geometry is impossible in general mathematics; it only shows it fails the framework's non-negativity axiom. It does not establish that the hyperbolic geometry is the only valid one, since the flat candidate also survives the gate. And it does not itself derive any physical constant; it is a lemma in a larger chain, not an end result.

/-- The spherical solution is negative at t = π. -/
theorem Gspher_negative_at_pi : Gspher Real.pi < 0 := by
  simp only [Gspher, Real.cos_pi]
  norm_num

/-- The spherical solution violates non-negativity. -/
theorem Gspher_violates_nonnegativity : ¬ IsNonNegativeG Gspher := by
  intro h
  have := h Real.pi
  have hneg := Gspher_negative_at_pi
  linarith

/-- **Curvature Gate Theorem (Statement)**:
    Under structural axioms + constant curvature:
    1. Flat (κ = 0) ⟹ G = t²/2 (counterexample, no interaction)
    2. Hyperbolic (κ = -1) ⟹ G = cosh(t) - 1 (RCL)
    3. Spherical (κ = +1) ⟹ violates non-negativity

    Therefore: Non-negativity + Interaction ⟹ Hyperbolic (RCL).
-/
theorem curvature_gate_main (G : ℝ → ℝ)
    (hSmooth : ContDiff ℝ 2 G)
    (hNorm : G 0 = 0)
    (hCalib : deriv (deriv G) 0 = 1)
    (hEven : ∀ t, G (-t) = G t)
    (hNonNeg : IsNonNegativeG G)
    (hConstCurv : SatisfiesFlatODE G ∨ SatisfiesHyperbolicODE G ∨ SatisfiesSphericalODE G) :
    -- Spherical is ruled out by non-negativity
    -- Flat corresponds to no interaction
    -- Hyperbolic is the RCL
    SatisfiesFlatODE G ∨ SatisfiesHyperbolicODE G := by
  rcases hConstCurv with hFlat | hHyp | hSpher
  · left; exact hFlat
  · right; exact hHyp
  · -- Spherical: show G = Gspher (up to scaling), which violates non-negativity
    -- The ODE G'' = -(G + 1) with G(0) = 0 has unique solution G = cos - 1
    -- But this is ≤ 0 everywhere and < 0 at π
    exfalso
    -- From the ODE and initial conditions, G must behave like cos - 1
    -- At t = 0: G(0) = 0, G''(0) = -(G(0) + 1) = -1
    -- But our calibration requires G''(0) = 1, contradiction!
    have hcalib_spher := hSpher 0
    rw [hNorm] at hcalib_spher
    simp at hcalib_spher
    -- hcalib_spher : deriv (deriv G) 0 = -1
    -- hCalib : deriv (deriv G) 0 = 1
    rw [hCalib] at hcalib_spher
    norm_num at hcalib_spher

What this page does not claim

The spherical geometry is mathematically impossible in general. The hyperbolic geometry is the only valid cost metric. This theorem alone derives any physical constant. The framework's non-negativity axiom is itself derived rather than assumed.

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/DAlembert/CurvatureGate.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: