slope_average_eq
plain-language theorem explainer
The odd difference quotient of a real map g equals the average of the two slope quotients of g from the origin out to t and to −t, for every nonzero t. Analysts running the local L'Hôpital route for centered second differences cite this identity as the algebraic hinge. The proof is a short field rewrite of the slope definition with cancellation and commutativity of multiplication.
Claim. For every $g:\mathbb{R}\to\mathbb{R}$ and every $t\neq 0$, $$\frac{g(t)-g(-t)}{2t}=\frac{1}{2}\Bigl(\frac{g(t)-g(0)}{t}+\frac{g(-t)-g(0)}{-t}\Bigr).$$
background
This module is Gate A1 of the panel-locked "Normalization-Gated Schläfli Two-Jet" protocol in the Regge TT continuum-symbol campaign. It builds a plane-wave family of tetrahedron edge data, proves the nonlinear Regge action profile $S(t)$ is $C^n$ at $t=0$ for every finite $n$, and then extracts the fixed-$N$ TT Bloch symbol as $S''(0)$.
The slope of $g$ from $0$ to $t$ is the ordinary difference quotient $(g(t)-g(0))/t$. The centered second-difference bridge later needs the odd combination $(g(t)-g(-t))/(2t)$ rewritten as the average of the two slopes of $g$ (or of $\mathrm{deriv},f$) at the origin. That rewrite is purely algebraic and holds for any real $g$ and any $t\neq 0$; no continuity is required.
Upstream continuum-limit machinery (global $C^4$ lattice-Laplacian error bounds) is deliberately not used here. The panel forbids that global route for this family, so the local L'Hôpital path needs only this identity plus Mathlib slope-tendsto facts.
proof idea
Term-mode field algebra. Unfold the slope definition on both summands, cancel the two $g(0)$ subtractions, rewrite the negative-direction quotient via $\mathrm{div_neg}$, convert the resulting sum of quotients into a single difference of quotients over a common denominator, cancel the residual $g(0)$ terms, and finish by $\mathrm{div_div}$ together with $t\cdot 2=2\cdot t$. No analysis lemmas fire; the hypothesis $t\neq 0$ only keeps the divisions defined.
why it matters
Parent consumer is tendsto_centeredSecondDifference_of_contDiffAt, the reusable local bridge: if $f$ is $C^2$ at $0$, the centered second difference $(f(t)-2f(0)+f(-t))/t^2$ tends to $\mathrm{iteratedDeriv},2,f,0$ on the punctured neighborhood of $0$. One L'Hôpital pass reduces that limit to $(f'(t)-f'(-t))/(2t)\to f''(0)$; the present identity rewrites the left-hand side as the average of the two slope quotients of $\mathrm{deriv},f$, which then converges by the Mathlib slope characterization of derivatives.
That bridge is the analytic step that turns $C^2$ regularity of the plane-wave Regge action profile into existence of the fixed-$N$ TT Bloch symbol $S''(0)$. It closes Crux-1(c) Gate A1 without invoking the panel-forbidden global continuum-limit lemma (which demands global $C^4$ and is false for this family). In the broader Recognition gravity stack this is the local second-variation gate for the discrete Regge action, not a continuum Einstein-Hilbert derivation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.