Gravity Analysis Regge Edge Stencil4 D Finite Ttquadratic Gauge Part Axis Wave

A gauge test in four dimensions

In numerical approaches to gravity, one common strategy is to approximate spacetime with a grid of simplexes, such as triangles in two dimensions or tetrahedra in three. The Regge calculus, introduced by Tullio Regge in 1961, is the classic framework: it encodes curvature in the lengths of the grid's edges rather than in continuous fields. A key question is whether a discrete approximation built this way respects the symmetries of the continuous theory, especially the freedom to change coordinates without changing the physics, a symmetry known as gauge invariance.

The declaration finiteTTQuadratic_gaugePart_axisWave belongs to a machine-checked library of formal theorems, a collection where every result is verified by a computer proof checker. It concerns a specific four-dimensional construction: a grid based on the four-dimensional cube, with fifteen distinct classes of edge displacements. For each class, the construction defines a coefficient that measures how a perturbation of the metric, encoded in a matrix H, loads that edge. The declaration then forms a quadratic aggregate, essentially a sum of the squares of these coefficients over all fifteen classes.

The theorem itself states that when this aggregate is fed a pure gauge perturbation, a specific coordinate transformation that should have no physical effect, the result is exactly 32. This is a concrete, nonzero number. The significance is negative: a truly gauge-invariant quantity would give zero on a pure gauge input, because gauge transformations should not change the physics. The fact that the aggregate gives 32 means it fails this basic test. The theorem also records a companion result: the bilinear cross-term between a legitimate transverse-traceless perturbation and the gauge perturbation vanishes, which is a partial consistency check.

In Recognition Science, this result is part of a larger campaign to build a discrete theory of gravity from first principles. The framework's library is a growing collection of such machine-checked theorems, and this declaration is a small but honest increment. It does not claim to have found the correct discrete gravity action. It explicitly does not prove that the discrete theory converges to the Einstein-Hilbert action of general relativity. It does not even claim that the weights used in the quadratic aggregate, which are all set to one, are the physically correct ones. Deriving the true weights is listed as an open problem, and the declaration warns against reverse-engineering them from the known continuum answer.

What the theorem does provide is a precise, verified data point: a proposed building block, when tested against a fundamental symmetry, fails. This is useful information. It tells researchers that this particular aggregate, with these provisional weights, cannot serve as a gauge-invariant action by itself. The path forward is not to ignore the failure but to use it as a constraint, guiding the search for the correct weights or a different construction. In this way, a negative result in a formal library is a positive step: it eliminates a wrong turn with certainty, leaving the open problem better defined.

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

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

What this page does not claim

The theorem does not establish gauge invariance for the aggregate; it establishes the opposite. The theorem does not prove convergence to the Einstein-Hilbert action in four dimensions. The theorem does not derive the physically correct edge weights, which remain an open problem.

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: