IndisputableMonolith.Cosmology.BaryogenesisStaging
IndisputableMonolith/Cosmology/BaryogenesisStaging.lean · 1564 lines · 172 declarations
show as:
view math explainer →
1import Mathlib
2import IndisputableMonolith.Cosmology.SakharovFromLedger
3import IndisputableMonolith.Cosmology.SphaleronRate
4import IndisputableMonolith.Cosmology.EWPhaseTransition
5import IndisputableMonolith.StandardModel.JarlskogInvariant
6import IndisputableMonolith.StandardModel.RelativisticDOF
7
8/-!
9# Baryogenesis Staging
10
11Curated staging module for the Steve baryogenesis derivation loop.
12
13The purpose of this file is to hold small, honest theorem targets that prevent the
14baryogenesis lane from faking the missing mechanism. The first invariant is the
15sphaleron zero-protection obstruction: electroweak sphalerons conserve B-L, so if
16the sourced B-L charge is zero and sphalerons equilibrate, the surviving baryon
17number is zero.
18
19Loop-generated targets may be appended below the marker. They must not introduce
20new axioms, `admit`, or fake physics conditions as `True`.
21-/
22
23namespace IndisputableMonolith
24namespace Cosmology
25namespace BaryogenesisStaging
26
27noncomputable section
28
29/-- Standard Model sphaleron reprocessing coefficient for three generations:
30`B = (28 / 79) * (B - L)` after electroweak sphaleron equilibration. -/
31def sphaleronReprocessingFactor : ℚ := 28 / 79
32
33/-- If no B-L charge is sourced, sphaleron equilibrium leaves no baryon excess. -/
34theorem sphaleron_equilibrium_zero_of_zero_BminusL :
35 sphaleronReprocessingFactor * (0 : ℚ) = 0 := by
36 simp [sphaleronReprocessingFactor]
37
38/-- The reprocessing factor is positive. This makes the conversion a real sign-preserving
39map from a B-L relic to baryon number, not a tautology. -/
40theorem sphaleronReprocessingFactor_pos : 0 < sphaleronReprocessingFactor := by
41 norm_num [sphaleronReprocessingFactor]
42
43/-- The reprocessing factor is strictly less than one: sphalerons reprocess a B-L
44relic rather than copying it unchanged. -/
45theorem sphaleronReprocessingFactor_lt_one : sphaleronReprocessingFactor < 1 := by
46 norm_num [sphaleronReprocessingFactor]
47
48/-- Relic comoving B−L charge: source `a³ S_X` folded against the real
49 exponential survival kernel `exp(−∫ Γ)`. This is the B4 integral solution
50 of the comoving Boltzmann equation `dN_X/dt = a³ S_X − Γ_wash N_X`. -/
51noncomputable def relicCharge (a3S Γ : ℝ → ℝ) (t₀ tf : ℝ) : ℝ :=
52 ∫ t' in t₀..tf, a3S t' * Real.exp (-(∫ s in t'..tf, Γ s))
53
54noncomputable def washoutExponent (Γ : ℝ → ℝ) (t' tf : ℝ) : ℝ :=
55 ∫ s in t'..tf, Γ s
56
57theorem Bfinal_zero_iff_BminusL_zero (BmL : ℚ) :
58 (28 / 79 : ℚ) * BmL = 0 ↔ BmL = 0 := by
59 first
60 | rfl
61 | linarith
62 | nlinarith
63 | gcongr
64 | positivity
65 | norm_num
66 | ring
67 | abel
68 | field_simp
69 | omega
70 | simp_all
71 | simp
72 | aesop
73 | tauto
74 | decide
75 | exact le_refl _
76 | (intro _ <;> linarith)
77 | (intro _ <;> simp_all)
78 | (constructor <;> linarith)
79 | (constructor <;> simp_all)
80
81theorem obstruction_Bfinal (BminusL : ℚ) :
82 (28 / 79 : ℚ) * BminusL = 0 ↔ BminusL = 0 := by
83 first
84 | rfl
85 | linarith
86 | nlinarith
87 | gcongr
88 | positivity
89 | norm_num
90 | ring
91 | abel
92 | field_simp
93 | omega
94 | simp_all
95 | simp
96 | aesop
97 | tauto
98 | decide
99 | exact le_refl _
100 | (intro _ <;> linarith)
101 | (intro _ <;> simp_all)
102 | (constructor <;> linarith)
103 | (constructor <;> simp_all)
104
105structure FreezeOutWindow where
106 H : ℝ → ℝ
107 Γwash : ℝ → ℝ
108 chiDot : ℝ → ℝ
109 t₀ : ℝ
110 tf : ℝ
111 H_pos : ∀ t, 0 < H t
112 Γ_nonneg : ∀ t, 0 ≤ Γwash t
113 window_ord : t₀ ≤ tf
114 /-- Freeze-out is the crossing of the washout rate through Hubble. -/
115 crossing : Γwash tf = H tf
116 /-- Rolling background is static after the window closes. -/
117 static_after : ∀ t, tf < t → chiDot t = 0
118 /-- Rolling background is static before the window opens. -/
119 static_before : ∀ t, t < t₀ → chiDot t = 0
120
121noncomputable def muBL (Kx chiDot : ℝ) : ℝ := Kx * chiDot
122
123noncomputable def susceptibility (cχ T : ℝ) : ℝ := cχ * T ^ 2
124
125noncomputable def nEqBL (cχ T Kx chiDot : ℝ) : ℝ :=
126 susceptibility cχ T * muBL Kx chiDot
127
128noncomputable def sourceBL (Γ cχ T Kx chiDot : ℝ) : ℝ :=
129 Γ * nEqBL cχ T Kx chiDot
130
131/-- Gate (source-off, χ̇): no rolling background ⇒ no source. -/
132theorem sourceBL_zero_of_chiDot_zero (Γ cχ T Kx : ℝ) :
133 sourceBL Γ cχ T Kx 0 = 0 := by
134 unfold sourceBL nEqBL muBL susceptibility
135 ring
136
137open Real
138
139/-! ### B3→B4: rolling-χ source profile + exponential survival kernel
140
141We already have the *scalar* source `sourceBL Γ cχ T Kx chiDot` (B2) and the
142washout exponent `washoutExponent Γ t' tf` (B4). This node lifts the source to a
143time-dependent background `a³ S_X(t)` and integrates it against the exponential
144survival kernel `exp(−∫_{t'}^{tf} Γ_wash)`, proving the limiting gates needed
145before any number. Profiles `χ̇(t)`, `Γ_wash(t)`, `H(t)`, `c_χ(t)`, `T(t)` and
146the window endpoints stay symbolic (OPEN). -/
147
148/-- Rolling B-L source background fed into the Boltzmann integral:
149 `a³ S_X(t) = a(t)³ · Γ_wash(t) · c_χ(t) · T(t)² · K_X · χ̇(t)`,
150 built from the banked B2 scalar `sourceBL`. -/
151noncomputable def a3SourceBL (a Γw cχ T chiDot : ℝ → ℝ) (Kx : ℝ) (t : ℝ) : ℝ :=
152 (a t)^3 * sourceBL (Γw t) (cχ t) (T t) Kx (chiDot t)
153
154/-- Exponential survival kernel from `t'` to freeze-out `tf`:
155 `exp(−∫_{t'}^{tf} Γ_wash)`. This is the genuine Boltzmann survival factor,
156 NOT a polynomial `(1 − φ⁻⁸)ᵏ`. -/
157noncomputable def kernelBL (Γw : ℝ → ℝ) (t' tf : ℝ) : ℝ :=
158 Real.exp (- washoutExponent Γw t' tf)
159
160/-- The kernel is strictly positive: washout can suppress but never sign-flip. -/
161theorem kernelBL_pos (Γw : ℝ → ℝ) (t' tf : ℝ) : 0 < kernelBL Γw t' tf :=
162 Real.exp_pos _
163
164/-- Nonnegative accumulated washout ⇒ survival weight ≤ 1.
165 (`Γ_wash ≥ 0` integrated forward gives `∫ Γ_wash ≥ 0`, so `exp(−·) ≤ 1`.) -/
166theorem kernelBL_le_one_of_nonneg (Γw : ℝ → ℝ) (t' tf : ℝ)
167 (h : 0 ≤ washoutExponent Γw t' tf) : kernelBL Γw t' tf ≤ 1 := by
168 unfold kernelBL
169 rw [Real.exp_le_one_iff]
170 linarith
171
172/-- Boltzmann relic (comoving B-L charge surviving to `tf`):
173 `∫_{t₀}^{tf} a³ S_X(t') · exp(−∫_{t'}^{tf} Γ_wash) dt'`.
174 Real exponential survival under the integral — the B4 acceptance shape. -/
175noncomputable def relicChargeProfile
176 (a Γw cχ T chiDot : ℝ → ℝ) (Kx t₀ tf : ℝ) : ℝ :=
177 ∫ t' in t₀..tf, a3SourceBL a Γw cχ T chiDot Kx t' * kernelBL Γw t' tf
178
179/-- Pointwise source-off: `χ̇(t) = 0` kills the background at `t`,
180 routing through the banked B2 lemma `sourceBL_zero_of_chiDot_zero`. -/
181theorem a3SourceBL_zero_of_chiDot_zero
182 (a Γw cχ T chiDot : ℝ → ℝ) (Kx t : ℝ) (h : chiDot t = 0) :
183 a3SourceBL a Γw cχ T chiDot Kx t = 0 := by
184 unfold a3SourceBL
185 rw [h, sourceBL_zero_of_chiDot_zero, mul_zero]
186
187/-- **Source-off limit (B3/B4 gate):** if the rolling field is frozen
188 (`χ̇ ≡ 0`) on the whole window, the relic vanishes identically.
189 This is the `dotChi = 0 ⇒ no relic` falsifier, composing B2→B4. -/
190theorem relicChargeProfile_zero_of_chiDot_zero
191 (a Γw cχ T chiDot : ℝ → ℝ) (Kx t₀ tf : ℝ)
192 (h : ∀ t', chiDot t' = 0) :
193 relicChargeProfile a Γw cχ T chiDot Kx t₀ tf = 0 := by
194 unfold relicChargeProfile
195 have hz : ∀ t', a3SourceBL a Γw cχ T chiDot Kx t' * kernelBL Γw t' tf = 0 := by
196 intro t'
197 rw [a3SourceBL_zero_of_chiDot_zero a Γw cχ T chiDot Kx t' (h t'), zero_mul]
198 simp only [hz, intervalIntegral.integral_zero]
199
200/-- **Orientation reversal (pointwise):** flipping the rolling direction
201 `χ̇ ↦ −χ̇` flips the source background, because `sourceBL` is linear in `χ̇`
202 through `muBL Kx χ̇ = Kx·χ̇`. The integral-level sign flip then follows from
203 linearity of `∫` (integrability tagged OPEN). -/
204theorem a3SourceBL_odd
205 (a Γw cχ T chiDot : ℝ → ℝ) (Kx t : ℝ) :
206 a3SourceBL a Γw cχ T (fun s => - chiDot s) Kx t
207 = - a3SourceBL a Γw cχ T chiDot Kx t := by
208 simp only [a3SourceBL, sourceBL, nEqBL, susceptibility, muBL]
209 ring
210
211namespace EntropyPhotonConversion
212
213/-- **B6 observable epoch tag.** The entropy/photon multiplier `R = s/n_γ` is
214 evaluated TODAY, i.e. *after* e⁺e⁻ annihilation has dumped its entropy into
215 the photon bath. Before annihilation `s/n_γ` differs (the e± degrees of
216 freedom are still relativistic), so the epoch must be named explicitly to
217 forbid silently using the wrong multiplier. This is a transparent wrapper
218 that records the epoch; numerically `R` is bounded by
219 `entropyPhotonRatio_today_band ∈ (7.0, 7.1)`. -/
220noncomputable def entropyPhotonRatioPostAnnihilation (R : ℝ) : ℝ := R
221
222/-- **B6 base carrier.** Convert a frozen comoving yield `Y_B = n_B/s` into the
223 observable `η_B = n_B/n_γ` by the dimensionless multiplier `R = s/n_γ`:
224
225 η_B = R · Y_B.
226
227 `Y_B` is dimensionless (charge per entropy), `R` is dimensionless
228 (entropy per photon), so the product is dimensionless `n_B/n_γ`. No
229 magnitude is chosen here — both `R` and `Y_B` are formal arguments. -/
230noncomputable def etaBFromYield (R YB : ℝ) : ℝ := R * YB
231
232/-- The epoch-tagged multiplier is the multiplier used by the carrier:
233 `etaBFromYield` consumes exactly `entropyPhotonRatioPostAnnihilation R`. -/
234theorem etaBFromYield_uses_postAnnihilation (R YB : ℝ) :
235 etaBFromYield (entropyPhotonRatioPostAnnihilation R) YB = R * YB := by
236 unfold etaBFromYield entropyPhotonRatioPostAnnihilation; ring
237
238/-- **Source-off gate.** A zero frozen yield gives a zero observable. This is the
239 propagation endpoint: `χ̇ = 0` on the window ⇒ `Y_{B-L} = 0`
240 (`relicChargeProfile_zero_of_chiDot_zero`) ⇒ `Y_B = 0` ⇒ `η_B = 0`. -/
241theorem etaBFromYield_zero_of_YB_zero (R : ℝ) :
242 etaBFromYield R 0 = 0 := by
243 unfold etaBFromYield; ring
244
245/-- **Linearity in the yield.** The carrier is additive in `Y_B`, so it cannot
246 manufacture asymmetry: the observable is exactly proportional to the
247 upstream frozen charge. -/
248theorem etaBFromYield_add (R YB₁ YB₂ : ℝ) :
249 etaBFromYield R (YB₁ + YB₂) = etaBFromYield R YB₁ + etaBFromYield R YB₂ := by
250 unfold etaBFromYield; ring
251
252/-- **Sign preservation.** A positive multiplier maps a positive yield to a
253 positive observable. With `R ∈ (7.0,7.1) > 0`, the sign of `η_B` is the sign
254 of the frozen `Y_B`. -/
255theorem etaBFromYield_pos_of_pos (R YB : ℝ) (hR : 0 < R) (hY : 0 < YB) :
256 0 < etaBFromYield R YB := by
257 unfold etaBFromYield; exact mul_pos hR hY
258
259/-- **Orientation reversal.** Flipping the 8-tick orientation flips `Y_B`
260 (`a3SourceBL_odd` upstream); the linear carrier carries that flip to `η_B`. -/
261theorem etaBFromYield_odd (R YB : ℝ) :
262 etaBFromYield R (-YB) = - etaBFromYield R YB := by
263 unfold etaBFromYield; ring
264
265end EntropyPhotonConversion
266
267namespace SourceCoefficient
268
269open Constants
270
271/-- **CKN source coefficient.** B−L is gauge-anomaly-free, so the only χ source
272 is the derivative coupling `(∂_μχ/f_χ)·J^μ_{B-L}`, giving
273 `μ_{B-L} = ε·χ̇/f_χ`. Hence `K_X = ε/f_χ`: sign `ε` from the 8-tick
274 orientation, magnitude from the decay constant `f_χ`. No η_B input. -/
275noncomputable def KXcoeff (ε fχ : ℝ) : ℝ := ε / fχ
276
277theorem KXcoeff_eq (ε fχ : ℝ) : KXcoeff ε fχ = ε / fχ := rfl
278
279/-- Nonzero orientation and finite decay constant give a nonzero coefficient. -/
280theorem KXcoeff_ne_zero (ε fχ : ℝ) (hε : ε ≠ 0) (hf : fχ ≠ 0) :
281 KXcoeff ε fχ ≠ 0 := div_ne_zero hε hf
282
283/-- Orientation reversal negates the source coefficient — structural origin of
284 the sign carried to η_B via `a3SourceBL_odd` / `etaBFromYield_odd`. -/
285theorem KXcoeff_orient_odd (ε fχ : ℝ) :
286 KXcoeff (-ε) fχ = - KXcoeff ε fχ := by
287 unfold KXcoeff; ring
288
289/-- `μ_{B-L} = ε·χ̇/f_χ`, linear in χ̇ and source-off at χ̇ = 0. -/
290theorem muBL_from_KXcoeff (ε fχ chiDot : ℝ) :
291 muBL (KXcoeff ε fχ) chiDot = ε * chiDot / fχ := by
292 unfold muBL KXcoeff; ring
293
294/-- Source-off limit at the coefficient level. -/
295theorem muBL_from_KXcoeff_zero (ε fχ : ℝ) :
296 muBL (KXcoeff ε fχ) 0 = 0 := by
297 rw [muBL_from_KXcoeff]; ring
298
299end SourceCoefficient
300
301theorem outOfEquilibrium_falsifiable
302 (Γw H : ℝ → ℝ) (tf : ℝ) (hsuper : ∀ t, H t < Γw t) :
303 ¬ (Γw tf = H tf ∧ ∀ t, tf < t → Γw t < H t) := by
304 rintro ⟨hcross, _⟩
305 have h := hsuper tf
306 rw [hcross] at h
307 exact lt_irrefl _ h
308
309namespace SakharovFromLedger
310
311/-- Sphaleron-equilibrium reprocessing factor as a function of
312 fermion generation count N and Higgs-doublet count nH.
313 Origin: chemical-potential balance (sphaleron anomaly + Yukawa
314 equilibrium + hypercharge neutrality), Harvey & Turner (1990). -/
315def reprocessingFactorOf (N nH : ℤ) : ℚ :=
316 (8 * N + 4 * nH) / (22 * N + 13 * nH)
317
318/-- The banked constant 28/79 is the N=3, n_H=1 instance. -/
319theorem reprocessingFactorOf_SM :
320 reprocessingFactorOf 3 1 = sphaleronReprocessingFactor := by
321 unfold reprocessingFactorOf
322 norm_num [sphaleronReprocessingFactor]
323
324/-- Generation-count falsifier: the factor is not universal.
325 A four-generation world gives 36/101 ≠ 28/79. -/
326theorem reprocessingFactorOf_gen_sensitive :
327 reprocessingFactorOf 4 1 ≠ reprocessingFactorOf 3 1 := by
328 unfold reprocessingFactorOf
329 norm_num
330
331/-- Zero-protection obstruction restated through the derived factor:
332 for ANY generation/Higgs content, B−L = 0 forces B = 0. -/
333theorem obstruction_via_derivedFactor (N nH : ℤ) :
334 reprocessingFactorOf N nH * (0 : ℚ) = 0 := by
335 simp
336
337end SakharovFromLedger
338
339namespace SakharovFromLedger
340
341/-- Zero-protection through the DERIVED factor, for arbitrary gauge content.
342 B_final = factor·(B−L) vanishes IFF B−L vanishes, provided the sphaleron
343 anomaly numerator 8N+4nH and denominator 22N+13nH are nonzero.
344 Protection is tied to the NONVANISHING anomaly numerator, not to one
345 magic rational. -/
346theorem obstruction_via_derivedFactor_iff (N nH : ℤ) (BmL : ℚ)
347 (hnum : ((8 * N + 4 * nH : ℤ) : ℚ) ≠ 0)
348 (hden : ((22 * N + 13 * nH : ℤ) : ℚ) ≠ 0) :
349 reprocessingFactorOf N nH * BmL = 0 ↔ BmL = 0 := by
350 unfold reprocessingFactorOf
351 rw [div_mul_eq_mul_div, div_eq_zero_iff]
352 push_cast
353 rw [mul_eq_zero]
354 constructor
355 · rintro ((h | h) | h)
356 · exact absurd (by push_cast at hnum ⊢; exact h) hnum
357 · exact h
358 · exact absurd (by push_cast at hden ⊢; exact h) hden
359 · intro h
360 left; right; exact h
361
362/-- FORCING direction (physical payload): for SM content (N=3, n_H=1),
363 a nonzero baryon relic forces a nonzero B−L. This is the contrapositive
364 that sends the loop out of sphaleron internals and into the B2
365 out-of-orbit CP-odd source. -/
366theorem nonzero_relic_forces_BminusL (BmL : ℚ)
367 (h : reprocessingFactorOf 3 1 * BmL ≠ 0) : BmL ≠ 0 := by
368 intro hz
369 exact h (by rw [hz, mul_zero])
370
371end SakharovFromLedger
372
373namespace SakharovFromLedger
374
375/-- The derived sphaleron factor, evaluated at forced SM content
376 (N_gen = 3, n_H = 1), equals 28/79 by explicit anomaly-coefficient
377 arithmetic:
378 numerator 8·3 + 4·1 = 28
379 denominator 22·3 + 13·1 = 79.
380 This certifies that the literal constant in every obstruction lemma
381 IS the Harvey–Turner functional form, not an asserted magic rational. -/
382theorem reprocessingFactorOf_SM_value :
383 reprocessingFactorOf 3 1 = (28 / 79 : ℚ) := by
384 unfold reprocessingFactorOf
385 norm_num
386
387/-- The opaque banked def is pinned to its literal value, so
388 `reprocessingFactorOf_SM` and `obstruction_Bfinal` refer to the
389 SAME computed rational. -/
390theorem sphaleronReprocessingFactor_value :
391 sphaleronReprocessingFactor = (28 / 79 : ℚ) := by
392 rw [← reprocessingFactorOf_SM, reprocessingFactorOf_SM_value]
393
394end SakharovFromLedger
395
396namespace SakharovFromLedger
397
398/-- Lepton-axis equilibrium reprocessing coefficient at N_g = 3:
399 L = (−51/79)(B−L). Paired partner of `sphaleronReprocessingFactor`. -/
400def leptonReprocessingFactor : ℚ := -51 / 79
401
402/-- CLOSURE: the baryon and lepton equilibrium coefficients differ by exactly 1.
403 This is the arithmetic content of "B−L is the conserved combination":
404 (28/79) − (−51/79) = 79/79 = 1.
405 It is NOT the kernel statement (`obstruction_Bfinal`) and NOT the contraction
406 (`relic_bounded_by_source`); it is the cross-axis identity those lemmas assume. -/
407theorem reprocessing_conserves_BminusL :
408 sphaleronReprocessingFactor - leptonReprocessingFactor = 1 := by
409 rw [sphaleronReprocessingFactor_value]
410 unfold leptonReprocessingFactor
411 norm_num
412
413/-- FIXED POINT: the equilibrium output charges reproduce the input B−L for every
414 source value. Sphalerons drive B and L but leave B−L invariant — the precise
415 sense in which they cannot be a B−L source. -/
416theorem output_BminusL_eq_input (BmL : ℚ) :
417 sphaleronReprocessingFactor * BmL - leptonReprocessingFactor * BmL = BmL := by
418 have hfac :
419 sphaleronReprocessingFactor * BmL - leptonReprocessingFactor * BmL
420 = (sphaleronReprocessingFactor - leptonReprocessingFactor) * BmL := by ring
421 rw [hfac, reprocessing_conserves_BminusL, one_mul]
422
423/-- ZERO-PROTECTION: with no B−L source, sphaleron equilibrium drives B to zero.
424 This is the obstruction that forces the baryogenesis route to produce B−L. -/
425theorem zero_BmL_gives_zero_B (BmL : ℚ) (h : BmL = 0) :
426 sphaleronReprocessingFactor * BmL = 0 := by
427 rw [h, mul_zero]
428
429end SakharovFromLedger
430
431namespace SakharovFromLedger
432
433/-- Equilibrium baryon number as the sphaleron map applied to the
434 separately given initial baryon and lepton numbers. Input is the
435 pair `(B, L)`, not the precomputed combination `B − L`. -/
436def sphaleronEquilibriumB (B L : ℚ) : ℚ :=
437 sphaleronReprocessingFactor * (B - L)
438
439/-- WASHOUT READING OF THE WALL. A purely `B+L` asymmetry (any `B = L`,
440 including `B ≠ 0`) is driven to `B_final = 0` by sphaleron
441 equilibration. -/
442theorem sphaleron_washes_out_BplusL (B L : ℚ) (h : B = L) :
443 sphaleronEquilibriumB B L = 0 := by
444 unfold sphaleronEquilibriumB
445 rw [h, sub_self, mul_zero]
446
447/-- TEETH: if the initial state carries genuine `B−L` (`B ≠ L`), the
448 equilibrium baryon number is nonzero. The wall erases exactly the
449 `B+L` direction and nothing else. -/
450theorem sphaleron_preserves_only_BminusL (B L : ℚ) (h : B ≠ L) :
451 sphaleronEquilibriumB B L ≠ 0 := by
452 unfold sphaleronEquilibriumB
453 have hsub : B - L ≠ 0 := sub_ne_zero.mpr h
454 exact mul_ne_zero (ne_of_gt sphaleronReprocessingFactor_pos) hsub
455
456end SakharovFromLedger
457
458namespace SakharovFromLedger
459
460/-- Sphaleron-reprocessed baryon number acting on the real-valued frozen
461 B−L charge produced by the Boltzmann relic. Same 28/79 factor as the
462 rational wall, lifted to the field where `relicChargeProfile` lives. -/
463noncomputable def BfinalFromRelicBL (BmL : ℝ) : ℝ := (28 / 79 : ℝ) * BmL
464
465/-- The wall is intact over ℝ: the reprocessed baryon number vanishes iff the
466 frozen B−L vanishes. Routes through the nonzero 28/79 factor. -/
467theorem BfinalFromRelicBL_zero_iff (BmL : ℝ) :
468 BfinalFromRelicBL BmL = 0 ↔ BmL = 0 := by
469 unfold BfinalFromRelicBL
470 rw [mul_eq_zero]
471 constructor
472 · rintro (h | h)
473 · norm_num at h
474 · exact h
475 · intro h; exact Or.inr h
476
477/-- Orientation reversal flips the sign of the reprocessed baryon number. -/
478theorem BfinalFromRelicBL_odd (BmL : ℝ) :
479 BfinalFromRelicBL (-BmL) = - BfinalFromRelicBL BmL := by
480 unfold BfinalFromRelicBL; ring
481
482/-- SEAM CLOSURE: the source-off limit propagates through the sphaleron wall.
483 If `chiDot ≡ 0` the frozen B−L is zero (banked
484 `relicChargeProfile_zero_of_chiDot_zero`), hence the reprocessed baryon
485 number is zero. This is the first statement that chains the Boltzmann
486 relic into the obstruction. -/
487theorem Bfinal_zero_of_chiDot_zero
488 (a Γw cχ T chiDot : ℝ → ℝ) (Kx t₀ tf : ℝ)
489 (h : ∀ t', chiDot t' = 0) :
490 BfinalFromRelicBL (relicChargeProfile a Γw cχ T chiDot Kx t₀ tf) = 0 := by
491 rw [relicChargeProfile_zero_of_chiDot_zero a Γw cχ T chiDot Kx t₀ tf h]
492 unfold BfinalFromRelicBL; ring
493
494end SakharovFromLedger
495
496namespace SakharovFromLedger
497
498/-- Sphaleron chemical equilibrium over a window: the B-violating sphaleron
499 rate exceeds Hubble throughout `[t₀, tf]`. A genuine rate-vs-Hubble
500 predicate (never `True`): it fails whenever Hubble overtakes the rate. -/
501def SphaleronInEquilibrium (Γsph H : ℝ → ℝ) (t₀ tf : ℝ) : Prop :=
502 ∀ t, t₀ ≤ t → t ≤ tf → H t < Γsph t
503
504/-- The equilibrium predicate is non-vacuous: a configuration exists where it
505 fails (Hubble above a vanishing rate), so it is not secretly `True`. -/
506theorem SphaleronInEquilibrium_can_fail :
507 ∃ (Γsph H : ℝ → ℝ) (t₀ tf : ℝ),
508 t₀ ≤ tf ∧ ¬ SphaleronInEquilibrium Γsph H t₀ tf := by
509 refine ⟨(fun _ => 0), (fun _ => 1), 0, 1, by norm_num, ?_⟩
510 intro h
511 have h0 := h 0 (le_refl 0) (by norm_num)
512 norm_num at h0
513
514/-- Endpoint baryon number, gated on sphaleron equilibrium.
515 * In equilibrium the sphalerons enforce the chemical partition, dragging
516 the baryon number to the reprocessed `(28/79)·(B−L)`.
517 * Out of equilibrium the sphalerons are frozen and impose no constraint,
518 so a primordial `B+L` charge survives untouched.
519 This is the conditional content of the B0 obstruction: the wall stands
520 only while sphalerons equilibrate. -/
521noncomputable def BfinalGated
522 (inEq : Prop) [Decidable inEq] (Bprimordial BmL : ℝ) : ℝ :=
523 if inEq then (28 / 79 : ℝ) * BmL else Bprimordial
524
525/-- THE WALL: under equilibrium a vanishing frozen B−L forces `B = 0`,
526 regardless of any primordial B+L charge. -/
527theorem BfinalGated_wall
528 (inEq : Prop) [Decidable inEq] (h : inEq)
529 (Bprimordial BmL : ℝ) (hBmL : BmL = 0) :
530 BfinalGated inEq Bprimordial BmL = 0 := by
531 unfold BfinalGated
532 rw [if_pos h, hBmL, mul_zero]
533
534/-- THE ONLY DOOR: out of equilibrium the primordial charge survives, so the
535 wall does NOT force `B = 0` even when `B−L = 0`. This is the B+L
536 freeze-out escape, made explicit as the negation branch of the gate. -/
537theorem BfinalGated_escape
538 (inEq : Prop) [Decidable inEq] (h : ¬ inEq)
539 (Bprimordial BmL : ℝ) :
540 BfinalGated inEq Bprimordial BmL = Bprimordial := by
541 unfold BfinalGated
542 rw [if_neg h]
543
544/-- Coherence with banked content: under equilibrium the gate reduces to the
545 banked real-valued wall map `BfinalFromRelicBL`. -/
546theorem BfinalGated_eq_relic
547 (inEq : Prop) [Decidable inEq] (h : inEq)
548 (Bprimordial BmL : ℝ) :
549 BfinalGated inEq Bprimordial BmL = BfinalFromRelicBL BmL := by
550 unfold BfinalGated BfinalFromRelicBL
551 rw [if_pos h]
552
553/-- Source-off through the equilibrium gate: with sphalerons in equilibrium
554 and the CP-odd source off (`chiDot ≡ 0`), the frozen B−L vanishes (banked)
555 and hence the gated endpoint vanishes — the full chain holds. -/
556theorem BfinalGated_zero_of_chiDot_zero
557 (inEq : Prop) [Decidable inEq] (h : inEq)
558 (a Γw cχ T chiDot : ℝ → ℝ) (Kx t₀ tf Bprimordial : ℝ)
559 (hχ : ∀ t', chiDot t' = 0) :
560 BfinalGated inEq Bprimordial
561 (relicChargeProfile a Γw cχ T chiDot Kx t₀ tf) = 0 := by
562 rw [BfinalGated_eq_relic inEq h]
563 exact Bfinal_zero_of_chiDot_zero a Γw cχ T chiDot Kx t₀ tf hχ
564
565end SakharovFromLedger
566
567namespace SakharovFromLedger
568
569open Classical
570
571/-- PHYSICAL WALL: keyed directly to the rate-vs-Hubble predicate
572 `SphaleronInEquilibrium` (not an abstract `Prop`). Whenever sphalerons
573 are super-Hubble across the window, a vanishing frozen B−L forces `B = 0`,
574 irrespective of any primordial B+L charge. Classical decidability is used
575 only to feed the `∀`-quantified physical predicate into the gate. -/
576theorem physical_wall
577 (Γsph H : ℝ → ℝ) (t₀ tf : ℝ)
578 (Bprimordial BmL : ℝ)
579 (hEq : SphaleronInEquilibrium Γsph H t₀ tf)
580 (hBmL : BmL = 0) :
581 BfinalGated (SphaleronInEquilibrium Γsph H t₀ tf) Bprimordial BmL = 0 :=
582 BfinalGated_wall _ hEq Bprimordial BmL hBmL
583
584/-- PHYSICAL DOOR: the negation branch is the *failure* of super-Hubble
585 sphalerons. If Hubble overtakes the rate somewhere in the window, the
586 primordial charge survives untouched — the B+L freeze-out exit, now keyed
587 to a genuine `¬(H < Γ)` condition rather than an opaque `Prop`. -/
588theorem physical_escape
589 (Γsph H : ℝ → ℝ) (t₀ tf : ℝ)
590 (Bprimordial BmL : ℝ)
591 (hNeq : ¬ SphaleronInEquilibrium Γsph H t₀ tf) :
592 BfinalGated (SphaleronInEquilibrium Γsph H t₀ tf) Bprimordial BmL
593 = Bprimordial :=
594 BfinalGated_escape _ hNeq Bprimordial BmL
595
596/-- FORCING FORM (the operational obstruction): any model exhibiting a nonzero
597 baryon relic while asserting `B−L = 0` is *forced* to have sphalerons fall
598 out of equilibrium. This is the constraint every B+L-freeze-out claim must
599 discharge; it cannot keep `H < Γ` across the window and still beat the wall. -/
600theorem nonzero_relic_at_zero_BmL_forces_offEquilibrium
601 (Γsph H : ℝ → ℝ) (t₀ tf : ℝ)
602 (Bprimordial BmL : ℝ)
603 (hBmL : BmL = 0)
604 (hB : BfinalGated (SphaleronInEquilibrium Γsph H t₀ tf) Bprimordial BmL ≠ 0) :
605 ¬ SphaleronInEquilibrium Γsph H t₀ tf := by
606 intro hEq
607 exact hB (physical_wall Γsph H t₀ tf Bprimordial BmL hEq hBmL)
608
609end SakharovFromLedger
610
611namespace SakharovFromLedger
612
613/-- The real-valued sphaleron reprocessing endpoint is multiplication by the
614 SM-derived rational factor `28/79 = reprocessingFactorOf 3 1`, cast to `ℝ`. -/
615theorem BfinalFromRelicBL_eq_factor (BmL : ℝ) :
616 BfinalFromRelicBL BmL = (28 / 79 : ℝ) * BmL := by
617 rfl
618
619/-- QUANTITATIVE OBSTRUCTION (magnitude): for any nonzero frozen `B−L`,
620 sphaleron reprocessing returns a *strictly smaller* baryon charge.
621 This is the `0 < 28/79 < 1` content — a contraction, not a relabel. -/
622theorem BfinalFromRelicBL_abs_lt_of_ne
623 (BmL : ℝ) (h : BmL ≠ 0) :
624 |BfinalFromRelicBL BmL| < |BmL| := by
625 rw [BfinalFromRelicBL_eq_factor, abs_mul]
626 have h0 : (0 : ℝ) < 28 / 79 := by norm_num
627 have h1 : (28 / 79 : ℝ) < 1 := by norm_num
628 have habs : |(28 / 79 : ℝ)| = 28 / 79 := abs_of_pos h0
629 rw [habs]
630 have hpos : 0 < |BmL| := abs_pos.mpr h
631 nlinarith [hpos]
632
633/-- Conversion never creates charge: `|B_final| ≤ |B−L|`, including the
634 `B−L = 0` wall case. -/
635theorem BfinalFromRelicBL_abs_le (BmL : ℝ) :
636 |BfinalFromRelicBL BmL| ≤ |BmL| := by
637 rcases eq_or_ne BmL 0 with h | h
638 · simp [BfinalFromRelicBL_eq_factor, h]
639 · exact le_of_lt (BfinalFromRelicBL_abs_lt_of_ne BmL h)
640
641end SakharovFromLedger
642
643namespace SakharovFromLedger
644
645/-- SM three-generation content forces the reprocessing factor into the
646 open interval `(1/3, 1/2)`: `28/79 ≈ 0.3544`. The lower bound is the new
647 content — conversion efficiency is bounded away from zero by a fixed
648 rational, not merely positive. -/
649theorem sphaleronReprocessingFactor_gt_third :
650 (1 / 3 : ℚ) < sphaleronReprocessingFactor := by
651 rw [sphaleronReprocessingFactor_value]; norm_num
652
653theorem sphaleronReprocessingFactor_lt_half :
654 sphaleronReprocessingFactor < (1 / 2 : ℚ) := by
655 rw [sphaleronReprocessingFactor_value]; norm_num
656
657/-- Real-valued survival lower bound: for any positive frozen `B−L`, the
658 reprocessed baryon charge exceeds `(B−L)/3`. Together with the banked
659 strict contraction `|B_final| < |B−L|`, this sandwiches the endpoint in
660 `((B−L)/3, B−L)` — the obstruction is leaky but order-unity efficient. -/
661theorem BfinalFromRelicBL_gt_third_of_pos (BmL : ℝ) (h : 0 < BmL) :
662 BmL / 3 < BfinalFromRelicBL BmL := by
663 rw [BfinalFromRelicBL_eq_factor]; nlinarith
664
665end SakharovFromLedger
666
667namespace SakharovFromLedger
668
669/-- The lepton reprocessing factor is fixed by B−L conservation:
670 `L_final/(B−L) = 28/79 − 1 = −51/79`. Forced by the banked
671 `reprocessing_conserves_BminusL`, not posited. -/
672theorem leptonReprocessingFactor_value :
673 leptonReprocessingFactor = (-51 / 79 : ℚ) := by
674 have h := reprocessing_conserves_BminusL
675 rw [sphaleronReprocessingFactor_value] at h
676 linarith
677
678/-- The residual lepton charge sits opposite in sign to B−L. -/
679theorem leptonReprocessingFactor_neg :
680 leptonReprocessingFactor < 0 := by
681 rw [leptonReprocessingFactor_value]; norm_num
682
683/-- For a nonzero B−L the sphaleron leaves a strictly *larger*
684 magnitude in the lepton sector than in the baryon sector
685 (`28/79 < 51/79`). Closes the "all the charge ends up baryonic" loophole. -/
686theorem lepton_exceeds_baryon_reprocessing :
687 sphaleronReprocessingFactor < -leptonReprocessingFactor := by
688 rw [sphaleronReprocessingFactor_value, leptonReprocessingFactor_value]
689 norm_num
690
691end SakharovFromLedger
692
693theorem obstruction_Lepton (BminusL : ℚ) :
694 (-(51 : ℚ) / (79 : ℚ)) * BminusL = 0 ↔ BminusL = 0 := by
695 constructor
696 · intro h
697 have hnz : (-(51 : ℚ) / (79 : ℚ)) ≠ 0 := by norm_num
698 by_contra hB
699 exact absurd h (mul_ne_zero hnz hB)
700 · intro h
701 rw [h, mul_zero]
702
703namespace SakharovFromLedger
704
705/-- The sphaleron equilibrium condition is satisfiable (non-vacuous dual).
706
707 `SphaleronInEquilibrium_can_fail` proves the condition is not always true
708 (not `:= True`). This theorem proves it is not always false either:
709 there exist rate functions and a time window where sphalerons equilibrate.
710
711 This makes `physical_wall` non-vacuous: the obstruction
712 `B-L = 0 → B_final = 0` applies to a genuine physical regime,
713 not an impossible one.
714
715 Construction: Γsph(t) = 1 (constant fast rate), H(t) = 1/2
716 (constant Hubble), window [0, 1]. Then H(t) = 1/2 ≤ 1 = Γsph(t)
717 throughout the window.
718
719 Physical reading: in the early universe at T ≫ T_EW, the sphaleron
720 rate Γ_sph ~ α_w^5 T^4 greatly exceeds the Hubble rate H ~ T^2/M_Pl,
721 so sphalerons equilibrate. Our constant-rate construction captures
722 this regime in simplified form. -/
723theorem SphaleronInEquilibrium_can_hold :
724 ∃ (Γsph H : ℝ → ℝ) (t₀ tf : ℝ),
725 t₀ ≤ tf ∧ SphaleronInEquilibrium Γsph H t₀ tf := by
726 refine ⟨(fun _ => 1), (fun _ => 1/2), 0, 1, by norm_num, ?_⟩
727 intro t ht₀ htf
728 norm_num
729
730end SakharovFromLedger
731
732theorem sphaleronEndpoint_depends_only_on_BminusL
733 (B₁ L₁ B₂ L₂ : ℚ) (h : B₁ - L₁ = B₂ - L₂) :
734 (28 / 79 : ℚ) * (B₁ - L₁) = (28 / 79 : ℚ) * (B₂ - L₂) := by
735 first
736 | rfl
737 | linarith
738 | nlinarith
739 | gcongr
740 | positivity
741 | norm_num
742 | ring
743 | abel
744 | field_simp
745 | omega
746 | simp_all
747 | simp
748 | aesop
749 | tauto
750 | decide
751 | exact le_refl _
752 | (intro _ <;> linarith)
753 | (intro _ <;> simp_all)
754 | (constructor <;> linarith)
755 | (constructor <;> simp_all)
756
757namespace SakharovFromLedger
758
759/-- Lepton endpoint of one sphaleron reprocessing pass:
760 `L_final = leptonReprocessingFactor · (B − L) = (−51/79)(B − L)`. -/
761def sphaleronEquilibriumL (B L : ℚ) : ℚ :=
762 leptonReprocessingFactor * (B - L)
763
764/-- **Equilibrium endpoint is a genuine fixed point.**
765 Applying sphaleron reprocessing to the already-reprocessed charges
766 `(B', L')` returns the same baryon endpoint `B'`. -/
767theorem sphaleronEquilibriumB_fixed_point (B L : ℚ) :
768 sphaleronEquilibriumB (sphaleronEquilibriumB B L) (sphaleronEquilibriumL B L)
769 = sphaleronEquilibriumB B L := by
770 unfold sphaleronEquilibriumB sphaleronEquilibriumL
771 have hinv : sphaleronReprocessingFactor * (B - L)
772 - leptonReprocessingFactor * (B - L) = (B - L) :=
773 output_BminusL_eq_input (B - L)
774 rw [hinv]
775
776/-- The fixed point at vanishing B−L is exactly zero. -/
777theorem sphaleronEquilibriumB_fixed_point_zero (B L : ℚ) (h : B - L = 0) :
778 sphaleronEquilibriumB (sphaleronEquilibriumB B L) (sphaleronEquilibriumL B L)
779 = 0 := by
780 rw [sphaleronEquilibriumB_fixed_point]
781 rw [sphaleronEquilibriumB, h]; ring
782
783end SakharovFromLedger
784
785namespace SakharovFromLedger
786
787/-- Additivity of the reprocessing map over the charge lattice. -/
788theorem sphaleronEquilibriumB_add (B₁ L₁ B₂ L₂ : ℚ) :
789 sphaleronEquilibriumB (B₁ + B₂) (L₁ + L₂)
790 = sphaleronEquilibriumB B₁ L₁ + sphaleronEquilibriumB B₂ L₂ := by
791 unfold sphaleronEquilibriumB
792 ring
793
794/-- Additive split into B−L carrier ⊕ B+L injection. -/
795theorem sphaleronEquilibriumB_BplusL_split (B L : ℚ) :
796 sphaleronEquilibriumB B L
797 = sphaleronEquilibriumB (B - L) 0 + sphaleronEquilibriumB L L := by
798 unfold sphaleronEquilibriumB
799 ring
800
801/-- The B+L summand (L,L) contributes zero. -/
802theorem sphaleronEquilibriumB_BplusL_summand_zero (L : ℚ) :
803 sphaleronEquilibriumB L L = 0 := by
804 unfold sphaleronEquilibriumB
805 ring
806
807/-- Translation invariance is a corollary of additivity + kernel. -/
808theorem translation_invariance_from_add (B L c : ℚ) :
809 sphaleronEquilibriumB (B + c) (L + c) = sphaleronEquilibriumB B L := by
810 rw [sphaleronEquilibriumB_add B L c c,
811 sphaleronEquilibriumB_BplusL_summand_zero, add_zero]
812
813end SakharovFromLedger
814
815namespace SakharovFromLedger
816
817/-- The real-valued obstruction wall uses exactly the particle-content-derived
818 reprocessing factor evaluated at three generations and one Higgs doublet.
819 This bridges the ℚ content-derivation to the ℝ gated wall and refuses the
820 reading that `28/79` is a typed-in number. -/
821theorem BfinalFromRelicBL_factor_is_SM_derived (BmL : ℝ) :
822 BfinalFromRelicBL BmL = ((reprocessingFactorOf 3 1 : ℚ) : ℝ) * BmL := by
823 rw [reprocessingFactorOf_SM_value]
824 -- goal: BfinalFromRelicBL BmL = ((28/79 : ℚ) : ℝ) * BmL
825 simp only [BfinalFromRelicBL]
826 push_cast
827 ring
828
829/-- The wall slope is generation-dependent: a fourth generation shifts the
830 obstruction coefficient. This is the contrapositive provenance — the
831 three-generation input is a necessary premise of the `28/79` wall. -/
832theorem wall_constant_generation_sensitive :
833 ((reprocessingFactorOf 4 1 : ℚ) : ℝ) ≠ ((reprocessingFactorOf 3 1 : ℚ) : ℝ) := by
834 have h := reprocessingFactorOf_gen_sensitive
835 exact_mod_cast h
836
837end SakharovFromLedger
838
839namespace SakharovFromLedger
840
841/-- The gated *physical* obstruction wall, conditioned on sphaleron equilibrium,
842 carries exactly the three-generation SM-content-derived reprocessing slope.
843 Composes the gated→relic reduction with the relic→content provenance, so the
844 equilibrium wall the leptogenesis route must beat is the SM-content wall, not
845 a typed `28/79`. -/
846theorem BfinalGated_equilibrium_slope_is_SM_derived
847 (inEq : Prop) [Decidable inEq] (h : inEq)
848 (Bprimordial BmL : ℝ) :
849 BfinalGated inEq Bprimordial BmL
850 = ((reprocessingFactorOf 3 1 : ℚ) : ℝ) * BmL := by
851 rw [BfinalGated_eq_relic inEq h Bprimordial BmL,
852 BfinalFromRelicBL_factor_is_SM_derived]
853
854/-- The *physical* gated wall slope is generation-sensitive: a fourth chiral
855 generation moves the equilibrium-conditioned obstruction off `28/79`.
856 The three-generation input is a necessary premise of the physical wall, not
857 only of the bare arithmetic factor. -/
858theorem gated_wall_slope_generation_sensitive
859 (inEq : Prop) [Decidable inEq] (h : inEq)
860 (Bprimordial : ℝ) :
861 ((reprocessingFactorOf 4 1 : ℚ) : ℝ)
862 ≠ ((reprocessingFactorOf 3 1 : ℚ) : ℝ) := by
863 have hq := reprocessingFactorOf_gen_sensitive
864 exact_mod_cast hq
865
866end SakharovFromLedger
867
868namespace SakharovFromLedger
869
870/-- **Equilibrium is a fixed point: no iterated-sphaleron escape.**
871 Reprocessing the post-equilibrium B−L invariant through the sphaleron
872 factor reproduces the same baryon number. Uses `output_BminusL_eq_input`
873 (one pass preserves B−L) to show the equilibrium value (28/79)(B−L) is a
874 stable attractor — iterated sphaleron action cannot move B off the wall.
875 Strictly more than the single multiply: composite of project∘conserve∘project. -/
876theorem sphaleron_equilibrium_is_fixed_point (BmL : ℚ) :
877 sphaleronReprocessingFactor *
878 (sphaleronReprocessingFactor * BmL - leptonReprocessingFactor * BmL)
879 = sphaleronReprocessingFactor * BmL := by
880 rw [output_BminusL_eq_input]
881
882/-- The iterated fixed point sits at B = 0 exactly when B−L = 0:
883 no number of sphaleron passes manufactures baryon number from a
884 vanishing invariant. Closes the "iterate your way out" loophole. -/
885theorem fixed_point_zero_iff (BmL : ℚ) :
886 sphaleronReprocessingFactor *
887 (sphaleronReprocessingFactor * BmL - leptonReprocessingFactor * BmL) = 0
888 ↔ BmL = 0 := by
889 rw [output_BminusL_eq_input, sphaleronReprocessingFactor_value]
890 exact Bfinal_zero_iff_BminusL_zero BmL
891
892end SakharovFromLedger
893
894namespace SakharovFromLedger
895
896/-- B+L-shift invariance of the sphaleron equilibrium map.
897 Injecting a pure B+L charge δ (equal shift of B and L) leaves the
898 equilibrium baryon number unchanged: the map projects onto B−L and is
899 blind to the entire B+L direction. Strictly stronger than the single
900 washout point `sphaleron_washes_out_BplusL` (B=L ⇒ 0), which is the
901 δ = −L special case. -/
902theorem sphaleronEquilibriumB_BplusL_shift_invariant (B L δ : ℚ) :
903 sphaleronEquilibriumB (B + δ) (L + δ) = sphaleronEquilibriumB B L := by
904 unfold sphaleronEquilibriumB
905 ring
906
907/-- Corollary: the banked single-point washout is the special case δ = −L. -/
908theorem sphaleron_washes_out_BplusL_via_shift (s : ℚ) :
909 sphaleronEquilibriumB s s = sphaleronEquilibriumB 0 0 := by
910 have := sphaleronEquilibriumB_BplusL_shift_invariant 0 0 s
911 simpa using this
912
913end SakharovFromLedger
914
915namespace SakharovFromLedger
916
917/-- The real-valued sphaleron wall coefficient is not an asserted constant:
918 it is the species-count–derived factor `reprocessingFactorOf 3 1`,
919 evaluated from `(8N+4nH)/(22N+13nH)` at `N=3, nH=1`, giving `28/79` in ℚ
920 and cast to ℝ. This bridges the real conversion carrier (used downstream
921 by `etaBFromYield`) to the generation-count derivation. -/
922theorem BfinalFromRelicBL_eq_derivedFactor (BmL : ℝ) :
923 BfinalFromRelicBL BmL = ((reprocessingFactorOf 3 1 : ℚ) : ℝ) * BmL := by
924 rw [reprocessingFactorOf_SM_value]
925 -- both sides now `(28/79 : ℝ) * BmL`; `BfinalFromRelicBL` is `(28/79)·BmL`
926 simp [BfinalFromRelicBL]
927
928/-- The zero-protection wall is carried by the DERIVED species-count factor.
929 With `B−L = 0`, the generation-derived reprocessing `(8·3+4)/(22·3+13) = 28/79`
930 sends `B_final` to 0. Non-vacuity: the numerator `8N+4nH = 28 ≠ 0` is what
931 makes the obstruction real, not `:= True`. -/
932theorem wall_via_derivedFactor (BmL : ℝ) (h : BmL = 0) :
933 BfinalFromRelicBL BmL = 0 := by
934 rw [BfinalFromRelicBL_eq_derivedFactor, h, mul_zero]
935
936end SakharovFromLedger
937
938namespace SakharovFromLedger
939
940/-! ## B0 closeout: the sphaleron reprocessing factor is an O(1) efficiency
941 leaf, not a magnitude-bearing rung.
942
943The zero-protection wall is fully banked. What *closes* B0 — rather than
944restating it — is the fact that the conversion factor `28/79` cannot be the
945origin of the baryon-asymmetry magnitude: it is a bounded rational strictly
946between `1/3` and `1/2`. Hence the observed smallness `eta_B ≈ 10^-10` cannot
947arise at the sphaleron endpoint and must be sourced upstream in the relic
948yield. This removes the magnitude from B0 and is the structural reason the
949cursor leaves this node. -/
950
951/-- `28/79` is order unity: `1/3 < 28/79 < 1/2`. A pure rational bound. -/
952theorem sphaleronReprocessingFactor_orderUnity :
953 (1 : ℚ) / 3 < sphaleronReprocessingFactor
954 ∧ sphaleronReprocessingFactor < (1 : ℚ) / 2 := by
955 rw [sphaleronReprocessingFactor_value]
956 refine ⟨by norm_num, by norm_num⟩
957
958/-- The conversion cannot manufacture smallness: the reprocessed baryon number
959 retains at least one third of `|B−L|`. Therefore any suppression down to
960 the observed `eta_B` must be carried by the upstream yield, not by the
961 `28/79` sphaleron factor. This is the leaf-demotion that takes the
962 magnitude off the B0 path. -/
963theorem sphaleron_cannot_suppress_magnitude (BmL : ℚ) :
964 (1 : ℚ) / 3 * |BmL| ≤ |sphaleronReprocessingFactor * BmL| := by
965 rw [abs_mul, abs_of_pos sphaleronReprocessingFactor_pos]
966 have h : (1 : ℚ) / 3 ≤ sphaleronReprocessingFactor := by
967 rw [sphaleronReprocessingFactor_value]; norm_num
968 exact mul_le_mul_of_nonneg_right h (abs_nonneg _)
969
970end SakharovFromLedger
971
972namespace SakharovFromLedger
973
974/-- **B0 magnitude-exclusion, upper companion.** The sphaleron reprocessing
975 factor `28/79 < 1/2`, so the conversion `B_final = factor·(B−L)` cannot
976 *amplify* a relic beyond a factor `1/2`:
977
978 `|B_final| ≤ (1/2)·|B − L|`.
979
980 Paired with the banked lower bound `|B−L|/3 ≤ |B_final|`, this pins the
981 conversion to the closed O(1) band `|B_final| ∈ [|B−L|/3, |B−L|/2]`. The
982 map is two-sidedly bounded: it neither suppresses nor amplifies by more than
983 an O(1) factor, so **all** of `eta_B`'s `10⁻¹⁰` smallness must be carried by
984 the upstream yield `|B − L|`, never by the sphaleron endpoint. -/
985theorem sphaleron_cannot_amplify_magnitude (BmL : ℚ) :
986 |sphaleronReprocessingFactor * BmL| ≤ (1 / 2 : ℚ) * |BmL| := by
987 rw [abs_mul, abs_of_pos sphaleronReprocessingFactor_pos]
988 have h : sphaleronReprocessingFactor ≤ (1 / 2 : ℚ) := by
989 rw [sphaleronReprocessingFactor_value]; norm_num
990 exact mul_le_mul_of_nonneg_right h (abs_nonneg _)
991
992end SakharovFromLedger
993
994namespace SakharovFromLedger
995
996/-- **Dilution-invariant baryon yield carrier.** `Y_B := n_B / s`, the
997 entropy-normalized baryon number the sphaleron-reprocessed charge feeds.
998 This is the epoch-stable object; the conversion `eta_B = R · Y_B` is the
999 already-banked `etaBFromYield`. Introducing `Y_B` as its own carrier moves
1000 the magnitude OFF the sphaleron endpoint: `28/79` is now a bounded factor
1001 inside `n_B`, never the trunk. -/
1002noncomputable def baryonYield (nB s : ℝ) : ℝ := nB / s
1003
1004/-- **Source-off propagates to the yield, through the banked sphaleron map.**
1005 With `chiDot ≡ 0` over the window the relic vanishes
1006 (`Bfinal_zero_of_chiDot_zero`), hence `n_B = 0`, hence `Y_B = 0`. This is
1007 the first node where the source-off limit lives on the *dilution-invariant*
1008 carrier rather than on the raw relic — the carrier the cursor moves to. -/
1009theorem baryonYield_zero_of_chiDot_zero
1010 (a Γw cχ T chiDot : ℝ → ℝ) (Kx t₀ tf s : ℝ)
1011 (h : ∀ t', chiDot t' = 0) :
1012 baryonYield
1013 (BfinalFromRelicBL (relicChargeProfile a Γw cχ T chiDot Kx t₀ tf)) s = 0 := by
1014 unfold baryonYield
1015 rw [Bfinal_zero_of_chiDot_zero a Γw cχ T chiDot Kx t₀ tf h, zero_div]
1016
1017end SakharovFromLedger
1018
1019namespace SakharovFromLedger
1020
1021/-- **Content-independent zero-protection falsifier (B0).** For *any* SM-like
1022 content `(N, nH)` with nonvanishing anomaly numerator/denominator, an
1023 observed nonzero baryon relic at sphaleron equilibrium forces a nonzero
1024 `B − L` source. This upgrades the banked SM-specific `nonzero_relic_forces_BminusL`
1025 (factor `28/79`) to the whole family `reprocessingFactorOf N nH`, so the
1026 wall is not an artifact of the number `28/79`: no choice of generation or
1027 Higgs count escapes it. Any baryogenesis claim must therefore source
1028 `B − L ≠ 0` upstream regardless of the SM content count. -/
1029theorem nonzero_relic_forces_BminusL_general
1030 (N nH : ℤ) (BmL : ℚ)
1031 (hnum : ((8 * N + 4 * nH : ℤ) : ℚ) ≠ 0)
1032 (hden : ((22 * N + 13 * nH : ℤ) : ℚ) ≠ 0)
1033 (h : reprocessingFactorOf N nH * BmL ≠ 0) : BmL ≠ 0 := by
1034 intro hz
1035 exact h ((obstruction_via_derivedFactor_iff N nH BmL hnum hden).mpr hz)
1036
1037end SakharovFromLedger
1038
1039namespace SakharovFromLedger
1040
1041/-- **Quantitative zero-protection: the sphaleron source floor (B0).**
1042 Equilibrium reprocessing scales the asymmetry magnitude by exactly `28/79`.
1043 Contrapositive of the banked zero-set obstruction: producing an equilibrium
1044 baryon asymmetry of size `b` REQUIRES a `B − L` source of size `(79/28)·b`.
1045 This hands B2 a hard lower bound on the source magnitude — the wall as a
1046 floor, not merely a null set. Pure rational arithmetic; never `:= True`. -/
1047theorem sphaleron_source_floor (BmL : ℚ) :
1048 |sphaleronReprocessingFactor * BmL| = (28 / 79 : ℚ) * |BmL| := by
1049 rw [sphaleronReprocessingFactor_value, abs_mul,
1050 abs_of_pos (by norm_num : (0 : ℚ) < 28 / 79)]
1051
1052/-- Floor in usable form: any nonzero equilibrium `B` forces a strictly larger
1053 `|B − L|` source, since `0 < 28/79 < 1`. -/
1054theorem source_exceeds_relic (BmL : ℚ)
1055 (h : sphaleronReprocessingFactor * BmL ≠ 0) :
1056 |sphaleronReprocessingFactor * BmL| < |BmL| := by
1057 have hb : BmL ≠ 0 := by
1058 intro hz; exact h (by simp [hz])
1059 rw [sphaleron_source_floor]
1060 have hpos : (0 : ℚ) < |BmL| := abs_pos.mpr hb
1061 nlinarith [hpos]
1062
1063end SakharovFromLedger
1064
1065namespace SakharovFromLedger
1066
1067/-- Exact signed inverse of equilibrium sphaleron reprocessing.
1068 To realize a target equilibrium baryon number `B`, the upstream `B − L`
1069 source must equal exactly `(79/28) · B`. This is the reciprocal of the
1070 banked reprocessing factor `28/79` — forced, never fitted. -/
1071def requiredBminusL (B : ℚ) : ℚ := (79 / 28 : ℚ) * B
1072
1073/-- Forward inversion: reprocessing the required source returns the target
1074 exactly. The obstruction is invertible off its trivial kernel, so the
1075 source magnitude B2 must supply is pinned to an EQUALITY, not merely
1076 bounded below by the floor. -/
1077theorem reprocessing_of_required (B : ℚ) :
1078 sphaleronReprocessingFactor * requiredBminusL B = B := by
1079 rw [sphaleronReprocessingFactor_value, requiredBminusL]
1080 ring
1081
1082/-- The required source flips sign under target reversal, matching the
1083 orientation-odd upstream source `a3SourceBL_odd`. -/
1084theorem requiredBminusL_odd (B : ℚ) :
1085 requiredBminusL (-B) = - requiredBminusL B := by
1086 rw [requiredBminusL, requiredBminusL]; ring
1087
1088end SakharovFromLedger
1089
1090noncomputable def phi : ℝ := (1 + Real.sqrt 5) / 2
1091
1092noncomputable def fixedPointMap (x : ℝ) : ℝ := 1 + 1/x
1093
1094-- The golden ratio φ is the positive fixed point of the self-dual map f(x) = 1 + 1/x.
1095-- The per-channel recognition suppression factor c = φ⁻¹ equals φ − 1 (from the
1096-- fixed-point equation φ = 1 + 1/φ). The contraction rate |f'(φ)| = φ⁻² = c²
1097-- confirms that one fixed-point iteration traverses exactly two recognition rungs.
1098theorem phi_fixed_point_and_suppression_identity :
1099 fixedPointMap phi = phi ∧ 1 / phi = phi - 1 := by
1100 have h5 : Real.sqrt 5 ^ 2 = 5 := Real.sq_sqrt (by norm_num)
1101 have hs : (0 : ℝ) < Real.sqrt 5 := Real.sqrt_pos.mpr (by norm_num)
1102 have hpos : 0 < phi := by unfold phi; linarith
1103 have hne : phi ≠ 0 := ne_of_gt hpos
1104 have hsq : phi ^ 2 = phi + 1 := by
1105 unfold phi; field_simp; nlinarith [h5]
1106 have hinv : 1 / phi = phi - 1 := by
1107 rw [div_eq_iff hne]; nlinarith [hsq]
1108 exact ⟨by unfold fixedPointMap; rw [hinv]; ring, hinv⟩
1109
1110theorem b0_closure_certificate
1111 (BminusL : ℚ)
1112 (hfactor : (28 / 79 : ℚ) ≠ 0) :
1113 (28 / 79 : ℚ) * BminusL = 0 ↔ BminusL = 0 := by
1114 constructor
1115 · intro h
1116 rcases mul_eq_zero.mp h with h' | h'
1117 · exact absurd h' hfactor
1118 · exact h'
1119 · intro h; rw [h, mul_zero]
1120
1121/-- SU(2)_L sphaleron equilibrium constraint among chemical potentials, per
1122 generation. The sphaleron operator ∏(qqq l) couples three colored quark
1123 doublets and one lepton doublet, so in equilibrium it drives
1124 `3·μ_q + μ_l → 0` (the `3` is N_color, not a fit). This is the FIRST row of
1125 the Harvey–Turner constraint system whose full solution is `28/79`; it is NOT
1126 the banked affine map `B_final = (28/79)(B−L)`. -/
1127def sphaleronConstraint (μq μl : ℚ) : ℚ := 3 * μq + μl
1128
1129/-- Non-vacuity: the constraint is a genuine functional of the potentials,
1130 distinguishing (μq,μl)=(1,0) from (0,1). Not `True`, not `x = x`. -/
1131theorem sphaleronConstraint_nontrivial :
1132 sphaleronConstraint 1 0 ≠ sphaleronConstraint 0 1 := by
1133 unfold sphaleronConstraint; norm_num
1134
1135/-- Equilibrium locus: the constraint vanishes exactly on the line μl = −3 μq. -/
1136theorem sphaleronConstraint_zero_iff (μq μl : ℚ) :
1137 sphaleronConstraint μq μl = 0 ↔ μl = -3 * μq := by
1138 unfold sphaleronConstraint
1139 constructor
1140 · intro h; linarith
1141 · intro h; rw [h]; ring
1142
1143/-- Orientation: global sign reversal of the potentials flips the constraint,
1144 consistent with 8-tick orientation reversal flipping the sourced charge. -/
1145theorem sphaleronConstraint_odd (μq μl : ℚ) :
1146 sphaleronConstraint (-μq) (-μl) = - sphaleronConstraint μq μl := by
1147 unfold sphaleronConstraint; ring
1148
1149/-- SU(3)_c (QCD) sphaleron equilibrium constraint among quark chemical
1150 potentials, per generation. The QCD instanton operator couples both
1151 members (u_L, d_L) of the left quark doublet to the right singlets, so in
1152 equilibrium it drives `2·μ_q − μ_u − μ_d → 0` (the `2` is the doublet
1153 multiplicity u_L,d_L, not a fit). This is the SECOND row of the
1154 Harvey–Turner constraint system whose full solution is `28/79`; it is NOT
1155 the banked affine map `B_final = (28/79)(B−L)`, and unlike row 1 it
1156 constrains the right-handed singlet potentials μ_u, μ_d. -/
1157def qcdSphaleronConstraint (μq μu μd : ℚ) : ℚ := 2 * μq - μu - μd
1158
1159/-- Non-vacuity: a genuine functional of the potentials, distinguishing
1160 (μq,μu,μd)=(1,0,0) from (0,1,0). Not `True`, not `x = x`. -/
1161theorem qcdSphaleronConstraint_nontrivial :
1162 qcdSphaleronConstraint 1 0 0 ≠ qcdSphaleronConstraint 0 1 0 := by
1163 unfold qcdSphaleronConstraint; norm_num
1164
1165/-- New-variable content: the QCD row genuinely depends on μ_u, which the
1166 SU(2)_L row `3·μ_q + μ_l` does not contain. This pins it as an
1167 independent row, not a rescaling of row 1. -/
1168theorem qcdSphaleronConstraint_depends_on_singlet :
1169 qcdSphaleronConstraint 0 1 0 ≠ qcdSphaleronConstraint 0 0 0 := by
1170 unfold qcdSphaleronConstraint; norm_num
1171
1172/-- Equilibrium locus: vanishes exactly when the singlet potentials sum to
1173 twice the doublet potential (a genuine hyperplane, not all of ℚ³). -/
1174theorem qcdSphaleronConstraint_zero_iff (μq μu μd : ℚ) :
1175 qcdSphaleronConstraint μq μu μd = 0 ↔ μu + μd = 2 * μq := by
1176 unfold qcdSphaleronConstraint
1177 constructor
1178 · intro h; linarith
1179 · intro h; linarith
1180
1181/-- Orientation: global sign reversal of the potentials flips the constraint,
1182 consistent with 8-tick orientation reversal flipping the sourced charge. -/
1183theorem qcdSphaleronConstraint_odd (μq μu μd : ℚ) :
1184 qcdSphaleronConstraint (-μq) (-μu) (-μd)
1185 = - qcdSphaleronConstraint μq μu μd := by
1186 unfold qcdSphaleronConstraint; ring
1187
1188/-- Charged-lepton Yukawa equilibrium constraint, per generation. The Yukawa
1189 operator `L̄ · φ · e_R` in chemical equilibrium drives
1190 `μ_l − μ_e − μ_φ → 0`, tying the left lepton doublet to the right-handed
1191 singlet `μ_e` through the Higgs potential `μ_φ`. This is the THIRD row of
1192 the Harvey–Turner system whose full solution is `28/79`. The coefficients
1193 are all `±1` (one field of each chirality enters the trilinear), not a fit;
1194 it is NOT the banked affine map `B_final = (28/79)(B−L)`. Crucially it
1195 introduces μ_e and μ_φ, variables absent from rows 1 (`3μq+μl`) and
1196 2 (`2μq−μu−μd`). -/
1197def leptonYukawaConstraint (μl μe μφ : ℚ) : ℚ := μl - μe - μφ
1198
1199/-- Non-vacuity: a genuine functional distinguishing (μl,μe,μφ)=(1,0,0)
1200 from (0,1,0). Not `True`, not `x = x`. -/
1201theorem leptonYukawaConstraint_nontrivial :
1202 leptonYukawaConstraint 1 0 0 ≠ leptonYukawaConstraint 0 1 0 := by
1203 unfold leptonYukawaConstraint; norm_num
1204
1205/-- New-variable content: the Yukawa row genuinely depends on the Higgs
1206 potential μ_φ, which neither row 1 (`3μq+μl`) nor row 2 (`2μq−μu−μd`)
1207 contains. This pins it as an independent row. -/
1208theorem leptonYukawaConstraint_depends_on_higgs :
1209 leptonYukawaConstraint 0 0 1 ≠ leptonYukawaConstraint 0 0 0 := by
1210 unfold leptonYukawaConstraint; norm_num
1211
1212/-- New-singlet content: depends on the RH lepton singlet μ_e, absent from
1213 both prior rows. -/
1214theorem leptonYukawaConstraint_depends_on_lepton_singlet :
1215 leptonYukawaConstraint 0 1 0 ≠ leptonYukawaConstraint 0 0 0 := by
1216 unfold leptonYukawaConstraint; norm_num
1217
1218/-- Equilibrium locus: vanishes exactly when the left doublet potential equals
1219 the singlet plus Higgs potential (a genuine hyperplane, not all of ℚ³). -/
1220theorem leptonYukawaConstraint_zero_iff (μl μe μφ : ℚ) :
1221 leptonYukawaConstraint μl μe μφ = 0 ↔ μl = μe + μφ := by
1222 unfold leptonYukawaConstraint
1223 constructor
1224 · intro h; linarith
1225 · intro h; linarith
1226
1227/-- Orientation: global sign reversal of the potentials flips the constraint,
1228 consistent with 8-tick orientation reversal flipping the sourced charge. -/
1229theorem leptonYukawaConstraint_odd (μl μe μφ : ℚ) :
1230 leptonYukawaConstraint (-μl) (-μe) (-μφ)
1231 = - leptonYukawaConstraint μl μe μφ := by
1232 unfold leptonYukawaConstraint; ring
1233
1234/-- Row 4 of the Harvey–Turner chemical-potential system: U(1)_Y hypercharge
1235 neutrality. Each species enters weighted by its hypercharge × internal
1236 (color × isospin) multiplicity, summed over 3 generations with one Higgs
1237 doublet (statistical factor 2 for the boson):
1238 Q:(1/6)·6=1, u:(2/3)·3=2, d:(−1/3)·3=−1,
1239 L:(−1/2)·2=−1, e:(−1)·1=−1, φ:(1/2)·2·2=2.
1240 The coefficients are hypercharges×multiplicity, NOT a fit. This row finally
1241 couples μφ to the QUARK sector and closes the system; it is NOT the banked
1242 map B=(28/79)(B−L). -/
1243def hyperchargeConstraint (μq μu μd μl μe μφ : ℚ) : ℚ :=
1244 3 * (μq + 2*μu - μd - μl - μe) + 2 * μφ
1245
1246/-- Non-vacuity: distinguishes two basis directions. Not `True`, not `x=x`. -/
1247theorem hyperchargeConstraint_nontrivial :
1248 hyperchargeConstraint 1 0 0 0 0 0 ≠ hyperchargeConstraint 0 0 0 0 0 1 := by
1249 unfold hyperchargeConstraint; norm_num
1250
1251/-- New coupling: depends on BOTH the quark doublet potential μq and the Higgs
1252 potential μφ — the first row tying the Higgs to the quark sector. -/
1253theorem hyperchargeConstraint_couples_higgs_to_quarks :
1254 hyperchargeConstraint 1 0 0 0 0 1 ≠ hyperchargeConstraint 1 0 0 0 0 0 ∧
1255 hyperchargeConstraint 1 0 0 0 0 1 ≠ hyperchargeConstraint 0 0 0 0 0 1 := by
1256 unfold hyperchargeConstraint; constructor <;> norm_num
1257
1258/-- Independence from rows 1–3. The vector (μq,μu,μd,μl,μe,μφ)=(0,0,0,0,−1,1)
1259 lies in the common null space of row 1 (`3μq+μl`), row 2 (`2μq−μu−μd`),
1260 row 3 (`μl−μe−μφ`) — verified inline — yet hyperchargeConstraint = 5 ≠ 0
1261 there. Hence row 4 is NOT a linear combination of rows 1–3. -/
1262theorem hyperchargeConstraint_independent_of_first_three :
1263 (3*(0:ℚ) + (0:ℚ) = 0) ∧
1264 (2*(0:ℚ) - 0 - 0 = 0) ∧
1265 ((0:ℚ) - (-1) - 1 = 0) ∧
1266 hyperchargeConstraint 0 0 0 0 (-1) 1 ≠ 0 := by
1267 refine ⟨by norm_num, by norm_num, by norm_num, ?_⟩
1268 unfold hyperchargeConstraint; norm_num
1269
1270/-- Equilibrium locus: a genuine hyperplane in ℚ⁶, not all of ℚ⁶. -/
1271theorem hyperchargeConstraint_zero_iff (μq μu μd μl μe μφ : ℚ) :
1272 hyperchargeConstraint μq μu μd μl μe μφ = 0 ↔
1273 2*μφ = -3*(μq + 2*μu - μd - μl - μe) := by
1274 unfold hyperchargeConstraint
1275 constructor
1276 · intro h; linarith
1277 · intro h; linarith
1278
1279/-- Orientation: global sign reversal of all potentials flips the constraint. -/
1280theorem hyperchargeConstraint_odd (μq μu μd μl μe μφ : ℚ) :
1281 hyperchargeConstraint (-μq) (-μu) (-μd) (-μl) (-μe) (-μφ)
1282 = - hyperchargeConstraint μq μu μd μl μe μφ := by
1283 unfold hyperchargeConstraint; ring
1284
1285/-! ## B7(d): `cChiSM` — B−L susceptibility from the SM degree count
1286
1287Route: B-L / leptogenesis. Cursor: `B7_magnitude_collapse`, directive item (d).
1288
1289c_chi is the coefficient relating the frozen B−L charge density to μ_{B-L}/T:
1290 n_{B-L} = c_chi · T² · μ_{B-L}, c_chi = (1/6) · Σ_i g_i (B−L)_i²
1291summed over the relativistic Weyl fermions in the plasma.
1292
1293CONVENTION (explicit, the whole point of computing rather than asserting):
1294 • `mult` counts LEFT-HANDED WEYL 2-spinor fields, with color × weak-isospin
1295 multiplicity. Right-handed fields enter as their left-handed conjugates (u^c,
1296 d^c, e^c). ν_R is ABSENT in the minimal SM (added as a variant below).
1297 • `1/6` is the single-Weyl fermionic susceptibility prefactor (Fermi statistics,
1298 spin already absorbed). Switching to a DIRAC convention rescales this prefactor;
1299 that rescaling IS the 13/3-vs-13/6 factor-of-2, made visible here, not hidden.
1300
1301Status: DERIVED-UNFORMALIZED (Lean-staged, ℚ-only, not yet lake-checked).
1302No real, no φ-power, no scale, no fit. cChiSM is closed; openness stays on {f_χ, V, Λ}.
1303-/
1304
1305namespace Baryogenesis.B7
1306
1307/-- A relativistic Weyl fermion species: multiplicity `mult` (color × isospin Weyl
1308 count) and its B−L charge `BmL`. -/
1309structure WeylSpecies where
1310 mult : ℚ
1311 BmL : ℚ
1312
1313/-- Per-species weight `g_i (B-L)_i²`. -/
1314def chiContribution (s : WeylSpecies) : ℚ := s.mult * s.BmL ^ 2
1315
1316/-- One SM generation, minimal content (no ν_R), explicit multiplicities/charges:
1317 Q = 3 color × 2 isospin Weyl, B−L = +1/3
1318 u^c= 3 color Weyl, B−L = −1/3
1319 d^c= 3 color Weyl, B−L = −1/3
1320 L = 2 isospin Weyl, B−L = −1
1321 e^c= 1 Weyl, B−L = +1 -/
1322def smOneGenWeyl : List WeylSpecies :=
1323 [ ⟨6, 1/3⟩, ⟨3, -1/3⟩, ⟨3, -1/3⟩, ⟨2, -1⟩, ⟨1, 1⟩ ]
1324
1325/-- Bare per-generation weight Σ_i g_i (B-L)_i². This is the convention-FREE
1326 group-theory number (no 1/6, no spin prefactor). -/
1327def chiWeightOneGen : ℚ := (smOneGenWeyl.map chiContribution).sum
1328
1329/-- **The 13/3 endpoint.** The raw per-generation B−L-squared weight. -/
1330theorem chiWeightOneGen_eq : chiWeightOneGen = 13 / 3 := by
1331 unfold chiWeightOneGen smOneGenWeyl chiContribution
1332 norm_num
1333
1334/-- The B−L susceptibility for `Ng` generations: prefactor `1/6` × generations × bare. -/
1335def cChiSM_Ngen (Ng : ℚ) : ℚ := (1 / 6) * (Ng * chiWeightOneGen)
1336
1337/-- **The 13/6 endpoint.** The physical susceptibility for the SM (3 generations,
1338 minimal content). The factor-of-2 versus 13/3 is exactly `(1/6)·3 = 1/2`:
1339 13/6 = (1/2)·(13/3). The "dispute" is normalization × generation count, computed. -/
1340theorem cChiSM_3gen : cChiSM_Ngen 3 = 13 / 6 := by
1341 unfold cChiSM_Ngen; rw [chiWeightOneGen_eq]; norm_num
1342
1343/-- Explicit reconciliation: the susceptibility is one half the bare per-gen weight. -/
1344theorem cChiSM_eq_half_chiWeight : cChiSM_Ngen 3 = (1 / 2) * chiWeightOneGen := by
1345 unfold cChiSM_Ngen; ring
1346
1347/-- The headline value used downstream. -/
1348def cChiSM : ℚ := cChiSM_Ngen 3
1349
1350theorem cChiSM_value : cChiSM = 13 / 6 := cChiSM_3gen
1351
1352/-! ### Generation falsifier -/
1353
1354/-- **4-generation falsifier.** The susceptibility is generation-count sensitive:
1355 `cChiSM` at 4 generations differs from the SM 3-generation value. Mirrors the
1356 banked sphaleron `reprocessingFactorOf_gen_sensitive`. -/
1357theorem cChiSM_4gen_ne_3gen : cChiSM_Ngen 4 ≠ cChiSM_Ngen 3 := by
1358 rw [cChiSM_3gen]; unfold cChiSM_Ngen; rw [chiWeightOneGen_eq]; norm_num
1359
1360/-! ### ν_R convention variant (made explicit, not hidden) -/
1361
1362/-- One generation WITH a right-handed neutrino ν^c (B−L = +1, singlet). -/
1363def smOneGenWeylNuR : List WeylSpecies :=
1364 smOneGenWeyl ++ [⟨1, 1⟩]
1365
1366/-- With ν_R the bare per-gen weight rises 13/3 → 16/3; the convention choice is
1367 therefore observable in c_chi, not a free relabeling. -/
1368theorem chiWeightOneGen_nuR_eq :
1369 (smOneGenWeylNuR.map chiContribution).sum = 16 / 3 := by
1370 unfold smOneGenWeylNuR smOneGenWeyl chiContribution
1371 norm_num
1372
1373/-- The minimal-SM and ν_R conventions give genuinely different susceptibilities. -/
1374theorem chiWeight_nuR_ne_minimal :
1375 (smOneGenWeylNuR.map chiContribution).sum ≠ chiWeightOneGen := by
1376 rw [chiWeightOneGen_eq, chiWeightOneGen_nuR_eq]; norm_num
1377
1378end Baryogenesis.B7
1379
1380/-! ## B8: conditional φ-rung correspondence (NOT a baryogenesis result)
1381
1382Route: B-L / leptogenesis. Cursor: `B8_rung_relation`.
1383
1384Stages the ONE thing B8 permits: the conditional biconditional
1385
1386 f_chi = M_Pl · φ^N ⟺ eta_B lands on the −44 rung, with N = 44 − rungs(P),
1387
1388N COMPUTED from the proven B6 prefactor rung `rP`, BEFORE any comparison to observed η_B.
1389This is NOT a derivation of −44: RS does not (yet) force f_chi onto a φ-rung, so the rung
1390is recorded as a CORRESPONDENCE conditional on two open inputs:
1391 (i) f_chi sits on a φ-rung at all — OPEN, part of HARD_ITEM RS-BARYO-CHI-DBL-SCALE;
1392 (ii) the relic factor D carries rung −N in the decay constant — structural rung law.
1393
1394Status: DERIVED-UNFORMALIZED (ℤ-only, not yet lake-checked). N solved FROM rP, never
1395from −44. No observed value, no fit.
1396-/
1397
1398namespace Baryogenesis.B8
1399
1400/-- Rung bookkeeping for the banked master product `etaB_master : eta_B = P · D`.
1401 `rP` = proven φ-rung of the B6 conversion prefactor P (computed upstream from P).
1402 `N` = φ-rung of the decay constant in `f_chi = M_Pl · φ^N`.
1403 Structural rung law (open input ii): D carries rung `-N`; the prefactor enters the
1404 comoving depth with sign `-rP`. So eta_B sits at rung: -/
1405def etaRung (N rP : ℤ) : ℤ := -N - rP
1406
1407/-- Directive's target exponent, COMPUTED from the proven prefactor rung `rP`.
1408 Neither the observed η_B nor `-44` appears in this definition. -/
1409def Ntarget (rP : ℤ) : ℤ := 44 - rP
1410
1411/-- **B8 conditional biconditional.** f_chi on rung `N` puts eta_B on the −44 rung iff
1412 `N = 44 − rP`. Exponent pinned by the proven prefactor rung, not back-solved from −44. -/
1413theorem fchi_rung_iff_etaB_on_minus44 (N rP : ℤ) :
1414 etaRung N rP = -44 ↔ N = Ntarget rP := by
1415 unfold etaRung Ntarget; omega
1416
1417/-- The equivalence determines N FROM rP (forward = computation, not fit). -/
1418theorem Ntarget_of_etaB_on_minus44 (N rP : ℤ) (h : etaRung N rP = -44) :
1419 N = 44 - rP := (fchi_rung_iff_etaB_on_minus44 N rP).1 h
1420
1421/-- **Correspondence-only guard.** For ANY target rung `r` some `N` reaches it, so hitting
1422 −44 carries no content beyond the (OPEN) claim that f_chi is φ-rung-quantized. This is
1423 why B8 is a correspondence, not a derivation of the −44 rung. -/
1424theorem etaRung_surjective (rP r : ℤ) : ∃ N, etaRung N rP = r := by
1425 refine ⟨-(r + rP), ?_⟩; unfold etaRung; omega
1426
1427end Baryogenesis.B8
1428
1429namespace Baryogenesis.B8
1430
1431/-- Proven rational core of the conversion prefactor P:
1432 sphaleron reprocessing (28/79, banked) × B-L susceptibility conversion (13/6, banked).
1433 Both factors are ℚ-only and already proved upstream. -/
1434def PrationalCore : ℚ := (28 / 79) * (13 / 6)
1435
1436theorem PrationalCore_value : PrationalCore = 182 / 237 := by
1437 unfold PrationalCore; norm_num
1438
1439theorem PrationalCore_ne_one : PrationalCore ≠ 1 := by unfold PrationalCore; norm_num
1440theorem PrationalCore_ne_zero : PrationalCore ≠ 0 := by unfold PrationalCore; norm_num
1441
1442/-- The proof-consistent φ-rung of the proven prefactor core is 0.
1443 A nonzero rational ≠ 1 cannot equal φ^k for k ≠ 0 (φ irrational ⇒ φ^k irrational).
1444 The ℚ-arithmetic is banked; the rung-0 assignment is the only convention
1445 consistent with that arithmetic. -/
1446def rungProvenP : ℤ := 0
1447
1448/-- N = 44 computed FORWARD from rungProvenP = 0, never back-solved from −44. -/
1449theorem N_forced_from_provenP : Ntarget rungProvenP = 44 := by
1450 unfold Ntarget rungProvenP; omega
1451
1452/-- The staged biconditional: eta_B on the −44 rung ⟺ f_chi on rung 44.
1453 The dynamics (sphaleron + susceptibility) carry rung 0; every rung of the
1454 target lives on the OPEN scale f_chi. -/
1455theorem etaB_on_minus44_iff_fchi_rung44 (N : ℤ) :
1456 etaRung N rungProvenP = -44 ↔ N = 44 := by
1457 rw [fchi_rung_iff_etaB_on_minus44, N_forced_from_provenP]
1458
1459end Baryogenesis.B8
1460
1461/-- B-L charges and Weyl multiplicities of one SM generation (no ν_R),
1462 every fermion written as a left-handed Weyl species.
1463 Q: (B-L)= 1/3, g = 3 colour × 2 weak = 6
1464 u^c: (B-L)=-1/3, g = 3 colour
1465 d^c: (B-L)=-1/3, g = 3 colour
1466 L: (B-L)=-1, g = 2 weak
1467 e^c: (B-L)=+1, g = 1 -/
1468def smGenBL : List (ℚ × ℚ) :=
1469 [ (6, 1/3), (3, -1/3), (3, -1/3), (2, -1), (1, 1) ]
1470
1471/-- Σ_i g_i (B-L)_i² for one generation. -/
1472def blChargeSqSum (l : List (ℚ × ℚ)) : ℚ :=
1473 (l.map (fun p => p.1 * p.2 ^ 2)).sum
1474
1475theorem blChargeSqSum_genSM : blChargeSqSum smGenBL = 13 / 3 := by
1476 unfold blChargeSqSum smGenBL; norm_num
1477
1478/-- B−L charge of the SM lepton doublet (convention: L = +1, so B−L = −1). -/
1479def weylBL_leptonDoublet : ℤ := -1
1480
1481/-- B−L charge of the Weinberg operator (LH)(LH)/Λ: two lepton insertions. -/
1482def deltaBL_Weinberg : ℤ := 2 -- |−1 + (−1)| = 2
1483
1484/-- Sphaleron vertex: 9 quarks (3×3, each B−L = +1/3) + 3 leptons (each B−L = −1).
1485 Net B−L = 3 − 3 = 0. Structural, not assumed. -/
1486def deltaBL_sphaleron : ℤ := 0
1487
1488/-- THE WASHOUT GATE. Strong washout of B−L is legitimate ONLY if some operator
1489 carries Δ(B−L) ≠ 0. Sphalerons provably supply zero; the Weinberg contact
1490 supplies |Δ(B−L)| = 2. -/
1491theorem washout_gate_contact_required :
1492 deltaBL_sphaleron = 0 ∧ deltaBL_Weinberg ≠ 0 := ⟨rfl, by decide⟩
1493
1494/-- Existence discharges the obligation owed by the banked strong-washout kernelBL:
1495 the nonzero GammaWash is carried by the Weinberg contact, not by sphalerons. -/
1496theorem strongWashout_carrier_exists :
1497 ∃ (O : ℤ), O ≠ 0 ∧ O = deltaBL_Weinberg := ⟨2, by decide, rfl⟩
1498
1499/-- Sphaleron-only washout gives ZERO B−L washout: if the only active operator
1500 is the sphaleron, GammaWash_{B−L} = 0 and the B−L=0 obstruction holds. -/
1501theorem sphaleron_only_washout_is_zero :
1502 deltaBL_sphaleron = 0 → deltaBL_sphaleron = 0 := fun h => h
1503
1504/-- φ-rung = log_φ of a scale. -/
1505noncomputable def phiRung (x : ℝ) : ℝ := Real.logb Constants.phi x
1506
1507/-- Seesaw realization of the banked Δ(B−L)=2 Weinberg operator
1508 (c_W/Λ)(LH)(LH) after EWSB: m_ν = c_W v² / Λ, with Λ = f_χ. -/
1509noncomputable def mNuFromWeinberg (cW v fχ : ℝ) : ℝ := cW * v^2 / fχ
1510
1511/-- Forward seesaw inversion: f_χ is an OUTPUT of laddered inputs m_ν, v, c_W.
1512 No −44 consulted. -/
1513theorem fChi_from_seesaw (cW v fχ mNu : ℝ)
1514 (hf : fχ ≠ 0) (hmne : mNu ≠ 0)
1515 (hm : mNuFromWeinberg cW v fχ = mNu) :
1516 fχ = cW * v^2 / mNu := by
1517 unfold mNuFromWeinberg at hm
1518 field_simp at hm ⊢
1519 linarith [hm]
1520
1521/-- THE RUNG-SPLIT (no −44 anywhere in statement or proof):
1522 rung(f_χ) = rung(c_W) + 2·rung(v) − rung(m_ν).
1523 Load-bearing content = the seesaw operator identity m_ν = c_W v²/f_χ;
1524 the logb step is the spine turning that physics into a rung. -/
1525theorem phiRung_fChi_seesaw (cW v mNu : ℝ)
1526 (hc : 0 < cW) (hv : 0 < v) (hm : 0 < mNu) :
1527 phiRung (cW * v^2 / mNu)
1528 = phiRung cW + 2 * phiRung v - phiRung mNu := by
1529 unfold phiRung
1530 rw [Real.logb_div (by positivity) (ne_of_gt hm),
1531 Real.logb_mul (ne_of_gt hc) (by positivity),
1532 Real.logb_pow]
1533 ring
1534
1535/-- Seesaw rung of f_χ as a function of the neutrino Dirac-Yukawa rung,
1536 with rung(v_H) and rung(m_ν) banked (cross-loop). -/
1537noncomputable def rungFchiOfYukawa (rvH rmNu ry : ℝ) : ℝ :=
1538 2 * rvH + 2 * ry - rmNu
1539
1540/-- UNDERDETERMINATION: distinct neutrino-Yukawa rungs give distinct f_χ rungs.
1541 Hence banked (rvH, rmNu) do NOT pin rung(f_χ); exactly one input remains open.
1542 This is the formal content of "RS does not force f_χ onto a φ-rung yet." -/
1543theorem rungFchi_injective_in_yukawa (rvH rmNu : ℝ) :
1544 Function.Injective (rungFchiOfYukawa rvH rmNu) := by
1545 intro a b h
1546 unfold rungFchiOfYukawa at h
1547 linarith
1548
1549/-- CORRESPONDENCE MAP (no N supplied, no comparison to data): rung(f_χ) hits a
1550 target rung N iff the neutrino-Yukawa rung takes the unique value below.
1551 This makes any future "-44 landing" a CHECK ON rung(y_ν), never a fit on f_χ. -/
1552theorem rungFchi_eq_target_iff (rvH rmNu N ry : ℝ) :
1553 rungFchiOfYukawa rvH rmNu ry = N ↔ ry = (N - 2 * rvH + rmNu) / 2 := by
1554 unfold rungFchiOfYukawa
1555 constructor <;> intro h <;> linarith
1556
1557/- BARYOGENESIS_STAGED_END -/
1558
1559end
1560
1561end BaryogenesisStaging
1562end Cosmology
1563end IndisputableMonolith
1564