Gravity Analysis Regge Bloch Fold4 D Bloch Fold11 Axis Ttplus Wave Star Ne Zero

A nonzero fold at a special wave vector

In numerical relativity, the Regge calculus approximates spacetime by a lattice of flat simplices, here four-dimensional triangle hinges. The Recognition Science framework studies a discrete quadratic form, the Bloch fold, which sums contributions from all oriented slots in one lattice cell as a function of a wave vector. The theorem blochFold11_axisTTPlus_waveStar_ne_zero states that at the special wave vector with components (π/2, π/2, π/2, 0), this fold, evaluated on a specific matrix called axisTTPlus, is not zero; in fact it equals -3.

The result is a consistency check. The framework's library of machine-checked theorems proves that this nonzero value follows from exact integer arithmetic, not from approximation. The same calculation also shows that a different matrix, a decoy gauge term, gives -4 + 4√2, also nonzero, which the framework interprets as a sign that discrete gauge invariance holds only up to a finite-difference identity. The theorem is one of several in the same file: it builds on a factorization identity at zero momentum, a bilinearity property, and a structural vanishing result for other difference masks.

What the theorem does not claim is as important as what it does. It does not evaluate the mass-squared Taylor coefficient against the Einstein–Hilbert or transverse-traceless continuum symbol; that comparison remains a future step. It does not prove that the Regge action converges to general relativity in four dimensions, a statement the framework marks as open. And it does not imply anything about the physical existence of gravitational waves; the wave vector here is a mathematical parameter in a lattice calculation, not a physical momentum.

For the general reader, the practical takeaway is that this is a small, precisely stated building block in a larger research program. The framework's library checks each step with a proof assistant, so the arithmetic is reliable. But the leap from this lattice calculation to continuum physics is not made here, and the framework does not pretend otherwise.

/-- Nonvacuity of the finite-momentum fold on axis TT. -/
theorem blochFold11_axisTTPlus_waveStar_ne_zero :
    blochFold11 axisTTPlus waveStar ≠ 0 := by
  rw [blochFold11_axisTTPlus_waveStar]; norm_num

What this page does not claim

The theorem does not evaluate the m² Taylor coefficient against the Einstein–Hilbert or transverse-traceless continuum symbol. The theorem does not prove S_RS_converges_EH_4d. The theorem does not establish any property of physical gravitational waves.

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