Foundation Dalembert Wlogalpha One Wlog Alpha Eq One

The coordinate rescaling

The declaration wlog_alpha_eq_one settles a question about the cost, the price a recognition event pays in the framework's ledger, a discrete record of events. After calibration fixes a constant, the cost functions form a family F_α(x) = (1/α²)(cosh(α ln x) − 1), with α ≥ 1. The theorem proves that every member of this family is the canonical cost J(x) = (x + x⁻¹)/2 − 1, just viewed through a rescaling of the coordinate x. Raising x to the power α is a group automorphism of the positive reals under multiplication, so it preserves the multiplicative structure; α only reparametrizes the coordinate, it does not create a structurally new cost.

Setting α = 1 recovers J exactly, and the unit-curvature condition, the second derivative at zero equaling 1, holds for every α ≠ 0. The theorem bundles four facts: the rescaling identity F_α(x) = (1/α²)J(x^α), the recovery F₁(x) = J(x), the automorphism property (xy)^α = x^αy^α, and the calibration invariance. Together they mean the parameter α is a gauge choice, not a physical knob. The proof is a machine-checked theorem in the framework's library of formal theorems, derived from the earlier result that any cost satisfying the five plain conditions must equal J.

What the declaration does not claim is just as important. It does not say that α is meaningless; it says α is a coordinate rescaling, so any property that is invariant under such rescalings is the same for all α. It does not claim that the cost function is unique in the sense that no other function could serve; it claims that within the calibrated family, all members are the canonical J up to rescaling. It also does not claim that the rescaling map is an automorphism of any larger structure, only of the multiplicative group of positive reals. The theorem is a statement about the cost family, not about the physical meaning of α itself.

The consequence for the framework is that the forcing chain, which derives the golden ratio, the eight-tick cycle, and three spatial dimensions from J, does not depend on which α one picks. The chain goes through for α = 1, and the wlog theorem says that is enough. A reader who wants to check the framework's claims can focus on the single canonical cost J, knowing that the α-parameterized family adds no new structure. That is the practical payoff: one function to study, not a family.

/-- **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'⟩

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

The parameter α is physically meaningless; it is a coordinate rescaling, not a physical degree of freedom. The cost function is unique in the sense that no other function could serve; it is unique up to coordinate rescaling within the calibrated family. The rescaling map is an automorphism of any structure beyond the multiplicative group of positive reals.

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: