Gravity Analysis Regge Bloch Local Incidence4 D Bloch Fold All Mean Local Eq Dis

The mean-local equivalence

In the Recognition Science framework's machine-checked library of formal theorems, a declaration named blochFoldAllMeanLocal_eq_distinctHinge proves an equality between two ways of computing a quantity called the Bloch fold. The first way, blochFoldAllMeanLocal, averages a kernel over each orbit before folding. The second way, blochFoldAllDistinctHinge, computes the fold directly from distinct hinge positions. The theorem states that for any 4x4 real matrix H and any real vector m, these two computations produce the same real number.

The proof is a direct consequence of a scaling property: each orbit's mean-local term is the orbit's original term divided by the orbit's star size. Summing over all orbit types cancels the scaling factors, leaving the distinct-hinge result. The theorem is tagged THEOREM in the framework's taxonomy, meaning it is proved in the Lean 4 proof assistant with no axioms beyond the standard three, and it is a formal statement about the framework's own definitions.

The theorem does not claim that the mean-local approach is physically correct. A separate status structure in the same file records that the position-resolved variant, which expands the star at cube-translate bases, does not close the Einstein-Hilbert action at -1/4 and does not recover the gap action. The theorem also does not claim that the mean-local approach is the only way to compute the fold, nor that it is the physically relevant one. It is a formal equivalence between two specific definitions, not a statement about the physical world.

theorem blochFoldAllMeanLocal_eq_distinctHinge (H : Mat4) (m : Fin 4 → ℝ) :
    blochFoldAllMeanLocal H m = blochFoldAllDistinctHinge H m := by
  unfold blochFoldAllMeanLocal blochFoldAllDistinctHinge
  refine Finset.sum_congr rfl fun ty _ =>
    blochFoldOrbitMeanLocal_eq_scaled ty H m

theorem blochFoldAllMeanLocal_eq_distinctHinge (H : Mat4) (m : Fin 4 → ℝ) :
    blochFoldAllMeanLocal H m = blochFoldAllDistinctHinge H m := by
  unfold blochFoldAllMeanLocal blochFoldAllDistinctHinge
  refine Finset.sum_congr rfl fun ty _ =>
    blochFoldOrbitMeanLocal_eq_scaled ty H m

theorem reggeBlochLocalIncidence4DStatus_flags :
    reggeBlochLocalIncidence4DStatus.meanLocalEqualsDistinctHinge = true ∧
      reggeBlochLocalIncidence4DStatus.positionResolvedT11Defined = true ∧
        reggeBlochLocalIncidence4DStatus.pathBClosesEH = false ∧
          reggeBlochLocalIncidence4DStatus.gapActionRecovery = false := by
  decide

What this page does not claim

The theorem does not prove the physical correctness of the mean-local approach. The theorem does not establish that the position-resolved variant is equivalent to distinct-hinge. The theorem does not claim that the mean-local approach is the only valid way to compute the Bloch fold.

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