Gravity Analysis Regge4 Dtensor Algebraic Closer Continuum Face Normalized Plus

A vanishing check in four dimensions

In the Recognition Science framework, a ledger (a discrete record of events) carries a quantity called the transported distinct-hinge moment, a number associated with how a geometric object, a four-dimensional polytope, bends at its hinges. The declaration continuumFace_normalizedPlus_e0Dir_vanishes is a proved statement about this quantity. It says that when you take a particular polarization state, called the plus state, and look along a specific direction, called e0, the value of this moment, after dividing by the squared length of the direction, is exactly zero.

This is a narrow, concrete result. It is one ray evaluation among many. The framework's library also proves that along the symbol direction the same normalized plus state gives negative one sixteenth, and that the cross state along e0 also gives negative one sixteenth. The vanishing along e0 for the plus state is the one clean zero in this small table. The proof is a direct computation: it unfolds the definition of the moment form, rewrites with a previously established lemma about the normalized plus state, and simplifies the arithmetic. The statement is a theorem, meaning it is checked by the machine and rests on no framework-specific axioms.

The declaration does not claim that this vanishing is part of a general law. The library explicitly marks as open the search for a universal tensor contraction, a single formula that would reproduce the distinct-hinge moment for all polarization states and all nonzero directions. That closed form is the goal. This vanishing is a data point, not the formula. The library also leaves open a geometric explanation for why the continuum value differs from the Einstein-Hilbert value by a factor of four. The vanishing does not install that missing factor; it does not flip a separate status flag called gap action recovery, which remains false.

What the result changes is the shape of the evidence. Anyone working toward the closed form now has a checked corner of the space: the plus state along e0 must return zero in any candidate formula. A proposed universal contraction that does not vanish there is already wrong. The declaration is a small but real constraint, a fixed point that the unfinished theory must respect.

theorem continuumFace_normalizedPlus_e0Dir_vanishes :
    distinctHingeMomentForm ((Real.sqrt 2)⁻¹ • axisTTPlus) e0Dir /
        (∑ i : Fin 4, e0Dir i * e0Dir i) =
      (0 : ℝ) := by
  unfold distinctHingeMomentForm
  rw [m2TransportedAllOrbitMomentDistinctHinge_axisTTPlusNormalized_e0Dir,
    e0Dir_normSq]
  norm_num

theorem does_not_flip_gap_action_recovery :
    regge4DTensorAlgebraicCloserStatus.gapActionRecovery = false :=
  rfl

What this page does not claim

This declaration does not establish a general closed-form formula for the distinct-hinge moment. This declaration does not provide a geometric explanation for the factor of four residual. This declaration does not change the status of gap action recovery, which remains false.

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