Foundation Dalembert Wlogalpha One Cosh Log Eq Jcost Rpow

The rescaling identity

The declaration cosh_log_eq_jcost_rpow proves a specific identity about the framework's cost function, which measures the price of recognizing one state from another. In plain terms, it shows that for any positive number x and any real parameter α, the expression cosh(α · ln x) − 1 equals J(x^α), where J is the canonical cost function J(y) = (y + y⁻¹)/2 − 1. This identity connects the hyperbolic cosine, a standard mathematical function, to the framework's central cost object.

The practical consequence is a rescaling property. The framework considers a family of cost functions F_α(x) = (1/α²)(cosh(α ln x) − 1), parameterized by α. The identity proves that each such F_α is just the canonical cost J applied to x^α, scaled by 1/α². Since raising x to the power α is a coordinate change on the positive real numbers, the parameter α does not create a new kind of cost; it only reparametrizes the same underlying structure. Setting α = 1 recovers J exactly, and the unit-curvature condition, a calibration requirement, holds for every α.

This is a theorem in the machine-checked library of formal theorems, meaning the proof is verified by a computer. It is part of a larger chain showing that the canonical cost function J is unique under certain axioms. The rescaling identity is a technical lemma within that chain, not a standalone physical prediction.

What the declaration does not claim is equally important. It does not assert that α has physical meaning or that any particular value of α is preferred. It does not derive the canonical cost function J from scratch; that uniqueness is established elsewhere. It only shows that within the parameterized family, all members are equivalent up to rescaling, so the framework can focus on α = 1 without loss of generality.

/-- Core identity: cosh(α log x) − 1 = J(x^α) for x > 0.
    Proof uses x^α = exp(α log x), then Jcost ∘ exp = cosh − 1. -/
theorem cosh_log_eq_jcost_rpow (α x : ℝ) (hx : 0 < x) :
    cosh (α * log x) - 1 = Jcost (x ^ α) := by
  have h : x ^ α = exp (α * log x) := by
    rw [rpow_def_of_pos hx, mul_comm]
  rw [h, ← Jcost_exp_cosh]

/-- **Rescaling Identity**: F_α(x) = (1/α²) · J(x^α). -/
theorem cost_alpha_rescaling (α x : ℝ) (hx : 0 < x) :
    CostAlpha α x = (1 / α ^ 2) * Jcost (x ^ α) := by
  unfold CostAlpha CostAlphaLog
  congr 1
  exact cosh_log_eq_jcost_rpow α x hx

/-- Setting α = 1 gives F₁(x) = J(x) for x > 0. -/
theorem cost_alpha_one_eq_jcost (x : ℝ) (hx : 0 < x) :
    CostAlpha 1 x = Jcost x := by
  rw [cost_alpha_rescaling 1 x hx]
  simp [rpow_one]

/-- **Calibration Invariance**: G_α''(0) = 1 for every α ≠ 0.
    The unit-curvature condition is independent of the rescaling parameter. -/
theorem costAlphaLog_unit_curvature (α : ℝ) (hα : α ≠ 0) :
    deriv (deriv (CostAlphaLog α)) 0 = 1 := by
  rw [deriv_costAlphaLog_eq α hα, (hasDerivAt_sinhDivAlpha α hα 0).deriv,
      mul_zero, cosh_zero]

What this page does not claim

This declaration does not prove the uniqueness of the canonical cost function J. It does not assign physical meaning to the parameter α. It does not claim that the identity holds for non-positive x.

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/Foundation/DAlembert/WLOGAlphaOne.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: