Encyclopedia Gravity Gravity Seven Gaps Discrete Lichnerowicz Continuum Profile Second Deriv

ARTICLE 3 claims 2 theorems 1 model

Gravity Seven Gaps Discrete Lichnerowicz Continuum Profile Second Deriv

A machine-checked proof that the simplest continuous wave has exactly the second derivative expected of it, and nothing more.

Verify this page

The continuum profile

A plane wave is the simplest repeating disturbance: a smooth oscillation, like a sine wave, that travels through space and time. In the framework's machine-checked library of formal theorems, the declaration continuumProfile_second_deriv concerns the one-dimensional profile of such a wave, written mathematically as exp(2πikt), where k is the wavenumber and t is time. The theorem proves that the second derivative of this profile with respect to time is exactly -(2πk)² times the original profile. In other words, the acceleration of the wave's amplitude is proportional to its displacement, with the constant of proportionality being the square of the spatial frequency, scaled by 2π.

This result is the continuum counterpart to a discrete result proved in the same file. On a lattice, the discrete Laplacian operator, applied to a plane wave, yields an eigenvalue that depends on the lattice spacing. The theorem discreteEigenvalue_tendsto shows that as the lattice spacing shrinks to zero, this discrete eigenvalue converges to (2πk)², which is precisely the eigenvalue of the continuum second derivative. The continuumProfile_second_deriv theorem confirms that (2πk)² is indeed the genuine eigenvalue of the continuum operator along the wave direction, closing the loop between the discrete and continuous descriptions.

In Recognition Science, this result is a step in the Seven-Gaps campaign, specifically the operator convergence gap. It establishes that on a flat three-dimensional torus, the discrete perturbation spectrum on a lattice converges to the spectrum of the continuum Lichnerowicz operator, at least along one axis. The Lichnerowicz operator, in this flat background, reduces to the negative Laplacian, and its eigenvalue on a transverse-traceless plane wave is (2πk)². This is a definitional choice, not a curved-space theorem, and the convergence is proved only for axis-aligned modes.

The theorem does not claim anything about curved backgrounds or quasinormal modes. The file explicitly marks these as open problems. It also does not claim isotropic recovery of the full Lichnerowicz spectrum; the axis-sector scope is a deliberate restriction, because the continuum moment tensor is anisotropic, with the body-diagonal direction being roughly 4.9 times stiffer than an axis direction. The result is a precise, narrow bridge between discrete and continuous descriptions, not a general theory of gravitational wave spectra.

THEOREM continuumProfile_second_deriv · IndisputableMonolith/Gravity/SevenGaps/DiscreteLichnerowicz.lean
continuumProfile_second_deriv · IndisputableMonolith/Gravity/SevenGaps/DiscreteLichnerowicz.lean:453 
/-- THEOREM. Second derivative of the continuum profile: `-(2πk)²` times the
profile. So `(2πk)²` is the genuine `-d²/dt²` eigenvalue of the continuum
mode along the wave direction (the mode is constant in the transverse
directions). -/
theorem continuumProfile_second_deriv (k : ℕ) (t : ℝ) :
    HasDerivAt (fun s : ℝ => 2 * (Real.pi : ℂ) * Complex.I * (k : ℂ) * continuumProfile k s)
      (((-((2 * Real.pi * (k : ℝ)) ^ 2) : ℝ) : ℂ) * continuumProfile k t) t := by
  have h := (continuumProfile_hasDerivAt k t).const_mul
    (2 * (Real.pi : ℂ) * Complex.I * (k : ℂ))
  have heq : ((-((2 * Real.pi * (k : ℝ)) ^ 2) : ℝ) : ℂ) * continuumProfile k t
      = 2 * (Real.pi : ℂ) * Complex.I * (k : ℂ)
        * (2 * (Real.pi : ℂ) * Complex.I * (k : ℂ) * continuumProfile k t) := by
    push_cast
    linear_combination (-4 * (Real.pi : ℂ) ^ 2 * (k : ℂ) ^ 2 * continuumProfile k t)
      * Complex.I_sq
  rw [heq]
  exact h
THEOREM discreteEigenvalue_tendsto · IndisputableMonolith/Gravity/SevenGaps/DiscreteLichnerowicz.lean
discreteEigenvalue_tendsto · IndisputableMonolith/Gravity/SevenGaps/DiscreteLichnerowicz.lean:204 
/-- THEOREM (the core convergence result; AXIS SECTOR ONLY). For fixed
wavenumber `k`, the discrete eigenvalue `4 N² sin²(πk/N)` of the AXIS mode
converges to the continuum eigenvalue `(2πk)²` as the lattice is refined.
Proof: `4N² sin²(πk/N) = (2πk)² (sin x / x)²` with `x = πk/N → 0`, and
`sin x / x → 1` at `0` (from `HasDerivAt sin 1 0` via the slope
characterization); the wavenumber `k = 0` is handled separately (both sides
vanish identically).

Scope: this is a statement about axis-aligned modes of the axis-stencil
Laplacian. Test G (`FreudenthalStencilPreflight`/`FreudenthalEnergyLimit`,
commits 7b808f75b4, 1d3ed6da06) kernel-proved the full continuum moment
tensor is anisotropic, `A₀ = (1+√2)I + (√2+√3)J`, which axis stencils
cannot see; do not read this as isotropic flat-space recovery. The
direction-resolved symbol question is governed by the C10 probe (plan
receipt P-iso, 2026-07-15). -/
theorem discreteEigenvalue_tendsto (k : ℕ) :
    Filter.Tendsto (fun N : ℕ => discreteEigenvalue N k) Filter.atTop
      (nhds ((2 * Real.pi * (k : ℝ)) ^ 2)) := by
  rcases Nat.eq_zero_or_pos k with hk | hk
  · subst hk
    have hzero : (fun N : ℕ => discreteEigenvalue N 0) = fun _ : ℕ => (0 : ℝ) := by
      funext N
      norm_num [discreteEigenvalue]
    rw [hzero]
    have h0 : ((2 * Real.pi * ((0 : ℕ) : ℝ)) ^ 2 : ℝ) = 0 := by norm_num
    rw [h0]
    exact tendsto_const_nhds
  · have hk' : (0 : ℝ) < (k : ℝ) := by exact_mod_cast hk
    -- sin y / y → 1 as y → 0 (through nonzero values)
    have hslope : Filter.Tendsto (fun y : ℝ => Real.sin y / y) (𝓝[≠] (0 : ℝ)) (nhds 1) := by
      have h := Real.hasDerivAt_sin 0
      rw [Real.cos_zero] at h
      have h2 := hasDerivAt_iff_tendsto_slope.mp h
      refine h2.congr ?_
      intro y
      rw [slope_def_field]
      simp
    -- x_N = πk/N → 0 within nonzero values
    have hx0 : Filter.Tendsto (fun N : ℕ => Real.pi * (k : ℝ) / (N : ℝ)) Filter.atTop
        (nhds 0) := tendsto_const_div_atTop_nhds_zero_nat (Real.pi * (k : ℝ))
    have hxmem : ∀ᶠ N : ℕ in Filter.atTop,
        Real.pi * (k : ℝ) / (N : ℝ) ∈ ({0}ᶜ : Set ℝ) := by
      filter_upwards [Filter.eventually_ge_atTop 1] with N hN
      have hNpos : (0 : ℝ) < (N : ℝ) := by exact_mod_cast hN
      have hpos : 0 < Real.pi * (k : ℝ) / (N : ℝ) :=
        div_pos (mul_pos Real.pi_pos hk') hNpos
      simp only [Set.mem_compl_iff, Set.mem_singleton_iff]
      exact ne_of_gt hpos
    have hx : Filter.Tendsto (fun N : ℕ => Real.pi * (k : ℝ) / (N : ℝ)) Filter.atTop
        (𝓝[≠] (0 : ℝ)) :=
      tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within _ hx0 hxmem
    have hcomp := hslope.comp hx
    simp only [Function.comp_def] at hcomp
    have hmul : Filter.Tendsto
        (fun N : ℕ => (2 * Real.pi * (k : ℝ)) ^ 2
          * (Real.sin (Real.pi * (k : ℝ) / (N : ℝ)) / (Real.pi * (k : ℝ) / (N : ℝ))) ^ 2)
        Filter.atTop (nhds ((2 * Real.pi * (k : ℝ)) ^ 2 * 1 ^ 2)) :=
      tendsto_const_nhds.mul (hcomp.pow 2)
    rw [one_pow, mul_one] at hmul
    refine hmul.congr' ?_
    filter_upwards [Filter.eventually_ge_atTop 1] with N hN
    have hNpos : (0 : ℝ) < (N : ℝ) := by exact_mod_cast hN
    have hN0 : (N : ℝ) ≠ 0 := ne_of_gt hNpos
    have hπk : Real.pi * (k : ℝ) ≠ 0 := ne_of_gt (mul_pos Real.pi_pos hk')
    simp only [discreteEigenvalue]
    field_simp
    ring
MODEL lichnerowiczFlatEigenvalue · IndisputableMonolith/Gravity/SevenGaps/DiscreteLichnerowicz.lean
lichnerowiczFlatEigenvalue · IndisputableMonolith/Gravity/SevenGaps/DiscreteLichnerowicz.lean:471 
/-- MODEL. Flat-background Lichnerowicz eigenvalue on the wavenumber-`k` TT
plane wave: `(2πk)²`.

Justification (why this is the honest definition): the Lichnerowicz operator
on a Ricci-flat background acts on TT perturbations as
`Δ_L h_ab = -∇² h_ab - 2 R_acbd h^cd`. On the FLAT 3-torus the Riemann
tensor vanishes identically, so `Δ_L` reduces to `-∇²` (minus the flat
Laplacian) on TT tensors. The TT plane wave with wavenumber `k` along an
axis of the unit torus has `-∇²` eigenvalue `(2πk)²`; the along-axis part of
this is PROVED above (`continuumProfile_second_deriv`), and the transverse
derivatives vanish because the mode is constant in `y, z`. No curved-space
geometry is formalized here; this definition encodes the flat reduction
only. -/
noncomputable def lichnerowiczFlatEigenvalue (k : ℕ) : ℝ :=
  (2 * Real.pi * (k : ℝ)) ^ 2

What this page does not claim

The theorem does not claim any result for curved backgrounds or quasinormal modes. The theorem does not claim isotropic recovery of the full Lichnerowicz spectrum. The theorem does not claim that the discrete Laplacian is isotropic.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Gravity/SevenGaps/DiscreteLichnerowicz.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND