Gravity Analysis Regge Bloch Fold4 D Phased Class Dot Transported Deficit

The phased class dot

The phased class dot, a weighted sum that assigns a number to each of 15 possible displacement patterns, is the core object in a four-dimensional Regge calculus model. Regge calculus approximates curved spacetime by flat triangular pieces, like a geodesic dome approximating a sphere. The declaration in question, phasedClassDot_transportedDeficit, is a formal definition inside the Recognition Science framework's machine-checked library of formal theorems. It takes a vector of weights, a 4-by-4 matrix representing the metric, and a wave vector, then sums over all 15 displacement patterns the product of the weight and a plane-wave perturbed deficit angle.

What the library proves is a set of exact algebraic identities about this object at a special wave vector, called waveStar, where three of the four momentum components are π/2 and the fourth is zero. At that point, the sum over all 72 oriented slots of the axis contribution equals -3, a nonzero value that rules out the possibility that the expression is identically zero. The gauge contribution equals -4 + 4√2, also nonzero. Each term in the sum is an integer multiple of π/4 in its phase, so every slot term can be written as (N₁ + N₂·√2)/8 with decidable integers. The library proves these integer certificates match the natural-number tables on all 240 oriented slots, a closed geometric-to-certificate correspondence.

The framework's library also proves that at zero momentum, the factorized phased fold equals the committed orbit-zero-momentum quadratic, a consistency gate. It proves bilinearity of the fold in the metric matrix, and it proves that two difference masks give identically zero contributions for every wave vector, meaning those area supports miss the axis-TT class loads entirely. The axiom footprint is exactly the three standard axioms of the ambient type theory: propositional extensionality, choice, and quotient soundness, with no framework-specific axioms added.

In Recognition Science, this is one step in a campaign toward quantum gravity. The declaration establishes a precise, machine-checked algebraic fact about a discrete model at one special momentum configuration. It does not claim the model reproduces Einstein-Hilbert gravity in the continuum limit; that comparison is explicitly deferred to a later lane. It does not prove the convergence of the recognition-science action to the Einstein-Hilbert action in four dimensions. It does not establish that the gap action recovery works. The result is a closed, exact computation about a discrete object, not a physical claim about the continuum.

What a reader can take away is that the framework has produced a fully verified algebraic structure for a finite-momentum Bloch fold, with every phase an integer multiple of π/4 and every certificate an integer combination of 1 and √2. This is the kind of exact, checkable scaffolding that a larger physical claim would need to stand on. The honesty of the declaration is that it names precisely what it does not yet do: it does not bridge to the continuum, and it does not claim the convergence that would make it a statement about observed gravity.

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

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

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

This declaration does not evaluate the m² Taylor coefficient against the Einstein-Hilbert or TT continuum symbol. This declaration does not prove S_RS_converges_EH_4d. This declaration does not flip gap_action_recovery.

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: