Pith. sign in
module module high

IndisputableMonolith.Foundation.DAlembert.CurvatureGate

show as:
view Lean formalization →

The CurvatureGate module defines the log-coordinate lift of a cost function F to H(t) = F(e^t) + 1 together with curvature-specific G forms. Researchers establishing the d'Alembert structure from interaction axioms cite it when moving from functional equations to ODE verification. The module supplies direct definitions of Gquad, Gcosh, Gspher and one-line verifications that each satisfies its target ODE while exhibiting a counterexample for the mismatched case.

claimLet $F$ satisfy the Recognition Composition Law. Define the log-lift $H(t) := F(e^t) + 1$. Introduce curvature representatives $G_{ m quad}(t) = t^2/2$, $G_{ m cosh}(t) = m cosh(t) - 1$, $G_{ m spher}(t)$ and verify $G''(t) = G(t) + 1$ (hyperbolic), $G''(t) = 1$ (flat), or the spherical analogue.

background

The module sits inside the Foundation.DAlembert namespace and imports the Cost module (source of the Recognition Composition Law J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y)) together with the Counterexamples module. The latter records that existence of a combiner P satisfying F(xy) + F(x/y) = P(F(x), F(y)) does not by itself force the d'Alembert structure on the log-lift of F. Local notation therefore centers on the log-coordinate objects H_of_F and G_of_F that convert the original multiplicative relation into additive ODE statements.

proof idea

This is a definition module whose structure consists of introducing H_of_F and G_of_F, then instantiating the three curvature cases Gquad, Gcosh, Gspher. Each satisfies_ theorem is a direct algebraic check of the second derivative against the target right-hand side; the final Gquad_not_hyperbolic is a one-line counterexample showing the quadratic form fails the hyperbolic ODE.

why it matters in Recognition Science

The module supplies the concrete log-lift objects required by the curvature gate. It is imported by AnalyticBridge (which proves that structural axioms plus interaction force the d'Alembert equation on H), by FourthGate (which formalizes the normalized hyperbolic closure G''(t) = G(t) + 1), and by TriangulatedProof (which assembles the four gates into the unified inevitability theorem). It therefore closes the curvature component of Gate 3 in the T0-T8 forcing chain.

scope and limits

used by (3)

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

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (21)