Gravity Analysis Regge Edge Stencil4 D Finite Ttbilinear Axis Ttplus Gauge

A gauge test in four dimensions

In the search for a quantum theory of gravity, physicists often test a mathematical object by checking whether it is gauge-invariant: whether its value stays the same under a transformation that merely relabels the description of the physical system. The declaration finiteTTBilinear_axisTTPlus_gauge concerns a specific bilinear form, a kind of pairing between two matrices, used in a four-dimensional lattice model of gravity. The theorem states that this pairing, evaluated on a particular traceless-transverse matrix and a pure gauge perturbation, equals zero exactly.

The result is part of a larger machine-checked library of formal theorems, a collection of proofs verified by computer. The library's authors are building a discrete model of gravity, where spacetime is approximated by a grid or lattice. The specific declaration is a single, narrow result: it records that the bilinear form is zero for one chosen pair of inputs. This is a precise, kernel-checked statement, meaning it is proved without gaps or unverified assumptions.

The theorem does not claim that the underlying quadratic form, which sums the squares of edge coefficients, is gauge-invariant. In fact, the library explicitly records the opposite: the quadratic form evaluated on a pure gauge input is 32, not zero. This distinction matters. The bilinear form's zero value for this one pair does not imply the full theory respects gauge symmetry. The library's documentation states that exact gauge invariance of the provisional aggregate fails, and it provides an explicit counterexample.

Also, the declaration does not prove that the discrete model converges to the classical Einstein-Hilbert action of general relativity. The library marks that convergence as an open problem. The weights used in the quadratic form are provisional, with all classes weighted equally; the correct weights for the four-dimensional Regge action are not derived here. The theorem is a building block, not a final verdict on the theory.

What the declaration does establish is a concrete, verifiable fact about a specific mathematical construction. It acts as a checkpoint in a long program: it confirms that the bilinear form behaves as expected for one test case, and it helps map the territory of what is and is not gauge-invariant in this discrete approach. For a reader, the takeaway is that this is a small, honest step in a larger investigation, not a claim of a complete theory of quantum gravity.

theorem finiteTTBilinear_axisTTPlus_gauge :
    finiteTTBilinear axisTTPlus (gaugePart axisWave axisGaugeVector) = 0 := by
  unfold finiteTTBilinear
  have hterm :
      ∀ d : Fin 15,
        classCoeff axisTTPlus d *
            classCoeff (gaugePart axisWave axisGaugeVector) d =
          (2 : ℝ) * (crossNat d : ℝ) := by
    intro d
    rw [classCoeff_axisTTPlus, classCoeff_gaugePart_axis]
    unfold crossNat
    cases classBit d 0 <;> cases classBit d 2 <;>
      cases classBit d 3 <;> norm_num
  simp_rw [hterm, ← Finset.mul_sum, ← Int.cast_sum, sum_crossNat]
  norm_num

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_gaugePart_axisWave_ne_zero :
    finiteTTQuadratic (gaugePart axisWave axisGaugeVector) ≠ 0 := by
  rw [finiteTTQuadratic_gaugePart_axisWave]
  norm_num

What this page does not claim

This theorem does not prove that the full discrete model is gauge-invariant. This theorem does not prove convergence to the Einstein-Hilbert action of general relativity. The provisional weights used in the quadratic form are not the final physical weights.

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: