fundamentalLattice
plain-language theorem explainer
The declaration defines the fundamental lattice as the voxel lattice whose spacing equals the base length l0. QFT researchers deriving a natural ultraviolet cutoff from spacetime discreteness would cite this construction to anchor the Brillouin zone. The definition is a direct record construction supplying the spacing field of the VoxelLattice structure.
Claim. The fundamental lattice is the voxel lattice with spacing equal to the fundamental length $l_0$.
background
The QFT module derives the ultraviolet cutoff from Recognition Science discreteness. Spacetime is modeled as a voxel lattice whose spacing parameter sets the scale at which momenta become periodic. The structure defaults to four dimensions and bounds physical momenta inside the first Brillouin zone, with maximum momentum given by $p_max = π ℏ / l_0$ as stated in the sibling definition.
proof idea
One-line definition that constructs the VoxelLattice record by setting the spacing field to l0.
why it matters
This definition supplies the concrete lattice object required by the downstream theorem that the Brillouin cutoff equals π times p_max. It implements the core step of the QFT-013 program for natural UV regularization from information-theoretic discreteness. The construction inherits the phi-ladder scaling through the upstream l0 and period definitions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.