ConformalSchlaefliAlongLineTarget
plain-language theorem explainer
The strongest along-line Schläfli target: for every vertex potential and every real parameter on the conformal ray, the edge sum of hinge measure times deficit line-derivative is identically zero. Discrete-gravity and Regge analysts cite it as the global geometric cancellation that kills the weighted deficit-derivative term in the first variation. It is a pure Prop interface; proofs discharge it from expansion plus local tetrahedral Schläfli.
Claim. For an incidence-consistent 3D triangulation $K$, the conformal Schläfli-along-line target asserts: for every vertex potential $\xi$ and every real parameter $t$, $$\sum_e h\bigl(t\cdot\xi, e\bigr)\,\delta'_e(t)=0,$$ where $h$ is the hinge measure in the conformal metric along the line through $\xi$ and $\delta'_e(t)$ is the actual $t$-derivative of the deficit angle on edge $e$.
background
This module isolates the hard second-variation calculation for nonlinear Regge action: the second directional derivative of the action at the flat potential must match the canonical incidence Hessian. Targets here package geometric identities needed before that chain-rule endpoint is closed.
A conformal line is the one-parameter family of vertex potentials $t\mapsto t\cdot\xi$ (flat at $t=0$). Hinge measure $h$ is the length weight on each edge in the conformal metric; deficit line-derivatives are ordinary derivatives of dihedral deficit along that path. The classical Schläfli identity on each tetrahedron reads $\sum_{e\in\tau}\ell_e,d\theta_{e,\tau}=0$.
The weaker sibling stationary target only asks that the weighted sum $\sum_e h,\delta'$ have derivative zero at the flat point. The present target is stronger: the sum itself vanishes at every $t$, not merely near flatness. Summing local Schläfli over tetrahedra cancels the $\sum h,\delta'$ contribution in the Regge first variation, leaving $S'(t)=\sum\delta,h'$ and forcing $V(t):=\sum h,\delta'=0$.
proof idea
This declaration is a Prop-valued definition, not a proved theorem. It names the identity to be established.
Downstream, conformalSchlaefliAlongLine_of_expansion_and_local discharges it by combining an expansion target with the local along-line Schläfli identity (per-tetrahedron length-weighted sum of actual dihedral derivatives vanishes at every $t$). The proof introduces $\xi$ and $t$ and assembles the global edge sum from those local cancellations.
Once the Prop holds, two one-step corollaries follow: the weighted deficit-derivative is eventually zero along the line, and (via the eventually-zero-to-stationary bridge) the stationary target at the flat point holds.
why it matters
In the nonlinear Regge Hessian program this is the strongest geometric Schläfli package: one global identity closes the full weighted-deficit-derivative stationary target and every typed-edge or per-displacement-class consumer without class-by-class decomposition.
Immediate parents: the of-expansion-and-local constructor; the eventually-zero and stationary corollaries that feed the second-variation input; and the gravity-side specialization CanonicalPeriodicConformalSchlaefliAlongLineTarget on the periodic Freudenthal torus, which instantiates the same Prop on the canonical encoded complex and aims at the $N=5$ stationary target there.
Framework role: it is pure 3D discrete geometry (Regge calculus on triangulations), aligning with the $D=3$ forcing landmark, and supplies the cancellation that lets the nonlinear Hessian equal the canonical incidence form once the remaining chain-rule calculation is filled in. It does not itself touch $\varphi$-ladder masses or $\alpha$; it is infrastructure for the geometric side of the gravity bridge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.