Foundation Dalembert Curvature Gate Gspher Violates Nonnegativity

The spherical candidate

The declaration Gspher_violates_nonnegativity is a formal theorem in the framework's machine-checked library, a collection of theorems verified by a computer. It concerns a specific function, Gspher(t) = cos(t) - 1, which is one of three candidate shapes for a cost metric, a mathematical rule that assigns a cost to comparing two states. The theorem states that this function is not non-negative: it takes negative values for some inputs. The proof is simple and exact: at t = π, the cosine of π is -1, so Gspher(π) = -2, which is less than zero.

This matters because the framework's recognition ledger, a discrete record of comparison events, requires that costs never be negative. A negative cost would mean a comparison could yield a benefit, which the framework treats as impossible. The theorem is a key step in a larger result called the curvature gate, which classifies possible cost metrics by their curvature: flat (G(t) = t²/2), hyperbolic (G(t) = cosh(t) - 1), or spherical (G(t) = 1 - cos(t)). The gate shows that, under the framework's axioms, the spherical option is ruled out because it violates non-negativity, leaving only the flat and hyperbolic candidates. The hyperbolic form is the one the framework identifies as the correct cost, derived from the forced composition law.

The declaration does not claim that the spherical function is the only one that fails non-negativity, nor does it prove that the hyperbolic form is the unique valid cost. It also does not assert anything about the physical world directly; it is a statement about a mathematical function within a formal system. The theorem's role is narrow: it eliminates one candidate geometry, supporting the framework's conclusion that the cost metric must be non-trivially curved.

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

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

/-- **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 function is the only candidate that fails non-negativity. The hyperbolic form is the unique valid cost metric. The theorem makes any direct claim about physical measurements.

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: