tendsto_centeredSecondDifference_of_contDiffAt
plain-language theorem explainer
If a real function is twice continuously differentiable at the origin, its centered second difference quotient converges on the punctured neighborhood to the second derivative at zero. Analysts in the Regge TT continuum-symbol program cite this as the reusable local bridge from discrete second differences to S''(0). The proof is one L'Hôpital pass on a 0/0 form, then slope averaging of the first derivative.
Claim. Let $f:\mathbb{R}\to\mathbb{R}$ be $C^2$ at $0$. Then $$\frac{f(t)-2f(0)+f(-t)}{t^2}\to f''(0)$$ along the punctured neighborhood filter of $0$ (i.e., $t\to 0$ with $t\neq 0$).
background
This module is Gate A1 of the Normalization-Gated Schläfli Two-Jet protocol in the Regge TT continuum-symbol campaign. It establishes local smoothness of the plane-wave Regge action profile $S(t)$ at the flat Freudenthal background and identifies the fixed-$N$ TT Bloch symbol with a multiple of $S''(0)$.
The centered second difference is the discrete two-jet used by the preflight second-difference functional. The only analytic input needed here is local $C^2$ at the origin: existence of a neighborhood on which $f$ is twice continuously differentiable, so that $\mathrm{deriv},f$ is differentiable at $0$ with derivative $f''(0)$.
The module deliberately avoids the global continuum-limit lemma that demands $C^4$ on all of $\mathbb{R}$, a hypothesis false for the plane-wave family. The local bridge is therefore the approved route from discrete second differences to the second variation.
proof idea
Extract a symmetric open ball on which $f$ is $C^2$. Then $\mathrm{deriv},f$ is $C^1$ on that ball, hence differentiable at $0$ with derivative $D:=(\mathrm{deriv},(\mathrm{deriv},f))(0)$.
On the punctured neighborhood, both numerator $g(t)=f(t)-2f(0)+f(-t)$ and denominator $t^2$ tend to $0$, and both admit derivatives: $g'(t)=f'(t)-f'(-t)$ and $(t^2)'=2t\neq 0$. One application of L'Hôpital for $0/0$ forms on the punctured filter reduces the quotient to $(f'(t)-f'(-t))/(2t)$.
That expression is the average of the two slope quotients of $\mathrm{deriv},f$ at $0$ and $-t$. Each slope tends to $D$ by the characterization of the derivative via slopes, so their average tends to $D$, which equals the second iterated derivative of $f$ at $0$.
why it matters
This is item (d) of the module: the reusable local bridge. Downstream, the headline existence theorem applies it to the plane-wave action profile $S$ to conclude that the fixed-$N$ TT Bloch symbol exists and equals $(2/N^3)\cdot S''(0)$, with exact bookkeeping and no stray factor of $1/2$.
It is also reused in the continuum-limit lane to obtain the local cosine two-jet $(\cos(qa)-1)/q^2\to -a^2/2$, feeding higher-order symbol analysis.
Within Recognition Science gravity, this closes the analytic step that turns discrete Regge second differences into a continuum second variation without invoking a global $C^4$ hypothesis forbidden by the panel protocol. It does not yet evaluate the symbol; it only identifies the limit with $S''(0)$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.