pith. sign in
module module high

IndisputableMonolith.Foundation.DAlembert.CurvatureGate

show as:
view Lean formalization →

CurvatureGate supplies the log-coordinate lift of a multiplicative cost function F together with the three curvature-specific G functions (quadratic, cosh, spherical). Researchers proving the bridge from interaction axioms to d'Alembert structure cite these definitions when changing variables to additive t. The module is purely definitional; it records the explicit maps and the three ODE-satisfaction lemmas without further derivation.

claim$H(t) := F(e^t) + 1$, $G_{ ext{quad}}(t) := t^2/2$, $G_{ ext{cosh}}(t) := rac12( ext{cosh}(t)-1)$, $G_{ ext{spher}}(t) := 1 - ext{cos}(t)$ together with the statements that each $G$ satisfies its respective second-order ODE.

background

The module works inside the Recognition Science setting where a cost function F obeys the Recognition Composition Law and is lifted to additive coordinates via the exponential map. The log-lift H converts the multiplicative interaction condition on F into an additive functional equation on H. Counterexamples imported from the sibling module show that the mere existence of a combiner P is insufficient to force the d'Alembert form; the curvature-specific G functions are therefore introduced to classify the possible second-order behaviors (flat, hyperbolic, spherical).

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the concrete log-coordinate objects required by the Bridge Theorem in AnalyticBridge and by the Fourth Gate in FourthGate; those modules in turn feed the unified inevitability result in TriangulatedProof. It therefore occupies the position immediately after the counterexample warning and before the analytic forcing argument that converts structural axioms into the d'Alembert equation.

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)