Cost Cauchy Auxiliary

The auxiliary function

In the classification of solutions to a functional equation, a standard move is to introduce an auxiliary function that simplifies the problem. Here the equation is d'Alembert's, H(t+u) + H(t-u) = 2·H(t)·H(u), with H(0) = 1. The auxiliary function is φ(t) = H(t) + √(H(t)² - 1). This is the hyperbolic cosine analogue: if H(t) = cosh(λt), then φ(t) = e^(λt). The square root is real when H(t) ≥ 1, which is the case that matters for the Recognition Science cost function.

The point of φ is that it converts a d'Alembert equation into a multiplicative one. The key identity is φ(t+u) = φ(t)·φ(u), which is the Cauchy multiplicative equation. For a continuous positive function, that equation forces φ(t) = e^(λt), and then H(t) = cosh(λt). This is the classic Aczél classification: a continuous d'Alembert solution with H(0) = 1 is either cosh or cos, depending on whether H ever exceeds 1.

The machine-checked library of formal theorems records the status precisely. The definitions and three theorems are proved: φ(0) = 1, φ(t) > 0 when H(t) ≥ 1, and H(t) = (φ(t) + φ(t)⁻¹)/2. The multiplicative identity is stated as a conditional assumption, not yet proved. The step from multiplicative Cauchy to exponential is also stated as an assumption, not proved. The full classification theorem is therefore conditional on those two bridge lemmas.

In plain language: the module sets up the machinery for the cosh branch of the classification, proves the easy facts about the auxiliary function, and clearly marks the two remaining gaps. It does not claim the full classification, and it does not yet connect to the Recognition Science cost function. What it establishes is a clean, honest scaffold for a standard piece of analysis.

/-- φ(t) = H(t) + √(H(t)² - 1) for d'Alembert solutions with H(t) ≥ 1. -/
def phi (H : ℝ → ℝ) (t : ℝ) : ℝ :=
  H t + Real.sqrt (H t ^ 2 - 1)

/-- φ(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]

/-- φ(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

/-- 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

The multiplicative identity φ(t+u) = φ(t)·φ(u) is not proved in this module; it is stated as an assumption. The step from multiplicative Cauchy to exponential is not proved; it is stated as an assumption. The full Aczél classification is not proved; it is conditional on the two bridge lemmas. This module does not connect the auxiliary function to the Recognition Science cost function.

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: