canonicalQuadraticAlongLine
plain-language theorem explainer
Canonical quadratic piece of the nonlinear Regge action along the conformal ray through a vertex potential ξ. Cited wherever the action is split into quadratic model plus remainder for the nonlinear Hessian identity. Defined as one-half the Hessian quadratic form of the canonical Regge Hessian on the line potential at scale t.
Claim. Given an incidence-consistent 3D triangulation $K$ and a vertex potential $\xi$, the canonical quadratic term along the conformal line is $\tfrac12\,Q_{H(K)}(\ell_\xi(t))$, where $H(K)$ is the canonical Regge Hessian of $K$ and $\ell_\xi(t)$ is the line potential through $\xi$ at real parameter $t$.
background
This module isolates the hard analytic step for the full nonlinear Regge action: the second directional derivative at the flat potential must recover the canonical incidence Hessian. Once that identity is in hand, the existing second-variation input package follows at once.
The setup uses a 3D triangulation $K$ with an incidence-consistency hypothesis, vertex potentials on $K$, and the canonical Regge Hessian built from that incidence data. The Hessian quadratic form $Q_H$ is the associated bilinear energy. A conformal line through $\xi$ is the one-parameter family of potentials obtained by scaling $\xi$ (the line potential at $t$).
The companion remainder along the same line is the action minus this quadratic model (and the constant flat value). Downstream lemmas treat the pair (quadratic, remainder) as the exact algebraic split of the restricted action.
proof idea
Pure definition, not a proof. The body is the scalar $\tfrac12$ times the Hessian quadratic form of canonicalReggeHessian K hK evaluated on the line potential through $\xi$ at $t$. No lemmas are applied; later differentiability and derivative facts unfold this expression and differentiate under the quadratic form.
why it matters
This is the explicit quadratic model in the one-dimensional split of the nonlinear Regge action along every conformal line. The split theorem writes the restricted action as flat value plus this quadratic plus the canonical remainder; after that reduction, only the second variation of the remainder remains.
It feeds the second-derivative identity that the quadratic line has exactly the canonical Regge Hessian as its second directional derivative at zero, the first-derivative formula along the line, and the tangency targets that compare the true action derivative to the derivative of this quadratic. Those facts close the chain-rule calculation that the nonlinear directional Hessian equals the canonical incidence Hessian (the module's endpoint).
In the broader Recognition geometry stack this is scaffolding for discrete curvature matching continuum second variation, not a new physical postulate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.