WeightedDeficitDerivativeStationaryTarget
plain-language theorem explainer
Defines the stationarity target for the weighted deficit-derivative sum along every conformal line through a flat 3D Regge configuration: that sum has vanishing first derivative at the flat point. Anyone proving the nonlinear Regge Hessian or second-order Schläfli identities cites this Prop as the geometric input. It is a pure Prop abbreviation, not a proved statement.
Claim. For a 3D triangulation $K$ with consistent incidence and a flat configuration, the following holds: for every vertex potential $\xi$, the real function $$t \mapsto \sum_e \ell_e(\xi_t)\,\partial_t\delta_e(\xi_t)$$ has derivative zero at $t=0$, where $\ell_e$ is the conformal hinge (edge) measure and $\delta_e$ is the angular deficit along the conformal line $\xi_t$.
background
The module isolates the hard remaining step for the nonlinear Regge action: the second directional derivative of the action at a flat vertex potential must equal the canonical incidence Hessian. Once that identity is in hand, the existing second-variation input package follows at once.
In 3D Regge calculus the hinge measure is the edge length. Under the vertex-conformal ansatz it becomes $\ell_e(\xi)=\sqrt{g_e},\exp((\xi_u+\xi_v)/2)$. The deficit at a hinge is $\delta=2\pi-\sum\theta$. Along a conformal line $\xi_t=t\xi$ one forms the product $\ell_e(\xi_t),\partial_t\delta_e(\xi_t)$ and sums over edges. Classical Schläfli says the unweighted sum of $\ell,d\delta$ vanishes identically on closed simplicial complexes; the present target asks only that the $t$-derivative of that weighted sum vanish at the flat point $t=0$.
The definition packages exactly that first-order stationarity statement as a Prop, ready to be discharged by a local geometric argument (differentiating Schläfli cancellation through the conformal line) or by weaker near-zero expansions.
proof idea
No proof: this is a definitional Prop. The body is the universal quantification over vertex potentials $\xi$ of a HasDerivAt assertion for the edge-sum of conformal hinge measure times deficit line derivative, evaluated at value $0$ and point $t=0$. Downstream lemmas discharge it from stronger inputs such as conformal Schläfli along the line, eventual vanishing, or a near-zero expansion plus locality.
why it matters
This target is the geometric hinge between first-order Schläfli cancellation and the second-variation calculus of the nonlinear Regge action. It is the hypothesis of secondSchlaefliAlongLine_of_weightedStationary, which upgrades stationarity to the full second-order Schläfli identity along the line, and of the product-rule and tangency theorems that identify the second directional derivative with the canonical incidence Hessian (productRuleDerivativeCanonicalHessian_of_weightedStationary_and_edgeStencil, nonlinearDirectionalHessian_of_weightedStationary_and_edgeStencil, actionDerivativeTangencyToQuadratic_of_weightedStationary_and_edgeStencil).
In the Recognition geometry stack this closes the second chain-rule step needed for the flat-point Hessian of the discrete action, the discrete analogue of the Einstein-Hilbert second variation. It does not itself invoke the forcing chain (T5-T8) or the Recognition Composition Law; those enter only when the Regge Hessian is later matched to continuum curvature and the $\varphi$-ladder constants. The open geometric obligation is to prove the Prop from a near-flat conformal Schläfli theorem; several discharge lemmas already reduce that obligation to weaker local statements.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.