Gravity No Graviton Lattice Matches Continuum

The lattice and the continuum agree

In general relativity, gravitational waves have two independent polarizations, often called plus and cross. This is a counting statement: the mathematics of a symmetric, traceless, transverse tensor in three spatial dimensions leaves exactly two free components. The declaration lattice_matches_continuum proves that a discrete lattice model of spacetime, built from a finite set of points, produces the same count of two. The theorem is a formal equality in the machine-checked library of formal theorems: the number of gravitational wave modes on the lattice equals the number of polarizations in the continuum.

The lattice count comes from a simple bookkeeping of constraints. A symmetric tensor in D dimensions has D(D+1)/2 components. Subtracting one trace constraint and D gauge constraints leaves the physical modes. In three dimensions this is 6 minus 1 minus 3, which equals 2. The continuum count uses the same formula. The theorem states that these two numbers are equal, and the proof is a direct computation verified by the kernel of the proof assistant.

This agreement is a consistency check, not a derivation of new physics. It shows that the discrete lattice does not introduce extra gravitational wave polarizations beyond what general relativity predicts. The framework's claim is that gravity is emergent curvature of the lattice, not a force mediated by a spin-2 particle. The theorem supports that picture by showing the lattice reproduces a known continuum result, but it does not by itself prove that gravity is emergent or that the lattice is the correct description of spacetime.

In Recognition Science, the gravitational coupling constant is defined as κ = 8φ⁵, where φ is the golden ratio. This is an algebraic number derived from the framework's cost function, not a free parameter. The framework also predicts a specific value for the Bose-Marletto-Vedral entanglement rate, approximately 88.7, which is a falsifiable prediction distinguishing emergent from particle-mediated gravity. The lattice_matches_continuum theorem does not address these predictions; it only establishes the polarization count agreement.

/-- Lattice and continuum agree on polarization count. -/
theorem lattice_matches_continuum :
    lattice_gw_modes 3 = gw_polarization_count 3 := by
  rw [lattice_gw_modes_eq_two, gw_polarizations_eq_two]

/-- For D=3: lattice GW modes = 6 - 1 - 3 = 2. -/
theorem lattice_gw_modes_eq_two : lattice_gw_modes 3 = 2 := by
  native_decide

/-- In D = 3 spatial dimensions, there are exactly 2 GW polarizations. -/
theorem gw_polarizations_eq_two : gw_polarization_count 3 = 2 := by native_decide

theorem gravity_not_force_mediated : gravity_is_emergent := ZeroParameterGravity.kappa_pos

/-- κ is a polynomial function of φ alone. -/
theorem kappa_from_phi_alone :
    ZeroParameterGravity.kappa_rs = 8 * phi ^ 5 :=
  ZeroParameterGravity.kappa_rs_closed_form

/-- BMV coupling is in the predicted numerical band (85.6, 90.4). -/
theorem BMV_coupling_bounds : 85.6 < BMV_coupling ∧ BMV_coupling < 90.4 :=
  ZeroParameterGravity.kappa_bounds

What this page does not claim

The theorem does not prove that gravity is emergent; it only shows a consistency between the lattice and continuum polarization counts. The theorem does not derive the value of the gravitational coupling constant or the BMV prediction. The theorem does not address whether the lattice model is the correct or unique description of spacetime.

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/NoGraviton.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: