HingeDeficitLineDifferentiabilityNearZeroTarget
plain-language theorem explainer
Packages the near-zero differentiability of conformal hinge measures and Regge deficit angles along every line potential through a vertex potential. Anyone proving the finite product rule for the first action derivative near the flat point cites this target. It is a pure Prop definition: the quantified differentiability statement itself, later discharged from flat configurations.
Claim. For an incidence-consistent 3D triangulation $K$, the following property holds: for every vertex potential $\xi$, eventually for all $t$ near $0$, and for every edge $e$, both $s \mapsto$ (conformal hinge measure of $e$ along the line potential through $\xi$ at $s$) and $s \mapsto$ (Regge deficit angle of $e$ along that same line) are differentiable at $t$.
background
The module isolates the hard endpoint of the nonlinear Regge Hessian: the second directional derivative of the Regge action at the flat potential must match the canonical incidence Hessian. Once that chain-rule calculation is in place, the existing second-variation input package follows at once.
Under the vertex-conformal ansatz, the 3D hinge measure on a global edge is the conformal edge length: square root of the squared edge length times an exponential of the averaged endpoint potentials. The deficit angle at an edge is $2\pi$ minus the sum of local deficit contributions over tetrahedra. A line potential is the straight-line path $s \mapsto$ (base + $s\cdot\xi$) in the space of vertex potentials.
This declaration does not compute derivatives. It names the minimal factorwise differentiability needed before one may differentiate a product of hinge measure and deficit once more at the flat point.
proof idea
Definition only: the body is the Prop $\forall,\xi,;\forall^{\mathrm{f}},t\in\mathrm{nhds}(0),;\forall,e,$ both maps $s\mapsto$ hingeMeasureUnderConformal along the line potential and $s\mapsto$ deficitAngle along that line are DifferentiableAt $t$. No tactics, no lemmas applied. Downstream, flat-configuration data discharges the Prop; the product-rule theorem consumes it as a hypothesis.
why it matters
Sits on the nonlinear Hessian proof interface. The parent theorem actionDerivativeProductRuleNearZero_of_factorDifferentiability takes this Prop as hypothesis and concludes the near-zero product-rule target for the action derivative (filter-upwards on the eventual differentiability of both factors). The sibling hingeDeficitLineDifferentiabilityNearZero_of_flatConfiguration shows the Prop holds whenever the triangulation carries a flat configuration, so the target is not an extra axiom.
In the broader Recognition geometry stack this is bookkeeping for the second variation of the discrete Einstein-Hilbert (Regge) action under conformal vertex potentials. It does not itself touch T5-T8 or the RCL; it clears the analytic side condition so the directional Hessian can be identified with the canonical incidence form.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.