brillouinCutoff
plain-language theorem explainer
brillouinCutoff defines the first Brillouin zone momentum bound on a discrete voxel lattice as π ħ divided by the lattice spacing. QFT researchers deriving finite loop integrals from spacetime discreteness cite it to bound UV momenta. The definition is a direct algebraic expression using the lattice spacing field and the RS value of ħ.
Claim. For a voxel lattice with spacing $a$, the Brillouin zone cutoff momentum is $k_B = π ħ / a$.
background
The module QFT-013 derives a natural ultraviolet cutoff from Recognition Science discreteness: spacetime consists of voxels with spacing $l_0 = c τ_0$, so momenta cannot exceed the first Brillouin zone $|k| < π/a$. VoxelLattice is the structure carrying this spacing (and default dimension 4). The constant ħ is imported from Constants as $φ^{-5}$ in RS-native units (with parallel CODATA definitions in sibling modules). Upstream p_max supplies the base scale ħ/l0; the present definition multiplies by π to recover the zone boundary.
proof idea
One-line definition that multiplies Real.pi by the imported ħ constant and divides by the spacing field of the input VoxelLattice structure.
why it matters
This definition supplies the explicit Brillouin cutoff used to prove equality with π p_max in the downstream theorem brillouin_equals_pmax. It realizes the natural UV regularization proposed in the module for QFT-013, bounding momenta in the discrete lattice to regularize divergences. It connects to the RS forcing chain by enforcing the discreteness scale τ0 into momentum space.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.