Gravity Analysis Regge Bloch Local Incidence M2 Eval4 D

A local check on a gravity candidate

Regge calculus is a way of doing general relativity without smooth geometry: spacetime is chopped into flat pieces, usually four-dimensional simplices, joined along shared faces. The name comes from Tullio Regge, who introduced the idea in 1961. Instead of Einstein's field equations as differential equations, one writes them as algebraic conditions on the lengths of the edges of the pieces. The framework called Recognition Science, which builds physical structure from a discrete ledger of recognition events, uses such discrete models to test whether its own proposed quantum gravity candidate behaves correctly.

The module named ReggeBlochLocalIncidenceM2Eval4D examines a specific candidate called Path B. The name mixes Regge calculus with a Bloch wave ansatz, a standard tool from solid-state physics where quantum states in a periodic potential are written as plane waves times a periodic function. The module asks two questions. First, does Path B reproduce the same local behavior as a simpler known construction called the distinct-hinge witness, when averaged over all orbit directions? Second, does Path B restore the symmetry that a physical vacuum should have, namely isotropy, the property that no direction is special?

The answers are clean. On the four witness directions tested, the mean-local Path B value exactly equals the distinct-hinge value in every case: minus one quarter for two directions, zero for a third, minus one eighth for the fourth. This agreement is proved in the machine-checked library of formal theorems. But on the isotropy question, Path B fails. When the position is resolved instead of averaged, the value along one direction is zero while along another it is minus one eighth, so the two disagree. The module states this plainly: position-resolved Path B does not close the Einstein-Hilbert gap, does not inhabit the continuum limit, and does not flip the recovery flag for the gap action. The status record sets four flags true and two false.

What this establishes in plain language is a negative result with a positive byproduct. The negative result: the Path B candidate, when examined at local incidence in four dimensions, is not isotropic and therefore cannot serve as the discrete seed of a physical vacuum. The positive byproduct: the mean-local averaging procedure exactly matches the distinct-hinge construction on all tested witnesses, which suggests the averaging is not introducing spurious errors, and the failure is intrinsic to Path B, not an artifact of the test. The module does not claim that no discrete gravity model works; it claims that this one does not, and it proves the specific numbers.

theorem pathB_vs_distinctHinge_witness_table :
    m2MeanLocalAllOrbitMoment axisTTPlus symbolDir =
        m2TransportedAllOrbitMomentDistinctHinge axisTTPlus symbolDir ∧
      m2MeanLocalAllOrbitMoment axisTTCross symbolDir =
        m2TransportedAllOrbitMomentDistinctHinge axisTTCross symbolDir ∧
      m2MeanLocalAllOrbitMoment axisTTPlus e0Dir =
        m2TransportedAllOrbitMomentDistinctHinge axisTTPlus e0Dir ∧
      m2MeanLocalAllOrbitMoment axisTTCross e0Dir =
        m2TransportedAllOrbitMomentDistinctHinge axisTTCross e0Dir ∧
      m2MeanLocalAllOrbitMoment axisTTPlus symbolDir = (-1 / 4 : ℝ) ∧
      m2MeanLocalAllOrbitMoment axisTTCross symbolDir = (-1 / 4 : ℝ) ∧
      m2MeanLocalAllOrbitMoment axisTTPlus e0Dir = (0 : ℝ) ∧
      m2MeanLocalAllOrbitMoment axisTTCross e0Dir = (-1 / 8 : ℝ) := by
  refine ⟨?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_⟩
  · exact m2MeanLocalAllOrbitMoment_eq_distinctHinge _ _
  · exact m2MeanLocalAllOrbitMoment_eq_distinctHinge _ _
  · exact m2MeanLocalAllOrbitMoment_eq_distinctHinge _ _
  · exact m2MeanLocalAllOrbitMoment_eq_distinctHinge _ _
  · exact m2PathB_meanLocal_axisTTPlus_symbolDir
  · exact m2PathB_meanLocal_axisTTCross_symbolDir
  · exact m2PathB_meanLocal_axisTTPlus_e0Dir
  · exact m2PathB_meanLocal_axisTTCross_e0Dir

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

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

theorem pathB_does_not_inhabit_eh :
    regge4DTorusContinuumLimitStatus.ehTendstoInhabited = false :=
  rfl

theorem does_not_flip_gap_action_recovery :
    reggeBlochLocalIncidenceM2Eval4DStatus.gapActionRecovery = false :=
  rfl

What this page does not claim

No claim that Path B fails for all possible directions, only for the four tested witnesses. No claim that the distinct-hinge construction is physically correct, only that it agrees with Path B on these witnesses. No claim that discrete gravity in general is ruled out by this module.

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: