IndisputableMonolith.Masses.JCostPerturbation
IndisputableMonolith/Masses/JCostPerturbation.lean · 1634 lines · 89 declarations
show as:
view math explainer →
1import Mathlib
2import IndisputableMonolith.Constants
3import IndisputableMonolith.Constants.AlphaDerivation
4-- import IndisputableMonolith.Constants.Alpha -- [not in public release]
5-- import IndisputableMonolith.Physics.MassTopology -- [not in public release]
6-- import IndisputableMonolith.Physics.LeptonGenerations.Defs -- [not in public release]
7-- import IndisputableMonolith.Verification.LeptonCoefficientPerturbation -- [not in public release]
8
9/-!
10# Mass-Layer J-Cost Perturbation Bridge
11
12This module upstreams the current O4 perturbative closure into the `Masses.*`
13namespace and ties it to the canonical lepton-step definitions.
14
15This module now serves as the Lean closure package for O4 coefficient forcing.
16It certifies:
171. the `Jcost(1+α)` perturbative channel form,
182. the explicit `α² + 12α³` radiative decomposition used in `refined_shift`,
193. exact geometric evaluations of the zeroth-order constants in the same path.
20-/
21
22namespace IndisputableMonolith
23namespace Masses
24namespace JCostPerturbation
25
26open Constants
27open Constants.AlphaDerivation
28open Physics
29open Physics.MassTopology
30open Physics.LeptonGenerations
31open Verification.LeptonCoefficientPerturbation
32
33noncomputable section
34
35/-- Upstreamed channel form of the `Jcost(1+α)` perturbation. -/
36theorem jcost_two_channel_form :
37 ∃ c : ℝ, 2 * Cost.Jcost (1 + alpha) = alpha ^ 2 + c * alpha ^ 3 ∧ |c| ≤ 4 :=
38 two_jcost_one_plus_alpha_expansion
39
40/-- Upstreamed uniqueness form for the perturbative cubic channel coefficient in
41`2*Jcost(1+α) = α² + cα³`. -/
42theorem jcost_two_channel_coeff_unique :
43 ∃! c : ℝ, 2 * Cost.Jcost (1 + alpha) = alpha ^ 2 + c * alpha ^ 3 :=
44 exists_unique_two_jcost_channel_coeff
45
46/-- Canonical cubic-channel coefficient for the doubled `Jcost(1+α)` expansion. -/
47noncomputable def jcost_two_channel_coeff : ℝ :=
48 by
49 classical
50 exact Classical.choose (ExistsUnique.exists jcost_two_channel_coeff_unique)
51
52/-- The canonical coefficient satisfies the doubled-channel identity. -/
53theorem jcost_two_channel_coeff_spec :
54 2 * Cost.Jcost (1 + alpha) = alpha ^ 2 + jcost_two_channel_coeff * alpha ^ 3 := by
55 classical
56 have h_exists : ∃ c : ℝ, 2 * Cost.Jcost (1 + alpha) = alpha ^ 2 + c * alpha ^ 3 :=
57 ExistsUnique.exists jcost_two_channel_coeff_unique
58 simpa [jcost_two_channel_coeff] using (Classical.choose_spec h_exists)
59
60/-- Characterization form: a coefficient satisfies the doubled-channel identity
61iff it equals the canonical coefficient. -/
62theorem jcost_two_channel_coeff_iff (c : ℝ) :
63 (2 * Cost.Jcost (1 + alpha) = alpha ^ 2 + c * alpha ^ 3) ↔
64 c = jcost_two_channel_coeff := by
65 constructor
66 · intro hc
67 exact two_jcost_cubic_coeff_unique (c1 := c) (c2 := jcost_two_channel_coeff) hc
68 jcost_two_channel_coeff_spec
69 · intro hc
70 simpa [hc] using jcost_two_channel_coeff_spec
71
72/-- Exact edge/face constants appearing in the lepton correction path. -/
73theorem mass_topology_counts :
74 E_total = 12 ∧ E_passive = 11 ∧ W = 17 := by
75 constructor
76 · native_decide
77 constructor
78 · native_decide
79 · native_decide
80
81/-- Canonical ledger fraction value in the electron-break base shift. -/
82theorem ledger_fraction_eq_29_over_44 :
83 ledger_fraction = (29 : ℚ) / 44 := by
84 native_decide
85
86/-- Algebraic uniqueness of the `29/(11k)` normalization at the canonical ratio. -/
87theorem ratio_29_over_11k_forces_k_eq_four
88 {k : ℕ} (hk : 0 < k)
89 (hfrac : (29 : ℚ) / ((11 : ℚ) * k) = (29 : ℚ) / 44) :
90 k = 4 := by
91 have hkq_ne : ((11 : ℚ) * k) ≠ 0 := by
92 have hk_ne : (k : ℚ) ≠ 0 := by
93 exact_mod_cast (Nat.ne_of_gt hk)
94 exact mul_ne_zero (by norm_num) hk_ne
95 have hcross : (29 : ℚ) * 44 = (29 : ℚ) * ((11 : ℚ) * k) := by
96 exact (div_eq_div_iff hkq_ne (by norm_num : (44 : ℚ) ≠ 0)).mp hfrac
97 have hkq : (k : ℚ) = 4 := by
98 nlinarith [hcross]
99 exact Nat.cast_inj.mp (by simpa using hkq)
100
101/-- In the normalized geometric family `(W+E)/(kE_p)`, the canonical ratio forces `k = 4`. -/
102theorem ledger_fraction_denominator_forced
103 {k : ℕ} (hk : 0 < k)
104 (h : ((W + E_total : ℚ) / (k * E_passive) = ledger_fraction)) :
105 k = 4 := by
106 have hW : W = 17 := mass_topology_counts.2.2
107 have hE : E_total = 12 := mass_topology_counts.1
108 have hEp : E_passive = 11 := mass_topology_counts.2.1
109 have hraw : ((17 + 12 : ℚ) / ((k : ℚ) * 11)) = ((17 + 12 : ℚ) / ((4 : ℚ) * 11)) := by
110 simpa [ledger_fraction, hW, hE, hEp, Nat.cast_mul, Nat.cast_add, Nat.cast_ofNat,
111 mul_comm, mul_left_comm, mul_assoc] using h
112 have hfrac : (29 : ℚ) / ((11 : ℚ) * k) = (29 : ℚ) / 44 := by
113 have htmp := hraw
114 norm_num at htmp
115 simpa [mul_comm, mul_left_comm, mul_assoc] using htmp
116 exact ratio_29_over_11k_forces_k_eq_four hk hfrac
117
118/-- Positivity-free denominator forcing in `(W+E)/(kE_p)`:
119 canonical ledger-fraction matching still forces `k = 4` without
120 explicitly assuming `k > 0`. -/
121theorem ledger_fraction_denominator_forced_no_hk
122 {k : ℕ}
123 (h : ((W + E_total : ℚ) / (k * E_passive) = ledger_fraction)) :
124 k = 4 := by
125 have hk : 0 < k := by
126 by_cases hk0 : k = 0
127 · subst hk0
128 have hfrac0 : ledger_fraction = (0 : ℚ) := by simpa using h.symm
129 have hledger_ne_zero : ledger_fraction ≠ 0 := by
130 rw [ledger_fraction_eq_29_over_44]
131 norm_num
132 exact (hledger_ne_zero hfrac0).elim
133 · exact Nat.pos_of_ne_zero hk0
134 exact ledger_fraction_denominator_forced hk h
135
136/-- Rational-scale version of denominator forcing in `(W+E)/(cE_p)`: canonical
137 ledger fraction matching forces `c = 4`. -/
138theorem ledger_fraction_denominator_scale_forced
139 {c : ℚ} (hc_pos : 0 < c)
140 (h : ((W + E_total : ℚ) / (c * E_passive) = ledger_fraction)) :
141 c = 4 := by
142 have hW : W = 17 := mass_topology_counts.2.2
143 have hE : E_total = 12 := mass_topology_counts.1
144 have hEp : E_passive = 11 := mass_topology_counts.2.1
145 have hraw : ((17 + 12 : ℚ) / (c * 11)) = ((17 + 12 : ℚ) / ((4 : ℚ) * 11)) := by
146 simpa [ledger_fraction, hW, hE, hEp, mul_comm, mul_left_comm, mul_assoc] using h
147 have hfrac : (29 : ℚ) / ((11 : ℚ) * c) = (29 : ℚ) / 44 := by
148 have htmp := hraw
149 norm_num at htmp
150 simpa [mul_comm, mul_left_comm, mul_assoc] using htmp
151 have hc_ne : c ≠ 0 := ne_of_gt hc_pos
152 have hc11_ne : ((11 : ℚ) * c) ≠ 0 := mul_ne_zero (by norm_num) hc_ne
153 have hcross : (29 : ℚ) * 44 = (29 : ℚ) * ((11 : ℚ) * c) := by
154 exact (div_eq_div_iff hc11_ne (by norm_num : (44 : ℚ) ≠ 0)).mp hfrac
155 nlinarith [hcross]
156
157/-- Positivity-free rational-scale denominator forcing in `(W+E)/(cE_p)`:
158 canonical ledger-fraction matching still forces `c = 4` without
159 explicitly assuming `c > 0`. -/
160theorem ledger_fraction_denominator_scale_forced_no_hc_pos
161 {c : ℚ}
162 (h : ((W + E_total : ℚ) / (c * E_passive) = ledger_fraction)) :
163 c = 4 := by
164 have hc_ne : c ≠ 0 := by
165 intro hc0
166 subst hc0
167 have hfrac0 : ledger_fraction = (0 : ℚ) := by
168 simpa using h.symm
169 have hledger_ne_zero : ledger_fraction ≠ 0 := by
170 rw [ledger_fraction_eq_29_over_44]
171 norm_num
172 exact (hledger_ne_zero hfrac0).elim
173 have hW : W = 17 := mass_topology_counts.2.2
174 have hE : E_total = 12 := mass_topology_counts.1
175 have hEp : E_passive = 11 := mass_topology_counts.2.1
176 have hraw : ((17 + 12 : ℚ) / (c * 11)) = ((17 + 12 : ℚ) / ((4 : ℚ) * 11)) := by
177 simpa [ledger_fraction, hW, hE, hEp, mul_comm, mul_left_comm, mul_assoc] using h
178 have hfrac : (29 : ℚ) / ((11 : ℚ) * c) = (29 : ℚ) / 44 := by
179 have htmp := hraw
180 norm_num at htmp
181 simpa [mul_comm, mul_left_comm, mul_assoc] using htmp
182 have hc11_ne : ((11 : ℚ) * c) ≠ 0 := mul_ne_zero (by norm_num) hc_ne
183 have hcross : (29 : ℚ) * 44 = (29 : ℚ) * ((11 : ℚ) * c) := by
184 exact (div_eq_div_iff hc11_ne (by norm_num : (44 : ℚ) ≠ 0)).mp hfrac
185 nlinarith [hcross]
186
187/-- In the numerator-offset family `((W+E)+n)/(4E_p)`, canonical matching forces `n = 0`. -/
188theorem ledger_fraction_numerator_offset_forced
189 {n : ℚ}
190 (h : (((W + E_total : ℚ) + n) / (4 * E_passive) = ledger_fraction)) :
191 n = 0 := by
192 have hW : W = 17 := mass_topology_counts.2.2
193 have hE : E_total = 12 := mass_topology_counts.1
194 have hEp : E_passive = 11 := mass_topology_counts.2.1
195 have hraw : ((29 : ℚ) + n) / 44 = (29 : ℚ) / 44 := by
196 simpa [ledger_fraction, hW, hE, hEp, add_assoc, add_comm, add_left_comm,
197 mul_comm, mul_left_comm, mul_assoc] using h
198 nlinarith [hraw]
199
200/-- In the normalized two-weight family `(aW + bE)/(4E_p)` with total weight `a+b=2`,
201 canonical matching forces `(a,b) = (1,1)`. -/
202theorem ledger_fraction_weight_split_forced
203 {a b : ℚ}
204 (hsum : a + b = 2)
205 (h : ((a * (W : ℚ) + b * (E_total : ℚ)) / (4 * E_passive) = ledger_fraction)) :
206 a = 1 ∧ b = 1 := by
207 have hW : W = 17 := mass_topology_counts.2.2
208 have hE : E_total = 12 := mass_topology_counts.1
209 have hEp : E_passive = 11 := mass_topology_counts.2.1
210 have hlin : (a * 17 + b * 12) / 44 = ((17 + 12 : ℚ) / 44) := by
211 simpa [ledger_fraction, hW, hE, hEp] using h
212 have hcross : (a * 17 + b * 12) * 44 = ((17 + 12 : ℚ) * 44) := by
213 exact (div_eq_div_iff (by norm_num : (44 : ℚ) ≠ 0) (by norm_num : (44 : ℚ) ≠ 0)).mp hlin
214 have hnum : a * 17 + b * 12 = (17 + 12 : ℚ) := by
215 nlinarith [hcross]
216 have ha : a = 1 := by nlinarith [hsum, hnum]
217 have hb : b = 1 := by nlinarith [hsum, hnum]
218 exact ⟨ha, hb⟩
219
220/-- Joint Diophantine forcing for integer numerator/denominator perturbations of the
221 ledger fraction: under passive-edge band `n ≤ E_p`, canonical matching in
222 `((W+E)+n)/(kE_p)` forces `k = 4` and `n = 0`. -/
223theorem ledger_fraction_kn_forced_under_passive_bound
224 {k n : ℕ} (hk : 0 < k) (hn_le : n ≤ E_passive)
225 (h : ((((W + E_total + n : ℕ) : ℚ) / (k * E_passive)) = ledger_fraction)) :
226 k = 4 ∧ n = 0 := by
227 have hW : W = 17 := mass_topology_counts.2.2
228 have hE : E_total = 12 := mass_topology_counts.1
229 have hEp : E_passive = 11 := mass_topology_counts.2.1
230 have hraw : (((29 + n : ℕ) : ℚ) / ((k * 11 : ℕ) : ℚ)) = ((12 + 17 : ℚ) / (4 * 11)) := by
231 simpa [ledger_fraction, hW, hE, hEp, Nat.cast_add, Nat.cast_mul, Nat.cast_ofNat,
232 add_assoc, add_comm, add_left_comm] using h
233 have hraw29 : (((29 + n : ℕ) : ℚ) / ((k * 11 : ℕ) : ℚ)) = (29 : ℚ) / 44 := by
234 have htmp := hraw
235 norm_num at htmp
236 simpa using htmp
237 have hk11_ne : ((k * 11 : ℕ) : ℚ) ≠ 0 := by
238 exact_mod_cast (Nat.mul_ne_zero (Nat.ne_of_gt hk) (by decide : 11 ≠ 0))
239 have hcross : (((29 + n : ℕ) : ℚ) * 44) = (29 : ℚ) * (((k * 11 : ℕ) : ℚ)) := by
240 have htmp := hraw29
241 field_simp [hk11_ne] at htmp
242 nlinarith [htmp]
243 have hcrossNat : (29 + n) * 44 = 29 * (k * 11) := by
244 exact_mod_cast hcross
245 have hlin : 44 * (29 + n) = 319 * k := by
246 nlinarith [hcrossNat]
247 have hn11 : n ≤ 11 := by
248 simpa [hEp] using hn_le
249 have hk4 : k = 4 := by
250 omega
251 have hn0 : n = 0 := by
252 omega
253 exact ⟨hk4, hn0⟩
254
255/-- Positivity-free integer-band closure for ledger-fraction perturbations:
256 under passive-edge band `n ≤ E_p`, canonical matching in
257 `((W+E)+n)/(kE_p)` forces `k = 4` and `n = 0` without explicit `k > 0`. -/
258theorem ledger_fraction_kn_forced_under_passive_bound_no_hk
259 {k n : ℕ} (hn_le : n ≤ E_passive)
260 (h : ((((W + E_total + n : ℕ) : ℚ) / (k * E_passive)) = ledger_fraction)) :
261 k = 4 ∧ n = 0 := by
262 have hk : 0 < k := by
263 by_cases hk0 : k = 0
264 · subst hk0
265 have hfrac0 : ledger_fraction = (0 : ℚ) := by
266 simpa using h.symm
267 have hledger_ne_zero : ledger_fraction ≠ 0 := by
268 rw [ledger_fraction_eq_29_over_44]
269 norm_num
270 exact (hledger_ne_zero hfrac0).elim
271 · exact Nat.pos_of_ne_zero hk0
272 exact ledger_fraction_kn_forced_under_passive_bound hk hn_le h
273
274/-- Zeroth-order geometric part of the refined shift in explicit numeric form. -/
275theorem base_shift_eq_34_plus_29_over_44 :
276 base_shift = (34 : ℝ) + ((29 : ℚ) / 44 : ℚ) := by
277 have hW : (W : ℝ) = 17 := by exact_mod_cast mass_topology_counts.2.2
278 calc
279 base_shift = 2 * (W : ℝ) + (ledger_fraction : ℝ) := by simp [base_shift]
280 _ = 2 * 17 + (((29 : ℚ) / 44 : ℚ) : ℝ) := by
281 simp [hW, ledger_fraction_eq_29_over_44]
282 _ = (34 : ℝ) + ((29 : ℚ) / 44 : ℚ) := by ring
283
284/-- In the affine `W`-multiplier family `uW + ledger_fraction`, canonical
285 `base_shift` matching forces `u = 2`. -/
286theorem base_shift_wallpaper_multiplier_forced
287 {u : ℝ}
288 (h : base_shift = u * (W : ℝ) + (ledger_fraction : ℝ)) :
289 u = 2 := by
290 have hcanon : base_shift = 2 * (W : ℝ) + (ledger_fraction : ℝ) := by
291 simp [base_shift]
292 have hmul : u * (W : ℝ) = 2 * (W : ℝ) := by
293 linarith [h, hcanon]
294 have hW_ne : (W : ℝ) ≠ 0 := by
295 exact_mod_cast (show W ≠ 0 by native_decide)
296 exact mul_right_cancel₀ hW_ne hmul
297
298/-- With canonical `2W` term fixed, matching `base_shift` in the denominator family
299 `2W + (W+E)/(kE_p)` forces `k = 4`. -/
300theorem base_shift_denominator_forced
301 {k : ℕ} (hk : 0 < k)
302 (h : base_shift = 2 * (W : ℝ) +
303 ((((W + E_total : ℚ) / (k * E_passive)) : ℚ) : ℝ)) :
304 k = 4 := by
305 have hcanon : base_shift = 2 * (W : ℝ) + (ledger_fraction : ℝ) := by
306 simp [base_shift]
307 have hfracR :
308 ((((W + E_total : ℚ) / (k * E_passive)) : ℚ) : ℝ) = (ledger_fraction : ℝ) := by
309 linarith [h, hcanon]
310 have hfracQ : ((W + E_total : ℚ) / (k * E_passive)) = ledger_fraction := by
311 exact_mod_cast hfracR
312 exact ledger_fraction_denominator_forced hk hfracQ
313
314/-- Positivity-free packaged denominator forcing for `base_shift`:
315 with canonical `2W` term fixed, matching
316 `2W + (W+E)/(kE_p)` still forces `k = 4` without explicit `k > 0`. -/
317theorem base_shift_denominator_forced_no_hk
318 {k : ℕ}
319 (h : base_shift = 2 * (W : ℝ) +
320 ((((W + E_total : ℚ) / (k * E_passive)) : ℚ) : ℝ)) :
321 k = 4 := by
322 have hcanon : base_shift = 2 * (W : ℝ) + (ledger_fraction : ℝ) := by
323 simp [base_shift]
324 have hfracR :
325 ((((W + E_total : ℚ) / (k * E_passive)) : ℚ) : ℝ) = (ledger_fraction : ℝ) := by
326 linarith [h, hcanon]
327 have hfracQ : ((W + E_total : ℚ) / (k * E_passive)) = ledger_fraction := by
328 exact_mod_cast hfracR
329 exact ledger_fraction_denominator_forced_no_hk hfracQ
330
331/-- Positivity-free rational-scale packaged denominator forcing for `base_shift`:
332 with canonical `2W` term fixed, matching
333 `2W + (W+E)/(cE_p)` still forces `c = 4` without explicit `c > 0`. -/
334theorem base_shift_denominator_scale_forced_no_hc_pos
335 {c : ℚ}
336 (h : base_shift = 2 * (W : ℝ) +
337 ((((W + E_total : ℚ) / (c * E_passive)) : ℚ) : ℝ)) :
338 c = 4 := by
339 have hcanon : base_shift = 2 * (W : ℝ) + (ledger_fraction : ℝ) := by
340 simp [base_shift]
341 have hfracR :
342 ((((W + E_total : ℚ) / (c * E_passive)) : ℚ) : ℝ) = (ledger_fraction : ℝ) := by
343 linarith [h, hcanon]
344 have hfracQ : ((W + E_total : ℚ) / (c * E_passive)) = ledger_fraction := by
345 exact_mod_cast hfracR
346 exact ledger_fraction_denominator_scale_forced_no_hc_pos hfracQ
347
348/-- With canonical `2W` term fixed, matching `base_shift` in the numerator-offset family
349 `2W + ((W+E)+n)/(4E_p)` forces `n = 0`. -/
350theorem base_shift_numerator_offset_forced
351 {n : ℚ}
352 (h : base_shift = 2 * (W : ℝ) +
353 (((((W + E_total : ℚ) + n) / (4 * E_passive)) : ℚ) : ℝ)) :
354 n = 0 := by
355 have hcanon : base_shift = 2 * (W : ℝ) + (ledger_fraction : ℝ) := by
356 simp [base_shift]
357 have hfracR :
358 (((((W + E_total : ℚ) + n) / (4 * E_passive)) : ℚ) : ℝ) = (ledger_fraction : ℝ) := by
359 linarith [h, hcanon]
360 have hfracQ : (((W + E_total : ℚ) + n) / (4 * E_passive)) = ledger_fraction := by
361 exact_mod_cast hfracR
362 exact ledger_fraction_numerator_offset_forced hfracQ
363
364/-- With canonical `2W` term fixed, matching `base_shift` in the normalized
365 two-weight family `2W + (aW+bE)/(4E_p)` with `a+b=2` forces `(a,b)=(1,1)`. -/
366theorem base_shift_weight_split_forced
367 {a b : ℚ}
368 (hsum : a + b = 2)
369 (h : base_shift = 2 * (W : ℝ) +
370 ((((a * (W : ℚ) + b * (E_total : ℚ)) / (4 * E_passive)) : ℚ) : ℝ)) :
371 a = 1 ∧ b = 1 := by
372 have hcanon : base_shift = 2 * (W : ℝ) + (ledger_fraction : ℝ) := by
373 simp [base_shift]
374 have hfracR :
375 ((((a * (W : ℚ) + b * (E_total : ℚ)) / (4 * E_passive)) : ℚ) : ℝ) = (ledger_fraction : ℝ) := by
376 linarith [h, hcanon]
377 have hfracQ : ((a * (W : ℚ) + b * (E_total : ℚ)) / (4 * E_passive)) = ledger_fraction := by
378 exact_mod_cast hfracR
379 exact ledger_fraction_weight_split_forced hsum hfracQ
380
381/-- Packaged `base_shift` closure for integer numerator/denominator perturbations:
382 under passive-edge band `n ≤ E_p`, matching
383 `2W + ((W+E)+n)/(kE_p)` forces `k = 4` and `n = 0`. -/
384theorem base_shift_kn_forced_under_passive_bound
385 {k n : ℕ} (hk : 0 < k) (hn_le : n ≤ E_passive)
386 (h : base_shift = 2 * (W : ℝ) +
387 (((((W + E_total + n : ℕ) : ℚ) / (k * E_passive)) : ℚ) : ℝ)) :
388 k = 4 ∧ n = 0 := by
389 have hcanon : base_shift = 2 * (W : ℝ) + (ledger_fraction : ℝ) := by
390 simp [base_shift]
391 have hfracR :
392 (((((W + E_total + n : ℕ) : ℚ) / (k * E_passive)) : ℚ) : ℝ) = (ledger_fraction : ℝ) := by
393 linarith [h, hcanon]
394 have hfracQ : ((((W + E_total + n : ℕ) : ℚ) / (k * E_passive)) = ledger_fraction) := by
395 exact_mod_cast hfracR
396 exact ledger_fraction_kn_forced_under_passive_bound hk hn_le hfracQ
397
398/-- Positivity-free packaged `base_shift` closure for integer perturbations:
399 under passive-edge band `n ≤ E_p`, matching
400 `2W + ((W+E)+n)/(kE_p)` forces `k = 4` and `n = 0`
401 without explicit `k > 0`. -/
402theorem base_shift_kn_forced_under_passive_bound_no_hk
403 {k n : ℕ} (hn_le : n ≤ E_passive)
404 (h : base_shift = 2 * (W : ℝ) +
405 (((((W + E_total + n : ℕ) : ℚ) / (k * E_passive)) : ℚ) : ℝ)) :
406 k = 4 ∧ n = 0 := by
407 have hcanon : base_shift = 2 * (W : ℝ) + (ledger_fraction : ℝ) := by
408 simp [base_shift]
409 have hfracR :
410 (((((W + E_total + n : ℕ) : ℚ) / (k * E_passive)) : ℚ) : ℝ) = (ledger_fraction : ℝ) := by
411 linarith [h, hcanon]
412 have hfracQ : ((((W + E_total + n : ℕ) : ℚ) / (k * E_passive)) = ledger_fraction) := by
413 exact_mod_cast hfracR
414 exact ledger_fraction_kn_forced_under_passive_bound_no_hk hn_le hfracQ
415
416/-- Upstreamed radiative decomposition (`α² + 12α³`) used by the mass topology path. -/
417theorem radiative_correction_channel_form :
418 radiative_correction = alpha ^ 2 + 12 * alpha ^ 3 :=
419 radiative_correction_channel_decomposition
420
421/-- Refined shift split into geometric base plus explicit radiative channels. -/
422theorem refined_shift_channel_form :
423 refined_shift = base_shift + (alpha ^ 2 + 12 * alpha ^ 3) := by
424 simpa [refined_shift] using congrArg (fun x => base_shift + x) radiative_correction_channel_form
425
426/-- In the cubic-channel family `α² + cα³`, canonical radiative matching forces `c = 12`. -/
427theorem radiative_cubic_coeff_forced
428 {c : ℝ}
429 (h : radiative_correction = alpha ^ 2 + c * alpha ^ 3) :
430 c = 12 := by
431 have hcanon : radiative_correction = alpha ^ 2 + 12 * alpha ^ 3 :=
432 radiative_correction_channel_form
433 have hα_bounds := Physics.ElectronMass.Necessity.alpha_bounds
434 have hα_pos : 0 < alpha := by linarith [hα_bounds.1]
435 have hα_ne : alpha ≠ 0 := ne_of_gt hα_pos
436 have hmul : c * alpha ^ 3 = 12 * alpha ^ 3 := by
437 linarith [h, hcanon]
438 exact mul_right_cancel₀ (pow_ne_zero 3 hα_ne) hmul
439
440/-- `refined_shift` version of cubic-channel forcing:
441 in `base_shift + (α² + cα³)`, canonical matching forces `c = 12`. -/
442theorem refined_shift_cubic_coeff_forced
443 {c : ℝ}
444 (h : refined_shift = base_shift + (alpha ^ 2 + c * alpha ^ 3)) :
445 c = 12 := by
446 have hcanon : refined_shift = base_shift + radiative_correction := by
447 simp [refined_shift]
448 have hrad : radiative_correction = alpha ^ 2 + c * alpha ^ 3 := by
449 linarith [h, hcanon]
450 exact radiative_cubic_coeff_forced hrad
451
452/-- Joint affine-family forcing for `refined_shift` once base-shift role is fixed:
453 if `base_shift = uW + ledger_fraction`, then matching
454 `refined_shift = uW + ledger_fraction + (α² + cα³)` forces `u = 2` and `c = 12`. -/
455theorem refined_shift_full_affine_forced_from_base_role
456 {u c : ℝ}
457 (hb : base_shift = u * (W : ℝ) + (ledger_fraction : ℝ))
458 (h : refined_shift = u * (W : ℝ) + (ledger_fraction : ℝ) + (alpha ^ 2 + c * alpha ^ 3)) :
459 u = 2 ∧ c = 12 := by
460 have hu : u = 2 := base_shift_wallpaper_multiplier_forced hb
461 have hc : c = 12 := by
462 have hshift : refined_shift = base_shift + (alpha ^ 2 + c * alpha ^ 3) := by
463 calc
464 refined_shift = u * (W : ℝ) + (ledger_fraction : ℝ) + (alpha ^ 2 + c * alpha ^ 3) := h
465 _ = base_shift + (alpha ^ 2 + c * alpha ^ 3) := by simp [hb]
466 exact refined_shift_cubic_coeff_forced hshift
467 exact ⟨hu, hc⟩
468
469/-- Dual packaged route for `refined_shift` affine forcing:
470 if cubic-channel scale is fixed (`c = 12`), then matching
471 `uW + ledger_fraction + (α² + cα³)` forces the wallpaper multiplier `u = 2`. -/
472theorem refined_shift_wallpaper_multiplier_forced_from_cubic_scale
473 {u c : ℝ}
474 (hc : c = 12)
475 (h : refined_shift = u * (W : ℝ) + (ledger_fraction : ℝ) + (alpha ^ 2 + c * alpha ^ 3)) :
476 u = 2 := by
477 have hshift : refined_shift = u * (W : ℝ) + (ledger_fraction : ℝ) + (alpha ^ 2 + 12 * alpha ^ 3) := by
478 simpa [hc] using h
479 have hbase : base_shift = u * (W : ℝ) + (ledger_fraction : ℝ) := by
480 linarith [hshift, refined_shift_channel_form]
481 exact base_shift_wallpaper_multiplier_forced hbase
482
483/-- Under fixed base-shift role, affine `refined_shift` matching packages an
484 equivalence between wallpaper multiplier and cubic channel:
485 `u = 2 ↔ c = 12`. -/
486theorem refined_shift_wallpaper_iff_cubic_from_base_role
487 {u c : ℝ}
488 (hb : base_shift = u * (W : ℝ) + (ledger_fraction : ℝ))
489 (h : refined_shift = u * (W : ℝ) + (ledger_fraction : ℝ) + (alpha ^ 2 + c * alpha ^ 3)) :
490 u = 2 ↔ c = 12 := by
491 have hpair : u = 2 ∧ c = 12 :=
492 refined_shift_full_affine_forced_from_base_role hb h
493 constructor
494 · intro _hu
495 exact hpair.2
496 · intro hc
497 exact refined_shift_wallpaper_multiplier_forced_from_cubic_scale hc h
498
499/-- Electron-to-muon step split: fixed geometric term minus quadratic channel. -/
500theorem step_e_mu_channel_split :
501 step_e_mu = (E_passive : ℝ) + 1 / (4 * Real.pi) - correction_order_2 := by
502 simp [step_e_mu, correction_order_2]
503
504/-- With fixed inverse-π term and quadratic channel, canonical matching forces
505 the passive-edge zeroth-order term in `e→μ`. -/
506theorem step_e_mu_passive_term_forced
507 {s : ℝ}
508 (h : step_e_mu = s + 1 / (4 * Real.pi) - correction_order_2) :
509 s = (E_passive : ℝ) := by
510 have hcanon : step_e_mu = (E_passive : ℝ) + 1 / (4 * Real.pi) - correction_order_2 :=
511 step_e_mu_channel_split
512 linarith [h, hcanon]
513
514/-- In the quadratic-channel family `E_p + 1/(4π) - qα²`, canonical `e→μ`
515 matching forces `q = 1`. -/
516theorem step_e_mu_quadratic_scale_forced
517 {q : ℝ}
518 (h : step_e_mu = (E_passive : ℝ) + 1 / (4 * Real.pi) - q * correction_order_2) :
519 q = 1 := by
520 have hcanon : step_e_mu = (E_passive : ℝ) + 1 / (4 * Real.pi) - correction_order_2 :=
521 step_e_mu_channel_split
522 have hmul : q * correction_order_2 = correction_order_2 := by
523 linarith [h, hcanon]
524 have hα_bounds := Physics.ElectronMass.Necessity.alpha_bounds
525 have hα_pos : 0 < alpha := by linarith [hα_bounds.1]
526 have hα_ne : alpha ≠ 0 := ne_of_gt hα_pos
527 have hco2_ne : correction_order_2 ≠ 0 := by
528 simpa [correction_order_2] using (pow_ne_zero 2 hα_ne)
529 have hmul' : q * correction_order_2 = (1 : ℝ) * correction_order_2 := by
530 simpa [one_mul] using hmul
531 exact mul_right_cancel₀ hco2_ne hmul'
532
533/-- Joint forcing in the mixed `e→μ` family
534 `E_p + 1/(kπ) - qα²`: if the inverse-π slot matches canonically, then
535 canonical matching forces both `k = 4` and `q = 1`. -/
536theorem step_e_mu_invpi_quadratic_forced
537 {k : ℕ} {q : ℝ} (hk : 0 < k)
538 (hchan : 1 / ((k : ℝ) * Real.pi) = 1 / (4 * Real.pi))
539 (h : step_e_mu = (E_passive : ℝ) + 1 / ((k : ℝ) * Real.pi) - q * correction_order_2) :
540 k = 4 ∧ q = 1 := by
541 have hkpi_ne : ((k : ℝ) * Real.pi) ≠ 0 := by positivity
542 have h4pi_ne : (4 * Real.pi : ℝ) ≠ 0 := by positivity
543 have hmul : (1 : ℝ) * (4 * Real.pi) = (1 : ℝ) * ((k : ℝ) * Real.pi) := by
544 exact (div_eq_div_iff hkpi_ne h4pi_ne).1 hchan
545 have hden : (k : ℝ) * Real.pi = 4 * Real.pi := by
546 nlinarith [hmul]
547 have hk_real : (k : ℝ) = 4 := mul_right_cancel₀ (ne_of_gt Real.pi_pos) hden
548 have hk4 : k = 4 := Nat.cast_inj.mp (by simpa using hk_real)
549 have hq1 : q = 1 := by
550 have h' : step_e_mu = (E_passive : ℝ) + 1 / (4 * Real.pi) - q * correction_order_2 := by
551 simpa [hk4] using h
552 exact step_e_mu_quadratic_scale_forced h'
553 exact ⟨hk4, hq1⟩
554
555/-- Positivity-free mixed forcing for `e→μ`:
556 in `E_p + 1/(kπ) - qα²`, inverse-π slot matching derives denominator
557 positivity and forces `k = 4`, `q = 1` without explicit `k > 0`. -/
558theorem step_e_mu_invpi_quadratic_forced_no_hk
559 {k : ℕ} {q : ℝ}
560 (hchan : 1 / ((k : ℝ) * Real.pi) = 1 / (4 * Real.pi))
561 (h : step_e_mu = (E_passive : ℝ) + 1 / ((k : ℝ) * Real.pi) - q * correction_order_2) :
562 k = 4 ∧ q = 1 := by
563 have hk : 0 < k := by
564 by_cases hk0 : k = 0
565 · subst hk0
566 have hzero : (0 : ℝ) = 1 / (4 * Real.pi) := by
567 calc
568 (0 : ℝ) = 1 / ((0 : ℝ) * Real.pi) := by simp
569 _ = 1 / (4 * Real.pi) := by simpa using hchan
570 have hpos : (0 : ℝ) < 1 / (4 * Real.pi) := by positivity
571 linarith
572 · exact Nat.pos_of_ne_zero hk0
573 exact step_e_mu_invpi_quadratic_forced hk hchan h
574
575/-- Dual packaged route for mixed `e→μ` forcing:
576 if quadratic scale is fixed (`q = 1`), then in
577 `E_p + 1/(kπ) - qα²` canonical matching forces `k = 4`. -/
578theorem step_e_mu_invpi_denominator_forced_from_quadratic_scale
579 {k : ℕ} {q : ℝ} (hk : 0 < k)
580 (hq : q = 1)
581 (h : step_e_mu = (E_passive : ℝ) + 1 / ((k : ℝ) * Real.pi) - q * correction_order_2) :
582 k = 4 := by
583 have h' : step_e_mu = (E_passive : ℝ) + 1 / ((k : ℝ) * Real.pi) - correction_order_2 := by
584 simpa [hq] using h
585 have hcanon : step_e_mu = (E_passive : ℝ) + 1 / (4 * Real.pi) - correction_order_2 :=
586 step_e_mu_channel_split
587 have hfrac : 1 / ((k : ℝ) * Real.pi) = 1 / (4 * Real.pi) := by
588 linarith [h', hcanon]
589 have hkpi_ne : ((k : ℝ) * Real.pi) ≠ 0 := by positivity
590 have h4pi_ne : (4 * Real.pi : ℝ) ≠ 0 := by positivity
591 have hmul : (1 : ℝ) * (4 * Real.pi) = (1 : ℝ) * ((k : ℝ) * Real.pi) := by
592 exact (div_eq_div_iff hkpi_ne h4pi_ne).1 hfrac
593 have hden : (k : ℝ) * Real.pi = 4 * Real.pi := by
594 nlinarith [hmul]
595 have hk_real : (k : ℝ) = 4 := mul_right_cancel₀ (ne_of_gt Real.pi_pos) hden
596 exact Nat.cast_inj.mp (by simpa using hk_real)
597
598/-- Positivity-free quadratic-fixed route for mixed `e→μ` forcing:
599 in `E_p + 1/(kπ) - qα²`, canonical matching and `q=1` force `k=4`
600 without explicit denominator-positivity assumptions. -/
601theorem step_e_mu_invpi_denominator_forced_from_quadratic_scale_no_hk
602 {k : ℕ} {q : ℝ}
603 (hq : q = 1)
604 (h : step_e_mu = (E_passive : ℝ) + 1 / ((k : ℝ) * Real.pi) - q * correction_order_2) :
605 k = 4 := by
606 have h' : step_e_mu = (E_passive : ℝ) + 1 / ((k : ℝ) * Real.pi) - correction_order_2 := by
607 simpa [hq] using h
608 by_cases hk0 : k = 0
609 · subst hk0
610 have hcanon : step_e_mu = (E_passive : ℝ) + 1 / (4 * Real.pi) - correction_order_2 :=
611 step_e_mu_channel_split
612 have hEq : (E_passive : ℝ) - correction_order_2 =
613 (E_passive : ℝ) + 1 / (4 * Real.pi) - correction_order_2 := by
614 calc
615 (E_passive : ℝ) - correction_order_2 = step_e_mu := by
616 simpa using h'.symm
617 _ = (E_passive : ℝ) + 1 / (4 * Real.pi) - correction_order_2 := hcanon
618 have hfalse : (1 / (4 * Real.pi) : ℝ) = 0 := by
619 linarith [hEq]
620 have hpos : (0 : ℝ) < 1 / (4 * Real.pi) := by positivity
621 linarith
622 · have hk : 0 < k := Nat.pos_of_ne_zero hk0
623 exact step_e_mu_invpi_denominator_forced_from_quadratic_scale hk hq h
624
625/-- Packaged mixed-family closure for `e→μ` under passive role + inverse-π channel match:
626 in `s + 1/(kπ) - qα²`, canonical matching forces `s = E_p`, `k = 4`, `q = 1`. -/
627theorem step_e_mu_full_mixed_family_forced_from_passive_and_channel
628 {s : ℝ} {k : ℕ} {q : ℝ} (hk : 0 < k)
629 (hs : s = (E_passive : ℝ))
630 (hchan : 1 / ((k : ℝ) * Real.pi) = 1 / (4 * Real.pi))
631 (h : step_e_mu = s + 1 / ((k : ℝ) * Real.pi) - q * correction_order_2) :
632 s = (E_passive : ℝ) ∧ k = 4 ∧ q = 1 := by
633 have hkq : k = 4 ∧ q = 1 := by
634 have h' : step_e_mu = (E_passive : ℝ) + 1 / ((k : ℝ) * Real.pi) - q * correction_order_2 := by
635 simpa [hs] using h
636 exact step_e_mu_invpi_quadratic_forced hk hchan h'
637 exact ⟨hs, hkq.1, hkq.2⟩
638
639/-- Positivity-free packaged mixed-family closure for `e→μ`
640 under passive role + inverse-π channel match:
641 in `s + 1/(kπ) - qα²`, canonical matching forces `s = E_p`, `k = 4`, `q = 1`
642 without explicit `k > 0`. -/
643theorem step_e_mu_full_mixed_family_forced_from_passive_and_channel_no_hk
644 {s : ℝ} {k : ℕ} {q : ℝ}
645 (hs : s = (E_passive : ℝ))
646 (hchan : 1 / ((k : ℝ) * Real.pi) = 1 / (4 * Real.pi))
647 (h : step_e_mu = s + 1 / ((k : ℝ) * Real.pi) - q * correction_order_2) :
648 s = (E_passive : ℝ) ∧ k = 4 ∧ q = 1 := by
649 have hkq : k = 4 ∧ q = 1 := by
650 have h' : step_e_mu = (E_passive : ℝ) + 1 / ((k : ℝ) * Real.pi) - q * correction_order_2 := by
651 simpa [hs] using h
652 exact step_e_mu_invpi_quadratic_forced_no_hk hchan h'
653 exact ⟨hs, hkq.1, hkq.2⟩
654
655/-- Complementary mixed-family packaging under passive role + quadratic-scale fixation:
656 in `s + 1/(kπ) - qα²`, canonical matching and `q=1` force `s = E_p`, `k = 4`, `q = 1`. -/
657theorem step_e_mu_full_mixed_family_forced_from_passive_and_quadratic_scale
658 {s : ℝ} {k : ℕ} {q : ℝ} (hk : 0 < k)
659 (hs : s = (E_passive : ℝ))
660 (hq : q = 1)
661 (h : step_e_mu = s + 1 / ((k : ℝ) * Real.pi) - q * correction_order_2) :
662 s = (E_passive : ℝ) ∧ k = 4 ∧ q = 1 := by
663 have hk4 : k = 4 := by
664 have h' : step_e_mu = (E_passive : ℝ) + 1 / ((k : ℝ) * Real.pi) - q * correction_order_2 := by
665 simpa [hs] using h
666 exact step_e_mu_invpi_denominator_forced_from_quadratic_scale hk hq h'
667 exact ⟨hs, hk4, hq⟩
668
669/-- Positivity-free complementary mixed-family packaging under passive role
670 + quadratic-scale fixation:
671 in `s + 1/(kπ) - qα²`, canonical matching and `q=1` force
672 `s = E_p`, `k = 4`, `q = 1` without explicit `k > 0`. -/
673theorem step_e_mu_full_mixed_family_forced_from_passive_and_quadratic_scale_no_hk
674 {s : ℝ} {k : ℕ} {q : ℝ}
675 (hs : s = (E_passive : ℝ))
676 (hq : q = 1)
677 (h : step_e_mu = s + 1 / ((k : ℝ) * Real.pi) - q * correction_order_2) :
678 s = (E_passive : ℝ) ∧ k = 4 ∧ q = 1 := by
679 have hk4 : k = 4 := by
680 have h' : step_e_mu = (E_passive : ℝ) + 1 / ((k : ℝ) * Real.pi) - q * correction_order_2 := by
681 simpa [hs] using h
682 exact step_e_mu_invpi_denominator_forced_from_quadratic_scale_no_hk hq h'
683 exact ⟨hs, hk4, hq⟩
684
685/-- In the mixed canonical family `E_p + 1/(kπ) - qα²`, denominator and quadratic
686 slots are equivalent under canonical matching: `k = 4 ↔ q = 1`. -/
687theorem step_e_mu_denominator_iff_quadratic_scale
688 {k : ℕ} {q : ℝ} (hk : 0 < k)
689 (h : step_e_mu = (E_passive : ℝ) + 1 / ((k : ℝ) * Real.pi) - q * correction_order_2) :
690 k = 4 ↔ q = 1 := by
691 constructor
692 · intro hk4
693 have h' : step_e_mu = (E_passive : ℝ) + 1 / (4 * Real.pi) - q * correction_order_2 := by
694 simpa [hk4] using h
695 exact step_e_mu_quadratic_scale_forced h'
696 · intro hq1
697 exact step_e_mu_invpi_denominator_forced_from_quadratic_scale hk hq1 h
698
699/-- In the one-parameter family `E_p + 1/(kπ) - α²`, matching the canonical step forces `k = 4`. -/
700theorem step_e_mu_invpi_denominator_forced
701 {k : ℕ} (hk : 0 < k)
702 (h : step_e_mu = (E_passive : ℝ) + 1 / ((k : ℝ) * Real.pi) - correction_order_2) :
703 k = 4 := by
704 have hcanon : step_e_mu = (E_passive : ℝ) + 1 / (4 * Real.pi) - correction_order_2 :=
705 step_e_mu_channel_split
706 have hfrac : 1 / ((k : ℝ) * Real.pi) = 1 / (4 * Real.pi) := by
707 linarith [h, hcanon]
708 have hk_real_pos : 0 < (k : ℝ) := by
709 exact_mod_cast hk
710 have hkpi_ne : ((k : ℝ) * Real.pi) ≠ 0 := by positivity
711 have h4pi_ne : (4 * Real.pi : ℝ) ≠ 0 := by positivity
712 have hmul : (1 : ℝ) * (4 * Real.pi) = (1 : ℝ) * ((k : ℝ) * Real.pi) := by
713 exact (div_eq_div_iff hkpi_ne h4pi_ne).1 hfrac
714 have hden : (k : ℝ) * Real.pi = 4 * Real.pi := by
715 nlinarith [hmul]
716 have hpi_ne : Real.pi ≠ 0 := by exact ne_of_gt Real.pi_pos
717 have hk_real : (k : ℝ) = 4 := mul_right_cancel₀ hpi_ne hden
718 exact Nat.cast_inj.mp (by simpa using hk_real)
719
720/-- Positivity-free inverse-π forcing for `e→μ`:
721 denominator positivity is derived from canonical matching itself. -/
722theorem step_e_mu_invpi_denominator_forced_no_hk
723 {k : ℕ}
724 (h : step_e_mu = (E_passive : ℝ) + 1 / ((k : ℝ) * Real.pi) - correction_order_2) :
725 k = 4 := by
726 by_cases hk0 : k = 0
727 · subst hk0
728 have hcanon : step_e_mu = (E_passive : ℝ) + 1 / (4 * Real.pi) - correction_order_2 :=
729 step_e_mu_channel_split
730 have hEq : (E_passive : ℝ) - correction_order_2 =
731 (E_passive : ℝ) + 1 / (4 * Real.pi) - correction_order_2 := by
732 calc
733 (E_passive : ℝ) - correction_order_2 = step_e_mu := by
734 simpa using h.symm
735 _ = (E_passive : ℝ) + 1 / (4 * Real.pi) - correction_order_2 := hcanon
736 have hfalse : (1 / (4 * Real.pi) : ℝ) = 0 := by
737 linarith [hEq]
738 have hpos : (0 : ℝ) < 1 / (4 * Real.pi) := by positivity
739 linarith
740 · have hk : 0 < k := Nat.pos_of_ne_zero hk0
741 exact step_e_mu_invpi_denominator_forced hk h
742
743/-- Positivity-free mixed-family equivalence for `e→μ`:
744 in the canonical family `E_p + 1/(kπ) - qα²`, denominator and quadratic slots
745 remain equivalent under canonical matching without an explicit `k > 0` premise. -/
746theorem step_e_mu_denominator_iff_quadratic_scale_no_hk
747 {k : ℕ} {q : ℝ}
748 (h : step_e_mu = (E_passive : ℝ) + 1 / ((k : ℝ) * Real.pi) - q * correction_order_2) :
749 k = 4 ↔ q = 1 := by
750 constructor
751 · intro hk4
752 have h' : step_e_mu = (E_passive : ℝ) + 1 / (4 * Real.pi) - q * correction_order_2 := by
753 simpa [hk4] using h
754 exact step_e_mu_quadratic_scale_forced h'
755 · intro hq1
756 have h' : step_e_mu = (E_passive : ℝ) + 1 / ((k : ℝ) * Real.pi) - correction_order_2 := by
757 simpa [hq1] using h
758 exact step_e_mu_invpi_denominator_forced_no_hk h'
759
760/-- Real-scale version of the inverse-π forcing for `e→μ`: canonical matching forces scale `4`. -/
761theorem step_e_mu_invpi_scale_forced
762 {c : ℝ} (hc_pos : 0 < c)
763 (h : step_e_mu = (E_passive : ℝ) + 1 / (c * Real.pi) - correction_order_2) :
764 c = 4 := by
765 have hcanon : step_e_mu = (E_passive : ℝ) + 1 / (4 * Real.pi) - correction_order_2 :=
766 step_e_mu_channel_split
767 have hfrac : 1 / (c * Real.pi) = 1 / (4 * Real.pi) := by
768 linarith [h, hcanon]
769 have hcpi_ne : (c * Real.pi) ≠ 0 := by positivity
770 have h4pi_ne : (4 * Real.pi : ℝ) ≠ 0 := by positivity
771 have hmul : (1 : ℝ) * (4 * Real.pi) = (1 : ℝ) * (c * Real.pi) := by
772 exact (div_eq_div_iff hcpi_ne h4pi_ne).1 hfrac
773 have hden : c * Real.pi = 4 * Real.pi := by
774 nlinarith [hmul]
775 exact mul_right_cancel₀ (ne_of_gt Real.pi_pos) hden
776
777/-- Positivity-free real-scale inverse-π forcing for `e→μ`:
778 canonical matching forces scale `4` without an explicit `c > 0` premise. -/
779theorem step_e_mu_invpi_scale_forced_no_hc_pos
780 {c : ℝ}
781 (h : step_e_mu = (E_passive : ℝ) + 1 / (c * Real.pi) - correction_order_2) :
782 c = 4 := by
783 have hcanon : step_e_mu = (E_passive : ℝ) + 1 / (4 * Real.pi) - correction_order_2 :=
784 step_e_mu_channel_split
785 have hfrac : 1 / (c * Real.pi) = 1 / (4 * Real.pi) := by
786 linarith [h, hcanon]
787 by_cases hc0 : c = 0
788 · subst hc0
789 have hzero : (0 : ℝ) = 1 / (4 * Real.pi) := by
790 calc
791 (0 : ℝ) = 1 / ((0 : ℝ) * Real.pi) := by simp
792 _ = 1 / (4 * Real.pi) := by simpa using hfrac
793 have hpos : (0 : ℝ) < 1 / (4 * Real.pi) := by positivity
794 linarith
795 · have hcpi_ne : (c * Real.pi) ≠ 0 := mul_ne_zero hc0 (ne_of_gt Real.pi_pos)
796 have h4pi_ne : (4 * Real.pi : ℝ) ≠ 0 := by positivity
797 have hmul : (1 : ℝ) * (4 * Real.pi) = (1 : ℝ) * (c * Real.pi) := by
798 exact (div_eq_div_iff hcpi_ne h4pi_ne).1 hfrac
799 have hden : c * Real.pi = 4 * Real.pi := by
800 nlinarith [hmul]
801 exact mul_right_cancel₀ (ne_of_gt Real.pi_pos) hden
802
803/-- Full one-parameter forcing for `e→μ` once passive-edge zeroth-order term is fixed:
804 in `s + 1/(kπ) - α²`, canonical matching forces `k = 4`. -/
805theorem step_e_mu_full_family_forced_from_passive_term
806 {s : ℝ} {k : ℕ} (hk : 0 < k)
807 (hs : s = (E_passive : ℝ))
808 (h : step_e_mu = s + 1 / ((k : ℝ) * Real.pi) - correction_order_2) :
809 s = (E_passive : ℝ) ∧ k = 4 := by
810 have h' : step_e_mu = (E_passive : ℝ) + 1 / ((k : ℝ) * Real.pi) - correction_order_2 := by
811 simpa [hs] using h
812 exact ⟨hs, step_e_mu_invpi_denominator_forced hk h'⟩
813
814/-- Positivity-free full one-parameter forcing for `e→μ` once passive-edge
815 zeroth-order term is fixed:
816 in `s + 1/(kπ) - α²`, canonical matching forces `k = 4` without explicit
817 denominator-positivity assumptions. -/
818theorem step_e_mu_full_family_forced_from_passive_term_no_hk
819 {s : ℝ} {k : ℕ}
820 (hs : s = (E_passive : ℝ))
821 (h : step_e_mu = s + 1 / ((k : ℝ) * Real.pi) - correction_order_2) :
822 s = (E_passive : ℝ) ∧ k = 4 := by
823 have h' : step_e_mu = (E_passive : ℝ) + 1 / ((k : ℝ) * Real.pi) - correction_order_2 := by
824 simpa [hs] using h
825 exact ⟨hs, step_e_mu_invpi_denominator_forced_no_hk h'⟩
826
827/-- Real-scale full forcing for `e→μ` once passive-edge zeroth-order term is fixed:
828 in `s + 1/(cπ) - α²`, canonical matching forces `c = 4`. -/
829theorem step_e_mu_full_real_family_forced_from_passive_term
830 {s c : ℝ} (hc_pos : 0 < c)
831 (hs : s = (E_passive : ℝ))
832 (h : step_e_mu = s + 1 / (c * Real.pi) - correction_order_2) :
833 s = (E_passive : ℝ) ∧ c = 4 := by
834 have h' : step_e_mu = (E_passive : ℝ) + 1 / (c * Real.pi) - correction_order_2 := by
835 simpa [hs] using h
836 exact ⟨hs, step_e_mu_invpi_scale_forced hc_pos h'⟩
837
838/-- Positivity-free real-scale full forcing for `e→μ` once passive-edge
839 zeroth-order term is fixed:
840 in `s + 1/(cπ) - α²`, canonical matching forces `c = 4` without explicit
841 `c > 0`. -/
842theorem step_e_mu_full_real_family_forced_from_passive_term_no_hc_pos
843 {s c : ℝ}
844 (hs : s = (E_passive : ℝ))
845 (h : step_e_mu = s + 1 / (c * Real.pi) - correction_order_2) :
846 s = (E_passive : ℝ) ∧ c = 4 := by
847 have h' : step_e_mu = (E_passive : ℝ) + 1 / (c * Real.pi) - correction_order_2 := by
848 simpa [hs] using h
849 exact ⟨hs, step_e_mu_invpi_scale_forced_no_hc_pos h'⟩
850
851/-- Positivity-free real-scale equivalence packaging for `e→μ`:
852 under canonical matching in `s + 1/(cπ) - α²`, passive term and
853 denominator scale are linked as `c = 4 ↔ s = E_p`. -/
854theorem step_e_mu_scale_iff_passive_term_no_hc_pos
855 {s c : ℝ}
856 (h : step_e_mu = s + 1 / (c * Real.pi) - correction_order_2) :
857 c = 4 ↔ s = (E_passive : ℝ) := by
858 constructor
859 · intro hc4
860 have h' : step_e_mu = s + 1 / (4 * Real.pi) - correction_order_2 := by
861 simpa [hc4] using h
862 linarith [h', step_e_mu_channel_split]
863 · intro hs
864 have h' : step_e_mu = (E_passive : ℝ) + 1 / (c * Real.pi) - correction_order_2 := by
865 simpa [hs] using h
866 exact step_e_mu_invpi_scale_forced_no_hc_pos h'
867
868/-- Packaged forcing from inverse-π channel matching in `e→μ`:
869 if the inverse-π slot matches canonically, then the denominator and passive
870 zeroth-order term are both forced in `s + 1/(kπ) - α²`. -/
871theorem step_e_mu_full_family_forced_from_channel_match
872 {s : ℝ} {k : ℕ} (hk : 0 < k)
873 (hchan : 1 / ((k : ℝ) * Real.pi) = 1 / (4 * Real.pi))
874 (h : step_e_mu = s + 1 / ((k : ℝ) * Real.pi) - correction_order_2) :
875 s = (E_passive : ℝ) ∧ k = 4 := by
876 have hkpi_ne : ((k : ℝ) * Real.pi) ≠ 0 := by positivity
877 have h4pi_ne : (4 * Real.pi : ℝ) ≠ 0 := by positivity
878 have hmul : (1 : ℝ) * (4 * Real.pi) = (1 : ℝ) * ((k : ℝ) * Real.pi) := by
879 exact (div_eq_div_iff hkpi_ne h4pi_ne).1 hchan
880 have hden : (k : ℝ) * Real.pi = 4 * Real.pi := by
881 nlinarith [hmul]
882 have hk_real : (k : ℝ) = 4 := by
883 exact mul_right_cancel₀ (ne_of_gt Real.pi_pos) hden
884 have hk4 : k = 4 := Nat.cast_inj.mp (by simpa using hk_real)
885 have hs : s = (E_passive : ℝ) := by
886 have h' : step_e_mu = s + 1 / (4 * Real.pi) - correction_order_2 := by
887 simpa [hk4] using h
888 linarith [h', step_e_mu_channel_split]
889 exact ⟨hs, hk4⟩
890
891/-- Positivity-free packaged forcing from inverse-π channel matching in `e→μ`:
892 if the inverse-π slot matches canonically, then denominator and passive
893 zeroth-order term are forced in `s + 1/(kπ) - α²` without explicit
894 denominator-positivity assumptions. -/
895theorem step_e_mu_full_family_forced_from_channel_match_no_hk
896 {s : ℝ} {k : ℕ}
897 (hchan : 1 / ((k : ℝ) * Real.pi) = 1 / (4 * Real.pi))
898 (h : step_e_mu = s + 1 / ((k : ℝ) * Real.pi) - correction_order_2) :
899 s = (E_passive : ℝ) ∧ k = 4 := by
900 have hk : 0 < k := by
901 by_cases hk0 : k = 0
902 · subst hk0
903 have hzero : (0 : ℝ) = 1 / (4 * Real.pi) := by
904 calc
905 (0 : ℝ) = 1 / ((0 : ℝ) * Real.pi) := by simp
906 _ = 1 / (4 * Real.pi) := by simpa using hchan
907 have hpos : (0 : ℝ) < 1 / (4 * Real.pi) := by positivity
908 linarith
909 · exact Nat.pos_of_ne_zero hk0
910 exact step_e_mu_full_family_forced_from_channel_match hk hchan h
911
912/-- The linear alpha coefficient in `step_mu_tau` evaluates to `37/2`. -/
913theorem step_mu_tau_linear_coeff_eq_37_over_2 :
914 ((2 * wallpaper_groups + D : ℝ) / 2) = (37 : ℝ) / 2 := by
915 norm_num [wallpaper_groups, D]
916
917/-- Muon-to-tau step in explicit geometric/linear-alpha form. -/
918theorem step_mu_tau_channel_split :
919 step_mu_tau = (6 : ℝ) - ((37 : ℝ) / 2) * alpha := by
920 have hcoeff : ((2 * wallpaper_groups + D : ℝ) / 2) = (37 : ℝ) / 2 :=
921 step_mu_tau_linear_coeff_eq_37_over_2
922 have hfaces : (cube_faces D : ℝ) = 6 := by
923 norm_num [cube_faces, D]
924 calc
925 step_mu_tau = (cube_faces D : ℝ) - ((2 * wallpaper_groups + D : ℝ) / 2) * alpha := by
926 simp [step_mu_tau]
927 _ = (cube_faces D : ℝ) - ((37 : ℝ) / 2) * alpha := by rw [hcoeff]
928 _ = (6 : ℝ) - ((37 : ℝ) / 2) * alpha := by rw [hfaces]
929
930/-- With fixed linear-alpha coefficient, canonical matching forces the face-count
931 zeroth-order term in `μ→τ`. -/
932theorem step_mu_tau_face_term_forced
933 {f : ℝ}
934 (h : step_mu_tau = f - ((37 : ℝ) / 2) * alpha) :
935 f = (cube_faces D : ℝ) := by
936 have hcanon : step_mu_tau = (cube_faces D : ℝ) - ((37 : ℝ) / 2) * alpha := by
937 calc
938 step_mu_tau = (6 : ℝ) - ((37 : ℝ) / 2) * alpha := step_mu_tau_channel_split
939 _ = (cube_faces D : ℝ) - ((37 : ℝ) / 2) * alpha := by norm_num [cube_faces, D]
940 linarith [h, hcanon]
941
942/-- Numeric form of `step_mu_tau_face_term_forced`: canonical matching forces `F = 6`. -/
943theorem step_mu_tau_face_count_forced
944 {f : ℝ}
945 (h : step_mu_tau = f - ((37 : ℝ) / 2) * alpha) :
946 f = 6 := by
947 have hf : f = (cube_faces D : ℝ) := step_mu_tau_face_term_forced h
948 have hfaces : (cube_faces D : ℝ) = 6 := by norm_num [cube_faces, D]
949 linarith [hf, hfaces]
950
951/-- In the linear family `F - cα`, matching the canonical μ→τ step forces `c = 37/2`. -/
952theorem step_mu_tau_linear_coeff_forced
953 {c : ℝ}
954 (h : step_mu_tau = (cube_faces D : ℝ) - c * alpha) :
955 c = (37 : ℝ) / 2 := by
956 have hcanon : step_mu_tau = (cube_faces D : ℝ) - ((37 : ℝ) / 2) * alpha := by
957 calc
958 step_mu_tau = (6 : ℝ) - ((37 : ℝ) / 2) * alpha := step_mu_tau_channel_split
959 _ = (cube_faces D : ℝ) - ((37 : ℝ) / 2) * alpha := by norm_num [cube_faces, D]
960 have hα_bounds := Physics.ElectronMass.Necessity.alpha_bounds
961 have hα_pos : 0 < alpha := by linarith [hα_bounds.1]
962 have hα_ne : alpha ≠ 0 := ne_of_gt hα_pos
963 have hmul : c * alpha = ((37 : ℝ) / 2) * alpha := by
964 linarith [h, hcanon]
965 exact mul_right_cancel₀ hα_ne hmul
966
967/-- Full affine-family forcing for `μ→τ` once the zeroth-order face term is fixed:
968 in `f - cα`, canonical matching forces both `f = 6` and `c = 37/2`. -/
969theorem step_mu_tau_full_affine_forced_from_face_term
970 {f c : ℝ}
971 (hf : f = (cube_faces D : ℝ))
972 (h : step_mu_tau = f - c * alpha) :
973 f = 6 ∧ c = (37 : ℝ) / 2 := by
974 have hc : c = (37 : ℝ) / 2 := by
975 have h' : step_mu_tau = (cube_faces D : ℝ) - c * alpha := by
976 simpa [hf] using h
977 exact step_mu_tau_linear_coeff_forced h'
978 have hf6 : f = 6 := by
979 calc
980 f = (cube_faces D : ℝ) := hf
981 _ = 6 := by norm_num [cube_faces, D]
982 exact ⟨hf6, hc⟩
983
984/-- Convenience specialization: if `f = 6`, canonical matching in `f - cα`
985 forces the canonical linear coefficient `c = 37/2`. -/
986theorem step_mu_tau_coeff_forced_from_six_face_term
987 {c : ℝ}
988 (h : step_mu_tau = (6 : ℝ) - c * alpha) :
989 c = (37 : ℝ) / 2 := by
990 have hf : (6 : ℝ) = (cube_faces D : ℝ) := by
991 norm_num [cube_faces, D]
992 have h' : step_mu_tau = (cube_faces D : ℝ) - c * alpha := by
993 simpa [hf] using h
994 exact step_mu_tau_linear_coeff_forced h'
995
996/-- In the denominator family `F - ((2W + D)/k)α`, matching canonical `μ→τ` forces `k = 2`. -/
997theorem step_mu_tau_denominator_forced
998 {k : ℕ} (hk : 0 < k)
999 (h : step_mu_tau = (cube_faces D : ℝ) - (((2 * wallpaper_groups + D : ℝ) / (k : ℝ)) * alpha)) :
1000 k = 2 := by
1001 have hcanon : step_mu_tau = (cube_faces D : ℝ) - ((37 : ℝ) / 2) * alpha := by
1002 calc
1003 step_mu_tau = (6 : ℝ) - ((37 : ℝ) / 2) * alpha := step_mu_tau_channel_split
1004 _ = (cube_faces D : ℝ) - ((37 : ℝ) / 2) * alpha := by norm_num [cube_faces, D]
1005 have hα_bounds := Physics.ElectronMass.Necessity.alpha_bounds
1006 have hα_pos : 0 < alpha := by linarith [hα_bounds.1]
1007 have hα_ne : alpha ≠ 0 := ne_of_gt hα_pos
1008 have hmul :
1009 (((2 * wallpaper_groups + D : ℝ) / (k : ℝ)) * alpha) = ((37 : ℝ) / 2) * alpha := by
1010 linarith [h, hcanon]
1011 have hcoeff : ((2 * wallpaper_groups + D : ℝ) / (k : ℝ)) = (37 : ℝ) / 2 :=
1012 mul_right_cancel₀ hα_ne hmul
1013 have hnum : ((2 * wallpaper_groups + D : ℝ)) = 37 := by
1014 norm_num [wallpaper_groups, D]
1015 have h37 : ((37 : ℝ) / (k : ℝ)) = (37 : ℝ) / 2 := by
1016 calc
1017 (37 : ℝ) / (k : ℝ) = ((2 * wallpaper_groups + D : ℝ) / (k : ℝ)) := by
1018 simp [hnum]
1019 _ = (37 : ℝ) / 2 := hcoeff
1020 have hk_ne : (k : ℝ) ≠ 0 := by
1021 exact_mod_cast (Nat.ne_of_gt hk)
1022 have hcross : (37 : ℝ) * 2 = (37 : ℝ) * (k : ℝ) := by
1023 exact (div_eq_div_iff hk_ne (by norm_num : (2 : ℝ) ≠ 0)).mp h37
1024 have hk_real : (k : ℝ) = 2 := by nlinarith [hcross]
1025 exact Nat.cast_inj.mp (by simpa using hk_real)
1026
1027/-- Real-scale version of μ→τ denominator forcing: canonical matching in
1028 `F - ((2W + D)/c)α` forces `c = 2`. -/
1029theorem step_mu_tau_scale_forced
1030 {c : ℝ} (hc_pos : 0 < c)
1031 (h : step_mu_tau = (cube_faces D : ℝ) - (((2 * wallpaper_groups + D : ℝ) / c) * alpha)) :
1032 c = 2 := by
1033 have hcanon : step_mu_tau = (cube_faces D : ℝ) - ((37 : ℝ) / 2) * alpha := by
1034 calc
1035 step_mu_tau = (6 : ℝ) - ((37 : ℝ) / 2) * alpha := step_mu_tau_channel_split
1036 _ = (cube_faces D : ℝ) - ((37 : ℝ) / 2) * alpha := by norm_num [cube_faces, D]
1037 have hα_bounds := Physics.ElectronMass.Necessity.alpha_bounds
1038 have hα_pos : 0 < alpha := by linarith [hα_bounds.1]
1039 have hα_ne : alpha ≠ 0 := ne_of_gt hα_pos
1040 have hmul :
1041 (((2 * wallpaper_groups + D : ℝ) / c) * alpha) = ((37 : ℝ) / 2) * alpha := by
1042 linarith [h, hcanon]
1043 have hcoeff : ((2 * wallpaper_groups + D : ℝ) / c) = (37 : ℝ) / 2 :=
1044 mul_right_cancel₀ hα_ne hmul
1045 have hnum : ((2 * wallpaper_groups + D : ℝ)) = 37 := by
1046 norm_num [wallpaper_groups, D]
1047 have h37 : ((37 : ℝ) / c) = (37 : ℝ) / 2 := by
1048 calc
1049 (37 : ℝ) / c = ((2 * wallpaper_groups + D : ℝ) / c) := by
1050 simp [hnum]
1051 _ = (37 : ℝ) / 2 := hcoeff
1052 have hc_ne : c ≠ 0 := ne_of_gt hc_pos
1053 have hcross : (37 : ℝ) * 2 = (37 : ℝ) * c := by
1054 exact (div_eq_div_iff hc_ne (by norm_num : (2 : ℝ) ≠ 0)).mp h37
1055 nlinarith [hcross]
1056
1057/-- Positivity-free real-scale μ→τ denominator forcing:
1058 canonical matching in `F - ((2W + D)/c)α` still forces `c = 2`
1059 without explicitly assuming `c > 0`. -/
1060theorem step_mu_tau_scale_forced_no_hc_pos
1061 {c : ℝ}
1062 (h : step_mu_tau = (cube_faces D : ℝ) - (((2 * wallpaper_groups + D : ℝ) / c) * alpha)) :
1063 c = 2 := by
1064 have hc_ne : c ≠ 0 := by
1065 intro hc0
1066 subst hc0
1067 have hface : step_mu_tau = (cube_faces D : ℝ) := by
1068 simpa using h
1069 have hcanon : step_mu_tau =
1070 (cube_faces D : ℝ) - ((37 : ℝ) / 2) * alpha := by
1071 calc
1072 step_mu_tau = (6 : ℝ) - ((37 : ℝ) / 2) * alpha := step_mu_tau_channel_split
1073 _ = (cube_faces D : ℝ) - ((37 : ℝ) / 2) * alpha := by
1074 norm_num [cube_faces, D]
1075 have hα_bounds := Physics.ElectronMass.Necessity.alpha_bounds
1076 have hα_pos : 0 < alpha := by linarith [hα_bounds.1]
1077 linarith [hface, hcanon, hα_pos]
1078 have hcanon : step_mu_tau = (cube_faces D : ℝ) - ((37 : ℝ) / 2) * alpha := by
1079 calc
1080 step_mu_tau = (6 : ℝ) - ((37 : ℝ) / 2) * alpha := step_mu_tau_channel_split
1081 _ = (cube_faces D : ℝ) - ((37 : ℝ) / 2) * alpha := by norm_num [cube_faces, D]
1082 have hα_bounds := Physics.ElectronMass.Necessity.alpha_bounds
1083 have hα_pos : 0 < alpha := by linarith [hα_bounds.1]
1084 have hα_ne : alpha ≠ 0 := ne_of_gt hα_pos
1085 have hmul :
1086 (((2 * wallpaper_groups + D : ℝ) / c) * alpha) = ((37 : ℝ) / 2) * alpha := by
1087 linarith [h, hcanon]
1088 have hcoeff : ((2 * wallpaper_groups + D : ℝ) / c) = (37 : ℝ) / 2 :=
1089 mul_right_cancel₀ hα_ne hmul
1090 have hnum : ((2 * wallpaper_groups + D : ℝ)) = 37 := by
1091 norm_num [wallpaper_groups, D]
1092 have h37 : ((37 : ℝ) / c) = (37 : ℝ) / 2 := by
1093 calc
1094 (37 : ℝ) / c = ((2 * wallpaper_groups + D : ℝ) / c) := by simp [hnum]
1095 _ = (37 : ℝ) / 2 := hcoeff
1096 have hcross : (37 : ℝ) * 2 = (37 : ℝ) * c := by
1097 exact (div_eq_div_iff hc_ne (by norm_num : (2 : ℝ) ≠ 0)).mp h37
1098 nlinarith [hcross]
1099
1100/-- Positivity-free packaged real-scale forcing for `μ→τ`:
1101 with face-term role fixed, canonical matching in
1102 `f - ((2W + D)/c)α` forces `f = 6` and `c = 2`
1103 without explicit `c > 0`. -/
1104theorem step_mu_tau_full_real_family_forced_from_face_term_no_hc_pos
1105 {f c : ℝ}
1106 (hf : f = (cube_faces D : ℝ))
1107 (h : step_mu_tau = f - (((2 * wallpaper_groups + D : ℝ) / c) * alpha)) :
1108 f = 6 ∧ c = 2 := by
1109 have h' : step_mu_tau =
1110 (cube_faces D : ℝ) - (((2 * wallpaper_groups + D : ℝ) / c) * alpha) := by
1111 simpa [hf] using h
1112 have hc2 : c = 2 := step_mu_tau_scale_forced_no_hc_pos h'
1113 have hf6 : f = 6 := by
1114 calc
1115 f = (cube_faces D : ℝ) := hf
1116 _ = 6 := by norm_num [cube_faces, D]
1117 exact ⟨hf6, hc2⟩
1118
1119/-- Positivity-free real-scale equivalence packaging for `μ→τ`:
1120 under canonical matching in `f - ((2W + D)/c)α`, the face count and
1121 denominator scale are linked as `c = 2 ↔ f = 6`. -/
1122theorem step_mu_tau_scale_iff_face_count_no_hc_pos
1123 {f c : ℝ}
1124 (h : step_mu_tau = f - (((2 * wallpaper_groups + D : ℝ) / c) * alpha)) :
1125 c = 2 ↔ f = 6 := by
1126 constructor
1127 · intro hc2
1128 have hcanon : step_mu_tau = (6 : ℝ) - ((37 : ℝ) / 2) * alpha := step_mu_tau_channel_split
1129 have h' : step_mu_tau = f - ((37 : ℝ) / 2) * alpha := by
1130 calc
1131 step_mu_tau = f - (((2 * wallpaper_groups + D : ℝ) / c) * alpha) := h
1132 _ = f - (((2 * wallpaper_groups + D : ℝ) / 2) * alpha) := by simp [hc2]
1133 _ = f - ((37 : ℝ) / 2) * alpha := by norm_num [wallpaper_groups, D]
1134 linarith [hcanon, h']
1135 · intro hf6
1136 have hfCube : f = (cube_faces D : ℝ) := by
1137 calc
1138 f = 6 := hf6
1139 _ = (cube_faces D : ℝ) := by norm_num [cube_faces, D]
1140 have h' : step_mu_tau =
1141 (cube_faces D : ℝ) - (((2 * wallpaper_groups + D : ℝ) / c) * alpha) := by
1142 simpa [hfCube] using h
1143 exact step_mu_tau_scale_forced_no_hc_pos h'
1144
1145/-- Cross-sector positivity-free real-scale iff packaging:
1146 combines `e→μ` and `μ→τ` canonical real-scale matchings into one statement.
1147 Under canonical matching forms, denominator scales are equivalent to their
1148 corresponding zeroth-order geometric terms without explicit positivity
1149 assumptions. -/
1150theorem lepton_real_scale_iff_bundle_no_hc_pos
1151 {s c_e f c_mu : ℝ}
1152 (he : step_e_mu = s + 1 / (c_e * Real.pi) - correction_order_2)
1153 (hmu : step_mu_tau = f - (((2 * wallpaper_groups + D : ℝ) / c_mu) * alpha)) :
1154 (c_e = 4 ↔ s = (E_passive : ℝ)) ∧ (c_mu = 2 ↔ f = 6) := by
1155 refine ⟨?_, ?_⟩
1156 · exact step_e_mu_scale_iff_passive_term_no_hc_pos he
1157 · exact step_mu_tau_scale_iff_face_count_no_hc_pos hmu
1158
1159/-- In the numerator-offset family `F - ((2W+n)/2)α`, canonical matching forces
1160 the offset to be exactly `n = D` (hence `n = 3`). -/
1161theorem step_mu_tau_numerator_offset_forced
1162 {n : ℕ}
1163 (h : step_mu_tau =
1164 (cube_faces D : ℝ) - ((((2 * wallpaper_groups + n : ℕ) : ℝ) / 2) * alpha)) :
1165 n = D := by
1166 have hcanon : step_mu_tau =
1167 (cube_faces D : ℝ) - ((((2 * wallpaper_groups + D : ℕ) : ℝ) / 2) * alpha) := by
1168 simp [step_mu_tau]
1169 have hα_bounds := Physics.ElectronMass.Necessity.alpha_bounds
1170 have hα_pos : 0 < alpha := by linarith [hα_bounds.1]
1171 have hα_ne : alpha ≠ 0 := ne_of_gt hα_pos
1172 have hmul :
1173 ((((2 * wallpaper_groups + n : ℕ) : ℝ) / 2) * alpha) =
1174 ((((2 * wallpaper_groups + D : ℕ) : ℝ) / 2) * alpha) := by
1175 linarith [h, hcanon]
1176 have hcoeff :
1177 (((2 * wallpaper_groups + n : ℕ) : ℝ) / 2) =
1178 (((2 * wallpaper_groups + D : ℕ) : ℝ) / 2) :=
1179 mul_right_cancel₀ hα_ne hmul
1180 have hnumR :
1181 ((2 * wallpaper_groups + n : ℕ) : ℝ) =
1182 ((2 * wallpaper_groups + D : ℕ) : ℝ) := by
1183 nlinarith [hcoeff]
1184 have hnumN : 2 * wallpaper_groups + n = 2 * wallpaper_groups + D := by
1185 exact_mod_cast hnumR
1186 exact Nat.add_left_cancel hnumN
1187
1188/-- Joint Diophantine forcing for the `μ→τ` coefficient family:
1189 with `n` constrained to the dimensional band `n ≤ D`, canonical matching in
1190 `F - ((2W+n)/k)α` forces both `k = 2` and `n = D`. -/
1191theorem step_mu_tau_kn_forced_under_dim_bound
1192 {k n : ℕ} (hk : 0 < k) (hn_le : n ≤ D)
1193 (h : step_mu_tau =
1194 (cube_faces D : ℝ) - ((((2 * wallpaper_groups + n : ℕ) : ℝ) / (k : ℝ)) * alpha)) :
1195 k = 2 ∧ n = D := by
1196 have hcanon : step_mu_tau =
1197 (cube_faces D : ℝ) - ((37 : ℝ) / 2) * alpha := by
1198 calc
1199 step_mu_tau = (6 : ℝ) - ((37 : ℝ) / 2) * alpha := step_mu_tau_channel_split
1200 _ = (cube_faces D : ℝ) - ((37 : ℝ) / 2) * alpha := by
1201 norm_num [cube_faces, D]
1202 have hα_bounds := Physics.ElectronMass.Necessity.alpha_bounds
1203 have hα_pos : 0 < alpha := by linarith [hα_bounds.1]
1204 have hα_ne : alpha ≠ 0 := ne_of_gt hα_pos
1205 have hmul :
1206 ((((2 * wallpaper_groups + n : ℕ) : ℝ) / (k : ℝ)) * alpha)
1207 = ((37 : ℝ) / 2) * alpha := by
1208 linarith [h, hcanon]
1209 have hcoeff :
1210 (((2 * wallpaper_groups + n : ℕ) : ℝ) / (k : ℝ))
1211 = (37 : ℝ) / 2 := by
1212 exact mul_right_cancel₀ hα_ne hmul
1213 have hk_ne : (k : ℝ) ≠ 0 := by
1214 exact_mod_cast (Nat.ne_of_gt hk)
1215 have hcross :
1216 (2 : ℝ) * ((2 * wallpaper_groups + n : ℕ) : ℝ) = (37 : ℝ) * (k : ℝ) := by
1217 have htmp := hcoeff
1218 field_simp [hk_ne] at htmp
1219 nlinarith [htmp]
1220 have hD3 : D = 3 := by native_decide
1221 have hA_le : 2 * wallpaper_groups + n ≤ 37 := by
1222 have hn3 : n ≤ 3 := by simpa [hD3] using hn_le
1223 calc
1224 2 * wallpaper_groups + n ≤ 2 * wallpaper_groups + 3 := Nat.add_le_add_left hn3 _
1225 _ = 37 := by native_decide
1226 have hA_leR : ((2 * wallpaper_groups + n : ℕ) : ℝ) ≤ 37 := by
1227 exact_mod_cast hA_le
1228 have hk_le_twoR : (k : ℝ) ≤ 2 := by
1229 nlinarith [hcross, hA_leR]
1230 have hk_le_two : k ≤ 2 := by exact_mod_cast hk_le_twoR
1231 have hcrossNat : 2 * (2 * wallpaper_groups + n) = 37 * k := by
1232 exact_mod_cast hcross
1233 have hk_ne_one : k ≠ 1 := by
1234 intro hk1
1235 have hcontra : 2 * (2 * wallpaper_groups + n) = 37 := by
1236 simpa [hk1] using hcrossNat
1237 omega
1238 have hk_cases : k = 1 ∨ k = 2 := by
1239 have hk_ge_one : 1 ≤ k := Nat.succ_le_of_lt hk
1240 omega
1241 have hk_two : k = 2 := by
1242 rcases hk_cases with hk1 | hk2
1243 · exact (hk_ne_one hk1).elim
1244 · exact hk2
1245 have hA_eq37 : 2 * wallpaper_groups + n = 37 := by
1246 have h74 : 2 * (2 * wallpaper_groups + n) = 74 := by
1247 simpa [hk_two] using hcrossNat
1248 omega
1249 have hW17 : wallpaper_groups = 17 := by native_decide
1250 have hn3 : n = 3 := by
1251 omega
1252 have hnD : n = D := by
1253 calc
1254 n = 3 := hn3
1255 _ = D := by simp [hD3]
1256 exact ⟨hk_two, hnD⟩
1257
1258/-- Positivity-free Diophantine forcing for the `μ→τ` coefficient family:
1259 with `n ≤ D`, canonical matching in `F - ((2W+n)/k)α` still forces
1260 `k = 2` and `n = D`, deriving denominator positivity from the match itself. -/
1261theorem step_mu_tau_kn_forced_under_dim_bound_no_hk
1262 {k n : ℕ} (hn_le : n ≤ D)
1263 (h : step_mu_tau =
1264 (cube_faces D : ℝ) - ((((2 * wallpaper_groups + n : ℕ) : ℝ) / (k : ℝ)) * alpha)) :
1265 k = 2 ∧ n = D := by
1266 have hk : 0 < k := by
1267 by_cases hk0 : k = 0
1268 · subst hk0
1269 have hface : step_mu_tau = (cube_faces D : ℝ) := by
1270 simpa using h
1271 have hcanon : step_mu_tau =
1272 (cube_faces D : ℝ) - ((37 : ℝ) / 2) * alpha := by
1273 calc
1274 step_mu_tau = (6 : ℝ) - ((37 : ℝ) / 2) * alpha := step_mu_tau_channel_split
1275 _ = (cube_faces D : ℝ) - ((37 : ℝ) / 2) * alpha := by
1276 norm_num [cube_faces, D]
1277 have hα_bounds := Physics.ElectronMass.Necessity.alpha_bounds
1278 have hα_pos : 0 < alpha := by linarith [hα_bounds.1]
1279 linarith [hface, hcanon, hα_pos]
1280 · exact Nat.pos_of_ne_zero hk0
1281 exact step_mu_tau_kn_forced_under_dim_bound hk hn_le h
1282
1283/-- Under dimensional band `n ≤ D`, canonical matching in `F - ((2W+n)/k)α`
1284 makes denominator and numerator slots equivalent: `k = 2 ↔ n = D`. -/
1285theorem step_mu_tau_denominator_iff_numerator_under_dim_bound
1286 {k n : ℕ} (hk : 0 < k) (hn_le : n ≤ D)
1287 (h : step_mu_tau =
1288 (cube_faces D : ℝ) - ((((2 * wallpaper_groups + n : ℕ) : ℝ) / (k : ℝ)) * alpha)) :
1289 k = 2 ↔ n = D := by
1290 have hkn : k = 2 ∧ n = D := step_mu_tau_kn_forced_under_dim_bound hk hn_le h
1291 constructor
1292 · intro _hk2
1293 exact hkn.2
1294 · intro _hnD
1295 exact hkn.1
1296
1297/-- Positivity-free denominator/numerator slot equivalence for `μ→τ`:
1298 with `n ≤ D`, canonical matching still packages `k = 2 ↔ n = D` without an
1299 explicit `k > 0` premise. -/
1300theorem step_mu_tau_denominator_iff_numerator_under_dim_bound_no_hk
1301 {k n : ℕ} (hn_le : n ≤ D)
1302 (h : step_mu_tau =
1303 (cube_faces D : ℝ) - ((((2 * wallpaper_groups + n : ℕ) : ℝ) / (k : ℝ)) * alpha)) :
1304 k = 2 ↔ n = D := by
1305 have hkn : k = 2 ∧ n = D := step_mu_tau_kn_forced_under_dim_bound_no_hk hn_le h
1306 constructor
1307 · intro _hk2
1308 exact hkn.2
1309 · intro _hnD
1310 exact hkn.1
1311
1312/-- Cross-sector positivity-free integer-family iff packaging:
1313 combines `e→μ` mixed-slot equivalence and `μ→τ` denominator/numerator
1314 equivalence into a single bundled statement. -/
1315theorem lepton_integer_slot_iff_bundle_no_hk
1316 {k_e : ℕ} {q : ℝ} {k_mu n : ℕ}
1317 (h_e : step_e_mu = (E_passive : ℝ) + 1 / ((k_e : ℝ) * Real.pi) - q * correction_order_2)
1318 (hn_le : n ≤ D)
1319 (h_mu : step_mu_tau =
1320 (cube_faces D : ℝ) - ((((2 * wallpaper_groups + n : ℕ) : ℝ) / (k_mu : ℝ)) * alpha)) :
1321 (k_e = 4 ↔ q = 1) ∧ (k_mu = 2 ↔ n = D) := by
1322 refine ⟨?_, ?_⟩
1323 · exact step_e_mu_denominator_iff_quadratic_scale_no_hk h_e
1324 · exact step_mu_tau_denominator_iff_numerator_under_dim_bound_no_hk hn_le h_mu
1325
1326/-- Under dimensional band `n ≤ D`, canonical matching in `F - ((2W+n)/k)α`
1327 makes coefficient-slot and canonical integer pair equivalent:
1328 `((2W+n)/k) = 37/2 ↔ (k = 2 ∧ n = D)`. -/
1329theorem step_mu_tau_coeff_iff_kn_under_dim_bound
1330 {k n : ℕ} (hk : 0 < k) (hn_le : n ≤ D)
1331 (h : step_mu_tau =
1332 (cube_faces D : ℝ) - ((((2 * wallpaper_groups + n : ℕ) : ℝ) / (k : ℝ)) * alpha)) :
1333 (((2 * wallpaper_groups + n : ℕ) : ℝ) / (k : ℝ) = (37 : ℝ) / 2) ↔
1334 (k = 2 ∧ n = D) := by
1335 constructor
1336 · intro _hcoeff
1337 exact step_mu_tau_kn_forced_under_dim_bound hk hn_le h
1338 · intro hkn
1339 rcases hkn with ⟨hk2, hnD⟩
1340 have hnum : ((2 * wallpaper_groups + n : ℕ) : ℝ) = (37 : ℝ) := by
1341 calc
1342 ((2 * wallpaper_groups + n : ℕ) : ℝ)
1343 = ((2 * wallpaper_groups + D : ℕ) : ℝ) := by simp [hnD]
1344 _ = (37 : ℝ) := by norm_num [wallpaper_groups, D]
1345 calc
1346 (((2 * wallpaper_groups + n : ℕ) : ℝ) / (k : ℝ))
1347 = (37 : ℝ) / (k : ℝ) := by simp [hnum]
1348 _ = (37 : ℝ) / 2 := by simp [hk2]
1349
1350/-- Positivity-free coefficient-slot equivalence for `μ→τ`:
1351 with `n ≤ D`, canonical matching still packages
1352 `((2W+n)/k = 37/2) ↔ (k = 2 ∧ n = D)` without an explicit `k > 0` premise. -/
1353theorem step_mu_tau_coeff_iff_kn_under_dim_bound_no_hk
1354 {k n : ℕ} (hn_le : n ≤ D)
1355 (h : step_mu_tau =
1356 (cube_faces D : ℝ) - ((((2 * wallpaper_groups + n : ℕ) : ℝ) / (k : ℝ)) * alpha)) :
1357 (((2 * wallpaper_groups + n : ℕ) : ℝ) / (k : ℝ) = (37 : ℝ) / 2) ↔
1358 (k = 2 ∧ n = D) := by
1359 constructor
1360 · intro _hcoeff
1361 exact step_mu_tau_kn_forced_under_dim_bound_no_hk hn_le h
1362 · intro hkn
1363 rcases hkn with ⟨hk2, hnD⟩
1364 have hnum : ((2 * wallpaper_groups + n : ℕ) : ℝ) = (37 : ℝ) := by
1365 calc
1366 ((2 * wallpaper_groups + n : ℕ) : ℝ)
1367 = ((2 * wallpaper_groups + D : ℕ) : ℝ) := by simp [hnD]
1368 _ = (37 : ℝ) := by norm_num [wallpaper_groups, D]
1369 calc
1370 (((2 * wallpaper_groups + n : ℕ) : ℝ) / (k : ℝ))
1371 = (37 : ℝ) / (k : ℝ) := by simp [hnum]
1372 _ = (37 : ℝ) / 2 := by simp [hk2]
1373
1374/-- Packaged full-family coefficient-slot equivalence for constrained `μ→τ` families:
1375 with face-term role fixed and dimensional band `n ≤ D`, canonical matching in
1376 `f - ((2W+n)/k)α` forces `f = 6` and packages
1377 `((2W+n)/k = 37/2) ↔ (k = 2 ∧ n = D)`. -/
1378theorem step_mu_tau_full_family_coeff_iff_under_dim_bound
1379 {f : ℝ} {k n : ℕ} (hk : 0 < k) (hn_le : n ≤ D)
1380 (hf : f = (cube_faces D : ℝ))
1381 (h : step_mu_tau = f - ((((2 * wallpaper_groups + n : ℕ) : ℝ) / (k : ℝ)) * alpha)) :
1382 f = 6 ∧
1383 ((((2 * wallpaper_groups + n : ℕ) : ℝ) / (k : ℝ) = (37 : ℝ) / 2) ↔
1384 (k = 2 ∧ n = D)) := by
1385 have h' : step_mu_tau =
1386 (cube_faces D : ℝ) - ((((2 * wallpaper_groups + n : ℕ) : ℝ) / (k : ℝ)) * alpha) := by
1387 simpa [hf] using h
1388 have hcoeffiff :
1389 ((((2 * wallpaper_groups + n : ℕ) : ℝ) / (k : ℝ) = (37 : ℝ) / 2) ↔
1390 (k = 2 ∧ n = D)) :=
1391 step_mu_tau_coeff_iff_kn_under_dim_bound hk hn_le h'
1392 have hf6 : f = 6 := by
1393 calc
1394 f = (cube_faces D : ℝ) := hf
1395 _ = 6 := by norm_num [cube_faces, D]
1396 exact ⟨hf6, hcoeffiff⟩
1397
1398/-- Positivity-free packaged full-family coefficient-slot equivalence for
1399 constrained `μ→τ` families:
1400 with face-term role fixed and `n ≤ D`, canonical matching in
1401 `f - ((2W+n)/k)α` forces `f = 6` and packages
1402 `((2W+n)/k = 37/2) ↔ (k = 2 ∧ n = D)` without explicit `k > 0`. -/
1403theorem step_mu_tau_full_family_coeff_iff_under_dim_bound_no_hk
1404 {f : ℝ} {k n : ℕ} (hn_le : n ≤ D)
1405 (hf : f = (cube_faces D : ℝ))
1406 (h : step_mu_tau = f - ((((2 * wallpaper_groups + n : ℕ) : ℝ) / (k : ℝ)) * alpha)) :
1407 f = 6 ∧
1408 ((((2 * wallpaper_groups + n : ℕ) : ℝ) / (k : ℝ) = (37 : ℝ) / 2) ↔
1409 (k = 2 ∧ n = D)) := by
1410 have h' : step_mu_tau =
1411 (cube_faces D : ℝ) - ((((2 * wallpaper_groups + n : ℕ) : ℝ) / (k : ℝ)) * alpha) := by
1412 simpa [hf] using h
1413 have hcoeffiff :
1414 ((((2 * wallpaper_groups + n : ℕ) : ℝ) / (k : ℝ) = (37 : ℝ) / 2) ↔
1415 (k = 2 ∧ n = D)) :=
1416 step_mu_tau_coeff_iff_kn_under_dim_bound_no_hk hn_le h'
1417 have hf6 : f = 6 := by
1418 calc
1419 f = (cube_faces D : ℝ) := hf
1420 _ = 6 := by norm_num [cube_faces, D]
1421 exact ⟨hf6, hcoeffiff⟩
1422
1423/-- Assumption-reduced coefficient equivalence for constrained `μ→τ` families:
1424 under dimensional band `n ≤ D`, canonical matching in `f - ((2W+n)/k)α`
1425 makes coefficient-slot matching equivalent to full canonical closure:
1426 `((2W+n)/k = 37/2) ↔ (f = 6 ∧ k = 2 ∧ n = D)`. -/
1427theorem step_mu_tau_coeff_iff_full_forced_under_dim_bound
1428 {f : ℝ} {k n : ℕ} (hk : 0 < k) (hn_le : n ≤ D)
1429 (h : step_mu_tau = f - ((((2 * wallpaper_groups + n : ℕ) : ℝ) / (k : ℝ)) * alpha)) :
1430 ((((2 * wallpaper_groups + n : ℕ) : ℝ) / (k : ℝ) = (37 : ℝ) / 2) ↔
1431 (f = 6 ∧ k = 2 ∧ n = D)) := by
1432 constructor
1433 · intro hcoeff
1434 have hface : step_mu_tau = f - ((37 : ℝ) / 2) * alpha := by
1435 calc
1436 step_mu_tau = f - ((((2 * wallpaper_groups + n : ℕ) : ℝ) / (k : ℝ)) * alpha) := h
1437 _ = f - ((37 : ℝ) / 2) * alpha := by rw [hcoeff]
1438 have hf6 : f = 6 := step_mu_tau_face_count_forced hface
1439 have hfCube : f = (cube_faces D : ℝ) := by
1440 calc
1441 f = 6 := hf6
1442 _ = (cube_faces D : ℝ) := by norm_num [cube_faces, D]
1443 have h' : step_mu_tau =
1444 (cube_faces D : ℝ) - ((((2 * wallpaper_groups + n : ℕ) : ℝ) / (k : ℝ)) * alpha) := by
1445 simpa [hfCube] using h
1446 have hkn : k = 2 ∧ n = D := step_mu_tau_kn_forced_under_dim_bound hk hn_le h'
1447 exact ⟨hf6, hkn.1, hkn.2⟩
1448 · intro hfull
1449 rcases hfull with ⟨hf6, hk2, hnD⟩
1450 have hnum : ((2 * wallpaper_groups + n : ℕ) : ℝ) = (37 : ℝ) := by
1451 calc
1452 ((2 * wallpaper_groups + n : ℕ) : ℝ)
1453 = ((2 * wallpaper_groups + D : ℕ) : ℝ) := by simp [hnD]
1454 _ = (37 : ℝ) := by norm_num [wallpaper_groups, D]
1455 calc
1456 (((2 * wallpaper_groups + n : ℕ) : ℝ) / (k : ℝ))
1457 = (37 : ℝ) / (k : ℝ) := by simp [hnum]
1458 _ = (37 : ℝ) / 2 := by simp [hk2]
1459
1460/-- Assumption-reduced variant of coefficient-match forcing:
1461 denominator positivity is derived from the coefficient equation itself, so
1462 `k > 0` need not be assumed explicitly. -/
1463theorem step_mu_tau_full_family_forced_from_coeff_match_no_hk
1464 {f : ℝ} {k n : ℕ} (hn_le : n ≤ D)
1465 (hcoeff : (((2 * wallpaper_groups + n : ℕ) : ℝ) / (k : ℝ)) = (37 : ℝ) / 2)
1466 (h : step_mu_tau = f - ((((2 * wallpaper_groups + n : ℕ) : ℝ) / (k : ℝ)) * alpha)) :
1467 f = 6 ∧ k = 2 ∧ n = D := by
1468 have hk : 0 < k := by
1469 by_cases hk0 : k = 0
1470 · subst hk0
1471 have hfalse : (0 : ℝ) = (37 : ℝ) / 2 := by simpa using hcoeff
1472 norm_num at hfalse
1473 · exact Nat.pos_of_ne_zero hk0
1474 have hiff :
1475 ((((2 * wallpaper_groups + n : ℕ) : ℝ) / (k : ℝ) = (37 : ℝ) / 2) ↔
1476 (f = 6 ∧ k = 2 ∧ n = D)) :=
1477 step_mu_tau_coeff_iff_full_forced_under_dim_bound hk hn_le h
1478 exact hiff.mp hcoeff
1479
1480/-- Assumption-reduced coefficient equivalence:
1481 with dimensional band `n ≤ D`, canonical matching in `f - ((2W+n)/k)α`
1482 gives `((2W+n)/k = 37/2) ↔ (f = 6 ∧ k = 2 ∧ n = D)` without an explicit
1483 `k > 0` premise. -/
1484theorem step_mu_tau_coeff_iff_full_forced_under_dim_bound_no_hk
1485 {f : ℝ} {k n : ℕ} (hn_le : n ≤ D)
1486 (h : step_mu_tau = f - ((((2 * wallpaper_groups + n : ℕ) : ℝ) / (k : ℝ)) * alpha)) :
1487 ((((2 * wallpaper_groups + n : ℕ) : ℝ) / (k : ℝ) = (37 : ℝ) / 2) ↔
1488 (f = 6 ∧ k = 2 ∧ n = D)) := by
1489 constructor
1490 · intro hcoeff
1491 exact step_mu_tau_full_family_forced_from_coeff_match_no_hk hn_le hcoeff h
1492 · intro hfull
1493 rcases hfull with ⟨_hf6, hk2, hnD⟩
1494 have hnum : ((2 * wallpaper_groups + n : ℕ) : ℝ) = (37 : ℝ) := by
1495 calc
1496 ((2 * wallpaper_groups + n : ℕ) : ℝ)
1497 = ((2 * wallpaper_groups + D : ℕ) : ℝ) := by simp [hnD]
1498 _ = (37 : ℝ) := by norm_num [wallpaper_groups, D]
1499 calc
1500 (((2 * wallpaper_groups + n : ℕ) : ℝ) / (k : ℝ))
1501 = (37 : ℝ) / (k : ℝ) := by simp [hnum]
1502 _ = (37 : ℝ) / 2 := by simp [hk2]
1503
1504/-- Packaged equivalence closure for constrained `μ→τ` families:
1505 with face-term role fixed and dimensional band `n ≤ D`, canonical matching in
1506 `f - ((2W+n)/k)α` forces `f = 6` and equivalently `k = 2 ↔ n = D`. -/
1507theorem step_mu_tau_full_family_iff_under_dim_bound
1508 {f : ℝ} {k n : ℕ} (hk : 0 < k) (hn_le : n ≤ D)
1509 (hf : f = (cube_faces D : ℝ))
1510 (h : step_mu_tau = f - ((((2 * wallpaper_groups + n : ℕ) : ℝ) / (k : ℝ)) * alpha)) :
1511 f = 6 ∧ (k = 2 ↔ n = D) := by
1512 have h' : step_mu_tau =
1513 (cube_faces D : ℝ) - ((((2 * wallpaper_groups + n : ℕ) : ℝ) / (k : ℝ)) * alpha) := by
1514 simpa [hf] using h
1515 have hiff : k = 2 ↔ n = D :=
1516 step_mu_tau_denominator_iff_numerator_under_dim_bound hk hn_le h'
1517 have hf6 : f = 6 := by
1518 calc
1519 f = (cube_faces D : ℝ) := hf
1520 _ = 6 := by norm_num [cube_faces, D]
1521 exact ⟨hf6, hiff⟩
1522
1523/-- Positivity-free packaged equivalence closure for constrained `μ→τ` families:
1524 with face-term role fixed and `n ≤ D`, canonical matching in
1525 `f - ((2W+n)/k)α` forces `f = 6` and packages `k = 2 ↔ n = D`
1526 without explicit `k > 0`. -/
1527theorem step_mu_tau_full_family_iff_under_dim_bound_no_hk
1528 {f : ℝ} {k n : ℕ} (hn_le : n ≤ D)
1529 (hf : f = (cube_faces D : ℝ))
1530 (h : step_mu_tau = f - ((((2 * wallpaper_groups + n : ℕ) : ℝ) / (k : ℝ)) * alpha)) :
1531 f = 6 ∧ (k = 2 ↔ n = D) := by
1532 have h' : step_mu_tau =
1533 (cube_faces D : ℝ) - ((((2 * wallpaper_groups + n : ℕ) : ℝ) / (k : ℝ)) * alpha) := by
1534 simpa [hf] using h
1535 have hiff : k = 2 ↔ n = D :=
1536 step_mu_tau_denominator_iff_numerator_under_dim_bound_no_hk hn_le h'
1537 have hf6 : f = 6 := by
1538 calc
1539 f = (cube_faces D : ℝ) := hf
1540 _ = 6 := by norm_num [cube_faces, D]
1541 exact ⟨hf6, hiff⟩
1542
1543/-- Packaged constrained-family forcing for `μ→τ`:
1544 with face-term role fixed and `n ≤ D`, canonical matching in
1545 `f - ((2W+n)/k)α` forces `f = 6`, `k = 2`, and `n = D`. -/
1546theorem step_mu_tau_full_family_forced_under_dim_bound
1547 {f : ℝ} {k n : ℕ} (hk : 0 < k) (hn_le : n ≤ D)
1548 (hf : f = (cube_faces D : ℝ))
1549 (h : step_mu_tau = f - ((((2 * wallpaper_groups + n : ℕ) : ℝ) / (k : ℝ)) * alpha)) :
1550 f = 6 ∧ k = 2 ∧ n = D := by
1551 have h' : step_mu_tau =
1552 (cube_faces D : ℝ) - ((((2 * wallpaper_groups + n : ℕ) : ℝ) / (k : ℝ)) * alpha) := by
1553 simpa [hf] using h
1554 have hkn : k = 2 ∧ n = D := step_mu_tau_kn_forced_under_dim_bound hk hn_le h'
1555 have hf6 : f = 6 := by
1556 calc
1557 f = (cube_faces D : ℝ) := hf
1558 _ = 6 := by norm_num [cube_faces, D]
1559 exact ⟨hf6, hkn.1, hkn.2⟩
1560
1561/-- Positivity-free packaged constrained-family forcing for `μ→τ`:
1562 with face-term role fixed and `n ≤ D`, canonical matching in
1563 `f - ((2W+n)/k)α` forces `f = 6`, `k = 2`, and `n = D`
1564 without explicit `k > 0`. -/
1565theorem step_mu_tau_full_family_forced_under_dim_bound_no_hk
1566 {f : ℝ} {k n : ℕ} (hn_le : n ≤ D)
1567 (hf : f = (cube_faces D : ℝ))
1568 (h : step_mu_tau = f - ((((2 * wallpaper_groups + n : ℕ) : ℝ) / (k : ℝ)) * alpha)) :
1569 f = 6 ∧ k = 2 ∧ n = D := by
1570 have h' : step_mu_tau =
1571 (cube_faces D : ℝ) - ((((2 * wallpaper_groups + n : ℕ) : ℝ) / (k : ℝ)) * alpha) := by
1572 simpa [hf] using h
1573 have hkn : k = 2 ∧ n = D := step_mu_tau_kn_forced_under_dim_bound_no_hk hn_le h'
1574 have hf6 : f = 6 := by
1575 calc
1576 f = (cube_faces D : ℝ) := hf
1577 _ = 6 := by norm_num [cube_faces, D]
1578 exact ⟨hf6, hkn.1, hkn.2⟩
1579
1580/-- Complementary packaged forcing for `μ→τ` from canonical coefficient match:
1581 with dimensional band `n ≤ D`, if the coefficient slot equals `37/2` in
1582 `f - ((2W+n)/k)α`, then canonical matching forces `f = 6`, `k = 2`, and `n = D`. -/
1583theorem step_mu_tau_full_family_forced_from_coeff_match
1584 {f : ℝ} {k n : ℕ} (hk : 0 < k) (hn_le : n ≤ D)
1585 (hcoeff : (((2 * wallpaper_groups + n : ℕ) : ℝ) / (k : ℝ)) = (37 : ℝ) / 2)
1586 (h : step_mu_tau = f - ((((2 * wallpaper_groups + n : ℕ) : ℝ) / (k : ℝ)) * alpha)) :
1587 f = 6 ∧ k = 2 ∧ n = D := by
1588 have hface : step_mu_tau = f - ((37 : ℝ) / 2) * alpha := by
1589 calc
1590 step_mu_tau = f - ((((2 * wallpaper_groups + n : ℕ) : ℝ) / (k : ℝ)) * alpha) := h
1591 _ = f - ((37 : ℝ) / 2) * alpha := by rw [hcoeff]
1592 have hf6 : f = 6 := step_mu_tau_face_count_forced hface
1593 have hfCube : f = (cube_faces D : ℝ) := by
1594 calc
1595 f = 6 := hf6
1596 _ = (cube_faces D : ℝ) := by norm_num [cube_faces, D]
1597 have h' : step_mu_tau =
1598 (cube_faces D : ℝ) - ((((2 * wallpaper_groups + n : ℕ) : ℝ) / (k : ℝ)) * alpha) := by
1599 simpa [hfCube] using h
1600 have hkn : k = 2 ∧ n = D := step_mu_tau_kn_forced_under_dim_bound hk hn_le h'
1601 exact ⟨hf6, hkn.1, hkn.2⟩
1602
1603/-- O4 closure certificate (channel-level form):
1604 electron-break refinement splits into canonical geometric + radiative channels,
1605 and both generation steps are in canonical forced forms. -/
1606theorem o4_channel_closure_certificate :
1607 refined_shift = (2 * (W : ℝ) + (ledger_fraction : ℝ)) + (alpha ^ 2 + 12 * alpha ^ 3) ∧
1608 step_e_mu = (E_passive : ℝ) + 1 / (4 * Real.pi) - correction_order_2 ∧
1609 step_mu_tau = (cube_faces D : ℝ) - ((37 : ℝ) / 2) * alpha := by
1610 refine ⟨?_, step_e_mu_channel_split, ?_⟩
1611 · calc
1612 refined_shift = base_shift + (alpha ^ 2 + 12 * alpha ^ 3) := refined_shift_channel_form
1613 _ = (2 * (W : ℝ) + (ledger_fraction : ℝ)) + (alpha ^ 2 + 12 * alpha ^ 3) := by
1614 simp [base_shift]
1615 · calc
1616 step_mu_tau = (6 : ℝ) - ((37 : ℝ) / 2) * alpha := step_mu_tau_channel_split
1617 _ = (cube_faces D : ℝ) - ((37 : ℝ) / 2) * alpha := by
1618 norm_num [cube_faces, D]
1619
1620/-- O4 closure certificate (coefficient slots):
1621 canonical integer/rational slots are forced in the primary one-parameter
1622 constrained families used for the lepton chain. -/
1623theorem o4_slot_forcing_certificate :
1624 ledger_fraction = (29 : ℚ) / 44 ∧
1625 step_mu_tau = (cube_faces D : ℝ) - ((((2 * wallpaper_groups + D : ℕ) : ℝ) / 2) * alpha) ∧
1626 step_e_mu = (E_passive : ℝ) + 1 / (4 * Real.pi) - correction_order_2 := by
1627 refine ⟨ledger_fraction_eq_29_over_44, ?_, step_e_mu_channel_split⟩
1628 simp [step_mu_tau]
1629
1630end
1631end JCostPerturbation
1632end Masses
1633end IndisputableMonolith
1634