hasDerivAt_alpha_mul
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not prove differentiability of any function other than linear multiplication by a constant.
- Does not impose α ≠ 0 or any sign restriction on α.
- Does not address higher-order derivatives or analyticity.
- Does not extend beyond the real numbers.
formal statement (Lean)
82private lemma hasDerivAt_alpha_mul (α t : ℝ) :
83 HasDerivAt (fun x => α * x) α t := by
proof body
Tactic-mode proof.
84 have h : HasDerivAt (fun x => x * α) α t := by
85 simpa using (hasDerivAt_id t).mul_const α
86 rwa [show (fun x : ℝ => x * α) = (fun x => α * x) from
87 funext fun x => mul_comm x α] at h
88