IndisputableMonolith.Gravity.Analysis.ReggeBlochLocalIncidenceM2Eval4D

   1import Mathlib
   2import IndisputableMonolith.Gravity.Analysis.ReggeBlochLocalIncidence4D
   3import IndisputableMonolith.Gravity.Analysis.ReggeBlochTransportedAllOrbitM2Eval4D
   4import IndisputableMonolith.Gravity.Analysis.Regge4DContinuumPreflight
   5import IndisputableMonolith.Gravity.Analysis.Regge4DTorusContinuumLimit
   6
   7/-!
   8# Path B vs distinct-hinge witness comparison
   9
  10Mean-local Path B equals distinct-hinge on every ray (vacuous).
  11Position-resolved Path B does **not** hit EH and does **not** restore
  12isotropy (MEASURED receipt
  13`state/qg_full_theory/probe_pathB_local_incidence_20260721.json`).
  14
  15Does **not** flip `gap_action_recovery`.
  16-/
  17
  18namespace IndisputableMonolith
  19namespace Gravity
  20namespace Analysis
  21namespace ReggeBlochLocalIncidenceM2Eval4D
  22
  23open BigOperators
  24open ReggeBlochLocalIncidence4D
  25open ReggeBlochTransportedAllOrbit4D
  26open ReggeBlochTransportedAllOrbitM2Eval4D
  27open ReggeBlochM2Symbol4D
  28open Regge4DContinuumPreflight
  29open Regge4DTorusContinuumLimit
  30open EdgeTTDecomposition4D
  31
  32noncomputable section
  33
  34theorem m2PathB_meanLocal_axisTTPlus_symbolDir :
  35    m2MeanLocalAllOrbitMoment axisTTPlus symbolDir = (-1 / 4 : ℝ) := by
  36  rw [m2MeanLocalAllOrbitMoment_eq_distinctHinge,
  37    m2TransportedAllOrbitMomentDistinctHinge_axisTTPlus_symbolDir]
  38
  39theorem m2PathB_meanLocal_axisTTCross_symbolDir :
  40    m2MeanLocalAllOrbitMoment axisTTCross symbolDir = (-1 / 4 : ℝ) := by
  41  rw [m2MeanLocalAllOrbitMoment_eq_distinctHinge,
  42    m2TransportedAllOrbitMomentDistinctHinge_axisTTCross_symbolDir]
  43
  44theorem m2PathB_meanLocal_axisTTPlus_e0Dir :
  45    m2MeanLocalAllOrbitMoment axisTTPlus e0Dir = (0 : ℝ) := by
  46  rw [m2MeanLocalAllOrbitMoment_eq_distinctHinge,
  47    m2TransportedAllOrbitMomentDistinctHinge_axisTTPlus_e0Dir]
  48
  49theorem m2PathB_meanLocal_axisTTCross_e0Dir :
  50    m2MeanLocalAllOrbitMoment axisTTCross e0Dir = (-1 / 8 : ℝ) := by
  51  rw [m2MeanLocalAllOrbitMoment_eq_distinctHinge,
  52    m2TransportedAllOrbitMomentDistinctHinge_axisTTCross_e0Dir]
  53
  54theorem m2PathB_meanLocal_plus_cross_disagree_e0Dir :
  55    m2MeanLocalAllOrbitMoment axisTTPlus e0Dir ≠
  56      m2MeanLocalAllOrbitMoment axisTTCross e0Dir := by
  57  rw [m2PathB_meanLocal_axisTTPlus_e0Dir, m2PathB_meanLocal_axisTTCross_e0Dir]
  58  norm_num
  59
  60private lemma symbolDir_normSq :
  61    (∑ i : Fin 4, symbolDir i * symbolDir i) = (2 : ℝ) := by
  62  simp [symbolDir, Fin.sum_univ_four]; norm_num
  63
  64theorem continuumFace_meanLocal_normalizedPlus_symbolDir :
  65    m2MeanLocalAllOrbitMoment ((Real.sqrt 2)⁻¹ • axisTTPlus) symbolDir /
  66      (∑ i : Fin 4, symbolDir i * symbolDir i) =
  67      (-1 / 16 : ℝ) := by
  68  rw [m2MeanLocalAllOrbitMoment_smul,
  69    m2PathB_meanLocal_axisTTPlus_symbolDir, symbolDir_normSq,
  70    inv_pow, Real.sq_sqrt (by norm_num : (0 : ℝ) ≤ 2)]
  71  norm_num
  72
  73theorem meanLocal_pinned_face_ne_eh :
  74    m2MeanLocalAllOrbitMoment ((Real.sqrt 2)⁻¹ • axisTTPlus) symbolDir /
  75      (∑ i : Fin 4, symbolDir i * symbolDir i) ≠
  76      einsteinHilbertTTCoefficient4D := by
  77  rw [continuumFace_meanLocal_normalizedPlus_symbolDir,
  78    einsteinHilbertTTCoefficient4D_eq]
  79  norm_num
  80
  81theorem pathB_vs_distinctHinge_witness_table :
  82    m2MeanLocalAllOrbitMoment axisTTPlus symbolDir =
  83        m2TransportedAllOrbitMomentDistinctHinge axisTTPlus symbolDir ∧
  84      m2MeanLocalAllOrbitMoment axisTTCross symbolDir =
  85        m2TransportedAllOrbitMomentDistinctHinge axisTTCross symbolDir ∧
  86      m2MeanLocalAllOrbitMoment axisTTPlus e0Dir =
  87        m2TransportedAllOrbitMomentDistinctHinge axisTTPlus e0Dir ∧
  88      m2MeanLocalAllOrbitMoment axisTTCross e0Dir =
  89        m2TransportedAllOrbitMomentDistinctHinge axisTTCross e0Dir ∧
  90      m2MeanLocalAllOrbitMoment axisTTPlus symbolDir = (-1 / 4 : ℝ) ∧
  91      m2MeanLocalAllOrbitMoment axisTTCross symbolDir = (-1 / 4 : ℝ) ∧
  92      m2MeanLocalAllOrbitMoment axisTTPlus e0Dir = (0 : ℝ) ∧
  93      m2MeanLocalAllOrbitMoment axisTTCross e0Dir = (-1 / 8 : ℝ) := by
  94  refine ⟨?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_⟩
  95  · exact m2MeanLocalAllOrbitMoment_eq_distinctHinge _ _
  96  · exact m2MeanLocalAllOrbitMoment_eq_distinctHinge _ _
  97  · exact m2MeanLocalAllOrbitMoment_eq_distinctHinge _ _
  98  · exact m2MeanLocalAllOrbitMoment_eq_distinctHinge _ _
  99  · exact m2PathB_meanLocal_axisTTPlus_symbolDir
 100  · exact m2PathB_meanLocal_axisTTCross_symbolDir
 101  · exact m2PathB_meanLocal_axisTTPlus_e0Dir
 102  · exact m2PathB_meanLocal_axisTTCross_e0Dir
 103
 104/-- Position-resolved Path B does not close EH (status false / OPEN). -/
 105theorem pathB_positionResolved_does_not_close_eh :
 106    Regge4DPathBPositionResolvedClosesEH = False :=
 107  Regge4DPathBPositionResolvedClosesEH_status_open
 108
 109theorem pathB_does_not_inhabit_eh :
 110    regge4DTorusContinuumLimitStatus.ehTendstoInhabited = false :=
 111  rfl
 112
 113structure ReggeBlochLocalIncidenceM2Eval4DStatus where
 114  meanLocalEqualsDistinctHingeOnWitnesses : Bool
 115  e0AnisotropyPersistsUnderMeanLocal : Bool
 116  factor4ResidualPersistsUnderMeanLocal : Bool
 117  positionResolvedClosesEH : Bool
 118  gapActionRecovery : Bool
 119
 120def reggeBlochLocalIncidenceM2Eval4DStatus :
 121    ReggeBlochLocalIncidenceM2Eval4DStatus where
 122  meanLocalEqualsDistinctHingeOnWitnesses := true
 123  e0AnisotropyPersistsUnderMeanLocal := true
 124  factor4ResidualPersistsUnderMeanLocal := true
 125  positionResolvedClosesEH := false
 126  gapActionRecovery := false
 127
 128theorem reggeBlochLocalIncidenceM2Eval4DStatus_flags :
 129    reggeBlochLocalIncidenceM2Eval4DStatus.meanLocalEqualsDistinctHingeOnWitnesses =
 130        true ∧
 131      reggeBlochLocalIncidenceM2Eval4DStatus.e0AnisotropyPersistsUnderMeanLocal =
 132        true ∧
 133        reggeBlochLocalIncidenceM2Eval4DStatus.factor4ResidualPersistsUnderMeanLocal =
 134          true ∧
 135          reggeBlochLocalIncidenceM2Eval4DStatus.positionResolvedClosesEH =
 136            false ∧
 137            reggeBlochLocalIncidenceM2Eval4DStatus.gapActionRecovery =
 138              false := by
 139  decide
 140
 141theorem does_not_flip_gap_action_recovery :
 142    reggeBlochLocalIncidenceM2Eval4DStatus.gapActionRecovery = false :=
 143  rfl
 144
 145end
 146
 147end ReggeBlochLocalIncidenceM2Eval4D
 148end Analysis
 149end Gravity
 150end IndisputableMonolith
 151