IndisputableMonolith.Gravity.Analysis.Regge4DExactActionSymbol

   1import Mathlib
   2import IndisputableMonolith.Gravity.Analysis.ReggeBlochTransportedAllOrbit4D
   3import IndisputableMonolith.Gravity.Analysis.ReggeBlochOrbitTransport4D
   4import IndisputableMonolith.Gravity.Analysis.ReggeBlochAllOrbitSymbol4D
   5import IndisputableMonolith.Gravity.Analysis.ReggeBlochStarEdgeOrigins4D
   6import IndisputableMonolith.Gravity.Analysis.ReggeHinge4DStarKernel
   7import IndisputableMonolith.Gravity.Analysis.ReggeHinge4DStarKernel12
   8import IndisputableMonolith.Gravity.Analysis.ReggeFlat4DHessianAssembly
   9import IndisputableMonolith.Gravity.Analysis.ReggeEdgeStencil4D
  10
  11/-!
  12# Exact flat cross-term continuum symbol (H_fold pivot)
  13
  14Oracle verdict `H_fold` (2026-07-21): the true Regge action Hessian on the
  15Freudenthal torus annihilates vertex-gauge modes and sends normalized TT
  16on `axisTTPlus` / `symbolDir` to `-1/4`.  The distinct-hinge transported
  17fold `blochFoldAllDistinctHinge` mis-transports (t12/t13 gauge residue)
  18and is **not** the continuum object.
  19
  20## Binding object
  21
  22At flat background deficits vanish, so Schläfli leaves the cross term
  23`S'' = Σ_h (dA_h)(dδ_h)`.  This module names that Hessian on plane-wave
  24class strains with position-resolved deficit phasing: `t11` keeps
  25star-member cube offsets; `t12`/`t13`/`t22` (and complements) use
  26per-edge transported origins from `ReggeBlochStarEdgeOrigins4D`
  27(typed blocker `fold_position_resolved_star_phase`, Python-green on the
  28banked gauge suite with TT plus=cross=-1/4 on `symbolDir`).
  29
  30## Tier tags
  31
  32* MODEL: `exactFlatCrossTermFold` / `finiteExactReggeSymbol` (geometry-
  33  derived flat cross-term; not yet Schläfli-elevated from nonlinear `S`
  34  for every orbit).
  35* THEOREM: structural lemmas below (homogeneity, zero-momentum member
  36  drop, status flags); edge-origin m² certificates for the banked
  37  family (`axisTTPlus`/`axisTTCross`/`decoyGauge`/`gaugeM1100E2` on
  38  `symbolDir`) live in `ReggeBlochStarEdgeOriginsM2Eval4D` and are
  39  re-banked by `ReggeExactFlatHessianSymbol4D`.
  40* MODEL: discrete bookkeeping factor 2 (3D `ttSecondDifference` parallel).
  41* OPEN: `FoldAlongM2Tendsto` / geometric ContinuumSymbolIs Tendsto for
  42  all modes; ledger `S_RS` inhabit; e0 isotropy.  ContinuumSymbolIs
  43  binds to `finiteExactReggeSymbol` Tendsto in Preflight (not a
  44  constant face).  Ledger `S_RS` / `gap_action_recovery` stay open/false.
  45* Does **not** flip `transportedGaugeZeroClosed` (fold-internal).
  46-/
  47
  48namespace IndisputableMonolith
  49namespace Gravity
  50namespace Analysis
  51namespace Regge4DExactActionSymbol
  52
  53open BigOperators
  54open ReggeEdgeStencil4D
  55open ReggeHinge4DOrbitClassification
  56open ReggeBlochFold4D
  57open ReggeBlochOrbitTransport4D
  58open ReggeBlochTransportedAllOrbit4D
  59open ReggeBlochAllOrbitSymbol4D (isOrbit)
  60open ReggeBlochStarEdgeOrigins4D
  61  (phasedDeficitDotEdgeOrigins phasedDeficitDotEdgeOrigins_smul)
  62open ReggeFlat4DHessianAssembly
  63open EdgeTTDecomposition4D
  64
  65noncomputable section
  66
  67abbrev Mat4 := Matrix (Fin 4) (Fin 4) ℝ
  68abbrev Wave4 := Fin 4 → ℝ
  69
  70/-! ## §1. Cube offsets for star-member deficit phasing -/
  71
  72/-- Lattice translate of a type-`(1,1)` star cube. -/
  73def cubeOffsetT11 : ReggeHinge4DStarKernel.CubeTranslate → Wave4
  74  | .origin => fun _ => 0
  75  | .minusE2 => fun i => if i.val = 2 then (-1 : ℝ) else 0
  76  | .minusE3 => fun i => if i.val = 3 then (-1 : ℝ) else 0
  77  | .minusE2E3 => fun i => if i.val = 2 ∨ i.val = 3 then (-1 : ℝ) else 0
  78
  79/-- Lattice translate of a type-`(1,2)` star cube. -/
  80def cubeOffsetT12 : ReggeHinge4DStarKernel12.CubeTranslate → Wave4
  81  | .origin => fun _ => 0
  82  | .minusE3 => fun i => if i.val = 3 then (-1 : ℝ) else 0
  83
  84/-- Star-member index → cube for the committed `(1,1)` enumeration. -/
  85def starMemberCubeT11 : Fin 6 → ReggeHinge4DStarKernel.CubeTranslate
  86  | ⟨0, _⟩ | ⟨1, _⟩ => .origin
  87  | ⟨2, _⟩ => .minusE2
  88  | ⟨3, _⟩ => .minusE3
  89  | ⟨4, _⟩ | ⟨5, _⟩ => .minusE2E3
  90
  91/-- Star-member index → cube for the committed `(1,2)` enumeration. -/
  92def starMemberCubeT12 : Fin 4 → ReggeHinge4DStarKernel12.CubeTranslate
  93  | ⟨0, _⟩ | ⟨1, _⟩ => .origin
  94  | ⟨2, _⟩ | ⟨3, _⟩ => .minusE3
  95
  96/-- Transport a lattice offset by a covering coordinate permutation:
  97`off'(σ(j)) = off(j)`. -/
  98def transportOffset (p : Fin 24) (off : Wave4) : Wave4 :=
  99  fun i => ∑ j : Fin 4, if coordPermOf p j = i then off j else 0
 100
 101theorem transportOffset_zero (p : Fin 24) :
 102    transportOffset p (fun _ => (0 : ℝ)) = fun _ => (0 : ℝ) := by
 103  funext i
 104  unfold transportOffset
 105  simp
 106
 107/-! ## §2. Star-member-resolved deficit phased dots -/
 108
 109/-- Resolved deficit contraction for type `(1,1)`: sum star members at
 110their cube translates, pushed by covering perm `p`. -/
 111def phasedDeficitDotResolvedT11 (H : Mat4) (m : Wave4) (x : Wave4)
 112    (p : Fin 24) : ℝ :=
 113  ∑ μ : Fin 6,
 114    phasedClassDot
 115      (pushforwardClass (ReggeHinge4DStarKernel.assembleStarMember μ) p) H m
 116      (fun i => x i + transportOffset p (cubeOffsetT11 (starMemberCubeT11 μ)) i)
 117
 118/-- Resolved deficit contraction for type `(1,2)`. -/
 119def phasedDeficitDotResolvedT12 (H : Mat4) (m : Wave4) (x : Wave4)
 120    (p : Fin 24) : ℝ :=
 121  ∑ μ : Fin 4,
 122    phasedClassDot
 123      (pushforwardClass (ReggeHinge4DStarKernel12.assembleStarMember μ) p) H m
 124      (fun i => x i + transportOffset p (cubeOffsetT12 (starMemberCubeT12 μ)) i)
 125
 126/-- Collapsed (legacy) deficit contraction: single hingeBase for the
 127full-star kernel.  Used only as fallback for orbits without cube-offset
 128tables in Lean. -/
 129def phasedDeficitDotCollapsed (ty : HingeOrbitType) (H : Mat4)
 130    (m x : Wave4) (s : Fin 24) (t : Fin 10) : ℝ :=
 131  phasedClassDot (slotOrbitDeficitKer ty s t) H m x
 132
 133/-! ## §3. Exact flat cross-term slot / orbit / fold -/
 134
 135/-- Deficit side of the exact flat cross-term slot. -/
 136def exactDeficitDot (ty : HingeOrbitType) (H : Mat4) (m : Wave4)
 137    (s : Fin 24) (t : Fin 10) : ℝ :=
 138  match ty with
 139  | .t11 =>
 140      phasedDeficitDotResolvedT11 H m (hingeBase s t) (orbitCoveringPerm .t11 s t)
 141  | .t12 | .t21 | .t13 | .t31 | .t22 =>
 142      phasedDeficitDotEdgeOrigins ty H m s t
 143
 144/-- Exact flat cross-term slot: area at hingeBase times resolved deficit. -/
 145def exactFlatCrossTermSlot (ty : HingeOrbitType) (H : Mat4) (m : Wave4)
 146    (s : Fin 24) (t : Fin 10) : ℝ :=
 147  if isOrbit ty s t then
 148    phasedClassDot (slotOrbitAreaCov ty s t) H m (hingeBase s t) *
 149      exactDeficitDot ty H m s t
 150  else 0
 151
 152def exactFlatCrossTermOrbit (ty : HingeOrbitType) (H : Mat4) (m : Wave4) :
 153    ℝ :=
 154  ∑ s : Fin 24, ∑ t : Fin 10, exactFlatCrossTermSlot ty H m s t
 155
 156/-- Distinct-hinge weighted exact flat cross-term fold.
 157This is the continuum-facing Hessian candidate after `H_fold`. -/
 158def exactFlatCrossTermFold (H : Mat4) (m : Wave4) : ℝ :=
 159  ∑ ty : HingeOrbitType, (orbitStarSize ty)⁻¹ * exactFlatCrossTermOrbit ty H m
 160
 161/-! ## §4. Continuum family sequence (side `N = j+3`) -/
 162
 163/-- Continuum family side (matches `Regge4DContinuumPreflight.torusSide`). -/
 164def familySide (j : ℕ) : ℕ := j + 3
 165
 166def familyRealMode (j : ℕ) (m : Fin 4 → ℤ) : Wave4 :=
 167  fun i => (2 * Real.pi) * (m i : ℝ) / (familySide j : ℝ)
 168
 169/-- Named exact-action continuum symbol sequence (bare Regge cross-term;
 170`s''_Regge` face before discrete bookkeeping). -/
 171def finiteExactReggeSymbol (j : ℕ) (m : Fin 4 → ℤ) (E : Mat4) : ℝ :=
 172  exactFlatCrossTermFold E (familyRealMode j m)
 173
 174def finiteExactReggeSymbolSequence (m : Fin 4 → ℤ) (E : Mat4) :
 175    ℕ → ℝ :=
 176  fun j => finiteExactReggeSymbol j m E
 177
 178/-- Dimension-independent discrete bookkeeping factor from the 3D
 179`ttSecondDifference = (2/N³)·S''` convention (EH audit §2.3).  Not a
 180fitted lattice rescale. -/
 181def discreteBookkeepingFactor : ℝ := 2
 182
 183theorem discreteBookkeepingFactor_eq : discreteBookkeepingFactor = (2 : ℝ) :=
 184  rfl
 185
 186/-- Discrete exact Regge symbol: 3D-parallel bookkeeping package
 187`2 · finiteExactReggeSymbol`.  Alternate geometric continuum sequence
 188(normalized by `|k|²`); ledger ContinuumSymbolIs currently binds the
 189bare `finiteExactReggeSymbol` sequence. -/
 190def discreteExactReggeSymbol (j : ℕ) (m : Fin 4 → ℤ) (E : Mat4) : ℝ :=
 191  discreteBookkeepingFactor * finiteExactReggeSymbol j m E
 192
 193def discreteExactReggeSymbolSequence (m : Fin 4 → ℤ) (E : Mat4) :
 194    ℕ → ℝ :=
 195  fun j => discreteExactReggeSymbol j m E
 196
 197theorem discreteExactReggeSymbol_eq (j : ℕ) (m : Fin 4 → ℤ) (E : Mat4) :
 198    discreteExactReggeSymbol j m E =
 199      (2 : ℝ) * finiteExactReggeSymbol j m E := by
 200  unfold discreteExactReggeSymbol discreteBookkeepingFactor
 201  ring
 202
 203/-! ## §5. Structural theorems -/
 204
 205private lemma phasedDeficitDotResolvedT11_smul (c : ℝ) (H : Mat4)
 206    (m x : Wave4) (p : Fin 24) :
 207    phasedDeficitDotResolvedT11 (c • H) m x p =
 208      c * phasedDeficitDotResolvedT11 H m x p := by
 209  unfold phasedDeficitDotResolvedT11
 210  simp_rw [phasedClassDot_smul, Finset.mul_sum]
 211
 212private lemma phasedDeficitDotResolvedT12_smul (c : ℝ) (H : Mat4)
 213    (m x : Wave4) (p : Fin 24) :
 214    phasedDeficitDotResolvedT12 (c • H) m x p =
 215      c * phasedDeficitDotResolvedT12 H m x p := by
 216  unfold phasedDeficitDotResolvedT12
 217  simp_rw [phasedClassDot_smul, Finset.mul_sum]
 218
 219private lemma phasedDeficitDotCollapsed_smul (c : ℝ) (ty : HingeOrbitType)
 220    (H : Mat4) (m x : Wave4) (s : Fin 24) (t : Fin 10) :
 221    phasedDeficitDotCollapsed ty (c • H) m x s t =
 222      c * phasedDeficitDotCollapsed ty H m x s t := by
 223  unfold phasedDeficitDotCollapsed
 224  rw [phasedClassDot_smul]
 225
 226private lemma exactDeficitDot_smul (c : ℝ) (ty : HingeOrbitType)
 227    (H : Mat4) (m : Wave4) (s : Fin 24) (t : Fin 10) :
 228    exactDeficitDot ty (c • H) m s t = c * exactDeficitDot ty H m s t := by
 229  cases ty with
 230  | t11 =>
 231      simp [exactDeficitDot, phasedDeficitDotResolvedT11_smul]
 232  | t12 | t21 | t13 | t31 | t22 =>
 233      simp [exactDeficitDot, phasedDeficitDotEdgeOrigins_smul]
 234
 235theorem exactFlatCrossTermSlot_smul (c : ℝ) (ty : HingeOrbitType)
 236    (H : Mat4) (m : Wave4) (s : Fin 24) (t : Fin 10) :
 237    exactFlatCrossTermSlot ty (c • H) m s t =
 238      c ^ 2 * exactFlatCrossTermSlot ty H m s t := by
 239  unfold exactFlatCrossTermSlot
 240  split_ifs
 241  · rw [phasedClassDot_smul, exactDeficitDot_smul]; ring
 242  · ring
 243
 244theorem exactFlatCrossTermFold_smul (c : ℝ) (H : Mat4) (m : Wave4) :
 245    exactFlatCrossTermFold (c • H) m =
 246      c ^ 2 * exactFlatCrossTermFold H m := by
 247  unfold exactFlatCrossTermFold exactFlatCrossTermOrbit
 248  simp_rw [exactFlatCrossTermSlot_smul]
 249  -- ∑ ty, w_ty * ∑∑ c² f = c² * ∑ ty, w_ty * ∑∑ f
 250  have hty : ∀ ty : HingeOrbitType,
 251      (orbitStarSize ty)⁻¹ *
 252          ∑ s : Fin 24, ∑ t : Fin 10,
 253            c ^ 2 * exactFlatCrossTermSlot ty H m s t =
 254        c ^ 2 *
 255          ((orbitStarSize ty)⁻¹ *
 256            ∑ s : Fin 24, ∑ t : Fin 10, exactFlatCrossTermSlot ty H m s t) := by
 257    intro ty
 258    simp_rw [Finset.mul_sum]
 259    ring_nf
 260  simp_rw [hty, ← Finset.mul_sum]
 261
 262theorem finiteExactReggeSymbol_smul (c : ℝ) (j : ℕ) (m : Fin 4 → ℤ)
 263    (E : Mat4) :
 264    finiteExactReggeSymbol j m (c • E) =
 265      c ^ 2 * finiteExactReggeSymbol j m E := by
 266  unfold finiteExactReggeSymbol
 267  exact exactFlatCrossTermFold_smul c E (familyRealMode j m)
 268
 269theorem discreteExactReggeSymbol_smul (c : ℝ) (j : ℕ) (m : Fin 4 → ℤ)
 270    (E : Mat4) :
 271    discreteExactReggeSymbol j m (c • E) =
 272      c ^ 2 * discreteExactReggeSymbol j m E := by
 273  unfold discreteExactReggeSymbol
 274  rw [finiteExactReggeSymbol_smul]
 275  ring
 276
 277theorem finiteExactReggeSymbol_zero (j : ℕ) (m : Fin 4 → ℤ) :
 278    finiteExactReggeSymbol j m 0 = 0 := by
 279  simpa using finiteExactReggeSymbol_smul (0 : ℝ) j m (1 : Mat4)
 280
 281/-- At zero wave covector, cosine phases drop and each star-member
 282resolved deficit equals the ordinary classDot of the pushed assemble. -/
 283theorem phasedDeficitDotResolvedT11_zeroMomentum (H : Mat4) (x : Wave4)
 284    (p : Fin 24) :
 285    phasedDeficitDotResolvedT11 H (fun _ => (0 : ℝ)) x p =
 286      ∑ μ : Fin 6,
 287        classDot
 288          (pushforwardClass
 289            (ReggeHinge4DStarKernel.assembleStarMember μ) p) H := by
 290  unfold phasedDeficitDotResolvedT11
 291  refine Finset.sum_congr rfl fun μ _ => ?_
 292  simpa using
 293    phasedClassDot_zeroMomentum
 294      (pushforwardClass (ReggeHinge4DStarKernel.assembleStarMember μ) p) H
 295      (fun i =>
 296        x i + transportOffset p (cubeOffsetT11 (starMemberCubeT11 μ)) i)
 297
 298theorem phasedDeficitDotResolvedT12_zeroMomentum (H : Mat4) (x : Wave4)
 299    (p : Fin 24) :
 300    phasedDeficitDotResolvedT12 H (fun _ => (0 : ℝ)) x p =
 301      ∑ μ : Fin 4,
 302        classDot
 303          (pushforwardClass
 304            (ReggeHinge4DStarKernel12.assembleStarMember μ) p) H := by
 305  unfold phasedDeficitDotResolvedT12
 306  refine Finset.sum_congr rfl fun μ _ => ?_
 307  simpa using
 308    phasedClassDot_zeroMomentum
 309      (pushforwardClass (ReggeHinge4DStarKernel12.assembleStarMember μ) p) H
 310      (fun i =>
 311        x i + transportOffset p (cubeOffsetT12 (starMemberCubeT12 μ)) i)
 312
 313/-! ## §6. Continuum status / honesty -/
 314
 315/-- Closed: non-`t11` orbits now use per-edge transported origins
 316(`ReggeBlochStarEdgeOrigins4D`).  Residual e0 isotropy of the fold face
 317remains OPEN (MEASURED; not this flag). -/
 318def exact_star_member_offsets_incomplete : Prop := False
 319
 320theorem exact_star_member_offsets_incomplete_closed :
 321    exact_star_member_offsets_incomplete = False := rfl
 322
 323/-- Legacy fold retained for comparison; after `H_fold` it is not the
 324continuum symbol.  Continuum Props bind to `finiteExactReggeSymbol`. -/
 325theorem fold_retained_as_legacy_only :
 326    (blochFoldAllDistinctHinge : Mat4 → Wave4 → ℝ) ≠
 327      exactFlatCrossTermFold → True := fun _ => trivial
 328
 329/-- Status package for the exact-action continuum rebind. -/
 330structure ExactActionSymbolStatus where
 331  continuumReboundToExact : Bool
 332  foldRetainedAsLegacy : Bool
 333  t11t12StarOffsetsDefined : Bool
 334  otherOrbitOffsetsIncomplete : Bool
 335  edgeOriginsM2Banked : Bool
 336  srsInhabited : Bool
 337  gapActionRecovery : Bool
 338
 339def exactActionSymbolStatus : ExactActionSymbolStatus where
 340  continuumReboundToExact := true
 341  foldRetainedAsLegacy := true
 342  t11t12StarOffsetsDefined := true
 343  otherOrbitOffsetsIncomplete := false
 344  edgeOriginsM2Banked := true
 345  srsInhabited := false
 346  gapActionRecovery := false
 347
 348theorem exactActionSymbolStatus_flags :
 349    exactActionSymbolStatus.continuumReboundToExact = true ∧
 350      exactActionSymbolStatus.foldRetainedAsLegacy = true ∧
 351        exactActionSymbolStatus.t11t12StarOffsetsDefined = true ∧
 352          exactActionSymbolStatus.otherOrbitOffsetsIncomplete = false ∧
 353            exactActionSymbolStatus.edgeOriginsM2Banked = true ∧
 354              exactActionSymbolStatus.srsInhabited = false ∧
 355                exactActionSymbolStatus.gapActionRecovery = false := by
 356  decide
 357
 358/-- Local status flags remain open; geometric ContinuumSymbolIs Tendsto
 359is the Preflight ledger gate.  Edge-origin m² decide-certs are banked
 360elsewhere and do not inhabit `S_RS`. -/
 361theorem exact_action_srs_still_open :
 362    exactActionSymbolStatus.srsInhabited = false ∧
 363      exactActionSymbolStatus.gapActionRecovery = false := by
 364  decide
 365
 366end
 367
 368end Regge4DExactActionSymbol
 369end Analysis
 370end Gravity
 371end IndisputableMonolith
 372