hasDerivAt_sin_const_mul
plain-language theorem explainer
The map s ↦ sin(c s) is differentiable at every real t, with derivative c cos(c t). Analysts on the Freudenthal continuum-energy panel cite it to justify the first gradient component of the fixed witness field sin(2πx) and to feed the closed-form interval integral of cos²(2πx). The proof is a one-line chain-rule assembly: scale the identity map by c, then apply the library sine rule.
Claim. For all real $c$ and $t$, the function $s \mapsto \sin(c s)$ is differentiable at $t$ and its derivative there equals $c\,\cos(c t)$.
background
This module develops the action-level continuum limit of the frozen quadratic Regge-Hessian energy on the canonical periodic Freudenthal family (QG Phase 2b, panel-locked Test G stage 2). The fixed nonconstant C² witness is $f(x,y,z)=\sin(2\pi x)$, sampled onto the side-$N$ lattice. Independently of the lattice, the continuum target is $\int_{[0,1]^3}\langle\nabla f,A_0\nabla f\rangle=A_0[0,0]\cdot 2\pi^2$, which reduces to an interval integral of $(2\pi\cos(2\pi t))^2$ because the energy density depends only on the first coordinate.
Mathlib's HasDerivAt is the pointwise Fréchet (here ordinary) derivative predicate on $\mathbb{R}$. The continuum target and the witness gradient both need the elementary fact that sine of a constant multiple is differentiable, with the expected chain-rule formula. That is exactly what this lemma records, before specializing $c=2\pi$ on the section $s\mapsto f(s,0,0)$.
proof idea
Term-mode chain rule. Start from differentiability of the identity map at $t$, scale by the constant $c$ (product rule for constant multiplication), then apply the library rule for the derivative of sine. A final simpa aligns the resulting derivative expression with $c\cos(c t)$. No case splits and no analysis beyond the standard real calculus lemmas.
why it matters
Two immediate parents sit in the same module. witnessField_section_hasDerivAt specializes this lemma at $c=2\pi$ to prove that the first gradient component of the witness field along the $x$-axis is the honest derivative $2\pi\cos(2\pi t)$. integral_cos_sq_two_pi uses a related antiderivative whose derivative identity is the same chain-rule pattern, evaluating $\int_0^1\cos^2(2\pi x),dx=1/2$.
Together those facts make continuumTarget a fully Lean-justified positive real (via continuumTarget_pos and nonconstancy of the witness), independent of any lattice computation. That target is the comparison value in the panel-locked stage-2 rate bound $|E_N-\int\langle\nabla f,A_0\nabla f\rangle|\le C/N$ with explicit $C=A_0[0,0]\cdot(2\pi)^4/24$. The module scope stays partial: the pillar-2 path-sum flag remains red pending refinement-indexed measure-weighted sums over triangulation classes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.