PeriodicTTHessianLichnerowiczMatchData5
plain-language theorem explainer
Data record packaging a Regge TT Hessian operator and a lattice Lichnerowicz operator on periodic edge perturbations at N=5, plus the assertion that the two agree on the longitudinal TT subspace. Discrete-gravity and spin-2 lattice workers cite it when closing the Track 1.D Hessian match. Pure structure definition: no proof body, only the carrier type for a future inhabited instance.
Claim. A data record consisting of two operators $H_{\mathrm{Regge}}$ and $L_{\mathrm{Lich}}$ sending periodic edge perturbations (real functions on the typed Freudenthal edges at $N=5$) to periodic edge perturbations, together with a proof that for every edge perturbation $\varepsilon$ in the periodic longitudinal transverse-traceless subspace one has $H_{\mathrm{Regge}}(\varepsilon)=L_{\mathrm{Lich}}(\varepsilon)$.
background
Track 1.D opens the tensor/shear sector of the weak-field metric. Track 1.B's conformal ansatz assigns one scalar potential per vertex and induces edge-length changes by averaging endpoints; that scalar slice cannot represent pure shear, so it misses transverse-traceless gravitational-wave modes. This module separates independent edge perturbations from vertex-conformal ones and records elementary rectangle obstructions for the conformal ansatz.
A periodic edge perturbation at $N=5$ is a real-valued function on the typed edges of the periodic Freudenthal torus. The match target states that, on the longitudinal TT subspace of those perturbations, the Regge second-variation Hessian operator equals the discrete spin-2 Lichnerowicz stencil. Spatial dimension is the forced $D=3$ from the RS chain (linking requires three spatial dimensions).
proof idea
No proof: the declaration is a structure (data carrier). Its three fields are the Regge TT Hessian map, the lattice Lichnerowicz map, and a Prop field requiring those maps to agree on every longitudinal TT edge perturbation via the named match predicate at $N=5$. Inhabiting the structure is the analytic work: build both operators from the Regge edge Hessian and the spin-2 stencil, then discharge the equality on the TT subspace.
why it matters
Closes the interface for the forward Track 1.D Hessian-to-Lichnerowicz target at $N=5$. Without an inhabited instance, the discrete spin-2 sector remains a scaffold: conformal (scalar) modes alone cannot carry TT gravitational waves. The parent program is the tensor/shear track that complements the conformal ansatz and aims at a lattice Lichnerowicz match on pure shear. Framework landmarks: $D=3$ spatial dimensions from the forcing chain, and the eight-tick/periodic lattice geometry underlying the Freudenthal torus. No downstream theorems yet consume this structure; it is the typed hole future match proofs must fill.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.