pith. machine review for the scientific record. sign in
def definition def or abbrev high

CostAlphaLog

show as:
view Lean formalization →

CostAlphaLog supplies the explicit α-parameterized cost G_α(t) = (1/α²)(cosh(α t) − 1) in logarithmic coordinates. Researchers working on the bilinear family and coordinate fixation cite it when isolating the J-cost under fourth-derivative calibration. The definition is obtained by direct substitution of the group automorphism x ↦ x^α into the base J-cost expression.

claimThe α-parameterized cost in log coordinates is the function $G_α(t) = (1/α²)(cosh(α t) − 1)$ for real α ≠ 0 and t.

background

The module establishes the WLOG α = 1 proposition after the calibration κ(F) = 1 forces c = 2α². The calibrated family is written F_α(x) = (1/α²)(cosh(α ln x) − 1) for α ≥ 1, which is equivalent to (1/α²) · J(x^α) where J(x) = (x + x⁻¹)/2 − 1. The map x ↦ x^α is a group automorphism of (ℝ₊, ·), so α merely reparametrises the multiplicative coordinate and the unit-curvature condition G_α''(0) = 1 holds uniformly.

proof idea

One-line definition that transcribes the rescaled J-cost into the logarithmic variable t = ln x. It relies on the multiplicativity theorem for J-automorphisms and the cost definition induced by a multiplicative recognizer.

why it matters in Recognition Science

The definition is the central object fed into AlphaCoordinateFixationCert and the α-pin theorem, which use the fourth-derivative calibration G^(4)(0) = α² to force α = 1 and isolate J. It completes the coordinate-rescaling step of the WLOG α = 1 proposition. The construction sits inside the forcing chain at the J-uniqueness stage (T5) and supplies the concrete family whose rigidity is later used to recover D = 3.

scope and limits

formal statement (Lean)

  29def CostAlphaLog (α t : ℝ) : ℝ :=

proof body

Definition body.

  30  (1 / α ^ 2) * (cosh (α * t) - 1)
  31
  32/-- The α-parameterized cost in multiplicative coordinates:
  33    F_α(x) = (1/α²)(cosh(α ln x) − 1). -/

used by (18)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (3)

Lean names referenced from this declaration's body.