IndisputableMonolith.Gravity.Analysis.RecognitionMeshExactJBridge4D

   1import Mathlib
   2import IndisputableMonolith.Gravity.Analysis.Regge4DContinuumPreflight
   3import IndisputableMonolith.Gravity.Analysis.ReggeFlat4DHessianAssembly
   4import IndisputableMonolith.Gravity.Analysis.ReggeBlochTransportedAllOrbit4D
   5import IndisputableMonolith.Gravity.Analysis.ReggeBlochAllOrbitSymbol4D
   6import IndisputableMonolith.Gravity.Analysis.Regge4DTorusContinuumLimit
   7import IndisputableMonolith.Gravity.Analysis.EdgeTTDecomposition4D
   8import IndisputableMonolith.Gravity.Analysis.ReggeExactFlatHessianBlochSymbol4D
   9import IndisputableMonolith.Gravity.Analysis.ReggeExactFlatHessianBlochTorusBridge4D
  10import IndisputableMonolith.Gravity.Analysis.ReggeExactMidpointM2TTIdentity4D
  11
  12/-!
  13# Recognition mesh exact-J → Option-C midpoint Bloch bridge (value level)
  14
  15QG full-theory campaign, Recognition gate of the 4D continuum closure.
  16Constructs the canonical Recognition mesh carrier for the periodic
  17Freudenthal 4-torus and attaches a value-level action whose amplitude
  18Hessian is the geometric Option-C midpoint Bloch symbol on the same
  19torus family.
  20
  21## Binding honesty
  22
  23* **MODEL** (Regge identification): `exactJActionOnMesh` is defined as the
  24  exact midpoint Bloch symbol on edge classes at amplitude `ε`
  25  (the geometric Option-C continuum object). Elevating that Hessian to
  26  the literal nonlinear Regge action via Schläfli remains OPEN;
  27  star-edge origins for non-`t11` orbits are now landed
  28  (`ReggeBlochStarEdgeOrigins4D`).
  29* This module does **not** consume `ExactJRefinementFamilyLimit` as a
  30  continuum premise (that family is amplitude scaling / response-level).
  31* Arbitrary `TestVariationPullback` hypotheses are excluded
  32  (`ArbitraryPullbackExcluded` from the preflight).
  33* Preferred limit shape: amplitude Hessian at fixed mesh, then `N → ∞`.
  34* **THEOREM:** amplitude Hessian exists and equals the mesh true-Regge
  35  Hessian by construction (`ExactJEqualsTrueReggeHessian`).
  36* **THEOREM:** iterated `N → ∞` Tendsto closes at the scale-explicit
  37  Option-C face `continuumEHScaleExplicitFace E`
  38  (`RecognitionExactJConvergesEH`) by composing the discrete torus bridge
  39  with the exact midpoint m² TT / gauge faces.
  40* Does **not** flip `gap_action_recovery`.
  41* Does **not** inhabit `S_RS_converges_EH_4d`.
  42-/
  43
  44namespace IndisputableMonolith
  45namespace Gravity
  46namespace Analysis
  47namespace RecognitionMeshExactJBridge4D
  48
  49open Regge4DContinuumPreflight
  50open ReggeFlat4DHessianAssembly
  51open Regge4DTorusContinuumLimit (intModeDir)
  52open EdgeTTDecomposition4D (IsTT)
  53open ReggeBlochAllOrbitSymbol4D (m2AllOrbitMomentPoly)
  54open ReggeExactFlatHessianBlochSymbol4D
  55open ReggeExactFlatHessianBlochTorusBridge4D
  56open ReggeExactMidpointM2TTIdentity4D
  57  (exactMidpointBlochM2_eq_neg_eighth_frobenius_tt
  58    exactMidpointBlochM2_gauge_rayleigh_eq_zero)
  59open Filter Topology
  60
  61noncomputable section
  62
  63/-- Local alias: preflight `Mat4` (avoids clash with transported abbrev). -/
  64abbrev Mat4 := Regge4DContinuumPreflight.Mat4
  65abbrev Wave4 := Regge4DContinuumPreflight.Wave4
  66
  67private theorem frobeniusNormSq_preflight_eq_identity (H : Mat4) :
  68    Regge4DContinuumPreflight.frobeniusNormSq H =
  69      ReggeExactMidpointM2TTIdentity4D.frobeniusNormSq H :=
  70  rfl
  71
  72private theorem waveNormSq_preflight_eq_identity (k : Wave4) :
  73    Regge4DContinuumPreflight.waveNormSq k =
  74      ReggeExactMidpointM2TTIdentity4D.waveNormSq k :=
  75  rfl
  76
  77/-! ## §1. Canonical Recognition mesh on the Freudenthal torus -/
  78
  79/-- Recognition-native mesh data for continuum index `j` (side `j+3`).
  80The exact flat cross-term Hessian on this carrier is the concrete
  81edge-class geometry; the continuum index records the torus family. -/
  82structure RecognitionFreudenthalMesh4D where
  83  continuumIndex : ℕ
  84  deriving Repr
  85
  86def RecognitionFreudenthalMesh4D.side (M : RecognitionFreudenthalMesh4D) : ℕ :=
  87  torusSide M.continuumIndex
  88
  89def RecognitionFreudenthalMesh4D.toTorus (M : RecognitionFreudenthalMesh4D) :
  90    CanonicalFreudenthalTorus4D :=
  91  ⟨M.continuumIndex⟩
  92
  93theorem RecognitionFreudenthalMesh4D.side_eq_torus
  94    (M : RecognitionFreudenthalMesh4D) :
  95    M.side = M.toTorus.side := rfl
  96
  97/-- Canonical mesh family used by the Recognition gate. -/
  98def canonicalRecognitionMesh (j : ℕ) : RecognitionFreudenthalMesh4D :=
  99  ⟨j⟩
 100
 101theorem canonicalRecognitionMesh_side (j : ℕ) :
 102    (canonicalRecognitionMesh j).side = j + 3 := rfl
 103
 104/-! ## §2. True-weight Regge Hessian on the mesh (edge classes) -/
 105
 106/-- Torus wave covector for the mesh side and integer mode. -/
 107def meshWave (M : RecognitionFreudenthalMesh4D) (m : IntMode4) : Wave4 :=
 108  realMode M.side m
 109
 110/-- Geometry-derived Option-C midpoint Bloch symbol on the Freudenthal
 111mesh.
 112
 113MODEL relative to nonlinear Regge: this is the assembled flat
 114midpoint Hessian, not yet fully Schläfli-elevated for every orbit. -/
 115def meshTrueReggeQuadraticHessian (M : RecognitionFreudenthalMesh4D)
 116    (m : IntMode4) (E : Mat4) : ℝ :=
 117  exactMidpointBlochSymbol E (meshWave M m)
 118
 119/-- True-weight zero-momentum Regge Hessian on the same polarization
 120(already proved to vanish on TT/gauge/trace in the assembly module). -/
 121def trueReggeZeroMomHessian (E : Mat4) : ℝ :=
 122  trueWeightZeroMomQuadratic E
 123
 124/-! ## §3. Value-level exact-J action (MODEL: Regge identification) -/
 125
 126/-- Recognition exact-J action on the mesh at amplitude `ε`.
 127
 128MODEL: identified with the true-weight Regge quadratic Hessian on the
 129same edge-class perturbation `ε • E` (homogeneous of degree two in the
 130fold).  Not an ArbitraryPullback / TestVariationPullback substitute.
 131Schläfli elevation remains OPEN. -/
 132def exactJActionOnMesh (M : RecognitionFreudenthalMesh4D)
 133    (m : IntMode4) (E : Mat4) (ε : ℝ) : ℝ :=
 134  (1 / 2) * ε ^ 2 * meshTrueReggeQuadraticHessian M m E
 135
 136theorem exactJActionOnMesh_eq
 137    (M : RecognitionFreudenthalMesh4D) (m : IntMode4) (E : Mat4) (ε : ℝ) :
 138    exactJActionOnMesh M m E ε =
 139      (1 / 2) * ε ^ 2 * meshTrueReggeQuadraticHessian M m E := rfl
 140
 141theorem exactJActionOnMesh_at_zero
 142    (M : RecognitionFreudenthalMesh4D) (m : IntMode4) (E : Mat4) :
 143    exactJActionOnMesh M m E 0 = 0 := by
 144  unfold exactJActionOnMesh
 145  ring
 146
 147/-- Second central difference of the exact-J action in amplitude. -/
 148def exactJSecondDiff (M : RecognitionFreudenthalMesh4D)
 149    (m : IntMode4) (E : Mat4) (ε : ℝ) : ℝ :=
 150  (exactJActionOnMesh M m E ε
 151    - 2 * exactJActionOnMesh M m E 0
 152    + exactJActionOnMesh M m E (-ε)) / ε ^ 2
 153
 154/-- **THEOREM:** for `ε ≠ 0` the amplitude second difference equals the
 155mesh true-Regge Hessian exactly (pure quadratic action). -/
 156theorem exactJSecondDiff_eq_meshHessian
 157    (M : RecognitionFreudenthalMesh4D) (m : IntMode4) (E : Mat4)
 158    {ε : ℝ} (hε : ε ≠ 0) :
 159    exactJSecondDiff M m E ε = meshTrueReggeQuadraticHessian M m E := by
 160  unfold exactJSecondDiff exactJActionOnMesh
 161  have hε2 : ε ^ 2 ≠ 0 := pow_ne_zero 2 hε
 162  field_simp [hε2]
 163  ring
 164
 165/-- The action is quadratic (not the previous definitional `0` shell):
 166its amplitude second difference is independent of `ε` for `ε ≠ 0`. -/
 167theorem exactJSecondDiff_independent_of_amplitude
 168    (M : RecognitionFreudenthalMesh4D) (m : IntMode4) (E : Mat4)
 169    {ε₁ ε₂ : ℝ} (h₁ : ε₁ ≠ 0) (h₂ : ε₂ ≠ 0) :
 170    exactJSecondDiff M m E ε₁ = exactJSecondDiff M m E ε₂ := by
 171  rw [exactJSecondDiff_eq_meshHessian M m E h₁,
 172    exactJSecondDiff_eq_meshHessian M m E h₂]
 173
 174/-! ## §4. Named bridge targets -/
 175
 176/-- At each fixed mesh, the amplitude second difference tends to a
 177quadratic tangent as `ε → 0`. -/
 178def ExactJAmplitudeHessianExists (M : RecognitionFreudenthalMesh4D)
 179    (m : IntMode4) (E : Mat4) (H : ℝ) : Prop :=
 180  Filter.Tendsto (fun ε : ℝ => exactJSecondDiff M m E ε)
 181    (nhdsWithin 0 {(0 : ℝ)}ᶜ) (nhds H)
 182
 183/-- **THEOREM:** the amplitude Hessian exists and equals the mesh
 184true-Regge Hessian. -/
 185theorem exactJAmplitudeHessian_eq_mesh
 186    (M : RecognitionFreudenthalMesh4D) (m : IntMode4) (E : Mat4) :
 187    ExactJAmplitudeHessianExists M m E
 188      (meshTrueReggeQuadraticHessian M m E) := by
 189  unfold ExactJAmplitudeHessianExists
 190  have hcongr :
 191      (fun ε : ℝ => exactJSecondDiff M m E ε) =ᶠ[nhdsWithin 0 {(0 : ℝ)}ᶜ]
 192        fun _ : ℝ => meshTrueReggeQuadraticHessian M m E := by
 193    filter_upwards [self_mem_nhdsWithin] with ε hε
 194    exact exactJSecondDiff_eq_meshHessian M m E hε
 195  exact (tendsto_congr' hcongr).mpr tendsto_const_nhds
 196
 197/-- Value-level identification of the exact-J amplitude Hessian with the
 198true-weight Regge Hessian on the same carrier (fixed mesh). -/
 199def ExactJEqualsTrueReggeHessian : Prop :=
 200  ∀ (j : ℕ) (m : IntMode4) (E : Mat4),
 201    m ≠ 0 →
 202      IsTTPolarization4D (fun i => (m i : ℝ)) E →
 203        ∃ H : ℝ,
 204          ExactJAmplitudeHessianExists (canonicalRecognitionMesh j) m E H ∧
 205            H = meshTrueReggeQuadraticHessian (canonicalRecognitionMesh j) m E
 206
 207/-- **THEOREM:** exact-J amplitude Hessian equals the mesh true-Regge
 208Hessian by construction (MODEL action identification). -/
 209theorem exactJEqualsTrueReggeHessian_holds :
 210    ExactJEqualsTrueReggeHessian := by
 211  intro j m E _hm _hTT
 212  refine ⟨meshTrueReggeQuadraticHessian (canonicalRecognitionMesh j) m E,
 213    exactJAmplitudeHessian_eq_mesh _ _ _, rfl⟩
 214
 215/-- Iterated continuum target: for each mesh take the amplitude Hessian,
 216then send mesh side `N → ∞` to the scale-explicit Option-C EH face after
 217`|k|²` normalization. -/
 218def RecognitionExactJConvergesEH : Prop :=
 219  ∀ (m : IntMode4) (E : Mat4),
 220    m ≠ 0 →
 221      IsTT (fun i => (m i : ℝ)) E →
 222        ∃ H : ℕ → ℝ,
 223          (∀ j : ℕ,
 224              ExactJAmplitudeHessianExists (canonicalRecognitionMesh j) m E
 225                (H j)) ∧
 226            Filter.Tendsto
 227              (fun j : ℕ => H j / momentumNormSq (torusSide j) m)
 228              Filter.atTop (nhds (continuumEHScaleExplicitFace E))
 229
 230/-- Non-vanishing of torus momentum for nonzero integer modes. -/
 231theorem momentumNormSq_ne_zero_of_mode
 232    (N : ℕ) (m : IntMode4) (hN : 0 < N) (hm : m ≠ 0) :
 233    momentumNormSq N m ≠ 0 := by
 234  rw [momentumNormSq_eq]
 235  have hsum : ∑ i : Fin 4, (m i : ℝ) ^ 2 ≠ 0 := by
 236    intro hzero
 237    have hmi : ∀ i : Fin 4, (m i : ℝ) = 0 := by
 238      intro i
 239      have :=
 240        (Finset.sum_eq_zero_iff_of_nonneg
 241            (fun i (_ : i ∈ Finset.univ) => sq_nonneg (m i : ℝ))).1
 242          hzero i (Finset.mem_univ i)
 243      exact sq_eq_zero_iff.mp this
 244    apply hm
 245    funext i
 246    exact Int.cast_eq_zero.mp (hmi i)
 247  have hN0 : (N : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr (ne_of_gt hN)
 248  have hpi : (2 * Real.pi : ℝ) ≠ 0 := by
 249    exact mul_ne_zero (by norm_num : (2 : ℝ) ≠ 0) Real.pi_ne_zero
 250  have hscale : ((2 * Real.pi) / (N : ℝ)) ^ 2 ≠ 0 :=
 251    pow_ne_zero 2 (div_ne_zero hpi hN0)
 252  exact mul_ne_zero hscale hsum
 253
 254theorem torusSide_pos (j : ℕ) : 0 < torusSide j := by
 255  unfold torusSide; omega
 256
 257/-- If the normalized mesh true-Regge Hessian tends to the scale-explicit
 258EH face, the Recognition iterated continuum Prop holds.
 259
 260This is the honest dependence on the algebraic/transported closer:
 261inhabit the hypothesis only when that closer proves the normalized
 262midpoint moment equals the Option-C face (not by baking EH into the
 263action). -/
 264theorem recognitionExactJConvergesEH_of_normalized_mesh
 265    (hlim :
 266      ∀ (m : IntMode4) (E : Mat4),
 267        m ≠ 0 →
 268          IsTT (fun i => (m i : ℝ)) E →
 269            Filter.Tendsto
 270              (fun j : ℕ =>
 271                meshTrueReggeQuadraticHessian (canonicalRecognitionMesh j) m E /
 272                  momentumNormSq (torusSide j) m)
 273              Filter.atTop (nhds (continuumEHScaleExplicitFace E))) :
 274    RecognitionExactJConvergesEH := by
 275  intro m E hm hTT
 276  refine ⟨fun j =>
 277      meshTrueReggeQuadraticHessian (canonicalRecognitionMesh j) m E, ?_, ?_⟩
 278  · intro j
 279    exact exactJAmplitudeHessian_eq_mesh _ _ _
 280  · exact hlim m E hm hTT
 281
 282/-- Gauge-zero companion for the Recognition mesh midpoint sequence. -/
 283def RecognitionExactJConvergesGaugeZero : Prop :=
 284  ∀ (m : IntMode4) (v : Wave4),
 285    m ≠ 0 →
 286      Filter.Tendsto
 287        (fun j : ℕ =>
 288          meshTrueReggeQuadraticHessian (canonicalRecognitionMesh j) m
 289              (pureGaugeFamily (fun i => (m i : ℝ)) v) /
 290            momentumNormSq (torusSide j) m)
 291        Filter.atTop (nhds 0)
 292
 293/-- The Recognition mesh midpoint sequence closes at the scale-explicit
 294Option-C EH face. -/
 295theorem recognitionExactJConvergesEH_closed :
 296    RecognitionExactJConvergesEH := by
 297  intro m E hm hTT
 298  refine ⟨fun j =>
 299      meshTrueReggeQuadraticHessian (canonicalRecognitionMesh j) m E, ?_, ?_⟩
 300  · intro j
 301    exact exactJAmplitudeHessian_eq_mesh _ _ _
 302  ·
 303    set k : Wave4 := fun i => (m i : ℝ)
 304    have hbridge := discrete_torus_family_bridge m E hm
 305    have hk : waveNormSq k ≠ 0 := waveNormSq_intMode_ne_zero m hm
 306    have hRay := exactMidpointBlochM2_eq_neg_eighth_frobenius_tt E k hTT
 307    have hF :
 308        ReggeExactMidpointM2TTIdentity4D.frobeniusNormSq E =
 309          frobeniusNormSq E :=
 310      (frobeniusNormSq_preflight_eq_identity E).symm
 311    have hw :
 312        ReggeExactMidpointM2TTIdentity4D.waveNormSq k = waveNormSq k :=
 313      (waveNormSq_preflight_eq_identity k).symm
 314    have hEq :
 315        exactMidpointBlochM2 E k / waveNormSq k =
 316          continuumEHScaleExplicitFace E := by
 317      calc
 318        exactMidpointBlochM2 E k / waveNormSq k
 319            = ((-(1 / 8) : ℝ) *
 320                  ReggeExactMidpointM2TTIdentity4D.frobeniusNormSq E *
 321                  ReggeExactMidpointM2TTIdentity4D.waveNormSq k) /
 322                waveNormSq k := by
 323              rw [hRay]
 324        _ = ((-(1 / 8) : ℝ) * frobeniusNormSq E * waveNormSq k) /
 325              waveNormSq k := by
 326              rw [hF, hw]
 327        _ = (-(1 / 8) : ℝ) * frobeniusNormSq E := by
 328              field_simp [hk]
 329        _ = continuumEHScaleExplicitFace E :=
 330              (continuumEHScaleExplicitFace_eq E).symm
 331    simpa [meshTrueReggeQuadraticHessian, meshWave, RecognitionFreudenthalMesh4D.side,
 332      canonicalRecognitionMesh, k, hEq] using hbridge
 333
 334/-- The Recognition mesh midpoint sequence vanishes on pure-gauge faces. -/
 335theorem recognitionExactJConvergesGaugeZero_closed :
 336    RecognitionExactJConvergesGaugeZero := by
 337  intro m v hm
 338  set E : Mat4 := pureGaugeFamily (fun i => (m i : ℝ)) v
 339  set k : Wave4 := fun i => (m i : ℝ)
 340  have hbridge := discrete_torus_family_bridge m E hm
 341  have hk : waveNormSq k ≠ 0 := waveNormSq_intMode_ne_zero m hm
 342  have hk' : ReggeExactMidpointM2TTIdentity4D.waveNormSq k ≠ 0 := by
 343    simpa [waveNormSq_preflight_eq_identity] using hk
 344  have hGauge : exactMidpointBlochM2 E k / waveNormSq k = 0 := by
 345    simpa [E, pureGaugeFamily] using exactMidpointBlochM2_gauge_rayleigh_eq_zero k v hk'
 346  simpa [meshTrueReggeQuadraticHessian, meshWave, RecognitionFreudenthalMesh4D.side,
 347    canonicalRecognitionMesh, E, k, hGauge] using hbridge
 348
 349/-- Parallel conditional on the factorized torus moment polynomial
 350equaling the frozen EH coefficient (same shape as the old
 351dictionary-constant theorem).  Does **not** discharge
 352`RecognitionExactJConvergesEH` by itself: the factorized scaffold is
 353not the transported continuum object
 354(`L-p1-factorized-vs-transported-fold`).  Recorded so a future
 355transported-moment equality can be swapped in. -/
 356def FactorizedMomentEqualsEH : Prop :=
 357  ∀ (m : IntMode4) (E : Mat4),
 358    m ≠ 0 →
 359      IsTT (fun i => (m i : ℝ)) E →
 360        m2AllOrbitMomentPoly E (intModeDir m) =
 361          continuumEHScaleExplicitFace E
 362
 363/-- Decoy: arbitrary pullbacks remain excluded. -/
 364theorem decoy_pullback_excluded : ArbitraryPullbackExcluded :=
 365  decoy_arbitrary_pullback_excluded
 366
 367/-! ## §5. Status -/
 368
 369structure RecognitionMeshExactJBridge4DStatus where
 370  meshCarrierDefined : Bool
 371  /-- Amplitude Hessian existence: CLOSED (equals mesh true-Regge). -/
 372  amplitudeHessianOpen : Bool
 373  /-- Iterated EH Tendsto: CLOSED at the scale-explicit Option-C face. -/
 374  iteratedEHOpen : Bool
 375  /-- Exact-J = true Regge Hessian: CLOSED by MODEL identification. -/
 376  equalsTrueReggeOpen : Bool
 377  gapActionRecovery : Bool
 378  /-- Honesty: Schläfli elevation of the MODEL action is not claimed. -/
 379  schlafliElevationOpen : Bool
 380
 381def recognitionMeshExactJBridge4DStatus :
 382    RecognitionMeshExactJBridge4DStatus where
 383  meshCarrierDefined := true
 384  amplitudeHessianOpen := false
 385  iteratedEHOpen := false
 386  equalsTrueReggeOpen := false
 387  gapActionRecovery := false
 388  schlafliElevationOpen := true
 389
 390theorem recognitionMeshExactJBridge4DStatus_flags :
 391    recognitionMeshExactJBridge4DStatus.meshCarrierDefined = true ∧
 392      recognitionMeshExactJBridge4DStatus.amplitudeHessianOpen = false ∧
 393        recognitionMeshExactJBridge4DStatus.iteratedEHOpen = false ∧
 394          recognitionMeshExactJBridge4DStatus.equalsTrueReggeOpen = false ∧
 395            recognitionMeshExactJBridge4DStatus.gapActionRecovery = false ∧
 396              recognitionMeshExactJBridge4DStatus.schlafliElevationOpen =
 397                true := by
 398  decide
 399
 400/-- Recognition closes the Option-C iterated EH face without flipping the ledger flag. -/
 401theorem recognition_iterated_eh_closed :
 402    recognitionMeshExactJBridge4DStatus.iteratedEHOpen = false ∧
 403      recognitionMeshExactJBridge4DStatus.gapActionRecovery = false := by
 404  decide
 405
 406end
 407
 408end RecognitionMeshExactJBridge4D
 409end Analysis
 410end Gravity
 411end IndisputableMonolith
 412