Foundation Dalembert Curvature Gate Gquad Satisfies Flat

The flat counterexample

The declaration Gquad_satisfies_flat proves, in the framework's machine-checked library of formal theorems, that the function G(t) = t²/2 satisfies the defining equation of a flat geometry. In this context, a metric is flat when its second derivative is constant and equal to 1, written as G''(t) = 1. This is the simplest possible case: the curve is a parabola, and its curvature is zero everywhere. The declaration is a recognition cost, a measure of the price of comparing two states, that shows what a geometry with no interaction between comparisons looks like.

The flat case is the counterexample in a larger classification. The framework's curvature gate divides possible cost metrics into three types: flat, hyperbolic, and spherical. The hyperbolic case, G(t) = cosh(t) - 1, satisfies G''(t) = G(t) + 1 and represents entangled comparisons that diverge exponentially. The spherical case, G(t) = 1 - cos(t), satisfies G''(t) = -(G(t) + 1) and represents periodic comparisons, but it is ruled out because it becomes negative. The flat case is also ruled out, not because it violates any equation, but because it represents a world where comparisons are independent and carry no holistic structure. The framework proves that the real recognition cost must be hyperbolic, not flat.

What the declaration does not claim is just as important. It does not prove that flat geometry is impossible or contradictory; it only proves that the quadratic function satisfies the flat equation. The exclusion of flat geometry comes from a separate theorem, curvature_gate_main, which assumes smoothness, normalization, calibration, evenness, and non-negativity, and then concludes that only flat or hyperbolic are possible. The spherical case is eliminated by non-negativity, and the flat case is eliminated by the requirement that recognition geometry be non-trivially curved, a principle stated separately. The declaration Gquad_satisfies_flat is a building block, not the final verdict.

In plain terms, this theorem pins down what "flat" means in the framework's language and gives it a concrete representative. It is the baseline against which the hyperbolic case is measured, and it is the option that the framework ultimately rejects. The consequence is that the framework's cost function is not the simple quadratic, but the more complex hyperbolic form that forces the golden ratio and the rest of the derived structure.

/-- Gquad satisfies the flat ODE: G''(t) = 1. -/
theorem Gquad_satisfies_flat : SatisfiesFlatODE Gquad := by
  intro t
  -- G(t) = t²/2, G'(t) = t, G''(t) = 1
  have h1 : deriv Gquad = fun t => t := by
    ext s
    unfold Gquad
    have hd : HasDerivAt (fun t => t ^ 2 / 2) s s := by
      have := hasDerivAt_pow 2 s
      simp only [Nat.cast_ofNat, pow_one] at this
      have h := this.div_const 2
      convert h using 1
      ring
    exact hd.deriv
  have h2 : deriv (deriv Gquad) t = 1 := by
    rw [h1]
    simp only [deriv_id'']
  exact h2

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

What this page does not claim

This declaration does not prove that flat geometry is impossible or contradictory. This declaration does not prove that the hyperbolic case is the correct one; that is a separate theorem. This declaration does not establish any empirical claim about the physical world.

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: