Foundation Dalembert Wlogalpha One Cost Alpha Rescaling

The rescaling identity

The cost function J(x) = (x + 1/x)/2 − 1 measures the price of a recognition event when the underlying scale is fixed. A natural question is whether allowing a rescaling parameter α produces genuinely new costs. The answer, proved in the machine-checked library of formal theorems, is no: the α-parameterized family F_α(x) = (1/α²)(cosh(α ln x) − 1) is exactly the canonical cost J evaluated at x^α, scaled by 1/α². The identity F_α(x) = (1/α²) · J(x^α) holds for every positive x and every α ≥ 1.

The reason is that the map x ↦ x^α is a group automorphism of the positive reals under multiplication: it preserves products, the identity, and inverses. It therefore merely reparametrises the multiplicative coordinate, like changing from meters to feet. Setting α = 1 recovers J exactly, and the unit-curvature condition G_α″(0) = 1 holds for every α ≠ 0. The parameter does not introduce a structurally new cost function; it only changes the ruler.

In Recognition Science, this result is the coordinate-rescaling proposition. It establishes that the five conditions forcing J also force the entire α-family: once calibration fixes the constant c = 2α², the solution is unique up to this coordinate change. The theorem cost_alpha_rescaling in the library's WLOGAlphaOne module states the identity in full generality, and the companion theorem wlog_alpha_eq_one packages it with the recovery, the group automorphism, and the calibration invariance.

The practical consequence is a reduction: any statement about a calibrated cost can be checked at α = 1, and the result transfers to every α by the rescaling. This is what "without loss of generality" means here, and it is a proved equivalence, not a heuristic. The framework's forcing chain, which derives the golden ratio and the eight-tick cycle from J, therefore does not depend on which α one starts from.

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

/-- **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 claim that α itself is derived or forced; it remains a free parameter. The theorem does not claim that the cost function is unique without the calibration condition. The theorem does not claim that the framework derives the fine-structure 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/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: