module module high

`IndisputableMonolith.Foundation.DAlembert.CurvatureGate`

This module supplies the log-coordinate representation of a cost function F, defining the lift H(t) = F(e^t) + 1 together with concrete G realizations (quadratic, cosh, spherical) and verification lemmas for the associated ODEs. Researchers formalizing the curvature gate and the transition from algebraic axioms to differential structure in Recognition Science cite it when bridging to the d'Alembert equation. The module consists of direct definitions plus short verification lemmas that check ODE satisfaction for each G variant.

claimThe log-lift is $H(t) := F(e^t) + 1$. Associated curvature functions are $G_mathrm{quad}$, $G_mathrm{cosh}$, $G_mathrm{spher}$ satisfying the flat ODE $G'' = 1$, the hyperbolic ODE $G'' = G + 1$, and the spherical ODE $G'' = -G + 1$ respectively.

background

Recognition Science works with cost functions F obeying the Recognition Composition Law. In log coordinates the d'Alembert structure becomes an ODE on the lift H(t) = F(e^t) + 1. The upstream Cost module supplies the basic cost axioms while the Counterexamples module records that the mere existence of a combiner P satisfying F(xy) + F(x/y) = P(F(x), F(y)) does not force the d'Alembert equation on the log-lift.

proof idea

This is a definition module. It introduces G_of_F and H_of_F, instantiates the three concrete realizations Gquad, Gcosh, Gspher, and supplies the verification lemmas Gquad_satisfies_flat, Gcosh_satisfies_hyperbolic, Gspher_satisfies_spherical together with the counterexample Gquad_not_hyperbolic.

why it matters in Recognition Science

The module supplies the curvature representations required by the AnalyticBridge module (Bridge Theorem: interaction implies H satisfies d'Alembert), the FourthGate module (d'Alembert structure as normalized closure with hyperbolic ODE G''(t) = G(t) + 1), and the TriangulatedProof module (unification of the four gates). It therefore fills the curvature gate (Gate 3) in the Option A formulation.

scope and limits

Does not prove that any given F satisfies the interaction axiom.
Does not derive the d'Alembert equation from algebraic axioms alone.
Does not address the entanglement or interaction gates.
Does not compute numerical constants such as phi or alpha.

used by (3)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Foundation.DAlembert.AnalyticBridge module_import
IndisputableMonolith.Foundation.DAlembert.FourthGate module_import
IndisputableMonolith.Foundation.DAlembert.TriangulatedProof module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Cost module_import
IndisputableMonolith.Foundation.DAlembert.Counterexamples module_import

declarations in this module (21)

def G_of_F L38
def H_of_F L41
def Gquad L46
def Gcosh L49
def Gspher L52
def SatisfiesHyperbolicODE L57
def SatisfiesFlatODE L61
def SatisfiesSphericalODE L65
theorem Gquad_satisfies_flat L71
theorem Gcosh_satisfies_hyperbolic L90
theorem Gspher_satisfies_spherical L104
theorem Gquad_not_hyperbolic L124
theorem Gcosh_not_flat L140
theorem Gspher_nonpositive L155
theorem Gspher_negative_at_pi L162
def IsNonNegativeG L167
theorem Gspher_violates_nonnegativity L170
inductive CurvatureType L179
theorem curvature_gate_main L195
theorem curvature_gate_dichotomy L225
theorem curvature_gate_summary L249