Gravity Analysis Regge Exact Flat Hessian Bloch Symbol Zero4 D Q Coeff Cast Eq S

A coefficient identity

In the framework's machine-checked library of formal theorems, a ledger (a discrete record of events) can carry weights on its edges. The declaration qCoeff_cast_eq_sum is a tiny but necessary bridge between two ways of writing the same number. On one side stands a rational coefficient qCoeff that appears in a quartic form; on the other side stands a sum of real-valued monomials, one per coupling in a fixed table. The theorem says these two expressions are equal after casting the rational to a real.

Why does that matter? The library wants to prove that a certain zero-momentum symbol vanishes for every matrix H. It expands that symbol into a sum of quartic terms, each multiplied by a coefficient. If every coefficient is zero, the whole sum collapses. The coefficients are rational numbers, but the monomials are real. The identity qCoeff_cast_eq_sum lets the proof move freely between the rational and real viewpoints, so a certificate that each rational coefficient is zero can be lifted to the real sum. Without this bridge, the expansion would stall at a type mismatch.

The declaration does not claim that the quartic form vanishes, nor that the symbol vanishes. Those are separate theorems that come later in the file. It also does not claim anything about the physical meaning of the couplings or about gravity itself. It is a formal rewriting lemma, pure algebra, with no physics content beyond the names it carries.

private theorem qCoeff_cast_eq_sum (a b c d : Fin 4) :
    (qCoeff a b c d : ℝ) =
      ∑ i : CouplingIdx, couplingMonomial couplingTable[i] a b c d := by
  unfold qCoeff couplingMonomial
  rw [Rat.cast_sum]
  refine Finset.sum_congr rfl fun _ _ => ?_
  push_cast
  ring

private theorem factor_HabHcd (H : Mat4) (a b c d : Fin 4) :
    (∑ i : CouplingIdx,
        couplingMonomial couplingTable[i] a b c d * H a b * H c d) =
      (qCoeff a b c d : ℝ) * H a b * H c d := by
  have hα :
      ∀ i : CouplingIdx,
        couplingMonomial couplingTable[i] a b c d * H a b * H c d =
          couplingMonomial couplingTable[i] a b c d * (H a b * H c d) := by
    intro i; ring
  simp_rw [hα]
  rw [← Finset.sum_mul, ← qCoeff_cast_eq_sum]
  ring

What this page does not claim

The declaration does not assert that any quartic form vanishes. The declaration does not assert that the zero-momentum symbol vanishes. The declaration does not assign physical meaning to the couplings.

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: