Encyclopedia Gravity Gravity Seven Gaps Discrete Lichnerowicz Polarizations Linear Independent

ARTICLE 3 claims 3 theorems

Gravity Seven Gaps Discrete Lichnerowicz Polarizations Linear Independent

A machine-checked proof that the two standard gravitational wave polarizations are distinct, and why that is only a small piece of the story.

Verify this page

The two polarizations

In general relativity, gravitational waves have two independent polarization states, often called plus and cross. The declaration polarizations_linearIndependent is a machine-checked proof that the two 3 by 3 matrices representing these states, epsPlus and epsCross, are linearly independent over the complex numbers. This means neither can be written as a scalar multiple of the other; they are genuinely different directions in the space of possible wave shapes. The proof is part of a larger effort to connect a discrete lattice model of gravity to the continuous theory.

The two matrices are simple to write down. The plus polarization has entries 1 and -1 on the second and third diagonal positions, with zeros elsewhere. The cross polarization has entries 1 in the second row, third column and third row, second column, with zeros elsewhere. The theorem also proves each matrix is symmetric, has zero trace, and has a zero first row and first column. These properties match the standard transverse-traceless gauge conditions used in general relativity.

The linear independence result is a small but necessary step in a larger proof. The framework's library, a machine-checked collection of formal theorems, uses these polarizations to build plane wave solutions on a discrete lattice. The key convergence theorem, discrete_tt_spectrum_converges_to_flat_lichnerowicz, shows that the eigenvalues of these discrete waves approach the continuum value (2πk)² as the lattice spacing shrinks to zero. This is the first genuine connection between a discrete perturbation spectrum and the continuum Lichnerowicz operator, but it is limited to waves traveling along one axis.

In Recognition Science, this work is part of the Seven-Gaps campaign, a program to close seven identified gaps between discrete and continuous gravity. The linear independence proof is a foundational piece, but it does not by itself establish anything about curved spacetime. The framework explicitly marks curved backgrounds and quasinormal mode spectra as open problems. The flat-space reduction of the Lichnerowicz operator to the Laplacian is a definitional choice, not a curved-space theorem.

The practical consequence is that the discrete model has the correct number of independent wave polarizations, matching the continuum theory. This is a necessary condition for the discrete model to be a faithful representation of gravity, though not a sufficient one. The proof ensures that the two polarizations do not collapse into one another on the lattice, preserving the physical degrees of freedom.

THEOREM polarizations_linearIndependent · IndisputableMonolith/Gravity/SevenGaps/DiscreteLichnerowicz.lean
polarizations_linearIndependent · IndisputableMonolith/Gravity/SevenGaps/DiscreteLichnerowicz.lean:408 
/-- THEOREM. The two standard polarizations are linearly independent over ℂ:
they span the 2D TT polarization space for the axis wave. -/
theorem polarizations_linearIndependent :
    LinearIndependent ℂ ![epsPlus, epsCross] := by
  rw [linearIndependent_fin2]
  constructor
  · intro h
    have h12 : (![epsPlus, epsCross] 1) 1 2 = (0 : Matrix (Fin 3) (Fin 3) ℂ) 1 2 := by
      rw [h]
    have e1 : (![epsPlus, epsCross] 1) 1 2 = (1 : ℂ) := rfl
    have e2 : ((0 : Matrix (Fin 3) (Fin 3) ℂ) 1 2 : ℂ) = 0 := rfl
    rw [e1, e2] at h12
    exact one_ne_zero h12
  · intro a h
    have h11 : (a • ![epsPlus, epsCross] 1) 1 1 = (![epsPlus, epsCross] 0) 1 1 := by
      rw [h]
    have e1 : (a • ![epsPlus, epsCross] 1) 1 1 = a * 0 := rfl
    have e2 : ((![epsPlus, epsCross] 0) 1 1 : ℂ) = 1 := rfl
    rw [e1, e2, mul_zero] at h11
    exact zero_ne_one h11
THEOREM epsPlus_isSymm · epsCross_isSymm · epsPlus_traceless · epsCross_traceless · epsPlus_row0 · epsCross_row0 · IndisputableMonolith/Gravity/SevenGaps/DiscreteLichnerowicz.lean
epsPlus_isSymm · IndisputableMonolith/Gravity/SevenGaps/DiscreteLichnerowicz.lean:374 
theorem epsPlus_isSymm : epsPlus.IsSymm := by
  ext i j
  fin_cases i <;> fin_cases j <;> simp [epsPlus]
epsCross_isSymm · IndisputableMonolith/Gravity/SevenGaps/DiscreteLichnerowicz.lean:378 
theorem epsCross_isSymm : epsCross.IsSymm := by
  ext i j
  fin_cases i <;> fin_cases j <;> simp [epsCross]
epsPlus_traceless · IndisputableMonolith/Gravity/SevenGaps/DiscreteLichnerowicz.lean:382 
theorem epsPlus_traceless : Matrix.trace epsPlus = 0 := by
  rw [Matrix.trace_fin_three]
  show (0 : ℂ) + 1 + (-1) = 0
  norm_num
epsCross_traceless · IndisputableMonolith/Gravity/SevenGaps/DiscreteLichnerowicz.lean:387 
theorem epsCross_traceless : Matrix.trace epsCross = 0 := by
  rw [Matrix.trace_fin_three]
  show (0 : ℂ) + 0 + 0 = 0
  norm_num
epsPlus_row0 · IndisputableMonolith/Gravity/SevenGaps/DiscreteLichnerowicz.lean:392 
theorem epsPlus_row0 : ∀ j, epsPlus 0 j = 0 := by
  intro j
  fin_cases j <;> simp [epsPlus]
epsCross_row0 · IndisputableMonolith/Gravity/SevenGaps/DiscreteLichnerowicz.lean:396 
theorem epsCross_row0 : ∀ j, epsCross 0 j = 0 := by
  intro j
  fin_cases j <;> simp [epsCross]
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

What this page does not claim

The proof does not establish anything about curved spacetime or quasinormal modes. The flat-space reduction of the Lichnerowicz operator is a definitional choice, not a curved-space theorem. The convergence result is limited to waves traveling along one axis, not isotropic recovery.

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