Cost Cauchy Auxiliary H From Phi

Recovering the cost from its auxiliary

The d'Alembert equation, H(t+u) + H(t-u) = 2H(t)H(u), is a functional equation whose continuous solutions are exactly the hyperbolic cosine, the ordinary cosine, and constant functions. The hyperbolic cosine appears when the solution takes values greater than 1, and the classification proceeds by building an auxiliary function φ(t) = H(t) + √(H(t)² - 1). This φ is positive, equals 1 at zero, and satisfies the multiplicative Cauchy equation φ(t+u) = φ(t)φ(u), which for continuous positive functions forces φ(t) = e^(λt). Recovering H from φ is then a matter of algebra: H(t) = (φ(t) + φ(t)⁻¹)/2, the formula that defines the hyperbolic cosine.

The declaration H_from_phi in the framework's machine-checked library of formal theorems establishes exactly this recovery step. It proves that whenever H(t) ≥ 1, the identity H(t) = (φ(t) + φ(t)⁻¹)/2 holds, where φ is the auxiliary function defined above. This is a purely algebraic statement about real numbers, and the proof is a direct calculation from the definition of φ. The theorem is a component of the larger Aczél classification strategy, which aims to show that the only continuous d'Alembert solutions with H(0) = 1 and H(t) ≥ 1 are of the form H(t) = cosh(λt).

In Recognition Science, this classification matters because the framework's cost function J is defined so that H = 1 + J satisfies the d'Alembert equation. Since J grows unboundedly, H achieves values greater than 1, placing it in the hyperbolic cosine branch. The recovery formula H_from_phi is therefore the bridge that lets the framework pass from a solution of the d'Alembert equation to the explicit exponential form, and from there to the golden ratio and the forcing chain that derives physical constants. The theorem itself, however, does not prove that φ is multiplicative, nor that continuous multiplicative functions are exponentials; those are separate, conditional steps in the library.

What H_from_phi does not claim is just as important. It does not assert that every d'Alembert solution is a hyperbolic cosine, because that requires the two bridge lemmas: the multiplicativity of φ and the exponential form from the Cauchy equation. It does not claim that the auxiliary function is defined for all real inputs, since the square root requires H(t) ≥ 1. And it does not, by itself, derive any physical constant or the golden ratio; those conclusions depend on the full forcing chain, not on this single recovery identity. The theorem is a precise, narrow algebraic fact, and the framework's larger claims rest on the complete chain of such facts, each with its own proof and conditions.

/-- H(t) can be recovered from φ: H(t) = (φ(t) + φ(t)⁻¹) / 2 when φ(t) > 0. -/
theorem H_from_phi (H : ℝ → ℝ) (t : ℝ) (ht : 1 ≤ H t) :
    H t = (phi H t + (phi H t)⁻¹) / 2 := by
  unfold phi
  set s := Real.sqrt (H t ^ 2 - 1)
  have hs_sq : s ^ 2 = H t ^ 2 - 1 := by
    exact Real.sq_sqrt (by nlinarith : 0 ≤ H t ^ 2 - 1)
  have hs_nonneg : 0 ≤ s := Real.sqrt_nonneg _
  have h_pos : 0 < H t + s := by linarith
  have h_inv : (H t + s)⁻¹ = H t - s := by
    have : (H t + s) * (H t - s) = 1 := by nlinarith [hs_sq]
    rw [eq_comm, inv_eq_of_mul_eq_one_right this]
  rw [h_inv]
  ring

What this page does not claim

H_from_phi does not prove that every continuous d'Alembert solution is a hyperbolic cosine. H_from_phi does not derive the golden ratio or any physical constant. H_from_phi does not establish that the auxiliary function φ is multiplicative.

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/Cost/CauchyAuxiliary.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: