pith. sign in
module module high

IndisputableMonolith.Foundation.SimplicialLedger.LorentzEmergence

show as:
view Lean formalization →

The LorentzEmergence module defines the axis dispersion relation of the cubic-lattice Laplacian together with isotropy and bound lemmas that support emergence of Lorentz structure. Researchers modeling discrete spacetime or lattice discretizations in Recognition Science would cite these objects. The module consists of definitions and short lemmas that start from the explicit cosine formula and establish nonnegativity plus envelope properties.

claimThe axis dispersion is given by $ω_α(a,k)= (2/a²)(1−cos(ak))$. Related lemmas establish nonnegativity, upper bounds by the isotropic envelope, and rotation invariance of that envelope.

background

The module resides in Foundation.SimplicialLedger and imports Mathlib trigonometric and power libraries plus IndisputableMonolith.Constants. The upstream Constants module supplies the RS-native time quantum τ₀ = 1 tick that sets the scale for all lattice quantities. The supplied module doc-comment states the dispersion relation of the cubic-lattice Laplacian at a single axis.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the dispersion, nonnegativity, and isotropy facts required by LorentzEmergenceCert and lorentzEmergenceCert. It therefore contributes to the Recognition Science derivation of D = 3 and the eight-tick octave from the J-uniqueness fixed point (T5–T8).

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (11)