Gravity Analysis Regge Bloch Orbit Transport4 D Orbit Covering Perm

The covering permutation

In the Recognition Science framework's analysis of four-dimensional Regge calculus, a lattice of hinges carries discrete curvature data. The declaration orbitCoveringPerm is a definition inside the framework's machine-checked library of formal theorems. It answers a bookkeeping question: for each hinge slot in the lattice, which of the 24 possible coordinate permutations should transport the curvature data correctly? The answer is the first permutation, in a fixed ordering, that satisfies the covering equation for that slot. The library proves, as a theorem, that such a permutation exists for every slot, and that the chosen one agrees with the legacy hand-written table on the special (1,1) slots.

The definition itself is a search: given a hinge orbit type and a slot index, it scans the list of 24 permutations and returns the first one that makes the coordinate difference masks match the slot's expected values. The key theorem, orbitCoveringPerm_covers, states that for every slot, the permutation returned by this search does indeed cover the slot, meaning the equation holds. A second theorem, orbitCoveringPerm_spec, packages this into the explicit form: when the orbit type matches the slot's type, the coordinate permutation applied to the orbit representative yields exactly the slot's difference masks. This is a purely combinatorial statement about finite sets of 24 and 10 elements, checked by exhaustive case analysis.

What the declaration does not claim is broader physical content. It does not assert that this transport rule is the physically correct dynamics of gravity, nor that it derives from the framework's core cost function. The transport is a definitional choice, a model for how curvature data moves across the lattice. The existence theorem is real, but it is a statement about permutations and masks, not about spacetime geometry. The framework's own docstring warns that the older hand table is (1,1)-only and must not be used for other slots; the new covering rule is meant to replace it uniformly, but the physical justification for the rule itself remains a modeling assumption.

The practical consequence is a uniform, machine-verified transport rule for all hinge slots, removing a known gap in the older table. A reader can now rely on the covering permutation for any slot, with the assurance that the covering equation holds, without needing to check each case by hand. The rule is a tool inside the framework's gravity analysis, not a new law of physics.

/-- 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 transport rule is not derived from the framework's core cost function or forcing chain. The existence theorem says nothing about the physical correctness of the transport dynamics. The declaration does not establish any property of the covering permutation beyond the finite combinatorial covering equation.

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: