VoxelLattice
plain-language theorem explainer
The VoxelLattice structure models discrete spacetime in Recognition Science via a real spacing parameter and a default four-dimensional setting that includes time. QFT researchers seeking a first-principles UV regularization from lattice discreteness cite it as the type that bounds momenta inside the Brillouin zone. It is introduced as a bare structure definition with no proof obligations or computational content.
Claim. A voxel lattice is a structure consisting of a real number $l$ for lattice spacing together with a natural number $d$ (defaulting to 4) for spacetime dimension.
background
The QFT.UVCutoff module targets derivation of a natural ultraviolet cutoff from Recognition Science discreteness at the fundamental time scale τ₀. The VoxelLattice structure supplies the discrete lattice whose spacing corresponds to l₀ = c τ₀ (with c = 1 in RS units) and whose dimension is set to 4 to include one time coordinate. Downstream definitions such as fundamentalLattice instantiate the structure with spacing := l0 while brillouinCutoff computes the momentum bound π ħ / spacing, directly implementing the Brillouin-zone cutoff stated in the module doc-comment.
proof idea
The declaration is a structure definition that introduces the VoxelLattice type with fields spacing : ℝ and dimension : ℕ := 4. No lemmas, tactics, or reductions are applied; the body is empty and the construction is purely declarative.
why it matters
VoxelLattice supplies the discrete-spacetime foundation for the UV-cutoff program in QFT-013, feeding the brillouinCutoff and fundamentalLattice definitions that realize the natural momentum bound p_max = π ħ / l₀. It implements the Recognition Science claim that spacetime discreteness at the τ₀ scale regularizes all UV divergences, linking to the eight-tick octave and T8 spatial-dimension result by adopting total dimension 4. The structure closes the interface between the PhiForcing foundation and concrete QFT regularization without introducing additional hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.