edgeAngleContributionOfField_flat
plain-language theorem explainer
On the periodic Freudenthal torus, evaluating the per-tetrahedron dihedral angle contribution of an edge against the flat squared-length field recovers exactly the certified typed-edge angle from the periodic angle-sum chain. Anyone building the flat-point deficit or true Regge action identities cites this. The proof is a short case split on the canonical edge-slot lookup, reducing via the flat squared-edge identity to the Freudenthal local dihedral angle.
Claim. For every periodic edge $e$ and every periodic Freudenthal tetrahedron $\tau$ on the $N\times N\times N$ torus, the angle contribution of $e$ in $\tau$ computed from the flat edge-length field equals the certified typed-edge angle contribution of $(e,\tau)$ in the periodic angle-sum chain.
background
This module is Stage 1 of the Regge TT continuum-symbol program: it defines the true nonlinear 3D Regge action on the canonical periodic Freudenthal torus as a function of an arbitrary edge squared-length field, together with the flat point and the TT Bloch symbol object. The action reuses existing Cayley–Menger dihedral angles and deficit machinery rather than re-deriving geometry.
An edge field assigns a real squared length to each positive-displacement periodic edge. The flat field is the constant unit assignment. For a field $\ell$, the per-tetrahedron angle contribution of an edge $e$ in a cell-tetrahedron $\tau$ is zero when $e$ is not a local edge of $\tau$, and otherwise the dihedral angle of $\tau$ at the matching local slot, read off the six squared edges of $\tau$ via the canonical edge-slot lookup.
Upstream, canonicalEdgeSlot? is the computable local slot map on the periodic skeleton; deficits are $2\pi$ minus the sum of incident dihedrals. The certified typed contribution is the geometry already fixed by the periodic angle-sum chain, independent of any dynamical field.
proof idea
Unfold both sides to the common definition that cases on canonicalEdgeSlot? e cellTet. On the none branch both sides are definitionally zero, so rfl closes. On the some f branch, simplify the field-side dihedral through tetDihedralAngleOfField and the already-proved identity that the flat field reproduces the canonical local squared-edge tuple (tetSqEdgesOfField_flat), landing on freudenthalLocalDihedralAngle, which is exactly the certified typed contribution.
why it matters
This is the hinge-level flat-point lemma for the true Regge action preflight. Its sole direct consumer is deficitOfField_flatEdgeField, which sums these contributions over all incident tetrahedra and invokes the certified periodic angle-sum target to conclude that every edge deficit vanishes at the flat assignment. That deficit vanishing then feeds trueReggeAction_flatEdgeField, establishing that the nonlinear action sits at a critical flat point before any TT second-variation or Bloch-symbol analysis.
In the broader QG campaign this is pure Stage-1 scaffolding closure: geometry is not re-proved here; the periodic angle-sum chain is reused. It does not touch the open continuum isotropy target ReggeTTContinuumIsotropyTarget (the claimed $K(0)=-(1/4)I_{TT}$ Einstein–Hilbert coefficient), which remains numerical evidence only. Framework-wise it sits in the discrete gravity layer that must be solid before continuum TT symbol claims can be stated in Lean.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.