Gravity Analysis Regge Bloch Transported All Orbit4 D M2 Transported Orbit Momen

The full transported moment

In the Recognition Science framework's machine-checked library of formal theorems, the declaration m2TransportedOrbitMomentFull_smul is a definition, not a theorem about physics. It assembles a numerical quantity, the full transported moment, by summing contributions from all six orbit types in a four-dimensional discrete geometry. The definition takes a 4 by 4 real matrix H, which models the metric or background field, and a direction vector, then produces a single real number. This number is meant to represent a moment, a weighted measure of how the geometry responds along that direction.

The key property that the declaration establishes is a scaling law. If you multiply the matrix H by a scalar c, the full transported moment scales by c squared. In symbols, for any real c, matrix H, and direction m, the value at c times H equals c squared times the value at H. This is a homogeneity property, a common and expected behavior for a quantity that is quadratic in the metric. The proof is a direct computation from the definition, relying on the same property holding for each individual orbit's contribution, which is also proved in the library.

The definition is built from more basic pieces. Each of the six orbit types has its own moment, and the full version sums them. There is also a variant that weights each orbit by the reciprocal of its star size, the number of cells in its local star, before summing. The full version does not apply this weighting. The declaration also does not claim that the full moment matches any particular physical observable, nor does it assert that the quantity tends to a limit as some parameter grows. Those are left as open targets in the library.

What this means in practice is that the framework has a precisely defined, machine-checked object with a clean scaling behavior. It is a building block, not a final physical prediction. The scaling law is a useful check on the definition's consistency, and it provides a foundation for future work that might connect this discrete moment to continuum physics, such as the Einstein-Hilbert action. That connection, however, is not made by this declaration.

def m2TransportedAllOrbitMoment (H : Mat4) (dir : Fin 4 → ℝ) : ℝ :=
  ∑ ty : HingeOrbitType, m2TransportedOrbitMoment ty H dir

theorem blochFoldAll_smul (c : ℝ) (H : Mat4) (m : Fin 4 → ℝ) :
    blochFoldAll (c • H) m = c ^ 2 * blochFoldAll H m := by
  unfold blochFoldAll
  simp_rw [blochFoldOrbit_smul, ← Finset.mul_sum]

What this page does not claim

This declaration does not claim that the full transported moment equals any measured physical quantity. It does not claim that the moment has a well-defined limit as the discrete grid is refined. It does not claim that the full moment matches the Einstein-Hilbert action or any other continuum expression.

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