IndisputableMonolith.Cosmology.EtaBPrefactorDerivation

   1import Mathlib
   2import IndisputableMonolith.Constants
   3import IndisputableMonolith.Foundation.GapDerivation
   4import IndisputableMonolith.Cosmology.BaryonAsymmetryExact
   5import IndisputableMonolith.Cosmology.BaryonHigherOrder
   6import IndisputableMonolith.Cosmology.EtaBIntervalCert
   7
   8/-!
   9# η_B Order-One Prefactor c: SELECTED ANSATZ, NOT A DERIVATION
  10
  11**HONESTY CORRECTION (2026-07-06 audit, Thapa baryon-photon follow-up).**
  12This module's earlier docstring said it "derives the order-one prefactor
  13structurally". That was an overclaim, and it is retracted. The accurate
  14status of the prefactor `c_RS = (1 − φ^(−8))^2` is:
  15
  161. **Selected, not derived.** The squared form was chosen from a family
  17   of a-priori-comparable order-one lookalikes — (1 − δ), (1 − δ)^2,
  18   (1 − 2δ), e^(−2δ), and others with δ = φ^(−8) — because it moves the
  19   bare rung φ^(−44) ≈ 6.41×10⁻¹⁰ into the Planck band. No Boltzmann or
  20   rate calculation in this repository produces the squared polynomial
  21   form; a genuine thermal washout is exponential in Γ/H and
  22   temperature-dependent, and this factor is neither.
  23
  242. **The prefactor is numerically the missing sub-rung.** Any residual
  25   factor of order (0.9, 1.0) applied to φ^(−44) would land in the band;
  26   the selection therefore carries essentially no independent
  27   evidential weight beyond the decade-level match of the bare rung.
  28
  293. **What IS proved (and remains proved):** the algebra
  30   `c_RS_expanded`, positivity, `c_RS < 1`, and the interval arithmetic
  31   showing c_RS · φ^(−44) ∈ (6.0, 6.2)×10⁻¹⁰. These are kernel-checked
  32   facts about a *defined* quantity, not evidence that the definition is
  33   the physical washout.
  34
  35The two-sided-washout story (matter and antimatter sectors each
  36contributing one factor of (1 − δ) at the 8-tick rung) is retained
  37below as the *motivating heuristic* for why the squared form was tried
  38first. It is a HYPOTHESIS with no rate derivation behind it.
  39
  40## Epistemic Status
  41
  42DEF (ansatz): c_RS = (1 − φ^(−8))^2, a selected order-one factor.
  43THEOREM (algebra and numerical bounds only): positivity, c_RS < 1,
  44and the band inclusion c_RS · φ^(−44) ∈ (6.0, 6.2) × 10⁻¹⁰.
  45HYPOTHESIS (interpretive, no supporting calculation): the two-sided
  46washout reading of the square.
  47
  48OPEN: a Boltzmann/rate derivation with explicit Γ/H that either
  49produces this factor or replaces it. Until that exists, the honest
  50paper-level claim is the decade-level match of the bare rung φ^(−44),
  51and this module must not be cited as a precision prediction.
  52
  53Falsifier (unchanged): η_B measured outside (6.0, 6.2) × 10⁻¹⁰ at
  54> 3σ kills the squared ansatz specifically.
  55
  56## Status: 0 sorry, 0 RS-specific axiom
  57-/
  58
  59namespace IndisputableMonolith
  60namespace Cosmology
  61namespace EtaBPrefactorDerivation
  62
  63open Constants
  64open BaryonAsymmetryExact (eta_B_phi_scale eta_B_phi_scale_pos)
  65open BaryonHigherOrder (delta_washout delta_pos delta_lt_one
  66  correction_factor correction_factor_pos correction_factor_lt_one)
  67
  68noncomputable section
  69
  70/-! ## Part 1: The Two-Sided Washout Prefactor -/
  71
  72/-- The η_B order-one prefactor from two-sided 8-tick sphaleron washout.
  73
  74    Each of the matter and antimatter sectors carries one dimensionGap
  75    worth of fermionic DOF, so the washout factor (1 − φ^(−8)) appears
  76    once per sector, giving the squared structural prefactor. -/
  77def c_RS : ℝ := correction_factor ^ 2
  78
  79/-- Equivalent expanded form: c_RS = (1 − φ^(−8))^2. -/
  80theorem c_RS_expanded : c_RS = (1 - phi ^ (-8 : ℤ)) ^ 2 := by
  81  unfold c_RS BaryonHigherOrder.correction_factor BaryonHigherOrder.delta_washout
  82  rfl
  83
  84/-- The prefactor is positive. -/
  85theorem c_RS_pos : 0 < c_RS := by
  86  unfold c_RS
  87  exact pow_pos correction_factor_pos 2
  88
  89/-- The prefactor is strictly less than 1 (correction is real). -/
  90theorem c_RS_lt_one : c_RS < 1 := by
  91  unfold c_RS
  92  have h1 : correction_factor < 1 := correction_factor_lt_one
  93  have h2 : 0 < correction_factor := correction_factor_pos
  94  calc correction_factor ^ 2
  95      = correction_factor * correction_factor := by ring
  96    _ < 1 * 1 := by
  97        apply mul_lt_mul' h1.le h1 h2.le
  98        norm_num
  99    _ = 1 := by norm_num
 100
 101/-- The prefactor is order-one: 0 < c_RS < 1. -/
 102theorem c_RS_in_unit_interval : 0 < c_RS ∧ c_RS < 1 :=
 103  ⟨c_RS_pos, c_RS_lt_one⟩
 104
 105/-! ## Part 2: φ^8 Bounds via the Fibonacci Identity -/
 106
 107/-- φ^8 = 21φ + 13 from the Fibonacci formula φ^(n+1) = F(n+1)φ + F(n).
 108    Derived stepwise via φ^3, φ^4, φ^8 = (φ^4)^2 with substitutions
 109    `phi_sq_eq : phi^2 = phi + 1`. -/
 110theorem phi_pow_8_fib : phi ^ (8 : ℕ) = 21 * phi + 13 := by
 111  have h2 : phi ^ 2 = phi + 1 := phi_sq_eq
 112  have h4 : phi ^ 4 = 3 * phi + 2 := by
 113    have hexp : phi ^ 4 = phi ^ 2 * phi ^ 2 := by ring
 114    rw [hexp, h2]
 115    ring_nf
 116    linarith [h2]
 117  have hexp : phi ^ 8 = phi ^ 4 * phi ^ 4 := by ring
 118  rw [hexp, h4]
 119  ring_nf
 120  linarith [h2]
 121
 122/-- φ^8 > 46.81 (from φ > 1.61). -/
 123theorem phi_pow_8_lower : phi ^ (8 : ℕ) > 46.81 := by
 124  rw [phi_pow_8_fib]
 125  have hphi : phi > 1.61 := phi_gt_onePointSixOne
 126  linarith
 127
 128/-- φ^8 < 47.03 (from φ < 1.62). -/
 129theorem phi_pow_8_upper : phi ^ (8 : ℕ) < 47.03 := by
 130  rw [phi_pow_8_fib]
 131  have hphi : phi < 1.62 := phi_lt_onePointSixTwo
 132  linarith
 133
 134/-! ## Part 3: φ^(-8) Bounds (zpow form) -/
 135
 136private lemma phi_zpow_neg8_eq_inv : phi ^ (-8 : ℤ) = (phi ^ (8 : ℕ))⁻¹ := by
 137  rw [show ((-8 : ℤ)) = -((8 : ℕ) : ℤ) from by norm_num, zpow_neg, zpow_natCast]
 138
 139/-- φ^(-8) > 0.02126 (lower bound from φ^8 < 47.03). -/
 140theorem phi_zpow_neg8_lower : phi ^ (-8 : ℤ) > 0.02126 := by
 141  rw [phi_zpow_neg8_eq_inv]
 142  have hupper : phi ^ (8 : ℕ) < 47.03 := phi_pow_8_upper
 143  have hpos : (0 : ℝ) < phi ^ (8 : ℕ) := pow_pos phi_pos 8
 144  have h1 : (phi ^ (8 : ℕ))⁻¹ > (47.03 : ℝ)⁻¹ := by
 145    rw [gt_iff_lt, inv_lt_inv₀ (by norm_num : (0:ℝ) < 47.03) hpos]
 146    exact hupper
 147  have h2 : (47.03 : ℝ)⁻¹ ≥ 0.02126 := by norm_num
 148  linarith
 149
 150/-- φ^(-8) < 0.02137 (upper bound from φ^8 > 46.81). -/
 151theorem phi_zpow_neg8_upper : phi ^ (-8 : ℤ) < 0.02137 := by
 152  rw [phi_zpow_neg8_eq_inv]
 153  have hlower : phi ^ (8 : ℕ) > 46.81 := phi_pow_8_lower
 154  have hpos : (0 : ℝ) < phi ^ (8 : ℕ) := pow_pos phi_pos 8
 155  have h1 : (phi ^ (8 : ℕ))⁻¹ < (46.81 : ℝ)⁻¹ := by
 156    rw [inv_lt_inv₀ hpos (by norm_num : (0:ℝ) < 46.81)]
 157    exact hlower
 158  have h2 : (46.81 : ℝ)⁻¹ ≤ 0.02137 := by norm_num
 159  linarith
 160
 161/-! ## Part 4: Bounds on (1 − φ^(-8)) and c_RS -/
 162
 163/-- (1 − φ^(−8)) > 0.978. -/
 164theorem one_minus_phi_neg8_lower : (1 - phi ^ (-8 : ℤ)) > 0.978 := by
 165  have h := phi_zpow_neg8_upper
 166  linarith
 167
 168/-- (1 − φ^(−8)) < 0.979. -/
 169theorem one_minus_phi_neg8_upper : (1 - phi ^ (-8 : ℤ)) < 0.979 := by
 170  have h := phi_zpow_neg8_lower
 171  linarith
 172
 173/-- c_RS > 0.956 (lower numerical bound). -/
 174theorem c_RS_lower : c_RS > 0.956 := by
 175  rw [c_RS_expanded]
 176  have hl : (1 - phi ^ (-8 : ℤ)) > 0.978 := one_minus_phi_neg8_lower
 177  have hu : (1 - phi ^ (-8 : ℤ)) < 0.979 := one_minus_phi_neg8_upper
 178  have hpos : 0 < (1 - phi ^ (-8 : ℤ)) := by linarith
 179  nlinarith [hl, hu, hpos]
 180
 181/-- c_RS < 0.959 (upper numerical bound). -/
 182theorem c_RS_upper : c_RS < 0.959 := by
 183  rw [c_RS_expanded]
 184  have hl : (1 - phi ^ (-8 : ℤ)) > 0.978 := one_minus_phi_neg8_lower
 185  have hu : (1 - phi ^ (-8 : ℤ)) < 0.979 := one_minus_phi_neg8_upper
 186  have hpos : 0 < (1 - phi ^ (-8 : ℤ)) := by linarith
 187  nlinarith [hl, hu, hpos]
 188
 189/-! ## Part 5: φ^(-44) Bounds via the Fibonacci Identity -/
 190
 191private lemma phi_zpow_neg44_eq_inv : phi ^ (-44 : ℤ) = (phi ^ (44 : ℕ))⁻¹ := by
 192  rw [show ((-44 : ℤ)) = -((44 : ℕ) : ℤ) from by norm_num, zpow_neg, zpow_natCast]
 193
 194/-- φ^(−44) > 6.37 × 10⁻¹⁰ (uses φ < 1.62 in the Fibonacci formula). -/
 195theorem phi_zpow_neg44_lower : phi ^ (-44 : ℤ) > 6.37e-10 := by
 196  rw [phi_zpow_neg44_eq_inv]
 197  have hupper : phi ^ (44 : ℕ) < 1.5698e9 := by
 198    rw [EtaBIntervalCert.phi_pow_44_fib]
 199    have hphi_lt : phi < 1.62 := phi_lt_onePointSixTwo
 200    nlinarith
 201  have hpos : (0 : ℝ) < phi ^ (44 : ℕ) := pow_pos phi_pos 44
 202  have h1 : (phi ^ (44 : ℕ))⁻¹ > (1.5698e9 : ℝ)⁻¹ := by
 203    rw [gt_iff_lt, inv_lt_inv₀ (by norm_num : (0:ℝ) < 1.5698e9) hpos]
 204    exact hupper
 205  have h2 : (1.5698e9 : ℝ)⁻¹ ≥ 6.37e-10 := by norm_num
 206  linarith
 207
 208/-- φ^(−44) < 6.40 × 10⁻¹⁰ (uses φ > 1.61 in the Fibonacci formula). -/
 209theorem phi_zpow_neg44_upper : phi ^ (-44 : ℤ) < 6.40e-10 := by
 210  rw [phi_zpow_neg44_eq_inv]
 211  have hlower : phi ^ (44 : ℕ) > 1.5627e9 := by
 212    rw [EtaBIntervalCert.phi_pow_44_fib]
 213    have hphi_gt : phi > 1.61 := phi_gt_onePointSixOne
 214    nlinarith
 215  have hpos : (0 : ℝ) < phi ^ (44 : ℕ) := pow_pos phi_pos 44
 216  have h1 : (phi ^ (44 : ℕ))⁻¹ < (1.5627e9 : ℝ)⁻¹ := by
 217    rw [inv_lt_inv₀ hpos (by norm_num : (0:ℝ) < 1.5627e9)]
 218    exact hlower
 219  have h2 : (1.5627e9 : ℝ)⁻¹ < 6.40e-10 := by norm_num
 220  linarith
 221
 222/-! ## Part 6: The Corrected η_B Prediction -/
 223
 224/-- The fully-corrected RS prediction for η_B:
 225    η_B^RS = c_RS × φ^(−44) = (1 − φ^(−8))^2 × φ^(−44). -/
 226def eta_B_corrected_two_sided : ℝ := c_RS * eta_B_phi_scale
 227
 228/-- The corrected prediction is positive. -/
 229theorem eta_B_corrected_two_sided_pos : 0 < eta_B_corrected_two_sided := by
 230  unfold eta_B_corrected_two_sided
 231  exact mul_pos c_RS_pos eta_B_phi_scale_pos
 232
 233/-- The corrected prediction is strictly less than the leading term φ^(−44). -/
 234theorem corrected_lt_leading : eta_B_corrected_two_sided < eta_B_phi_scale := by
 235  unfold eta_B_corrected_two_sided
 236  have h := c_RS_lt_one
 237  have hpos := eta_B_phi_scale_pos
 238  calc c_RS * eta_B_phi_scale
 239      < 1 * eta_B_phi_scale := mul_lt_mul_of_pos_right h hpos
 240    _ = eta_B_phi_scale := one_mul _
 241
 242/-! ## Part 7: The Tight Numerical Band Containing the Observed Value -/
 243
 244/-- η_B^RS > 6.0 × 10⁻¹⁰ (strict lower bound). -/
 245theorem eta_B_corrected_lower : eta_B_corrected_two_sided > 6.0e-10 := by
 246  unfold eta_B_corrected_two_sided eta_B_phi_scale
 247  have hc : c_RS > 0.956 := c_RS_lower
 248  have hphi_lower : phi ^ (-44 : ℤ) > 6.37e-10 := phi_zpow_neg44_lower
 249  have hcpos : (0 : ℝ) < c_RS := c_RS_pos
 250  have hphi_pos : (0 : ℝ) < phi ^ (-44 : ℤ) := zpow_pos phi_pos (-44)
 251  -- 0.956 × 6.37e-10 = 6.0897e-10 > 6.0e-10
 252  nlinarith [hc, hphi_lower, hcpos, hphi_pos]
 253
 254/-- η_B^RS < 6.2 × 10⁻¹⁰ (strict upper bound). -/
 255theorem eta_B_corrected_upper : eta_B_corrected_two_sided < 6.2e-10 := by
 256  unfold eta_B_corrected_two_sided eta_B_phi_scale
 257  have hc : c_RS < 0.959 := c_RS_upper
 258  have hphi_upper : phi ^ (-44 : ℤ) < 6.40e-10 := phi_zpow_neg44_upper
 259  have hcpos : (0 : ℝ) < c_RS := c_RS_pos
 260  have hphi_pos : (0 : ℝ) < phi ^ (-44 : ℤ) := zpow_pos phi_pos (-44)
 261  -- 0.959 × 6.40e-10 = 6.1376e-10 < 6.2e-10
 262  nlinarith [hc, hphi_upper, hcpos, hphi_pos]
 263
 264/-- The corrected RS prediction lies in the band (6.0, 6.2) × 10⁻¹⁰,
 265    which contains the Planck 2018 central value 6.10 × 10⁻¹⁰. -/
 266theorem eta_B_corrected_in_observed_band :
 267    eta_B_corrected_two_sided > 6.0e-10 ∧ eta_B_corrected_two_sided < 6.2e-10 :=
 268  ⟨eta_B_corrected_lower, eta_B_corrected_upper⟩
 269
 270/-- The Planck 2018 observed central value 6.10 × 10⁻¹⁰ falls inside
 271    the predicted band (6.0, 6.2) × 10⁻¹⁰. -/
 272theorem observed_in_predicted_band :
 273    (6.0e-10 : ℝ) < 6.10e-10 ∧ (6.10e-10 : ℝ) < 6.2e-10 := by
 274  constructor <;> norm_num
 275
 276/-! ## Part 8: Comparison with the First-Order Correction -/
 277
 278/-- The two-sided correction is strictly stronger than the first-order
 279    one-sided correction (since c_RS = correction_factor² < correction_factor). -/
 280theorem two_sided_stronger_than_one_sided :
 281    c_RS < correction_factor := by
 282  unfold c_RS
 283  have h1 : correction_factor < 1 := correction_factor_lt_one
 284  have h2 : 0 < correction_factor := correction_factor_pos
 285  calc correction_factor ^ 2
 286      = correction_factor * correction_factor := by ring
 287    _ < 1 * correction_factor := mul_lt_mul_of_pos_right h1 h2
 288    _ = correction_factor := one_mul _
 289
 290/-- The two-sided corrected prediction is strictly smaller than the
 291    one-sided corrected prediction (`BaryonHigherOrder.eta_B_corrected`). -/
 292theorem two_sided_corrected_lt_one_sided :
 293    eta_B_corrected_two_sided < BaryonHigherOrder.eta_B_corrected := by
 294  unfold eta_B_corrected_two_sided BaryonHigherOrder.eta_B_corrected
 295  have h := two_sided_stronger_than_one_sided
 296  have hpos := eta_B_phi_scale_pos
 297  have := mul_lt_mul_of_pos_right h hpos
 298  linarith [this]
 299
 300/-! ## Part 9: Master Certificate -/
 301
 302/-- The η_B prefactor certificate.
 303
 304    The order-one prefactor c in η_B = c × J_CP × (Γ_sph/H) / g★
 305    is structurally derived as c_RS = (1 − φ^(−8))^2 from
 306    two-sided 8-tick sphaleron washout. -/
 307structure EtaBPrefactorCert where
 308  /-- c_RS is order-one. -/
 309  prefactor_in_unit : 0 < c_RS ∧ c_RS < 1
 310  /-- Numerical band on c_RS. -/
 311  prefactor_band : c_RS > 0.956 ∧ c_RS < 0.959
 312  /-- Two-sided expansion. -/
 313  expanded : c_RS = (1 - phi ^ (-8 : ℤ)) ^ 2
 314  /-- Corrected prediction lies in the (6.0, 6.2) × 10⁻¹⁰ band. -/
 315  prediction_band :
 316    eta_B_corrected_two_sided > 6.0e-10 ∧ eta_B_corrected_two_sided < 6.2e-10
 317  /-- Planck 2018 central value 6.10 × 10⁻¹⁰ is inside the band. -/
 318  observed_inside : (6.0e-10 : ℝ) < 6.10e-10 ∧ (6.10e-10 : ℝ) < 6.2e-10
 319  /-- The two-sided correction strictly improves on the one-sided
 320      correction. -/
 321  improves_on_one_sided :
 322    eta_B_corrected_two_sided < BaryonHigherOrder.eta_B_corrected
 323
 324/-- **THE η_B PREFACTOR THEOREM**:
 325
 326    The order-one prefactor c in the η_B baryogenesis formula is
 327    structurally determined by the two-sided 8-tick washout:
 328
 329      c_RS := (1 − φ^(−8))^2
 330
 331    The corrected RS prediction
 332    η_B^RS = c_RS × φ^(−44)
 333    lies in the band (6.0, 6.2) × 10⁻¹⁰, which contains the Planck 2018
 334    central value 6.10 × 10⁻¹⁰. -/
 335theorem eta_B_prefactor_cert : EtaBPrefactorCert where
 336  prefactor_in_unit := c_RS_in_unit_interval
 337  prefactor_band := ⟨c_RS_lower, c_RS_upper⟩
 338  expanded := c_RS_expanded
 339  prediction_band := eta_B_corrected_in_observed_band
 340  observed_inside := observed_in_predicted_band
 341  improves_on_one_sided := two_sided_corrected_lt_one_sided
 342
 343end
 344
 345end EtaBPrefactorDerivation
 346end Cosmology
 347end IndisputableMonolith
 348