pith. sign in
structure

LorentzViolationCert

definition
show as:
module
IndisputableMonolith.Physics.LorentzViolationBoundFromRS
domain
Physics
line
32 · github
papers citing
none yet

plain-language theorem explainer

The LorentzViolationCert structure records that the Lorentz violation test categories number exactly five and that the violation term enters at quadratic order in the dispersion relation. Researchers working on lattice-to-continuum limits in quantum gravity or SME constraints would cite this certificate when linking Recognition Science to observable bounds. The definition directly assembles the finite cardinality of the test categories with the constant quadratic order.

Claim. A structure $C$ such that the set of Lorentz violation test categories has cardinality 5 and the Lorentz violation enters at order 2 in the dispersion relation.

background

In the Recognition Science lattice treatment, wavelengths much larger than the lattice spacing reduce the dispersion to the continuum Laplacian, leaving Lorentz violation as an O(a²k²) correction that stays invisible until |k| approaches 1/a. The five test categories are photon dispersion, CPT violation, SME parameters, UHECR GZK cutoff, and graviton dispersion. The upstream definition fixes the order of magnitude at 2, matching this quadratic term, while the module states the resulting bound δ_LV < (a/λ_Planck)² ≈ 10^{-66}.

proof idea

This is a structure definition that directly records the cardinality of the Lorentz violation test categories together with the predefined quadratic order of magnitude.

why it matters

The certificate supplies the two fields required by the downstream instance lorentzViolationCert that closes the module. It fills the A4 quantum gravity step by confirming that the five canonical test categories match the configuration dimension and that the suppression remains quadratic, consistent with the lattice-to-continuum reduction. The construction supports the claim that any observable Lorentz violation is pushed far below current experimental reach.

Switch to Lean above to see the machine-checked source, dependencies, and usage graph.