continuum_isotropic
plain-language theorem explainer
continuum_isotropic defines the squared Euclidean norm of a three-dimensional wave vector k, which supplies the rotationally invariant target for the leading-order lattice dispersion. Physicists examining emergent Lorentz symmetry from cubic lattices cite it as the continuum Laplacian eigenvalue that erases directional preference at long wavelengths. The definition is a direct sum of the three squared components.
Claim. For a wave vector $k = (k_1, k_2, k_3) ∈ ℝ^3$, the rotationally invariant continuum Laplacian eigenvalue is defined by $|k|^2 = ∑_{i=1}^3 k_i^2$.
background
This definition sits inside the module that derives Lorentz emergence from a cubic ledger, resolving the risk that a discrete lattice would select a preferred frame. The lattice dispersion is constructed as the sum over three axes of the single-axis term axis_dispersion a (k_i), each of which satisfies 1 − cos(x) ≤ x²/2 and therefore stays below k_i². The resulting upper envelope is exactly the isotropic quantity |k|², independent of the direction of k. Upstream, dispersion is the full three-dimensional sum, while the trigonometric bound is taken from standard real-analysis inequalities.
proof idea
One-line definition that expands directly to the sum of squares over the three components indexed by Fin 3.
why it matters
It supplies the isotropic target used by dispersion_upper_bound_by_isotropic to prove dispersion a k ≤ continuum_isotropic k and by isotropic_envelope_rotation_invariant to show that the envelope depends only on |k|. Both results are collected inside the LorentzEmergenceCert structure, which certifies that the cubic ledger produces rotationally invariant continuum physics at leading order and thereby addresses the anisotropy concern raised in the module documentation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.