Encyclopedia Cost Cost Aczel Theorem

ARTICLE 4 claims 4 theorems

Cost Aczel Theorem

The Aczél theorem proves that every continuous solution to the d'Alembert equation with H(0) = 1 is infinitely smooth and must be one of three functions: constant one, hyperbolic cosine, or cosine.

Verify this page

The Aczél Classification

The Aczél theorem is a result in functional equations that Recognition Science uses to remove its last foundational hypothesis. It concerns functions H that satisfy the d'Alembert equation H(t+u) + H(t-u) = 2·H(t)·H(u) with H(0) = 1. The theorem states that if H is continuous, then H must be one of exactly three forms: H(t) = 1, H(t) = cosh(λt), or H(t) = cos(λt) for some real λ. All three are infinitely differentiable, so continuity alone forces smoothness.

The proof in the kernel-checked library 4 proceeds by an integration bootstrap. A continuous H has an antiderivative Φ, and the d'Alembert equation yields a representation formula expressing H(t) as a quotient of differences of Φ. This formula lets each derivative of H be expressed in terms of derivatives of Φ, so H gains one degree of smoothness at a time. Repeating the argument shows H is C^n for every n, hence C^∞. Once H is smooth, differentiating the d'Alembert equation twice gives the ordinary differential equation H'' = c·H with c = H''(0). Solving this ODE yields the three possible forms.

The module establishes that the proposition H_AczelClassification, which was previously the sole remaining axiom in the IndisputableMonolith codebase, holds unconditionally. The theorem h_aczel_classification_proved is established with zero sorry and zero axioms. This means the entire Recognition Science framework, including the forcing chain that derives the golden ratio, the eight-tick cycle, and three spatial dimensions, now rests on the standard axioms of the the kernel-checked library kernel alone. The Aczél theorem is not a physical claim; it is a mathematical fact that supplies the smoothness needed for the cost function derivation.

THEOREM dAlembert_contDiff_top · IndisputableMonolith/Cost/AczelTheorem.lean
dAlembert_contDiff_top · IndisputableMonolith/Cost/AczelTheorem.lean:351 
/-- The full Aczél classification theorem. Continuous d'Alembert with H(0) = 1
    implies H ∈ {cosh(λ·), cos(λ·), 1}, all of which are C^∞. -/
private theorem dAlembert_contDiff_top (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 ℝ ⊤ H := by
  have h_sm : ContDiff ℝ smooth H := dAlembert_contDiff_smooth H h_one h_cont h_dAl
  have h2 : ContDiff ℝ 2 H := by exact_mod_cast (contDiff_infty.mp h_sm) 2
  have hDiff : Differentiable ℝ H := h2.differentiable (by decide : (2 : WithTop ℕ∞) ≠ 0)
  have h_H'0 : deriv H 0 = 0 :=
    even_deriv_at_zero H (dAlembert_even H h_one h_dAl) hDiff.differentiableAt
  have h_ode := dAlembert_to_ODE_general H h_sm h_dAl
  set c := deriv (deriv H) 0
  have hDD : Differentiable ℝ (deriv H) := by
    rw [show (2 : WithTop ℕ∞) = 1 + 1 from rfl] at h2
    exact (contDiff_succ_iff_deriv.mp h2).2.2.differentiable
      (by decide : (1 : WithTop ℕ∞) ≠ 0)
  by_cases hc_pos : 0 < c
  · -- Case c > 0: H = cosh(√c · t)
    have hsc_ne : Real.sqrt c ≠ 0 := ne_of_gt (Real.sqrt_pos.mpr hc_pos)
    let g : ℝ → ℝ := fun s => H (s / Real.sqrt c)
    have h_div : ∀ s, HasDerivAt (fun x => x / Real.sqrt c) (Real.sqrt c)⁻¹ s := fun s => by
      have := (hasDerivAt_id s).div_const (Real.sqrt c)
      simp only [id, one_div] at this; exact this
    have hg_d : ∀ s, HasDerivAt g (deriv H (s / Real.sqrt c) * (Real.sqrt c)⁻¹) s :=
      fun s => (hDiff _).hasDerivAt.comp s (h_div s)
    have hg_ode : ∀ t, deriv (deriv g) t = g t := by
      intro s
      have hg1 : deriv g = fun s => deriv H (s / Real.sqrt c) * (Real.sqrt c)⁻¹ :=
        funext fun s => (hg_d s).deriv
      have h_dd_g : HasDerivAt (deriv g)
          ((deriv (deriv H) (s / Real.sqrt c) * (Real.sqrt c)⁻¹) * (Real.sqrt c)⁻¹) s := by
        rw [hg1]
        exact ((hDD (s / Real.sqrt c)).hasDerivAt.comp s (h_div s)).mul_const _
      rw [h_dd_g.deriv, h_ode (s / Real.sqrt c)]
      simp only [g]
      rw [show c * H (s / Real.sqrt c) * (Real.sqrt c)⁻¹ * (Real.sqrt c)⁻¹ =
          H (s / Real.sqrt c) * (c * ((Real.sqrt c)⁻¹ * (Real.sqrt c)⁻¹)) from by ring,
          show (Real.sqrt c)⁻¹ * (Real.sqrt c)⁻¹ = (Real.sqrt c * Real.sqrt c)⁻¹ from
            (mul_inv_rev _ _).symm,
          Real.mul_self_sqrt (le_of_lt hc_pos),
          mul_inv_cancel₀ (ne_of_gt hc_pos), mul_one]
    have h_eq : ∀ t, H t = Real.cosh (Real.sqrt c * t) := fun t => by
      have := ode_cosh_uniqueness_contdiff g (h2.comp (contDiff_id.div_const _))
        hg_ode (by simp [g, h_one]) (by rw [(hg_d 0).deriv]; simp [h_H'0])
        (Real.sqrt c * t)
      simp only [g, mul_div_cancel_left₀ _ hsc_ne] at this; exact this
    rw [show H = fun t => Real.cosh (Real.sqrt c * t) from funext h_eq]
    exact Real.contDiff_cosh.comp (contDiff_const.mul contDiff_id)
  · by_cases hc_neg : c < 0
    · -- Case c < 0: H = cos(√|c| · t)
      set c' := -c
      have hsc_ne : Real.sqrt c' ≠ 0 := ne_of_gt (Real.sqrt_pos.mpr (neg_pos.mpr hc_neg))
      let g : ℝ → ℝ := fun s => H (s / Real.sqrt c')
      have h_div : ∀ s, HasDerivAt (fun x => x / Real.sqrt c') (Real.sqrt c')⁻¹ s :=
        fun s => by
        have := (hasDerivAt_id s).div_const (Real.sqrt c')
        simp only [id, one_div] at this; exact this
      have hg_d : ∀ s, HasDerivAt g (deriv H (s / Real.sqrt c') * (Real.sqrt c')⁻¹) s :=
        fun s => (hDiff _).hasDerivAt.comp s (h_div s)
      have hg_ode : ∀ t, deriv (deriv g) t = -(g t) := by
        intro s
        have hg1 : deriv g = fun s => deriv H (s / Real.sqrt c') * (Real.sqrt c')⁻¹ :=
          funext fun s => (hg_d s).deriv
        have h_dd_g : HasDerivAt (deriv g)
            ((deriv (deriv H) (s / Real.sqrt c') * (Real.sqrt c')⁻¹) * (Real.sqrt c')⁻¹) s := by
          rw [hg1]
          exact ((hDD (s / Real.sqrt c')).hasDerivAt.comp s (h_div s)).mul_const _
        rw [h_dd_g.deriv, h_ode (s / Real.sqrt c')]
        simp only [g, c']
        rw [show c * H (s / Real.sqrt (-c)) * (Real.sqrt (-c))⁻¹ * (Real.sqrt (-c))⁻¹ =
            H (s / Real.sqrt (-c)) * (c * ((Real.sqrt (-c))⁻¹ * (Real.sqrt (-c))⁻¹)) from
              by ring,
            show (Real.sqrt (-c))⁻¹ * (Real.sqrt (-c))⁻¹ = (Real.sqrt (-c) * Real.sqrt (-c))⁻¹
              from (mul_inv_rev _ _).symm,
            Real.mul_self_sqrt (le_of_lt (neg_pos.mpr hc_neg)),
            show c * (-c)⁻¹ = -(1 : ℝ) from by
              have hc_ne : c ≠ 0 := ne_of_lt hc_neg
              field_simp]
        ring
      have h_eq : ∀ t, H t = Real.cos (Real.sqrt c' * t) := fun t => by
        have := ode_cos_uniqueness g (h2.comp (contDiff_id.div_const _))
          hg_ode (by simp [g, h_one]) (by rw [(hg_d 0).deriv]; simp [h_H'0])
          (Real.sqrt c' * t)
        simp only [g, mul_div_cancel_left₀ _ hsc_ne] at this; exact this
      rw [show H = fun t => Real.cos (Real.sqrt c' * t) from funext h_eq]
      exact Real.contDiff_cos.comp (contDiff_const.mul contDiff_id)
    · -- Case c = 0: H = 1
      have hc0 : c = 0 := le_antisymm (not_lt.mp hc_pos) (not_lt.mp hc_neg)
      have h_H'_zero : ∀ t, deriv H t = 0 := by
        have := is_const_of_deriv_eq_zero hDD (fun t => by rw [h_ode t, hc0, zero_mul])
        intro t; have := this t 0; simp [h_H'0] at this; exact this
      rw [show H = fun _ => (1 : ℝ) from funext fun t => by
        have := is_const_of_deriv_eq_zero hDiff h_H'_zero t 0
        simp [h_one] at this; exact this]
      exact contDiff_const
THEOREM dAlembert_contDiff_nat · IndisputableMonolith/Cost/AczelTheorem.lean
dAlembert_contDiff_nat · IndisputableMonolith/Cost/AczelTheorem.lean:205 
/-- Core bootstrap: continuous d'Alembert → C^n for all n. -/
private theorem dAlembert_contDiff_nat (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) :
    ∀ n : ℕ, ContDiff ℝ (n : ℕ∞) H := by
  obtain ⟨δ, _, hδ_ne⟩ := exists_integral_ne_zero H h_one h_cont
  have h_rep := representation_formula H h_cont h_dAl hδ_ne
  intro n; induction n with
  | zero => exact contDiff_zero.mpr h_cont
  | succ n ih =>
    have h_phi := phi_contDiff_succ H h_cont ih
    have h1 : ContDiff ℝ ((n + 1 : ℕ) : ℕ∞) (fun t => Phi H (t + δ)) :=
      h_phi.comp (contDiff_id.add contDiff_const)
    have h2 : ContDiff ℝ ((n + 1 : ℕ) : ℕ∞) (fun t => Phi H (t - δ)) :=
      h_phi.comp (contDiff_id.sub contDiff_const)
    have h4 : ContDiff ℝ ((n + 1 : ℕ) : ℕ∞)
        (fun t => (Phi H (t + δ) - Phi H (t - δ)) / (2 * Phi H δ)) :=
      (h1.sub h2).div_const _
    exact (funext h_rep) ▸ h4
THEOREM h_aczel_classification_proved · IndisputableMonolith/Cost/AczelTheorem.lean
h_aczel_classification_proved · IndisputableMonolith/Cost/AczelTheorem.lean:450 
/-- **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.
THEOREM h_aczel_classification_proved · IndisputableMonolith/Cost/AczelTheorem.lean
h_aczel_classification_proved · IndisputableMonolith/Cost/AczelTheorem.lean:450 
/-- **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

Not claiming the Aczél theorem is a physical law or an empirical observation. Not claiming the proof derives the specific value of λ in the cosine or hyperbolic cosine solutions. Not claiming the Aczél theorem alone derives the cost function or any 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/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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND