Encyclopedia Gravity Gravity Analysis Regge Bloch Fold4 D Factorized Bloch Fold11 Zero Momentum

ARTICLE 3 claims 3 theorems

Gravity Analysis Regge Bloch Fold4 D Factorized Bloch Fold11 Zero Momentum

A machine-checked identity shows that, at zero momentum, a factorized gravity expression exactly matches the committed quadratic form, a consistency gate for a much larger program.

Verify this page

The zero-momentum identity

In numerical relativity and lattice quantum gravity, a central task is to approximate the continuous Einstein equations by discrete sums over small geometric cells. One approach, Regge calculus, replaces smooth spacetime with a network of flat triangular pieces, and the curvature is concentrated along the hinges where triangles meet. The declaration factorizedBlochFold11_zeroMomentum is a theorem in the Recognition Science framework's machine-checked library of formal theorems: it proves that a particular factorized expression, built from plane-wave phases and hinge data, equals the committed zero-momentum quadratic form for the type-(1,1) orbit.

The identity is a consistency gate. The framework defines two different-looking objects: a factorized fold that multiplies phase factors cell by cell, and a quadratic form that was committed earlier as the target for one orbit type. The theorem states that, when the wave vector is set to zero, these two objects are exactly equal for every 4x4 matrix H. The proof is fully checked by the kernel, with no axioms beyond the standard three [propext, Classical.choice, Quot.sound], and no "sorry" or "admit" gaps. It is a precise, finite algebraic statement, not a numerical approximation.

The theorem also carries structural information. At a special wave vector with three components equal to pi/2 and one equal to zero, the axis contribution sums to -3 and the gauge contribution to -4 + 4√2, both nonzero, which shows the fold is not vacuous. Every midpoint phase at that wave vector is a natural multiple of pi/4, so each slot term lands in the ring (N1 + N2√2)/8 with decidable integers. The geometric certificates match the integer tables on all 240 oriented slots, closing the loop between geometry and algebra.

What the theorem does not do is equally important. It does not evaluate the m² Taylor coefficient against the Einstein-Hilbert or transverse-traceless continuum symbol; that is a separate, later step. It does not prove that the full Recognition Science action converges to the Einstein-Hilbert action in four dimensions, a goal named S_RS_converges_EH_4d and still open. It does not flip the gap_action_recovery flag. The identity is a necessary consistency check, not a physical derivation.

THEOREM factorizedBlochFold11_zeroMomentum · IndisputableMonolith/Gravity/Analysis/ReggeBlochFold4D.lean
factorizedBlochFold11_zeroMomentum · IndisputableMonolith/Gravity/Analysis/ReggeBlochFold4D.lean:154 
/-- Consistency gate: factorized fold at zero momentum recovers the
committed `(1,1)` orbit quadratic. -/
theorem factorizedBlochFold11_zeroMomentum (H : Mat4) :
    factorizedBlochFold11 H (fun _ => (0 : ℝ)) =
      orbitZeroMomQuadratic .t11 H := by
  unfold factorizedBlochFold11 orbitZeroMomQuadratic orbitCellCount
    orbitAreaCov orbitDeficitKernel
  have hterm : ∀ s t,
      factorizedSlotTerm H (fun _ => (0 : ℝ)) s t =
        (if isT11 s t then (1 : ℝ) else 0) *
          (classDot areaCov11 H *
            classDot ReggeHinge4DStarKernel.fullStarClassKernel H) := by
    intro s t
    unfold factorizedSlotTerm
    by_cases h : isT11 s t <;> simp [h, phasedClassDot_zeroMomentum]
  simp_rw [hterm]
  -- Pull the constant product out of the double sum.
  rw [show
      (∑ s : Fin 24, ∑ t : Fin 10,
          (if isT11 s t then (1 : ℝ) else 0) *
            (classDot areaCov11 H *
              classDot ReggeHinge4DStarKernel.fullStarClassKernel H)) =
        (∑ s : Fin 24, ∑ t : Fin 10, (if isT11 s t then (1 : ℝ) else 0)) *
          (classDot areaCov11 H *
            classDot ReggeHinge4DStarKernel.fullStarClassKernel H) by
    simp_rw [Finset.sum_mul]]
  rw [t11_count_real]
  ring
THEOREM sum_axisStarContrib · sum_gaugeStarContrib · IndisputableMonolith/Gravity/Analysis/ReggeBlochFold4D.lean
sum_axisStarContrib · IndisputableMonolith/Gravity/Analysis/ReggeBlochFold4D.lean:466 
/-- 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
sum_gaugeStarContrib · IndisputableMonolith/Gravity/Analysis/ReggeBlochFold4D.lean:501 
/-- 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
THEOREM cos_quarterTurns · IndisputableMonolith/Gravity/Analysis/ReggeBlochFold4D.lean
cos_quarterTurns · IndisputableMonolith/Gravity/Analysis/ReggeBlochFold4D.lean:587 
/-- Exact table for `cos(k·π/4)`, valid for every natural `k`. -/
theorem cos_quarterTurns (k : ℕ) :
    Real.cos ((k : ℝ) * (Real.pi / 4)) =
      (cosC1 (k % 8) : ℝ) + (cosC2 (k % 8) : ℝ) * (Real.sqrt 2 / 2) := by
  have hmod : ((k % 8 : ℕ) : ℝ) + 8 * ((k / 8 : ℕ) : ℝ) = (k : ℝ) := by
    exact_mod_cast congrArg (fun n : ℕ => (n : ℝ)) (Nat.mod_add_div k 8)
  have hsplit : (k : ℝ) * (Real.pi / 4) =
      ((k % 8 : ℕ) : ℝ) * (Real.pi / 4) +
        ((k / 8 : ℕ) : ℝ) * (2 * Real.pi) := by
    rw [← hmod]; ring
  rw [hsplit,
    (Real.cos_periodic.nat_mul (k / 8)) (((k % 8 : ℕ) : ℝ) * (Real.pi / 4))]
  have h8 : k % 8 = 0 ∨ k % 8 = 1 ∨ k % 8 = 2 ∨ k % 8 = 3 ∨ k % 8 = 4 ∨
      k % 8 = 5 ∨ k % 8 = 6 ∨ k % 8 = 7 := by omega
  rcases h8 with h | h | h | h | h | h | h | h <;> rw [h]
  · norm_num [cosC1, cosC2, Real.cos_zero]
  · norm_num [cosC1, cosC2, Real.cos_pi_div_four]
  · rw [show ((2 : ℕ) : ℝ) * (Real.pi / 4) = Real.pi / 2 by push_cast; ring]
    norm_num [cosC1, cosC2, Real.cos_pi_div_two]
  · rw [show ((3 : ℕ) : ℝ) * (Real.pi / 4) = Real.pi - Real.pi / 4 by
      push_cast; ring]
    rw [Real.cos_pi_sub]
    norm_num [cosC1, cosC2, Real.cos_pi_div_four]
  · rw [show ((4 : ℕ) : ℝ) * (Real.pi / 4) = Real.pi by push_cast; ring]
    norm_num [cosC1, cosC2, Real.cos_pi]
  · rw [show ((5 : ℕ) : ℝ) * (Real.pi / 4) = Real.pi + Real.pi / 4 by
      push_cast; ring]
    rw [Real.cos_add]
    norm_num [cosC1, cosC2, Real.cos_pi, Real.sin_pi, Real.cos_pi_div_four]
  · rw [show ((6 : ℕ) : ℝ) * (Real.pi / 4) = Real.pi + Real.pi / 2 by
      push_cast; ring]
    rw [Real.cos_add]
    norm_num [cosC1, cosC2, Real.cos_pi, Real.sin_pi, Real.cos_pi_div_two]
  · rw [show ((7 : ℕ) : ℝ) * (Real.pi / 4) = 2 * Real.pi - Real.pi / 4 by
      push_cast; ring]
    rw [Real.cos_sub]
    norm_num [cosC1, cosC2, Real.cos_two_pi, Real.sin_two_pi,
      Real.cos_pi_div_four]

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 convergence of the Recognition Science action to Einstein-Hilbert in four dimensions. The theorem does not flip the gap_action_recovery flag.

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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND