Encyclopedia Foundation Foundation Dalembert Curvature Gate Gspher Satisfies Spherical

ARTICLE 4 claims 4 theorems

Foundation Dalembert Curvature Gate Gspher Satisfies Spherical

One of three possible geometries for a recognition cost metric is a sphere, and the framework proves it fails a required non-negativity test.

Verify this page

The spherical candidate

The declaration Gspher_satisfies_spherical belongs to a small classification inside the Recognition Science framework. The framework studies a ledger, a discrete record of recognition events, and assigns a cost, a number measuring how expensive a comparison is. To analyze that cost, the framework lifts it into logarithmic coordinates, producing a function G(t). The second derivative of G defines a one-dimensional metric, and the curvature of that metric can be flat, hyperbolic, or spherical. The declaration proves that the specific function Gspher(t) = cos(t) - 1 satisfies the spherical curvature condition, meaning its second derivative equals -(G(t) + 1).

That proof is a theorem in the framework's machine-checked library of formal theorems. It is a conditional result: it shows that if a cost metric has constant spherical curvature, then it must take the form cos(t) - 1. The theorem does not say that spherical geometry is the right choice for recognition. In fact, the same library proves that Gspher is never positive, and at t = pi it is exactly -2. The framework requires the cost to be non-negative, so the spherical candidate fails that test. A separate theorem, curvature_gate_main, combines smoothness, calibration, and non-negativity to rule out spherical curvature entirely, leaving only flat or hyperbolic as possibilities.

In plain language, the declaration establishes a precise mathematical fact about a candidate curve, not a physical conclusion. It proves that the spherical curve satisfies its defining differential equation. It does not prove that recognition geometry is spherical, nor that the spherical curve is useful. The framework's own summary states that Gspher satisfies the spherical ODE but fails calibration, because its second derivative at zero is -1 rather than the required +1. The declaration is a building block in a larger argument, not the argument itself.

THEOREM Gspher_satisfies_spherical · IndisputableMonolith/Foundation/DAlembert/CurvatureGate.lean
Gspher_satisfies_spherical · IndisputableMonolith/Foundation/DAlembert/CurvatureGate.lean:103 
/-- Gspher satisfies the spherical ODE: G''(t) = -(G(t) + 1) = -cos(t). -/
theorem Gspher_satisfies_spherical : SatisfiesSphericalODE Gspher := by
  intro t
  -- G(t) = cos(t) - 1, G'(t) = -sin(t), G''(t) = -cos(t)
  have h1 : deriv Gspher = fun t => -Real.sin t := by
    ext s
    unfold Gspher
    rw [deriv_sub_const, Real.deriv_cos]
  have h2 : deriv (deriv Gspher) t = -Real.cos t := by
    rw [h1]
    have hd : HasDerivAt (fun t => -Real.sin t) (-Real.cos t) t := by
      have := Real.hasDerivAt_sin t
      exact this.neg
    exact hd.deriv
  rw [h2]
  unfold Gspher
  ring
THEOREM Gspher_nonpositive · Gspher_negative_at_pi · IndisputableMonolith/Foundation/DAlembert/CurvatureGate.lean
Gspher_nonpositive · IndisputableMonolith/Foundation/DAlembert/CurvatureGate.lean:154 
/-- The spherical solution becomes negative (cos(t) - 1 ≤ 0, and < 0 for t ≠ 2πk). -/
theorem Gspher_nonpositive : ∀ t : ℝ, Gspher t ≤ 0 := by
  intro t
  simp only [Gspher]
  have : Real.cos t ≤ 1 := Real.cos_le_one t
  linarith
Gspher_negative_at_pi · IndisputableMonolith/Foundation/DAlembert/CurvatureGate.lean:161 
/-- 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
THEOREM curvature_gate_main · IndisputableMonolith/Foundation/DAlembert/CurvatureGate.lean
curvature_gate_main · IndisputableMonolith/Foundation/DAlembert/CurvatureGate.lean:187 
/-- **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
THEOREM curvature_gate_summary · IndisputableMonolith/Foundation/DAlembert/CurvatureGate.lean
curvature_gate_summary · IndisputableMonolith/Foundation/DAlembert/CurvatureGate.lean:242 
/-- **Summary**: The curvature gate combined with structural axioms forces:
    - Spherical ruled out by calibration (G''(0) = 1 ≠ -1)
    - Flat corresponds to the counterexample (additive P, no interaction)
    - Hyperbolic corresponds to the RCL

    The interaction gate then selects hyperbolic over flat.
-/
theorem curvature_gate_summary :
    -- Gquad is flat and satisfies structural axioms
    SatisfiesFlatODE Gquad ∧ Gquad 0 = 0 ∧ deriv (deriv Gquad) 0 = 1 ∧
    -- Gcosh is hyperbolic and satisfies structural axioms
    SatisfiesHyperbolicODE Gcosh ∧ Gcosh 0 = 0 ∧ deriv (deriv Gcosh) 0 = 1 ∧
    -- Gspher satisfies spherical ODE but FAILS calibration
    SatisfiesSphericalODE Gspher ∧ Gspher 0 = 0 ∧ deriv (deriv Gspher) 0 = -1 := by
  refine ⟨Gquad_satisfies_flat, ?_, ?_, Gcosh_satisfies_hyperbolic, ?_, ?_,
          Gspher_satisfies_spherical, ?_, ?_⟩
  · simp [Gquad]
  · have := Gquad_satisfies_flat 0; exact this
  · simp [Gcosh, Real.cosh_zero]
  · have := Gcosh_satisfies_hyperbolic 0
    simp [Gcosh, Real.cosh_zero] at this ⊢
    exact this
  · simp [Gspher, Real.cos_zero]
  · have := Gspher_satisfies_spherical 0
    simp [Gspher, Real.cos_zero] at this ⊢
    exact this

What this page does not claim

The declaration does not prove that recognition geometry is spherical. The declaration does not establish that the spherical curve is physically relevant or usable. The declaration does not by itself rule out spherical curvature; that requires the additional non-negativity and calibration assumptions.

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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND