IndisputableMonolith.Gravity.Analysis.GeometricFoldVsDictionary4D

   1import Mathlib
   2import IndisputableMonolith.Gravity.Analysis.ReggeNormalizationDerived4D
   3import IndisputableMonolith.Gravity.Analysis.ReggeExactFlatHessianSymbol4D
   4import IndisputableMonolith.Gravity.Analysis.Regge4DExactActionSymbol
   5
   6/-!
   7# The geometric hinge fold is not the dictionary, and the gap is exactly two
   8
   9Arc 2, step 8.  Step 7 derived the Einstein-Hilbert transverse-traceless second
  10variation (`-(1/4)` per unit Frobenius and momentum) and pinned Regge's
  11normalization `ρ = 1/2`, which made the banked dictionary's `-(1/8)` the second
  12variation of the Regge action.  That closed the coefficient question.  It said
  13nothing about the limit, and this module is about what the tree's convergence
  14theorem actually converges.
  15
  16## The five objects
  17
  18`SRSConvergesEH4D.GeometricTendstoResidualOpen` bundles five typed residuals.
  19Four have inhabitants.  The fifth, `TypedResidual_fold_eq_midpointBloch` (R1),
  20asserts that the geometric hinge fold `Regge4DExactActionSymbol.exactFlatCrossTermFold`
  21equals the algebraic dictionary `exactMidpointBlochSymbol`, and no inhabitant of
  22it exists anywhere in the tree.  Since
  23`Regge4DContinuumPreflight.Regge4DContinuumSymbolIs` binds the dictionary, R1 is
  24the only statement that would carry the convergence theorem to the mesh.
  25
  26## What is proved here
  27
  28R1 is **false**, and the discrepancy is not a mystery: at both banked
  29transverse-traceless witnesses the dictionary's m² is exactly twice the geometric
  30hinge moment.  The corrected residual is therefore R1′, that *twice* the fold
  31equals the dictionary, and the tree already contains the doubled object under the
  32name `discreteExactReggeSymbol`.
  33
  34That makes the residual factor 4 recorded in `Regge4DTorusContinuumLimit`
  35(`-(1/16)` geometric against `-(1/4)` Einstein-Hilbert) a product of two twos:
  36the fold-to-action factor proved here, and Regge's `1/ρ` derived in step 7.  Only
  37the second is derived.
  38
  39§7 records why the earlier certificate suite could not have caught this.  Two of
  40its four witnesses on `symbolDir` are gauge zeros, and a witness where the
  41geometric side vanishes makes every candidate factor give the same prediction.
  42The other two were compared against `exactHessianM2AxisTTPlusCoeff`, a banked
  43constant documented as a coefficient per unit momentum, while the certificates
  44are values at `|symbolDir|² = 2`.  The numerals agreed and the quantities did
  45not.
  46
  47## Tags
  48
  49* THEOREM: everything below, at the base triple.  No `native_decide`, no `sorry`.
  50* Scope: the two named transverse-traceless witnesses on `symbolDir`.  The
  51  refutation of R1 needs only one witness; two independent ones agreeing at the
  52  same factor is what makes the factor a measurement rather than a coincidence.
  53* Not claimed: that the m² moment used here is the m² of `exactFlatCrossTermFold`
  54  itself.  `m2AllOrbitMomentDistinctHingeEdgeOrigins` is a hybrid (t11 from the
  55  legacy transported path, the other five orbits from edge origins) and is the
  56  object every banked geometric certificate in this tree is about.  Linking it to
  57  `exactFlatCrossTermFold` is a separate uninhabited step, named in §8.
  58-/
  59
  60namespace IndisputableMonolith
  61namespace Gravity
  62namespace Analysis
  63namespace GeometricFoldVsDictionary4D
  64
  65open BigOperators
  66open EdgeTTDecomposition4D (IsTT IsTraceless euclideanTrace axisTTPlus axisTTCross)
  67open ReggeBlochM2Symbol4D (symbolDir)
  68open ReggeExactFlatHessianBlochSymbol4D (exactMidpointBlochM2)
  69open ReggeBlochStarEdgeOrigins4D (m2AllOrbitMomentDistinctHingeEdgeOrigins)
  70open ReggeExactMidpointM2TTIdentity4D (exactMidpointBlochM2_eq_neg_eighth_frobenius_tt)
  71
  72noncomputable section
  73
  74/-! ## §1. Witness arithmetic
  75
  76The two banked polarizations both have Frobenius square 2 and the banked
  77direction has momentum square 2.  Every number below is one of these three.
  78-/
  79
  80theorem frobId_axisTTPlus :
  81    ReggeExactMidpointM2TTIdentity4D.frobeniusNormSq axisTTPlus = 2 := by
  82  unfold ReggeExactMidpointM2TTIdentity4D.frobeniusNormSq axisTTPlus
  83  norm_num [Fin.sum_univ_four]
  84
  85theorem frobId_axisTTCross :
  86    ReggeExactMidpointM2TTIdentity4D.frobeniusNormSq axisTTCross = 2 := by
  87  unfold ReggeExactMidpointM2TTIdentity4D.frobeniusNormSq axisTTCross
  88  norm_num [Fin.sum_univ_four]
  89
  90theorem waveId_symbolDir :
  91    ReggeExactMidpointM2TTIdentity4D.waveNormSq symbolDir = 2 := by
  92  unfold ReggeExactMidpointM2TTIdentity4D.waveNormSq symbolDir
  93  norm_num [Fin.sum_univ_four]
  94
  95/-- `symbolDir` is transverse to both banked polarizations, because their first two
  96rows and columns vanish.  Needed to apply the 1,208-row identity at this
  97direction rather than at the unit axis wave. -/
  98theorem axisTTPlus_isTT_symbolDir : IsTT symbolDir axisTTPlus := by
  99  refine ⟨?_, ?_, ?_⟩
 100  · intro i j; fin_cases i <;> fin_cases j <;> rfl
 101  · unfold IsTraceless euclideanTrace axisTTPlus
 102    simp [Fin.sum_univ_four]
 103  · intro i
 104    fin_cases i <;> simp [axisTTPlus, symbolDir, Fin.sum_univ_four]
 105
 106theorem axisTTCross_isTT_symbolDir : IsTT symbolDir axisTTCross := by
 107  refine ⟨?_, ?_, ?_⟩
 108  · intro i j; fin_cases i <;> fin_cases j <;> rfl
 109  · unfold IsTraceless euclideanTrace axisTTCross
 110    simp [Fin.sum_univ_four]
 111  · intro i
 112    fin_cases i <;> simp [axisTTCross, symbolDir, Fin.sum_univ_four]
 113
 114/-! ## §2. P1: the dictionary's m² at the witnesses
 115
 116From the banked identity over all 1,208 rows, with no tolerance and no
 117normalization freedom.
 118-/
 119
 120theorem dict_m2_axisTTPlus_symbolDir :
 121    exactMidpointBlochM2 axisTTPlus symbolDir = -(1 / 2 : ℝ) := by
 122  rw [exactMidpointBlochM2_eq_neg_eighth_frobenius_tt axisTTPlus symbolDir
 123      axisTTPlus_isTT_symbolDir, frobId_axisTTPlus, waveId_symbolDir]
 124  norm_num
 125
 126theorem dict_m2_axisTTCross_symbolDir :
 127    exactMidpointBlochM2 axisTTCross symbolDir = -(1 / 2 : ℝ) := by
 128  rw [exactMidpointBlochM2_eq_neg_eighth_frobenius_tt axisTTCross symbolDir
 129      axisTTCross_isTT_symbolDir, frobId_axisTTCross, waveId_symbolDir]
 130  norm_num
 131
 132/-! ## §3. The geometric moment at the same witnesses
 133
 134Restated from the banked `decide` certificates over `Fin 24 × Fin 10`, which are
 135kernel-checked and use no `native_decide`.
 136-/
 137
 138theorem geom_m2_axisTTPlus_symbolDir :
 139    m2AllOrbitMomentDistinctHingeEdgeOrigins axisTTPlus symbolDir = (-1 / 4 : ℝ) :=
 140  ReggeExactFlatHessianSymbol4D.exactHessian_m2_axisTTPlus_symbolDir
 141
 142theorem geom_m2_axisTTCross_symbolDir :
 143    m2AllOrbitMomentDistinctHingeEdgeOrigins axisTTCross symbolDir = (-1 / 4 : ℝ) :=
 144  ReggeExactFlatHessianSymbol4D.exactHessian_m2_axisTTCross_symbolDir
 145
 146theorem geom_m2_decoyGauge_symbolDir :
 147    m2AllOrbitMomentDistinctHingeEdgeOrigins ReggeEdgeStencil4D.decoyGauge symbolDir
 148      = (0 : ℝ) :=
 149  ReggeExactFlatHessianSymbol4D.exactHessian_m2_decoyGauge_symbolDir
 150
 151/-! ## §4. P2: R1 is false, and the gap is exactly two -/
 152
 153/-- **P2, first witness.**  The geometric hinge moment and the dictionary disagree. -/
 154theorem geom_ne_dict_axisTTPlus :
 155    m2AllOrbitMomentDistinctHingeEdgeOrigins axisTTPlus symbolDir
 156      ≠ exactMidpointBlochM2 axisTTPlus symbolDir := by
 157  rw [geom_m2_axisTTPlus_symbolDir, dict_m2_axisTTPlus_symbolDir]
 158  norm_num
 159
 160/-- **P2, second witness.**  Independently, on the cross polarization. -/
 161theorem geom_ne_dict_axisTTCross :
 162    m2AllOrbitMomentDistinctHingeEdgeOrigins axisTTCross symbolDir
 163      ≠ exactMidpointBlochM2 axisTTCross symbolDir := by
 164  rw [geom_m2_axisTTCross_symbolDir, dict_m2_axisTTCross_symbolDir]
 165  norm_num
 166
 167/-- **P2, the quantity.**  The dictionary is exactly twice the geometric moment. -/
 168theorem dict_eq_two_geom_axisTTPlus :
 169    exactMidpointBlochM2 axisTTPlus symbolDir
 170      = 2 * m2AllOrbitMomentDistinctHingeEdgeOrigins axisTTPlus symbolDir := by
 171  rw [dict_m2_axisTTPlus_symbolDir, geom_m2_axisTTPlus_symbolDir]
 172  norm_num
 173
 174theorem dict_eq_two_geom_axisTTCross :
 175    exactMidpointBlochM2 axisTTCross symbolDir
 176      = 2 * m2AllOrbitMomentDistinctHingeEdgeOrigins axisTTCross symbolDir := by
 177  rw [dict_m2_axisTTCross_symbolDir, geom_m2_axisTTCross_symbolDir]
 178  norm_num
 179
 180/-! ## §5. Discrimination: the factor is pinned, not fitted -/
 181
 182/-- The factor is unique.  Any real `c` satisfying the relation at the plus witness
 183is 2, so this is a measurement of the factor and not a choice of it. -/
 184theorem factor_pinned_axisTTPlus (c : ℝ)
 185    (h : exactMidpointBlochM2 axisTTPlus symbolDir
 186          = c * m2AllOrbitMomentDistinctHingeEdgeOrigins axisTTPlus symbolDir) :
 187    c = 2 := by
 188  rw [dict_m2_axisTTPlus_symbolDir, geom_m2_axisTTPlus_symbolDir] at h
 189  linarith
 190
 191theorem factor_pinned_axisTTCross (c : ℝ)
 192    (h : exactMidpointBlochM2 axisTTCross symbolDir
 193          = c * m2AllOrbitMomentDistinctHingeEdgeOrigins axisTTCross symbolDir) :
 194    c = 2 := by
 195  rw [dict_m2_axisTTCross_symbolDir, geom_m2_axisTTCross_symbolDir] at h
 196  linarith
 197
 198/-- `c = 1` fails, which is exactly the statement that R1 is refuted. -/
 199theorem factor_one_fails :
 200    exactMidpointBlochM2 axisTTPlus symbolDir
 201      ≠ 1 * m2AllOrbitMomentDistinctHingeEdgeOrigins axisTTPlus symbolDir := by
 202  rw [dict_m2_axisTTPlus_symbolDir, geom_m2_axisTTPlus_symbolDir]
 203  norm_num
 204
 205/-- `c = 4` fails too, so the fold-to-dictionary gap is not the whole factor 4
 206that separates the fold from the Einstein-Hilbert face. -/
 207theorem factor_four_fails :
 208    exactMidpointBlochM2 axisTTPlus symbolDir
 209      ≠ 4 * m2AllOrbitMomentDistinctHingeEdgeOrigins axisTTPlus symbolDir := by
 210  rw [dict_m2_axisTTPlus_symbolDir, geom_m2_axisTTPlus_symbolDir]
 211  norm_num
 212
 213/-! ## §6. P3 and P4: the two twos, and the factor four they compose to -/
 214
 215/-- The doubled geometric object already exists in the tree, and its factor is the
 216one measured in §4. -/
 217theorem doubled_fold_is_the_named_object (j : ℕ) (m : Fin 4 → ℤ)
 218    (E : Matrix (Fin 4) (Fin 4) ℝ) :
 219    Regge4DExactActionSymbol.discreteExactReggeSymbol j m E
 220      = 2 * Regge4DExactActionSymbol.finiteExactReggeSymbol j m E :=
 221  Regge4DExactActionSymbol.discreteExactReggeSymbol_eq j m E
 222
 223/-- **P3.**  Two definitions in this tree carry the name `discreteBookkeepingFactor`,
 224both equal 2, and they do different jobs: the first carries the geometric fold to
 225the Regge action, the second carries the Regge action to the Einstein-Hilbert
 226integral (step 7's `1/ρ`).  Their product is the residual 4. -/
 227theorem two_distinct_bookkeeping_factors :
 228    Regge4DExactActionSymbol.discreteBookkeepingFactor = 2 ∧
 229      ReggeExactFlatHessianNormGate4D.discreteBookkeepingFactor = 2 ∧
 230        Regge4DExactActionSymbol.discreteBookkeepingFactor
 231            * ReggeExactFlatHessianNormGate4D.discreteBookkeepingFactor = 4 := by
 232  refine ⟨Regge4DExactActionSymbol.discreteBookkeepingFactor_eq, ?_, ?_⟩
 233  · exact ReggeExactFlatHessianNormGate4D.discreteBookkeepingFactor_eq_two
 234  · rw [Regge4DExactActionSymbol.discreteBookkeepingFactor_eq,
 235      ReggeExactFlatHessianNormGate4D.discreteBookkeepingFactor_eq_two]
 236    norm_num
 237
 238theorem ehFace_axisTTPlus_symbolDir :
 239    ContinuumTTSecondVariation4D.ehFace axisTTPlus symbolDir = -(1 : ℝ) := by
 240  unfold ContinuumTTSecondVariation4D.ehFace
 241  rw [show EdgeTTDecomposition4D.momentumSq symbolDir = 2 from waveId_symbolDir,
 242    show ContinuumTTSecondVariation4D.frobSq axisTTPlus = 2 from frobId_axisTTPlus]
 243  norm_num
 244
 245/-- **P4.**  The derived Einstein-Hilbert face is four times the geometric hinge
 246moment at the witness, and §6 names both factors of that four.  Step 7 derived
 247one of them; the other is the subject of §8. -/
 248theorem ehFace_eq_four_times_geom :
 249    ContinuumTTSecondVariation4D.ehFace axisTTPlus symbolDir
 250      = 4 * m2AllOrbitMomentDistinctHingeEdgeOrigins axisTTPlus symbolDir := by
 251  rw [ehFace_axisTTPlus_symbolDir, geom_m2_axisTTPlus_symbolDir]
 252  norm_num
 253
 254/-- The Regge action face sits strictly between them, which is the whole content of
 255the two-step decomposition. -/
 256theorem reggeFace_between :
 257    ReggeNormalizationDerived4D.reggeFace ReggeNormalizationDerived4D.reggeNormalization
 258        axisTTPlus symbolDir
 259      = 2 * m2AllOrbitMomentDistinctHingeEdgeOrigins axisTTPlus symbolDir := by
 260  rw [ReggeNormalizationDerived4D.reggeFace_eq_dictionary axisTTPlus symbolDir
 261      axisTTPlus_isTT_symbolDir]
 262  exact dict_eq_two_geom_axisTTPlus
 263
 264/-! ## §7. Why the banked certificate suite could not have caught this
 265
 266Two of the four witnesses on `symbolDir` are gauge zeros.  Where the geometric
 267side vanishes, every candidate factor makes the same prediction, so such a
 268witness carries no information about the factor at all.  The two
 269transverse-traceless witnesses were read against a banked constant in a
 270different normalization.
 271-/
 272
 273/-- A witness on which the geometric moment vanishes cannot distinguish any two
 274candidate factors. -/
 275theorem vanishing_witness_admits_every_factor
 276    (H : Matrix (Fin 4) (Fin 4) ℝ) (k : Fin 4 → ℝ)
 277    (hg : m2AllOrbitMomentDistinctHingeEdgeOrigins H k = 0) (c c' : ℝ) :
 278    c * m2AllOrbitMomentDistinctHingeEdgeOrigins H k
 279      = c' * m2AllOrbitMomentDistinctHingeEdgeOrigins H k := by
 280  rw [hg]; ring
 281
 282/-- Instantiated at the banked gauge decoy: that certificate is compatible with
 283every factor, so its passing was never evidence about the factor. -/
 284theorem decoyGauge_admits_every_factor (c c' : ℝ) :
 285    c * m2AllOrbitMomentDistinctHingeEdgeOrigins ReggeEdgeStencil4D.decoyGauge symbolDir
 286      = c' * m2AllOrbitMomentDistinctHingeEdgeOrigins ReggeEdgeStencil4D.decoyGauge
 287          symbolDir :=
 288  vanishing_witness_admits_every_factor _ _ geom_m2_decoyGauge_symbolDir c c'
 289
 290/-- By contrast the transverse-traceless witness is informative, because the
 291geometric moment there is nonzero. -/
 292theorem tt_witness_is_informative :
 293    m2AllOrbitMomentDistinctHingeEdgeOrigins axisTTPlus symbolDir ≠ 0 := by
 294  rw [geom_m2_axisTTPlus_symbolDir]
 295  norm_num
 296
 297/-- The normalization mismatch that hid the factor.  `exactHessianM2AxisTTPlusCoeff`
 298is documented as the m² coefficient per unit momentum; the geometric certificate
 299is a value at `|symbolDir|² = 2`.  Read as the same quantity the two numerals
 300agree, and read correctly they differ. -/
 301theorem banked_coefficient_is_not_the_certificate_value :
 302    ReggeExactFlatHessianSymbol4D.exactHessianM2AxisTTPlusCoeff
 303        * ReggeExactMidpointM2TTIdentity4D.waveNormSq symbolDir
 304      ≠ m2AllOrbitMomentDistinctHingeEdgeOrigins axisTTPlus symbolDir := by
 305  rw [ReggeExactFlatHessianSymbol4D.exactHessianM2AxisTTPlusCoeff_eq, waveId_symbolDir,
 306    geom_m2_axisTTPlus_symbolDir]
 307  norm_num
 308
 309/-- And the numerals do coincide, which is how the mismatch survived reading. -/
 310theorem the_numerals_coincide :
 311    ReggeExactFlatHessianSymbol4D.exactHessianM2AxisTTPlusCoeff
 312      = m2AllOrbitMomentDistinctHingeEdgeOrigins axisTTPlus symbolDir := by
 313  rw [ReggeExactFlatHessianSymbol4D.exactHessianM2AxisTTPlusCoeff_eq,
 314    geom_m2_axisTTPlus_symbolDir]
 315  norm_num
 316
 317/-! ## §8. R1′, the corrected residual, and the discriminating gate -/
 318
 319/-- **R1′.**  The residual that should have been stated: twice the geometric hinge
 320fold equals the dictionary, everywhere, not once the fold equals it.  Stated for
 321the m² moments, which is where every certificate in this tree lives.  Uninhabited:
 322§4 establishes it at two witnesses only. -/
 323def FoldTimesTwoEqDictionaryM2 : Prop :=
 324  ∀ (H : Matrix (Fin 4) (Fin 4) ℝ) (k : Fin 4 → ℝ),
 325    IsTT k H →
 326      exactMidpointBlochM2 H k
 327        = 2 * m2AllOrbitMomentDistinctHingeEdgeOrigins H k
 328
 329/-- What §4 does establish: R1′ at the two banked witnesses, which is a strictly
 330weaker statement than `FoldTimesTwoEqDictionaryM2` and is named separately so the
 331two are never confused. -/
 332def FoldTimesTwoEqDictionaryAtBankedWitnesses : Prop :=
 333  exactMidpointBlochM2 axisTTPlus symbolDir
 334      = 2 * m2AllOrbitMomentDistinctHingeEdgeOrigins axisTTPlus symbolDir ∧
 335    exactMidpointBlochM2 axisTTCross symbolDir
 336      = 2 * m2AllOrbitMomentDistinctHingeEdgeOrigins axisTTCross symbolDir
 337
 338theorem foldTimesTwoEqDictionaryAtBankedWitnesses_holds :
 339    FoldTimesTwoEqDictionaryAtBankedWitnesses :=
 340  ⟨dict_eq_two_geom_axisTTPlus, dict_eq_two_geom_axisTTCross⟩
 341
 342/-- The discriminating gate for this step.  Six conjuncts, three of them
 343refutations, so the gate fails if any of the four numbers involved moves.  It is
 344not a `Bool`, and it does not report success on an empty computation. -/
 345def FoldDictionaryFactorDischarged : Prop :=
 346  FoldTimesTwoEqDictionaryAtBankedWitnesses
 347    ∧ (m2AllOrbitMomentDistinctHingeEdgeOrigins axisTTPlus symbolDir
 348        ≠ exactMidpointBlochM2 axisTTPlus symbolDir)
 349    ∧ (exactMidpointBlochM2 axisTTPlus symbolDir
 350        ≠ 1 * m2AllOrbitMomentDistinctHingeEdgeOrigins axisTTPlus symbolDir)
 351    ∧ (exactMidpointBlochM2 axisTTPlus symbolDir
 352        ≠ 4 * m2AllOrbitMomentDistinctHingeEdgeOrigins axisTTPlus symbolDir)
 353    ∧ ContinuumTTSecondVariation4D.ehFace axisTTPlus symbolDir
 354        = 4 * m2AllOrbitMomentDistinctHingeEdgeOrigins axisTTPlus symbolDir
 355    ∧ Regge4DExactActionSymbol.discreteBookkeepingFactor
 356        * ReggeExactFlatHessianNormGate4D.discreteBookkeepingFactor = 4
 357
 358theorem foldDictionaryFactorDischarged_holds : FoldDictionaryFactorDischarged := by
 359  refine ⟨foldTimesTwoEqDictionaryAtBankedWitnesses_holds, geom_ne_dict_axisTTPlus,
 360    factor_one_fails, factor_four_fails, ehFace_eq_four_times_geom, ?_⟩
 361  exact two_distinct_bookkeeping_factors.2.2
 362
 363/-- The honest reading of the convergence chain after this step.  Each conjunct is
 364an equation or a refutation over the reals, so the statement can fail. -/
 365def ConvergenceReachesDictionaryNotTheHingeMoment : Prop :=
 366  (m2AllOrbitMomentDistinctHingeEdgeOrigins axisTTPlus symbolDir
 367      ≠ exactMidpointBlochM2 axisTTPlus symbolDir)
 368    ∧ (m2AllOrbitMomentDistinctHingeEdgeOrigins axisTTCross symbolDir
 369        ≠ exactMidpointBlochM2 axisTTCross symbolDir)
 370    ∧ FoldTimesTwoEqDictionaryAtBankedWitnesses
 371
 372theorem convergenceReachesDictionaryNotTheHingeMoment_holds :
 373    ConvergenceReachesDictionaryNotTheHingeMoment :=
 374  ⟨geom_ne_dict_axisTTPlus, geom_ne_dict_axisTTCross,
 375    foldTimesTwoEqDictionaryAtBankedWitnesses_holds⟩
 376
 377end
 378
 379end GeometricFoldVsDictionary4D
 380end Analysis
 381end Gravity
 382end IndisputableMonolith
 383