Pith. sign in
module module moderate

IndisputableMonolith.Physics.LorentzViolationBoundFromRS

show as:
view Lean formalization →

The module Physics.LorentzViolationBoundFromRS establishes that Lorentz violation is quadratic, O(a²k²), in the dispersion relation under Recognition Science. Physicists studying modified dispersion or quantum gravity bounds would cite it to link LV effects to the RS time quantum. The module organizes this via a sequence of definitions for test categories, counts, orders of magnitude, quadratic terms, and a violation certificate.

claimLorentz violation satisfies $LV = O(a^2 k^2)$ in the dispersion relation, where $a$ denotes lattice spacing and $k$ the wave number, with the RS time quantum $ au_0 = 1$ tick fixing the scale.

background

The module imports the RS time quantum $ au_0 = 1$ tick from IndisputableMonolith.Constants. It introduces LVTestCategory, lvTestCount, lvOrderOfMagnitude, lv_quadratic, LorentzViolationCert, and lorentzViolationCert to structure the bound. The setting is the Recognition Science derivation of physics from a single functional equation, with constants fixed in RS-native units and the forcing chain determining D = 3 dimensions.

proof idea

This is a definition module, no proofs. The argument is organized by first categorizing LV tests, then counting instances, determining the order of magnitude, establishing the quadratic form lv_quadratic, and finally issuing the LorentzViolationCert.

why it matters in Recognition Science

The module supplies the explicit LV bound for use in downstream physics derivations within the Recognition framework. It fills the step connecting the time quantum $ au_0$ to observable dispersion corrections, consistent with the T0-T8 forcing chain and the Recognition Composition Law.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (6)