pith. machine review for the scientific record. sign in
module module high

IndisputableMonolith.Foundation.SimplicialLedger.LorentzEmergence

show as:
view Lean formalization →

This module defines the axial dispersion relation of the cubic-lattice Laplacian and assembles supporting quantities that prepare the emergence of Lorentz invariance in a simplicial ledger. Lattice modelers and discrete-spacetime researchers cite the explicit form ω_axis(a, k) = (2/a²)(1 - cos(a k)) when checking continuum limits. The module is organized as a chain of definitions and lemmas that establish bounds, non-negativity, and isotropy envelopes.

claimThe axial dispersion is given by $ω_α(a,k) = (2/a²)(1 - cos(a k))$, with auxiliary maps axis_dispersion, dispersion, continuum_isotropic, and envelope bounds that certify rotation invariance.

background

The module resides in Foundation.SimplicialLedger.LorentzEmergence and imports Mathlib real analysis together with the Constants module. The upstream Constants declaration supplies the RS time quantum τ₀ = 1 tick. Its central object is the single-axis dispersion relation quoted in the module doc-comment: ω_axis(a, k) = (2 / a²) · (1 − cos(a · k)).

proof idea

This is a definition module, no proofs. It proceeds by successive definitions that introduce axis_dispersion, dispersion, continuum_isotropic, and the LorentzEmergenceCert certificate, together with supporting lemmas on upper bounds and non-negativity.

why it matters in Recognition Science

These definitions supply the lattice starting point that feeds LorentzEmergenceCert and the downstream isotropy arguments. The construction fills the step from discrete Laplacian to continuum limit inside the Recognition Science forcing chain, supporting the emergence of isotropic propagation and D = 3.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (11)