Foundation Dalembert Curvature Gate

The curvature gate

The d'Alembert curvature gate is a formal result in Recognition Science, a framework that models how a system keeps a discrete record of events, called a ledger. The result concerns the cost of recognition, the price a system pays to tell two states apart. The framework's library, a machine-checked collection of formal theorems, proves that this cost metric cannot be flat. It must have constant nonzero curvature, a property that makes comparisons depend on each other rather than remaining independent.

The classical starting point is a function G(t) that represents the cost in logarithmic coordinates. The framework defines a one-dimensional metric from it, ds² = G''(t) dt², where G'' is the second derivative. The curvature of this metric takes one of three constant values. Flat space, with curvature zero, corresponds to G(t) = t²/2. Hyperbolic space, with curvature negative one, corresponds to G(t) = cosh(t) - 1. Spherical space, with curvature positive one, corresponds to G(t) = 1 - cos(t).

The framework's library proves a dichotomy theorem. Under structural axioms, which include normalization at zero and a calibration condition, the spherical case is ruled out because it violates non-negativity: the function 1 - cos(t) is never positive, and it is negative at t = π. The flat case is also eliminated, not by contradiction but by the requirement that recognition geometry be non-trivially curved. The result, curvature_gate_main, states that a smooth, even, non-negative function satisfying the constant curvature condition must be either flat or hyperbolic. The hyperbolic solution, G(t) = cosh(t) - 1, is the one the framework adopts as the recognition cost law.

The physical interpretation is direct. Flat geometry means comparisons are independent, with no holistic structure. Hyperbolic geometry means comparisons are entangled, and nearby states diverge exponentially. The gate therefore selects a world where recognition is a connected, curved affair, not a collection of isolated judgments. This is a proved theorem in the framework's library, not a hypothesis, and it is a step toward deriving the golden ratio and the eight-tick recognition cycle elsewhere in the framework.

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

/-- 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 hyperbolic G from the RCL. -/
noncomputable def Gcosh (t : ℝ) : ℝ := Real.cosh t - 1

What this page does not claim

The curvature gate does not prove that the physical universe is hyperbolic. The flat solution G(t) = t²/2 is not shown to be impossible, only to be outside the recognition cost law. The module does not derive the value of any physical constant.

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: