IndisputableMonolith.Gravity.Analysis.ReggeBlochOrbitTransport4D

   1import Mathlib
   2import IndisputableMonolith.Gravity.Analysis.ReggeHinge4DOrbitClassification
   3import IndisputableMonolith.Gravity.Analysis.ReggeBlochFold4D
   4
   5/-!
   6# Orbit covering permutations for 4D Regge Bloch transport
   7
   8For each hinge slot `(s,t)` of orbit type `ty`, the covering coordinate
   9permutation is the **first** `p : Fin 24` (in `permAxes` order) such that
  10
  11  `permDiffPair (coordPermOf p) (orbitRep ty) = (diffMaskA s t, diffMaskB s t)`.
  12
  13This is the transport used for **all** orbits.  The hand table
  14`transportPermOfDiff` / `slotTransportPerm` is `(1,1)`-only and must not be
  15used for non-`(1,1)` slots (MEASURED: factorized vs transported fold lesson).
  16
  17## Tier tags
  18
  19* THEOREM: covering existence on every slot; agreement with
  20  `slotTransportPerm` on `(1,1)`.
  21* No `sorry` / `admit` / new axioms / `native_decide` / `: True` shells.
  22-/
  23
  24namespace IndisputableMonolith
  25namespace Gravity
  26namespace Analysis
  27namespace ReggeBlochOrbitTransport4D
  28
  29open ReggeHinge4DOrbitClassification
  30open ReggeBlochFold4D
  31
  32noncomputable section
  33
  34/-- Boolean cover test for a candidate coordinate permutation. -/
  35def coversOrbitSlot (ty : HingeOrbitType) (s : Fin 24) (t : Fin 10)
  36    (p : Fin 24) : Bool :=
  37  decide
  38    (permDiffPair (coordPermOf p) (orbitRep ty).1 (orbitRep ty).2 =
  39      (diffMaskA s t, diffMaskB s t))
  40
  41/-- First covering `S₄` index for slot `(s,t)` relative to `orbitRep ty`.
  42Falls back to `0` only if no cover exists (never on realizable slots). -/
  43def orbitCoveringPerm (ty : HingeOrbitType) (s : Fin 24) (t : Fin 10) :
  44    Fin 24 :=
  45  match List.find? (coversOrbitSlot ty s t) (List.finRange 24) with
  46  | some p => p
  47  | none => 0
  48
  49set_option maxRecDepth 8000 in
  50set_option maxHeartbeats 400000 in
  51/-- Every lattice slot is covered by its own orbit representative. -/
  52theorem orbitCoveringPerm_covers (s : Fin 24) (t : Fin 10) :
  53    coversOrbitSlot (hingeOrbitType s t) s t
  54        (orbitCoveringPerm (hingeOrbitType s t) s t) = true := by
  55  fin_cases s <;> fin_cases t <;> decide
  56
  57/-- Packaging: when `ty` is the slot's orbit type, the covering equation holds. -/
  58theorem orbitCoveringPerm_spec (ty : HingeOrbitType) (s : Fin 24) (t : Fin 10)
  59    (h : hingeOrbitType s t = ty) :
  60    permDiffPair (coordPermOf (orbitCoveringPerm ty s t))
  61        (orbitRep ty).1 (orbitRep ty).2 =
  62      (diffMaskA s t, diffMaskB s t) := by
  63  have hc := orbitCoveringPerm_covers s t
  64  subst h
  65  simpa [coversOrbitSlot, decide_eq_true_iff] using hc
  66
  67set_option maxRecDepth 8000 in
  68set_option maxHeartbeats 400000 in
  69/-- On `(1,1)` slots the covering perm agrees with the legacy table. -/
  70theorem orbitCoveringPerm_t11_eq_slotTransportPerm (s : Fin 24) (t : Fin 10) :
  71    orbitCoveringPerm .t11 s t = slotTransportPerm s t := by
  72  fin_cases s <;> fin_cases t <;> decide
  73
  74end
  75
  76end ReggeBlochOrbitTransport4D
  77end Analysis
  78end Gravity
  79end IndisputableMonolith
  80