lvTestCount
plain-language theorem explainer
The theorem asserts that the finite type of Lorentz violation test categories contains exactly five elements. Researchers bounding Lorentz violation in quantum gravity models would reference this cardinality when constructing the overall certification object. The proof proceeds by a single decision tactic that leverages the derived Fintype instance on the inductive enumeration of the five categories.
Claim. The finite set of Lorentz violation test categories, consisting of photon dispersion, CPT violation, SME parameters, UHECR GZK cutoff, and graviton dispersion, has cardinality five: $|LVTestCategory| = 5$.
background
The Lorentz Violation Bound from RS module starts from the lattice dispersion relation, which reduces to the continuum Laplacian at wavelengths much larger than the lattice spacing a, producing Lorentz violation corrections of order O(a²k²). The module enumerates five canonical test categories for such violations: photon dispersion, CPT violation, SME parameters, UHECR GZK cutoff, and graviton dispersion, setting this count equal to the configuration dimension D = 5. Upstream results supply the full 3D lattice-Laplacian dispersion definition and the collision-free properties of empirical programs that underwrite the emergence of Lorentz invariance.
proof idea
The proof is a one-line wrapper that applies the decide tactic directly to the equality Fintype.card LVTestCategory = 5. The tactic succeeds because the inductive definition of LVTestCategory derives both DecidableEq and Fintype, allowing Lean to enumerate the five constructors and compute the cardinality without invoking additional lemmas.
why it matters
This cardinality supplies the five_tests field inside the lorentzViolationCert definition that assembles the complete Lorentz violation certification. It implements the module claim that the five test categories equal configDim D = 5 and supports the derived bound δ_LV < (a/λ_Planck)² ≈ 10^{-66} obtained from the lattice spacing relative to the Planck length. In the Recognition Science framework the result anchors the T8 step that fixes D = 3 spatial dimensions while extending the test count to the five-category configuration used for experimental bounds.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.