IndisputableMonolith.Gravity.Analysis.ReggeNormalizationDerived4D

   1import Mathlib
   2import IndisputableMonolith.Gravity.Analysis.ContinuumTTSecondVariation4D
   3import IndisputableMonolith.Gravity.Analysis.ReggeExactMidpointM2TTIdentity4D
   4
   5/-!
   6# Regge's normalization constant, derived and then measured by the dictionary
   7
   8Arc 2, step 7, second half.  `ContinuumTTSecondVariation4D` derived, from the
   9Levi-Civita connection alone and with no access to anything on the Regge side,
  10that the phase average of `d²/dt² ∫ R √g` per unit volume on a real
  11transverse-traceless cosine wave is
  12
  13  `ehFace H k = -(1/4) · |k|² · ‖H‖²_F`.
  14
  15This module puts that beside the banked dictionary value and asks what constant
  16relates them.
  17
  18## A4, the fourth classical input
  19
  20The discrete object is the **Regge action** `Σ_h A_h δ_h`, area times deficit
  21(the generator's own header: `S'' = Σ_h (dA_h)(dδ_h)`).  That is not
  22`∫ R √g`; Regge's normalization is
  23
  24  `Σ_h A_h δ_h = ρ · ∫ R √g`,  with  `ρ = 1/2`.
  25
  26This module does **not** assume `ρ`.  It leaves it free, shows the dictionary
  27forces `ρ = 1/2` (§4), refutes `ρ = 1` which is what the frozen preflight
  28implicitly used (§5), and checks `ρ = 1/2` independently against Gauss-Bonnet on
  29two triangulated spheres (§6).
  30
  31## The result
  32
  33The factor of two between the computed `-(1/8)` and the frozen `-(1/4)` is
  34Regge's normalization constant.  Both numbers are correct; they are faces of two
  35different actions.  `discreteBookkeepingFactor := 2` is `1/ρ`, and it is
  36derivable, so the historical gate did not fail because the Regge computation was
  37wrong.  It failed because the two sides were varying different functionals.
  38
  39Expected axiom footprint: `[propext, Classical.choice, Quot.sound]`.
  40-/
  41
  42namespace IndisputableMonolith
  43namespace Gravity
  44namespace Analysis
  45namespace ReggeNormalizationDerived4D
  46
  47open BigOperators
  48open EdgeTTDecomposition4D
  49  (Mat4 IsTT momentumSq axisWave axisTTPlus axisTTPlus_isTT)
  50open ReggeExactFlatHessianBlochSymbol4D (exactMidpointBlochM2)
  51open ReggeExactMidpointM2TTIdentity4D
  52  (frobeniusNormSq waveNormSq exactMidpointBlochM2_eq_neg_eighth_frobenius_tt)
  53open ContinuumTTSecondVariation4D
  54  (ehFace frobSq phaseAverage densityOfPhase phaseAverage_const_mul phaseAverage_cos_sq)
  55
  56noncomputable section
  57
  58abbrev Wave4 := Fin 4 → ℝ
  59
  60/-! ## §1. The two sides use the same two scalars -/
  61
  62theorem frobSq_eq (H : Mat4) : frobSq H = frobeniusNormSq H := rfl
  63
  64theorem momentumSq_eq (k : Wave4) : momentumSq k = waveNormSq k := rfl
  65
  66/-! ## §2. A4 with the constant left free -/
  67
  68/-- **A4, unfixed.**  If `Σ_h A_h δ_h = ρ · ∫ R √g`, then the continuum face the
  69discrete Regge Hessian must be compared against is `ρ` times the derived
  70Einstein-Hilbert face.  `ρ` is a free real here and is pinned in §4. -/
  71def reggeFace (ρ : ℝ) (H : Mat4) (k : Wave4) : ℝ := ρ * ehFace H k
  72
  73/-- Regge's normalization constant, `Σ_h A_h δ_h = (1/2) ∫ R √g`.  Checked
  74independently in §6. -/
  75def reggeNormalization : ℝ := 1 / 2
  76
  77theorem reggeFace_eq (ρ : ℝ) (H : Mat4) (k : Wave4) :
  78    reggeFace ρ H k = -(ρ / 4) * frobeniusNormSq H * waveNormSq k := by
  79  unfold reggeFace ehFace
  80  rw [frobSq_eq, momentumSq_eq]
  81  ring
  82
  83/-! ## §3. P2: the match -/
  84
  85/-- **P2.**  At Regge's normalization the derived continuum face equals the
  86banked dictionary m² moment exactly, for every transverse-traceless `H` at every
  87momentum `k`.  No residual factor, and no tolerance: both sides are exact. -/
  88theorem reggeFace_eq_dictionary (H : Mat4) (k : Wave4) (hTT : IsTT k H) :
  89    reggeFace reggeNormalization H k = exactMidpointBlochM2 H k := by
  90  rw [exactMidpointBlochM2_eq_neg_eighth_frobenius_tt H k hTT, reggeFace_eq]
  91  unfold reggeNormalization
  92  ring
  93
  94/-! ## §4. P3: the dictionary measures Regge's constant -/
  95
  96/-- **P3.**  The 1,208 rows, built from exact Heron areas and Gram dihedral
  97derivatives with no input from any continuum theorem, force `ρ = 1/2`.  This is a
  98check that could have failed. -/
  99theorem regge_normalization_pinned (H : Mat4) (k : Wave4) (hTT : IsTT k H) (ρ : ℝ)
 100    (hne : frobeniusNormSq H * waveNormSq k ≠ 0)
 101    (h : reggeFace ρ H k = exactMidpointBlochM2 H k) :
 102    ρ = 1 / 2 := by
 103  rw [exactMidpointBlochM2_eq_neg_eighth_frobenius_tt H k hTT, reggeFace_eq] at h
 104  have hc : (ρ / 4 - 1 / 8) * (frobeniusNormSq H * waveNormSq k) = 0 := by
 105    linear_combination -h
 106  rcases mul_eq_zero.mp hc with h1 | h2
 107  · linarith
 108  · exact absurd h2 hne
 109
 110/-! ## §5. Discrimination: the instrument fires, and the wrong constants fail -/
 111
 112theorem frobeniusNormSq_axisTTPlus : frobeniusNormSq axisTTPlus = 2 := by
 113  norm_num [frobeniusNormSq, Fin.sum_univ_four, axisTTPlus]
 114
 115theorem waveNormSq_axisWave : waveNormSq axisWave = 1 := by
 116  norm_num [waveNormSq, Fin.sum_univ_four, axisWave]
 117
 118theorem witness_nonzero : frobeniusNormSq axisTTPlus * waveNormSq axisWave ≠ 0 := by
 119  rw [frobeniusNormSq_axisTTPlus, waveNormSq_axisWave]
 120  norm_num
 121
 122/-- **Discrimination 4.**  The witness carries a nonzero value, so the agreement
 123of §3 is not two zeros meeting. -/
 124theorem dictionary_witness_value :
 125    exactMidpointBlochM2 axisTTPlus axisWave = -(1 / 4) := by
 126  rw [exactMidpointBlochM2_eq_neg_eighth_frobenius_tt axisTTPlus axisWave axisTTPlus_isTT,
 127    frobeniusNormSq_axisTTPlus, waveNormSq_axisWave]
 128  norm_num
 129
 130/-- **Discrimination 2.**  `ρ = 1`, which is what comparing the discrete Regge
 131action against `∫ R √g` assumes, and what the frozen preflight did, is refuted at
 132the witness. -/
 133theorem rho_one_fails :
 134    reggeFace 1 axisTTPlus axisWave ≠ exactMidpointBlochM2 axisTTPlus axisWave := by
 135  rw [reggeFace_eq, dictionary_witness_value, frobeniusNormSq_axisTTPlus,
 136    waveNormSq_axisWave]
 137  norm_num
 138
 139/-- **Discrimination 3.**  Every `ρ ≠ 1/2` is refuted, so the constant is pinned
 140and not merely consistent. -/
 141theorem rho_pinned_at_witness (ρ : ℝ)
 142    (h : reggeFace ρ axisTTPlus axisWave = exactMidpointBlochM2 axisTTPlus axisWave) :
 143    ρ = 1 / 2 :=
 144  regge_normalization_pinned axisTTPlus axisWave axisTTPlus_isTT ρ witness_nonzero h
 145
 146/-! ## §6. A4 checked independently, in two dimensions
 147
 148A hinge in two dimensions is a vertex and its `(d-2)`-volume is `1`, so the Regge
 149action is the plain deficit sum `Σ_v δ_v`.  Gauss-Bonnet gives `∫ K √g = 2πχ`,
 150and `R = 2K` in two dimensions, so `∫ R √g = 4πχ`.  Regge's constant is therefore
 151`2πχ / 4πχ = 1/2` on every closed surface, independent of topology.  Checked on
 152two triangulations of the sphere with different vertex counts and different
 153vertex degrees; a wrong constant fails both. -/
 154
 155/-- Tetrahedron: four vertices, each meeting three equilateral triangles. -/
 156theorem tetrahedron_deficit_sum :
 157    (4 : ℝ) * (2 * Real.pi - 3 * (Real.pi / 3)) = 4 * Real.pi := by ring
 158
 159/-- Octahedron: six vertices, each meeting four equilateral triangles. -/
 160theorem octahedron_deficit_sum :
 161    (6 : ℝ) * (2 * Real.pi - 4 * (Real.pi / 3)) = 4 * Real.pi := by ring
 162
 163/-- `∫ R √g` on the sphere: Gauss-Bonnet gives `∫K√g = 2πχ = 4π`, and `R = 2K`. -/
 164def sphereEHIntegral : ℝ := 2 * (2 * Real.pi * 2)
 165
 166/-- Both polyhedra give a deficit sum of `4π`, and `4π = (1/2) · 8π`. -/
 167theorem regge_constant_from_gauss_bonnet :
 168    (4 : ℝ) * Real.pi = reggeNormalization * sphereEHIntegral := by
 169  unfold reggeNormalization sphereEHIntegral
 170  ring
 171
 172/-- The same check refutes `ρ = 1`: it would demand a deficit sum of `8π`, and
 173both polyhedra give `4π`. -/
 174theorem gauss_bonnet_refutes_rho_one :
 175    (4 : ℝ) * Real.pi ≠ 1 * sphereEHIntegral := by
 176  unfold sphereEHIntegral
 177  intro h
 178  have hpi : (0 : ℝ) < Real.pi := Real.pi_pos
 179  linarith
 180
 181/-! ## §7. A second route to the same continuum face
 182
 183The `-h·G⁽¹⁾` density of `ContinuumTTSecondVariation4D` §5 is one textbook form.
 184The other is the quadratic Lagrangian `-(1/4) ∂_λ h_{μν} ∂^λ h^{μν}`, whose
 185second derivative along `t h` is `-(1/2) ∂h·∂h`, giving a density in `sin²`
 186rather than `cos²`.  The two densities differ pointwise, because they differ by a
 187total derivative, and agree on average.  Agreement of two independent textbook
 188forms is a check on A3's normalization. -/
 189
 190theorem phaseAverage_sin_sq : phaseAverage (fun θ => Real.sin θ ^ 2) = 1 / 2 := by
 191  have hpi : Real.pi ≠ 0 := Real.pi_ne_zero
 192  unfold phaseAverage
 193  rw [integral_sin_sq, Real.sin_two_pi, Real.sin_zero]
 194  field_simp
 195  ring
 196
 197/-- Density of the quadratic-Lagrangian route, as a function of the phase. -/
 198def lagrangianDensityOfPhase (H : Mat4) (k : Wave4) (θ : ℝ) : ℝ :=
 199  -((1 / 2 : ℝ) * waveNormSq k * frobeniusNormSq H) * Real.sin θ ^ 2
 200
 201theorem lagrangian_route_same_face (H : Mat4) (k : Wave4) :
 202    phaseAverage (lagrangianDensityOfPhase H k) = ehFace H k := by
 203  unfold lagrangianDensityOfPhase ehFace
 204  rw [phaseAverage_const_mul, phaseAverage_sin_sq, frobSq_eq, momentumSq_eq]
 205  ring
 206
 207/-- The two routes really are different densities: at zero phase one vanishes and
 208the other does not.  They agree only after averaging, which is what makes their
 209agreement informative. -/
 210theorem two_routes_differ_pointwise (H : Mat4) (k : Wave4)
 211    (hne : waveNormSq k * frobeniusNormSq H ≠ 0) :
 212    lagrangianDensityOfPhase H k 0 ≠ densityOfPhase H k 0 := by
 213  have hl : lagrangianDensityOfPhase H k 0 = 0 := by
 214    unfold lagrangianDensityOfPhase
 215    rw [Real.sin_zero]
 216    ring
 217  have hd : densityOfPhase H k 0
 218      = -((1 / 2 : ℝ) * (waveNormSq k * frobeniusNormSq H)) := by
 219    unfold densityOfPhase
 220    rw [frobSq_eq, momentumSq_eq, Real.cos_zero]
 221    ring
 222  rw [hl, hd]
 223  intro h
 224  exact hne (by linarith)
 225
 226/-! ## §8. P4: what the tree's constants actually are -/
 227
 228/-- **P4.**  `discreteBookkeepingFactor = 2` is `1/ρ`, Regge's normalization
 229constant inverted.  It is not bookkeeping and it is not a fudge; it is derivable,
 230and §6 derives it. -/
 231theorem discreteBookkeepingFactor_is_inverse_regge :
 232    ReggeExactFlatHessianNormGate4D.discreteBookkeepingFactor * reggeNormalization = 1 := by
 233  unfold reggeNormalization
 234  rw [ReggeExactFlatHessianNormGate4D.discreteBookkeepingFactor_eq_two]
 235  norm_num
 236
 237/-- **The frozen preflight coefficient was never a wrong number.**  It is exactly
 238the derived Einstein-Hilbert face, per unit Frobenius and per unit momentum.  It
 239is the right face for `∫ R √g` and the wrong face for `Σ_h A_h δ_h`, which is
 240what the dictionary tabulates. -/
 241theorem frozen_preflight_is_the_eh_integral_face (H : Mat4) (k : Wave4) :
 242    ehFace H k
 243      = ReggeExactFlatHessianNormGate4D.frozenPreflightEHCoefficient
 244          * frobeniusNormSq H * waveNormSq k := by
 245  unfold ehFace ReggeExactFlatHessianNormGate4D.frozenPreflightEHCoefficient
 246    ReggeExactFlatHessianSymbol4D.einsteinHilbertTTCoefficient4D
 247  rw [frobSq_eq, momentumSq_eq]
 248  ring
 249
 250/-- And the banked `-(1/8)` is exactly the face of the discrete action.  Both
 251constants in the tree are correct faces of different functionals. -/
 252theorem exact_unit_coefficient_is_the_regge_face (H : Mat4) (k : Wave4) :
 253    reggeFace reggeNormalization H k
 254      = ReggeExactFlatHessianNormGate4D.exactUnitFrobeniusTTCoefficient
 255          * frobeniusNormSq H * waveNormSq k := by
 256  unfold reggeFace reggeNormalization ehFace
 257    ReggeExactFlatHessianNormGate4D.exactUnitFrobeniusTTCoefficient
 258    ReggeExactFlatHessianSymbol4D.exactHessianM2UnitFrobeniusTTCoeff
 259  rw [frobSq_eq, momentumSq_eq]
 260  ring
 261
 262/-! ## §9. A gate that can fail
 263
 264`ReggeExactFlatHessianNormGate4D.NormalizationGatePass` is the Bool literal
 265`true`, so it reports success no matter what any coefficient in the tree is; it
 266cannot discriminate.  The proposition below is its discriminating replacement:
 267each conjunct is an equation or a refutation over the actual constants, and
 268changing any coefficient in the tree breaks one of them. -/
 269
 270def NormalizationGateDischarged : Prop :=
 271  (∀ H : Mat4, ∀ k : Wave4, IsTT k H →
 272      reggeFace reggeNormalization H k = exactMidpointBlochM2 H k)
 273    ∧ (∀ ρ : ℝ, reggeFace ρ axisTTPlus axisWave
 274        = exactMidpointBlochM2 axisTTPlus axisWave → ρ = 1 / 2)
 275    ∧ reggeFace 1 axisTTPlus axisWave ≠ exactMidpointBlochM2 axisTTPlus axisWave
 276    ∧ exactMidpointBlochM2 axisTTPlus axisWave = -(1 / 4)
 277    ∧ (4 : ℝ) * Real.pi = reggeNormalization * sphereEHIntegral
 278    ∧ (4 : ℝ) * Real.pi ≠ 1 * sphereEHIntegral
 279
 280theorem normalizationGateDischarged : NormalizationGateDischarged :=
 281  ⟨fun H k hTT => reggeFace_eq_dictionary H k hTT,
 282   rho_pinned_at_witness,
 283   rho_one_fails,
 284   dictionary_witness_value,
 285   regge_constant_from_gauss_bonnet,
 286   gauss_bonnet_refutes_rho_one⟩
 287
 288/-- Everything step 7 claims, in one proposition. -/
 289def Step7Cert : Prop :=
 290  NormalizationGateDischarged
 291    ∧ (∀ H : Mat4, ∀ k : Wave4, phaseAverage (lagrangianDensityOfPhase H k) = ehFace H k)
 292    ∧ ReggeExactFlatHessianNormGate4D.discreteBookkeepingFactor * reggeNormalization = 1
 293    ∧ (∀ H : Mat4, ∀ k : Wave4, ehFace H k
 294        = ReggeExactFlatHessianNormGate4D.frozenPreflightEHCoefficient
 295            * frobeniusNormSq H * waveNormSq k)
 296    ∧ (4 : ℝ) * (2 * Real.pi - 3 * (Real.pi / 3)) = 4 * Real.pi
 297    ∧ (6 : ℝ) * (2 * Real.pi - 4 * (Real.pi / 3)) = 4 * Real.pi
 298
 299theorem step7Cert : Step7Cert :=
 300  ⟨normalizationGateDischarged,
 301   lagrangian_route_same_face,
 302   discreteBookkeepingFactor_is_inverse_regge,
 303   frozen_preflight_is_the_eh_integral_face,
 304   tetrahedron_deficit_sum,
 305   octahedron_deficit_sum⟩
 306
 307/-! ## §10. Status strings -/
 308
 309/-- What is now derived, and what remains assumed. -/
 310def typedResidual_arc2_normalization : String :=
 311  "CLOSED: arc 2's factor of two is Regge's normalization constant, Σ_h A_h δ_h = (1/2)∫R√g. \
 312The continuum face is DERIVED in ContinuumTTSecondVariation4D from the Levi-Civita \
 313connection with no access to the Regge side; the dictionary then PINS ρ = 1/2 on the whole \
 314TT space at every momentum, and ρ = 1 is refuted at the witness. ρ = 1/2 is separately \
 315checked against Gauss-Bonnet on two triangulated spheres. REMAINING ASSUMPTION: A3, that \
 316d²/dt² ∫√gR = -∫ h·G⁽¹⁾, cross-checked here against the quadratic-Lagrangian route. \
 317NOT CLOSED BY THIS: the geometric mesh Tendsto that S_RS_converges_EH_4d needs; this \
 318settles the coefficient, not the convergence."
 319
 320/-- The naming defect this step exposes, recorded rather than silently renamed. -/
 321def typedResidual_naming_defect : String :=
 322  "NAMING: ReggeExactFlatHessianNormGate4D.continuumEHDiscreteFace computes \
 323discreteBookkeepingFactor * exactUnitFrobeniusTTCoefficient * frobeniusSq = -(1/4)·F, which \
 324is the face of ∫R√g and NOT the face of the discrete Regge action, whose face is -(1/8)·F. \
 325The name says the opposite of what the function returns. Left in place because downstream \
 326modules depend on it; readers should use ReggeNormalizationDerived4D.reggeFace instead. \
 327Likewise NormalizationGatePass is the Bool literal true and cannot fail; its discriminating \
 328replacement is NormalizationGateDischarged in §9."
 329
 330end
 331
 332end ReggeNormalizationDerived4D
 333end Analysis
 334end Gravity
 335end IndisputableMonolith
 336