DeficitSecondLineDifferentiabilityAtZeroTarget
plain-language theorem explainer
Named Prop asserting that, on any finite 3D Regge triangulation, the first derivative of each edge deficit angle along every conformal line of vertex potentials is differentiable at the flat point t=0. Downstream hinge packaging uses it as the deficit half of second-line differentiability. Pure definition: the body is the quantified DifferentiableAt statement, with no proof obligation here.
Claim. For a finite 3D Regge triangulation $K$, write $\delta_e(\phi)$ for the deficit angle at edge $e$ and $\phi_t = \phi_0 + t\xi$ for the conformal line through the flat potential in direction $\xi$. The target asserts: for every vertex potential $\xi$ and every edge $e$, the real map $t \mapsto \frac{d}{ds}\big|_{s=t}\delta_e(\phi_s)$ is differentiable at $t=0$.
background
The ambient setting is the nonlinear Regge Hessian interface: the second directional derivative of the Regge action at the flat conformal potential must match the canonical incidence Hessian. A finite 3D triangulation supplies abstract incidence (vertices, edges, tets) and nondegenerate squared-edge data on each tetrahedron. Vertex potentials are real assignments to vertices; the zero assignment is the flat background.
Along a fixed direction $\xi$, one forms the conformal line of potentials and differentiates geometric quantities in the line parameter $t$. The deficit-line derivative is the ordinary one-variable derivative of the edge deficit angle along that line. The present target asks only that this first derivative itself be differentiable at $t=0$, i.e. that a second derivative of the deficit along the line exist at the flat point.
The module isolates the remaining hard local calculation (cofactor and arccos derivatives near flatness). Once supplied, the existing second-variation input package follows immediately.
proof idea
No proof: this is a Prop-valued definition. The body is the universal statement that for every vertex potential $\xi$ and every edge index $e$, the map $t \mapsto \mathrm{deficitLineDeriv}(K,\xi,e,t)$ is differentiable at $0$ over $\mathbb{R}$. That map is itself defined as the one-variable derivative of the deficit angle along the conformal line through the flat potential.
why it matters
This is the deficit half of the second-line differentiability package needed for the nonlinear Regge Hessian. The immediate consumer is the hinge-level packaging theorem: given incidence consistency and this target, one obtains hinge-deficit second-line differentiability at zero by pairing the already-available hinge-length differentiability at zero with the deficit clause supplied here.
That packaging sits on the path to the module's endpoint: the second directional derivative of the full nonlinear Regge action at the flat potential equals the canonical incidence Hessian. The module doc frames the whole chain as calculation, not a new physical assumption; discharging this Prop is the remaining local analytic step before the second-variation input is unconditional.
In the broader Recognition geometry stack this is classical Regge calculus analysis (deficit angles, conformal vertex potentials), not a forcing-chain landmark (T5–T8). It is scaffolding for the geometric side of the discrete action, not a claim about $\varphi$, the eight-tick octave, or $D=3$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.