Gravity Analysis Regge Edge Stencil4 D Finite Ttquadratic Eq Bilinear

A finite probe of gravity's edge

In numerical relativity, a Regge stencil is a recipe for approximating the curvature of spacetime by looking at the edges of a four-dimensional grid. The declaration finiteTTQuadratic is a specific such recipe: it takes a small disturbance of the grid, measures the response along fifteen different edge directions, squares each response, and adds them up. The companion object finiteTTBilinear does the same for two disturbances at once, multiplying their responses before summing. The key equation, proved in the machine-checked library of formal theorems, is the polarization identity: the quadratic form on a sum equals the sum of the individual quadratics plus twice the bilinear cross term, exactly as in ordinary algebra.

This identity matters because it is the first step toward understanding how the grid's energy responds to combinations of disturbances. The library proves that the quadratic form is symmetric, that it vanishes on the zero disturbance, and that it is even under sign reversal. It also evaluates the form on three test disturbances: a pure trace, a pure gauge, and a transverse-traceless seed. The pure trace gives 80, the pure gauge gives 32, and the transverse-traceless seed gives a nonzero 8. These numbers are not physics yet; they are checks that the formula behaves as a well-defined algebraic object.

The honest limits are sharp. The weights attached to the fifteen edge classes are all set to 1, a provisional choice; the true weights of the four-dimensional Regge Hessian are an open problem. The form is not gauge invariant: a pure gauge disturbance produces a nonzero value of 32, so the identity that holds is recorded explicitly rather than claimed to vanish. This does not prove convergence to the Einstein-Hilbert action, does not complete the ledger name edge_tt_decomposition (a discrete record of how transverse-traceless pieces separate), and does not recover the gap action. What is established is a finite, exact algebraic scaffold on which later increments can build.

/-- Exact quadratic expansion / polarization identity. -/
theorem finiteTTQuadratic_add (A B : Mat4) :
    finiteTTQuadratic (A + B) =
      finiteTTQuadratic A + finiteTTQuadratic B + 2 * finiteTTBilinear A B := by
  unfold finiteTTQuadratic finiteTTBilinear
  have h :
      ∀ d : Fin 15,
        classCoeff (A + B) d ^ 2 =
          classCoeff A d ^ 2 + classCoeff B d ^ 2 +
            2 * (classCoeff A d * classCoeff B d) := by
    intro d
    rw [classCoeff_add]
    ring
  simp_rw [h, Finset.sum_add_distrib, Finset.mul_sum]

theorem sum_weightSqNat : (∑ d : Fin 15, classWeightNat d ^ 2) = 80 := by
  unfold classWeightNat classBit maskOf
  decide

theorem finiteTTQuadratic_gaugePart_axisWave :
    finiteTTQuadratic (gaugePart axisWave axisGaugeVector) = 32 := by
  unfold finiteTTQuadratic
  have hterm :
      ∀ d : Fin 15,
        classCoeff (gaugePart axisWave axisGaugeVector) d ^ 2 =
          (4 : ℝ) * (hasBit0 d : ℝ) := by
    intro d
    rw [classCoeff_gaugePart_axis]
    unfold hasBit0
    cases classBit d 0 <;> norm_num
  simp_rw [hterm, ← Finset.mul_sum, ← Nat.cast_sum, sum_hasBit0]
  norm_num

theorem finiteTTQuadratic_axisTTPlus_isTT_seed :
    IsTT axisWave axisTTPlus ∧ finiteTTQuadratic axisTTPlus ≠ 0 :=
  ⟨axisTTPlus_isTT, finiteTTQuadratic_axisTTPlus_ne_zero⟩

theorem finiteTTQuadratic_gaugePart_axisWave_ne_zero :
    finiteTTQuadratic (gaugePart axisWave axisGaugeVector) ≠ 0 := by
  rw [finiteTTQuadratic_gaugePart_axisWave]
  norm_num

What this page does not claim

This does not prove convergence to the Einstein-Hilbert action in four dimensions. This does not establish gauge invariance of the provisional quadratic form. This does not complete the ledger decomposition of transverse-traceless edge modes.

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/Analysis/ReggeEdgeStencil4D.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: