Encyclopedia Foundation Foundation Dalembert Full Unconditional D Alembert Forces Cosh Is Theorem

ARTICLE 2 claims 2 theorems

Foundation Dalembert Full Unconditional D Alembert Forces Cosh Is Theorem

A single functional equation, with no extra assumptions, forces the hyperbolic cosine as the only possible smooth solution.

Verify this page

The forced cosine

The hyperbolic cosine, cosh, is the even function that describes a hanging cable's curve and the shape of a catenary. It is defined by cosh(t) = (e^t + e^(-t))/2. The declaration in question proves that this function is not just one possible solution to a classic equation, but the only one, given a few basic conditions.

The equation is d'Alembert's functional equation, H(t + u) + H(t - u) = 2 * H(t) * H(u), a relation that appears in geometry and probability. The theorem, named dAlembert_forces_cosh_is_theorem, states: if a twice-differentiable function H satisfies this equation, has H(0) = 1, and its second derivative at zero equals 1, then H must be cosh(t) for every real number t. The proof of this uniqueness result is a standard one, relying on converting the functional equation into an ordinary differential equation and applying an existence and uniqueness theorem.

In Recognition Science, this result is a key step in a longer chain. The framework starts with a ledger, a discrete record of recognition events, and a cost, a measure of the price of recognizing one thing as another. The framework models the cost of a comparison as a function F(x), where x is the ratio of two quantities. A consistency condition, that the cost of a combined comparison must be a function of the individual costs, leads to a multiplicative version of d'Alembert's equation. The theorem then forces the logarithm of the cost to be cosh minus one, which in turn pins down the exact form of the cost function as J(x) = (x + 1/x)/2 - 1.

The power of this specific declaration is that it removes a previous assumption. Earlier versions of the argument required the unknown function P, which describes how costs combine, to be a polynomial. This theorem proves that P's form is also forced, with no such assumption. The machine-checked library of formal theorems records this as a fully unconditional result, meaning both the cost function and the combination rule are uniquely determined from the basic axioms.

This does not, however, claim that the physical universe must obey this equation. The theorem is a mathematical statement about functions. The framework's later step, applying this cost function to physical constants and particle masses, is a separate, empirical check, not part of this proof. The declaration itself only establishes the mathematical uniqueness result.

THEOREM dAlembert_forces_cosh_is_theorem · IndisputableMonolith/Foundation/DAlembert/FullUnconditional.lean
dAlembert_forces_cosh_is_theorem · IndisputableMonolith/Foundation/DAlembert/FullUnconditional.lean:216 
/-- `dAlembert_forces_cosh_hypothesis` is provable from Aczél's theorem.
    ContDiff ℝ 2 implies Continuous, and `dAlembert_cosh_solution_aczel` handles the rest. -/
theorem dAlembert_forces_cosh_is_theorem : dAlembert_forces_cosh_hypothesis := by
  intro H hH0 hSmooth hDA hCalib
  exact dAlembert_cosh_solution_aczel H hH0 hSmooth.continuous hDA hCalib
THEOREM full_unconditional_inevitability · IndisputableMonolith/Foundation/DAlembert/FullUnconditional.lean
full_unconditional_inevitability · IndisputableMonolith/Foundation/DAlembert/FullUnconditional.lean:273 
/-- **THEOREM (Full Unconditional Inevitability)**

If F : ℝ₊ → ℝ satisfies:
1. F(1) = 0 (normalization)
2. F(x) = F(1/x) (symmetry)
3. F ∈ C² (smoothness)
4. G''(0) = 1 where G(t) = F(exp(t)) (calibration)
5. F(xy) + F(x/y) = P(F(x), F(y)) for SOME function P

Then:
- F(x) = J(x) = (x + 1/x)/2 - 1
- P(u, v) = 2uv + 2u + 2v for all u, v ≥ 0

**NO ASSUMPTION ON P IS MADE.**
-/
theorem full_unconditional_inevitability
    (hyps : FullUnconditionalHypotheses)
    (F : ℝ → ℝ)
    (P : ℝ → ℝ → ℝ)
    (hSymm : ∀ x : ℝ, 0 < x → F x = F x⁻¹)
    (hUnit : F 1 = 0)
    (hSmooth : ContDiff ℝ 2 F)
    (hCalib : deriv (deriv (G F)) 0 = 1)
    (hCons : ∀ x y : ℝ, 0 < x → 0 < y → F (x * y) + F (x / y) = P (F x) (F y)) :
    -- Conclusion 1: F = J
    (∀ x : ℝ, 0 < x → F x = Cost.Jcost x) ∧
    -- Conclusion 2: P = RCL polynomial on [0, ∞)²
    (∀ u v : ℝ, 0 ≤ u → 0 ≤ v → P u v = 2 * u * v + 2 * u + 2 * v) := by
  -- First establish F = J (used by both parts)
  have hP_RCL := hyps.consistency_RCL F P hSymm hUnit hSmooth hCons
  have hG_RCL : ∀ t u : ℝ, G F (t + u) + G F (t - u) =
      2 * G F t * G F u + 2 * G F t + 2 * G F u := by
    intro t u
    simp only [G]
    have hexp_t : 0 < Real.exp t := Real.exp_pos t
    have hexp_u : 0 < Real.exp u := Real.exp_pos u
    have h := hCons (Real.exp t) (Real.exp u) hexp_t hexp_u
    rw [hP_RCL (Real.exp t) (Real.exp u) hexp_t hexp_u] at h
    rw [← Real.exp_add, ← Real.exp_sub] at h
    exact h
  have hG0 : G F 0 = 0 := G_zero_of_unit F hUnit
  let Hlocal := fun t => G F t + 1
  have hH0 : Hlocal 0 = 1 := by
    simp only [Hlocal, G, Real.exp_zero]; rw [hUnit]; ring
  have hH_dA : ∀ t u : ℝ, Hlocal (t + u) + Hlocal (t - u) = 2 * Hlocal t * Hlocal u :=
    H_dAlembert_of_G_RCL (G F) hG0 hG_RCL
  have hH_smooth : ContDiff ℝ 2 Hlocal := by
    simp only [Hlocal]
    exact (hSmooth.comp Real.contDiff_exp).add contDiff_const
  have hH_calib : deriv (deriv Hlocal) 0 = 1 := by
    have h1 : deriv Hlocal = deriv (G F) := by
      ext t; change deriv (fun s => G F s + 1) t = deriv (G F) t
      simpa using (deriv_add_const (f := G F) (x := t) (c := (1 : ℝ)))
    have h2 : deriv (deriv Hlocal) = deriv (deriv (G F)) := congrArg deriv h1
    exact (congrArg (fun g => g 0) h2).trans hCalib
  have hH_cosh : ∀ t, Hlocal t = Real.cosh t :=
    hyps.dAlembert_cosh Hlocal hH0 hH_smooth hH_dA hH_calib
  have hG_cosh : ∀ t, G F t = Real.cosh t - 1 := fun t => by
    have h := hH_cosh t; simp only [Hlocal] at h; linarith
  have hF_eq_J : ∀ x : ℝ, 0 < x → F x = Cost.Jcost x := by
    intro x hx
    rw [← Real.exp_log hx]
    have h1 := hG_cosh (Real.log x); simp only [G] at h1
    have h2 := Jcost_G_eq_cosh_sub_one (Real.log x); simp only [G] at h2
    linarith
  constructor
  · exact hF_eq_J
  · -- Part 2: P is determined since F = J and J is surjective
    intro u v hu hv
    -- Since F = J, any instance of the consistency equation is J's RCL
    have hCons_J : ∀ x y : ℝ, 0 < x → 0 < y →
        Cost.Jcost (x * y) + Cost.Jcost (x / y) = P (Cost.Jcost x) (Cost.Jcost y) := by
      intro x y hx hy
      rw [← hF_eq_J (x * y) (mul_pos hx hy), ← hF_eq_J (x / y) (div_pos hx hy),
          ← hF_eq_J x hx, ← hF_eq_J y hy]
      exact hCons x y hx hy
    exact P_determined_nonneg P hCons_J u v hu hv

What this page does not claim

This theorem does not claim that the physical universe must obey this equation. The theorem does not prove that the cost function applies to any specific physical system. The theorem does not derive the fine-structure constant or any other physical constant.

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

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND