Cost Cauchy Auxiliary Phi Pos

The auxiliary function

The classical d'Alembert functional equation is H(t+u) + H(t-u) = 2H(t)H(u), a relation that forces a function to behave like a hyperbolic cosine or an ordinary cosine. In the classification of continuous solutions with H(0) = 1, the framework's library formalizes the branch where H takes values at least 1, the case relevant to its cost function. The auxiliary function φ(t) = H(t) + √(H(t)² - 1) is the key construction: it converts the d'Alembert equation into the multiplicative Cauchy equation φ(t+u) = φ(t)φ(u), which for continuous positive functions forces the exponential form φ(t) = e^(λt).

The declaration phi_pos establishes a single, precise fact: whenever H(t) ≥ 1, the auxiliary function φ(t) is strictly positive. The proof is a short algebraic argument: the square root term is nonnegative because H(t)² - 1 ≥ 0, and adding it to H(t) ≥ 1 gives a sum strictly greater than zero. This positivity is not a technical footnote; it is the condition that licenses the logarithm step in the classification. Without φ(t) > 0, one cannot define g(t) = log φ(t) and reduce the multiplicative equation to the additive Cauchy equation g(t+u) = g(t) + g(u), whose continuous solutions are exactly the linear functions g(t) = λt.

The lemma is proved in the machine-checked library of formal theorems, with the full statement: for any real function H and any real t, if 1 ≤ H(t), then 0 < φ(t). It also comes with a companion result, phi_at_zero, showing φ(0) = 1 when H(0) = 1. These two facts together give the recovery formula H(t) = (φ(t) + φ(t)⁻¹)/2, which inverts the construction and closes the loop back to the hyperbolic cosine form.

What phi_pos does not claim is as important as what it proves. It does not assert that the multiplicative Cauchy equation holds; that is a separate statement, H_PhiMultiplicative, which remains conditional in the library. It does not prove that continuous positive multiplicative functions are exponentials; that is the standard Cauchy result, stated as a hypothesis with a proof roadmap but not yet formalized. And it does not, by itself, complete the classification of d'Alembert solutions. The full classification theorem, aczel_classification_conditional, assembles phi_pos together with the two bridge lemmas, and it is explicitly conditional on them.

For the reader, the practical consequence is this: the framework has nailed down the algebraic foundation of the cosh branch, and the positivity lemma is the load-bearing floor beneath it. What remains open is the analytic bridge, the step that turns the algebraic identity into the exponential form. That gap is named, not hidden, and it is the precise place where the framework's proof currently stops.

/-- φ(t) > 0 when H(t) ≥ 1. -/
theorem phi_pos (H : ℝ → ℝ) (t : ℝ) (ht : 1 ≤ H t) : 0 < phi H t := by
  unfold phi
  have h_sq : 0 ≤ H t ^ 2 - 1 := by nlinarith
  have h_sqrt : 0 ≤ Real.sqrt (H t ^ 2 - 1) := Real.sqrt_nonneg _
  linarith

/-- φ(0) = 1 when H(0) = 1. -/
theorem phi_at_zero (H : ℝ → ℝ) (h_one : H 0 = 1) : phi H 0 = 1 := by
  simp [phi, h_one]

/-- The full Aczél classification, conditional on the two bridge lemmas. -/
theorem aczel_classification_conditional
    (H : ℝ → ℝ)
    (h_one : H 0 = 1)
    (h_cont : Continuous H)
    (h_dA : ∀ t u, H (t + u) + H (t - u) = 2 * H t * H u)
    (h_phi_mult : H_PhiMultiplicative H)
    (h_cauchy : H_CauchyToExponential)
    (h_ge_one : ∀ t, 1 ≤ H t) :
    ∃ lam : ℝ, ∀ t, H t = Real.cosh (lam * t) := by
  have h_phi_cont : Continuous (phi H) := by
    unfold phi
    exact h_cont.add ((h_cont.pow 2).sub continuous_const).sqrt
  have h_phi_pos : ∀ t, 0 < phi H t := fun t => phi_pos H t (h_ge_one t)
  have h_phi_zero : phi H 0 = 1 := phi_at_zero H h_one
  have h_phi_cauchy : ∀ t u, phi H (t + u) = phi H t * phi H u :=
    fun t u => h_phi_mult t u (h_ge_one t) (h_ge_one u)
  obtain ⟨lam_, hlam⟩ := h_cauchy (phi H) h_phi_cont h_phi_pos h_phi_zero h_phi_cauchy
  refine ⟨lam_, fun t => ?_⟩
  have h_phi_exp : phi H t = Real.exp (lam_ * t) := hlam t
  have h_phi_neg : phi H (-t) = Real.exp (-(lam_ * t)) := by
    rw [hlam (-t)]; ring_nf
  have h_H_from_phi := H_from_phi H t (h_ge_one t)
  rw [h_phi_exp] at h_H_from_phi
  rw [Real.cosh_eq]
  convert h_H_from_phi using 1
  rw [exp_neg]

What this page does not claim

phi_pos does not prove that φ satisfies the multiplicative Cauchy equation. phi_pos does not prove that continuous positive multiplicative functions are exponentials. phi_pos does not, by itself, complete the classification of continuous d'Alembert solutions.

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: