Gravity Analysis Regge Exact Flat Hessian Bloch Symbol Zero4 D Sum Weight Eq Sum

The zero-momentum identity

The declaration sum_weight_eq_sum_quartic_terms is a formal identity inside the Recognition Science library. It states that a sum of coupling weights, one for each term in a fixed table of interactions, equals a quartic polynomial in the components of a 4 by 4 matrix H. Each coefficient of that polynomial is a rational number built from the table. The identity itself is a theorem, proved by expanding each weight and rearranging the sums.

The point of the identity is what follows from it. A separate theorem, exactMidpointBlochSymbolZero_eq_zero, uses it to show that the exact midpoint Bloch symbol vanishes at zero momentum. That means a particular combination of coupling weights, evaluated at the zero-momentum point, is exactly zero. The proof works by rewriting the symbol as the quartic form, then using the fact that every rational coefficient in that form is zero, a fact certified by a kernel-level computation.

In Recognition Science, the framework models physical structure through a discrete ledger of recognition events, and this identity is part of the analysis of flat space in that model. The declaration does not claim that the quartic form is zero for all matrices H; it claims only that the specific sum of weights equals the form, and that the form's coefficients vanish. It does not assert anything about curved space, about the physical interpretation of the Bloch symbol beyond this algebraic fact, or about the values of the coupling constants themselves.

private theorem sum_weight_eq_sum_quartic_terms (H : Mat4) :
    (∑ i : CouplingIdx, couplingWeight H couplingTable[i]) =
      ∑ a : Fin 4, ∑ b : Fin 4, ∑ c : Fin 4, ∑ d : Fin 4,
        (qCoeff a b c d : ℝ) * H a b * H c d := by
  refine (Finset.sum_congr rfl fun i _ =>
    couplingWeight_eq_quartic H couplingTable[i]).trans ?_
  refine (sum_comm_idx_fin4
      (fun (i : CouplingIdx) (a b c d : Fin 4) =>
        couplingMonomial (couplingTable[i]) a b c d * H a b * H c d)).trans ?_
  refine Finset.sum_congr rfl fun a _ => Finset.sum_congr rfl fun b _ =>
    Finset.sum_congr rfl fun c _ => Finset.sum_congr rfl fun d _ =>
      factor_HabHcd H a b c d

/-- **THEOREM:** the exact midpoint Bloch symbol vanishes at zero momentum. -/
theorem exactMidpointBlochSymbolZero_eq_zero (H : Mat4) :
    exactMidpointBlochSymbolZero H = 0 := by
  rw [exactMidpointBlochSymbolZero_eq_quartic]
  refine Finset.sum_eq_zero fun a _ => Finset.sum_eq_zero fun b _ =>
    Finset.sum_eq_zero fun c _ => Finset.sum_eq_zero fun d _ => ?_
  simp [qCoeff_eq_zero a b c d]

/-- **THEOREM:** every rational quartic coefficient vanishes. -/
theorem qCoeff_eq_zero : ∀ (a b c d : Fin 4), qCoeff a b c d = 0 := by
  intro a b c d
  rw [qCoeff_eq_kernelGlue]
  exact KernelGlue.qCoeff_eq_zero a b c d

What this page does not claim

The quartic form is zero for all matrices H; only the specific sum of weights equals the form. The identity applies to curved space or to any configuration beyond the flat-space setting in which it is proved. The coupling constants in the table are derived or assigned physical values by this declaration.

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