Gravity Analysis Regge Bloch Local Incidence M2 Eval4 D Path B Position Resolved

The negative result

In the Recognition Science framework's machine-checked library of formal theorems, a declaration named pathB_positionResolved_does_not_close_eh records a specific negative result. It proves that a particular construction, called position-resolved Path B, does not close the Einstein-Hilbert gap. In plain language, this means that a proposed procedure for averaging a discrete, combinatorial gravity model does not, in this specific form, recover the continuous classical action of general relativity. The theorem states this failure as a formal boolean value: the proposition that position-resolved Path B closes the gap is proven to be False.

This negative result sits within a broader comparison. The framework's library also proves that a simpler, mean-local version of Path B agrees with a distinct-hinge construction on all four tested directions, yielding values like -1/4 and 0 for certain orbit moments. However, the position-resolved version does not restore isotropy: the average moment along one direction differs from another, and the normalized value does not match the Einstein-Hilbert coefficient. The declaration confirms that this failure persists, and that it does not flip a separate flag called gap_action_recovery, meaning the gap is not recovered by this path.

What the declaration does not claim is equally important. It does not assert that no possible Path B variant could close the gap; it only establishes that this specific position-resolved version fails. It does not claim that the mean-local version fails, since that version is proven to match distinct-hinge on the witnesses. It also does not claim that the failure is a defect in the framework's overall approach to gravity; it is a recorded, precise status within a larger research program, not a judgment on the program's viability.

/-- Position-resolved Path B does not close EH (status false / OPEN). -/
theorem pathB_positionResolved_does_not_close_eh :
    Regge4DPathBPositionResolvedClosesEH = False :=
  Regge4DPathBPositionResolvedClosesEH_status_open

theorem m2PathB_meanLocal_plus_cross_disagree_e0Dir :
    m2MeanLocalAllOrbitMoment axisTTPlus e0Dir ≠
      m2MeanLocalAllOrbitMoment axisTTCross e0Dir := by
  rw [m2PathB_meanLocal_axisTTPlus_e0Dir, m2PathB_meanLocal_axisTTCross_e0Dir]
  norm_num

theorem does_not_flip_gap_action_recovery :
    reggeBlochLocalIncidenceM2Eval4DStatus.gapActionRecovery = false :=
  rfl

What this page does not claim

No possible Path B variant could close the gap. The mean-local version of Path B fails. The framework's overall approach to gravity is invalid.

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