secondDifferenceBookkeepingFactor4D
plain-language theorem explainer
The constant 2 that multiplies the second-difference symbol in the 4D density-normalized finite dictionary. Anyone matching the 4D torus action to the Bloch symbol cites it as the numerator of the prefactor (2/N^4). It is a one-line real definition, fixed by the same C10/3D bookkeeping convention used in three dimensions.
Claim. The second-difference bookkeeping factor in four spacetime dimensions is the real constant $2$. Equivalently, the density-normalized finite symbol uses the prefactor $(2/N^4)\,S''$ rather than the bare second difference $S''$.
background
The module builds the 4D torus continuum limit for a finite periodic Freudenthal action on side length $N=j+3$, with $N^4$ lattice sites and density weight $N^{-4}$. The goal is an action↔symbol dictionary parallel to the closed 3D path from Bloch assembly to continuum limit.
In both 3D and 4D the finite second-difference symbol is not bare $S''$: it carries a density-normalized prefactor $(2/N^d),S''$. The factor $2$ is dimension-independent bookkeeping; only the power of $N$ changes with dimension. In 3D one has $(2/N^3)\cdot(N^3/2)=1$ after the cell-sum cosine average; the 4D story is the same with $N^4$.
This constant is the numerator of that prefactor when $d=4$. Downstream it is divided by $N^4$ to form the density weight, then multiplied by the cell-sum cosine factor $N^4/2$ to cancel exactly to 1.
proof idea
Pure definition: the real is set equal to $2$. No lemmas, no tactics. Downstream equalities unfold this name and simplify by ring or positivity.
why it matters
It is the shared numerator that makes the 4D density dictionary cancel the same way as in 3D. The density weight is defined as this factor over $N^4$; the equality theorem rewrites that weight as $2/N^4$. The headline algebraic identity then multiplies weight by the cell-sum cosine factor and obtains exactly 1, so the canonical finite Hamiltonian matches the distinct-hinge Bloch fold once Schläfli elevation and the 4D cell-sum identity close.
Without freezing this constant at 2, the cancellation $(2/N^4)\cdot(N^4/2)=1$ would not hold and the continuum dictionary factor would not survive as 1. The module status notes that product-mesh and density identities are theorems, while the 4D cosine cell-sum identity and residual star-member offsets remain open; this definition is the bookkeeping hinge those results share. It does not flip gap action recovery.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.