Foundation Dalembert Wlogalpha One Cost Alpha Log Unit Curvature

Unit curvature and the rescaling theorem

In the Recognition Science framework, a cost is a function that assigns a nonnegative penalty to a recognition event, a discrete record of something being recognized. The framework's central object is the canonical cost J(x) = (x + 1/x)/2 − 1, which is forced by five plain conditions. But before that uniqueness is established, one must ask: could a parameter α produce genuinely different costs? The declaration costAlphaLog_unit_curvature answers no, and it does so through a property called unit curvature.

In log coordinates, where t = ln x, the α-parameterized cost is G_α(t) = (1/α²)(cosh(αt) − 1). Its second derivative at t = 0 is exactly 1 for every nonzero α. This is the unit-curvature condition: the cost's curvature at the origin, in these coordinates, is always one, regardless of α. The theorem costAlphaLog_unit_curvature proves this in the machine-checked library: deriv (deriv (CostAlphaLog α)) 0 = 1, for any α ≠ 0.

The consequence is a rescaling identity. The theorem cost_alpha_rescaling shows that F_α(x) = (1/α²) · J(x^α). The map x ↦ x^α is a group automorphism of the positive reals under multiplication, so α merely reparametrizes the coordinate, not the cost's structure. Setting α = 1 recovers J exactly, as cost_alpha_one_eq_jcost proves. The combined theorem wlog_alpha_eq_one states all four components at once: the rescaling identity, the α = 1 recovery, the group automorphism property, and the unit curvature. In plain language: every calibrated cost F_α is the canonical cost J under a coordinate rescaling, so α introduces no structurally new cost function.

What this does not claim: it does not say that α is physically meaningless, only that it does not change the cost's form. It does not prove that J is the unique cost; that is a separate theorem requiring the five conditions. And it does not assert that unit curvature alone forces J; the curvature condition is necessary but not sufficient without the other axioms. The theorem is a structural simplification, not a derivation of the cost itself.

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

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

/-- **WLOG α = 1**: Every calibrated cost F_α is the canonical cost J under
    coordinate rescaling. The parameter α does not introduce a structurally
    new cost function.

    Components:
    1. Rescaling identity: F_α(x) = (1/α²) · J(x^α)
    2. Recovery: F₁(x) = J(x)
    3. Group automorphism: (xy)^α = x^α · y^α
    4. Calibration invariance: G_α''(0) = 1 -/
theorem wlog_alpha_eq_one (α : ℝ) (hα : 0 < α) :
    (∀ x : ℝ, 0 < x → CostAlpha α x = (1 / α ^ 2) * Jcost (x ^ α))
    ∧ (∀ x : ℝ, 0 < x → CostAlpha 1 x = Jcost x)
    ∧ (∀ x y : ℝ, 0 < x → 0 < y → (x * y) ^ α = x ^ α * y ^ α)
    ∧ deriv (deriv (CostAlphaLog α)) 0 = 1 :=
  ⟨fun x hx => cost_alpha_rescaling α x hx,
   fun x hx => cost_alpha_one_eq_jcost x hx,
   fun _ _ hx hy => rpow_mul_hom' α hx hy,
   costAlphaLog_unit_curvature α hα.ne'⟩

What this page does not claim

The theorem does not prove that J is the unique cost function satisfying the framework's axioms. The theorem does not assign physical meaning to the parameter α. The unit-curvature condition alone does not force the canonical cost; it is one component of a larger derivation.

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: