Gravity Analysis Regge Exact Flat Hessian Bloch Symbol Zero4 D Edge Strain Mul E

The algebraic identity

The declaration edgeStrain_mul_edgeStrain is a theorem in the framework's machine-checked library of formal theorems. It establishes an algebraic identity about a quantity called edge strain, a measure of how a discrete geometric edge deforms. The theorem states that the product of two edge strains, one for a direction De and one for Dep, equals a sum over four indices of products of the strain components. In symbols: edgeStrain H De * edgeStrain H Dep = ∑_{a,b,c,d} H a b * H c d * De a * De b * Dep c * Dep d. This is a purely algebraic fact, proved by expanding definitions and rearranging sums.

The identity is a lemma, not an end in itself. It appears in a larger proof that the exact midpoint Bloch symbol, a quantity built from edge strains, vanishes at zero momentum. That vanishing is the main theorem of the file, exactMidpointBlochSymbolZero_eq_zero. The identity edgeStrain_mul_edgeStrain is one step in rewriting the product of strains into a form where the coefficients can be shown to cancel. The proof then uses a separate result, qCoeff_eq_zero, which states that all rational quartic coefficients vanish, to conclude the whole sum is zero.

What the declaration does not claim is equally important. It does not assert anything about the physical meaning of edge strain or the Bloch symbol. It does not say that the vanishing of the Bloch symbol implies anything about gravity in the real world. It is a formal identity about formal objects, proved by computation. The framework's larger claims about gravity rest on many such lemmas, but this single declaration is only a step in the algebra. It also does not claim that the product of edge strains is zero; it claims an equality between two expressions, one of which is a sum that later turns out to be zero.

private theorem edgeStrain_mul_edgeStrain (H : Mat4) (De Dep : Fin 4 → ℤ) :
    edgeStrain H De * edgeStrain H Dep =
      ∑ a : Fin 4, ∑ b : Fin 4, ∑ c : Fin 4, ∑ d : Fin 4,
        H a b * H c d * (De a : ℝ) * (De b : ℝ) * (Dep c : ℝ) * (Dep d : ℝ) := by
  unfold edgeStrain
  simp_rw [Finset.sum_mul, 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:** 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 declaration does not assert that edge strain or the Bloch symbol has any physical meaning. The declaration does not claim that the product of edge strains is zero; only that it equals a sum which later vanishes. The declaration does not establish any property of gravity in the conventional physical sense.

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: