Gravity Analysis Regge Edge Stencil4 D Finite Ttquadratic Axis Ttplus

The finite quadratic probe

In numerical relativity, a Regge edge stencil is a discrete pattern used to probe how spacetime geometry responds to small disturbances. The Recognition Science framework's machine-checked library of formal theorems has built a four-dimensional version of such a stencil. It examines fifteen distinct displacement classes, each a nonzero vector whose components are only 0 or 1, drawn from the corners of a four-dimensional hypercube. For each class, the calculation assigns a coefficient based on a plane-wave perturbation, then squares and sums those coefficients to form a single number called the finite quadratic, a discrete record of how strongly the disturbance registers.

The declaration finiteTTQuadratic_axisTTPlus establishes a concrete, non-vacuous result. It proves that for a particular perturbation named axisTTPlus, the finite quadratic is not zero. This matters because axisTTPlus belongs to a special family of perturbations called transverse-traceless, the kind gravitational waves represent. The theorem bundles two facts: that axisTTPlus is indeed transverse-traceless, and that its finite quadratic evaluates to 8, a nonzero value. This shows the probe is sensitive to at least one physically meaningful disturbance in four dimensions, not blind to it.

The declaration also carries explicit limits. It does not prove that the full Recognition Science action converges to the Einstein-Hilbert action of general relativity in four dimensions. It does not establish that the finite quadratic is gauge invariant; in fact, the library records that pure gauge loads produce a nonzero value of 32, so exact gauge invariance fails for this provisional aggregate. The weights used in the sum, all equal to one, are provisional; the true weights from the four-dimensional Regge Hessian remain an open problem. The declaration is a stepping stone, not a destination.

What the result changes is the practical setting for further work. It gives researchers a concrete, kernel-checked anchor: a specific transverse-traceless perturbation that the finite quadratic detects. It also provides decoy values, 32 for pure gauge and 80 for pure trace, that future refinements must distinguish from the physical 8. The declaration thus sharpens the target for deriving correct four-dimensional weights, turning an abstract open question into a measurable gap between provisional and correct behavior.

theorem finiteTTQuadratic_axisTTPlus_ne_zero :
    finiteTTQuadratic axisTTPlus ≠ 0 := by
  rw [finiteTTQuadratic_axisTTPlus]
  norm_num

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

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 declaration does not prove convergence to the Einstein-Hilbert action in four dimensions. The declaration does not establish gauge invariance of the finite quadratic. The declaration does not derive the true four-dimensional Regge 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: