Encyclopedia Gravity Gravity Analysis Regge Bloch Local Incidence4 D Bloch Fold Orbit Mean Local Eq S

ARTICLE 4 claims 4 theorems

Gravity Analysis Regge Bloch Local Incidence4 D Bloch Fold Orbit Mean Local Eq S

A machine-checked identity shows that averaging a gravity kernel over a symmetry orbit is the same as a scaled version of the original, a fact that anchors one path in a larger research program.

Verify this page

The scaling identity

In the Recognition Science framework, gravity is studied through discrete kernels: arrays of numbers attached to the edges and vertices of a four-dimensional lattice. The declaration blochFoldOrbitMeanLocal_eq_scaled is a theorem in the framework's machine-checked library of formal theorems. It states that for any orbit type, any 4 by 4 matrix, and any vector, the mean-local fold equals the inverse orbit star size times the ordinary fold. In plain terms, averaging a kernel over the 24 symmetries of a cube and the 10 positions of a hinge gives exactly the same result as taking the original kernel and dividing by a fixed integer, the size of the orbit's star.

The identity is a scaling law, not a new dynamical equation. It says that the operation of averaging over a symmetry orbit commutes with the operation of folding the kernel, up to a constant factor. The theorem blochFoldOrbitMeanLocal_eq_scaled is proved by unfolding the definitions and applying a sum congruence, a routine but fully verified step. The same scaling pattern appears in related declarations: the slot kernel, the slot term, and the second moment coefficient all obey the same inverse-star-size factor. This uniformity is what makes the mean-local construction a faithful rewriting of the distinct-hinge construction, not a different physical model.

The theorem does not claim that the mean-local path closes the Einstein-Hilbert action, nor that it recovers the missing factor that the path was designed to find. A separate status record in the same file sets pathBClosesEH to false and gapActionRecovery to false. The position-resolved extension, which would go beyond the mean-local averaging, is defined as the proposition False, meaning it is not established. The scaling identity is a necessary ingredient, but it is not a sufficient one: it guarantees algebraic consistency of the averaging step, not the physical closure of the program.

What the theorem changes is the status of one layer of the construction. Before the identity, the mean-local fold could have been an arbitrary new object requiring its own analysis. After it, the mean-local fold is known to be a scaled copy of the distinct-hinge fold, so any property that holds for the latter and is invariant under scaling transfers automatically. This is what lets the framework assert that the mean-local second moment equals the distinct-hinge second moment for all matrices and directions, a separate theorem in the same file. The scaling identity is the hinge on which that equivalence turns.

THEOREM blochFoldOrbitMeanLocal_eq_scaled · IndisputableMonolith/Gravity/Analysis/ReggeBlochLocalIncidence4D.lean
blochFoldOrbitMeanLocal_eq_scaled · IndisputableMonolith/Gravity/Analysis/ReggeBlochLocalIncidence4D.lean:127 
theorem blochFoldOrbitMeanLocal_eq_scaled (ty : HingeOrbitType) (H : Mat4)
    (m : Fin 4 → ℝ) :
    blochFoldOrbitMeanLocal ty H m =
      (orbitStarSize ty)⁻¹ * blochFoldOrbit ty H m := by
  unfold blochFoldOrbitMeanLocal blochFoldOrbit
  simp_rw [meanLocalSlotTerm_eq_scaled, ← Finset.mul_sum]
THEOREM slotOrbitMeanLocalKer_eq_scaled · meanLocalSlotTerm_eq_scaled · m2MeanLocalOrbitSlotCoeff_eq_scaled · IndisputableMonolith/Gravity/Analysis/ReggeBlochLocalIncidence4D.lean
slotOrbitMeanLocalKer_eq_scaled · IndisputableMonolith/Gravity/Analysis/ReggeBlochLocalIncidence4D.lean:73 
theorem slotOrbitMeanLocalKer_eq_scaled (ty : HingeOrbitType)
    (s : Fin 24) (t : Fin 10) (d : Fin 15) :
    slotOrbitMeanLocalKer ty s t d =
      (orbitStarSize ty)⁻¹ * slotOrbitDeficitKer ty s t d := by
  unfold slotOrbitMeanLocalKer transportedOrbitMeanLocal
    slotOrbitDeficitKer transportedOrbitDeficit pushforwardClass
    orbitMeanLocalKernel
  have h : ∀ d0 : Fin 15,
      (if permClass (orbitCoveringPerm ty s t) d0 = d then
          (orbitStarSize ty)⁻¹ * orbitSeedKernel ty d0 else 0) =
        (orbitStarSize ty)⁻¹ *
          (if permClass (orbitCoveringPerm ty s t) d0 = d then
            orbitSeedKernel ty d0 else 0) := by
    intro d0; split_ifs <;> ring
  simp_rw [h, ← Finset.mul_sum]
meanLocalSlotTerm_eq_scaled · IndisputableMonolith/Gravity/Analysis/ReggeBlochLocalIncidence4D.lean:96 
theorem meanLocalSlotTerm_eq_scaled (ty : HingeOrbitType) (H : Mat4)
    (m : Fin 4 → ℝ) (s : Fin 24) (t : Fin 10) :
    meanLocalSlotTerm ty H m s t =
      (orbitStarSize ty)⁻¹ * transportedOrbitSlotTerm ty H m s t := by
  unfold meanLocalSlotTerm transportedOrbitSlotTerm
  by_cases h : isOrbit ty s t
  · simp only [h, ite_true]
    have hker :
        phasedClassDot (slotOrbitMeanLocalKer ty s t) H m (hingeBase s t) =
          (orbitStarSize ty)⁻¹ *
            phasedClassDot (slotOrbitDeficitKer ty s t) H m
              (hingeBase s t) := by
      unfold phasedClassDot
      have hpt : ∀ d : Fin 15,
          slotOrbitMeanLocalKer ty s t d *
              planeWaveClassPert H m (hingeBase s t) d =
            (orbitStarSize ty)⁻¹ *
              (slotOrbitDeficitKer ty s t d *
                planeWaveClassPert H m (hingeBase s t) d) := by
        intro d
        rw [slotOrbitMeanLocalKer_eq_scaled]
        ring
      simp_rw [hpt, ← Finset.mul_sum]
    rw [hker]
    ring
  · simp [h]
m2MeanLocalOrbitSlotCoeff_eq_scaled · IndisputableMonolith/Gravity/Analysis/ReggeBlochLocalIncidence4D.lean:156 
theorem m2MeanLocalOrbitSlotCoeff_eq_scaled (ty : HingeOrbitType) (H : Mat4)
    (dir : Fin 4 → ℝ) (s : Fin 24) (t : Fin 10) :
    m2MeanLocalOrbitSlotCoeff ty H dir s t =
      (orbitStarSize ty)⁻¹ * m2TransportedOrbitSlotCoeff ty H dir s t := by
  change m2MeanLocalOrbitSlotCoeff ty H dir s t =
    (orbitStarSize ty)⁻¹ * m2TransportedOrbitSlotCoeffTrunc ty H dir s t
  unfold m2MeanLocalOrbitSlotCoeff m2TransportedOrbitSlotCoeffTrunc
  by_cases h : isOrbit ty s t
  · simp only [h, ↓reduceIte]
    have hsum :
        (∑ d : Fin 15,
            slotOrbitMeanLocalKer ty s t d * classCoeff H d *
              (phaseScaleDir dir (hingeBase s t) d) ^ 2) =
          (orbitStarSize ty)⁻¹ *
            ∑ d : Fin 15,
              slotOrbitDeficitKer ty s t d * classCoeff H d *
                (phaseScaleDir dir (hingeBase s t) d) ^ 2 := by
      have hpt : ∀ d : Fin 15,
          slotOrbitMeanLocalKer ty s t d * classCoeff H d *
              (phaseScaleDir dir (hingeBase s t) d) ^ 2 =
            (orbitStarSize ty)⁻¹ *
              (slotOrbitDeficitKer ty s t d * classCoeff H d *
                (phaseScaleDir dir (hingeBase s t) d) ^ 2) := by
        intro d
        rw [slotOrbitMeanLocalKer_eq_scaled]
        ring
      simp_rw [hpt, ← Finset.mul_sum]
    rw [hsum]
    ring
  · simp only [h, ↓reduceIte, mul_zero]
THEOREM m2MeanLocalAllOrbitMoment_eq_distinctHinge · IndisputableMonolith/Gravity/Analysis/ReggeBlochLocalIncidence4D.lean
m2MeanLocalAllOrbitMoment_eq_distinctHinge · IndisputableMonolith/Gravity/Analysis/ReggeBlochLocalIncidence4D.lean:201 
theorem m2MeanLocalAllOrbitMoment_eq_distinctHinge (H : Mat4)
    (dir : Fin 4 → ℝ) :
    m2MeanLocalAllOrbitMoment H dir =
      m2TransportedAllOrbitMomentDistinctHinge H dir := by
  unfold m2MeanLocalAllOrbitMoment m2TransportedAllOrbitMomentDistinctHinge
  refine Finset.sum_congr rfl fun ty _ =>
    m2MeanLocalOrbitMoment_eq_scaled ty H dir
THEOREM Regge4DPathBPositionResolvedClosesEH_status_open · IndisputableMonolith/Gravity/Analysis/ReggeBlochLocalIncidence4D.lean
Regge4DPathBPositionResolvedClosesEH_status_open · IndisputableMonolith/Gravity/Analysis/ReggeBlochLocalIncidence4D.lean:278 
theorem Regge4DPathBPositionResolvedClosesEH_status_open :
    Regge4DPathBPositionResolvedClosesEH = False :=
  rfl

What this page does not claim

The theorem does not claim that the mean-local path closes the Einstein-Hilbert action. The theorem does not claim that the position-resolved extension is defined. The theorem does not claim that the scaling identity holds for any kernel outside the mean-local construction.

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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND