brillouin_equals_pmax
plain-language theorem explainer
The theorem establishes that the Brillouin zone cutoff on the fundamental lattice equals π times the maximum momentum p_max. QFT researchers seeking a first-principles UV regulator from discrete spacetime would cite this equality to bound loop momenta. The proof is a one-line wrapper that unfolds the definitions of brillouinCutoff, fundamentalLattice, p_max and l0 then applies ring to obtain the identity.
Claim. The Brillouin zone cutoff for the fundamental lattice equals $π p_{max}$.
background
The module derives a natural ultraviolet cutoff for quantum field theory from Recognition Science discreteness. Spacetime is discrete at the fundamental length scale ℓ₀, so momenta are bounded by p_max = ℏ/τ₀. The Brillouin zone cutoff is the highest wave number admitted by the lattice before aliasing occurs. Upstream, l0 supplies the placeholder fundamental length (def l0 : ℝ := 1) while A from IntegrationGap encodes the active edge count per tick and the φ-power balance at D = 3.
proof idea
The proof unfolds brillouinCutoff, fundamentalLattice, p_max and l0, then invokes the ring tactic. This reduces the left-hand side directly to the right-hand side by algebraic cancellation in the underlying real arithmetic.
why it matters
The result supplies the concrete identification needed for the regularized loop integrals described in the module comment, where the RS cutoff Λ = p_max renders I(Λ) finite. It completes the core step of QFT-013 by equating the lattice Brillouin cutoff with π p_max, thereby grounding the claim that discreteness at the τ₀ scale eliminates UV divergences. No downstream theorems yet reference it, leaving open its insertion into explicit loop calculations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.