Gravity Analysis Regge Bloch Transported All Orbit4 D

The all-orbit fold

This construction lives inside a machine-checked library of formal theorems. It builds a single object, the all-orbit fold, that sums the gravitational response over every symmetry class of a four-dimensional lattice. The lattice has 24 slots and 15 independent directions. Each slot carries two pieces of local data: an area covector, a small directed patch of space, and a deficit kernel, a measure of how much that patch fails to close into a flat region. The fold transports these data across the lattice using a covering permutation, then sums the results. The plain idea is a bookkeeping device: take the local geometry, move it through all its symmetries, and add up the contributions.

The construction has a precise classical analogue. In Regge calculus, gravity is approximated by a triangulated space where curvature lives on hinges, the shared edges of simplices. The deficit angle at a hinge measures the failure of the surrounding space to be flat. This construction works in that tradition. Its name, Regge Bloch, signals the blend: Regge's discrete gravity and Bloch's theorem for periodic structures. The fold is the discrete analogue of integrating a local curvature density over a fundamental cell.

The library proves several structural facts. The fold is homogeneous: scaling the metric by a constant c scales the fold by c squared. It vanishes when the metric is zero. For the simplest orbit type, the t11 class, the transported area and deficit kernels recover the original untransported definitions exactly. The second moment, a measure of the fold's spread, matches the known symbol for that slice. These are formal theorems, checked by the kernel.

Two evaluations are stated as open targets, not theorems. The all-orbit second moment along a particular symbolic direction is conjectured to equal -5/2. A distinct-hinge weighted version is conjectured to equal -1/4. The library also records two larger open problems: the limit of the all-orbit moment as the lattice grows, and the recovery of the Einstein-Hilbert action in the continuum limit. The latter still requires a residual cell-sum dictionary. The construction does not flip a separate recovery flag for a gap action.

The practical consequence is a single, well-defined object that unifies the six orbit types into one sum. Before this construction, each orbit was treated separately. Now the fold is a single function of the metric and a momentum direction. That is the step the open targets need: a clean object to take limits of.

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]

/-- Compatibility wrapper (audit / older callers): same as `slotOrbitAreaCov_t11`. -/
theorem slotOrbitAreaCov_t11_eq (s : Fin 24) (t : Fin 10) (h : isT11 s t) :
    slotOrbitAreaCov .t11 s t = slotAreaCov s t :=
  slotOrbitAreaCov_t11 s t h

theorem transportedOrbitDeficit_t11 (p : Fin 24) :
    transportedOrbitDeficit .t11 p = transportedDeficit p := by
  funext d
  simp [transportedOrbitDeficit, pushforwardClass, transportedDeficit,
    orbitSeedKernel_t11]

What this page does not claim

Not a proof that the all-orbit second moment equals -5/2; that is an open target. Not a derivation of the Einstein-Hilbert action from the fold; the continuum limit is open. Not a claim that the fold is the unique or canonical discrete gravity action.

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: