CanonicalRemainderLineDifferentiabilityTarget
plain-language theorem explainer
Names the joint line-differentiability hypothesis needed to pass from the nonlinear Regge action to its canonical remainder along conformal rays. For every vertex potential and every real parameter, both the action restricted to that ray and the canonical quadratic form on the ray must be differentiable. Downstream lemmas use it to obtain the remainder derivative identity and to close the second-variation-zero argument once the nonlinear Hessian theorem is in hand. The quadratic half is elementary; the content is the action half.
Claim. For a finite incidence-consistent 3D Regge triangulation $K$, the following holds: for every vertex conformal potential $\xi$ and every $t \in \mathbb{R}$, the nonlinear Regge action restricted to the conformal line through the flat potential in direction $\xi$ is differentiable at $t$, and the canonical quadratic form (half the incidence Hessian evaluated on that line potential) is likewise differentiable at $t$.
background
The module isolates the remaining hard step for the full nonlinear Regge Hessian: the second directional derivative of the Regge action at the flat potential must equal the canonical incidence Hessian. Once that identity is available, the existing second-variation input package follows at once.
A Triangulation3D is a finite abstract 3D Regge complex (vertices, edges, tets with incidence and nondegenerate squared-edge data). IncidenceConsistent is the structural hypothesis on that incidence. Vertex conformal potentials are real assignments to vertices. The action along a line is the nonlinear Regge action evaluated on the one-parameter family of potentials obtained by scaling a fixed direction $\xi$ through the flat (zero) potential. The canonical quadratic along the same line is $\tfrac12$ times the quadratic form of the canonical Regge incidence Hessian on that line potential.
The remainder is action minus this quadratic. Differentiability of both pieces along every such ray is the minimal analytic input for a derivative identity on the remainder.
proof idea
Definitional, not a proved theorem. The body is the universal quantification over vertex potentials $\xi$ and real parameters $t$ of the conjunction of two DifferentiableAt statements: one for the action restricted to the conformal line, one for the canonical quadratic restricted to the same line. No tactics or lemmas are invoked; the Prop is the named target that smoothness lemmas are expected to discharge for the action factor (the quadratic factor is treated as elementary elsewhere).
why it matters
This target sits in the nonlinear Regge Hessian proof interface: it is the concrete differentiability gate between the action-line smoothness chain and the remainder calculus. Three local consumers depend on it. First, action-line differentiability implies this target, because the quadratic line is already known to be differentiable at every $t$. Second, assuming the target yields the canonical remainder derivative identity (pointwise in $\xi$ and $t$). Third, together with the nonlinear directional Hessian theorem, it feeds the lemma that the remainder has vanishing second variation, which is the endpoint needed so that the second directional derivative of the full nonlinear action matches the canonical incidence Hessian.
In the broader Recognition geometry stack this is scaffolding for discrete gravity / Regge calculus consistency in $D=3$ (forcing-chain T8), not a new physical hypothesis. It does not itself touch $\varphi$, the eight-tick octave, or the $\alpha$ band; it only clears an analytic step inside the Hessian identification.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.