Gravity Analysis Regge Bloch Fold4 D Transported Slot Term Gauge Wave Star

The transported slot term

In the Recognition Science framework's machine-checked library of formal theorems, a ledger (a discrete record of events) is used to model spacetime as a grid of points. The declaration transportedSlotTerm_gauge_waveStar is a theorem about one specific piece of that grid, called a slot. It establishes that, at a particular wave vector (a mathematical description of how a disturbance propagates), the value of a gauge-related term in that slot is exactly equal to an integer plus another integer times the square root of 2, divided by 8. This is not an approximation; it is a proven equality.

The calculation is part of a larger effort to show that the discrete model reproduces the behavior of gravity. The wave vector used, waveStar, has components equal to π/2 for three spatial directions and 0 for time. At this special point, the theorem proves that every phase in the model is a natural multiple of π/4. This fact allows the cosine and sine terms to be evaluated exactly, producing the clean algebraic form. The theorem is one of several that together verify the model's internal consistency at this wave vector.

The theorem is a THEOREM tag claim, meaning it is proved in the Lean 4 proof assistant with no unproven assumptions (no sorry or admit) and no new axioms. The expected axiom footprint is just the three standard axioms of the ambient type theory: propext, Classical.choice, and Quot.sound. The declaration does not claim to evaluate the model against the Einstein-Hilbert action, does not prove that the discrete model converges to general relativity, and does not claim to resolve any physical gauge invariance issue beyond the finite-difference identity.

def gaugeStarContrib (s : Fin 24) (t : Fin 10) : ℝ :=
  if gaugeStarKind s t = 1 then -1 + Real.sqrt 2 else 0

/-- Certificate sum for decoy gauge at `m⋆`: `-4 + 4√2`. -/
theorem sum_gaugeStarContrib :
    (∑ s : Fin 24, ∑ t : Fin 10, gaugeStarContrib s t) =
      -4 + 4 * Real.sqrt 2 := by
  unfold gaugeStarContrib
  set c : ℝ := -1 + Real.sqrt 2
  have hterm : ∀ s t,
      (if gaugeStarKind s t = 1 then c else (0 : ℝ)) =
        c * (if gaugeStarKind s t = 1 then (1 : ℝ) else 0) := by
    intro s t; by_cases h : gaugeStarKind s t = 1 <;> simp [h]
  simp_rw [hterm, ← Finset.mul_sum]
  have hc :
      (∑ s : Fin 24, ∑ t : Fin 10,
          if gaugeStarKind s t = 1 then (1 : ℝ) else 0) = 4 := by
    simpa [Nat.cast_sum] using
      congrArg (fun n : ℕ => (n : ℝ)) gaugeStarKind_count1
  rw [hc]
  unfold c
  ring

What this page does not claim

This does not evaluate the m² Taylor coefficient against the Einstein-Hilbert or TT continuum symbol. This does not prove that the discrete model converges to general relativity (S_RS_converges_EH_4d). This does not resolve the question of discrete gauge invariance at finite momentum beyond the finite-difference identity.

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: