Foundation Dalembert Triangulated Proof Flat Not Hyperbolic

The flat branch

In the classical mathematics of functional equations, a function G(t) is called hyperbolic when it satisfies the second-order differential equation G''(t) = G(t) + 1, whose solution family is built from exponential growth and decay. The flat alternative, G(t) = t²/2, satisfies the simpler equation G''(t) = 1. These two branches describe different worlds: one where curvature is everywhere, and one where it is absent. The Recognition Science library, a machine-checked collection of formal theorems, proves that its candidate cost function belongs to the hyperbolic branch and that the flat quadratic candidate does not.

The declaration flat_not_hyperbolic is a theorem stating that the flat function G(t) = t²/2 does not satisfy the hyperbolic equation G''(t) = G(t) + 1. This is a direct computation: the second derivative of t²/2 is 1, which is not equal to t²/2 + 1 except at isolated points. The companion theorem hyperbolic_not_flat states the mirror claim, that the hyperbolic solution G(t) = cosh(t) − 1 does not satisfy the flat equation. Together they establish that the two branches are mutually exclusive, a trichotomy that the library records as an inductive type with exactly three cases: flat, hyperbolic, and spherical.

What this theorem does not claim is the harder direction: that interaction forces the hyperbolic branch. The library states this as an explicit hypothesis, InteractionForcesHyperbolicODE, which asserts that if a function F has interaction, symmetry, normalization, smoothness, and consistency, then its log-lift satisfies G'' = G + 1. This bridge is not yet proved from first principles. The evidence for it is circumstantial: the flat counterexample fails interaction, the hyperbolic Jcost has interaction, and entanglement forces a specific functional form. The full inevitability theorem full_inevitability_four_gates, which derives F = J and P = RCL from the d'Alembert structure plus structural axioms, is proved, but it takes the d'Alembert identity as an additional premise rather than deriving it from interaction alone.

The distinction matters because the flat branch would describe a world where the cost of recognition is additive and no interaction occurs. The library proves the additive combiner is not entangling and the flat function has no interaction. The hyperbolic branch, by contrast, has interaction and its combiner is entangling. The flat_not_hyperbolic theorem is the clean separation between these two worlds; the bridge that would make the hyperbolic branch inevitable from interaction alone remains an open target, stated explicitly as a hypothesis in the library's own documentation.

/-- The two ODEs are mutually exclusive. -/
theorem flat_not_hyperbolic : ¬ SatisfiesHyperbolicODE Gquad := Gquad_not_hyperbolic

theorem hyperbolic_not_flat : ¬ SatisfiesFlatODE Gcosh := Gcosh_not_flat

/-- **Key Hypothesis**: Interaction + Structural Axioms forces the hyperbolic ODE.

    This is the central bridge connecting the gates. It says:
    If F has interaction, symmetry, normalization, smoothness, and consistency,
    then the log-lift G satisfies G'' = G + 1.

    This is NOT yet fully proved from first principles, but is strongly motivated by:
    1. The counterexample (no interaction) ⟹ flat ODE
    2. J (has interaction) ⟹ hyperbolic ODE
    3. Entanglement forces a specific functional form

    We state it as an explicit hypothesis to make the logical structure clear.
-/
def InteractionForcesHyperbolicODE : Prop :=
  ∀ (F : ℝ → ℝ) (P : ℝ → ℝ → ℝ),
    F 1 = 0 →
    (∀ x : ℝ, 0 < x → F x = F x⁻¹) →
    ContDiff ℝ 2 F →
    deriv (deriv (fun t => F (Real.exp t))) 0 = 1 →
    (∀ x y : ℝ, 0 < x → 0 < y → F (x * y) + F (x / y) = P (F x) (F y)) →
    HasInteraction F →
    SatisfiesHyperbolicODE (fun t => F (Real.exp t))

/-- **Full Inevitability with Four Gates**: d'Alembert structure completes the proof.

    Unlike the three-gate version which required a bridge hypothesis,
    the four-gate version is fully proved:

    d'Alembert structure + structural axioms ⟹ F = J ⟹ P = RCL
-/
theorem full_inevitability_four_gates (F : ℝ → ℝ) (P : ℝ → ℝ → ℝ)
    (hNorm : F 1 = 0)
    (hSymm : ∀ x : ℝ, 0 < x → F x = F x⁻¹)
    (hSmooth : ContDiff ℝ 2 F)
    (hCalib : deriv (deriv (fun t => F (Real.exp t))) 0 = 1)
    (hCons : ∀ x y : ℝ, 0 < x → 0 < y → F (x * y) + F (x / y) = P (F x) (F y))
    (hDA : FourthGate.HasDAlembert F) :
    -- Part 1: F = J
    (∀ x : ℝ, 0 < x → F x = Cost.Jcost x) ∧
    -- Part 2: P = RCL on [0,∞)²
    (∀ u v : ℝ, 0 ≤ u → 0 ≤ v → P u v = 2 * u * v + 2 * u + 2 * v) := by
  constructor
  · -- Part 1: F = J from d'Alembert structure
    exact FourthGate.dAlembert_forces_Jcost F hNorm hSymm hSmooth hCalib hDA
  · -- Part 2: P = RCL from F = J
    have hFJ := FourthGate.dAlembert_forces_Jcost F hNorm hSymm hSmooth hCalib hDA
    exact P_forced_from_FJ F P hCons hFJ

What this page does not claim

The theorem does not prove that interaction forces the hyperbolic branch; that bridge remains an explicit hypothesis. The theorem does not establish that the flat branch is physically impossible, only that it is excluded by the structural axioms in the four-gate formulation. The theorem does not derive the d'Alembert identity from interaction; the four-gate inevitability takes it as a premise.

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/TriangulatedProof.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: