Gravity Analysis Regge Exact Flat Hessian Bloch Symbol Zero4 D Coupling Weight E

The quartic identity

The declaration couplingWeight_eq_quartic is a formal theorem in the Recognition Science framework's machine-checked library of formal theorems. It states that for any 4x4 matrix H and any coupling in the framework's table, the coupling weight can be written as a sum of quartic monomials. Each monomial is a product of four entries of H, multiplied by a rational coefficient that depends on the coupling. This is a rewriting identity: it expresses one quantity in terms of another, nothing more.

The identity matters because it is the first step in a larger proof. The library also proves that every one of those rational coefficients is exactly zero. When you sum the quartic terms with zero coefficients, the whole sum collapses to zero. The final theorem, exactMidpointBlochSymbolZero_eq_zero, states that the exact midpoint Bloch symbol vanishes at zero momentum for every H. The quartic identity is the bridge that lets the proof pass from the definition of the symbol to the zero result.

In Recognition Science, the framework models gravity through a discrete ledger of recognition events. The coupling weight is a numerical weight assigned to a coupling in that ledger. The theorem does not say anything about the physical meaning of the weight, only that it can be expanded algebraically. It does not claim that the quartic form has any special geometric interpretation, nor that the zero result extends to nonzero momentum. The vanishing is proved only at zero momentum, and only for the exact midpoint symbol, not for other symbols the framework may define.

What the theorem gives the reader is a precise algebraic fact: a certain sum of products of matrix entries and rational coefficients is identically zero. It is a tool, not a physical law. Its value is that it closes a gap in the framework's chain of reasoning, showing that the zero-momentum symbol carries no residual coupling weight. That is the consequence: the framework's gravity model has no spurious coupling contribution at zero momentum, at least for this symbol.

private theorem couplingWeight_eq_quartic (H : Mat4) (coup : Coupling) :
    couplingWeight H coup =
      ∑ a : Fin 4, ∑ b : Fin 4, ∑ c : Fin 4, ∑ d : Fin 4,
        couplingMonomial coup a b c d * H a b * H c d := by
  unfold couplingWeight couplingMonomial
  rw [← couplingS_eq_s]
  have hre :
      (1 / 2 : ℝ) * (couplingS coup : ℝ) * edgeStrain H coup.De * edgeStrain H coup.Dep =
        ((1 / 2 : ℝ) * (couplingS coup : ℝ)) *
          (edgeStrain H coup.De * edgeStrain H coup.Dep) := by
    ring
  rw [hre, edgeStrain_mul_edgeStrain]
  simp_rw [Finset.mul_sum]
  refine Finset.sum_congr rfl fun _ _ => Finset.sum_congr rfl fun _ _ =>
    Finset.sum_congr rfl fun _ _ => Finset.sum_congr rfl fun _ _ => ?_
  ring

private theorem couplingWeight_eq_quartic (H : Mat4) (coup : Coupling) :
    couplingWeight H coup =
      ∑ a : Fin 4, ∑ b : Fin 4, ∑ c : Fin 4, ∑ d : Fin 4,
        couplingMonomial coup a b c d * H a b * H c d := by
  unfold couplingWeight couplingMonomial
  rw [← couplingS_eq_s]
  have hre :
      (1 / 2 : ℝ) * (couplingS coup : ℝ) * edgeStrain H coup.De * edgeStrain H coup.Dep =
        ((1 / 2 : ℝ) * (couplingS coup : ℝ)) *
          (edgeStrain H coup.De * edgeStrain H coup.Dep) := by
    ring
  rw [hre, edgeStrain_mul_edgeStrain]
  simp_rw [Finset.mul_sum]
  refine Finset.sum_congr rfl fun _ _ => Finset.sum_congr rfl fun _ _ =>
    Finset.sum_congr rfl fun _ _ => Finset.sum_congr rfl fun _ _ => ?_
  ring

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

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

What this page does not claim

The theorem does not claim the quartic form has any geometric meaning. It does not claim the Bloch symbol vanishes at nonzero momentum. It does not claim the coupling weight itself is zero, only that its quartic expansion has zero coefficients.

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: