PeriodicTTHessianMatchesLichnerowiczAtN5
plain-language theorem explainer
At N=5 on the periodic Freudenthal torus, this Prop asserts that a Regge Hessian operator and a lattice Lichnerowicz operator agree on every transverse-traceless edge perturbation. Track 1.D tensor/shear work cites it as the exact forward match target for spin-2 modes beyond the conformal ansatz. It is a pure definition: universal equality on the TT subspace, with no proof content.
Claim. Given two linear maps $H$ and $L$ from real edge perturbations of the $N=5$ periodic Freudenthal triangulation to themselves, the Hessian/Lichnerowicz match holds when, for every edge perturbation $\varepsilon$ lying in the longitudinal transverse-traceless subspace, $H(\varepsilon)=L(\varepsilon)$.
background
Track 1.D opens the tensor/shear sector of weak-field gravity on the discrete triangulation. Track 1.B only assigns a scalar potential at each vertex and pushes it to edges by endpoint averaging; that conformal slice cannot carry pure shear, so it misses transverse-traceless gravitational-wave modes. This module therefore treats independent edge-length perturbations as the primary objects and isolates those that are not vertex-conformal.
Edge data at $N=5$ are real functions on the typed periodic Freudenthal edges (PeriodicEdgePerturbation5). The longitudinal TT subspace is the discrete stand-in for spin-2, divergence-free, traceless metric perturbations. The classical continuum comparison is the Lichnerowicz operator on TT tensors; the discrete side is the second variation (Hessian) of the Regge action restricted to the same edge space.
The match predicate simply asks that those two operators coincide pointwise on the TT subspace. Instantiating the operators and proving the equality is deferred to a data structure that packages both maps together with this Prop.
proof idea
No proof: the declaration is a Prop-valued definition. It quantifies over edge perturbations, restricts to the longitudinal TT subspace at $N=5$, and demands definitional equality of the two supplied operators on that subspace. Downstream code supplies concrete Regge-Hessian and lattice-Lichnerowicz maps and discharges the resulting equality obligation.
why it matters
This is the exact forward Track 1.D target named in the doc-comment: Regge Hessian equals lattice Lichnerowicz on TT edge perturbations at $N=5$. It is consumed by the match-data structure, whose fields are the two operators plus a proof of this Prop (matches_on_tt). That structure is the analytic work-item for identifying the discrete spin-2 wave operator with the second variation of Regge calculus on the periodic Freudenthal torus.
In the broader Recognition scaffold, the conformal (scalar) sector is already separated; this predicate opens the pure-shear channel needed for gravitational waves. It does not yet invoke the forcing chain (T5–T8) or the Recognition Composition Law, but it sits in the gravity layer that must eventually connect discrete curvature variations back to the eight-tick and $D=3$ geometry forced upstream.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.