Cost Aczel Theorem D Alembert Locally Bounded

The boundedness lemma

The d'Alembert equation asks for functions H that behave nicely under addition and subtraction of their inputs. It is a functional equation that appears in many parts of mathematics and physics. The classical solutions, when H(0) = 1, are the hyperbolic cosine, the ordinary cosine, and the constant function 1. The equation was studied by Jean le Rond d'Alembert in the 1740s in the context of the vibrating string problem.

A function is called locally bounded if, on any finite interval, its values never exceed some fixed number. Every continuous function has this property, because a continuous function on a closed interval always attains a maximum. The theorem dAlembert_locally_bounded in the framework's machine-checked library of formal theorems states exactly this: if H satisfies the d'Alembert equation and is continuous, then H is locally bounded. The proof is short and direct: it uses the compactness of closed intervals to find the maximum of |H| on any interval [−R, R].

This lemma is not an end in itself. It is the first rung in a bootstrap argument that climbs from continuity to infinite smoothness. The framework's library shows that a continuous solution of the d'Alembert equation is automatically infinitely differentiable, and then that it satisfies a simple second-order differential equation H'' = c·H. Solving that equation gives the three classical solutions. The locally bounded lemma provides the initial regularity needed to start the bootstrap.

In Recognition Science, this chain of results has a specific role. The framework derives its central cost function J(x) = (x + 1/x)/2 − 1 from five plain conditions, and the d'Alembert equation appears in the proof that the cost function is unique. The Aczél classification theorem, which the framework's library proves in full, guarantees that the only continuous solutions are the smooth ones. This eliminates the last remaining unproven assumption in the framework's foundation: the classification was previously taken as a hypothesis, and now it is a proved theorem.

The lemma itself does not claim anything about the classification. It only establishes local boundedness from continuity. It does not say that every solution is smooth, nor does it identify the three solution families. Those are separate theorems in the library. The lemma is a supporting step, not the main result. A reader who wants the full classification must look at the later theorems in the same file.

/-- H2: Continuous d'Alembert solutions are locally bounded. -/
theorem dAlembert_locally_bounded (H : ℝ → ℝ)
    (h_cont : Continuous H) :
    ∀ R : ℝ, 0 < R → ∃ M : ℝ, ∀ t, |t| ≤ R → |H t| ≤ M := by
  intro R hR
  have := IsCompact.exists_isMaxOn (isCompact_Icc (a := -R) (b := R))
    (Set.nonempty_Icc.mpr (by linarith)) (h_cont.abs.continuousOn)
  obtain ⟨x, _, hx⟩ := this
  exact ⟨|H x|, fun t ht => by
    apply hx (Set.mem_Icc.mpr ⟨by linarith [abs_le.mp ht], by linarith [abs_le.mp ht]⟩)⟩

private theorem dAlembert_contDiff_smooth (H : ℝ → ℝ) (h_one : H 0 = 1) (h_cont : Continuous H)
    (h_dAl : ∀ t u, H (t + u) + H (t - u) = 2 * H t * H u) :
    ContDiff ℝ smooth H :=
  contDiff_infty.mpr (dAlembert_contDiff_nat H h_one h_cont h_dAl)

/-- **THEOREM (Aczél, PROVED)**: `H_AczelClassification` holds unconditionally.
    This eliminates the sole remaining foundation axiom. -/
theorem h_aczel_classification_proved : H_AczelClassification :=
  fun H h_one h_cont h_dAlembert => dAlembert_contDiff_top H h_one h_cont h_dAlembert

-- The typeclass-parameterized `aczel_dAlembert_smooth` lives in
-- `IndisputableMonolith.Cost.AczelClass` and is satisfied by the
-- `AczelSmoothnessPackage` instance in `IndisputableMonolith.Cost.AczelProof`,
-- which delegates to `dAlembert_contDiff_top` above.

What this page does not claim

The lemma does not identify the three solution families; that is a separate classification theorem. The lemma does not claim that all d'Alembert solutions are smooth; it only establishes local boundedness from continuity. The framework does not claim to derive the fine-structure constant alpha; its expression lands within about 5.6 ppm but its seed is an identification, not a derived coupling.

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