IndisputableMonolith.Gravity.Analysis.ReggeHinge4DOrbitClassification

   1import Mathlib
   2import IndisputableMonolith.Gravity.Analysis.ReggeHinge4DFlatKernel
   3import IndisputableMonolith.Gravity.Analysis.ReggeEdgeStencil4D
   4
   5/-!
   6# Regge 4D triangle-hinge orbit classification (Freudenthal / Kuhn cell)
   7
   8QG full-theory campaign, combinatorial prerequisite for assembling the
   9flat Hessian from per-orbit star kernels.  Imports the 24 Kuhn
  10simplices / `vertexMask` API of `ReggeHinge4DFlatKernel` and the
  1115-class mask utilities of `ReggeEdgeStencil4D`; never redefines them.
  12
  13## Tier tags (binding)
  14
  15* THEOREM: every named theorem below (kernel-checked; no `sorry`, no
  16  `admit`, no new axioms, no `native_decide`, no `: True` shells).
  17* Scope: **combinatorics only** of triangle hinges in one unit 4-cube
  18  Kuhn triangulation, up to lattice translation (difference masks) and
  19  triangulation-preserving symmetry.
  20* This does **not** evaluate per-orbit star kernels (other than the
  21  already-committed seed orbit in `ReggeHinge4DStarKernel`).
  22* This does **not** complete the flat Hessian of the 4D Regge action.
  23* This does **not** prove `S_RS_converges_EH_4d`.
  24* This does **not** flip `gap_action_recovery`.
  25
  26## What is proved (deliverable A, with honest refinement)
  27
  281. **Difference-mask type.** Every index-triple triangle in a Kuhn
  29   simplex is a monotone mask chain `m₀ ⊂ m₁ ⊂ m₂` with disjoint
  30   nonzero difference masks `(a,b) = (m₁⊕m₀, m₂⊕m₁)`; its type is the
  31   popcount pair `(|a|,|b|) ∈ {(1,1),(1,2),(2,1),(1,3),(3,1),(2,2)}`.
  322. **Cell enumeration.** Exactly `24 · C(5,3) = 240` oriented
  33   triangle slots; per-type counts
  34   `(72,48,48,24,24,24)` for types
  35   `(1,1),(1,2),(2,1),(1,3),(3,1),(2,2)`.
  363. **Lattice orbits under coordinate permutation.** Every realizable
  37   disjoint difference pair appears; the `S₄` action on bit positions
  38   preserves type and is transitive on realizable pairs of each type
  39   (six orbits).  The seed hinge `{0,e₀,e₀+e₁}` has type `(1,1)`.
  404. **Complement symmetry.** Bitwise complement `m ↦ m ⊕ 15` sends
  41   Kuhn vertex-sets to Kuhn vertex-sets and swaps type `(i,j)` with
  42   `(j,i)`.  Under the larger triangulation-preserving group
  43   `S₄ ⋊ {id, complement}`, types `(1,2)~(2,1)` and `(1,3)~(3,1)`
  44   merge, yielding **four** lattice orbits.
  455. **Within-cell absolute triangles.** Coordinate permutation does
  46   **not** act transitively on absolute mask-triples of a fixed type
  47   inside one cube (vertex-popcount profiles distinguish positions);
  48   lattice classification uses translation-normalized `(a,b)`, not
  49   absolute placement.
  506. **Local squared-length package** for one representative of each of
  51   the six `S₄`-orbits (flat Hamming weights of edges `a`, `b`, `a∨b`).
  527. **Gates:** seed nonvacuity; overlapping-mask decoy `(1,3)` is not
  53   a realizable difference pair.
  54
  55Expected axiom footprint: `[propext, Classical.choice, Quot.sound]`.
  56-/
  57
  58namespace IndisputableMonolith
  59namespace Gravity
  60namespace Analysis
  61namespace ReggeHinge4DOrbitClassification
  62
  63open ReggeHinge4DFlatKernel
  64open ReggeEdgeStencil4D
  65
  66/-! ## §1. Triangle slots and difference masks -/
  67
  68/-- The `C(5,3) = 10` increasing vertex-index triples in a 4-simplex. -/
  69def triangleIndexTriple : Fin 10 → Fin 5 × Fin 5 × Fin 5
  70  | 0 => (0, 1, 2)
  71  | 1 => (0, 1, 3)
  72  | 2 => (0, 1, 4)
  73  | 3 => (0, 2, 3)
  74  | 4 => (0, 2, 4)
  75  | 5 => (0, 3, 4)
  76  | 6 => (1, 2, 3)
  77  | 7 => (1, 2, 4)
  78  | 8 => (1, 3, 4)
  79  | 9 => (2, 3, 4)
  80  | ⟨n + 10, h⟩ => absurd h (by omega)
  81
  82/-- Hamming weight on the four low bits (masks in `{0,…,15}`). -/
  83def maskPop (m : ℕ) : ℕ :=
  84  (if Nat.testBit m 0 then 1 else 0) +
  85    (if Nat.testBit m 1 then 1 else 0) +
  86      (if Nat.testBit m 2 then 1 else 0) +
  87        (if Nat.testBit m 3 then 1 else 0)
  88
  89/-- Ordered vertex masks of triangle slot `t` in simplex `s`. -/
  90def triangleVertexMasks (s : Fin 24) (t : Fin 10) : ℕ × ℕ × ℕ :=
  91  let p := triangleIndexTriple t
  92  (vertexMask s p.1, vertexMask s p.2.1, vertexMask s p.2.2)
  93
  94/-- First difference mask `a = m₁ ⊕ m₀`. -/
  95def diffMaskA (s : Fin 24) (t : Fin 10) : ℕ :=
  96  let m := triangleVertexMasks s t
  97  Nat.xor m.2.1 m.1
  98
  99/-- Second difference mask `b = m₂ ⊕ m₁`. -/
 100def diffMaskB (s : Fin 24) (t : Fin 10) : ℕ :=
 101  let m := triangleVertexMasks s t
 102  Nat.xor m.2.2 m.2.1
 103
 104/-- Popcount-pair type of a triangle slot. -/
 105def hingeTypePop (s : Fin 24) (t : Fin 10) : ℕ × ℕ :=
 106  (maskPop (diffMaskA s t), maskPop (diffMaskB s t))
 107
 108/-- The six lattice orbit types under coordinate permutation. -/
 109inductive HingeOrbitType
 110  | t11
 111  | t12
 112  | t21
 113  | t13
 114  | t31
 115  | t22
 116  deriving DecidableEq, Repr, Fintype
 117
 118def HingeOrbitType.toPop : HingeOrbitType → ℕ × ℕ
 119  | .t11 => (1, 1)
 120  | .t12 => (1, 2)
 121  | .t21 => (2, 1)
 122  | .t13 => (1, 3)
 123  | .t31 => (3, 1)
 124  | .t22 => (2, 2)
 125
 126def popToOrbitType : ℕ × ℕ → Option HingeOrbitType
 127  | (1, 1) => some .t11
 128  | (1, 2) => some .t12
 129  | (2, 1) => some .t21
 130  | (1, 3) => some .t13
 131  | (3, 1) => some .t31
 132  | (2, 2) => some .t22
 133  | _ => none
 134
 135/-- THEOREM: every triangle slot has one of the six orbit types. -/
 136theorem hingeTypePop_is_orbitType (s : Fin 24) (t : Fin 10) :
 137    popToOrbitType (hingeTypePop s t) ≠ none := by
 138  fin_cases s <;> fin_cases t <;> decide
 139
 140/-- Typed orbit of a triangle slot. -/
 141def hingeOrbitType (s : Fin 24) (t : Fin 10) : HingeOrbitType :=
 142  (popToOrbitType (hingeTypePop s t)).getD .t11
 143
 144theorem hingeOrbitType_toPop (s : Fin 24) (t : Fin 10) :
 145    (hingeOrbitType s t).toPop = hingeTypePop s t := by
 146  fin_cases s <;> fin_cases t <;> decide
 147
 148/-- THEOREM: difference masks of every triangle slot are nonzero,
 149pairwise bitwise disjoint, and OR-bounded by four bits. -/
 150theorem triangle_diff_masks_ok (s : Fin 24) (t : Fin 10) :
 151    0 < diffMaskA s t ∧ 0 < diffMaskB s t ∧
 152      Nat.land (diffMaskA s t) (diffMaskB s t) = 0 ∧
 153        diffMaskA s t ≤ 15 ∧ diffMaskB s t ≤ 15 := by
 154  fin_cases s <;> fin_cases t <;> decide
 155
 156/-! ## §2. Per-type triangle counts in the 24-simplex cell -/
 157
 158/-- Indicator that slot `(s,t)` has popcount type `p`. -/
 159def triangleTypeNat (s : Fin 24) (t : Fin 10) (p : ℕ × ℕ) : ℕ :=
 160  if hingeTypePop s t = p then 1 else 0
 161
 162/-- Cell-wide count of oriented triangle slots of a given popcount type. -/
 163def cellTriangleCount (p : ℕ × ℕ) : ℕ :=
 164  ∑ s : Fin 24, ∑ t : Fin 10, triangleTypeNat s t p
 165
 166theorem cellTriangleCount_t11 : cellTriangleCount (1, 1) = 72 := by
 167  decide
 168
 169theorem cellTriangleCount_t12 : cellTriangleCount (1, 2) = 48 := by
 170  decide
 171
 172theorem cellTriangleCount_t21 : cellTriangleCount (2, 1) = 48 := by
 173  decide
 174
 175theorem cellTriangleCount_t13 : cellTriangleCount (1, 3) = 24 := by
 176  decide
 177
 178theorem cellTriangleCount_t31 : cellTriangleCount (3, 1) = 24 := by
 179  decide
 180
 181theorem cellTriangleCount_t22 : cellTriangleCount (2, 2) = 24 := by
 182  decide
 183
 184/-- THEOREM: per-type oriented counts in one Kuhn cell. -/
 185theorem cellTriangleCount_values :
 186    cellTriangleCount (1, 1) = 72 ∧
 187      cellTriangleCount (1, 2) = 48 ∧
 188        cellTriangleCount (2, 1) = 48 ∧
 189          cellTriangleCount (1, 3) = 24 ∧
 190            cellTriangleCount (3, 1) = 24 ∧
 191              cellTriangleCount (2, 2) = 24 :=
 192  ⟨cellTriangleCount_t11, cellTriangleCount_t12, cellTriangleCount_t21,
 193    cellTriangleCount_t13, cellTriangleCount_t31, cellTriangleCount_t22⟩
 194
 195/-- THEOREM: the six types partition all `240` oriented slots. -/
 196theorem cellTriangleCount_sum :
 197    cellTriangleCount (1, 1) + cellTriangleCount (1, 2) +
 198        cellTriangleCount (2, 1) + cellTriangleCount (1, 3) +
 199          cellTriangleCount (3, 1) + cellTriangleCount (2, 2) =
 200      240 := by
 201  simp [cellTriangleCount_t11, cellTriangleCount_t12, cellTriangleCount_t21,
 202    cellTriangleCount_t13, cellTriangleCount_t31, cellTriangleCount_t22]
 203
 204theorem oriented_slot_total :
 205    (Fintype.card (Fin 24) * Fintype.card (Fin 10)) = 240 := by
 206  decide
 207
 208/-! ## §3. Realizable difference pairs and decoy -/
 209
 210/-- Whether `(a,b)` arises as the difference pair of some cell triangle. -/
 211def isRealizableDiffPair (a b : ℕ) : Bool :=
 212  decide (∃ s : Fin 24, ∃ t : Fin 10,
 213    diffMaskA s t = a ∧ diffMaskB s t = b)
 214
 215/-- Bitwise-disjoint nonzero mask pair with masks in `{1,…,15}`. -/
 216def isDisjointDiffPair (a b : ℕ) : Bool :=
 217  decide (0 < a ∧ 0 < b ∧ a ≤ 15 ∧ b ≤ 15 ∧ Nat.land a b = 0)
 218
 219/-- THEOREM: every disjoint nonzero 4-bit difference pair is realized. -/
 220theorem disjoint_implies_realizable (a b : Fin 15) :
 221    Nat.land (maskOf a) (maskOf b) = 0 →
 222      isRealizableDiffPair (maskOf a) (maskOf b) = true := by
 223  fin_cases a <;> fin_cases b <;> decide
 224
 225/-- THEOREM (decoy): overlapping masks `(1,3)` are not a monotone
 226difference pair. -/
 227theorem decoy_overlapping_not_realizable :
 228    isRealizableDiffPair 1 3 = false := by
 229  decide
 230
 231theorem decoy_overlapping_is_not_disjoint :
 232    isDisjointDiffPair 1 3 = false := by
 233  decide
 234
 235/-- Seed hinge masks `{0,1,3}` as the slot `(s,t) = (0,0)`. -/
 236theorem seed_slot_masks :
 237    triangleVertexMasks 0 0 = (0, 1, 3) := by
 238  decide
 239
 240/-- THEOREM (nonvacuity): the seed hinge has type `(1,1)`. -/
 241theorem seed_hinge_type_t11 :
 242    hingeTypePop 0 0 = (1, 1) ∧ hingeOrbitType 0 0 = .t11 := by
 243  decide
 244
 245/-! ## §4. Coordinate-permutation action on masks -/
 246
 247/-- Apply a coordinate permutation (as a `Fin 4 → Fin 4` map) to a mask. -/
 248def permMask (σ : Fin 4 → Fin 4) (m : ℕ) : ℕ :=
 249  (if Nat.testBit m 0 then 2 ^ (σ 0).val else 0) +
 250    (if Nat.testBit m 1 then 2 ^ (σ 1).val else 0) +
 251      (if Nat.testBit m 2 then 2 ^ (σ 2).val else 0) +
 252        (if Nat.testBit m 3 then 2 ^ (σ 3).val else 0)
 253
 254/-- Lexicographic list of all 24 permutations of `Fin 4`, matching
 255`permAxes` order. -/
 256def coordPermOf (p : Fin 24) : Fin 4 → Fin 4 :=
 257  fun i =>
 258    match i, permAxes p with
 259    | 0, (a, _, _, _) => a
 260    | 1, (_, b, _, _) => b
 261    | 2, (_, _, c, _) => c
 262    | 3, (_, _, _, d) => d
 263
 264def permDiffPair (σ : Fin 4 → Fin 4) (a b : ℕ) : ℕ × ℕ :=
 265  (permMask σ a, permMask σ b)
 266
 267/-- THEOREM: every Kuhn coordinate permutation preserves `maskPop` on
 2684-bit masks. -/
 269theorem coordPerm_preserves_pop (p : Fin 24) (m : Fin 16) :
 270    maskPop (permMask (coordPermOf p) m.val) = maskPop m.val := by
 271  fin_cases p <;> fin_cases m <;> decide
 272
 273/-- THEOREM: coordinate permutation preserves popcount type of a
 274difference pair. -/
 275theorem coordPerm_preserves_type (p : Fin 24) (a b : Fin 16) :
 276    (maskPop (permMask (coordPermOf p) a.val),
 277      maskPop (permMask (coordPermOf p) b.val)) =
 278      (maskPop a.val, maskPop b.val) := by
 279  simp [coordPerm_preserves_pop p a, coordPerm_preserves_pop p b]
 280
 281/-- Canonical `S₄`-orbit representatives (one per popcount type). -/
 282def orbitRep : HingeOrbitType → ℕ × ℕ
 283  | .t11 => (1, 2)
 284  | .t12 => (1, 6)
 285  | .t21 => (3, 4)
 286  | .t13 => (1, 14)
 287  | .t31 => (7, 8)
 288  | .t22 => (3, 12)
 289
 290theorem orbitRep_realizable (ty : HingeOrbitType) :
 291    isRealizableDiffPair (orbitRep ty).1 (orbitRep ty).2 = true := by
 292  cases ty <;> decide
 293
 294theorem orbitRep_type (ty : HingeOrbitType) :
 295    (maskPop (orbitRep ty).1, maskPop (orbitRep ty).2) = ty.toPop := by
 296  cases ty <;> decide
 297
 298/-- Whether `(a,b)` lies in the `S₄`-orbit of the canonical rep of `ty`. -/
 299def inOrbitOfRep (ty : HingeOrbitType) (a b : ℕ) : Bool :=
 300  decide (∃ p : Fin 24,
 301    permDiffPair (coordPermOf p) (orbitRep ty).1 (orbitRep ty).2 = (a, b))
 302
 303/-- THEOREM: every realizable difference pair of a given type lies in
 304the single `S₄`-orbit of that type's representative (transitivity on
 305translation-normalized pairs). -/
 306theorem realizable_in_type_orbit (a b : Fin 15)
 307    (hdis : Nat.land (maskOf a) (maskOf b) = 0) :
 308    inOrbitOfRep
 309        (match popToOrbitType (maskPop (maskOf a), maskPop (maskOf b)) with
 310          | some ty => ty
 311          | none => .t11)
 312        (maskOf a) (maskOf b) =
 313      true := by
 314  fin_cases a <;> fin_cases b <;> first | decide | contradiction
 315
 316/-- Cleaner packaging: realizable pairs match their type orbit. -/
 317theorem realizable_matches_rep_orbit (s : Fin 24) (t : Fin 10) :
 318    inOrbitOfRep (hingeOrbitType s t) (diffMaskA s t) (diffMaskB s t) =
 319      true := by
 320  fin_cases s <;> fin_cases t <;> decide
 321
 322/-! ## §5. Complement symmetry merges `(i,j)` with `(j,i)` -/
 323
 324/-- Bitwise complement inside the unit 4-cube. -/
 325def complementMask (m : ℕ) : ℕ := Nat.xor m 15
 326
 327/-- THEOREM: complement sends every Kuhn simplex vertex-set to another
 328Kuhn simplex vertex-set in the same cell. -/
 329theorem complement_preserves_kuhn (s : Fin 24) :
 330    ∃ s' : Fin 24, ∀ i : Fin 5,
 331      vertexMask s' i = complementMask (vertexMask s (4 - i)) := by
 332  fin_cases s <;> decide
 333
 334/-- Complement of a difference pair, after reversing the monotone chain:
 335`(a,b) ↦ (b,a)` on the nose when masks are complementary-nested. -/
 336theorem complement_swaps_diff_pair (s : Fin 24) (t : Fin 10) :
 337    ∃ s' : Fin 24, ∃ t' : Fin 10,
 338      diffMaskA s' t' = diffMaskB s t ∧
 339        diffMaskB s' t' = diffMaskA s t := by
 340  fin_cases s <;> fin_cases t <;> decide
 341
 342/-- THEOREM: complement swaps popcount type `(i,j)` with `(j,i)`. -/
 343theorem complement_swaps_type (s : Fin 24) (t : Fin 10) :
 344    ∃ s' : Fin 24, ∃ t' : Fin 10,
 345      hingeTypePop s' t' =
 346        ((hingeTypePop s t).2, (hingeTypePop s t).1) := by
 347  fin_cases s <;> fin_cases t <;> decide
 348
 349/-- The four orbits under `S₄` plus complement. -/
 350inductive HingeOrbitTypeModComplement
 351  | o11
 352  | o12
 353  | o13
 354  | o22
 355  deriving DecidableEq, Repr, Fintype
 356
 357def HingeOrbitType.toModComplement : HingeOrbitType → HingeOrbitTypeModComplement
 358  | .t11 => .o11
 359  | .t12 | .t21 => .o12
 360  | .t13 | .t31 => .o13
 361  | .t22 => .o22
 362
 363theorem orbit_count_S4 : Fintype.card HingeOrbitType = 6 := by
 364  decide
 365
 366theorem orbit_count_S4_complement :
 367    Fintype.card HingeOrbitTypeModComplement = 4 := by
 368  decide
 369
 370/-! ## §6. Absolute within-cell triangles: type is not an `S₄`-orbit -/
 371
 372/-- Absolute vertex-mask triple of a slot, as a sorted 3-tuple of `ℕ`. -/
 373def absoluteTriple (s : Fin 24) (t : Fin 10) : ℕ × ℕ × ℕ :=
 374  triangleVertexMasks s t
 375
 376/-- Apply a coordinate permutation to an absolute triple. -/
 377def permTriple (p : Fin 24) (tr : ℕ × ℕ × ℕ) : ℕ × ℕ × ℕ :=
 378  (permMask (coordPermOf p) tr.1,
 379    permMask (coordPermOf p) tr.2.1,
 380    permMask (coordPermOf p) tr.2.2)
 381
 382/-- THEOREM (honest refinement): coordinate permutation does **not**
 383act transitively on absolute `(1,1)` triangles in the cell.  The seed
 384`{0,1,3}` and the interior chain `{1,3,7}` have the same difference
 385type but lie in distinct absolute `S₄`-orbits. -/
 386theorem absolute_t11_not_S4_transitive :
 387    hingeTypePop 0 0 = (1, 1) ∧
 388      hingeTypePop 0 6 = (1, 1) ∧
 389        absoluteTriple 0 0 = (0, 1, 3) ∧
 390          absoluteTriple 0 6 = (1, 3, 7) ∧
 391            (∀ p : Fin 24, permTriple p (0, 1, 3) ≠ (1, 3, 7)) := by
 392  decide
 393
 394/-! ## §7. Local squared-length data for star treatment -/
 395
 396/-- Flat squared edge lengths of a hinge with difference masks `(a,b)`:
 397the three boundary edges have Hamming weights `|a|`, `|b|`, `|a∨b|`. -/
 398structure OrbitLocalSq where
 399  lenA : ℕ
 400  lenB : ℕ
 401  lenAB : ℕ
 402  deriving DecidableEq, Repr
 403
 404def localSqOfDiff (a b : ℕ) : OrbitLocalSq :=
 405  ⟨maskPop a, maskPop b, maskPop (Nat.lor a b)⟩
 406
 407def orbitLocalSq : HingeOrbitType → OrbitLocalSq
 408  | ty => localSqOfDiff (orbitRep ty).1 (orbitRep ty).2
 409
 410theorem orbitLocalSq_values :
 411    orbitLocalSq .t11 = ⟨1, 1, 2⟩ ∧
 412      orbitLocalSq .t12 = ⟨1, 2, 3⟩ ∧
 413        orbitLocalSq .t21 = ⟨2, 1, 3⟩ ∧
 414          orbitLocalSq .t13 = ⟨1, 3, 4⟩ ∧
 415            orbitLocalSq .t31 = ⟨3, 1, 4⟩ ∧
 416              orbitLocalSq .t22 = ⟨2, 2, 4⟩ := by
 417  decide
 418
 419/-- THEOREM: local squared lengths of a cell triangle match its
 420difference-mask Hamming data. -/
 421theorem slot_localSq (s : Fin 24) (t : Fin 10) :
 422    localSqOfDiff (diffMaskA s t) (diffMaskB s t) =
 423      orbitLocalSq (hingeOrbitType s t) := by
 424  fin_cases s <;> fin_cases t <;> decide
 425
 426/-! ## §8. Status flags -/
 427
 428def hinge4DOrbitClassificationStatus : List String :=
 429  [ "THEOREM: six S4 lattice orbits by popcount type; cell counts 72/48/48/24/24/24"
 430  , "THEOREM: S4+complement merges (1,2)~(2,1) and (1,3)~(3,1) to four orbits"
 431  , "THEOREM: absolute within-cell triangles of fixed type need not form one S4 orbit"
 432  , "OPEN: per-orbit star kernels for the five non-seed S4 orbits"
 433  , "OPEN: flat Hessian assembly over all hinge orbits"
 434  , "NONCLAIM: S_RS_converges_EH_4d / gap_action_recovery" ]
 435
 436theorem hinge4DOrbitClassificationStatus_flags :
 437    hinge4DOrbitClassificationStatus.length = 6 ∧
 438      "OPEN: per-orbit star kernels for the five non-seed S4 orbits" ∈
 439        hinge4DOrbitClassificationStatus := by
 440  decide
 441
 442end ReggeHinge4DOrbitClassification
 443end Analysis
 444end Gravity
 445end IndisputableMonolith
 446