differentiableAt_eventually_of_contDiffAt_top
plain-language theorem explainer
Infinite differentiability of a real scalar map at a point forces ordinary differentiability at every nearby point. Workers on the nonlinear Regge second-variation chain cite it to discharge the eventual DifferentiableAt hypotheses along edge-length lines through a flat configuration. The argument is a short localization: ContDiffAt top yields a C^1 neighborhood, then open-set filter_upwards hands DifferentiableAt at each interior point.
Claim. Let $f:\mathbb{R}\to\mathbb{R}$ and $x\in\mathbb{R}$. If $f$ is $C^\infty$ at $x$, then there is a neighborhood of $x$ on which $f$ is differentiable at every point: $\forall^{\mathrm{eventually}} y\text{ near }x$, $f$ is differentiable at $y$.
background
The ambient module isolates the remaining hard step of the nonlinear Regge action: the second directional derivative of the action at a flat edge-length configuration must equal the canonical incidence Hessian. Once that identity is in hand, the existing second-variation input package follows at once.
The present lemma is pure real calculus infrastructure. ContDiffAt with order $\top$ means the map is infinitely differentiable at the base point (all derivatives of all orders exist in a neighborhood and are continuous at the point in the usual Mathlib sense). DifferentiableAt is the first-order Fréchet condition at a single point. The filter statement "eventually in nhds $x$" means the property holds on some open neighborhood of $x$.
No Recognition-specific geometry enters here; the lemma only supplies the analytic glue that later theorems apply to action, hinge-deficit, and local dihedral-angle restrictions along lines through a flat triangulation.
proof idea
Term-mode localization. From ContDiffAt of order $\top$, extract ContDiffOn of order $1$ on a set $u\in\mathrm{nhds},x$ (the order-$1$ truncation is admissible because $1\le\top$). Realize $u$ as containing an open neighborhood $v\ni x$. Filter-upwards over membership in $v$: for each such $y$, $u$ remains a neighborhood of $y$ by openness, so the ContDiffOn restriction yields DifferentiableOn of order $1$ on $u$, hence DifferentiableAt at $y$.
why it matters
Three downstream targets invoke this lemma almost verbatim: eventual differentiability of the action along lines through a flat configuration, the same for hinge deficits, and the same for local dihedral angles. Those targets are the analytic hypotheses needed before one can form first and second directional derivatives of the nonlinear Regge action and compare them to the canonical quadratic form on the incidence complex.
In the Recognition geometry stack this sits inside the nonlinear Hessian proof interface: the second directional derivative at the flat potential must match the incidence Hessian, after which the second-variation input package is immediate. The lemma itself is not a physics claim; it is the calculus step that lets $C^\infty$ line restrictions (available for the geometric quantities built from dihedral angles and edge lengths) produce the DifferentiableAt hypotheses required by the chain-rule calculation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.