edgeAngleContributionOfField
plain-language theorem explainer
Contribution of one Freudenthal tetrahedron to the dihedral-angle sum around a given periodic edge, under an arbitrary edge squared-length field. Returns the local dihedral angle when the edge is incident to that tet, and zero otherwise. Anyone assembling the Regge deficit or differentiating the true nonlinear action cites this. Implemented by a single match on the canonical edge-slot lookup.
Claim. Given an edge squared-length field $\ell$ on the side-$N$ periodic Freudenthal torus, a periodic edge $e$, and a periodic tetrahedron $\tau=(c,t)$, the contribution equals the dihedral angle of $\tau$ at the local slot occupied by $e$ if $e$ is one of the six edges of $\tau$, and equals $0$ otherwise.
background
This module builds the true nonlinear 3D Regge action on the canonical periodic Freudenthal torus as a function of an arbitrary edge squared-length field. An edge field assigns one real (a squared length) to each positive-displacement periodic edge. Periodic tetrahedra are pairs (cell vertex, Fin 6), the six Freudenthal tets inside each cubic cell.
The classical Regge deficit at a hinge is $2\pi$ minus the sum of incident dihedral angles. Here that sum is assembled tet-by-tet: for each candidate tet one must decide whether the given edge is among its six edges, and if so which local slot it occupies. That decision is the computable lookup canonicalEdgeSlot? on the periodic skeleton (match against the six localEdgeOf images).
When the edge is incident, the angle itself is the existing Cayley-Menger dihedral tetDihedralAngleOfField (arccos of the cm-cofactor ratio on the six squared lengths read off the field). Non-incident tets contribute nothing, so the global sum only sees the true star of the edge.
proof idea
Pure definition by case split on the optional slot returned by the canonical edge-slot lookup. On some f, return the field-dependent dihedral angle of the given tet at slot f. On none, return the constant $0$. No lemmas are applied; the body is the match itself.
why it matters
This is the atomic summand of the true-action deficit. deficitOfField is defined as $2\pi$ minus the sum of these contributions over all periodic tets, and the true nonlinear Regge action weights that deficit by $\sqrt{\ell_e}$. Downstream flat-point theorems (edgeAngleContributionOfField_flat, deficitOfField_flatEdgeField) and the conformal identification (deficitAngle_conformal_eq) all unfold through it.
In the QG full-theory campaign it is the hinge through which differentiability and symbol existence pass: hasDerivAt_contrib and hasDerivAt_deficit differentiate one contribution then the full deficit along plane-wave paths, and edgeAngleContribution_planeWave_contDiffAt upgrades the same case split to ContDiffAt at amplitude zero. Those feed the TT Bloch symbol object and the still-open continuum isotropy target (ReggeTTContinuumIsotropyTarget), whose numerical probe reports $K(0)=-(1/4)I_{TT}$ matching linearized Einstein-Hilbert TT.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.