Gravity Analysis Regge Bloch Orbit Transport4 D Covers Orbit Slot

What the covering check does

In the framework's model of gravity as a discrete lattice, a hinge is a small rotational element living on an edge of the lattice. Hinges come in types, and each type has a representative arrangement. Transporting a hinge from its representative to a particular slot on the lattice requires re-labeling the coordinate axes. The declaration coversOrbitSlot (a boolean function, returning true or false) answers one question: does a given permutation of the 24 coordinate-axis orderings correctly move the representative hinge to the target slot, matching the required difference masks for that slot?

The definition is concrete. It takes the hinge orbit type, the slot coordinates (one of 24 spatial slots and one of 10 time slots), and a candidate permutation. It computes the difference between the permuted representative and the slot's masks, and returns true exactly when they match. The companion function orbitCoveringPerm picks the first such permutation in a fixed order, falling back to the zero permutation only if no cover exists. The framework's machine-checked library of formal theorems proves that on every realizable slot, this chosen permutation does cover the slot, and that on the special (1,1) slot type it agrees with the older hand-written transport table.

What the declaration does not claim is broader. It does not assert that the chosen permutation is unique, nor that it is physically preferred over any other covering permutation. It does not establish that the transport rule is the actual dynamics of gravity; the physical bridge from recognition to lattice transport remains open. It only fixes a consistent, machine-checked rule for how hinge orbits are moved to slots, replacing a hand table that was valid only for one slot type.

For the reader, the practical consequence is that the lattice transport is now uniform across all slot types, with a formal guarantee that every slot has at least one covering permutation. This removes a known gap in the earlier hand table and gives the framework a single, auditable transport rule to build on.

/-- Boolean cover test for a candidate coordinate permutation. -/
def coversOrbitSlot (ty : HingeOrbitType) (s : Fin 24) (t : Fin 10)
    (p : Fin 24) : Bool :=
  decide
    (permDiffPair (coordPermOf p) (orbitRep ty).1 (orbitRep ty).2 =
      (diffMaskA s t, diffMaskB s t))

/-- Every lattice slot is covered by its own orbit representative. -/
theorem orbitCoveringPerm_covers (s : Fin 24) (t : Fin 10) :
    coversOrbitSlot (hingeOrbitType s t) s t
        (orbitCoveringPerm (hingeOrbitType s t) s t) = true := by
  fin_cases s <;> fin_cases t <;> decide

/-- On `(1,1)` slots the covering perm agrees with the legacy table. -/
theorem orbitCoveringPerm_t11_eq_slotTransportPerm (s : Fin 24) (t : Fin 10) :
    orbitCoveringPerm .t11 s t = slotTransportPerm s t := by
  fin_cases s <;> fin_cases t <;> decide

What this page does not claim

The declaration does not prove that the covering permutation is unique or physically preferred. It does not establish that the lattice transport rule is the actual dynamics of gravity. It does not claim that the older hand table is valid for non-(1,1) slots.

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