Pith. sign in
module module moderate

IndisputableMonolith.Foundation.AlphaCoordinateFixation

show as:
view Lean formalization →

Module pinning the free scale α in the calibrated d'Alembert cost family to α=1 by matching the fourth-order jet of the log-coordinate cost. Researchers citing uniqueness of J(x)=(x+x^{-1})/2-1 among F_α will use the high-calibration pin and the recovery of J. The argument computes successive derivatives of CostAlphaLog through order four, then equates the jet at the origin under a high-calibration hypothesis.

claimAfter unit calibration the cost family is $F_\alpha(x)=\alpha^{-2}(\cosh(\alpha\ln x)-1)$ for $\alpha\ge 1$. In the log coordinate $t=\ln x$, write $C_\alpha(t)$ for the corresponding cost. If $C_\alpha$ is high-calibrated (its fourth-order jet at $t=0$ matches the canonical jet), then $\alpha=1$ and $F_\alpha$ reduces to the unique $J$-cost $J(x)=\frac{x+x^{-1}}{2}-1$.

background

Upstream WLOG α=1 records the calibrated family after κ(F)=1 forces c=2α²:

F_α(x)=(1/α²)(cosh(α ln x)−1), α≥1,

equivalently F_α(x)=(1/α²)·J(x^α) with J(x)=(x+x^{-1})/2−1 (the T5 cost). The residual freedom is the coordinate scale α.

This module works in the logarithmic chart t=ln x. CostAlphaLog α is the pullback of F_α to that chart. Its first derivative is sinh(αt)/α; higher derivatives are computed through order four and evaluated at the origin. High calibration means the fourth-order jet of CostAlphaLog α at t=0 matches a fixed reference jet (the jet of the α=1 cost). The Cost import supplies the ambient J-cost and calculus infrastructure.

proof idea

Not a single theorem: a short calculus ladder plus two pin lemmas. Successive HasDerivAt lemmas give closed forms for the first through fourth derivatives of CostAlphaLog; companion equalities record the simplified expressions. The fourth derivative is evaluated at zero. IsHighCalibratedLog packages the jet-matching hypothesis; costAlphaLog_high_calibrated_iff relates that predicate to a numerical constraint on α. alpha_pin_under_high_calibration discharges α=1 from the constraint; alpha_pinned_to_one_implies_J substitutes back into the WLOG family and recovers J.

why it matters in Recognition Science

Closes the residual α-freedom left by the WLOG coordinate-rescaling proposition, so the calibrated d'Alembert family collapses to the single T5 cost J(x)=cosh(log x)−1. That uniqueness is the Recognition Composition Law cost used throughout the forcing chain. The graph snapshot lists no external used_by edges; the in-module capstone alpha_pinned_to_one_implies_J is the bridge that later foundation modules cite when they need “the” cost rather than the α-family. Does not itself touch T6–T8 (phi, eight-tick, D=3) or the α_EM band.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (16)