IndisputableMonolith.Cosmology.BaryonAsymmetryDerivation

   1import Mathlib
   2import IndisputableMonolith.Constants
   3import IndisputableMonolith.Foundation.GrayCodeChirality
   4import IndisputableMonolith.Foundation.ParticleGenerations
   5import IndisputableMonolith.StandardModel.CKMFromCube
   6import IndisputableMonolith.StandardModel.JarlskogInvariant
   7import IndisputableMonolith.Cosmology.SakharovFromLedger
   8
   9/-!
  10# Baryon Asymmetry η_B: Structural Scaffold + φ-Rung Hypothesis
  11
  12STATUS TAGS (honest split, per the 2026-06-25 external review):
  13
  14- **THEOREM (structural)**: η_B > 0 follows from J_CP > 0 (Jarlskog from
  15  Gray-code chirality) plus the Sakharov conditions. The SIGN of the
  16  asymmetry (matter exists) is the derived content of this module.
  17- **SCAFFOLD (does NOT match the observed number)**: `eta_B_structural :=
  18  J_CP / g_★` is the textbook proportionality skeleton. Numerically it is
  19  ≈ 3×10⁻⁵ / 106.75 ≈ 3×10⁻⁷, i.e. roughly 500× LARGER than the observed
  20  6.1×10⁻¹⁰. Only positivity and smallness (< 1) are proved. It is not the
  21  prediction, and no theorem here claims it is. The missing physics is the
  22  order-parameter dynamics through the transition (Boltzmann transport,
  23  washout), which is OPEN.
  24- **HYPOTHESIS (empirical rung match)**: the Planck-matched expression is
  25  η_B = φ⁻⁴⁴·(1−φ⁻⁸)² (see EtaBPrefactorDerivation / EtaBIntervalCert).
  26  Note it contains NO g_★ and no Γ_sph/H: the structural scaffold above and
  27  the rung match are two different objects, and this module does not
  28  pretend they are connected. Falsifier: a tightened CMB measurement of
  29  η_B outside the φ⁻⁴⁴·(1−φ⁻⁸)² band.
  30
  31## The Observable
  32
  33The baryon-to-photon ratio:
  34  η_B = n_B / n_γ ≈ 6.1 × 10⁻¹⁰
  35
  36Measured from:
  37- Big Bang Nucleosynthesis (BBN): η_B = (6.1 ± 0.3) × 10⁻¹⁰
  38- CMB (Planck 2018): η_B = (6.12 ± 0.04) × 10⁻¹⁰
  39
  40## The Structural Formula (scaffold)
  41
  42In electroweak baryogenesis, the baryon asymmetry has the shape:
  43
  44  η_B ∝ (ε_CP / g_★) × (washout factor)
  45
  46where:
  47- ε_CP ∝ J_CP (CP asymmetry, from JarlskogInvariant — RS-derived)
  48- g_★ = relativistic DOF at T_EW (SM bookkeeping with RS-sourced gauge
  49  group + generation count; see StandardModel.RelativisticDOF for the
  50  derived-vs-imported split — NOT "all forced by Q₃")
  51- the washout factor requires transport dynamics (OPEN; see
  52  EWPhaseTransition for the positive-definite Γ_sph/H scaffold)
  53
  54## The φ-rung hypothesis
  55
  56  η_B ≈ φ⁻⁴⁴ ≈ 6.38 × 10⁻¹⁰ (within ~4.5% of Planck before the prefactor;
  57  φ⁻⁴⁴·(1−φ⁻⁸)² lands within the Planck band).
  58
  59Note φ⁻⁴⁵ ≈ 3.9×10⁻¹⁰ is the Θ_crit reciprocal; the rung used for η_B is
  60−44 = 1 − 45, i.e. η_B ≈ φ/Θ_crit. Earlier drafts quoted φ⁻⁴⁵ for η_B
  61itself; that was a REAL inconsistency and −44 is the operative rung.
  62
  63## Main Results
  64
  651. `eta_B_structural`: structural formula (scaffold; wrong magnitude, see tag)
  662. `eta_B_positive`: η_B > 0 (matter dominates) — the derived sign
  673. `eta_B_rung` + `saturation_exponent`: the −44 = 1 − 45 rung arithmetic
  684. `BaryonAsymmetryCert`: master certificate
  69-/
  70
  71namespace IndisputableMonolith
  72namespace Cosmology
  73namespace BaryonAsymmetryDerivation
  74
  75open Constants
  76open Foundation.ParticleGenerations
  77open Foundation.GrayCodeChirality
  78open StandardModel.CKMFromCube
  79open StandardModel.JarlskogInvariant
  80open SakharovFromLedger
  81
  82/-! ## Part 1: The Particle Content
  83
  84The effective number of relativistic degrees of freedom at the EW scale
  85uses the SM particle content. Provenance (see StandardModel.RelativisticDOF
  86for the full split): the gauge GROUP and generation COUNT are RS-derived;
  87the matter representations, minimal-neutrino convention, and the 7/8
  88thermal integral are imported standard physics. The single number 106.75
  89is the high-temperature value; the temperature dependence g_★(T) is
  90implemented in Cosmology.GStarThresholds. -/
  91
  92/-- The SM relativistic DOF at T > T_EW: g_★ = 106.75.
  93    Standard high-temperature SM bookkeeping (bosons 28, fermions 90 with
  94    the 7/8 thermal weight; minimal-neutrino convention). Imported SM
  95    content with RS-sourced gauge group and generation count — NOT an
  96    independent RS prediction of a new number. Machine-checked assembly in
  97    StandardModel.RelativisticDOF (g_star_derived_eq); temperature-dependent
  98    version in Cosmology.GStarThresholds (g_star 200 = 427/4). -/
  99noncomputable def g_star : ℝ := 106.75
 100
 101/-- The number of generations enters the DOF count. -/
 102theorem dof_includes_three_gen : face_pairs 3 = 3 := rfl
 103
 104/-! ## Part 2: The Sphaleron Rate
 105
 106Sphalerons are nonperturbative gauge field configurations that violate B+L;
 107their rate at T > T_EW scales as Γ_sph/V ∝ κ·α_W⁵·T⁴. The dimensionless
 108rate and its positivity are formalized in Cosmology.SphaleronRate
 109(`sphaleron_rate_dimensionless`, `kappa_sph`), and the Γ_sph/H ratio
 110scaffold in Cosmology.EWPhaseTransition. A previous version of this module
 111carried a `sphaleron_rate_structure : Prop := True` placeholder here; it
 112was vacuous and has been removed (the review was right to flag it). -/
 113
 114/-! ## Part 3: The η_B Structural Formula (SCAFFOLD)
 115
 116Combining the shape of the ingredients:
 117
 118  η_B = c × J_CP / g_★
 119
 120where c is a dimensionless constant that requires the detailed EW phase
 121transition dynamics (OPEN — not computed anywhere in this repository).
 122
 123HONEST NUMERICS: with the repository's own J_CP ≈ 3×10⁻⁵ and g_★ = 106.75,
 124this structural value is ≈ 3×10⁻⁷ — roughly 500× larger than the observed
 1256.1×10⁻¹⁰. So `eta_B_structural` is NOT the prediction and is not used as
 126one; the theorems below prove only its SIGN (positive: matter exists,
 127inherited from J_CP > 0) and that it is < 1. The Planck-matched expression
 128φ⁻⁴⁴·(1−φ⁻⁸)² is a separate object (see module header). -/
 129
 130/-- The structural η_B: proportional to J_CP / g_★.
 131    SCAFFOLD ONLY — numerically ≈ 3×10⁻⁷, about 500× the observed value,
 132    because the order-one-suppressed washout constant c is not derived.
 133    Used solely for the sign theorem (η_B > 0) and the smallness bound. -/
 134noncomputable def eta_B_structural : ℝ := jarlskog_structural / g_star
 135
 136/-- η_B is positive: matter dominates over antimatter.
 137    This follows directly from J_CP > 0 and is the genuine derived content
 138    (the SIGN of the asymmetry, not its magnitude). -/
 139theorem eta_B_positive : eta_B_structural > 0 := by
 140  unfold eta_B_structural
 141  apply div_pos jarlskog_positive
 142  norm_num [g_star]
 143
 144/-- η_B is small: the structural value is below 1.
 145    (A weak bound; the honest magnitude statement is in the module header.) -/
 146theorem eta_B_small : eta_B_structural < 1 := by
 147  unfold eta_B_structural
 148  rw [div_lt_one (by norm_num [g_star] : (0:ℝ) < g_star)]
 149  linarith [(cp_small_but_nonzero).2, show g_star = 106.75 from rfl]
 150
 151/-! ## Part 4: The φ-Ladder Connection (HYPOTHESIS)
 152
 153The observed η_B ≈ 6.1 × 10⁻¹⁰ is close to φ⁻⁴⁴ ≈ 6.376 × 10⁻¹⁰ (within
 154~4.5%; the prefactor (1−φ⁻⁸)² moves it into the Planck band — see
 155EtaBIntervalCert). This is an empirical rung match with a named falsifier,
 156not a theorem.
 157
 158On the integer 44: it can be written as 4 × 11 (Gray-code flip count ×
 159torsion gap), as 45 − 1 (dimension gap D²(D+2) minus one), or as g_f/2 − 1
 160(half the fermionic DOF minus one). These are re-expressions of the SAME
 161integer, not independent derivations, and none of them is a mechanism that
 162forces the rung. The honest status: −44 is a HYPOTHESIS-grade rung
 163assignment whose support is the numerical match itself. The α⁻¹ seed 44π
 164uses the same integer; that is a shared numerological observation, not
 165independent evidence (see soul.mdc: the 44π seed is itself an
 166identification, not a derived coupling). -/
 167
 168/-- The φ-rung exponent for the baryon asymmetry scale.
 169    φ⁴⁴ ≈ 1.568 × 10⁹, so φ⁻⁴⁴ ≈ 6.376 × 10⁻¹⁰.
 170    The observed η_B ≈ 6.1 × 10⁻¹⁰ is within ~4.5% (before the
 171    (1−φ⁻⁸)² prefactor). HYPOTHESIS-grade rung assignment. -/
 172def eta_B_rung : ℤ := -44
 173
 174/-- The complementary φ-exponent 45 (the saturation threshold Θ_crit = φ⁴⁵
 175    in the full `reality` repository's extended framework; kept here as a
 176    bare integer definition). -/
 177def saturation_exponent : ℤ := 45
 178
 179/-- Rung arithmetic: η_B rung (−44) plus the saturation exponent (45)
 180    equals 1, i.e. η_B ≈ φ/Θ_crit at the rung level.
 181
 182    HONEST STATUS: this is exact integer arithmetic on two DEFINED rung
 183    assignments, each of which is a HYPOTHESIS-grade empirical match. The
 184    theorem proves the arithmetic relation between the two definitions,
 185    not a physical mechanism linking the two scales. Any interpretive
 186    reading of the −44/45 complementarity is a gloss on the arithmetic,
 187    falsifiable through either rung. -/
 188theorem eta_B_times_saturation :
 189    eta_B_rung + saturation_exponent = 1 := by
 190  simp [eta_B_rung, saturation_exponent]
 191
 192/-! ## Part 5: The Connection Chain
 193
 194The derivation chain from RCL to the SIGN of η_B:
 195
 196  RCL → J unique → φ forced → 8-tick + D=3 → Q₃
 197    → Gray code (chiral, [4,2,2])
 198      → CKM (torsion overlap)
 199        → δ_CKM (Berry phase ≠ 0)
 200          → J_CP > 0 (Jarlskog)
 201            → Sakharov conditions (3 from ledger)
 202              → η_B > 0 (matter exists)  [THEOREM — the derived content]
 203
 204The MAGNITUDE η_B ≈ φ⁻⁴⁴·(1−φ⁻⁸)² is a separate HYPOTHESIS-grade rung
 205match (Part 4), not the endpoint of this chain. -/
 206
 207/-- The chain to the SIGN of the asymmetry is complete: from the Sakharov
 208    conditions + J_CP > 0, a positive baryon asymmetry follows.
 209
 210    RS-derived ingredients in the chain:
 211    - 3 generations → from D = 3 (face_pairs)
 212    - chirality → from Gray code [0,1,3,2,6,7,5,4]
 213    - flip asymmetry → [4,2,2] from the specific Gray code path
 214    - torsion → {0, 11, 17} from CW filtration
 215    - J_CP → from Berry phase × torsion overlap
 216    - Sakharov → from ledger + J_CP + EW transition
 217
 218    NOT in this chain: the magnitude (the −44 rung is HYPOTHESIS; the
 219    structural J_CP/g_★ scaffold is ~500× too large — see header). -/
 220theorem derivation_chain_complete :
 221    face_pairs 3 = 3 ∧                          -- 3 generations
 222    IsChiral grayFlipCounts ∧                    -- chirality
 223    jarlskog_structural > 0 ∧                    -- CP violation
 224    deltaB_per_sphaleron = 3 ∧                   -- B violation
 225    eta_B_structural > 0 :=                      -- matter exists (sign)
 226  ⟨rfl, cycle_is_chiral, jarlskog_positive, rfl, eta_B_positive⟩
 227
 228/-! ## Part 6: Certificate -/
 229
 230/-- Baryon asymmetry certificate: the SIGN chain (THEOREM) plus the rung
 231    arithmetic (HYPOTHESIS-grade assignments; see Part 4 docstrings).
 232
 233    Parameterized over the UNDERIVED out-of-equilibrium proposition
 234    `EWFirstOrder` (see `SakharovFromLedger`): the certificate exists only
 235    conditionally on that named physical hypothesis. -/
 236structure BaryonAsymmetryCert (EWFirstOrder : Prop) where
 237  sakharov : SakharovConditions EWFirstOrder
 238  jarlskog_pos : jarlskog_structural > 0
 239  eta_pos : eta_B_structural > 0
 240  eta_small : eta_B_structural < 1
 241  phi_rung_connection : eta_B_rung + saturation_exponent = 1
 242  chain_complete : face_pairs 3 = 3 ∧ IsChiral grayFlipCounts ∧
 243                   jarlskog_structural > 0 ∧ deltaB_per_sphaleron = 3 ∧
 244                   eta_B_structural > 0
 245
 246/-- The baryon asymmetry certificate, CONDITIONAL on the out-of-equilibrium
 247    hypothesis (not derived here). -/
 248def baryonAsymmetryCert {EWFirstOrder : Prop} (hEW : EWFirstOrder) :
 249    BaryonAsymmetryCert EWFirstOrder where
 250  sakharov := sakharov_from_RS hEW
 251  jarlskog_pos := jarlskog_positive
 252  eta_pos := eta_B_positive
 253  eta_small := eta_B_small
 254  phi_rung_connection := by simp [eta_B_rung, saturation_exponent]
 255  chain_complete := derivation_chain_complete
 256
 257end BaryonAsymmetryDerivation
 258end Cosmology
 259end IndisputableMonolith
 260