hingeLine_contDiffAt_zero
plain-language theorem explainer
Along any straight line of vertex potentials through the origin, each conformal hinge (edge) measure is infinitely differentiable at t = 0. Anyone building the nonlinear Regge second variation or Schläfli-type chain rules cites this. The proof is ContDiffAt composition: the line map is C^∞ by coordinate fun_prop, and the hinge measure is C^∞ at the zero potential by the existing smoothness lemma.
Claim. Let $K$ be an incidence-consistent 3D triangulation and $\xi$ a vertex potential. For every edge $e$, the map $t \mapsto \ell_e(\xi_t)$ is $C^\infty$ at $t = 0$, where $\xi_t$ is the straight-line path of potentials through $\xi$ and $\ell_e$ is the conformal hinge measure (edge length) $\sqrt{q_e}\,\exp((\xi_u+\xi_v)/2)$.
background
This module isolates the hard endpoint of the nonlinear Regge calculation: the second directional derivative of the action at the flat potential must match the canonical incidence Hessian. Once that identity is in hand, the existing second-variation input package follows at once.
The conformal hinge measure on a global edge $e$ with endpoints $u,v$ is the Regge edge length under the vertex-conformal ansatz: $\sqrt{q_e},\exp((\xi_u+\xi_v)/2)$, with $q_e$ the squared reference length from incidence consistency. The line potential $\xi_t$ is the affine path $t \mapsto t\cdot\xi$ in the space of vertex potentials; at $t=0$ it is the zero potential.
Infinite differentiability is stated in the Mathlib sense $\mathrm{ContDiffAt},\mathbb{R},\top$, so every order of derivative exists in a neighborhood of the evaluation point. The hinge map itself is already known to be $C^\infty$ at the zero potential; the present result only threads that fact along the line path.
proof idea
Three short steps. First, the line map $t \mapsto \mathrm{linePotential}(K,\xi,t)$ is $C^\infty$ at $0$: rewrite with $\mathrm{contDiffAt_pi}$ and apply $\mathrm{fun_prop}$ coordinatewise after unfolding the definition. Second, the hinge measure as a function of the potential is $C^\infty$ at $\mathrm{linePotential}(K,\xi,0)$; rewrite that basepoint via $\mathrm{linePotential_zero}$ and invoke $\mathrm{ReggeActionSmoothness.hingeMeasureUnderConformal_contDiffAt_zero}$ at order $\top$. Third, compose the two $\mathrm{ContDiffAt}$ facts with $\mathrm{ContDiffAt.comp}$ at $x=0$, then tidy the composition with $\mathrm{Function.comp_def}$.
why it matters
Without $C^\infty$ of each hinge length along the potential line, none of the second-derivative product and Schläfli chain rules can fire at the flat point. Downstream, $\mathrm{hingeDeficitLineDifferentiabilityNearZero_of_flatConfiguration}$ packages neighborhood differentiability of hinge deficits; $\mathrm{productRule_hasDerivAt_secondProduct}$ and $\mathrm{weightedDeficitDerivative_hasDerivAt_secondSchlaefliSum}$ turn that into HasDerivAt statements for the action derivative and the weighted deficit sum.
Those lemmas feed the nonlinear directional Hessian targets in this module (action-derivative linearization and first-order tangency near zero), which close the second chain-rule calculation announced in the module doc. The same smoothness is reused in the physical six-tet cubic Dirichlet instance for canonical periodic Freudenthal tori, where weighted deficit-derivative base sums must be differentiable at the flat configuration. In the broader RS geometry stack this is pure scaffolding for the discrete Einstein-Hilbert second variation, not a new physical postulate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.