IndisputableMonolith.Verification.Item8ClosureTarget
IndisputableMonolith/Verification/Item8ClosureTarget.lean · 1069 lines · 102 declarations
show as:
view math explainer →
1import Mathlib
2import IndisputableMonolith.Constants
3import IndisputableMonolith.Constants.Alpha
4import IndisputableMonolith.Physics.RunningCouplings
5
6/-!
7# Item 8 Closure Target — Unified Sub-Leading Mass Formula
8
9This module develops the smallest precise theorem framework that would close the
10open quark sub-leading correction item (Item 8) and make the all-sector
11generalization falsifiable.
12
13## Summary of Results
14
15### Proved (sorry-free)
16
171. **`consistency_of_ratioFamily`**: The sign-split family forces
18 `gen12·s₁₂ + gen23·s₂₃ = 0` — a structural rigidity that PDG data violates.
19
202. **`etaFromData` + `etaL_gen12_identity` + `etaL_gen23_identity`**:
21 Closed-form η formula absorbs the consistency violation:
22 `η = (g₁₂·s₁₂ + g₂₃·s₂₃) / (ln(s₁₂/s₂₃) · (g₁₂·s₁₂ − g₂₃·s₂₃))`
23 with algebraic identities `1 + η·L = 2·g₁₂·s₁₂/D` and `1 − η·L = −2·g₂₃·s₂₃/D`.
24
253. **`refinedFamily_neg_solvable` / `refinedFamily_pos_solvable`**:
26 For any residual pair with nonzero gen12, non-degenerate cross-difference,
27 distinct steps, and nonzero coupling, the refined family has a solution.
28 Constructive proof via explicit coefficient formulas.
29
304. **`refinedFamily_neg_unique` / `refinedFamily_pos_unique`**:
31 If two coefficient sets produce identical refined-family outputs on a given
32 signature, their active coefficient `c` and `eta` must agree.
33 Proof via `calc`+`ring` to cancel common factors, then `linarith` for the
34 addition step and `mul_left_cancel₀`/`mul_right_cancel₀` for cancellation.
35 Combined with solvability (item 3), this gives **`∃!` for each sector**.
36
375. **`refined_neg_sector_closure`**: Full `∃!` for any `.neg` sector:
38 there exist unique `(c, η)` matching the data, and any solution (with
39 arbitrary `cPos`) must have the same `(c, η)`. Combines items 3–4 with
40 a helper `neg_cPos_irrelevant` showing `cPos` is unused for `.neg`.
41
426. **`signClass_collapse_to_refined`**: Sign-class family collapses to the
43 refined family when both η values agree.
44
45### Documented obstructions
46
47* **Universal η**: The 3-parameter refined family (universal η) is
48 unsatisfiable with mixed-scheme PDG quark data: η_up = −2.72 vs η_dn = −0.88
49 (3.1× disagreement).
50
51* **Mixed-scheme artifact**: LO QCD running reveals that the "universal sign
52 pattern" (δ₁₂ > 0, δ₂₃ < 0) is partly an artifact of comparing masses at
53 different renormalization scales. The c/u SDGT step of 13 is nearly exact
54 at a common scale (δ₁₂ ≈ −0.01).
55
56* **Lepton benchmark**: Leptons — with scheme-free pole masses — give
57 perturbative η = +0.065 (|η·L| ≈ 4%), validating the family form.
58
59### Strategy
60
61The lepton-anchored approach fixes η and cNeg from the two scheme-free lepton
62equations, then predicts anchor-scale quark residuals as genuine out-of-sample
63tests. The `RunningCouplings` module now provides LO mass transport with
64threshold matching (`transport_mass_through`); quark closure awaits NLO
65refinement of the running to reduce residual scheme dependence.
66
67## Interface
68
69* A sign class induced by `B_pow`
70* The ordered SDGT step pair `(step12, step23)` — sector-specific rung spacings
71 from the Q₃ cube decomposition
72* One coupling scalar `kappa`
73
74## Concrete data (§ ConcreteInstantiation)
75
76* PDG 2022 quark masses at mixed reference scales
77 (u,d,s at 2 GeV MS-bar; c at m_c; b at m_b; t pole)
78* Charged-lepton pole masses (scheme-free)
79* α_s = 2/17 from wallpaper-group fraction (proved in StrongForce)
80* Rung-unit residuals: δ = log_φ(observed ratio) − SDGT step
81
82### Approximate residual values (mixed-scheme PDG)
83
84| Sector | gen12 step | δ₁₂ (rungs) | gen23 step | δ₂₃ (rungs) | η |
85|--------|-----------|-------------|-----------|-------------|-------|
86| Up | 13 | +0.25 | 11 | −0.79 | −2.72 |
87| Down | 6 | +0.23 | 8 | −0.10 | −0.88 |
88| Lepton | 11 | +0.08 | 6 | −0.13 | +0.06 |
89
90Lepton η is perturbative (4%); quark η values are inflated by mixed-scale
91PDG artifacts, especially the t/c ratio (pole mass vs MS-bar at m_c).
92-/
93
94namespace IndisputableMonolith
95namespace Verification
96namespace Item8ClosureTarget
97
98/-- Sign class induced by the sign of `B_pow`. -/
99inductive BpowSign | neg | pos
100 deriving DecidableEq, Repr
101
102/-- Minimal structural signature for a sector's sub-leading correction law.
103 `step12` and `step23` are the sector-specific SDGT rung spacings
104 (cube-cell counts from the Q₃ decomposition). -/
105structure ResidualSignature where
106 sign : BpowSign
107 step12 : ℕ
108 step23 : ℕ
109 coupling : ℝ
110 step12_pos : 0 < step12
111 step23_pos : 0 < step23
112
113/-- Two sub-leading rung corrections: generation `1 → 2` and `2 → 3`. -/
114@[ext]
115structure ResidualPair where
116 gen12 : ℝ
117 gen23 : ℝ
118
119/-- The two global coefficients allowed by the smallest sign-split candidate family. -/
120structure RatioFamilyCoeffs where
121 cNeg : ℝ
122 cPos : ℝ
123
124/-- Negative-`B_pow` lepton signature, using the derived SDGT pair `(11, 6)`. -/
125def leptonSignature (kappa : ℝ) : ResidualSignature where
126 sign := .neg
127 step12 := 11
128 step23 := 6
129 coupling := kappa
130 step12_pos := by decide
131 step23_pos := by decide
132
133/-- Negative-`B_pow` up-quark signature, using the derived SDGT pair `(13, 11)`. -/
134def upQuarkSignature (kappa : ℝ) : ResidualSignature where
135 sign := .neg
136 step12 := 13
137 step23 := 11
138 coupling := kappa
139 step12_pos := by decide
140 step23_pos := by decide
141
142/-- Positive-`B_pow` down-quark signature, using the derived SDGT pair `(6, 8)`. -/
143def downQuarkSignature (kappa : ℝ) : ResidualSignature where
144 sign := .pos
145 step12 := 6
146 step23 := 8
147 coupling := kappa
148 step12_pos := by decide
149 step23_pos := by decide
150
151/-- Sign-split ratio family: the smallest closed-form candidate using only
152
1531. `sign(B_pow)` → selects `cNeg` or `cPos`
1542. the ordered SDGT step pair → weights the correction via step fraction
1553. one coupling scalar κ
156
157The gen-1→2 correction inherits the sign of `c`; the gen-2→3 correction
158inherits `−c`. This captures the universal empirical pattern δ₁₂ > 0,
159δ₂₃ < 0 when `c > 0`. -/
160noncomputable def ratioFamily (coeffs : RatioFamilyCoeffs)
161 (sig : ResidualSignature) : ResidualPair :=
162 let c :=
163 match sig.sign with
164 | .neg => coeffs.cNeg
165 | .pos => coeffs.cPos
166 let total := (sig.step12 : ℝ) + (sig.step23 : ℝ)
167 { gen12 := c * sig.coupling * (sig.step23 : ℝ) / total
168 , gen23 := -(c * sig.coupling * (sig.step12 : ℝ) / total)
169 }
170
171/-- The exact prediction produced by the candidate family for any signature. -/
172noncomputable def predictedResiduals (coeffs : RatioFamilyCoeffs)
173 (sig : ResidualSignature) : ResidualPair :=
174 ratioFamily coeffs sig
175
176/-- Equal structural signatures give equal predictions. This is the precise
177no-extra-knob property needed for later out-of-sample tests. -/
178theorem same_signature_same_prediction
179 (coeffs : RatioFamilyCoeffs) {sig1 sig2 : ResidualSignature}
180 (h : sig1 = sig2) :
181 predictedResiduals coeffs sig1 = predictedResiduals coeffs sig2 := by
182 subst h; rfl
183
184/-- Smallest precise target that would close Item 8.
185
186`upExact` and `downExact` are the exact quark residual pairs once derived.
187Proving this proposition would do two things:
188
1891. close Item 8 by fixing both quark residual pairs inside one closed family
1902. freeze the two global coefficients `(cNeg, cPos)`, making every later
191 lepton / genetic / theta instantiation an out-of-sample test rather than a
192 new fit
193-/
194def item8ClosureTarget
195 (upExact downExact : ResidualPair)
196 (kappaUp kappaDown : ℝ) : Prop :=
197 ∃! coeffs : RatioFamilyCoeffs,
198 predictedResiduals coeffs (upQuarkSignature kappaUp) = upExact ∧
199 predictedResiduals coeffs (downQuarkSignature kappaDown) = downExact
200
201/-! ## Structural Obstruction of the Sign-Split Family
202
203The sign-split family satisfies a rigid algebraic constraint: for any
204signature, the cross-product `gen12 · step12 + gen23 · step23 = 0`.
205This is a **necessary condition** for the family to match any given
206residual pair. Numerically:
207
208| Sector | gen12·s₁₂ + gen23·s₂₃ | violation |
209|--------|----------------------|-----------|
210| Lepton | +0.066 | 3.9% |
211| Down | +0.546 | 25.3% |
212| Up | −5.439 | 45.4% |
213
214The lepton data nearly satisfies the condition (scheme-free pole masses);
215the quark violations are larger, partly because PDG values mix scales.
216The up-quark t/c ratio (pole vs MS-bar at m_c) is the main outlier.
217-/
218
219theorem consistency_of_ratioFamily
220 (coeffs : RatioFamilyCoeffs) (sig : ResidualSignature) :
221 (ratioFamily coeffs sig).gen12 * (sig.step12 : ℝ) +
222 (ratioFamily coeffs sig).gen23 * (sig.step23 : ℝ) = 0 := by
223 obtain ⟨sign, s12, s23, κ, hs12, hs23⟩ := sig
224 unfold ratioFamily
225 dsimp only [ResidualPair.gen12, ResidualPair.gen23]
226 have htotal : (s12 : ℝ) + (s23 : ℝ) ≠ 0 := by
227 have : (0 : ℝ) < (s12 : ℝ) := Nat.cast_pos.mpr hs12
228 have : (0 : ℝ) < (s23 : ℝ) := Nat.cast_pos.mpr hs23
229 linarith
230 cases sign <;> simp only [] <;> field_simp [htotal] <;> ring
231
232/-- If the sign-split family matches a residual pair, that pair must satisfy
233 the cross-product identity. Contrapositive: if the identity fails,
234 no coefficients can make the family fit. -/
235theorem consistency_necessary
236 (coeffs : RatioFamilyCoeffs) (sig : ResidualSignature) (exact : ResidualPair)
237 (h : predictedResiduals coeffs sig = exact) :
238 exact.gen12 * (sig.step12 : ℝ) + exact.gen23 * (sig.step23 : ℝ) = 0 := by
239 rw [← h]; simp only [predictedResiduals]; exact consistency_of_ratioFamily coeffs sig
240
241/-! ## Refined Family: Log-Asymmetry Correction
242
243Since the sign-split family's structural constraint is violated by the data,
244we introduce a **single universal parameter** `η` that breaks the rigid
245ratio `gen12/gen23 = −step23/step12`. The correction is multiplicative and
246logarithmic in the step ratio:
247
248 gen12 = c · κ · (s₂₃/total) · (1 + η · ln(s₁₂/s₂₃))
249 gen23 = −c · κ · (s₁₂/total) · (1 − η · ln(s₁₂/s₂₃))
250
251With 3 parameters (cNeg, cPos, η) and 4 quark equations, the system is
252overdetermined by 1, making the `∃!` condition a genuine test (not a tautology).
253-/
254
255/-- Three global coefficients: two sign-class amplitudes plus a universal
256 log-asymmetry that modulates the gen12/gen23 ratio. -/
257structure RefinedCoeffs where
258 cNeg : ℝ
259 cPos : ℝ
260 eta : ℝ
261
262noncomputable def refinedFamily (coeffs : RefinedCoeffs)
263 (sig : ResidualSignature) : ResidualPair :=
264 let c :=
265 match sig.sign with
266 | .neg => coeffs.cNeg
267 | .pos => coeffs.cPos
268 let s12 := (sig.step12 : ℝ)
269 let s23 := (sig.step23 : ℝ)
270 let total := s12 + s23
271 let logAsym := Real.log (s12 / s23)
272 { gen12 := c * sig.coupling * s23 / total * (1 + coeffs.eta * logAsym)
273 , gen23 := -(c * sig.coupling * s12 / total * (1 - coeffs.eta * logAsym))
274 }
275
276noncomputable def refinedPrediction (coeffs : RefinedCoeffs)
277 (sig : ResidualSignature) : ResidualPair :=
278 refinedFamily coeffs sig
279
280/-- At η = 0, the refined family collapses to the original sign-split family. -/
281theorem refined_at_eta_zero (cN cP : ℝ) (sig : ResidualSignature) :
282 refinedFamily ⟨cN, cP, 0⟩ sig =
283 ratioFamily ⟨cN, cP⟩ sig := by
284 simp only [refinedFamily, ratioFamily, zero_mul, add_zero, sub_zero, mul_one]
285
286def refinedItem8ClosureTarget
287 (upExact downExact : ResidualPair)
288 (kappaUp kappaDown : ℝ) : Prop :=
289 ∃! coeffs : RefinedCoeffs,
290 refinedPrediction coeffs (upQuarkSignature kappaUp) = upExact ∧
291 refinedPrediction coeffs (downQuarkSignature kappaDown) = downExact
292
293/-! ## Closed-Form η Solution
294
295For any sector with residual pair `(g₁₂, g₂₃)` and SDGT steps `(s₁₂, s₂₃)`,
296the log-asymmetry parameter η that makes the refined family match the data
297exactly has a unique closed-form expression:
298
299 η = (g₁₂·s₁₂ + g₂₃·s₂₃) / (ln(s₁₂/s₂₃) · (g₁₂·s₁₂ − g₂₃·s₂₃))
300
301The numerator is exactly the consistency violation of the sign-split family
302(which forces `g₁₂·s₁₂ + g₂₃·s₂₃ = 0`), and the denominator is the
303log-asymmetry times the cross-difference.
304
305### Key algebraic identities
306
307When η has this value, the multiplicative correction factors simplify:
308
309 1 + η·L = 2·g₁₂·s₁₂ / (g₁₂·s₁₂ − g₂₃·s₂₃)
310 1 − η·L = −2·g₂₃·s₂₃ / (g₁₂·s₁₂ − g₂₃·s₂₃)
311
312where `L = ln(s₁₂/s₂₃)`. These identities reduce the solution for `c`
313to a single division, and the entire system closes algebraically.
314
315### Obstruction for universal η
316
317The formula yields different η values per sector with current PDG data:
318
319| Sector | η | |η·L| | Perturbative? |
320|--------|---------|--------|---------------|
321| Lepton | +0.065 | 0.039 | ✓ (4%) |
322| Down | −0.879 | 0.253 | marginal |
323| Up | −2.720 | 0.454 | ✗ (flips sign)|
324
325The 3-parameter refined family (universal η) is therefore UNSATISFIABLE
326with current mixed-scheme PDG quark data. Leptons — with scheme-free
327pole masses — give a perturbative η, validating the family structure.
328The quark η inflation is attributed to mixed-scale PDG artifacts
329(especially the t/c ratio: pole vs MS-bar at m_c).
330-/
331
332/-- Closed-form η from residual data: absorbs the consistency violation
333 of the sign-split family into a log-asymmetry correction.
334 Well-defined when `s₁₂ ≠ s₂₃` and `g₁₂·s₁₂ ≠ g₂₃·s₂₃`. -/
335noncomputable def etaFromData (g12 g23 s12 s23 : ℝ) : ℝ :=
336 (g12 * s12 + g23 * s23) / (Real.log (s12 / s23) * (g12 * s12 - g23 * s23))
337
338/-- When η is computed from the data, `1 + η·L` simplifies to
339 `2·g₁₂·s₁₂ / (g₁₂·s₁₂ − g₂₃·s₂₃)`. This is the identity that
340 makes the gen-1→2 equation close algebraically. -/
341theorem etaL_gen12_identity (g12 g23 s12 s23 : ℝ)
342 (hD : g12 * s12 - g23 * s23 ≠ 0)
343 (hL : Real.log (s12 / s23) ≠ 0) :
344 1 + etaFromData g12 g23 s12 s23 * Real.log (s12 / s23) =
345 2 * g12 * s12 / (g12 * s12 - g23 * s23) := by
346 unfold etaFromData
347 field_simp
348 ring
349
350/-- Companion identity: `1 − η·L = −2·g₂₃·s₂₃ / (g₁₂·s₁₂ − g₂₃·s₂₃)`.
351 This closes the gen-2→3 equation. -/
352theorem etaL_gen23_identity (g12 g23 s12 s23 : ℝ)
353 (hD : g12 * s12 - g23 * s23 ≠ 0)
354 (hL : Real.log (s12 / s23) ≠ 0) :
355 1 - etaFromData g12 g23 s12 s23 * Real.log (s12 / s23) =
356 -(2 * g23 * s23) / (g12 * s12 - g23 * s23) := by
357 unfold etaFromData
358 field_simp
359 ring
360
361/-- The consistency violation of the sign-split family is EXACTLY
362 what η absorbs: `g₁₂·s₁₂ + g₂₃·s₂₃ = η · L · (g₁₂·s₁₂ − g₂₃·s₂₃)`.
363 This is the fundamental equation relating the log-asymmetry parameter
364 to the data's departure from the rigid `gen12·s12 + gen23·s23 = 0` law. -/
365theorem eta_absorbs_consistency (g12 g23 s12 s23 : ℝ)
366 (hD : g12 * s12 - g23 * s23 ≠ 0)
367 (hL : Real.log (s12 / s23) ≠ 0) :
368 g12 * s12 + g23 * s23 =
369 etaFromData g12 g23 s12 s23 * Real.log (s12 / s23) *
370 (g12 * s12 - g23 * s23) := by
371 unfold etaFromData
372 field_simp
373
374/-- **SINGLE-SECTOR EXISTENCE**: For any residual pair with nonzero gen12,
375 non-degenerate cross-difference, distinct steps, and nonzero coupling,
376 the refined family has a solution. The proof constructs explicit
377 coefficients using `etaFromData` and verifies both components
378 via the `etaL_gen12/gen23_identity` theorems. -/
379theorem refinedFamily_neg_solvable
380 (g12 g23 : ℝ) (s12 s23 : ℕ) (κ : ℝ)
381 (hs12 : 0 < s12) (hs23 : 0 < s23)
382 (hκ : κ ≠ 0)
383 (hg12 : g12 ≠ 0)
384 (hD : g12 * (s12 : ℝ) - g23 * (s23 : ℝ) ≠ 0)
385 (hL : Real.log ((s12 : ℝ) / (s23 : ℝ)) ≠ 0) :
386 ∃ coeffs : RefinedCoeffs,
387 refinedFamily coeffs ⟨.neg, s12, s23, κ, hs12, hs23⟩ =
388 ⟨g12, g23⟩ := by
389 have hs23_ne : (s23 : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr (by omega)
390 have hs12_ne : (s12 : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr (by omega)
391 have h12 := etaL_gen12_identity g12 g23 (s12 : ℝ) (s23 : ℝ) hD hL
392 have h23 := etaL_gen23_identity g12 g23 (s12 : ℝ) (s23 : ℝ) hD hL
393 have h_corr_ne : 1 + etaFromData g12 g23 (s12 : ℝ) (s23 : ℝ) *
394 Real.log ((s12 : ℝ) / (s23 : ℝ)) ≠ 0 := by
395 rw [h12]
396 exact div_ne_zero (mul_ne_zero (mul_ne_zero (by norm_num) hg12) hs12_ne) hD
397 refine ⟨⟨g12 * ((s12 : ℝ) + (s23 : ℝ)) /
398 (κ * (s23 : ℝ) * (1 + etaFromData g12 g23 (s12 : ℝ) (s23 : ℝ) *
399 Real.log ((s12 : ℝ) / (s23 : ℝ)))),
400 0, etaFromData g12 g23 (s12 : ℝ) (s23 : ℝ)⟩, ?_⟩
401 have hD_swap : g12 * (s12 : ℝ) - (s23 : ℝ) * g23 ≠ 0 := by
402 rw [show g12 * (s12 : ℝ) - (s23 : ℝ) * g23 =
403 g12 * (s12 : ℝ) - g23 * (s23 : ℝ) from by ring]; exact hD
404 have hD_comm : -(g23 * (s23 : ℝ)) + g12 * (s12 : ℝ) ≠ 0 := by
405 intro h; exact hD (by linarith)
406 simp only [refinedFamily]
407 ext
408 · -- gen12: direct cancellation of cNeg · κ · s23 / total · (1 + η·L)
409 dsimp [ResidualPair.gen12]
410 field_simp
411 · -- gen23: substitute correction factors, then cancel D/D
412 dsimp [ResidualPair.gen23]
413 rw [h12, h23]
414 field_simp [hD_comm, hD_swap]
415
416/-- The positive-sign variant: same existence for `BpowSign.pos` sectors. -/
417theorem refinedFamily_pos_solvable
418 (g12 g23 : ℝ) (s12 s23 : ℕ) (κ : ℝ)
419 (hs12 : 0 < s12) (hs23 : 0 < s23)
420 (hκ : κ ≠ 0)
421 (hg12 : g12 ≠ 0)
422 (hD : g12 * (s12 : ℝ) - g23 * (s23 : ℝ) ≠ 0)
423 (hL : Real.log ((s12 : ℝ) / (s23 : ℝ)) ≠ 0) :
424 ∃ coeffs : RefinedCoeffs,
425 refinedFamily coeffs ⟨.pos, s12, s23, κ, hs12, hs23⟩ =
426 ⟨g12, g23⟩ := by
427 have hs23_ne : (s23 : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr (by omega)
428 have hs12_ne : (s12 : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr (by omega)
429 have h12 := etaL_gen12_identity g12 g23 (s12 : ℝ) (s23 : ℝ) hD hL
430 have h23 := etaL_gen23_identity g12 g23 (s12 : ℝ) (s23 : ℝ) hD hL
431 have h_corr_ne : 1 + etaFromData g12 g23 (s12 : ℝ) (s23 : ℝ) *
432 Real.log ((s12 : ℝ) / (s23 : ℝ)) ≠ 0 := by
433 rw [h12]
434 exact div_ne_zero (mul_ne_zero (mul_ne_zero (by norm_num) hg12) hs12_ne) hD
435 have hD_swap : g12 * (s12 : ℝ) - (s23 : ℝ) * g23 ≠ 0 := by
436 rw [show g12 * (s12 : ℝ) - (s23 : ℝ) * g23 =
437 g12 * (s12 : ℝ) - g23 * (s23 : ℝ) from by ring]; exact hD
438 have hD_comm : -(g23 * (s23 : ℝ)) + g12 * (s12 : ℝ) ≠ 0 := by
439 intro h; exact hD (by linarith)
440 refine ⟨⟨0, g12 * ((s12 : ℝ) + (s23 : ℝ)) /
441 (κ * (s23 : ℝ) * (1 + etaFromData g12 g23 (s12 : ℝ) (s23 : ℝ) *
442 Real.log ((s12 : ℝ) / (s23 : ℝ)))),
443 etaFromData g12 g23 (s12 : ℝ) (s23 : ℝ)⟩, ?_⟩
444 simp only [refinedFamily]
445 ext
446 · dsimp [ResidualPair.gen12]
447 field_simp
448 · dsimp [ResidualPair.gen23]
449 rw [h12, h23]
450 field_simp [hD_comm, hD_swap]
451
452/-- **SINGLE-SECTOR UNIQUENESS (neg)**: If two coefficient sets (with sign
453 class `.neg`) produce identical refined-family outputs on a given
454 signature, their active coefficient `cNeg` and `eta` must agree.
455 Combined with `refinedFamily_neg_solvable`, this gives `∃!`.
456
457 Proof strategy: extract gen12/gen23 component equations, cancel the
458 common factor `κ·s/total` from each, then add the two simplified
459 equations to get `c₁ = c₂`, and substitute back to get `eta₁ = eta₂`. -/
460theorem refinedFamily_neg_unique
461 (c₁ c₂ p₁ p₂ eta₁ eta₂ : ℝ)
462 (s12 s23 : ℕ) (κ : ℝ)
463 (hs12 : 0 < s12) (hs23 : 0 < s23)
464 (hκ : κ ≠ 0) (hc1 : c₁ ≠ 0)
465 (hL : Real.log ((s12 : ℝ) / (s23 : ℝ)) ≠ 0)
466 (h : refinedFamily ⟨c₁, p₁, eta₁⟩ ⟨.neg, s12, s23, κ, hs12, hs23⟩ =
467 refinedFamily ⟨c₂, p₂, eta₂⟩ ⟨.neg, s12, s23, κ, hs12, hs23⟩) :
468 c₁ = c₂ ∧ eta₁ = eta₂ := by
469 have hs23_ne : (s23 : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr (by omega)
470 have hs12_ne : (s12 : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr (by omega)
471 have htotal_ne : (s12 : ℝ) + (s23 : ℝ) ≠ 0 := ne_of_gt (by positivity)
472 -- Extract gen12 and gen23 component equations from the ResidualPair equality
473 have hg12 := congr_arg ResidualPair.gen12 h
474 have hg23 := congr_arg ResidualPair.gen23 h
475 dsimp only [refinedFamily] at hg12 hg23
476 -- hg23 has negation on both sides; strip it
477 replace hg23 := neg_inj.mp hg23
478 -- Cancel κ·s23/total from gen12 equation via calc + ring
479 have h1 : c₁ * (1 + eta₁ * Real.log (↑s12 / ↑s23)) =
480 c₂ * (1 + eta₂ * Real.log (↑s12 / ↑s23)) := by
481 have hf : κ * (↑s23 : ℝ) / ((↑s12 : ℝ) + ↑s23) ≠ 0 :=
482 div_ne_zero (mul_ne_zero hκ hs23_ne) htotal_ne
483 exact mul_right_cancel₀ hf (show
484 c₁ * (1 + eta₁ * Real.log (↑s12 / ↑s23)) * (κ * ↑s23 / (↑s12 + ↑s23)) =
485 c₂ * (1 + eta₂ * Real.log (↑s12 / ↑s23)) * (κ * ↑s23 / (↑s12 + ↑s23)) from by
486 calc _ = c₁ * κ * ↑s23 / (↑s12 + ↑s23) *
487 (1 + eta₁ * Real.log (↑s12 / ↑s23)) := by ring
488 _ = c₂ * κ * ↑s23 / (↑s12 + ↑s23) *
489 (1 + eta₂ * Real.log (↑s12 / ↑s23)) := hg12
490 _ = _ := by ring)
491 -- Cancel κ·s12/total from gen23 equation
492 have h2 : c₁ * (1 - eta₁ * Real.log (↑s12 / ↑s23)) =
493 c₂ * (1 - eta₂ * Real.log (↑s12 / ↑s23)) := by
494 have hf : κ * (↑s12 : ℝ) / ((↑s12 : ℝ) + ↑s23) ≠ 0 :=
495 div_ne_zero (mul_ne_zero hκ hs12_ne) htotal_ne
496 exact mul_right_cancel₀ hf (show
497 c₁ * (1 - eta₁ * Real.log (↑s12 / ↑s23)) * (κ * ↑s12 / (↑s12 + ↑s23)) =
498 c₂ * (1 - eta₂ * Real.log (↑s12 / ↑s23)) * (κ * ↑s12 / (↑s12 + ↑s23)) from by
499 calc _ = c₁ * κ * ↑s12 / (↑s12 + ↑s23) *
500 (1 - eta₁ * Real.log (↑s12 / ↑s23)) := by ring
501 _ = c₂ * κ * ↑s12 / (↑s12 + ↑s23) *
502 (1 - eta₂ * Real.log (↑s12 / ↑s23)) := hg23
503 _ = _ := by ring)
504 -- Add h1 and h2: eta terms cancel, leaving 2·c₁ = 2·c₂
505 have hc : c₁ = c₂ := by linarith
506 -- Substitute c₁ = c₂ into h1, cancel c₁ (≠ 0) then L (≠ 0)
507 have heta : eta₁ = eta₂ := by
508 rw [← hc] at h1
509 have := mul_left_cancel₀ hc1 h1
510 have : eta₁ * Real.log (↑s12 / ↑s23) = eta₂ * Real.log (↑s12 / ↑s23) := by linarith
511 exact mul_right_cancel₀ hL this
512 exact ⟨hc, heta⟩
513
514/-- **SINGLE-SECTOR UNIQUENESS (pos)**: Symmetric variant for `.pos` sign class. -/
515theorem refinedFamily_pos_unique
516 (n₁ n₂ c₁ c₂ eta₁ eta₂ : ℝ)
517 (s12 s23 : ℕ) (κ : ℝ)
518 (hs12 : 0 < s12) (hs23 : 0 < s23)
519 (hκ : κ ≠ 0) (hc1 : c₁ ≠ 0)
520 (hL : Real.log ((s12 : ℝ) / (s23 : ℝ)) ≠ 0)
521 (h : refinedFamily ⟨n₁, c₁, eta₁⟩ ⟨.pos, s12, s23, κ, hs12, hs23⟩ =
522 refinedFamily ⟨n₂, c₂, eta₂⟩ ⟨.pos, s12, s23, κ, hs12, hs23⟩) :
523 c₁ = c₂ ∧ eta₁ = eta₂ := by
524 have hs23_ne : (s23 : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr (by omega)
525 have hs12_ne : (s12 : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr (by omega)
526 have htotal_ne : (s12 : ℝ) + (s23 : ℝ) ≠ 0 := ne_of_gt (by positivity)
527 have hg12 := congr_arg ResidualPair.gen12 h
528 have hg23 := congr_arg ResidualPair.gen23 h
529 dsimp only [refinedFamily] at hg12 hg23
530 replace hg23 := neg_inj.mp hg23
531 have h1 : c₁ * (1 + eta₁ * Real.log (↑s12 / ↑s23)) =
532 c₂ * (1 + eta₂ * Real.log (↑s12 / ↑s23)) := by
533 have hf : κ * (↑s23 : ℝ) / ((↑s12 : ℝ) + ↑s23) ≠ 0 :=
534 div_ne_zero (mul_ne_zero hκ hs23_ne) htotal_ne
535 exact mul_right_cancel₀ hf (show
536 c₁ * (1 + eta₁ * Real.log (↑s12 / ↑s23)) * (κ * ↑s23 / (↑s12 + ↑s23)) =
537 c₂ * (1 + eta₂ * Real.log (↑s12 / ↑s23)) * (κ * ↑s23 / (↑s12 + ↑s23)) from by
538 calc _ = c₁ * κ * ↑s23 / (↑s12 + ↑s23) *
539 (1 + eta₁ * Real.log (↑s12 / ↑s23)) := by ring
540 _ = c₂ * κ * ↑s23 / (↑s12 + ↑s23) *
541 (1 + eta₂ * Real.log (↑s12 / ↑s23)) := hg12
542 _ = _ := by ring)
543 have h2 : c₁ * (1 - eta₁ * Real.log (↑s12 / ↑s23)) =
544 c₂ * (1 - eta₂ * Real.log (↑s12 / ↑s23)) := by
545 have hf : κ * (↑s12 : ℝ) / ((↑s12 : ℝ) + ↑s23) ≠ 0 :=
546 div_ne_zero (mul_ne_zero hκ hs12_ne) htotal_ne
547 exact mul_right_cancel₀ hf (show
548 c₁ * (1 - eta₁ * Real.log (↑s12 / ↑s23)) * (κ * ↑s12 / (↑s12 + ↑s23)) =
549 c₂ * (1 - eta₂ * Real.log (↑s12 / ↑s23)) * (κ * ↑s12 / (↑s12 + ↑s23)) from by
550 calc _ = c₁ * κ * ↑s12 / (↑s12 + ↑s23) *
551 (1 - eta₁ * Real.log (↑s12 / ↑s23)) := by ring
552 _ = c₂ * κ * ↑s12 / (↑s12 + ↑s23) *
553 (1 - eta₂ * Real.log (↑s12 / ↑s23)) := hg23
554 _ = _ := by ring)
555 have hc : c₁ = c₂ := by linarith
556 have heta : eta₁ = eta₂ := by
557 rw [← hc] at h1
558 have := mul_left_cancel₀ hc1 h1
559 have : eta₁ * Real.log (↑s12 / ↑s23) = eta₂ * Real.log (↑s12 / ↑s23) := by linarith
560 exact mul_right_cancel₀ hL this
561 exact ⟨hc, heta⟩
562
563/-- For `.neg` signatures, the `cPos` field is unused and can be changed freely. -/
564theorem neg_cPos_irrelevant (c q₁ q₂ η : ℝ) (s12 s23 : ℕ) (κ : ℝ)
565 (hs12 : 0 < s12) (hs23 : 0 < s23) :
566 refinedFamily ⟨c, q₁, η⟩ ⟨.neg, s12, s23, κ, hs12, hs23⟩ =
567 refinedFamily ⟨c, q₂, η⟩ ⟨.neg, s12, s23, κ, hs12, hs23⟩ := by
568 simp [refinedFamily]
569
570/-- For `.pos` signatures, the `cNeg` field is unused and can be changed freely. -/
571theorem pos_cNeg_irrelevant (q₁ q₂ c η : ℝ) (s12 s23 : ℕ) (κ : ℝ)
572 (hs12 : 0 < s12) (hs23 : 0 < s23) :
573 refinedFamily ⟨q₁, c, η⟩ ⟨.pos, s12, s23, κ, hs12, hs23⟩ =
574 refinedFamily ⟨q₂, c, η⟩ ⟨.pos, s12, s23, κ, hs12, hs23⟩ := by
575 simp [refinedFamily]
576
577/-- **SECTOR CLOSURE (neg)**: For any `.neg` sector with nonzero gen12,
578 non-degenerate cross-difference, distinct steps, and nonzero coupling,
579 the refined family has a **unique** active-coefficient solution (c, η).
580 This is the full `∃!` on the active parameters.
581
582 Combines `refinedFamily_neg_solvable` (existence) with
583 `refinedFamily_neg_unique` (uniqueness). -/
584theorem refined_neg_sector_closure
585 (g12 g23 : ℝ) (s12 s23 : ℕ) (κ : ℝ)
586 (hs12 : 0 < s12) (hs23 : 0 < s23)
587 (hκ : κ ≠ 0) (hg12 : g12 ≠ 0)
588 (hD : g12 * (s12 : ℝ) - g23 * (s23 : ℝ) ≠ 0)
589 (hL : Real.log ((s12 : ℝ) / (s23 : ℝ)) ≠ 0) :
590 ∃ c η : ℝ,
591 refinedFamily ⟨c, 0, η⟩ ⟨.neg, s12, s23, κ, hs12, hs23⟩ = ⟨g12, g23⟩ ∧
592 ∀ c' p' η',
593 refinedFamily ⟨c', p', η'⟩ ⟨.neg, s12, s23, κ, hs12, hs23⟩ = ⟨g12, g23⟩ →
594 c' = c ∧ η' = η := by
595 obtain ⟨⟨c, cp, η⟩, hexist⟩ :=
596 refinedFamily_neg_solvable g12 g23 s12 s23 κ hs12 hs23 hκ hg12 hD hL
597 refine ⟨c, η, ?_, ?_⟩
598 · -- Existence: swap cPos from cp to 0 (irrelevant for .neg)
599 exact (neg_cPos_irrelevant c 0 cp η s12 s23 κ hs12 hs23).trans hexist
600 · -- Uniqueness: any solution (c', p', η') must have c' = c, η' = η
601 intro c' p' η' h'
602 have hc_ne : c ≠ 0 := by
603 intro hc
604 exact hg12 (by
605 have := congr_arg ResidualPair.gen12 hexist
606 dsimp only [refinedFamily] at this
607 simp [hc] at this
608 linarith)
609 have ⟨hc, hη⟩ := refinedFamily_neg_unique c c' cp p' η η' s12 s23 κ
610 hs12 hs23 hκ hc_ne hL (hexist.trans h'.symm)
611 exact ⟨hc.symm, hη.symm⟩
612
613/-! ## Sign-Class Family: Independent η per B_pow Sign
614
615Since universal η is ruled out with current data, the natural generalization
616gives each sign class its own log-asymmetry parameter. With 4 parameters
617(cNeg, etaNeg, cPos, etaPos) and 4 quark equations, the system is exactly
618determined — each sector's 2 equations uniquely fix its (c, η) pair. -/
619
620/-- Four global coefficients: two (amplitude, log-asymmetry) pairs,
621 one per `B_pow` sign class. -/
622structure SignClassCoeffs where
623 cNeg : ℝ
624 etaNeg : ℝ
625 cPos : ℝ
626 etaPos : ℝ
627
628/-- Sign-class family with independent η per sign. Each sector's
629 gen12/gen23 ratio is individually adjustable via its sign-class η,
630 while the overall amplitude is set by c and coupling. -/
631noncomputable def signClassFamily (coeffs : SignClassCoeffs)
632 (sig : ResidualSignature) : ResidualPair :=
633 let (c, eta) :=
634 match sig.sign with
635 | .neg => (coeffs.cNeg, coeffs.etaNeg)
636 | .pos => (coeffs.cPos, coeffs.etaPos)
637 let s12 := (sig.step12 : ℝ)
638 let s23 := (sig.step23 : ℝ)
639 let total := s12 + s23
640 let logAsym := Real.log (s12 / s23)
641 { gen12 := c * sig.coupling * s23 / total * (1 + eta * logAsym)
642 , gen23 := -(c * sig.coupling * s12 / total * (1 - eta * logAsym))
643 }
644
645/-- When both η values agree, the sign-class family collapses
646 to the refined family with universal η. -/
647theorem signClass_collapse_to_refined
648 (cN cP eta : ℝ) (sig : ResidualSignature) :
649 signClassFamily ⟨cN, eta, cP, eta⟩ sig =
650 refinedFamily ⟨cN, cP, eta⟩ sig := by
651 simp only [signClassFamily, refinedFamily]
652 cases sig.sign <;> rfl
653
654/-! ## Concrete Instantiation: PDG Data + RS Coupling
655
656PDG 2022 experimental masses (MeV) at mixed reference scales.
657Quark masses carry the standard scheme caveat: u, d, s at 2 GeV MS-bar;
658c at m_c; b at m_b; t as pole mass. At LO in QCD the within-sector mass
659ratio is RG-invariant; NLO corrections are O(α_s) ≈ 12%. Once the RG
660bridge module compiles, quark residuals should be refined to anchor-scale
661ratios; the present values serve as the first concrete target.
662
663Charged-lepton pole masses are scheme-free (no RG caveat). -/
664
665section ConcreteInstantiation
666
667def pdg_up : ℝ := 2.16
668def pdg_charm : ℝ := 1270
669def pdg_top : ℝ := 172690
670def pdg_down : ℝ := 4.67
671def pdg_strange : ℝ := 93.4
672def pdg_bottom : ℝ := 4180
673def pdg_electron : ℝ := 0.510999
674def pdg_muon : ℝ := 105.658
675def pdg_tau : ℝ := 1776.86
676
677/-- RS-derived strong coupling constant: α_s = 2/17 (wallpaper-group fraction).
678 Proved to within 0.3σ of PDG α_s(M_Z) = 0.1179 ± 0.0009. -/
679noncomputable def alphaStrong : ℝ := 2 / 17
680
681/-- Rung-unit residual: `log_φ(observed ratio) − integer step`.
682 Measures the sub-leading correction in units of φ-ladder rungs. -/
683noncomputable def rungResidual (ratio : ℝ) (step : ℕ) : ℝ :=
684 Real.log ratio / Real.log Constants.phi - (step : ℝ)
685
686noncomputable def upGen12Residual : ℝ :=
687 rungResidual (pdg_charm / pdg_up) 13
688
689noncomputable def upGen23Residual : ℝ :=
690 rungResidual (pdg_top / pdg_charm) 11
691
692noncomputable def downGen12Residual : ℝ :=
693 rungResidual (pdg_strange / pdg_down) 6
694
695noncomputable def downGen23Residual : ℝ :=
696 rungResidual (pdg_bottom / pdg_strange) 8
697
698noncomputable def leptonGen12Residual : ℝ :=
699 rungResidual (pdg_muon / pdg_electron) 11
700
701noncomputable def leptonGen23Residual : ℝ :=
702 rungResidual (pdg_tau / pdg_muon) 6
703
704/-- Exact up-quark residual pair (from PDG mass ratios vs φ^{SDGT step}).
705 Approximate values: gen12 ≈ +0.25, gen23 ≈ −0.79 rungs. -/
706noncomputable def upExact : ResidualPair where
707 gen12 := upGen12Residual
708 gen23 := upGen23Residual
709
710/-- Exact down-quark residual pair (from PDG mass ratios vs φ^{SDGT step}).
711 Approximate values: gen12 ≈ +0.23, gen23 ≈ −0.10 rungs. -/
712noncomputable def downExact : ResidualPair where
713 gen12 := downGen12Residual
714 gen23 := downGen23Residual
715
716/-- Observed lepton residual pair (pole-mass ratios — no RG ambiguity).
717 Approximate values: gen12 ≈ +0.08, gen23 ≈ −0.13 rungs. -/
718noncomputable def leptonObserved : ResidualPair where
719 gen12 := leptonGen12Residual
720 gen23 := leptonGen23Residual
721
722/-! ### Specialized Closure Targets -/
723
724/-- **Item 8 Closure (Specialized)**: Both quark sectors fit the sign-split
725 ratio family with coupling κ = α_s = 2/17.
726 Proving this closes the open item and freezes the two global coefficients. -/
727noncomputable def item8Specialized : Prop :=
728 item8ClosureTarget upExact downExact alphaStrong alphaStrong
729
730/-- **All-Sector Verification**: The coefficients frozen by quark data also
731 reproduce the observed lepton residuals — a genuine out-of-sample test.
732
733 Leptons share `BpowSign.neg` with up quarks, so `cNeg` is already fixed
734 by the quark closure. If that same `cNeg` reproduces the lepton residuals
735 under the lepton signature `(11, 6)` and lepton coupling `κ_lep`, the
736 family is vindicated across sign classes.
737
738 The parameter `kappaLepton` is left free: the leading candidate is
739 `1 / (4 · π · 11)` (the RS electromagnetic coupling from α_seed). -/
740noncomputable def allSectorTest (kappaLepton : ℝ) : Prop :=
741 ∃ coeffs : RatioFamilyCoeffs,
742 predictedResiduals coeffs (upQuarkSignature alphaStrong) = upExact ∧
743 predictedResiduals coeffs (downQuarkSignature alphaStrong) = downExact ∧
744 predictedResiduals coeffs (leptonSignature kappaLepton) = leptonObserved
745
746/-! ### Refined Closure Targets -/
747
748/-- **Refined Item 8 Closure**: Both quark sectors fit the log-asymmetry
749 ratio family with κ = α_s = 2/17 and a single universal η.
750 This is overdetermined (3 parameters, 4 equations): the `∃!` is
751 a genuine test, not a tautology. -/
752noncomputable def refinedItem8Specialized : Prop :=
753 refinedItem8ClosureTarget upExact downExact alphaStrong alphaStrong
754
755/-- **Refined All-Sector Test**: The 3 coefficients frozen by quark data
756 also reproduce the lepton residuals (6 equations, 3 unknowns).
757 This is the strongest available falsification target. -/
758noncomputable def refinedAllSectorTest (kappaLepton : ℝ) : Prop :=
759 ∃ coeffs : RefinedCoeffs,
760 refinedPrediction coeffs (upQuarkSignature alphaStrong) = upExact ∧
761 refinedPrediction coeffs (downQuarkSignature alphaStrong) = downExact ∧
762 refinedPrediction coeffs (leptonSignature kappaLepton) = leptonObserved
763
764/-! ### Per-Sector η Values (from closed-form formula)
765
766Each sector's η is computed via `etaFromData` using PDG residuals and
767SDGT steps. The lepton value is small and perturbative (|η·L| ≈ 4%),
768confirming the family form works for scheme-free pole masses. Quark
769values are inflated by mixed-scale PDG artifacts. -/
770
771/-- Lepton η from pole-mass residuals: +0.065.
772 This is the cleanest data point — no RG ambiguity. -/
773noncomputable def leptonEta : ℝ :=
774 etaFromData leptonGen12Residual leptonGen23Residual 11 6
775
776/-- Up-quark η from mixed-scheme PDG: −2.72.
777 Inflated by the t/c mixed-scheme comparison (pole vs MS-bar at m_c). -/
778noncomputable def upQuarkEta : ℝ :=
779 etaFromData upGen12Residual upGen23Residual 13 11
780
781/-- Down-quark η from mixed-scheme PDG: −0.88. -/
782noncomputable def downQuarkEta : ℝ :=
783 etaFromData downGen12Residual downGen23Residual 6 8
784
785/-! ### Concrete Lepton Closure
786
787The lepton sector is the cleanest `.neg` test case because the masses are pole
788masses (no QCD scheme ambiguity). The non-degeneracy hypotheses needed by
789`refined_neg_sector_closure` can be verified directly from φ-power comparisons:
790
791* `μ/e > φ¹¹`, so `leptonGen12Residual > 0`
792* `τ/μ < φ⁶`, so `leptonGen23Residual < 0`
793
794This gives the full `∃!` closure for the concrete lepton signature `(11, 6)`
795at the candidate electromagnetic coupling `κ_lep = 1 / alpha_seed`. -/
796
797/-- Leading lepton coupling candidate from the RS electromagnetic seed:
798 `κ_lep = 1 / alpha_seed = 1 / (4π·11)`. -/
799noncomputable def kappaLeptonCandidate : ℝ := 1 / Constants.alpha_seed
800
801theorem kappaLeptonCandidate_pos : 0 < kappaLeptonCandidate := by
802 unfold kappaLeptonCandidate Constants.alpha_seed
803 positivity
804
805theorem kappaLeptonCandidate_ne_zero : kappaLeptonCandidate ≠ 0 :=
806 ne_of_gt kappaLeptonCandidate_pos
807
808/-- The lepton step log-asymmetry is positive: `log(11/6) > 0`. -/
809theorem leptonLogAsym_pos : 0 < Real.log ((11 : ℝ) / 6) := by
810 have hratio_gt_one : (1 : ℝ) < (11 : ℝ) / 6 := by norm_num
811 exact Real.log_pos hratio_gt_one
812
813theorem leptonLogAsym_ne_zero : Real.log ((11 : ℝ) / 6) ≠ 0 :=
814 ne_of_gt leptonLogAsym_pos
815
816/-- The μ/e residual is positive because the observed ratio exceeds `φ¹¹`. -/
817theorem leptonGen12Residual_pos : 0 < leptonGen12Residual := by
818 unfold leptonGen12Residual rungResidual
819 have hlogphi : 0 < Real.log Constants.phi := Real.log_pos Constants.one_lt_phi
820 have hphi11_lt : Constants.phi ^ (11 : ℕ) < pdg_muon / pdg_electron := by
821 have hphi11_lt_200 : Constants.phi ^ (11 : ℕ) < (200 : ℝ) := by
822 rw [Constants.phi_eleventh_eq]
823 linarith [Constants.phi_lt_onePointSixTwo]
824 have hratio_gt_200 : (200 : ℝ) < pdg_muon / pdg_electron := by
825 norm_num [pdg_muon, pdg_electron]
826 linarith
827 have hmain : (11 : ℝ) < Real.log (pdg_muon / pdg_electron) / Real.log Constants.phi := by
828 apply (lt_div_iff₀ hlogphi).2
829 rw [show (11 : ℝ) = (11 : ℕ) by norm_num, ← Real.log_rpow Constants.phi_pos]
830 apply Real.log_lt_log
831 · exact Real.rpow_pos_of_pos Constants.phi_pos 11
832 · simpa [Real.rpow_natCast] using hphi11_lt
833 linarith
834
835theorem leptonGen12Residual_ne_zero : leptonGen12Residual ≠ 0 :=
836 ne_of_gt leptonGen12Residual_pos
837
838/-- The τ/μ residual is negative because the observed ratio lies below `φ⁶`. -/
839theorem leptonGen23Residual_neg : leptonGen23Residual < 0 := by
840 unfold leptonGen23Residual rungResidual
841 have hlogphi : 0 < Real.log Constants.phi := Real.log_pos Constants.one_lt_phi
842 have hratio_lt : pdg_tau / pdg_muon < Constants.phi ^ (6 : ℕ) := by
843 have hratio_lt_17 : pdg_tau / pdg_muon < (17 : ℝ) := by
844 norm_num [pdg_tau, pdg_muon]
845 have h17_lt_phi6 : (17 : ℝ) < Constants.phi ^ (6 : ℕ) := by
846 rw [Constants.phi_sixth_eq]
847 linarith [Constants.phi_gt_onePointFive]
848 linarith
849 have hratio_pos : 0 < pdg_tau / pdg_muon := by
850 norm_num [pdg_tau, pdg_muon]
851 have hmain : Real.log (pdg_tau / pdg_muon) / Real.log Constants.phi < (6 : ℝ) := by
852 apply (div_lt_iff₀ hlogphi).2
853 rw [show (6 : ℝ) = (6 : ℕ) by norm_num, ← Real.log_rpow Constants.phi_pos]
854 apply Real.log_lt_log
855 · exact hratio_pos
856 · simpa [Real.rpow_natCast] using hratio_lt
857 linarith
858
859/-- The lepton cross-difference is strictly positive, hence nonzero. -/
860theorem leptonCrossDiff_pos :
861 0 < leptonGen12Residual * (11 : ℝ) - leptonGen23Residual * (6 : ℝ) := by
862 nlinarith [leptonGen12Residual_pos, leptonGen23Residual_neg]
863
864theorem leptonCrossDiff_ne_zero :
865 leptonGen12Residual * (11 : ℝ) - leptonGen23Residual * (6 : ℝ) ≠ 0 :=
866 ne_of_gt leptonCrossDiff_pos
867
868/-- Concrete `∃!` closure for the lepton `.neg` sector at the candidate
869 electromagnetic coupling `κ_lep = 1 / (4π·11)`. This freezes the active
870 pair `(cNeg, eta)` independently of the quark data. -/
871theorem leptonSectorClosure :
872 ∃ c η : ℝ,
873 refinedFamily ⟨c, 0, η⟩ (leptonSignature kappaLeptonCandidate) = leptonObserved ∧
874 ∀ c' p' η',
875 refinedFamily ⟨c', p', η'⟩ (leptonSignature kappaLeptonCandidate) = leptonObserved →
876 c' = c ∧ η' = η := by
877 have hs12 : 0 < 11 := by norm_num
878 have hs23 : 0 < 6 := by norm_num
879 simpa [leptonSignature, leptonObserved] using
880 refined_neg_sector_closure leptonGen12Residual leptonGen23Residual 11 6
881 kappaLeptonCandidate hs12 hs23 kappaLeptonCandidate_ne_zero
882 leptonGen12Residual_ne_zero leptonCrossDiff_ne_zero leptonLogAsym_ne_zero
883
884/-- Closed-form lepton anchor for the active `.neg` amplitude. This is the
885 explicit `cNeg` obtained from the lepton gen12 equation once `eta` is fixed
886 to `leptonEta`. -/
887noncomputable def leptonAnchoredCNeg (kappaLepton : ℝ) : ℝ :=
888 leptonGen12Residual * ((11 : ℝ) + 6) /
889 (kappaLepton * 6 * (1 + leptonEta * Real.log ((11 : ℝ) / 6)))
890
891/-- The lepton-anchored global coefficient package. `cPos` is left at `0`
892 because leptons only freeze the `.neg` branch. -/
893noncomputable def leptonAnchoredCoeffs (kappaLepton : ℝ) : RefinedCoeffs :=
894 ⟨leptonAnchoredCNeg kappaLepton, 0, leptonEta⟩
895
896/-! ### Anchor-Scale Quark Transport (LO scaffold)
897
898The current LO scaffold transports the PDG quark masses to the RS anchor scale
899`μ* = 182.201 GeV` using piecewise one-loop α_s and the one-loop mass anomalous
900dimension. This is the concrete bridge needed to compare lepton-frozen
901predictions against scheme-consistent quark residuals. -/
902
903/-- One-loop α_s in the `n_f = 6` region, anchored at `μ*`. -/
904noncomputable def alphaS6At (μ : ℝ) : ℝ :=
905 Physics.RG.alpha_s_running Physics.RG.rs_alpha_s_anchor (Physics.RG.b0_qcd 6)
906 μ Physics.RG.rs_anchor_scale
907
908/-- Boundary value α_s(m_t) obtained from the `n_f = 6` branch. -/
909noncomputable def alphaSAtTopThreshold : ℝ :=
910 alphaS6At Physics.RG.top_threshold.scale
911
912/-- One-loop α_s in the `n_f = 5` region, matched at the top threshold. -/
913noncomputable def alphaS5At (μ : ℝ) : ℝ :=
914 Physics.RG.alpha_s_running alphaSAtTopThreshold (Physics.RG.b0_qcd 5)
915 μ Physics.RG.top_threshold.scale
916
917/-- Boundary value α_s(m_b) obtained from the `n_f = 5` branch. -/
918noncomputable def alphaSAtBottomThreshold : ℝ :=
919 alphaS5At Physics.RG.bottom_threshold.scale
920
921/-- One-loop α_s in the `n_f = 4` region, matched at the bottom threshold. -/
922noncomputable def alphaS4At (μ : ℝ) : ℝ :=
923 Physics.RG.alpha_s_running alphaSAtBottomThreshold (Physics.RG.b0_qcd 4)
924 μ Physics.RG.bottom_threshold.scale
925
926/-- Boundary value α_s(m_c) obtained from the `n_f = 4` branch. -/
927noncomputable def alphaSAtCharmThreshold : ℝ :=
928 alphaS4At Physics.RG.charm_threshold.scale
929
930/-- One-loop α_s in the `n_f = 3` region, matched at the charm threshold. -/
931noncomputable def alphaS3At (μ : ℝ) : ℝ :=
932 Physics.RG.alpha_s_running alphaSAtCharmThreshold (Physics.RG.b0_qcd 3)
933 μ Physics.RG.charm_threshold.scale
934
935/-- Piecewise one-loop α_s stitched across the heavy-quark thresholds. -/
936noncomputable def alphaSPiecewise (μ : ℝ) : ℝ :=
937 if Physics.RG.top_threshold.scale ≤ μ then alphaS6At μ
938 else if Physics.RG.bottom_threshold.scale ≤ μ then alphaS5At μ
939 else if Physics.RG.charm_threshold.scale ≤ μ then alphaS4At μ
940 else alphaS3At μ
941
942/-- Shared PDG reference scale for the light MS-bar quarks (`u,d,s`). -/
943def quarkReferenceScale2GeV : ℝ := 2
944
945/-- Threshold lists for upward transport to the anchor scale. -/
946def thresholdsFromTwoGeV : List Physics.RG.FlavorThreshold :=
947 [Physics.RG.bottom_threshold, Physics.RG.top_threshold]
948
949def thresholdsFromCharm : List Physics.RG.FlavorThreshold :=
950 [Physics.RG.bottom_threshold, Physics.RG.top_threshold]
951
952def thresholdsFromBottom : List Physics.RG.FlavorThreshold :=
953 [Physics.RG.top_threshold]
954
955/-- Light and heavy quark masses transported to the anchor scale `μ*`. -/
956noncomputable def upMassAtAnchor : ℝ :=
957 Physics.RG.transport_mass_through pdg_up alphaSPiecewise quarkReferenceScale2GeV
958 Physics.RG.rs_anchor_scale thresholdsFromTwoGeV 4
959
960noncomputable def downMassAtAnchor : ℝ :=
961 Physics.RG.transport_mass_through pdg_down alphaSPiecewise quarkReferenceScale2GeV
962 Physics.RG.rs_anchor_scale thresholdsFromTwoGeV 4
963
964noncomputable def strangeMassAtAnchor : ℝ :=
965 Physics.RG.transport_mass_through pdg_strange alphaSPiecewise quarkReferenceScale2GeV
966 Physics.RG.rs_anchor_scale thresholdsFromTwoGeV 4
967
968noncomputable def charmMassAtAnchor : ℝ :=
969 Physics.RG.transport_mass_through pdg_charm alphaSPiecewise
970 Physics.RG.charm_threshold.scale Physics.RG.rs_anchor_scale thresholdsFromCharm 4
971
972noncomputable def bottomMassAtAnchor : ℝ :=
973 Physics.RG.transport_mass_through pdg_bottom alphaSPiecewise
974 Physics.RG.bottom_threshold.scale Physics.RG.rs_anchor_scale thresholdsFromBottom 5
975
976noncomputable def topMassAtAnchor : ℝ :=
977 Physics.RG.transport_mass_through pdg_top alphaSPiecewise
978 Physics.RG.top_threshold.scale Physics.RG.rs_anchor_scale [] 6
979
980/-- Anchor-scale quark residuals built from the transported masses. Under the
981 current LO scaffold, shell evaluation gives approximately:
982 up `(0.02, +0.57)` and down `(0.23, +0.19)` in rung units. -/
983noncomputable def anchorUpGen12Residual : ℝ :=
984 rungResidual (charmMassAtAnchor / upMassAtAnchor) 13
985
986noncomputable def anchorUpGen23Residual : ℝ :=
987 rungResidual (topMassAtAnchor / charmMassAtAnchor) 11
988
989noncomputable def anchorDownGen12Residual : ℝ :=
990 rungResidual (strangeMassAtAnchor / downMassAtAnchor) 6
991
992noncomputable def anchorDownGen23Residual : ℝ :=
993 rungResidual (bottomMassAtAnchor / strangeMassAtAnchor) 8
994
995noncomputable def anchorUpExact : ResidualPair where
996 gen12 := anchorUpGen12Residual
997 gen23 := anchorUpGen23Residual
998
999noncomputable def anchorDownExact : ResidualPair where
1000 gen12 := anchorDownGen12Residual
1001 gen23 := anchorDownGen23Residual
1002
1003/-- Up-sector out-of-sample prediction after freezing `(cNeg, eta)` on leptons. -/
1004noncomputable def leptonAnchoredUpPrediction (kappaLepton : ℝ) : ResidualPair :=
1005 refinedPrediction (leptonAnchoredCoeffs kappaLepton) (upQuarkSignature alphaStrong)
1006
1007/-- Two down-sector amplitudes implied by the transported anchor residuals once
1008 the lepton value of `eta` is frozen. Equality of these two expressions is
1009 the one-parameter down-sector consistency test under lepton anchoring. -/
1010noncomputable def downAnchorCPosFromGen12 : ℝ :=
1011 anchorDownGen12Residual * ((6 : ℝ) + 8) /
1012 (alphaStrong * 8 * (1 + leptonEta * Real.log ((6 : ℝ) / 8)))
1013
1014noncomputable def downAnchorCPosFromGen23 : ℝ :=
1015 -(anchorDownGen23Residual * ((6 : ℝ) + 8) /
1016 (alphaStrong * 6 * (1 - leptonEta * Real.log ((6 : ℝ) / 8))))
1017
1018/-- The concrete anchor-scale lepton-anchored falsification target:
1019 the up prediction must match the transported anchor residuals, and the down
1020 sector must induce a single consistent `cPos`. -/
1021noncomputable def leptonAnchoredAnchorTest : Prop :=
1022 leptonAnchoredUpPrediction kappaLeptonCandidate = anchorUpExact ∧
1023 downAnchorCPosFromGen12 = downAnchorCPosFromGen23
1024
1025/-! ### Lepton-Anchored Closure Strategy
1026
1027Since leptons provide scheme-free data with perturbative η ≈ 0.065,
1028the resolution strategy is:
1029
10301. **Anchor on leptons**: Fix η and cNeg from the two lepton equations
1031 (both generations share `BpowSign.neg` with up quarks).
10322. **Predict quarks at anchor scale**: The frozen (cNeg, η) pair
1033 predicts up-quark residuals at the anchor scale μ* = 182 GeV.
1034 Down quarks provide an independent prediction via cPos.
10353. **RG bridge**: Compile the `RunningCouplings` module to transport
1036 PDG quark masses to the anchor scale, producing scheme-consistent
1037 residuals for comparison.
1038
1039This makes the quark mass predictions genuine out-of-sample tests
1040rather than fits, and keeps the family form validated by clean data. -/
1041
1042/-- Lepton-anchored closure: the refined family with lepton-derived η
1043 fits both leptons (by construction) and predicts anchor-scale quarks.
1044 The proposition is: there exist global coefficients such that
1045 the family simultaneously fits leptons at coupling κ_lep and
1046 predicts quark residuals at the anchor scale. -/
1047noncomputable def leptonAnchoredTarget
1048 (kappaLepton : ℝ)
1049 (anchorUpExact anchorDownExact : ResidualPair) : Prop :=
1050 ∃ coeffs : RefinedCoeffs,
1051 refinedPrediction coeffs (leptonSignature kappaLepton) = leptonObserved ∧
1052 refinedPrediction coeffs (upQuarkSignature alphaStrong) = anchorUpExact ∧
1053 refinedPrediction coeffs (downQuarkSignature alphaStrong) = anchorDownExact
1054
1055/-- Sign-class family closure: the 4-parameter family with independent η
1056 per sign class fits all three sectors simultaneously.
1057 This is the full all-sector test (6 equations, 4 unknowns + 1 free κ_lep). -/
1058noncomputable def signClassAllSectorTarget (kappaLepton : ℝ) : Prop :=
1059 ∃ coeffs : SignClassCoeffs,
1060 signClassFamily coeffs (upQuarkSignature alphaStrong) = upExact ∧
1061 signClassFamily coeffs (downQuarkSignature alphaStrong) = downExact ∧
1062 signClassFamily coeffs (leptonSignature kappaLepton) = leptonObserved
1063
1064end ConcreteInstantiation
1065
1066end Item8ClosureTarget
1067end Verification
1068end IndisputableMonolith
1069