SecondSchlaefliAlongLineTarget
plain-language theorem explainer
Defines the second-order Schläfli identity along a conformal line on a flat, incidence-consistent 3D triangulation: for every vertex potential, a sum over edges of mixed hinge/deficit first derivatives plus length-weighted second deficit derivatives vanishes at the flat point. Regge-calculus and RS gravity proofs cite it as the cancellation target that removes one mixed term after flatness kills the bare deficit. It is a pure Prop abbreviation of that edge-sum identity, not a proved lemma.
Claim. Let $K$ be a 3-dimensional triangulation that is incidence-consistent and flat. The second-order Schläfli target along a conformal line asserts: for every vertex potential $\xi$, $$\sum_e\Bigl(\partial_t\ell_e(0)\,\partial_t\delta_e(0)+\ell_e(0)\,\partial_t^2\delta_e(0)\Bigr)=0,$$ where the sum runs over edges, $\ell_e(t)$ is the hinge measure along the conformal line through $\xi$, and $\delta_e(t)$ is the deficit angle along that line, both evaluated at the flat basepoint $t=0$.
background
The module isolates the hard endpoint of the nonlinear Regge calculation: the second directional derivative of the Regge action at a flat potential must equal the canonical incidence Hessian. After the first variation and product rule are expanded along a conformal line of vertex potentials, flatness kills the bare deficit-angle term, leaving a mixed hinge/deficit first-derivative piece and a length-weighted second deficit derivative.
Classical Schläfli says that length-weighted deficit variations cancel in closed form; the second-order version needed here is the edge-sum identity that cancels one copy of the mixed term against the second deficit derivative. Hinge measure under a conformal rescaling and the first and second line derivatives of deficit and hinge length are the geometric ingredients of that sum.
The surrounding interface treats this identity as a named target Prop so that later theorems can assume or discharge it without re-expanding the chain rule.
proof idea
Definitional: the body is exactly the universal quantification over vertex potentials of the stated edge sum set equal to zero. No tactics or lemmas are applied; the declaration packages the second-order Schläfli cancellation as a reusable Prop so downstream results can take it as a hypothesis or prove it equivalent to weighted-deficit stationarity.
why it matters
This target is the precise cancellation step the module needs before the second product rule can be identified with the canonical incidence Hessian. Downstream, secondProductRuleEqualsCanonicalHessian_of_secondSchlaefli_and_mixed consumes it together with a mixed-hinge target to obtain the full second-product-rule identity. It is also proved equivalent to weighted-deficit-derivative stationarity (both directions and the iff), so either formulation can be used as the hard geometric input.
In the gravity layer it is specialized to the canonical periodic Freudenthal torus (CanonicalPeriodicSecondSchlaefliAlongLineTarget) and related to a typed-edge form, tying the abstract Regge Hessian interface to the physical six-tet cubic Dirichlet instance. Within RS geometry this is the remaining analytic gate on the path from flat conformal variations to the quadratic Hessian that feeds the nonlinear second-variation theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.