LocalConformalSchlaefliAlongLineTarget
plain-language theorem explainer
Defines the local tetrahedral Schläfli identity along a conformal line: at every parameter and every tetrahedron, the length-weighted sum of actual dihedral-angle derivatives vanishes. Downstream Hessian and incidence arguments cite this Prop as the non-flat local calculus input. It is a pure predicate definition, not a proved theorem.
Claim. For a 3D triangulation $K$, the local conformal Schläfli-along-line target asserts: for every vertex potential $\xi$, every real parameter $t$, and every tetrahedron $\tau$, $$\sum_{f=1}^{6} \sqrt{\ell_f(\xi,t)^2}\,\partial_s\theta_f(\xi,s)\big|_{s=t}=0,$$ where $\ell_f$ are the local conformal edge lengths of $\tau$ at the line potential through $\xi$ at $t$, and $\theta_f$ are the corresponding dihedral angles under the conformal deformation.
background
The module isolates the remaining hard step for 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.
Regge calculus assigns to each hinge a deficit angle and an edge length; the classical Schläfli identity says that length-weighted sums of dihedral-angle variations cancel inside each simplex. Here the geometry is deformed along a conformal line of vertex potentials: edge lengths and dihedral angles become functions of a real parameter $t$. The local identity is the same cancellation, but evaluated at an arbitrary point on that line and written with genuine derivatives rather than a flat-point closed form.
The six-term sum runs over the edge slots of a single tetrahedron. Local conformal squared edge lengths supply the weights; the derivatives are of tetrahedral dihedral angles under the conformal family. Global hinge bookkeeping (deficit as minus sum of incident angles, reindexing of incidences) is deliberately left to a companion expansion target.
proof idea
No proof: this is a def whose body is a Prop. It packages the universal quantification over vertex potentials, line parameters, and tetrahedra, together with the six-edge weighted derivative sum set equal to zero. Downstream theorems treat the resulting predicate as a named hypothesis to be assumed or discharged separately.
why it matters
This predicate is the tetrahedral calculus content of Schläfli away from the flat point. The combiner conformalSchlaefliAlongLine_of_expansion_and_local takes an incidence-consistent triangulation, the global expansion/reindexing target, and this local target, and concludes the full conformal Schläfli-along-line target used in the nonlinear Hessian chain.
On the gravity side, the canonical periodic six-tet cubic Dirichlet instance specializes the same predicate to the encoded periodic Freudenthal torus, giving a concrete lattice instance of the local non-flat Schläfli condition. In the broader Recognition geometry stack this is scaffolding for matching the second directional derivative of the Regge action to the canonical incidence Hessian, not a new physical assumption.
It does not itself touch the forcing chain (T5–T8) or the Recognition Composition Law; those enter only indirectly through the constants and continuum-bridge context of the surrounding geometry modules.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.