l0
plain-language theorem explainer
l0 defines the fundamental length scale as the product of the speed of light and the base tick duration tau0. QFT researchers deriving a natural UV cutoff from spacetime discreteness would cite this to fix the lattice spacing. The definition is a direct multiplication that pulls c and tau0 from the imported Constants module.
Claim. The fundamental length scale is given by $l_0 = c τ_0$, where $c$ denotes the speed of light and $τ_0$ is the fundamental tick duration.
background
The QFT.UVCutoff module derives a natural ultraviolet cutoff for quantum field theory from Recognition Science discreteness at the τ₀ scale. Momenta are bounded by p_max = ℏ / l₀, which regularizes divergent loop integrals. The upstream Constants module supplies τ₀ as the duration of one tick (noncomputable def tau0 : ℝ := tick), while Compat.Constants provides a placeholder version of l0. The Cosmology.LargeScaleStructureFromRS.scale function illustrates the phi-ladder scaling used elsewhere in the framework.
proof idea
This is a one-line definition that multiplies the imported constant c by tau0 from Constants.
why it matters
l0 supplies the lattice spacing for fundamentalLattice and p_max, which in turn feed brillouin_equals_pmax and the regularization of log_divergence. It anchors the UV cutoff claim in the module's core insight that spacetime discreteness at τ₀ eliminates the need for ad-hoc renormalization. The definition closes the link from the T0-T8 forcing chain to concrete QFT scales, including the alpha band and phi-ladder mass formulas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.