pith. sign in
module module high

IndisputableMonolith.Physics.LorentzViolationBoundFromRS

show as:
view Lean formalization →

The module establishes that Lorentz violation effects from Recognition Science appear as O(a²k²) corrections in the dispersion relation. Physicists modeling discrete spacetime or deriving LV bounds from fundamental constants would cite it. The module organizes the argument via sibling definitions of test categories, counts, orders of magnitude, and certificates built on the RS time quantum.

claimLorentz violation satisfies $LV = O(a^2 k^2)$ in the dispersion relation, where $a$ is the lattice scale set by the RS time quantum and $k$ is the wave number.

background

The module imports Constants, whose doc-comment states: The fundamental RS time quantum (RS-native). τ₀ = 1 tick. It introduces LVTestCategory to classify tests of Lorentz invariance, lvTestCount to enumerate instances, lvOrderOfMagnitude to estimate size, and lv_quadratic to isolate the quadratic term. LorentzViolationCert and lorentzViolationCert certify the bound. The local setting is the extraction of physical dispersion corrections from the Recognition Science framework.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the quadratic LV bound that feeds into Recognition Science physics derivations, aligning with the forcing chain steps T5–T8 and the phi-ladder mass formula. It fills the step that keeps dispersion relations consistent with RS-native units where c = 1 and α^{-1} lies in (137.030, 137.039).

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (6)