Foundation Dalembert Curvature Gate Curvature Gate Summary

The curvature gate

The curvature gate is a step in the Recognition Science framework's derivation of its cost function. The framework models recognition as a discrete record of events, and the cost of that record is forced by a small set of conditions. One of those conditions concerns the geometry of the cost metric: it must have constant nonzero curvature. The declaration curvature_gate_summary packages the results of that gate into a single theorem.

The theorem examines three candidate metric shapes, expressed through the log-coordinate function G(t). The flat shape, G(t) = t²/2, satisfies the structural axioms and the calibration condition. The hyperbolic shape, G(t) = cosh(t) - 1, also satisfies those axioms and calibration. The spherical shape, G(t) = cos(t) - 1, satisfies its own curvature equation but fails calibration: its second derivative at zero is -1, not +1. The summary theorem states these three facts together.

The gate's role is to eliminate the spherical option. A separate theorem, curvature_gate_main, shows that under the full assumptions, including non-negativity of the cost, only the flat or hyperbolic shapes remain. The spherical shape is ruled out because it becomes negative, which a cost function cannot be. The flat shape remains as a counterexample to uniqueness, while the hyperbolic shape is the one the framework's chain of derivations selects.

In Recognition Science, this is the geometric path that leads to the golden ratio and the eight-tick cycle. The curvature gate is not a proof that the hyperbolic shape is the only possible cost; it is a proof that among the three constant-curvature candidates, only two survive the structural axioms, and only one of those is non-negative. The summary theorem is a compact statement of that dichotomy.

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

/-- Gcosh satisfies the hyperbolic ODE: G''(t) = G(t) + 1 = cosh(t). -/
theorem Gcosh_satisfies_hyperbolic : SatisfiesHyperbolicODE Gcosh := by
  intro t
  -- G(t) = cosh(t) - 1, G'(t) = sinh(t), G''(t) = cosh(t)
  have h1 : deriv Gcosh = Real.sinh := by
    ext s
    unfold Gcosh
    rw [deriv_sub_const, Real.deriv_cosh]
  have h2 : deriv (deriv Gcosh) t = Real.cosh t := by
    rw [h1, Real.deriv_sinh]
  rw [h2]
  unfold Gcosh
  ring

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

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

The curvature gate does not prove that the hyperbolic shape is the unique cost function; the flat shape remains a valid counterexample under the structural axioms. The summary theorem does not establish that the cost metric must have constant curvature; that is an assumption of the gate, not a consequence.

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: