IndisputableMonolith.Gravity.Analysis.SRSConvergesScope4D

   1import Mathlib
   2import IndisputableMonolith.Gravity.Analysis.SRSConvergesEH4D
   3import IndisputableMonolith.Gravity.Analysis.GeometricFoldVsDictionary4D
   4
   5/-!
   6# What `S_RS_converges_EH_4d_closed` establishes, and what it excludes
   7
   8Arc 2, step 8, task 2.  `SRSConvergesEH4D` is the ledger-facing export module and
   9is left untouched; this module states its scope from outside, as theorems rather
  10than as a docstring.
  11
  12## The reading
  13
  14`S_RS_converges_EH_4d` is `Regge4DContinuumEHTarget ∧ Regge4DContinuumGaugeZeroTarget`.
  15The first conjunct says: for every nonzero integer mode and every
  16transverse-traceless polarization, the mesh sequence bound by
  17`Regge4DContinuumSymbolIs`, divided by the mesh momentum norm, converges to
  18`continuumEHScaleExplicitFace E`.  Two facts fix what that means.
  19
  201. The bound sequence is `finiteExactMidpointBlochSymbol`, the algebraic 1,208-row
  21   dictionary, not the geometric hinge fold.  The limit is genuinely `j`-dependent
  22   and is not a constant face, so the 2026 revert of the constant-face inhabitation
  23   is respected.
  242. The limit value is `-(1/8) · ‖E‖²_F`, which arc 2 step 7 derived to be the
  25   **Regge action's** transverse-traceless face, equal to `ρ` times the
  26   Einstein-Hilbert face with `ρ = 1/2`.
  27
  28So the theorem says the dictionary mesh symbol converges to the Regge action's
  29second variation.  That is the correct target for a Regge action and it is
  30derived.  What the theorem's *name* suggests, convergence to the Einstein-Hilbert
  31face, is false and provably so: §2 below shows the sequence cannot converge to the
  32Einstein-Hilbert face on any polarization of nonzero Frobenius mass, because the
  33limit is unique and the two candidate values differ by the factor `1/ρ`.
  34
  35## What it does not reach
  36
  37The geometric hinge fold.  R1, `TypedResidual_fold_eq_midpointBloch`, is the only
  38statement in the tree that would carry this limit to the mesh, and it has no
  39inhabitant.  `GeometricFoldVsDictionary4D` measures the gap: at both banked
  40transverse-traceless witnesses the dictionary's m² is exactly twice the geometric
  41hinge m² moment, with the factor pinned against 1 and 4.  §3 turns that
  42measurement into a conditional refutation of R1, with the two remaining premises
  43stated explicitly rather than assumed.
  44
  45## Tags
  46
  47* THEOREM: §1, §2, §3, at the base triple.
  48* Scope of §2: the exclusion is per mode and per polarization of nonzero
  49  Frobenius mass, and it is an exclusion about this mesh sequence only.
  50* Not claimed: that R1 is refuted outright.  §3 is a conditional, and its two
  51  premises are the honest residual.
  52-/
  53
  54namespace IndisputableMonolith
  55namespace Gravity
  56namespace Analysis
  57namespace SRSConvergesScope4D
  58
  59open Filter Topology
  60open Regge4DContinuumPreflight
  61open EdgeTTDecomposition4D (IsTT axisTTPlus)
  62open ReggeBlochM2Symbol4D (symbolDir)
  63open ReggeExactFlatHessianBlochSymbol4D (exactMidpointBlochSymbol exactMidpointBlochM2)
  64open ReggeBlochStarEdgeOrigins4D (m2AllOrbitMomentDistinctHingeEdgeOrigins)
  65open SRSConvergesEH4D (TypedResidual_fold_eq_midpointBloch S_RS_converges_EH_4d_closed)
  66
  67noncomputable section
  68
  69abbrev Mat4 := Regge4DContinuumPreflight.Mat4
  70abbrev Wave4 := Regge4DContinuumPreflight.Wave4
  71
  72/-! ## §1. The limit value is the Regge action face, which is `ρ` times the
  73Einstein-Hilbert face -/
  74
  75/-- The value the convergence theorem converges to, in closed form. -/
  76theorem srs_limit_value (E : Mat4) :
  77    continuumEHScaleExplicitFace E = -(1 / 8 : ℝ) * frobeniusNormSq E :=
  78  continuumEHScaleExplicitFace_eq E
  79
  80/-- The Einstein-Hilbert face for the same polarization, derived in step 7 and
  81carried here through the preflight's own name for it. -/
  82theorem eh_face_value (E : Mat4) :
  83    discreteExactReggeContinuumFaceCoeff E
  84      = (2 : ℝ) * (-(1 / 8 : ℝ)) * frobeniusNormSq E :=
  85  discreteExactReggeContinuumFaceCoeff_eq E
  86
  87/-- **The scope statement.**  The limit is Regge's normalization times the
  88Einstein-Hilbert face, so the theorem is about the Regge action. -/
  89theorem srs_limit_is_regge_normalization_times_eh (E : Mat4) :
  90    continuumEHScaleExplicitFace E
  91      = ReggeNormalizationDerived4D.reggeNormalization
  92          * discreteExactReggeContinuumFaceCoeff E := by
  93  rw [srs_limit_value, eh_face_value, ReggeNormalizationDerived4D.reggeNormalization]
  94  ring
  95
  96/-- And the two are different wherever the polarization carries mass, which is
  97what makes the previous line a correction and not a restatement. -/
  98theorem srs_limit_ne_eh_face (E : Mat4) (hE : frobeniusNormSq E ≠ 0) :
  99    continuumEHScaleExplicitFace E ≠ discreteExactReggeContinuumFaceCoeff E := by
 100  rw [srs_limit_value, eh_face_value]
 101  intro h
 102  apply hE
 103  have : (-(1 / 8 : ℝ)) * frobeniusNormSq E = 0 := by linarith
 104  rcases mul_eq_zero.mp this with h1 | h2
 105  · exact absurd h1 (by norm_num)
 106  · exact h2
 107
 108/-! ## §2. What the convergence claim excludes -/
 109
 110/-- **THEOREM.**  The mesh sequence provably does **not** converge to the
 111Einstein-Hilbert face, on any nonzero mode and any transverse-traceless
 112polarization carrying Frobenius mass.  This is the exclusion the convergence
 113claim buys: the limit exists, it is unique, and it is the Regge face. -/
 114theorem mesh_sequence_does_not_converge_to_eh_face
 115    (m : IntMode4) (E : Mat4) (hm : m ≠ 0)
 116    (hTT : IsTT (fun i => (m i : ℝ)) E) (hE : frobeniusNormSq E ≠ 0) :
 117    ¬ Regge4DContinuumSymbolIs m E (discreteExactReggeContinuumFaceCoeff E) := by
 118  intro hEH
 119  have hRegge : Regge4DContinuumSymbolIs m E (continuumEHScaleExplicitFace E) :=
 120    S_RS_converges_EH_4d_closed.1 m E hm hTT
 121  exact srs_limit_ne_eh_face E hE (continuumSymbolIs_unique hRegge hEH)
 122
 123/-- The positive half, restated so the pair reads as one scoped verdict. -/
 124theorem mesh_sequence_converges_to_the_regge_face
 125    (m : IntMode4) (E : Mat4) (hm : m ≠ 0)
 126    (hTT : IsTT (fun i => (m i : ℝ)) E) :
 127    Regge4DContinuumSymbolIs m E
 128      (ReggeNormalizationDerived4D.reggeNormalization
 129        * discreteExactReggeContinuumFaceCoeff E) := by
 130  rw [← srs_limit_is_regge_normalization_times_eh E]
 131  exact S_RS_converges_EH_4d_closed.1 m E hm hTT
 132
 133/-! ## §3. R1, conditionally refuted, with the two remaining premises named
 134
 135R1 asserts that the geometric fold and the dictionary are equal *as functions*.
 136Any functional of the symbol therefore takes the same value on both.  The two
 137premises below say only that each side's banked m² certificate is such a
 138functional of that side's symbol, which is what the phrase "the m² moment of"
 139means.  Neither is proved anywhere in the tree, and naming them is the point.
 140-/
 141
 142/-- **THEOREM.**  Under the two naming premises, R1 is false.  `moment` is an
 143arbitrary functional on symbol functions, so this uses nothing about how a
 144Taylor coefficient is computed. -/
 145theorem R1_fails_if_the_moments_read_their_symbols
 146    (moment : (Wave4 → ℝ) → ℝ)
 147    (hFold : moment (fun k => Regge4DExactActionSymbol.exactFlatCrossTermFold axisTTPlus k)
 148      = m2AllOrbitMomentDistinctHingeEdgeOrigins axisTTPlus symbolDir)
 149    (hDict : moment (fun k => exactMidpointBlochSymbol axisTTPlus k)
 150      = exactMidpointBlochM2 axisTTPlus symbolDir) :
 151    ¬ TypedResidual_fold_eq_midpointBloch := by
 152  intro hR1
 153  have hfun :
 154      (fun k => Regge4DExactActionSymbol.exactFlatCrossTermFold axisTTPlus k)
 155        = (fun k => exactMidpointBlochSymbol axisTTPlus k) :=
 156    funext (fun k => hR1 axisTTPlus k)
 157  rw [hfun, hDict] at hFold
 158  exact GeometricFoldVsDictionary4D.geom_ne_dict_axisTTPlus hFold.symm
 159
 160/-- The premises are not vacuous: the inequality they collide with is a pair of
 161kernel-checked values, and it is strict. -/
 162theorem the_collision_is_real :
 163    m2AllOrbitMomentDistinctHingeEdgeOrigins axisTTPlus symbolDir
 164        ≠ exactMidpointBlochM2 axisTTPlus symbolDir ∧
 165      exactMidpointBlochM2 axisTTPlus symbolDir
 166        = 2 * m2AllOrbitMomentDistinctHingeEdgeOrigins axisTTPlus symbolDir :=
 167  ⟨GeometricFoldVsDictionary4D.geom_ne_dict_axisTTPlus,
 168    GeometricFoldVsDictionary4D.dict_eq_two_geom_axisTTPlus⟩
 169
 170/-! ## §4. The scoped verdict as one statement -/
 171
 172/-- Everything step 8 licenses about the convergence claim, in one Prop that can
 173fail: the mesh sequence converges to the Regge face, it does not converge to the
 174Einstein-Hilbert face, and the geometric side differs from the sequence by a
 175factor of two at the banked witness. -/
 176def Step8ScopedVerdict : Prop :=
 177  (∀ (m : IntMode4) (E : Mat4), m ≠ 0 → IsTT (fun i => (m i : ℝ)) E →
 178      Regge4DContinuumSymbolIs m E
 179        (ReggeNormalizationDerived4D.reggeNormalization
 180          * discreteExactReggeContinuumFaceCoeff E))
 181    ∧ (∀ (m : IntMode4) (E : Mat4), m ≠ 0 → IsTT (fun i => (m i : ℝ)) E →
 182        frobeniusNormSq E ≠ 0 →
 183          ¬ Regge4DContinuumSymbolIs m E (discreteExactReggeContinuumFaceCoeff E))
 184    ∧ (m2AllOrbitMomentDistinctHingeEdgeOrigins axisTTPlus symbolDir
 185        ≠ exactMidpointBlochM2 axisTTPlus symbolDir)
 186
 187theorem step8ScopedVerdict_holds : Step8ScopedVerdict :=
 188  ⟨fun m E hm hTT => mesh_sequence_converges_to_the_regge_face m E hm hTT,
 189    fun m E hm hTT hE => mesh_sequence_does_not_converge_to_eh_face m E hm hTT hE,
 190    GeometricFoldVsDictionary4D.geom_ne_dict_axisTTPlus⟩
 191
 192end
 193
 194end SRSConvergesScope4D
 195end Analysis
 196end Gravity
 197end IndisputableMonolith
 198