torusDensityWeight
plain-language theorem explainer
Defines the 4-torus action-average density weight as $N^{-4}$ for a periodic mesh of side $N$. Gravity continuum-limit arguments cite it when matching the finite Freudenthal action to the Bloch symbol dictionary. The body is a one-line real power definition, frozen against the wrong-power decoy used in preflight checks.
Claim. For each natural number $N$, the density weight of the action average on the 4-torus of side $N$ is $N^{-4}$.
background
The module treats the finite periodic Freudenthal action on a 4-torus of side $N=j+3$, with $N^4$ lattice sites. The continuum dictionary needs a density weight that turns site sums into continuum averages; the natural choice is one over the number of sites, hence $N^{-4}$.
This mirrors the closed 3D path, where the second-difference prefactor $(2/N^3)$ cancels the cell-sum factor $N^3/2$ to leave 1. In 4D the same bookkeeping is $(2/N^4)\cdot(N^4/2)=1$, so the canonical finite Hamiltonian equals the distinct-hinge Bloch fold once Schläfli elevation and the 4D cell-sum identity are in place.
A preflight decoy uses the wrong mesh power $N^{-2}$. The present weight is the correct $N^{-4}$ factor against which that decoy is discriminated.
proof idea
Pure definition: cast $N$ to $\mathbb{R}$ and raise its reciprocal to the fourth power. No lemmas or tactics.
why it matters
Anchors the density side of the 4D action↔symbol dictionary. Downstream, torusDensityWeight_eq_correct identifies it with the named correct weight by reflexivity, and torusDensityWeight_ne_wrong shows it differs from the wrong-mesh-power decoy for $N\ge 2$ via the preflight inequality. Together those facts freeze the continuum bookkeeping so that, once the open 4D cosine cell-sum identity closes, the surviving dictionary factor is 1 and canonicalFiniteH4D matches the distinct-hinge fold. It does not touch gap_action_recovery.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.