hasDerivAt_alpha_mul
plain-language theorem explainer
The lemma states that the map x ↦ α x is differentiable at every real t with derivative exactly α. It is invoked inside the WLOG α=1 reduction when differentiating the rescaled cost CostAlphaLog and the normalized sinh term. The proof is a short tactic sequence that obtains the derivative of x ↦ x * α from the identity map, then reorders factors via commutativity.
Claim. The function $f(x) = α x$ satisfies $f'(t) = α$ for every real number $t$.
background
The module establishes the WLOG α=1 proposition: after the calibration κ(F)=1 forces c=2α², the family F_α(x)=(1/α²)(cosh(α ln x)−1) for α≥1 is shown to be a reparametrization of the J-cost via the multiplicative automorphism x↦x^α. CostAlpha is defined by CostAlpha α x := CostAlphaLog α (log x), and the core identity cosh(α log x)−1 = J(x^α) recovers the base J-cost when α=1. The upstream result from PrimitiveDistinction supplies the seven-axiom foundation that yields the four structural conditions plus definitional facts used throughout the calibration argument.
proof idea
The tactic first constructs HasDerivAt (fun x => x * α) α t by applying mul_const to hasDerivAt_id t. It then rewrites the function expression to the desired order α * x by a single rwa that invokes funext and mul_comm.
why it matters
The lemma supplies the chain-rule step needed for hasDerivAt_costAlphaLog and hasDerivAt_sinhDivAlpha, which together verify that the unit-curvature condition G_α''(0)=1 holds for every α. This closes the calibration-invariance argument in the module and justifies the reduction to the α=1 case that recovers J exactly, consistent with T5 J-uniqueness and the eight-tick octave structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.