deriv2_comp_mul_left_at_zero
plain-language theorem explainer
The second derivative at the origin of a left-scaled map t ↦ g(m t) equals m² times g''(0), whenever g' is differentiable. Pure real calculus: each differentiation pulls out one factor of m. Cited when transporting log-curvature (calibration) of a recognition cost under the gauge x ↦ x^a, notably in the four-law completeness argument that discharges the analytic blocker T1′.
Claim. Let $g:\mathbb{R}\to\mathbb{R}$ be such that $g'$ is differentiable on $\mathbb{R}$, and let $m\in\mathbb{R}$. Then $$\frac{d^2}{ds^2}\Big|_{s=0}\, g(m s) = m^2\, g''(0).$$
background
In the Primitive Recognition Calculus, native costs obey four algebraic laws (reciprocity, normalization, composition, continuity). Passing to $G F = F\circ\exp$ and the shifted cost $H F = G F + 1$ converts the Recognition Composition Law into d'Alembert's functional equation $H(xy)+H(x/y)=2 H(x)H(y)$. Under an Aczél smoothness package, continuous d'Alembert solutions are $C^\infty$, so second derivatives at the origin are well-defined.
Calibration means unit positive log-curvature: $\kappa = (G F)''(0)=1$. Gauge substitutions of the form $x\mapsto x^a$ rescale the argument of $G F$ by a constant factor. Tracking how $\kappa$ transforms under that rescaling is exactly a second-derivative chain-rule computation at zero, which this lemma isolates.
The lemma itself is domain-agnostic real analysis: no Recognition axioms enter the statement. It is placed here because the four-law completeness proof needs a named, reusable identity for $(t\mapsto g(m t))''(0)=m^2 g''(0)$.
proof idea
Two applications of the Mathlib chain rule for left multiplication, then algebra.
First, deriv_comp_mul_left gives $\partial_s g(m s)=m, g'(m s)$ pointwise; rewrite the outer derivative with that identity. Differentiability of $s\mapsto g'(m s)$ at $0$ follows from differentiability of $g'$ and composition. Pull the constant $m$ out of the outer derivative via deriv_const_mul. Apply deriv_comp_mul_left again to $g'$ to obtain $\partial_s g'(m s)|_{s=0}=m, g''(0)$. Simplify $m\cdot 0=0$ and finish with ring: $m\cdot(m, g''(0))=m^2 g''(0)$.
why it matters
Feeds directly into prc_four_law_completeness_target, which discharges the isolated analytic blocker T1′: every positive-log-curvature four-law solution is gauge-equivalent to a calibrated one. The parent proof sets $\kappa=(G F)''(0)>0$, takes $c=\sqrt{\kappa}$, and substitutes $x\mapsto x^{1/c}$. That sends $G F$ to $t\mapsto G F(t/c)$, whose second derivative at the origin is $c^{-2}\kappa=1$ precisely by this lemma. Calibration then holds, so the conditional cost_laws_complete_of_calibratable upgrades to the unconditional prc_four_law_completeness.
In the broader forcing chain this closes the analytic gap between the algebraic four laws and uniqueness of the native $J$-cost (T5: $J(x)=(x+x^{-1})/2-1$), via the d'Alembert form of the Recognition Composition Law and Aczél smoothness. Without the $m^2$ transport, gauge equivalence to unit curvature would remain a handwave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.