Gravity Analysis Regge Bloch Local Incidence4 D M2 Mean Local All Orbit Moment E

The mean-local equivalence

In the Recognition Science framework's study of gravity in four dimensions, the declaration m2MeanLocalAllOrbitMoment_eq_distinctHinge is a proved theorem. It states that a certain averaged quantity, called the mean-local all-orbit moment, is exactly equal to another quantity called the transported distinct-hinge moment. Both are ways of computing a second-order moment, a measure of how a gravitational field responds to a probe, from a 4x4 matrix H and a direction vector. The theorem holds for any such matrix and direction, making it a fully general algebraic identity within its definitions.

The practical meaning is that, for this particular construction, the two approaches are interchangeable. The mean-local method averages a kernel over each orbit of a symmetry group, dividing by the orbit's size. The distinct-hinge method instead transports a single kernel to each position. The theorem proves these two procedures give identical results when summed over all orbit types. This is a useful simplification: it means the more complex averaging step can be replaced by the simpler distinct-hinge calculation without changing the outcome.

In Recognition Science, this equivalence is part of a larger investigation into how gravity emerges from a discrete ledger of recognition events. The framework models spacetime as a lattice of points, and gravitational effects arise from how these points recognize each other. The theorem is a step in checking whether a particular local-incidence construction, called Path B, can reproduce the expected Einstein-Hilbert action. The machine-checked library of formal theorems proves this equivalence, but the broader goal remains incomplete.

The theorem does not claim that the position-resolved version of Path B works. That version, which expands the star at each cube-translated base, is a separate and non-vacuous construction. The library explicitly marks it as open, with the proposition Regge4DPathBPositionResolvedClosesEH defined as false. A measured Python probe showed that extending the position-resolved method beyond the t11 orbit breaks the agreement with the distinct-hinge approach and fails to reach the expected Einstein-Hilbert value of -1/4. The theorem also does not claim that the mean-local method recovers the gap action recovery, which is also flagged as false in the status record.

What the equivalence does establish is a clean algebraic fact: for the mean-local, orbit-averaged construction, the two methods coincide for all inputs. This is a necessary but not sufficient step. It clears a path by showing the simpler method is valid where it applies, but it does not resolve the harder question of whether the full position-resolved construction closes the Einstein-Hilbert action. That question remains a target for future work.

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 :
    Regge4DPathBPositionResolvedClosesEH = False :=
  rfl

theorem does_not_flip_gap_action_recovery :
    reggeBlochLocalIncidence4DStatus.gapActionRecovery = false :=
  rfl

What this page does not claim

The theorem does not prove that the position-resolved Path B construction closes the Einstein-Hilbert action. The theorem does not claim that the mean-local method recovers the gap action recovery mechanism. The theorem does not establish any physical measurement or empirical prediction about gravity.

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: