ttSecondDifferenceDensityWeight_eq
plain-language theorem explainer
The second-difference density weight on the 4D periodic torus of side N equals 2/N^4. Gravity analysts cite it when matching the discrete Freudenthal second-difference prefactor to the Bloch cell-sum volume so their product cancels to 1. The proof unfolds the bookkeeping definitions and finishes by ring normalization.
Claim. For every natural number $N$, the second-difference density weight on the four-dimensional torus of side $N$ equals $2/N^{4}$.
background
The module builds the action-to-symbol dictionary for a finite periodic Freudenthal sequence on a 4D torus of side $N=j+3$, with $N^{4}$ sites and density weight $N^{-4}$ (already frozen against the wrong-power $N^{-2}$ decoy in preflight).
It parallels the closed 3D path: there the second-difference prefactor $2/N^{3}$ multiplies the Bloch cell-sum factor $N^{3}/2$ and cancels to 1, so the canonical finite Hamiltonian equals the raw cosine fold. In 4D the same bookkeeping is required with $N^{4}$ sites: once the (still open) 4D cosine cell-sum supplies $N^{4}/2$, the product $(2/N^{4})\cdot(N^{4}/2)$ must be identically 1.
This declaration records the closed algebraic form of that second-difference density weight, obtained from the 4D bookkeeping factor definition.
proof idea
Unfold the density-weight definition together with the underlying 4D second-difference bookkeeping factor, then apply ring to normalize the resulting rational expression in $N$ down to $2/N^{4}$. No external lemmas are needed beyond definitional expansion.
why it matters
This identity is the density half of the algebraic cancellation $(2/N^{4})\cdot(N^{4}/2)=1$ that the module status list records as proved. It freezes the 4D density dictionary so that, once the open 4D cosine cell-sum identity and residual star-member offsets close, the canonical finite 4D Hamiltonian matches the distinct-hinge Bloch fold with surviving dictionary factor exactly 1.
The construction sits in the gravity analysis stack parallel to the completed 3D Regge TT continuum path. It does not flip gap-action recovery. Spacetime dimension 4 here is the product of the forced spatial $D=3$ (T8) with one time direction; the mesh itself is the 4D product torus of side $N$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.