IndisputableMonolith.Constants.AlphaGenesis.U1Normalization

   1import Mathlib
   2import IndisputableMonolith.Constants.Alpha
   3import IndisputableMonolith.Constants.AlphaDerivation
   4import IndisputableMonolith.Numerics.Interval.AlphaBounds
   5
   6/-!
   7# Alpha Genesis M11: U(1) coupling-normalization verdict (quarantine)
   8
   9This module records the result of the make-or-break test: can the α seed
  10`4π·11` be promoted from an IDENTIFICATION ("channel-budget bridge") to a
  11THEOREM about a U(1) coupling normalization on the cube `Q₃`?
  12
  13## The test
  14
  15`Foundation.GaugeFromCube` derives the U(1) *group* (the parity quotient
  16`ℤ/2` of `Aut(Q₃) = B₃`), but never touches the α pipeline. A genuine
  17coupling-normalization theorem would read the inverse coupling off a
  18gauge-invariant U(1) Maxwell action on the cube. The QED normalization is
  19`α = e²/(4π)`, i.e. `α⁻¹ = (4π)·(stiffness)/e²`; the seed reads
  20`stiffness = 11` (passive edges) and `e² = 1`.
  21
  22## The result (negative, sharp)
  23
  24A gauge-invariant U(1) action on the cube graph counts **independent plaquette
  25field strengths**, i.e. the cycle rank of the 1-skeleton:
  26`b₁ = E − V + 1 = 12 − 8 + 1 = 5` (equivalently `6` faces `− 1` Bianchi/closure
  27relation). Gauge fixing removes `V − 1 = 7` link redundancies (one U(1) phase
  28per vertex, minus the global phase), leaving `12 − 7 = 5` physical link modes,
  29the same `5`.
  30
  31The seed's `11 = E − 1` removes only the single *active* edge, NOT the `7` gauge
  32redundancies. So `11` is a **ledger recognition-channel count, not a
  33gauge-invariant photon stiffness** (which is `5`). The two disagree:
  34`11 ≠ 5` (`seed_channel_count_ne_gauge_dof`).
  35
  36Consequently a genuine gauge-invariant Maxwell seed on the cube is
  37`4π·5 = 20π ≈ 62.8`, which is excluded from being `α⁻¹` by a wide margin
  38(`gauge_invariant_seed_excluded`: `< 63 < 137.030 < alphaInv`).
  39
  40## Verdict
  41
  42The channel-budget reading of `α⁻¹ = 4π·11` does NOT promote to a U(1)
  43coupling-normalization theorem. The `11` is a ledger channel count, not the
  44gauge-invariant photon degree-of-freedom count (`5`). The seed remains a
  45striking, cross-consistent *ledger* number (the same `11` appears in
  46`Ω_Λ = 11/16`, CKM, `η_B = φ⁻⁴⁴`, and `44 = 4·11`), but its identity with the
  47electromagnetic coupling is an identification at the ledger level, not a derived
  48gauge normalization. The honest formal object is the CONDITIONAL
  49`SeedNormalizationReading` below, whose third premise is exactly the
  50ledger-vs-gauge mismatch.
  51
  52STATUS: THEOREM (the combinatorial verdict); QUARANTINE (imports CODATA band
  53only through `alphaInv` numeric bounds).
  54-/
  55
  56namespace IndisputableMonolith
  57namespace Constants
  58namespace AlphaGenesis
  59namespace U1Normalization
  60
  61open Constants.AlphaDerivation
  62
  63/-! ## Gauge-invariant photon degree-of-freedom count on the cube -/
  64
  65/-- Independent plaquette field strengths of a U(1) gauge field on the cube
  66graph = the cycle rank (first Betti number) of the 1-skeleton, `b₁ = E − V + 1`.
  67For `Q₃`: `12 − 8 + 1 = 5`. -/
  68def cube_cycle_rank : ℕ := cube_edges D - cube_vertices D + 1
  69
  70theorem cube_cycle_rank_eq_5 : cube_cycle_rank = 5 := by
  71  unfold cube_cycle_rank; native_decide
  72
  73/-- The same count via faces minus the single global Bianchi/closure relation
  74(`∏_faces F = 1`): `6 − 1 = 5`. -/
  75theorem gauge_dof_via_faces : cube_faces D - 1 = cube_cycle_rank := by
  76  rw [cube_cycle_rank_eq_5]; native_decide
  77
  78/-- The U(1) gauge redundancy on the 12 link variables: one phase per vertex,
  79minus the global phase that acts trivially, `V − 1 = 7`. -/
  80def gauge_redundancy : ℕ := cube_vertices D - 1
  81
  82theorem gauge_redundancy_eq_7 : gauge_redundancy = 7 := by
  83  unfold gauge_redundancy; native_decide
  84
  85/-- Physical link modes = link variables − gauge redundancy = `E − (V − 1)`,
  86which equals the cycle rank: `12 − 7 = 5`. The two routes to the
  87gauge-invariant photon count agree. -/
  88theorem physical_link_dof_eq_cycle_rank :
  89    cube_edges D - gauge_redundancy = cube_cycle_rank := by
  90  rw [gauge_redundancy_eq_7, cube_cycle_rank_eq_5]; native_decide
  91
  92/-! ## The seed channel count is the ledger count, not the gauge count -/
  93
  94/-- The α seed channel count is the passive-edge count `E − 1 = 11`. This removes
  95only the single active edge, not the `V − 1 = 7` gauge redundancies. -/
  96theorem seed_channel_count : passive_field_edges D = 11 := passive_edges_at_D3
  97
  98/-- **VERDICT (combinatorial core).** The seed channel count `11` is NOT the
  99gauge-invariant photon degree-of-freedom count `5`. A gauge-invariant Maxwell
 100normalization on the cube would use the cycle rank, not the passive-edge count. -/
 101theorem seed_channel_count_ne_gauge_dof :
 102    passive_field_edges D ≠ cube_cycle_rank := by
 103  rw [seed_channel_count, cube_cycle_rank_eq_5]; norm_num
 104
 105/-! ## The gauge-invariant seed cannot be `α⁻¹` -/
 106
 107/-- The gauge-invariant Maxwell seed on the cube: `(4π) × (cycle rank)`. -/
 108noncomputable def gauge_invariant_seed : ℝ := 4 * Real.pi * (cube_cycle_rank : ℝ)
 109
 110theorem gauge_invariant_seed_eq_20pi : gauge_invariant_seed = 20 * Real.pi := by
 111  unfold gauge_invariant_seed
 112  rw [cube_cycle_rank_eq_5]
 113  push_cast
 114  ring
 115
 116/-- The gauge-invariant seed `20π ≈ 62.8` is excluded from being `α⁻¹` by a wide
 117margin: `gauge_invariant_seed < 63 < 137.030 < alphaInv`. So the genuine
 118gauge-invariant U(1) normalization on the cube cannot be the source of the
 119electromagnetic coupling; the seed's `137`-scale value requires the ledger
 120channel count `11`, not the gauge count `5`. -/
 121theorem gauge_invariant_seed_excluded :
 122    gauge_invariant_seed < Constants.alphaInv := by
 123  rw [gauge_invariant_seed_eq_20pi]
 124  have hpi : Real.pi < (3.141593 : ℝ) := Real.pi_lt_d6
 125  have h1 : (20 : ℝ) * Real.pi < 63 := by nlinarith [hpi]
 126  have h2 : (137.030 : ℝ) < Constants.alphaInv := Numerics.alphaInv_gt
 127  linarith
 128
 129/-! ## The honest conditional reading -/
 130
 131/-- A reading of the α seed `4π·11` as a U(1) coupling normalization. The seed
 132equals `(4π) × (stiffness)` with `e² = 1` ONLY under three inputs, the third of
 133which is precisely the ledger-vs-gauge mismatch: the stiffness used is the
 134passive-edge (ledger channel) count, which is NOT the gauge-invariant cycle
 135rank. So this is an identification, not a gauge-theory theorem. -/
 136structure SeedNormalizationReading : Prop where
 137  /-- (i) MODEL: Heaviside–Lorentz convention `α = e²/(4π)`. -/
 138  hl_convention : True
 139  /-- (ii) IDENTIFICATION: bare charge quantum `e² = 1` (J-cost Hessian `= 1`;
 140  the particle/antiparticle double-entry factor of `2` is not independently
 141  ruled out here). -/
 142  charge_unit_one : True
 143  /-- (iii) IDENTIFICATION (the load-bearing one): the photon stiffness is taken
 144  to be the passive-edge ledger channel count `11`, which is NOT the
 145  gauge-invariant cycle rank `5`. -/
 146  stiffness_is_ledger_not_gauge : passive_field_edges D ≠ cube_cycle_rank
 147
 148/-- The honest reading is inhabited, and its load-bearing premise is the proved
 149ledger-vs-gauge mismatch. This certifies the reading as an identification (it
 150holds), not a derivation (the gauge count would give `5`, not `11`). -/
 151def seedNormalizationReading : SeedNormalizationReading where
 152  hl_convention := trivial
 153  charge_unit_one := trivial
 154  stiffness_is_ledger_not_gauge := seed_channel_count_ne_gauge_dof
 155
 156/-- **U(1) normalization verdict certificate.** Bundles the make-or-break result:
 157the gauge-invariant photon count on the cube is `5` (two independent routes
 158agree), the seed uses the ledger channel count `11 ≠ 5`, and the genuine
 159gauge-invariant seed `20π` is excluded from `α⁻¹`. The channel-budget reading is
 160therefore an identification at the ledger level, not a derived U(1) coupling
 161normalization. -/
 162structure U1NormalizationVerdict : Prop where
 163  gauge_dof_is_5 : cube_cycle_rank = 5
 164  gauge_dof_two_routes_agree : cube_edges D - gauge_redundancy = cube_cycle_rank
 165  seed_uses_ledger_count : passive_field_edges D = 11
 166  ledger_ne_gauge : passive_field_edges D ≠ cube_cycle_rank
 167  gauge_seed_excluded : gauge_invariant_seed < Constants.alphaInv
 168
 169def u1NormalizationVerdict : U1NormalizationVerdict where
 170  gauge_dof_is_5 := cube_cycle_rank_eq_5
 171  gauge_dof_two_routes_agree := physical_link_dof_eq_cycle_rank
 172  seed_uses_ledger_count := seed_channel_count
 173  ledger_ne_gauge := seed_channel_count_ne_gauge_dof
 174  gauge_seed_excluded := gauge_invariant_seed_excluded
 175
 176end U1Normalization
 177end AlphaGenesis
 178end Constants
 179end IndisputableMonolith
 180