Pith. sign in
module module high

IndisputableMonolith.Foundation.SimplicialLedger.LorentzEmergence

show as:
view Lean formalization →

The module defines the axis dispersion relation of the cubic-lattice Laplacian along with isotropy checks and bounding lemmas. Researchers deriving continuum limits from discrete spacetime models in Recognition Science cite these objects. The module consists of definitions and direct trigonometric bounds with no complex proof structure.

claimThe axis dispersion is $\omega_{\rm axis}(a,k)=\frac{2}{a^2}(1-\cos(ak))$. Companion objects comprise the full dispersion function, the continuum isotropy predicate, and non-negativity plus upper-bound lemmas.

background

The module resides in Foundation.SimplicialLedger.LorentzEmergence and imports Mathlib real-analysis libraries together with IndisputableMonolith.Constants, whose sole content is the time quantum $\tau_0=1$ tick. The supplied DOC_COMMENT identifies the core object as the dispersion relation of the cubic-lattice Laplacian at a single axis. The local setting is a discrete cubic lattice whose Laplacian must recover isotropic linear dispersion in the long-wavelength limit.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The definitions and bounds feed the LorentzEmergenceCert sibling and supply the lattice dispersion needed for the emergence of relativistic structure. They instantiate the discrete model whose continuum limit is required for the D=3 spatial dimensions in the unified forcing chain.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (11)