Gravity Analysis Regge Bloch Fold4 D Bloch Fold11 Decoy Gauge Wave Star Ne Zero

A gauge check at one wave vector

In lattice gauge theory, a gauge symmetry is a transformation that leaves the physics unchanged. On a discrete grid, such symmetries often hold exactly at zero momentum, the limit of infinite wavelength, but can break down when momentum is finite. The declaration blochFold11_decoyGauge_waveStar_ne_zero is a machine-checked theorem about one such finite-momentum case in a four-dimensional Regge lattice model.

The theorem evaluates a specific quantity, called blochFold11, at a particular wave vector waveStar. This quantity is a sum over 240 oriented slots, each slot representing a triangle hinge in a single lattice cell, with phases assigned according to the wave vector. The wave vector chosen has components (π/2, π/2, π/2, 0), meaning the field varies on the scale of the lattice spacing itself. The theorem states that for a particular gauge transformation, called decoyGauge, the value of this sum is -4 + 4√2, which is nonzero.

The nonzero value is the point. It proves that the decoy gauge transformation is not an exact symmetry at this finite momentum. The gauge invariance that holds at zero momentum does not survive unchanged when the field varies rapidly. Instead, the statement says the failure is controlled: it equals a specific finite-difference identity, not an arbitrary error. This is a precise, quantitative statement about how a discrete symmetry degrades away from the long-wavelength limit.

The theorem is part of a larger verification campaign in the framework's machine-checked library of formal theorems. The library confirms that all named theorems in this file are kernel-checked, with no gaps, no admitted axioms, and no trivial shells. The specific declaration is one of several closing values that pin down the behavior of the model at this wave vector. It does not, however, connect this result to the continuum Einstein-Hilbert action, nor does it prove that the full lattice theory converges to general relativity.

What the result changes is the understanding of gauge symmetry on a lattice. It shows that a symmetry can be exact at zero momentum, fail at finite momentum, and yet fail in a way that is itself exactly computable. This is a concrete check on how discretization distorts the symmetries of continuous spacetime, a question that matters for any attempt to build quantum gravity from lattice building blocks.

/-- 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

/-- 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

/-- Certificate sum for axis TT at `m⋆`: `-3`. -/
theorem sum_axisStarContrib :
    (∑ s : Fin 24, ∑ t : Fin 10, axisStarContrib s t) = (-3 : ℝ) := by
  unfold axisStarContrib
  set a : ℝ := -Real.sqrt 2 / 8
  set b : ℝ := -1 / 4 + Real.sqrt 2 / 8
  have hterm : ∀ s t,
      (if axisStarKind s t = 1 then a
        else if axisStarKind s t = 2 then b else (0 : ℝ)) =
        a * (if axisStarKind s t = 1 then (1 : ℝ) else 0) +
          b * (if axisStarKind s t = 2 then (1 : ℝ) else 0) := by
    intro s t
    have hk : axisStarKind s t ≤ 2 := by
      unfold axisStarKind; split_ifs <;> simp
    match h : axisStarKind s t with
    | 0 => simp
    | 1 => simp
    | 2 => simp
    | n + 3 => omega
  simp_rw [hterm, Finset.sum_add_distrib, ← Finset.mul_sum]
  have hc1 :
      (∑ s : Fin 24, ∑ t : Fin 10,
          if axisStarKind s t = 1 then (1 : ℝ) else 0) = 12 := by
    simpa [Nat.cast_sum] using
      congrArg (fun n : ℕ => (n : ℝ)) axisStarKind_count1
  have hc2 :
      (∑ s : Fin 24, ∑ t : Fin 10,
          if axisStarKind s t = 2 then (1 : ℝ) else 0) = 12 := by
    simpa [Nat.cast_sum] using
      congrArg (fun n : ℕ => (n : ℝ)) axisStarKind_count2
  rw [hc1, hc2]
  -- a*12 + b*12 = -3
  unfold a b
  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 S_RS_converges_EH_4d, the convergence of the lattice action to general relativity. This does not flip gap_action_recovery, a separate recovery statement in the campaign.

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: