The Mathlib module lean/FrcMathlib/Theme/Gauge.lean of the framework's chart theme, the readings against the continuum that the master's rows L1, L3, L8 and P1 stake (ledger migration, task LM30): 63 theorems (9 definitions): 0 with no axioms, 0 at tier 1 (propext, Quot.sound), 63 at tier 2 (Classical.choice), 0 red; the mark's colour is the library's (violet, Mathlib; red a proof the gate rejects), each declaration's axioms on hover; the small plain glyph marks a definition (no proof, no axioms; on the ledger pages the plain glyph is instead a module cited as a whole). Each declaration is anchored; the ledger predicates cite them by name. ▶ open in Lean Live · axioms.log.
1import Mathlib23/-!4# FrcMathlib.Theme.Gauge — the chart theme's readings of the gauge sector (46-yangmills, 8 November 2026)56The chart clauses of 46-yangmills on Mathlib's reals, beside the core's window-fraction brackets (`FrcCore/Theme/YangMills.lean`,7no axioms): the two-loop run of the coupling as the exact implicit solution of the two-loop equation and the one-loop law8over `ℝ` (46:P2), the Herbst comparison of the declared coupling and the couplings at the chart's fixed points (46:C10), the9plaquette channel at the chart's cells with `Real.log` (46:C11), the operator family's values with `Real.sqrt` (46:C12) and the gap10of the transfer tally at the classical `π` (46:C21). The chart's11own numbers that no formula fixes — the eigenvalue reading `2.232` and the fixed-point roots `3.541`, `3.085`, `2.611` of the12grid operator — enter as hypotheses or literals, the chart's readings, as `35:C17`'s `2.2322` does in13`FrcMathlib/Theme/Hadrons.lean`; the theorems certify every number built on them. Every bracket is certified from `π` to14six places (`Real.pi_gt_d6`, `Real.pi_lt_d6`), `ln 2` to nine (`Real.log_two_gt_d9`, `Real.log_two_lt_d9`) and the series of15`log (1 − x)` with its tail (`Real.abs_log_sub_add_sum_range_le`); every numeric bracket is its own lemma (`logb_*`, `Fb_*`),16cited by the theorems. The names stay in `FRC.YangMillsML`, so the paper module `FrcMathlib/YangMills.lean` aliases them17beside the yangmills theme's. Classical (tier 2).18-/1920namespace FRC.YangMillsML2122open Finset Real2324/-! ## The logarithm brackets -/2526/-- The series bracket of `log (1 − x)` for `0 ≤ x < 1` after `n` terms, from Mathlib's tail bound:27with `S_n = Σ_{i<n} x^{i+1}/(i+1)`, `−S_n − x^{n+1}/(1−x) ≤ log (1 − x) ≤ −S_n + x^{n+1}/(1−x)`. -/28
theorem log_series_bracket (x : ℝ) (h0 : 0 ≤ x) (h1 : x < 1) (n : ℕ) :29 -(∑ i ∈ range n, x ^ (i + 1) / (i + 1)) - x ^ (n + 1) / (1 - x) ≤ log (1 - x) ∧30 log (1 - x) ≤ -(∑ i ∈ range n, x ^ (i + 1) / (i + 1)) + x ^ (n + 1) / (1 - x) := by31 have hx : |x| < 1 := by rw [abs_of_nonneg h0]; exact h132 have h := Real.abs_log_sub_add_sum_range_le hx n33 rw [abs_of_nonneg h0, abs_le] at h34 constructor <;> linarith [h.1, h.2]3536/-- `log q = log (q 2^k) − k log 2`, the mantissa `q 2^k ∈ (0, 1]` bracketed by the series after `n` terms: for rational37ends `lo ≤ −S_n − x^{n+1}/(q 2^k)` and `−S_n + x^{n+1}/(q 2^k) ≤ hi` with `x = 1 − q 2^k` (decided by `norm_num`),38`lo − k log 2 ≤ log q ≤ hi − k log 2`. -/39theorem log_mantissa_bracket (q : ℝ) (k n : ℕ) (lo hi : ℝ) (hq : 0 < q) (hq1 : q * 2 ^ k ≤ 1)40 (hlo : lo ≤ -(∑ i ∈ range n, (1 - q * 2 ^ k) ^ (i + 1) / (i + 1)) - (1 - q * 2 ^ k) ^ (n + 1) / (q * 2 ^ k))41 (hhi : -(∑ i ∈ range n, (1 - q * 2 ^ k) ^ (i + 1) / (i + 1)) + (1 - q * 2 ^ k) ^ (n + 1) / (q * 2 ^ k) ≤ hi) :42 lo - k * log 2 ≤ log q ∧ log q ≤ hi - k * log 2 := by43 have hr : 0 < q * 2 ^ k := by positivity44 have hx0 : 0 ≤ 1 - q * 2 ^ k := by linarith45 have hx1 : 1 - q * 2 ^ k < 1 := by linarith46 have h := log_series_bracket (1 - q * 2 ^ k) hx0 hx1 n47 have e2 : (1 : ℝ) - (1 - q * 2 ^ k) = q * 2 ^ k := by ring48 rw [e2] at h49 have e : log q = log (q * 2 ^ k) - k * log 2 := by50 rw [log_mul hq.ne' (by positivity), log_pow]; ring51 rw [e]52 constructor <;> linarith [h.1, h.2]5354/-! ## 46:P2 — the running coupling: the two-loop equation's exact solution and the one-loop law over `ℝ` -/5556/-- The two-loop integral: for `a = α/4π` the two-loop equation `da/d ln μ = −2 b₀ a² − 2 b₁ a³` has the exact solution57`F (a(μ)) = F (a(μ₀)) + ln (μ/μ₀)` with `F a = 1/(2 b₀ a) + (b₁/2b₀²) log (a/(b₀ + b₁ a))`, since `dF/da = −1/(2a²(b₀ + b₁ a))`58is the reciprocal of the equation's right side. -/59
noncomputable def F (b₀ b₁ a : ℝ) : ℝ := 1 / (2 * b₀ * a) + b₁ / (2 * b₀ ^ 2) * log (a / (b₀ + b₁ * a))6061/-- `F` is strictly decreasing on `a > 0` (for `b₀, b₁ > 0`), without calculus: with `z = a(b₀ + b₁a')/(a'(b₀ + b₁a))`,62`F a − F a' = (a' − a)/(2aa'(b₀ + b₁a')) + (b₁/2b₀²)(log z − (1 − 1/z))`, both terms positive (`1 − 1/z ≤ log z`). -/63theorem F_lt_of_lt (b₀ b₁ : ℝ) (h0 : 0 < b₀) (h1 : 0 < b₁) {a a' : ℝ} (ha : 0 < a) (haa : a < a') :64 F b₀ b₁ a' < F b₀ b₁ a := by65 have ha' : 0 < a' := lt_trans ha haa66 have hd : 0 < b₀ + b₁ * a := by positivity67 have hd' : 0 < b₀ + b₁ * a' := by positivity68 have hzpos : 0 < (a * (b₀ + b₁ * a')) / (a' * (b₀ + b₁ * a)) := by positivity69 have hlogz : log ((a * (b₀ + b₁ * a')) / (a' * (b₀ + b₁ * a))) = log (a / (b₀ + b₁ * a)) - log (a' / (b₀ + b₁ * a')) := by70 rw [← log_div (by positivity) (by positivity)]71 congr 172 field_simp73 have hbound := one_sub_inv_le_log_of_pos hzpos74 rw [hlogz, inv_div] at hbound75 have key : F b₀ b₁ a - F b₀ b₁ a' = (a' - a) / (2 * a * a' * (b₀ + b₁ * a')) +76 b₁ / (2 * b₀ ^ 2) * ((log (a / (b₀ + b₁ * a)) - log (a' / (b₀ + b₁ * a'))) - (1 - (a' * (b₀ + b₁ * a)) / (a * (b₀ + b₁ * a')))) := by77 unfold F78 field_simp79 ring80 have hpos1 : 0 < (a' - a) / (2 * a * a' * (b₀ + b₁ * a')) := by81 apply div_pos82 · linarith83 · positivity84 have hpos2 : 0 ≤ b₁ / (2 * b₀ ^ 2) * ((log (a / (b₀ + b₁ * a)) - log (a' / (b₀ + b₁ * a'))) - (1 - (a' * (b₀ + b₁ * a)) / (a * (b₀ + b₁ * a')))) := by85 apply mul_nonneg86 · positivity87 · linarith88 linarith8990/-- `F` is antitone on `a > 0`. -/91theorem F_le_of_le (b₀ b₁ : ℝ) (h0 : 0 < b₀) (h1 : 0 < b₁) {a a' : ℝ} (ha : 0 < a) (haa : a ≤ a') :92 F b₀ b₁ a' ≤ F b₀ b₁ a := by93 rcases lt_or_eq_of_le haa with h | h94 · exact le_of_lt (F_lt_of_lt b₀ b₁ h0 h1 ha h)95 · rw [h]9697/-- The solution of `F a = T` lies in `(lo, hi)` when `F hi < T < F lo`. -/98theorem a_of_F_bracket (b₀ b₁ : ℝ) (h0 : 0 < b₀) (h1 : 0 < b₁) {a lo hi T : ℝ} (hhi : 0 < hi) (ha : 0 < a)99 (hF : F b₀ b₁ a = T) (hT1 : T < F b₀ b₁ lo) (hT2 : F b₀ b₁ hi < T) : lo < a ∧ a < hi := by100 constructor101 · by_contra h102 rw [not_lt] at h103 have := F_le_of_le b₀ b₁ h0 h1 ha h104 linarith105 · by_contra h106 rw [not_lt] at h107 have := F_le_of_le b₀ b₁ h0 h1 hhi h108 linarith109110/-- `F` at a rational point, bracketed through a bracket of its logarithm: with `c₁ = 1/(2 b₀ r)` and `c₂ = b₁/(2 b₀²)`,111`c₁ + c₂ lo ≤ F r ≤ c₁ + c₂ hi` when `lo ≤ log (r/(b₀ + b₁ r)) ≤ hi`. -/112theorem F_bracket (b₀ b₁ r c₁ c₂ lo hi : ℝ) (h0 : 0 < b₀) (h1 : 0 ≤ b₁) (hc₁ : c₁ = 1 / (2 * b₀ * r))113 (hc₂ : c₂ = b₁ / (2 * b₀ ^ 2)) (hL : lo ≤ log (r / (b₀ + b₁ * r)) ∧ log (r / (b₀ + b₁ * r)) ≤ hi) :114 c₁ + c₂ * lo ≤ F b₀ b₁ r ∧ F b₀ b₁ r ≤ c₁ + c₂ * hi := by115 unfold F116 rw [← hc₁, ← hc₂]117 have hc : 0 ≤ c₂ := by rw [hc₂]; positivity118 constructor119 · linarith [mul_le_mul_of_nonneg_left hL.1 hc]120 · linarith [mul_le_mul_of_nonneg_left hL.2 hc]121122set_option maxHeartbeats 2000000 in123/-- The series bracket of `log (4.18 / 91.1876)` after `15` terms, mantissa `2^4`. -/124theorem logb_mb_MZ : (-0.310018955 : ℝ) - 4 * log 2 ≤ log (4.18 / 91.1876) ∧ log (4.18 / 91.1876) ≤ (-0.3100189532 : ℝ) - 4 * log 2 := by125 simpa using log_mantissa_bracket (4.18 / 91.1876) 4 15 (-0.310018955 : ℝ) (-0.3100189532 : ℝ) (by norm_num) (by norm_num)126 (by norm_num [sum_range_succ]) (by norm_num [sum_range_succ])127128set_option maxHeartbeats 2000000 in129/-- The series bracket of `log (1.77686 / 4.18)` after `11` terms, mantissa `2^1`. -/130theorem logb_mtau_mb : (-0.1623163046 : ℝ) - log 2 ≤ log (1.77686 / 4.18) ∧ log (1.77686 / 4.18) ≤ (-0.1623163042 : ℝ) - log 2 := by131 simpa using log_mantissa_bracket (1.77686 / 4.18) 1 11 (-0.1623163046 : ℝ) (-0.1623163042 : ℝ) (by norm_num) (by norm_num)132 (by norm_num [sum_range_succ]) (by norm_num [sum_range_succ])133134set_option maxHeartbeats 2000000 in135/-- The series bracket of `log ((29500 / 3141593 : ℝ) / ((23 / 3 : ℝ) + (116 / 3 : ℝ) * (29500 / 3141593 : ℝ)))` after `23` terms, mantissa `2^9`. -/136theorem logb_Fa0lo : (-0.5129240434 : ℝ) - 9 * log 2 ≤ log ((29500 / 3141593 : ℝ) / ((23 / 3 : ℝ) + (116 / 3 : ℝ) * (29500 / 3141593 : ℝ))) ∧ log ((29500 / 3141593 : ℝ) / ((23 / 3 : ℝ) + (116 / 3 : ℝ) * (29500 / 3141593 : ℝ))) ≤ (-0.5129240423 : ℝ) - 9 * log 2 := by137 simpa using log_mantissa_bracket ((29500 / 3141593 : ℝ) / ((23 / 3 : ℝ) + (116 / 3 : ℝ) * (29500 / 3141593 : ℝ))) 9 23 (-0.5129240434 : ℝ) (-0.5129240423 : ℝ) (by norm_num) (by norm_num)138 (by norm_num [sum_range_succ]) (by norm_num [sum_range_succ])139140/-- `F` at `a = 29500/3141593` (`b₀ = 23/3`, `b₁ = 116/3`), bracketed through `logb_Fa0lo`. -/141theorem Fb_a0lo : (409773 / 59000 : ℝ) + (174 / 529 : ℝ) * ((-0.5129240434 : ℝ) - 9 * log 2) ≤ F (23 / 3 : ℝ) (116 / 3 : ℝ) (29500 / 3141593 : ℝ) ∧142 F (23 / 3 : ℝ) (116 / 3 : ℝ) (29500 / 3141593 : ℝ) ≤ (409773 / 59000 : ℝ) + (174 / 529 : ℝ) * ((-0.5129240423 : ℝ) - 9 * log 2) :=143 F_bracket (23 / 3 : ℝ) (116 / 3 : ℝ) (29500 / 3141593 : ℝ) (409773 / 59000 : ℝ) (174 / 529 : ℝ) _ _ (by norm_num) (by norm_num) (by norm_num) (by norm_num) logb_Fa0lo144145set_option maxHeartbeats 2000000 in146/-- The series bracket of `log ((7375 / 785398 : ℝ) / ((23 / 3 : ℝ) + (116 / 3 : ℝ) * (7375 / 785398 : ℝ)))` after `23` terms, mantissa `2^9`. -/147theorem logb_Fa0hi : (-0.5129237395 : ℝ) - 9 * log 2 ≤ log ((7375 / 785398 : ℝ) / ((23 / 3 : ℝ) + (116 / 3 : ℝ) * (7375 / 785398 : ℝ))) ∧ log ((7375 / 785398 : ℝ) / ((23 / 3 : ℝ) + (116 / 3 : ℝ) * (7375 / 785398 : ℝ))) ≤ (-0.5129237384 : ℝ) - 9 * log 2 := by148 simpa using log_mantissa_bracket ((7375 / 785398 : ℝ) / ((23 / 3 : ℝ) + (116 / 3 : ℝ) * (7375 / 785398 : ℝ))) 9 23 (-0.5129237395 : ℝ) (-0.5129237384 : ℝ) (by norm_num) (by norm_num)149 (by norm_num [sum_range_succ]) (by norm_num [sum_range_succ])150151/-- `F` at `a = 7375/785398` (`b₀ = 23/3`, `b₁ = 116/3`), bracketed through `logb_Fa0hi`. -/152theorem Fb_a0hi : (1178097 / 169625 : ℝ) + (174 / 529 : ℝ) * ((-0.5129237395 : ℝ) - 9 * log 2) ≤ F (23 / 3 : ℝ) (116 / 3 : ℝ) (7375 / 785398 : ℝ) ∧153 F (23 / 3 : ℝ) (116 / 3 : ℝ) (7375 / 785398 : ℝ) ≤ (1178097 / 169625 : ℝ) + (174 / 529 : ℝ) * ((-0.5129237384 : ℝ) - 9 * log 2) :=154 F_bracket (23 / 3 : ℝ) (116 / 3 : ℝ) (7375 / 785398 : ℝ) (1178097 / 169625 : ℝ) (174 / 529 : ℝ) _ _ (by norm_num) (by norm_num) (by norm_num) (by norm_num) logb_Fa0hi155156set_option maxHeartbeats 2000000 in157/-- The series bracket of `log ((1779 / 100000 : ℝ) / ((23 / 3 : ℝ) + (116 / 3 : ℝ) * (1779 / 100000 : ℝ)))` after `27` terms, mantissa `2^8`. -/158theorem logb_F5lob : (-0.606747235 : ℝ) - 8 * log 2 ≤ log ((1779 / 100000 : ℝ) / ((23 / 3 : ℝ) + (116 / 3 : ℝ) * (1779 / 100000 : ℝ))) ∧ log ((1779 / 100000 : ℝ) / ((23 / 3 : ℝ) + (116 / 3 : ℝ) * (1779 / 100000 : ℝ))) ≤ (-0.6067472339 : ℝ) - 8 * log 2 := by159 simpa using log_mantissa_bracket ((1779 / 100000 : ℝ) / ((23 / 3 : ℝ) + (116 / 3 : ℝ) * (1779 / 100000 : ℝ))) 8 27 (-0.606747235 : ℝ) (-0.6067472339 : ℝ) (by norm_num) (by norm_num)160 (by norm_num [sum_range_succ]) (by norm_num [sum_range_succ])161162/-- `F` at `a = 1779/100000` (`b₀ = 23/3`, `b₁ = 116/3`), bracketed through `logb_F5lob`. -/163theorem Fb_5lob : (50000 / 13639 : ℝ) + (174 / 529 : ℝ) * ((-0.606747235 : ℝ) - 8 * log 2) ≤ F (23 / 3 : ℝ) (116 / 3 : ℝ) (1779 / 100000 : ℝ) ∧164 F (23 / 3 : ℝ) (116 / 3 : ℝ) (1779 / 100000 : ℝ) ≤ (50000 / 13639 : ℝ) + (174 / 529 : ℝ) * ((-0.6067472339 : ℝ) - 8 * log 2) :=165 F_bracket (23 / 3 : ℝ) (116 / 3 : ℝ) (1779 / 100000 : ℝ) (50000 / 13639 : ℝ) (174 / 529 : ℝ) _ _ (by norm_num) (by norm_num) (by norm_num) (by norm_num) logb_F5lob166167set_option maxHeartbeats 2000000 in168/-- The series bracket of `log ((8897 / 500000 : ℝ) / ((23 / 3 : ℝ) + (116 / 3 : ℝ) * (8897 / 500000 : ℝ)))` after `27` terms, mantissa `2^8`. -/169theorem logb_F5hib : (-0.6065409275 : ℝ) - 8 * log 2 ≤ log ((8897 / 500000 : ℝ) / ((23 / 3 : ℝ) + (116 / 3 : ℝ) * (8897 / 500000 : ℝ))) ∧ log ((8897 / 500000 : ℝ) / ((23 / 3 : ℝ) + (116 / 3 : ℝ) * (8897 / 500000 : ℝ))) ≤ (-0.6065409265 : ℝ) - 8 * log 2 := by170 simpa using log_mantissa_bracket ((8897 / 500000 : ℝ) / ((23 / 3 : ℝ) + (116 / 3 : ℝ) * (8897 / 500000 : ℝ))) 8 27 (-0.6065409275 : ℝ) (-0.6065409265 : ℝ) (by norm_num) (by norm_num)171 (by norm_num [sum_range_succ]) (by norm_num [sum_range_succ])172173/-- `F` at `a = 8897/500000` (`b₀ = 23/3`, `b₁ = 116/3`), bracketed through `logb_F5hib`. -/174theorem Fb_5hib : (750000 / 204631 : ℝ) + (174 / 529 : ℝ) * ((-0.6065409275 : ℝ) - 8 * log 2) ≤ F (23 / 3 : ℝ) (116 / 3 : ℝ) (8897 / 500000 : ℝ) ∧175 F (23 / 3 : ℝ) (116 / 3 : ℝ) (8897 / 500000 : ℝ) ≤ (750000 / 204631 : ℝ) + (174 / 529 : ℝ) * ((-0.6065409265 : ℝ) - 8 * log 2) :=176 F_bracket (23 / 3 : ℝ) (116 / 3 : ℝ) (8897 / 500000 : ℝ) (750000 / 204631 : ℝ) (174 / 529 : ℝ) _ _ (by norm_num) (by norm_num) (by norm_num) (by norm_num) logb_F5hib177178set_option maxHeartbeats 2000000 in179/-- The series bracket of `log ((1779 / 100000 : ℝ) / ((25 / 3 : ℝ) + (154 / 3 : ℝ) * (1779 / 100000 : ℝ)))` after `4` terms, mantissa `2^9`. -/180theorem logb_F4lob : (-0.0150450224 : ℝ) - 9 * log 2 ≤ log ((1779 / 100000 : ℝ) / ((25 / 3 : ℝ) + (154 / 3 : ℝ) * (1779 / 100000 : ℝ))) ∧ log ((1779 / 100000 : ℝ) / ((25 / 3 : ℝ) + (154 / 3 : ℝ) * (1779 / 100000 : ℝ))) ≤ (-0.0150450208 : ℝ) - 9 * log 2 := by181 simpa using log_mantissa_bracket ((1779 / 100000 : ℝ) / ((25 / 3 : ℝ) + (154 / 3 : ℝ) * (1779 / 100000 : ℝ))) 9 4 (-0.0150450224 : ℝ) (-0.0150450208 : ℝ) (by norm_num) (by norm_num)182 (by norm_num [sum_range_succ]) (by norm_num [sum_range_succ])183184/-- `F` at `a = 1779/100000` (`b₀ = 25/3`, `b₁ = 154/3`), bracketed through `logb_F4lob`. -/185theorem Fb_4lob : (2000 / 593 : ℝ) + (231 / 625 : ℝ) * ((-0.0150450224 : ℝ) - 9 * log 2) ≤ F (25 / 3 : ℝ) (154 / 3 : ℝ) (1779 / 100000 : ℝ) ∧186 F (25 / 3 : ℝ) (154 / 3 : ℝ) (1779 / 100000 : ℝ) ≤ (2000 / 593 : ℝ) + (231 / 625 : ℝ) * ((-0.0150450208 : ℝ) - 9 * log 2) :=187 F_bracket (25 / 3 : ℝ) (154 / 3 : ℝ) (1779 / 100000 : ℝ) (2000 / 593 : ℝ) (231 / 625 : ℝ) _ _ (by norm_num) (by norm_num) (by norm_num) (by norm_num) logb_F4lob188189set_option maxHeartbeats 2000000 in190/-- The series bracket of `log ((8897 / 500000 : ℝ) / ((25 / 3 : ℝ) + (154 / 3 : ℝ) * (8897 / 500000 : ℝ)))` after `4` terms, mantissa `2^9`. -/191theorem logb_F4hib : (-0.0148424084 : ℝ) - 9 * log 2 ≤ log ((8897 / 500000 : ℝ) / ((25 / 3 : ℝ) + (154 / 3 : ℝ) * (8897 / 500000 : ℝ))) ∧ log ((8897 / 500000 : ℝ) / ((25 / 3 : ℝ) + (154 / 3 : ℝ) * (8897 / 500000 : ℝ))) ≤ (-0.0148424069 : ℝ) - 9 * log 2 := by192 simpa using log_mantissa_bracket ((8897 / 500000 : ℝ) / ((25 / 3 : ℝ) + (154 / 3 : ℝ) * (8897 / 500000 : ℝ))) 9 4 (-0.0148424084 : ℝ) (-0.0148424069 : ℝ) (by norm_num) (by norm_num)193 (by norm_num [sum_range_succ]) (by norm_num [sum_range_succ])194195/-- `F` at `a = 8897/500000` (`b₀ = 25/3`, `b₁ = 154/3`), bracketed through `logb_F4hib`. -/196theorem Fb_4hib : (30000 / 8897 : ℝ) + (231 / 625 : ℝ) * ((-0.0148424084 : ℝ) - 9 * log 2) ≤ F (25 / 3 : ℝ) (154 / 3 : ℝ) (8897 / 500000 : ℝ) ∧197 F (25 / 3 : ℝ) (154 / 3 : ℝ) (8897 / 500000 : ℝ) ≤ (30000 / 8897 : ℝ) + (231 / 625 : ℝ) * ((-0.0148424069 : ℝ) - 9 * log 2) :=198 F_bracket (25 / 3 : ℝ) (154 / 3 : ℝ) (8897 / 500000 : ℝ) (30000 / 8897 : ℝ) (231 / 625 : ℝ) _ _ (by norm_num) (by norm_num) (by norm_num) (by norm_num) logb_F4hib199200set_option maxHeartbeats 2000000 in201/-- The series bracket of `log ((24927 / 1000000 : ℝ) / ((25 / 3 : ℝ) + (154 / 3 : ℝ) * (24927 / 1000000 : ℝ)))` after `19` terms, mantissa `2^8`. -/202theorem logb_F4lot : (-0.4097342393 : ℝ) - 8 * log 2 ≤ log ((24927 / 1000000 : ℝ) / ((25 / 3 : ℝ) + (154 / 3 : ℝ) * (24927 / 1000000 : ℝ))) ∧ log ((24927 / 1000000 : ℝ) / ((25 / 3 : ℝ) + (154 / 3 : ℝ) * (24927 / 1000000 : ℝ))) ≤ (-0.4097342382 : ℝ) - 8 * log 2 := by203 simpa using log_mantissa_bracket ((24927 / 1000000 : ℝ) / ((25 / 3 : ℝ) + (154 / 3 : ℝ) * (24927 / 1000000 : ℝ))) 8 19 (-0.4097342393 : ℝ) (-0.4097342382 : ℝ) (by norm_num) (by norm_num)204 (by norm_num [sum_range_succ]) (by norm_num [sum_range_succ])205206/-- `F` at `a = 24927/1000000` (`b₀ = 25/3`, `b₁ = 154/3`), bracketed through `logb_F4lot`. -/207theorem Fb_4lot : (20000 / 8309 : ℝ) + (231 / 625 : ℝ) * ((-0.4097342393 : ℝ) - 8 * log 2) ≤ F (25 / 3 : ℝ) (154 / 3 : ℝ) (24927 / 1000000 : ℝ) ∧208 F (25 / 3 : ℝ) (154 / 3 : ℝ) (24927 / 1000000 : ℝ) ≤ (20000 / 8309 : ℝ) + (231 / 625 : ℝ) * ((-0.4097342382 : ℝ) - 8 * log 2) :=209 F_bracket (25 / 3 : ℝ) (154 / 3 : ℝ) (24927 / 1000000 : ℝ) (20000 / 8309 : ℝ) (231 / 625 : ℝ) _ _ (by norm_num) (by norm_num) (by norm_num) (by norm_num) logb_F4lot210211set_option maxHeartbeats 2000000 in212/-- The series bracket of `log ((24937 / 1000000 : ℝ) / ((25 / 3 : ℝ) + (154 / 3 : ℝ) * (24937 / 1000000 : ℝ)))` after `19` terms, mantissa `2^8`. -/213theorem logb_F4hit : (-0.4093865473 : ℝ) - 8 * log 2 ≤ log ((24937 / 1000000 : ℝ) / ((25 / 3 : ℝ) + (154 / 3 : ℝ) * (24937 / 1000000 : ℝ))) ∧ log ((24937 / 1000000 : ℝ) / ((25 / 3 : ℝ) + (154 / 3 : ℝ) * (24937 / 1000000 : ℝ))) ≤ (-0.4093865462 : ℝ) - 8 * log 2 := by214 simpa using log_mantissa_bracket ((24937 / 1000000 : ℝ) / ((25 / 3 : ℝ) + (154 / 3 : ℝ) * (24937 / 1000000 : ℝ))) 8 19 (-0.4093865473 : ℝ) (-0.4093865462 : ℝ) (by norm_num) (by norm_num)215 (by norm_num [sum_range_succ]) (by norm_num [sum_range_succ])216217/-- `F` at `a = 24937/1000000` (`b₀ = 25/3`, `b₁ = 154/3`), bracketed through `logb_F4hit`. -/218theorem Fb_4hit : (60000 / 24937 : ℝ) + (231 / 625 : ℝ) * ((-0.4093865473 : ℝ) - 8 * log 2) ≤ F (25 / 3 : ℝ) (154 / 3 : ℝ) (24937 / 1000000 : ℝ) ∧219 F (25 / 3 : ℝ) (154 / 3 : ℝ) (24937 / 1000000 : ℝ) ≤ (60000 / 24937 : ℝ) + (231 / 625 : ℝ) * ((-0.4093865462 : ℝ) - 8 * log 2) :=220 F_bracket (25 / 3 : ℝ) (154 / 3 : ℝ) (24937 / 1000000 : ℝ) (60000 / 24937 : ℝ) (231 / 625 : ℝ) _ _ (by norm_num) (by norm_num) (by norm_num) (by norm_num) logb_F4hit221222set_option maxHeartbeats 1000000 in223/-- 46:P2 [chart] — **the two-loop run as the equation's exact solution.** From `α_s(M_Z) = 0.1180` at `M_Z = 91.1876` GeV224through `m_b = 4.18` (five flavours, `b₀ = 23/3`, `b₁ = 116/3`) to `m_τ = 1.77686` (four flavours, `b₀ = 25/3`, `b₁ = 154/3`),225with `a = α/4π` and the two-loop integral `F`: `α_s(m_b)` lies in `(0.2235, 0.2237)` and `α_s(m_τ)` in `(0.3132, 0.3134)` —226the chart's Runge–Kutta reading `0.313` (`chart_yangmills.two_loop`), against the τ-decay `0.312(15)`. Each solution is227bracketed by `F`'s monotonicity between rational ends, the logarithms by the series after `n` terms and `ln 2` to nine228places, `π` to six. -/229theorem two_loop_tau (a₀ a_b a_τ : ℝ) (h₀ : a₀ = 0.1180 / (4 * π)) (hb : 0 < a_b) (hτ : 0 < a_τ)230 (hFb : F (23 / 3) (116 / 3) a_b = F (23 / 3) (116 / 3) a₀ + log (4.18 / 91.1876))231 (hFτ : F (25 / 3) (154 / 3) a_τ = F (25 / 3) (154 / 3) a_b + log (1.77686 / 4.18)) :232 (0.2235 : ℝ) < 4 * π * a_b ∧ 4 * π * a_b < 0.2237 ∧ (0.3132 : ℝ) < 4 * π * a_τ ∧ 4 * π * a_τ < 0.3134 := by233 have hpi1 := pi_gt_d6234 have hpi2 := pi_lt_d6235 have hl1 := log_two_gt_d9236 have hl2 := log_two_lt_d9237 have hb0 : (0 : ℝ) < 23 / 3 := by norm_num238 have hb1 : (0 : ℝ) < 116 / 3 := by norm_num239 have hb0' : (0 : ℝ) < 25 / 3 := by norm_num240 have hb1' : (0 : ℝ) < 154 / 3 := by norm_num241 have ha₀lo : (29500 / 3141593 : ℝ) < a₀ := by242 rw [h₀, lt_div_iff₀ (by positivity)]; linarith243 have ha₀hi : a₀ < (7375 / 785398 : ℝ) := by244 rw [h₀, div_lt_iff₀ (by positivity)]; linarith245 have ha₀ : 0 < a₀ := lt_trans (by norm_num) ha₀lo246 have hLb := logb_mb_MZ247 have hLt := logb_mtau_mb248 have hFa0lo := Fb_a0lo249 have hFa0hi := Fb_a0hi250 have hF5lob := Fb_5lob251 have hF5hib := Fb_5hib252 have hF4lob := Fb_4lob253 have hF4hib := Fb_4hib254 have hF4lot := Fb_4lot255 have hF4hit := Fb_4hit256 have hFa₀1 := F_lt_of_lt (23 / 3) (116 / 3) hb0 hb1 ha₀ ha₀hi257 have hFa₀2 := F_lt_of_lt (23 / 3) (116 / 3) hb0 hb1 (by norm_num) ha₀lo258 have hab := a_of_F_bracket (23 / 3) (116 / 3) hb0 hb1 (lo := (1779 / 100000 : ℝ)) (hi := (8897 / 500000 : ℝ)) (by norm_num) hb hFb259 (by linarith) (by linarith)260 have hF4b1 := F_le_of_le (25 / 3) (154 / 3) hb0' hb1' hb (le_of_lt hab.2)261 have hF4b2 := F_le_of_le (25 / 3) (154 / 3) hb0' hb1' (by norm_num) (le_of_lt hab.1)262 have hat := a_of_F_bracket (25 / 3) (154 / 3) hb0' hb1' (lo := (24927 / 1000000 : ℝ)) (hi := (24937 / 1000000 : ℝ)) (by norm_num) hτ hFτ263 (by linarith) (by linarith)264 have hm1 := mul_lt_mul'' (by linarith : (4 : ℝ) * 3.141592 < 4 * π) hab.1 (by norm_num) (by norm_num)265 have hm2 := mul_lt_mul'' (by linarith : (4 : ℝ) * π < 4 * 3.141593) hab.2 (by positivity) hb.le266 have hm3 := mul_lt_mul'' (by linarith : (4 : ℝ) * 3.141592 < 4 * π) hat.1 (by norm_num) (by norm_num)267 have hm4 := mul_lt_mul'' (by linarith : (4 : ℝ) * π < 4 * 3.141593) hat.2 (by positivity) hτ.le268 norm_num at hm1 hm2 hm3 hm4269 exact ⟨by linarith, by linarith, by linarith, by linarith⟩270271set_option maxHeartbeats 1000000 in272/-- 46:P2 [chart] — **the one-loop law over `ℝ`**: `1/α(μ) = 1/α(μ₀) + (b₀/2π) ln (μ/μ₀)` across the same thresholds gives273`α_s(m_τ)` in `(0.2785, 0.2795)`, the row's `0.279`, `2.2` standard deviations below `0.312(15)`. -/274theorem one_loop_tau (α : ℝ)275 (h : 1 / α = 1 / 0.1180 + (23 / 3) / (2 * π) * log (4.18 / 91.1876) + (25 / 3) / (2 * π) * log (1.77686 / 4.18)) :276 (0.2785 : ℝ) < α ∧ α < 0.2795 ∧ (2.1 : ℝ) < (0.312 - 0.279) / 0.015 ∧ ((0.312 : ℝ) - 0.279) / 0.015 < 2.3 := by277 have hpi1 := pi_gt_d6278 have hpi2 := pi_lt_d6279 have hl1 := log_two_gt_d9280 have hl2 := log_two_lt_d9281 have hLb := logb_mb_MZ282 have hLt := logb_mtau_mb283 have hpos : 0 < 2 * π := by positivity284 have hp1 : (1 : ℝ) / (2 * 3.141593) < 1 / (2 * π) := one_div_lt_one_div_of_lt (by positivity) (by linarith)285 have hp2 : (1 : ℝ) / (2 * π) < 1 / (2 * 3.141592) := one_div_lt_one_div_of_lt (by positivity) (by linarith)286 have hLb' : log (4.18 / 91.1876) < 0 := by linarith [hLb.2]287 have hLt' : log (1.77686 / 4.18) < 0 := by linarith [hLt.2]288 have e : 1 / α = 1 / 0.1180 + 1 / (2 * π) * ((23 / 3) * log (4.18 / 91.1876) + (25 / 3) * log (1.77686 / 4.18)) := by289 rw [h]; ring290 set S := (23 / 3) * log (4.18 / 91.1876) + (25 / 3) * log (1.77686 / 4.18) with hS291 have hSneg : S < 0 := by rw [hS]; linarith292 have hS1 : ((-38452734889) / 1250000000 : ℝ) < S := by rw [hS]; linarith293 have hS2 : S < ((-922865636237) / 30000000000 : ℝ) := by rw [hS]; linarith294 have hm1 := mul_lt_mul_of_neg_right hp2 hSneg295 have hm2 := mul_lt_mul_of_pos_left hS1 (by positivity : (0 : ℝ) < 1 / (2 * 3.141592))296 have hm3 := mul_lt_mul_of_neg_right hp1 hSneg297 have hm4 := mul_lt_mul_of_pos_left hS2 (by positivity : (0 : ℝ) < 1 / (2 * 3.141593))298 norm_num at hm1 hm2 hm3 hm4299 have hinv1 : (3.5786 : ℝ) < 1 / α := by rw [e]; norm_num; linarith300 have hinv2 : 1 / α < (3.5787 : ℝ) := by rw [e]; norm_num; linarith301 have hαpos : 0 < α := by302 by_contra hneg303 rw [not_lt] at hneg304 have : 1 / α ≤ 0 := by305 rcases lt_or_eq_of_le hneg with h' | h'306 · exact le_of_lt (one_div_neg.mpr h')307 · rw [h']; simp308 linarith309 have hα : α = 1 / (1 / α) := (one_div_one_div α).symm310 refine ⟨?_, ?_, by norm_num, by norm_num⟩311 · rw [hα]; rw [lt_div_iff₀ (by positivity)]; nlinarith312 · rw [hα]; rw [div_lt_iff₀ (by positivity)]; nlinarith313314/-! ## 46:C10 — the Herbst comparison and the couplings at the chart's fixed points -/315316/-- 46:C10 [chart] — the declared coupling `α_s(√σ) = 2π/(9 ln 2)` lies in `(1.0065, 1.0075)` (the row's `1.007`), the317two-adjoint term's `C = C_A α_s` in `(3.015, 3.025)` (the row's `3.02`), above the Herbst bound `4/π` of the two-body form,318itself above the one-body bound `2/π`: `π² > 6 ln 2`. -/319theorem herbst_real : (1.0065 : ℝ) < 2 * π / (9 * log 2) ∧ 2 * π / (9 * log 2) < 1.0075 ∧320 (3.015 : ℝ) < 3 * (2 * π / (9 * log 2)) ∧ 3 * (2 * π / (9 * log 2)) < 3.025 ∧321 4 / π < 3 * (2 * π / (9 * log 2)) ∧ 2 / π < 4 / π ∧ 6 * log 2 < π ^ 2 := by322 have hpi1 := pi_gt_d6323 have hpi2 := pi_lt_d6324 have hl1 := log_two_gt_d9325 have hl2 := log_two_lt_d9326 have hlpos : 0 < 9 * log 2 := by linarith327 have h1 : (1.0065 : ℝ) < 2 * π / (9 * log 2) := by rw [lt_div_iff₀ hlpos]; nlinarith328 have h2 : 2 * π / (9 * log 2) < (1.0075 : ℝ) := by rw [div_lt_iff₀ hlpos]; nlinarith329 refine ⟨h1, h2, by linarith, by linarith, ?_, ?_, by nlinarith⟩330 · rw [div_lt_iff₀ (by positivity)]331 have : 3 * (2 * π / (9 * log 2)) * π = 2 * π ^ 2 / (3 * log 2) := by field_simp; ring332 rw [this, lt_div_iff₀ (by positivity)]333 nlinarith334 · exact div_lt_div_of_pos_right (by norm_num) (by positivity)335336set_option maxHeartbeats 2000000 in337/-- The series bracket of `log (1 / (2 * 3.541))` after `25` terms, mantissa `2^2`. -/338theorem logb_E3541 : (-0.5712619933 : ℝ) - 2 * log 2 ≤ log (1 / (2 * 3.541)) ∧ log (1 / (2 * 3.541)) ≤ (-0.5712619918 : ℝ) - 2 * log 2 := by339 simpa using log_mantissa_bracket (1 / (2 * 3.541)) 2 25 (-0.5712619933 : ℝ) (-0.5712619918 : ℝ) (by norm_num) (by norm_num)340 (by norm_num [sum_range_succ]) (by norm_num [sum_range_succ])341342set_option maxHeartbeats 2000000 in343/-- The series bracket of `log (1 / (2 * 3.085))` after `20` terms, mantissa `2^2`. -/344theorem logb_E3085 : (-0.4334044773 : ℝ) - 2 * log 2 ≤ log (1 / (2 * 3.085)) ∧ log (1 / (2 * 3.085)) ≤ (-0.4334044763 : ℝ) - 2 * log 2 := by345 simpa using log_mantissa_bracket (1 / (2 * 3.085)) 2 20 (-0.4334044773 : ℝ) (-0.4334044763 : ℝ) (by norm_num) (by norm_num)346 (by norm_num [sum_range_succ]) (by norm_num [sum_range_succ])347348set_option maxHeartbeats 2000000 in349/-- The series bracket of `log (1 / (2 * 2.611))` after `14` terms, mantissa `2^2`. -/350theorem logb_E2611 : (-0.2665861096 : ℝ) - 2 * log 2 ≤ log (1 / (2 * 2.611)) ∧ log (1 / (2 * 2.611)) ≤ (-0.2665861086 : ℝ) - 2 * log 2 := by351 simpa using log_mantissa_bracket (1 / (2 * 2.611)) 2 14 (-0.2665861096 : ℝ) (-0.2665861086 : ℝ) (by norm_num) (by norm_num)352 (by norm_num [sum_range_succ]) (by norm_num [sum_range_succ])353354/-- 46:C10 [chart] — the couplings at the chart's fixed points. The two-body fixed points of `2|p| + 2r − C/max(r, r_c)`355with `C = C_A α_s(E)` read at the bound state's own mass are the chart's roots `E = 3.541`, `3.085`, `2.611` at `r_c = 1`,356`1/2`, `1/4` cells (the Lanczos grid of `chart_yangmills.fixed_point_bisect`; none at `1/8`). At these roots the coupling357`C(E) = 2π/(3 ln 2E)` lies in `(1.0698, 1.0700)`, `(1.1508, 1.1511)`, `(1.2670, 1.2672)`: every fixed point sits below the358Herbst bound `4/π = 1.2732` of the two-body form, the quarter-cell one within `0.5 %` of it. -/359theorem fixed_point_couplings :360 (1.0698 : ℝ) < 2 * π / (3 * log (2 * 3.541)) ∧ 2 * π / (3 * log (2 * 3.541)) < (1.07 : ℝ) ∧361 (1.1508 : ℝ) < 2 * π / (3 * log (2 * 3.085)) ∧ 2 * π / (3 * log (2 * 3.085)) < (1.1511 : ℝ) ∧362 (1.267 : ℝ) < 2 * π / (3 * log (2 * 2.611)) ∧ 2 * π / (3 * log (2 * 2.611)) < (1.2672 : ℝ) ∧363 2 * π / (3 * log (2 * 2.611)) < 4 / π ∧ 0.995 * (4 / π) < 2 * π / (3 * log (2 * 2.611)) := by364 have hpi1 := pi_gt_d6365 have hpi2 := pi_lt_d6366 have hl1 := log_two_gt_d9367 have hl2 := log_two_lt_d9368 have hq0 := logb_E3541369 have hln0 : log (2 * 3.541) = -log (1 / (2 * 3.541)) := by rw [one_div, log_inv, neg_neg]370 have hL0 : (4893890881 / 2500000000 : ℝ) < log (2 * 3.541) ∧ log (2 * 3.541) < (19575563549 / 10000000000 : ℝ) := by371 rw [hln0]; constructor <;> linarith [hq0.1, hq0.2]372 have hpos0 : 0 < 3 * log (2 * 3.541) := by linarith [hL0.1]373 have hC0 : (1.0698 : ℝ) < 2 * π / (3 * log (2 * 3.541)) ∧ 2 * π / (3 * log (2 * 3.541)) < (1.07 : ℝ) := by374 constructor375 · rw [lt_div_iff₀ hpos0]; nlinarith [hL0.1, hL0.2]376 · rw [div_lt_iff₀ hpos0]; nlinarith [hL0.1, hL0.2]377 have hq1 := logb_E3085378 have hln1 : log (2 * 3.085) = -log (1 / (2 * 3.085)) := by rw [one_div, log_inv, neg_neg]379 have hL1 : (18196988369 / 10000000000 : ℝ) < log (2 * 3.085) ∧ log (2 * 3.085) < (18196988389 / 10000000000 : ℝ) := by380 rw [hln1]; constructor <;> linarith [hq1.1, hq1.2]381 have hpos1 : 0 < 3 * log (2 * 3.085) := by linarith [hL1.1]382 have hC1 : (1.1508 : ℝ) < 2 * π / (3 * log (2 * 3.085)) ∧ 2 * π / (3 * log (2 * 3.085)) < (1.1511 : ℝ) := by383 constructor384 · rw [lt_div_iff₀ hpos1]; nlinarith [hL1.1, hL1.2]385 · rw [div_lt_iff₀ hpos1]; nlinarith [hL1.1, hL1.2]386 have hq2 := logb_E2611387 have hln2 : log (2 * 2.611) = -log (1 / (2 * 2.611)) := by rw [one_div, log_inv, neg_neg]388 have hL2 : (4132201173 / 2500000000 : ℝ) < log (2 * 2.611) ∧ log (2 * 2.611) < (2066100589 / 1250000000 : ℝ) := by389 rw [hln2]; constructor <;> linarith [hq2.1, hq2.2]390 have hpos2 : 0 < 3 * log (2 * 2.611) := by linarith [hL2.1]391 have hC2 : (1.267 : ℝ) < 2 * π / (3 * log (2 * 2.611)) ∧ 2 * π / (3 * log (2 * 2.611)) < (1.2672 : ℝ) := by392 constructor393 · rw [lt_div_iff₀ hpos2]; nlinarith [hL2.1, hL2.2]394 · rw [div_lt_iff₀ hpos2]; nlinarith [hL2.1, hL2.2]395 have h4pi1 : (1.2672 : ℝ) < 4 / π := by rw [lt_div_iff₀ (by positivity)]; nlinarith396 have h4pi2 : 0.995 * (4 / π) < (1.2670 : ℝ) := by397 have : (0.995 : ℝ) * (4 / π) = 3.98 / π := by ring398 rw [this, div_lt_iff₀ (by positivity)]; nlinarith399 exact ⟨hC0.1, hC0.2, hC1.1, hC1.2, hC2.1, hC2.2, by linarith [hC2.2], by linarith [hC2.1]⟩400401/-! ## 46:C11 — the imported series and the ratio -/402403/-- The imported `0⁺⁺` series of the strong-coupling expansion to order `u^n` (Münster 1981, as quoted by Langelage,404Münster and Philipsen 2007, eq. 2.16): `Σ_{k=1}^{n} M_k u^k` with `M = (−3, 9, −27/2, −7, −297/2, 858827/10240, 47641149/71680)`. -/405noncomputable def P3 (u : ℝ) : ℝ := -3 * u + 9 * u ^ 2 - 27 / 2 * u ^ 3406noncomputable def P5 (u : ℝ) : ℝ := P3 u - 7 * u ^ 4 - 297 / 2 * u ^ 5407noncomputable def P7 (u : ℝ) : ℝ := P5 u + 858827 / 10240 * u ^ 6 + 47641149 / 71680 * u ^ 7408409/-- The channel's mass over the leading-order tension, `m/√σ = (−4 ln u + P)/√(−ln u)`. -/410noncomputable def ratio (u P : ℝ) : ℝ := (4 * (-log u) + P) / √(-log u)411412/-- A bracket of `ratio u P` from a bracket `Llo ≤ −log u ≤ Lhi` and rational square-root ends `slo² < Llo`, `Lhi < shi²`. -/413theorem ratio_bracket (u P Llo Lhi slo shi lo hi : ℝ) (hL : Llo ≤ -log u ∧ -log u ≤ Lhi)414 (hslo : 0 < slo) (hs1 : slo ^ 2 < Llo) (hshi : 0 < shi) (hs2 : Lhi < shi ^ 2) (hP : 0 < 4 * Llo + P)415 (hlo : lo ≤ (4 * Llo + P) / shi) (hhi : (4 * Lhi + P) / slo ≤ hi) : lo ≤ ratio u P ∧ ratio u P ≤ hi := by416 have hsq : 0 < slo ^ 2 := by positivity417 have hLpos : 0 < -log u := by linarith [hL.1]418 have hs_lo : slo < √(-log u) := by rw [lt_sqrt hslo.le]; linarith [hL.1]419 have hs_hi : √(-log u) < shi := by rw [sqrt_lt' hshi]; linarith [hL.2]420 have hspos : 0 < √(-log u) := lt_trans hslo hs_lo421 unfold ratio422 constructor423 · refine le_trans hlo ?_424 rw [div_le_div_iff₀ hshi hspos]425 nlinarith [hs_hi, hL.1, hP, hspos]426 · refine le_trans ?_ hhi427 rw [div_le_div_iff₀ hspos hslo]428 nlinarith [hs_lo, hL.2, hP, hspos, hLpos]429430/-! ## 46:C11 — the plaquette channel at the chart's cells -/431432/-- The step of the chart's cells in the stiffness (46:B6): the one-loop law of powers with `b₀ = 11` and the drive `g = 2`433lowers the stiffness by `11 ln 2/(8π²)` from one cell to the next. -/434noncomputable def cellStep : ℝ := 11 * log 2 / (8 * π ^ 2)435436/-- The stiffness of the chart's cell `n` (46:B6): `ϑ_n = 1 − n · 11 ln 2/(8π²)`; the cell `0` is channel unity. -/437noncomputable def cellStiffness (n : ℕ) : ℝ := 1 - n * cellStep438439/-- The computed terms of the frame's fundamental plaquette coefficient, through `ϑ⁷` (46:C7):440`ϑ/3 + ϑ²/6 − 5ϑ⁴/72 − ϑ⁵/24 + 7ϑ⁶/720 + 59ϑ⁷/2160`. -/441noncomputable def c3terms (t : ℝ) : ℝ :=442 t / 3 + t ^ 2 / 6 - 5 / 72 * t ^ 4 - 1 / 24 * t ^ 5 + 7 / 720 * t ^ 6 + 59 / 2160 * t ^ 7443444/-- The chart's `u` at the cell `n`: the sum of the computed terms at the cell's stiffness. -/445noncomputable def cellU (n : ℕ) : ℝ := c3terms (cellStiffness n)446447/-- The step between `0.096566906` and `0.0965669688`, from Mathlib's brackets of `ln 2` and of `π`. -/448theorem cellStep_bracket : (0.096566906 : ℝ) ≤ cellStep ∧ cellStep ≤ (0.0965669688 : ℝ) := by449 have hl1 := log_two_gt_d9450 have hl2 := log_two_lt_d9451 have hp1 := pi_gt_d6452 have hp2 := pi_lt_d6453 have hp0 : (0 : ℝ) < π := pi_pos454 have hsq1 : (9.8696002 : ℝ) < π ^ 2 := by nlinarith [hp1, hp0]455 have hsq2 : π ^ 2 < (9.8696066 : ℝ) := by nlinarith [hp2, hp0]456 have hpos : (0 : ℝ) < 8 * π ^ 2 := by positivity457 unfold cellStep458 constructor459 · rw [le_div_iff₀ hpos]; linarith460 · rw [div_le_iff₀ hpos]; linarith461462/-- The stiffness of the cell `n` between `1 − n · 0.0965669688` and `1 − n · 0.096566906`. -/463theorem cellStiffness_bracket (n : ℕ) :464 1 - n * (0.0965669688 : ℝ) ≤ cellStiffness n ∧ cellStiffness n ≤ 1 - n * (0.096566906 : ℝ) := by465 have h := cellStep_bracket466 have hn : (0 : ℝ) ≤ n := Nat.cast_nonneg n467 have h1 := mul_le_mul_of_nonneg_left h.1 hn468 have h2 := mul_le_mul_of_nonneg_left h.2 hn469 unfold cellStiffness470 constructor <;> linarith471472/-- The computed terms on an interval `0 ≤ a ≤ t ≤ b`: each term at the end its sign selects. -/473theorem c3terms_bracket (t a b : ℝ) (ha : 0 ≤ a) (hat : a ≤ t) (htb : t ≤ b) :474 a / 3 + a ^ 2 / 6 - 5 / 72 * b ^ 4 - 1 / 24 * b ^ 5 + 7 / 720 * a ^ 6 + 59 / 2160 * a ^ 7 ≤ c3terms t ∧475 c3terms t ≤ b / 3 + b ^ 2 / 6 - 5 / 72 * a ^ 4 - 1 / 24 * a ^ 5 + 7 / 720 * b ^ 6 + 59 / 2160 * b ^ 7 := by476 have ht : 0 ≤ t := le_trans ha hat477 have a2 := pow_le_pow_left₀ ha hat 2478 have a4 := pow_le_pow_left₀ ha hat 4479 have a5 := pow_le_pow_left₀ ha hat 5480 have a6 := pow_le_pow_left₀ ha hat 6481 have a7 := pow_le_pow_left₀ ha hat 7482 have b2 := pow_le_pow_left₀ ht htb 2483 have b4 := pow_le_pow_left₀ ht htb 4484 have b5 := pow_le_pow_left₀ ht htb 5485 have b6 := pow_le_pow_left₀ ht htb 6486 have b7 := pow_le_pow_left₀ ht htb 7487 unfold c3terms488 constructor <;> linarith489490/-- The three orders of the imported series on an interval `0 ≤ a ≤ u ≤ b`: each term at the end its sign selects. -/491theorem P_bracket (u a b : ℝ) (ha : 0 ≤ a) (hau : a ≤ u) (hub : u ≤ b) :492 (-3 * b + 9 * a ^ 2 - 27 / 2 * b ^ 3 ≤ P3 u ∧ P3 u ≤ -3 * a + 9 * b ^ 2 - 27 / 2 * a ^ 3) ∧493 (-3 * b + 9 * a ^ 2 - 27 / 2 * b ^ 3 - 7 * b ^ 4 - 297 / 2 * b ^ 5 ≤ P5 u ∧494 P5 u ≤ -3 * a + 9 * b ^ 2 - 27 / 2 * a ^ 3 - 7 * a ^ 4 - 297 / 2 * a ^ 5) ∧495 (-3 * b + 9 * a ^ 2 - 27 / 2 * b ^ 3 - 7 * b ^ 4 - 297 / 2 * b ^ 5 + 858827 / 10240 * a ^ 6 + 47641149 / 71680 * a ^ 7 ≤ P7 u ∧496 P7 u ≤ -3 * a + 9 * b ^ 2 - 27 / 2 * a ^ 3 - 7 * a ^ 4 - 297 / 2 * a ^ 5 + 858827 / 10240 * b ^ 6 + 47641149 / 71680 * b ^ 7) := by497 have hu : 0 ≤ u := le_trans ha hau498 have a2 := pow_le_pow_left₀ ha hau 2499 have a3 := pow_le_pow_left₀ ha hau 3500 have a4 := pow_le_pow_left₀ ha hau 4501 have a5 := pow_le_pow_left₀ ha hau 5502 have a6 := pow_le_pow_left₀ ha hau 6503 have a7 := pow_le_pow_left₀ ha hau 7504 have b2 := pow_le_pow_left₀ hu hub 2505 have b3 := pow_le_pow_left₀ hu hub 3506 have b4 := pow_le_pow_left₀ hu hub 4507 have b5 := pow_le_pow_left₀ hu hub 5508 have b6 := pow_le_pow_left₀ hu hub 6509 have b7 := pow_le_pow_left₀ hu hub 7510 unfold P7 P5 P3511 refine ⟨⟨by linarith, by linarith⟩, ⟨by linarith, by linarith⟩, ⟨by linarith, by linarith⟩⟩512513/-- A bracket of `ratio u P` from brackets `Llo ≤ −log u ≤ Lhi` and `Plo ≤ P ≤ Phi` and rational square-root ends514`slo² < Llo`, `Lhi < shi²`. -/515theorem ratio_bracket_Icc (u P Llo Lhi Plo Phi slo shi lo hi : ℝ) (hL : Llo ≤ -log u ∧ -log u ≤ Lhi)516 (hPb : Plo ≤ P ∧ P ≤ Phi) (hslo : 0 < slo) (hs1 : slo ^ 2 < Llo) (hshi : 0 < shi) (hs2 : Lhi < shi ^ 2)517 (hP : 0 < 4 * Llo + Plo) (hlo : lo ≤ (4 * Llo + Plo) / shi) (hhi : (4 * Lhi + Phi) / slo ≤ hi) :518 lo ≤ ratio u P ∧ ratio u P ≤ hi := by519 have hs_lo : slo < √(-log u) := by rw [lt_sqrt hslo.le]; linarith [hL.1]520 have hs_hi : √(-log u) < shi := by rw [sqrt_lt' hshi]; linarith [hL.2]521 have hspos : 0 < √(-log u) := lt_trans hslo hs_lo522 have hnum : 0 < 4 * (-log u) + P := by linarith [hL.1, hPb.1]523 unfold ratio524 constructor525 · refine le_trans hlo ?_526 rw [div_le_div_iff₀ hshi hspos]527 nlinarith [mul_nonneg hP.le (sub_nonneg.2 hs_hi.le),528 mul_nonneg (by linarith [hL.1, hPb.1] : (0 : ℝ) ≤ 4 * (-log u) + P - (4 * Llo + Plo)) hshi.le]529 · refine le_trans ?_ hhi530 rw [div_le_div_iff₀ hspos hslo]531 nlinarith [mul_nonneg hnum.le (sub_nonneg.2 hs_lo.le),532 mul_nonneg (by linarith [hL.2, hPb.2] : (0 : ℝ) ≤ 4 * Lhi + Phi - (4 * (-log u) + P)) hspos.le]533534set_option maxHeartbeats 4000000 in535/-- The series bracket of `log (0.04646)` after `12` terms, mantissa `2^4`. -/536theorem logb_cell9a : (-0.2965748555 : ℝ) - 4 * log 2 ≤ log (0.04646) ∧ log (0.04646) ≤ (-0.296574799 : ℝ) - 4 * log 2 := by537 simpa using log_mantissa_bracket (0.04646) 4 12 (-0.2965748555 : ℝ) (-0.296574799 : ℝ) (by norm_num) (by norm_num)538 (by norm_num [sum_range_succ]) (by norm_num [sum_range_succ])539540set_option maxHeartbeats 4000000 in541/-- The series bracket of `log (0.04647)` after `12` terms, mantissa `2^4`. -/542theorem logb_cell9b : (-0.2963596395 : ℝ) - 4 * log 2 ≤ log (0.04647) ∧ log (0.04647) ≤ (-0.2963595835 : ℝ) - 4 * log 2 := by543 simpa using log_mantissa_bracket (0.04647) 4 12 (-0.2963596395 : ℝ) (-0.2963595835 : ℝ) (by norm_num) (by norm_num)544 (by norm_num [sum_range_succ]) (by norm_num [sum_range_succ])545546set_option maxHeartbeats 4000000 in547/-- The series bracket of `log (0.08423)` after `14` terms, mantissa `2^3`. -/548theorem logb_cell8a : (-0.3947626548 : ℝ) - 3 * log 2 ≤ log (0.08423) ∧ log (0.08423) ≤ (-0.3947625055 : ℝ) - 3 * log 2 := by549 simpa using log_mantissa_bracket (0.08423) 3 14 (-0.3947626548 : ℝ) (-0.3947625055 : ℝ) (by norm_num) (by norm_num)550 (by norm_num [sum_range_succ]) (by norm_num [sum_range_succ])551552set_option maxHeartbeats 4000000 in553/-- The series bracket of `log (0.08424)` after `14` terms, mantissa `2^3`. -/554theorem logb_cell8b : (-0.3946439391 : ℝ) - 3 * log 2 ≤ log (0.08424) ∧ log (0.08424) ≤ (-0.3946437903 : ℝ) - 3 * log 2 := by555 simpa using log_mantissa_bracket (0.08424) 3 14 (-0.3946439391 : ℝ) (-0.3946437903 : ℝ) (by norm_num) (by norm_num)556 (by norm_num [sum_range_succ]) (by norm_num [sum_range_succ])557558set_option maxHeartbeats 4000000 in559/-- The series bracket of `log (0.12461)` after `2` terms, mantissa `2^3`. -/560theorem logb_cell7a : (-0.0031248977 : ℝ) - 3 * log 2 ≤ log (0.12461) ∧ log (0.12461) ≤ (-0.0031248367 : ℝ) - 3 * log 2 := by561 simpa using log_mantissa_bracket (0.12461) 3 2 (-0.0031248977 : ℝ) (-0.0031248367 : ℝ) (by norm_num) (by norm_num)562 (by norm_num [sum_range_succ]) (by norm_num [sum_range_succ])563564set_option maxHeartbeats 4000000 in565/-- The series bracket of `log (0.12462)` after `2` terms, mantissa `2^3`. -/566theorem logb_cell7b : (-0.003044649 : ℝ) - 3 * log 2 ≤ log (0.12462) ∧ log (0.12462) ≤ (-0.0030445926 : ℝ) - 3 * log 2 := by567 simpa using log_mantissa_bracket (0.12462) 3 2 (-0.003044649 : ℝ) (-0.0030445926 : ℝ) (by norm_num) (by norm_num)568 (by norm_num [sum_range_succ]) (by norm_num [sum_range_succ])569570set_option maxHeartbeats 4000000 in571/-- The series bracket of `log (0.16707)` after `14` terms, mantissa `2^2`. -/572theorem logb_cell6a : (-0.4030481223 : ℝ) - 2 * log 2 ≤ log (0.16707) ∧ log (0.16707) ≤ (-0.4030479283 : ℝ) - 2 * log 2 := by573 simpa using log_mantissa_bracket (0.16707) 2 14 (-0.4030481223 : ℝ) (-0.4030479283 : ℝ) (by norm_num) (by norm_num)574 (by norm_num [sum_range_succ]) (by norm_num [sum_range_succ])575576set_option maxHeartbeats 4000000 in577/-- The series bracket of `log (0.16708)` after `14` terms, mantissa `2^2`. -/578theorem logb_cell6b : (-0.4029882688 : ℝ) - 2 * log 2 ≤ log (0.16708) ∧ log (0.16708) ≤ (-0.4029880751 : ℝ) - 2 * log 2 := by579 simpa using log_mantissa_bracket (0.16708) 2 14 (-0.4029882688 : ℝ) (-0.4029880751 : ℝ) (by norm_num) (by norm_num)580 (by norm_num [sum_range_succ]) (by norm_num [sum_range_succ])581582set_option maxHeartbeats 4000000 in583/-- The series bracket of `log (0.25528)` after `23` terms, mantissa `2^1`. -/584theorem logb_cell4a : (-0.6722471836 : ℝ) - log 2 ≤ log (0.25528) ∧ log (0.25528) ≤ (-0.6722470436 : ℝ) - log 2 := by585 simpa using log_mantissa_bracket (0.25528) 1 23 (-0.6722471836 : ℝ) (-0.6722470436 : ℝ) (by norm_num) (by norm_num)586 (by norm_num [sum_range_succ]) (by norm_num [sum_range_succ])587588set_option maxHeartbeats 4000000 in589/-- The series bracket of `log (0.2553)` after `23` terms, mantissa `2^1`. -/590theorem logb_cell4b : (-0.6721688412 : ℝ) - log 2 ≤ log (0.2553) ∧ log (0.2553) ≤ (-0.6721687015 : ℝ) - log 2 := by591 simpa using log_mantissa_bracket (0.2553) 1 23 (-0.6721688412 : ℝ) (-0.6721687015 : ℝ) (by norm_num) (by norm_num)592 (by norm_num [sum_range_succ]) (by norm_num [sum_range_succ])593594set_option maxHeartbeats 4000000 in595/-- The series bracket of `log (0.29938)` after `18` terms, mantissa `2^1`. -/596theorem logb_cell3a : (-0.5128944752 : ℝ) - log 2 ≤ log (0.29938) ∧ log (0.29938) ≤ (-0.5128943777 : ℝ) - log 2 := by597 simpa using log_mantissa_bracket (0.29938) 1 18 (-0.5128944752 : ℝ) (-0.5128943777 : ℝ) (by norm_num) (by norm_num)598 (by norm_num [sum_range_succ]) (by norm_num [sum_range_succ])599600set_option maxHeartbeats 4000000 in601/-- The series bracket of `log (0.29939)` after `18` terms, mantissa `2^1`. -/602theorem logb_cell3b : (-0.5128610733 : ℝ) - log 2 ≤ log (0.29939) ∧ log (0.29939) ≤ (-0.512860976 : ℝ) - log 2 := by603 simpa using log_mantissa_bracket (0.29939) 1 18 (-0.5128610733 : ℝ) (-0.512860976 : ℝ) (by norm_num) (by norm_num)604 (by norm_num [sum_range_succ]) (by norm_num [sum_range_succ])605606set_option maxHeartbeats 4000000 in607/-- The series bracket of `log (0.34254)` after `14` terms, mantissa `2^1`. -/608theorem logb_cell2a : (-0.3782196998 : ℝ) - log 2 ≤ log (0.34254) ∧ log (0.34254) ≤ (-0.378219613 : ℝ) - log 2 := by609 simpa using log_mantissa_bracket (0.34254) 1 14 (-0.3782196998 : ℝ) (-0.378219613 : ℝ) (by norm_num) (by norm_num)610 (by norm_num [sum_range_succ]) (by norm_num [sum_range_succ])611612set_option maxHeartbeats 4000000 in613/-- The series bracket of `log (0.34255)` after `14` terms, mantissa `2^1`. -/614theorem logb_cell2b : (-0.3781905065 : ℝ) - log 2 ≤ log (0.34255) ∧ log (0.34255) ≤ (-0.3781904198 : ℝ) - log 2 := by615 simpa using log_mantissa_bracket (0.34255) 1 14 (-0.3781905065 : ℝ) (-0.3781904198 : ℝ) (by norm_num) (by norm_num)616 (by norm_num [sum_range_succ]) (by norm_num [sum_range_succ])617618set_option maxHeartbeats 4000000 in619/-- The series bracket of `log (23 / 54)` after `8` terms, mantissa `2^1`. -/620theorem logb_cell0a : (-0.1603426861 : ℝ) - log 2 ≤ log (23 / 54) ∧ log (23 / 54) ≤ (-0.1603426053 : ℝ) - log 2 := by621 simpa using log_mantissa_bracket (23 / 54) 1 8 (-0.1603426861 : ℝ) (-0.1603426053 : ℝ) (by norm_num) (by norm_num)622 (by norm_num [sum_range_succ]) (by norm_num [sum_range_succ])623624set_option maxHeartbeats 1000000 in625/-- The cell `n = 9`: the stiffness lies in `[0.13089728, 0.130897846]`, `u` in `[0.04646, 0.04647]`, and the orders `3`, `5`, `7` in the stated brackets. -/626theorem cell9_ratios :627 ((6.93 : ℝ) ≤ ratio (cellU 9) (P3 (cellU 9)) ∧ ratio (cellU 9) (P3 (cellU 9)) ≤ (6.94 : ℝ)) ∧628 ((6.93 : ℝ) ≤ ratio (cellU 9) (P5 (cellU 9)) ∧ ratio (cellU 9) (P5 (cellU 9)) ≤ (6.94 : ℝ)) ∧629 ((6.93 : ℝ) ≤ ratio (cellU 9) (P7 (cellU 9)) ∧ ratio (cellU 9) (P7 (cellU 9)) ≤ (6.94 : ℝ)) := by630 have hθ : (0.13089728 : ℝ) ≤ cellStiffness 9 ∧ cellStiffness 9 ≤ (0.130897846 : ℝ) := by631 have h := cellStiffness_bracket 9632 push_cast at h633 constructor <;> linarith [h.1, h.2]634 have hc := c3terms_bracket (cellStiffness 9) (0.13089728 : ℝ) (0.130897846 : ℝ) (by norm_num) hθ.1 hθ.2635 have hu : (0.04646 : ℝ) ≤ cellU 9 ∧ cellU 9 ≤ (0.04647 : ℝ) := by636 unfold cellU637 constructor638 · refine le_trans ?_ hc.1; norm_num639 · refine le_trans hc.2 ?_; norm_num640 have hua : (0 : ℝ) < 0.04646 := by norm_num641 have hla := Real.log_le_log hua hu.1642 have hlb := Real.log_le_log (lt_of_lt_of_le hua hu.1) hu.2643 have hl1 := log_two_gt_d9644 have hl2 := log_two_lt_d9645 have hA := logb_cell9a646 have hB := logb_cell9b647 have hL : (3.0689483047 : ℝ) ≤ -log (cellU 9) ∧ -log (cellU 9) ≤ (3.0691635787 : ℝ) := by648 constructor <;> linarith [hA.1, hA.2, hB.1, hB.2]649 have hP := P_bracket (cellU 9) (0.04646 : ℝ) (0.04647 : ℝ) (by norm_num) hu.1 hu.2650 have hP3 : (-0.1213379426 : ℝ) ≤ P3 (cellU 9) ∧ P3 (cellU 9) ≤ (-0.1212987045 : ℝ) := by651 constructor652 · refine le_trans ?_ hP.1.1; norm_num653 · refine le_trans hP.1.2 ?_; norm_num654 have hr3 := ratio_bracket_Icc (cellU 9) (P3 (cellU 9)) (3.0689483047 : ℝ) (3.0691635787 : ℝ) (-0.1213379426 : ℝ) (-0.1212987045 : ℝ) (1.7518413 : ℝ) (1.751903 : ℝ) (6.93 : ℝ) (6.94 : ℝ) hL hP3655 (by norm_num) (by norm_num) (by norm_num) (by norm_num) (by norm_num) (by norm_num) (by norm_num)656 have hP5 : (-0.1214027658 : ℝ) ≤ P5 (cellU 9) ∧ P5 (cellU 9) ≤ (-0.1213634649 : ℝ) := by657 constructor658 · refine le_trans ?_ hP.2.1.1; norm_num659 · refine le_trans hP.2.1.2 ?_; norm_num660 have hr5 := ratio_bracket_Icc (cellU 9) (P5 (cellU 9)) (3.0689483047 : ℝ) (3.0691635787 : ℝ) (-0.1214027658 : ℝ) (-0.1213634649 : ℝ) (1.7518413 : ℝ) (1.751903 : ℝ) (6.93 : ℝ) (6.94 : ℝ) hL hP5661 (by norm_num) (by norm_num) (by norm_num) (by norm_num) (by norm_num) (by norm_num) (by norm_num)662 have hP7 : (-0.1214016118 : ℝ) ≤ P7 (cellU 9) ∧ P7 (cellU 9) ≤ (-0.1213623093 : ℝ) := by663 constructor664 · refine le_trans ?_ hP.2.2.1; norm_num665 · refine le_trans hP.2.2.2 ?_; norm_num666 have hr7 := ratio_bracket_Icc (cellU 9) (P7 (cellU 9)) (3.0689483047 : ℝ) (3.0691635787 : ℝ) (-0.1214016118 : ℝ) (-0.1213623093 : ℝ) (1.7518413 : ℝ) (1.751903 : ℝ) (6.93 : ℝ) (6.94 : ℝ) hL hP7667 (by norm_num) (by norm_num) (by norm_num) (by norm_num) (by norm_num) (by norm_num) (by norm_num)668 exact ⟨hr3, hr5, hr7⟩669670set_option maxHeartbeats 1000000 in671/-- The cell `n = 8`: the stiffness lies in `[0.227464249, 0.227464752]`, `u` in `[0.08423, 0.08424]`, and the orders `3`, `5`, `7` in the stated brackets. -/672theorem cell8_ratios :673 ((6.16 : ℝ) ≤ ratio (cellU 8) (P3 (cellU 8)) ∧ ratio (cellU 8) (P3 (cellU 8)) ≤ (6.17 : ℝ)) ∧674 ((6.16 : ℝ) ≤ ratio (cellU 8) (P5 (cellU 8)) ∧ ratio (cellU 8) (P5 (cellU 8)) ≤ (6.17 : ℝ)) ∧675 ((6.16 : ℝ) ≤ ratio (cellU 8) (P7 (cellU 8)) ∧ ratio (cellU 8) (P7 (cellU 8)) ≤ (6.17 : ℝ)) := by676 have hθ : (0.227464249 : ℝ) ≤ cellStiffness 8 ∧ cellStiffness 8 ≤ (0.227464752 : ℝ) := by677 have h := cellStiffness_bracket 8678 push_cast at h679 constructor <;> linarith [h.1, h.2]680 have hc := c3terms_bracket (cellStiffness 8) (0.227464249 : ℝ) (0.227464752 : ℝ) (by norm_num) hθ.1 hθ.2681 have hu : (0.08423 : ℝ) ≤ cellU 8 ∧ cellU 8 ≤ (0.08424 : ℝ) := by682 unfold cellU683 constructor684 · refine le_trans ?_ hc.1; norm_num685 · refine le_trans hc.2 ?_; norm_num686 have hua : (0 : ℝ) < 0.08423 := by norm_num687 have hla := Real.log_le_log hua hu.1688 have hlb := Real.log_le_log (lt_of_lt_of_le hua hu.1) hu.2689 have hl1 := log_two_gt_d9690 have hl2 := log_two_lt_d9691 have hA := logb_cell8a692 have hB := logb_cell8b693 have hL : (2.4740853312 : ℝ) ≤ -log (cellU 8) ∧ -log (cellU 8) ≤ (2.4742041972 : ℝ) := by694 constructor <;> linarith [hA.1, hA.2, hB.1, hB.2]695 have hP := P_bracket (cellU 8) (0.08423 : ℝ) (0.08424 : ℝ) (by norm_num) hu.1 hu.2696 have hP3 : (-0.1969380484 : ℝ) ≤ P3 (cellU 8) ∧ P3 (cellU 8) ≤ (-0.1968900123 : ℝ) := by697 constructor698 · refine le_trans ?_ hP.1.1; norm_num699 · refine le_trans hP.1.2 ?_; norm_num700 have hr3 := ratio_bracket_Icc (cellU 8) (P3 (cellU 8)) (2.4740853312 : ℝ) (2.4742041972 : ℝ) (-0.1969380484 : ℝ) (-0.1968900123 : ℝ) (1.5729224 : ℝ) (1.5729605 : ℝ) (6.16 : ℝ) (6.17 : ℝ) hL hP3701 (by norm_num) (by norm_num) (by norm_num) (by norm_num) (by norm_num) (by norm_num) (by norm_num)702 have hP5 : (-0.1979205261 : ℝ) ≤ P5 (cellU 8) ∧ P5 (cellU 8) ≤ (-0.1978719488 : ℝ) := by703 constructor704 · refine le_trans ?_ hP.2.1.1; norm_num705 · refine le_trans hP.2.1.2 ?_; norm_num706 have hr5 := ratio_bracket_Icc (cellU 8) (P5 (cellU 8)) (2.4740853312 : ℝ) (2.4742041972 : ℝ) (-0.1979205261 : ℝ) (-0.1978719488 : ℝ) (1.5729224 : ℝ) (1.5729605 : ℝ) (6.16 : ℝ) (6.17 : ℝ) hL hP5707 (by norm_num) (by norm_num) (by norm_num) (by norm_num) (by norm_num) (by norm_num) (by norm_num)708 have hP7 : (-0.1978705836 : ℝ) ≤ P7 (cellU 8) ∧ P7 (cellU 8) ≤ (-0.1978219684 : ℝ) := by709 constructor710 · refine le_trans ?_ hP.2.2.1; norm_num711 · refine le_trans hP.2.2.2 ?_; norm_num712 have hr7 := ratio_bracket_Icc (cellU 8) (P7 (cellU 8)) (2.4740853312 : ℝ) (2.4742041972 : ℝ) (-0.1978705836 : ℝ) (-0.1978219684 : ℝ) (1.5729224 : ℝ) (1.5729605 : ℝ) (6.16 : ℝ) (6.17 : ℝ) hL hP7713 (by norm_num) (by norm_num) (by norm_num) (by norm_num) (by norm_num) (by norm_num) (by norm_num)714 exact ⟨hr3, hr5, hr7⟩715716set_option maxHeartbeats 1000000 in717/-- The cell `n = 7`: the stiffness lies in `[0.324031218, 0.324031658]`, `u` in `[0.12461, 0.12462]`, and the orders `3`, `5`, `7` in the stated brackets. -/718theorem cell7_ratios :719 ((5.59 : ℝ) ≤ ratio (cellU 7) (P3 (cellU 7)) ∧ ratio (cellU 7) (P3 (cellU 7)) ≤ (5.6 : ℝ)) ∧720 ((5.58 : ℝ) ≤ ratio (cellU 7) (P5 (cellU 7)) ∧ ratio (cellU 7) (P5 (cellU 7)) ≤ (5.59 : ℝ)) ∧721 ((5.58 : ℝ) ≤ ratio (cellU 7) (P7 (cellU 7)) ∧ ratio (cellU 7) (P7 (cellU 7)) ≤ (5.59 : ℝ)) := by722 have hθ : (0.324031218 : ℝ) ≤ cellStiffness 7 ∧ cellStiffness 7 ≤ (0.324031658 : ℝ) := by723 have h := cellStiffness_bracket 7724 push_cast at h725 constructor <;> linarith [h.1, h.2]726 have hc := c3terms_bracket (cellStiffness 7) (0.324031218 : ℝ) (0.324031658 : ℝ) (by norm_num) hθ.1 hθ.2727 have hu : (0.12461 : ℝ) ≤ cellU 7 ∧ cellU 7 ≤ (0.12462 : ℝ) := by728 unfold cellU729 constructor730 · refine le_trans ?_ hc.1; norm_num731 · refine le_trans hc.2 ?_; norm_num732 have hua : (0 : ℝ) < 0.12461 := by norm_num733 have hla := Real.log_le_log hua hu.1734 have hlb := Real.log_le_log (lt_of_lt_of_le hua hu.1) hu.2735 have hl1 := log_two_gt_d9736 have hl2 := log_two_lt_d9737 have hA := logb_cell7a738 have hB := logb_cell7b739 have hL : (2.0824861335 : ℝ) ≤ -log (cellU 7) ∧ -log (cellU 7) ≤ (2.0825664401 : ℝ) := by740 constructor <;> linarith [hA.1, hA.2, hB.1, hB.2]741 have hP := P_bracket (cellU 7) (0.12461 : ℝ) (0.12462 : ℝ) (by norm_num) hu.1 hu.2742 have hP3 : (-0.2602385802 : ℝ) ≤ P3 (cellU 7) ∧ P3 (cellU 7) ≤ (-0.2601798602 : ℝ) := by743 constructor744 · refine le_trans ?_ hP.1.1; norm_num745 · refine le_trans hP.1.2 ?_; norm_num746 have hr3 := ratio_bracket_Icc (cellU 7) (P3 (cellU 7)) (2.0824861335 : ℝ) (2.0825664401 : ℝ) (-0.2602385802 : ℝ) (-0.2601798602 : ℝ) (1.443082 : ℝ) (1.4431101 : ℝ) (5.59 : ℝ) (5.6 : ℝ) hL hP3747 (by norm_num) (by norm_num) (by norm_num) (by norm_num) (by norm_num) (by norm_num) (by norm_num)748 have hP5 : (-0.2663902715 : ℝ) ≤ P5 (cellU 7) ∧ P5 (cellU 7) ≤ (-0.2663292191 : ℝ) := by749 constructor750 · refine le_trans ?_ hP.2.1.1; norm_num751 · refine le_trans hP.2.1.2 ?_; norm_num752 have hr5 := ratio_bracket_Icc (cellU 7) (P5 (cellU 7)) (2.0824861335 : ℝ) (2.0825664401 : ℝ) (-0.2663902715 : ℝ) (-0.2663292191 : ℝ) (1.443082 : ℝ) (1.4431101 : ℝ) (5.58 : ℝ) (5.59 : ℝ) hL hP5753 (by norm_num) (by norm_num) (by norm_num) (by norm_num) (by norm_num) (by norm_num) (by norm_num)754 have hP7 : (-0.26576621 : ℝ) ≤ P7 (cellU 7) ∧ P7 (cellU 7) ≤ (-0.2657048322 : ℝ) := by755 constructor756 · refine le_trans ?_ hP.2.2.1; norm_num757 · refine le_trans hP.2.2.2 ?_; norm_num758 have hr7 := ratio_bracket_Icc (cellU 7) (P7 (cellU 7)) (2.0824861335 : ℝ) (2.0825664401 : ℝ) (-0.26576621 : ℝ) (-0.2657048322 : ℝ) (1.443082 : ℝ) (1.4431101 : ℝ) (5.58 : ℝ) (5.59 : ℝ) hL hP7759 (by norm_num) (by norm_num) (by norm_num) (by norm_num) (by norm_num) (by norm_num) (by norm_num)760 exact ⟨hr3, hr5, hr7⟩761762set_option maxHeartbeats 1000000 in763/-- The cell `n = 6`: the stiffness lies in `[0.420598187, 0.420598564]`, `u` in `[0.16707, 0.16708]`, and the orders `3`, `5`, `7` in the stated brackets. -/764theorem cell6_ratios :765 ((5.11 : ℝ) ≤ ratio (cellU 6) (P3 (cellU 6)) ∧ ratio (cellU 6) (P3 (cellU 6)) ≤ (5.12 : ℝ)) ∧766 ((5.09 : ℝ) ≤ ratio (cellU 6) (P5 (cellU 6)) ∧ ratio (cellU 6) (P5 (cellU 6)) ≤ (5.1 : ℝ)) ∧767 ((5.1 : ℝ) ≤ ratio (cellU 6) (P7 (cellU 6)) ∧ ratio (cellU 6) (P7 (cellU 6)) ≤ (5.11 : ℝ)) := by768 have hθ : (0.420598187 : ℝ) ≤ cellStiffness 6 ∧ cellStiffness 6 ≤ (0.420598564 : ℝ) := by769 have h := cellStiffness_bracket 6770 push_cast at h771 constructor <;> linarith [h.1, h.2]772 have hc := c3terms_bracket (cellStiffness 6) (0.420598187 : ℝ) (0.420598564 : ℝ) (by norm_num) hθ.1 hθ.2773 have hu : (0.16707 : ℝ) ≤ cellU 6 ∧ cellU 6 ≤ (0.16708 : ℝ) := by774 unfold cellU775 constructor776 · refine le_trans ?_ hc.1; norm_num777 · refine le_trans hc.2 ?_; norm_num778 have hua : (0 : ℝ) < 0.16707 := by norm_num779 have hla := Real.log_le_log hua hu.1780 have hlb := Real.log_le_log (lt_of_lt_of_le hua hu.1) hu.2781 have hl1 := log_two_gt_d9782 have hl2 := log_two_lt_d9783 have hA := logb_cell6a784 have hB := logb_cell6b785 have hL : (1.7892824357 : ℝ) ≤ -log (cellU 6) ∧ -log (cellU 6) ≤ (1.7893424839 : ℝ) := by786 constructor <;> linarith [hA.1, hA.2, hB.1, hB.2]787 have hP := P_bracket (cellU 6) (0.16707 : ℝ) (0.16708 : ℝ) (by norm_num) hu.1 hu.2788 have hP3 : (-0.3129946901 : ℝ) ≤ P3 (cellU 6) ∧ P3 (cellU 6) ≤ (-0.3129233113 : ℝ) := by789 constructor790 · refine le_trans ?_ hP.1.1; norm_num791 · refine le_trans hP.1.2 ?_; norm_num792 have hr3 := ratio_bracket_Icc (cellU 6) (P3 (cellU 6)) (1.7892824357 : ℝ) (1.7893424839 : ℝ) (-0.3129946901 : ℝ) (-0.3129233113 : ℝ) (1.3376405 : ℝ) (1.3376632 : ℝ) (5.11 : ℝ) (5.12 : ℝ) hL hP3793 (by norm_num) (by norm_num) (by norm_num) (by norm_num) (by norm_num) (by norm_num) (by norm_num)794 have hP5 : (-0.3377849098 : ℝ) ≤ P5 (cellU 6) ∧ P5 (cellU 6) ≤ (-0.3377064397 : ℝ) := by795 constructor796 · refine le_trans ?_ hP.2.1.1; norm_num797 · refine le_trans hP.2.1.2 ?_; norm_num798 have hr5 := ratio_bracket_Icc (cellU 6) (P5 (cellU 6)) (1.7892824357 : ℝ) (1.7893424839 : ℝ) (-0.3377849098 : ℝ) (-0.3377064397 : ℝ) (1.3376405 : ℝ) (1.3376632 : ℝ) (5.09 : ℝ) (5.1 : ℝ) hL hP5799 (by norm_num) (by norm_num) (by norm_num) (by norm_num) (by norm_num) (by norm_num) (by norm_num)800 have hP7 : (-0.3335462709 : ℝ) ≤ P7 (cellU 6) ∧ P7 (cellU 6) ≤ (-0.3334661337 : ℝ) := by801 constructor802 · refine le_trans ?_ hP.2.2.1; norm_num803 · refine le_trans hP.2.2.2 ?_; norm_num804 have hr7 := ratio_bracket_Icc (cellU 6) (P7 (cellU 6)) (1.7892824357 : ℝ) (1.7893424839 : ℝ) (-0.3335462709 : ℝ) (-0.3334661337 : ℝ) (1.3376405 : ℝ) (1.3376632 : ℝ) (5.1 : ℝ) (5.11 : ℝ) hL hP7805 (by norm_num) (by norm_num) (by norm_num) (by norm_num) (by norm_num) (by norm_num) (by norm_num)806 exact ⟨hr3, hr5, hr7⟩807808set_option maxHeartbeats 1000000 in809/-- The cell `n = 4`: the stiffness lies in `[0.613732124, 0.613732376]`, `u` in `[0.25528, 0.2553]`, and the orders `3`, `5`, `7` in the stated brackets. -/810theorem cell4_ratios :811 ((4.32 : ℝ) ≤ ratio (cellU 4) (P3 (cellU 4)) ∧ ratio (cellU 4) (P3 (cellU 4)) ≤ (4.33 : ℝ)) ∧812 ((4.16 : ℝ) ≤ ratio (cellU 4) (P5 (cellU 4)) ∧ ratio (cellU 4) (P5 (cellU 4)) ≤ (4.17 : ℝ)) ∧813 ((4.22 : ℝ) ≤ ratio (cellU 4) (P7 (cellU 4)) ∧ ratio (cellU 4) (P7 (cellU 4)) ≤ (4.23 : ℝ)) := by814 have hθ : (0.613732124 : ℝ) ≤ cellStiffness 4 ∧ cellStiffness 4 ≤ (0.613732376 : ℝ) := by815 have h := cellStiffness_bracket 4816 push_cast at h817 constructor <;> linarith [h.1, h.2]818 have hc := c3terms_bracket (cellStiffness 4) (0.613732124 : ℝ) (0.613732376 : ℝ) (by norm_num) hθ.1 hθ.2819 have hu : (0.25528 : ℝ) ≤ cellU 4 ∧ cellU 4 ≤ (0.2553 : ℝ) := by820 unfold cellU821 constructor822 · refine le_trans ?_ hc.1; norm_num823 · refine le_trans hc.2 ?_; norm_num824 have hua : (0 : ℝ) < 0.25528 := by norm_num825 have hla := Real.log_le_log hua hu.1826 have hlb := Real.log_le_log (lt_of_lt_of_le hua hu.1) hu.2827 have hl1 := log_two_gt_d9828 have hl2 := log_two_lt_d9829 have hA := logb_cell4a830 have hB := logb_cell4b831 have hL : (1.3653158818 : ℝ) ≤ -log (cellU 4) ∧ -log (cellU 4) ≤ (1.3653943644 : ℝ) := by832 constructor <;> linarith [hA.1, hA.2, hB.1, hB.2]833 have hP := P_bracket (cellU 4) (0.25528 : ℝ) (0.2553 : ℝ) (by norm_num) hu.1 hu.2834 have hP3 : (-0.4040286405 : ℝ) ≤ P3 (cellU 4) ∧ P3 (cellU 4) ≤ (-0.4038239459 : ℝ) := by835 constructor836 · refine le_trans ?_ hP.1.1; norm_num837 · refine le_trans hP.1.2 ?_; norm_num838 have hr3 := ratio_bracket_Icc (cellU 4) (P3 (cellU 4)) (1.3653158818 : ℝ) (1.3653943644 : ℝ) (-0.4040286405 : ℝ) (-0.4038239459 : ℝ) (1.1684672 : ℝ) (1.1685011 : ℝ) (4.32 : ℝ) (4.33 : ℝ) hL hP3839 (by norm_num) (by norm_num) (by norm_num) (by norm_num) (by norm_num) (by norm_num) (by norm_num)840 have hP5 : (-0.5948232665 : ℝ) ≤ P5 (cellU 4) ∧ P5 (cellU 4) ≤ (-0.594546179 : ℝ) := by841 constructor842 · refine le_trans ?_ hP.2.1.1; norm_num843 · refine le_trans hP.2.1.2 ?_; norm_num844 have hr5 := ratio_bracket_Icc (cellU 4) (P5 (cellU 4)) (1.3653158818 : ℝ) (1.3653943644 : ℝ) (-0.5948232665 : ℝ) (-0.594546179 : ℝ) (1.1684672 : ℝ) (1.1685011 : ℝ) (4.16 : ℝ) (4.17 : ℝ) hL hP5845 (by norm_num) (by norm_num) (by norm_num) (by norm_num) (by norm_num) (by norm_num) (by norm_num)846 have hP7 : (-0.5246544374 : ℝ) ≤ P7 (cellU 4) ∧ P7 (cellU 4) ≤ (-0.5243406784 : ℝ) := by847 constructor848 · refine le_trans ?_ hP.2.2.1; norm_num849 · refine le_trans hP.2.2.2 ?_; norm_num850 have hr7 := ratio_bracket_Icc (cellU 4) (P7 (cellU 4)) (1.3653158818 : ℝ) (1.3653943644 : ℝ) (-0.5246544374 : ℝ) (-0.5243406784 : ℝ) (1.1684672 : ℝ) (1.1685011 : ℝ) (4.22 : ℝ) (4.23 : ℝ) hL hP7851 (by norm_num) (by norm_num) (by norm_num) (by norm_num) (by norm_num) (by norm_num) (by norm_num)852 exact ⟨hr3, hr5, hr7⟩853854set_option maxHeartbeats 1000000 in855/-- The cell `n = 3`: the stiffness lies in `[0.710299093, 0.710299282]`, `u` in `[0.29938, 0.29939]`, and the orders `3`, `5`, `7` in the stated brackets. -/856theorem cell3_ratios :857 ((3.97 : ℝ) ≤ ratio (cellU 3) (P3 (cellU 3)) ∧ ratio (cellU 3) (P3 (cellU 3)) ≤ (3.98 : ℝ)) ∧858 ((3.6 : ℝ) ≤ ratio (cellU 3) (P5 (cellU 3)) ∧ ratio (cellU 3) (P5 (cellU 3)) ≤ (3.61 : ℝ)) ∧859 ((3.78 : ℝ) ≤ ratio (cellU 3) (P7 (cellU 3)) ∧ ratio (cellU 3) (P7 (cellU 3)) ≤ (3.79 : ℝ)) := by860 have hθ : (0.710299093 : ℝ) ≤ cellStiffness 3 ∧ cellStiffness 3 ≤ (0.710299282 : ℝ) := by861 have h := cellStiffness_bracket 3862 push_cast at h863 constructor <;> linarith [h.1, h.2]864 have hc := c3terms_bracket (cellStiffness 3) (0.710299093 : ℝ) (0.710299282 : ℝ) (by norm_num) hθ.1 hθ.2865 have hu : (0.29938 : ℝ) ≤ cellU 3 ∧ cellU 3 ≤ (0.29939 : ℝ) := by866 unfold cellU867 constructor868 · refine le_trans ?_ hc.1; norm_num869 · refine le_trans hc.2 ?_; norm_num870 have hua : (0 : ℝ) < 0.29938 := by norm_num871 have hla := Real.log_le_log hua hu.1872 have hlb := Real.log_le_log (lt_of_lt_of_le hua hu.1) hu.2873 have hl1 := log_two_gt_d9874 have hl2 := log_two_lt_d9875 have hA := logb_cell3a876 have hB := logb_cell3b877 have hL : (1.2060081563 : ℝ) ≤ -log (cellU 3) ∧ -log (cellU 3) ≤ (1.206041656 : ℝ) := by878 constructor <;> linarith [hA.1, hA.2, hB.1, hB.2]879 have hP := P_bracket (cellU 3) (0.29938 : ℝ) (0.29939 : ℝ) (by norm_num) hu.1 hu.2880 have hP3 : (-0.4537956084 : ℝ) ≤ P3 (cellU 3) ∧ P3 (cellU 3) ≤ (-0.4536754183 : ℝ) := by881 constructor882 · refine le_trans ?_ hP.1.1; norm_num883 · refine le_trans hP.1.2 ?_; norm_num884 have hr3 := ratio_bracket_Icc (cellU 3) (P3 (cellU 3)) (1.2060081563 : ℝ) (1.206041656 : ℝ) (-0.4537956084 : ℝ) (-0.4536754183 : ℝ) (1.0981839 : ℝ) (1.0981994 : ℝ) (3.97 : ℝ) (3.98 : ℝ) hL hP3885 (by norm_num) (by norm_num) (by norm_num) (by norm_num) (by norm_num) (by norm_num) (by norm_num)886 have hP5 : (-0.8672370496 : ℝ) ≤ P5 (cellU 3) ∧ P5 (cellU 3) ≤ (-0.867049695 : ℝ) := by887 constructor888 · refine le_trans ?_ hP.2.1.1; norm_num889 · refine le_trans hP.2.1.2 ?_; norm_num890 have hr5 := ratio_bracket_Icc (cellU 3) (P5 (cellU 3)) (1.2060081563 : ℝ) (1.206041656 : ℝ) (-0.8672370496 : ℝ) (-0.867049695 : ℝ) (1.0981839 : ℝ) (1.0981994 : ℝ) (3.6 : ℝ) (3.61 : ℝ) hL hP5891 (by norm_num) (by norm_num) (by norm_num) (by norm_num) (by norm_num) (by norm_num) (by norm_num)892 have hP7 : (-0.6635839986 : ℝ) ≤ P7 (cellU 3) ∧ P7 (cellU 3) ≤ (-0.6633510393 : ℝ) := by893 constructor894 · refine le_trans ?_ hP.2.2.1; norm_num895 · refine le_trans hP.2.2.2 ?_; norm_num896 have hr7 := ratio_bracket_Icc (cellU 3) (P7 (cellU 3)) (1.2060081563 : ℝ) (1.206041656 : ℝ) (-0.6635839986 : ℝ) (-0.6633510393 : ℝ) (1.0981839 : ℝ) (1.0981994 : ℝ) (3.78 : ℝ) (3.79 : ℝ) hL hP7897 (by norm_num) (by norm_num) (by norm_num) (by norm_num) (by norm_num) (by norm_num) (by norm_num)898 exact ⟨hr3, hr5, hr7⟩899900set_option maxHeartbeats 1000000 in901/-- The cell `n = 2`: the stiffness lies in `[0.806866062, 0.806866188]`, `u` in `[0.34254, 0.34255]`, and the orders `3`, `5`, `7` in the stated brackets. -/902theorem cell2_ratios :903 ((3.64 : ℝ) ≤ ratio (cellU 2) (P3 (cellU 2)) ∧ ratio (cellU 2) (P3 (cellU 2)) ≤ (3.65 : ℝ)) ∧904 ((2.87 : ℝ) ≤ ratio (cellU 2) (P5 (cellU 2)) ∧ ratio (cellU 2) (P5 (cellU 2)) ≤ (2.88 : ℝ)) ∧905 ((3.35 : ℝ) ≤ ratio (cellU 2) (P7 (cellU 2)) ∧ ratio (cellU 2) (P7 (cellU 2)) ≤ (3.37 : ℝ)) := by906 have hθ : (0.806866062 : ℝ) ≤ cellStiffness 2 ∧ cellStiffness 2 ≤ (0.806866188 : ℝ) := by907 have h := cellStiffness_bracket 2908 push_cast at h909 constructor <;> linarith [h.1, h.2]910 have hc := c3terms_bracket (cellStiffness 2) (0.806866062 : ℝ) (0.806866188 : ℝ) (by norm_num) hθ.1 hθ.2911 have hu : (0.34254 : ℝ) ≤ cellU 2 ∧ cellU 2 ≤ (0.34255 : ℝ) := by912 unfold cellU913 constructor914 · refine le_trans ?_ hc.1; norm_num915 · refine le_trans hc.2 ?_; norm_num916 have hua : (0 : ℝ) < 0.34254 := by norm_num917 have hla := Real.log_le_log hua hu.1918 have hlb := Real.log_le_log (lt_of_lt_of_le hua hu.1) hu.2919 have hl1 := log_two_gt_d9920 have hl2 := log_two_lt_d9921 have hA := logb_cell2a922 have hB := logb_cell2b923 have hL : (1.0713376001 : ℝ) ≤ -log (cellU 2) ∧ -log (cellU 2) ≤ (1.0713668806 : ℝ) := by924 constructor <;> linarith [hA.1, hA.2, hB.1, hB.2]925 have hP := P_bracket (cellU 2) (0.34254 : ℝ) (0.34255 : ℝ) (by norm_num) hu.1 hu.2926 have hP3 : (-0.5142794889 : ℝ) ≤ P3 (cellU 2) ∧ P3 (cellU 2) ≤ (-0.5141403092 : ℝ) := by927 constructor928 · refine le_trans ?_ hP.1.1; norm_num929 · refine le_trans hP.1.2 ?_; norm_num930 have hr3 := ratio_bracket_Icc (cellU 2) (P3 (cellU 2)) (1.0713376001 : ℝ) (1.0713668806 : ℝ) (-0.5142794889 : ℝ) (-0.5141403092 : ℝ) (1.0350542 : ℝ) (1.0350687 : ℝ) (3.64 : ℝ) (3.65 : ℝ) hL hP3931 (by norm_num) (by norm_num) (by norm_num) (by norm_num) (by norm_num) (by norm_num) (by norm_num)932 have hP5 : (-1.3110613267 : ℝ) ≤ P5 (cellU 2) ∧ P5 (cellU 2) ≤ (-1.3108086655 : ℝ) := by933 constructor934 · refine le_trans ?_ hP.2.1.1; norm_num935 · refine le_trans hP.2.1.2 ?_; norm_num936 have hr5 := ratio_bracket_Icc (cellU 2) (P5 (cellU 2)) (1.0713376001 : ℝ) (1.0713668806 : ℝ) (-1.3110613267 : ℝ) (-1.3108086655 : ℝ) (1.0350542 : ℝ) (1.0350687 : ℝ) (2.87 : ℝ) (2.88 : ℝ) hL hP5937 (by norm_num) (by norm_num) (by norm_num) (by norm_num) (by norm_num) (by norm_num) (by norm_num)938 have hP7 : (-0.807822877 : ℝ) ≤ P7 (cellU 2) ∧ P7 (cellU 2) ≤ (-0.8074713231 : ℝ) := by939 constructor940 · refine le_trans ?_ hP.2.2.1; norm_num941 · refine le_trans hP.2.2.2 ?_; norm_num942 have hr7 := ratio_bracket_Icc (cellU 2) (P7 (cellU 2)) (1.0713376001 : ℝ) (1.0713668806 : ℝ) (-0.807822877 : ℝ) (-0.8074713231 : ℝ) (1.0350542 : ℝ) (1.0350687 : ℝ) (3.35 : ℝ) (3.37 : ℝ) hL hP7943 (by norm_num) (by norm_num) (by norm_num) (by norm_num) (by norm_num) (by norm_num) (by norm_num)944 exact ⟨hr3, hr5, hr7⟩945946set_option maxHeartbeats 1000000 in947/-- Channel unity, the cell `n = 0`: the stiffness is `1`, the computed terms sum to `u = 23/54`, and the orders `3`, `5`, `7` lie in the stated brackets. -/948theorem cell0_ratios :949 ((2.95 : ℝ) ≤ ratio (cellU 0) (P3 (cellU 0)) ∧ ratio (cellU 0) (P3 (cellU 0)) ≤ (2.96 : ℝ)) ∧950 ((0.44 : ℝ) ≤ ratio (cellU 0) (P5 (cellU 0)) ∧ ratio (cellU 0) (P5 (cellU 0)) ≤ (0.45 : ℝ)) ∧951 ((2.81 : ℝ) ≤ ratio (cellU 0) (P7 (cellU 0)) ∧ ratio (cellU 0) (P7 (cellU 0)) ≤ (2.82 : ℝ)) := by952 have he : cellU 0 = 23 / 54 := by norm_num [cellU, cellStiffness, c3terms]953 have hu : (23 / 54 : ℝ) ≤ cellU 0 ∧ cellU 0 ≤ (23 / 54 : ℝ) := ⟨he.ge, he.le⟩954 have hua : (0 : ℝ) < 23 / 54 := by norm_num955 have hla := Real.log_le_log hua hu.1956 have hlb := Real.log_le_log (lt_of_lt_of_le hua hu.1) hu.2957 have hl1 := log_two_gt_d9958 have hl2 := log_two_lt_d9959 have hA := logb_cell0a960 have hB := logb_cell0a961 have hL : (0.8534897856 : ℝ) ≤ -log (cellU 0) ∧ -log (cellU 0) ≤ (0.8534898669 : ℝ) := by962 constructor <;> linarith [hA.1, hA.2, hB.1, hB.2]963 have hP := P_bracket (cellU 0) (23 / 54 : ℝ) (23 / 54 : ℝ) (by norm_num) hu.1 hu.2964 have hP3 : (-0.6881858711 : ℝ) ≤ P3 (cellU 0) ∧ P3 (cellU 0) ≤ (-0.688185871 : ℝ) := by965 constructor966 · refine le_trans ?_ hP.1.1; norm_num967 · refine le_trans hP.1.2 ?_; norm_num968 have hr3 := ratio_bracket_Icc (cellU 0) (P3 (cellU 0)) (0.8534897856 : ℝ) (0.8534898669 : ℝ) (-0.6881858711 : ℝ) (-0.688185871 : ℝ) (0.923845 : ℝ) (0.9238453 : ℝ) (2.95 : ℝ) (2.96 : ℝ) hL hP3969 (by norm_num) (by norm_num) (by norm_num) (by norm_num) (by norm_num) (by norm_num) (by norm_num)970 have hP5 : (-3.0001582079 : ℝ) ≤ P5 (cellU 0) ∧ P5 (cellU 0) ≤ (-3.0001582078 : ℝ) := by971 constructor972 · refine le_trans ?_ hP.2.1.1; norm_num973 · refine le_trans hP.2.1.2 ?_; norm_num974 have hr5 := ratio_bracket_Icc (cellU 0) (P5 (cellU 0)) (0.8534897856 : ℝ) (0.8534898669 : ℝ) (-3.0001582079 : ℝ) (-3.0001582078 : ℝ) (0.923845 : ℝ) (0.9238453 : ℝ) (0.44 : ℝ) (0.45 : ℝ) hL hP5975 (by norm_num) (by norm_num) (by norm_num) (by norm_num) (by norm_num) (by norm_num) (by norm_num)976 have hP7 : (-0.8092802977 : ℝ) ≤ P7 (cellU 0) ∧ P7 (cellU 0) ≤ (-0.8092802976 : ℝ) := by977 constructor978 · refine le_trans ?_ hP.2.2.1; norm_num979 · refine le_trans hP.2.2.2 ?_; norm_num980 have hr7 := ratio_bracket_Icc (cellU 0) (P7 (cellU 0)) (0.8534897856 : ℝ) (0.8534898669 : ℝ) (-0.8092802977 : ℝ) (-0.8092802976 : ℝ) (0.923845 : ℝ) (0.9238453 : ℝ) (2.81 : ℝ) (2.82 : ℝ) hL hP7981 (by norm_num) (by norm_num) (by norm_num) (by norm_num) (by norm_num) (by norm_num) (by norm_num)982 exact ⟨hr3, hr5, hr7⟩983984/-- 46:C11 [chart] — **the plaquette channel at the chart's cells.** With the stiffness `ϑ_n = 1 − n · 11 ln 2/(8π²)` of the cell985`n` (46:B6), `u` the sum of the computed terms of the frame's `c₃` through `ϑ⁷` at that stiffness (46:C7), the imported series986to the orders `3`, `5`, `7` (46:A11) and the tension at leading order, `m/√σ = (−4 ln u + P)/√(−ln u)` lies, order by order, in987`(6.93, 6.94)`, `(6.93, 6.94)`, `(6.93, 6.94)` at `n = 9`,988`(6.16, 6.17)`, `(6.16, 6.17)`, `(6.16, 6.17)` at `n = 8`,989`(5.59, 5.6)`, `(5.58, 5.59)`, `(5.58, 5.59)` at `n = 7`,990`(5.11, 5.12)`, `(5.09, 5.1)`, `(5.1, 5.11)` at `n = 6`,991`(4.32, 4.33)`, `(4.16, 4.17)`, `(4.22, 4.23)` at `n = 4`,992`(3.97, 3.98)`, `(3.6, 3.61)`, `(3.78, 3.79)` at `n = 3`,993`(3.64, 3.65)`, `(2.87, 2.88)`, `(3.35, 3.37)` at `n = 2`,994and at channel unity, where `u = 23/54`, in `(2.95, 2.96)`, `(0.44, 0.45)`, `(2.81, 2.82)`.995At the cells `n = 9, 8, 7, 6` the orders `3` and `5` lie within `1 %` of the seventh; at `n = 4` the three orders lie above `3.7`;996at `n = 3` the fifth order alone lies in the lattice bracket `(3.4, 3.7)`; at `n = 2` the third order alone does. -/997theorem plaquette_cells_values :998 (cellU 0 = 23 / 54) ∧999 ((6.93 : ℝ) ≤ ratio (cellU 9) (P3 (cellU 9)) ∧ ratio (cellU 9) (P3 (cellU 9)) ≤ (6.94 : ℝ) ∧ (6.93 : ℝ) ≤ ratio (cellU 9) (P5 (cellU 9)) ∧ ratio (cellU 9) (P5 (cellU 9)) ≤ (6.94 : ℝ) ∧ (6.93 : ℝ) ≤ ratio (cellU 9) (P7 (cellU 9)) ∧ ratio (cellU 9) (P7 (cellU 9)) ≤ (6.94 : ℝ)) ∧1000 ((6.16 : ℝ) ≤ ratio (cellU 8) (P3 (cellU 8)) ∧ ratio (cellU 8) (P3 (cellU 8)) ≤ (6.17 : ℝ) ∧ (6.16 : ℝ) ≤ ratio (cellU 8) (P5 (cellU 8)) ∧ ratio (cellU 8) (P5 (cellU 8)) ≤ (6.17 : ℝ) ∧ (6.16 : ℝ) ≤ ratio (cellU 8) (P7 (cellU 8)) ∧ ratio (cellU 8) (P7 (cellU 8)) ≤ (6.17 : ℝ)) ∧1001 ((5.59 : ℝ) ≤ ratio (cellU 7) (P3 (cellU 7)) ∧ ratio (cellU 7) (P3 (cellU 7)) ≤ (5.6 : ℝ) ∧ (5.58 : ℝ) ≤ ratio (cellU 7) (P5 (cellU 7)) ∧ ratio (cellU 7) (P5 (cellU 7)) ≤ (5.59 : ℝ) ∧ (5.58 : ℝ) ≤ ratio (cellU 7) (P7 (cellU 7)) ∧ ratio (cellU 7) (P7 (cellU 7)) ≤ (5.59 : ℝ)) ∧1002 ((5.11 : ℝ) ≤ ratio (cellU 6) (P3 (cellU 6)) ∧ ratio (cellU 6) (P3 (cellU 6)) ≤ (5.12 : ℝ) ∧ (5.09 : ℝ) ≤ ratio (cellU 6) (P5 (cellU 6)) ∧ ratio (cellU 6) (P5 (cellU 6)) ≤ (5.1 : ℝ) ∧ (5.1 : ℝ) ≤ ratio (cellU 6) (P7 (cellU 6)) ∧ ratio (cellU 6) (P7 (cellU 6)) ≤ (5.11 : ℝ)) ∧1003 ((4.32 : ℝ) ≤ ratio (cellU 4) (P3 (cellU 4)) ∧ ratio (cellU 4) (P3 (cellU 4)) ≤ (4.33 : ℝ) ∧ (4.16 : ℝ) ≤ ratio (cellU 4) (P5 (cellU 4)) ∧ ratio (cellU 4) (P5 (cellU 4)) ≤ (4.17 : ℝ) ∧ (4.22 : ℝ) ≤ ratio (cellU 4) (P7 (cellU 4)) ∧ ratio (cellU 4) (P7 (cellU 4)) ≤ (4.23 : ℝ)) ∧1004 ((3.97 : ℝ) ≤ ratio (cellU 3) (P3 (cellU 3)) ∧ ratio (cellU 3) (P3 (cellU 3)) ≤ (3.98 : ℝ) ∧ (3.6 : ℝ) ≤ ratio (cellU 3) (P5 (cellU 3)) ∧ ratio (cellU 3) (P5 (cellU 3)) ≤ (3.61 : ℝ) ∧ (3.78 : ℝ) ≤ ratio (cellU 3) (P7 (cellU 3)) ∧ ratio (cellU 3) (P7 (cellU 3)) ≤ (3.79 : ℝ)) ∧1005 ((3.64 : ℝ) ≤ ratio (cellU 2) (P3 (cellU 2)) ∧ ratio (cellU 2) (P3 (cellU 2)) ≤ (3.65 : ℝ) ∧ (2.87 : ℝ) ≤ ratio (cellU 2) (P5 (cellU 2)) ∧ ratio (cellU 2) (P5 (cellU 2)) ≤ (2.88 : ℝ) ∧ (3.35 : ℝ) ≤ ratio (cellU 2) (P7 (cellU 2)) ∧ ratio (cellU 2) (P7 (cellU 2)) ≤ (3.37 : ℝ)) ∧1006 ((2.95 : ℝ) ≤ ratio (cellU 0) (P3 (cellU 0)) ∧ ratio (cellU 0) (P3 (cellU 0)) ≤ (2.96 : ℝ) ∧ (0.44 : ℝ) ≤ ratio (cellU 0) (P5 (cellU 0)) ∧ ratio (cellU 0) (P5 (cellU 0)) ≤ (0.45 : ℝ) ∧ (2.81 : ℝ) ≤ ratio (cellU 0) (P7 (cellU 0)) ∧ ratio (cellU 0) (P7 (cellU 0)) ≤ (2.82 : ℝ)) ∧1007 (|ratio (cellU 9) (P3 (cellU 9)) - ratio (cellU 9) (P7 (cellU 9))| < 0.01 * ratio (cellU 9) (P7 (cellU 9)) ∧ |ratio (cellU 9) (P5 (cellU 9)) - ratio (cellU 9) (P7 (cellU 9))| < 0.01 * ratio (cellU 9) (P7 (cellU 9))) ∧1008 (|ratio (cellU 8) (P3 (cellU 8)) - ratio (cellU 8) (P7 (cellU 8))| < 0.01 * ratio (cellU 8) (P7 (cellU 8)) ∧ |ratio (cellU 8) (P5 (cellU 8)) - ratio (cellU 8) (P7 (cellU 8))| < 0.01 * ratio (cellU 8) (P7 (cellU 8))) ∧1009 (|ratio (cellU 7) (P3 (cellU 7)) - ratio (cellU 7) (P7 (cellU 7))| < 0.01 * ratio (cellU 7) (P7 (cellU 7)) ∧ |ratio (cellU 7) (P5 (cellU 7)) - ratio (cellU 7) (P7 (cellU 7))| < 0.01 * ratio (cellU 7) (P7 (cellU 7))) ∧1010 (|ratio (cellU 6) (P3 (cellU 6)) - ratio (cellU 6) (P7 (cellU 6))| < 0.01 * ratio (cellU 6) (P7 (cellU 6)) ∧ |ratio (cellU 6) (P5 (cellU 6)) - ratio (cellU 6) (P7 (cellU 6))| < 0.01 * ratio (cellU 6) (P7 (cellU 6))) ∧1011 ((3.7 : ℝ) < ratio (cellU 4) (P3 (cellU 4)) ∧ (3.7 : ℝ) < ratio (cellU 4) (P5 (cellU 4)) ∧ (3.7 : ℝ) < ratio (cellU 4) (P7 (cellU 4))) ∧1012 ((3.4 : ℝ) < ratio (cellU 3) (P5 (cellU 3)) ∧ ratio (cellU 3) (P5 (cellU 3)) < (3.7 : ℝ) ∧ (3.7 : ℝ) < ratio (cellU 3) (P3 (cellU 3)) ∧ (3.7 : ℝ) < ratio (cellU 3) (P7 (cellU 3))) ∧1013 ((3.4 : ℝ) < ratio (cellU 2) (P3 (cellU 2)) ∧ ratio (cellU 2) (P3 (cellU 2)) < (3.7 : ℝ) ∧ ratio (cellU 2) (P5 (cellU 2)) < (3.4 : ℝ) ∧ ratio (cellU 2) (P7 (cellU 2)) < (3.4 : ℝ)) := by1014 have h9 := cell9_ratios1015 have h8 := cell8_ratios1016 have h7 := cell7_ratios1017 have h6 := cell6_ratios1018 have h4 := cell4_ratios1019 have h3 := cell3_ratios1020 have h2 := cell2_ratios1021 have h0 := cell0_ratios1022 have he : cellU 0 = 23 / 54 := by norm_num [cellU, cellStiffness, c3terms]1023 refine ⟨he, ⟨h9.1.1, h9.1.2, h9.2.1.1, h9.2.1.2, h9.2.2.1, h9.2.2.2⟩, ⟨h8.1.1, h8.1.2, h8.2.1.1, h8.2.1.2, h8.2.2.1, h8.2.2.2⟩, ⟨h7.1.1, h7.1.2, h7.2.1.1, h7.2.1.2, h7.2.2.1, h7.2.2.2⟩, ⟨h6.1.1, h6.1.2, h6.2.1.1, h6.2.1.2, h6.2.2.1, h6.2.2.2⟩, ⟨h4.1.1, h4.1.2, h4.2.1.1, h4.2.1.2, h4.2.2.1, h4.2.2.2⟩, ⟨h3.1.1, h3.1.2, h3.2.1.1, h3.2.1.2, h3.2.2.1, h3.2.2.2⟩, ⟨h2.1.1, h2.1.2, h2.2.1.1, h2.2.1.2, h2.2.2.1, h2.2.2.2⟩, ⟨h0.1.1, h0.1.2, h0.2.1.1, h0.2.1.2, h0.2.2.1, h0.2.2.2⟩, ?_, ?_, ?_, ?_, ?_, ?_, ?_⟩1024 · constructor <;> rw [abs_lt] <;> constructor <;> linarith [h9.1.1, h9.1.2, h9.2.1.1, h9.2.1.2, h9.2.2.1, h9.2.2.2]1025 · constructor <;> rw [abs_lt] <;> constructor <;> linarith [h8.1.1, h8.1.2, h8.2.1.1, h8.2.1.2, h8.2.2.1, h8.2.2.2]1026 · constructor <;> rw [abs_lt] <;> constructor <;> linarith [h7.1.1, h7.1.2, h7.2.1.1, h7.2.1.2, h7.2.2.1, h7.2.2.2]1027 · constructor <;> rw [abs_lt] <;> constructor <;> linarith [h6.1.1, h6.1.2, h6.2.1.1, h6.2.1.2, h6.2.2.1, h6.2.2.2]1028 · exact ⟨by linarith [h4.1.1], by linarith [h4.2.1.1], by linarith [h4.2.2.1]⟩1029 · exact ⟨by linarith [h3.2.1.1], by linarith [h3.2.1.2], by linarith [h3.1.1], by linarith [h3.2.2.1]⟩1030 · exact ⟨by linarith [h2.1.1], by linarith [h2.1.2], by linarith [h2.2.1.2], by linarith [h2.2.2.2]⟩10311032/-! ## 46:C21 — the gap of the transfer tally at the classical `π` -/10331034/-- 46:C21 [chart] — **the gap at the classical `π`.** The gap of the transfer tally is `1/(2π + 2)` in the shell's `2π = p − 1`;1035read at the classical `π` the expression lies in `(0.12072, 0.12073)`, the row's `0.1207`. -/1036theorem gap_at_classical_pi : (0.12072 : ℝ) < 1 / (2 * π + 2) ∧ 1 / (2 * π + 2) < (0.12073 : ℝ) := by1037 have hp1 := pi_gt_d41038 have hp2 := pi_lt_d41039 have hpos : (0 : ℝ) < 2 * π + 2 := by positivity1040 constructor1041 · rw [lt_div_iff₀ hpos]; linarith1042 · rw [div_lt_iff₀ hpos]; linarith10431044/-! ## 46:C12 — the operator family's values -/10451046/-- 46:C12 [chart] — **the family against the lattice.** With the chart's eigenvalue `E₀ = 2.232` of `|p| + r` (the reading of104735:C17) and the dilation `E₀(a|p| + ϰr) = √(aϰ) E₀`, the six candidates `a ∈ {1, 2}`, `ϰ ∈ {1, 2, 9/4}` read `2.232`,1048`(3.156, 3.157)`, `3.348`, `(3.156, 3.157)`, `4.464`, `(4.734, 4.735)` (the row's `2.232`, `3.157`, `3.348`, `3.157`, `4.464`,1049`4.735`); none lies inside any determination's error, `3.70(6)`, `3.63(10)`, `3.405(21)`, and the nearest, `3.348`, lies1050`1.7 %` below the direct value. -/1051theorem wrap_family_values (E₀ : ℝ) (hE : E₀ = 2.232) :1052 (3.156 : ℝ) < √2 * E₀ ∧ √2 * E₀ < 3.157 ∧ √(9 / 4) * E₀ = 3.348 ∧ √4 * E₀ = 4.464 ∧1053 (4.734 : ℝ) < √(9 / 2) * E₀ ∧ √(9 / 2) * E₀ < 4.735 ∧1054 E₀ < 3.384 ∧ √2 * E₀ < 3.384 ∧ √(9 / 4) * E₀ < 3.384 ∧ 3.76 < √4 * E₀ ∧ 3.76 < √(9 / 2) * E₀ ∧1055 (0.016 : ℝ) < (3.405 - √(9 / 4) * E₀) / 3.405 ∧ (3.405 - √(9 / 4) * E₀) / 3.405 < 0.018 := by1056 subst hE1057 have h2a : (1.4142 : ℝ) < √2 := by rw [lt_sqrt (by norm_num)]; norm_num1058 have h2b : √2 < (1.4143 : ℝ) := by rw [sqrt_lt' (by norm_num)]; norm_num1059 have h94 : √(9 / 4 : ℝ) = 3 / 2 := by1060 rw [show (9 / 4 : ℝ) = (3 / 2) ^ 2 by norm_num, sqrt_sq (by norm_num)]1061 have h4 : √(4 : ℝ) = 2 := by1062 rw [show (4 : ℝ) = 2 ^ 2 by norm_num, sqrt_sq (by norm_num)]1063 have h92a : (2.1213 : ℝ) < √(9 / 2) := by rw [lt_sqrt (by norm_num)]; norm_num1064 have h92b : √(9 / 2 : ℝ) < (2.1214 : ℝ) := by rw [sqrt_lt' (by norm_num)]; norm_num1065 rw [h94, h4]1066 refine ⟨by nlinarith, by nlinarith, by norm_num, by norm_num, by nlinarith, by nlinarith, by norm_num, by nlinarith,1067 by norm_num, by norm_num, by nlinarith, ?_, ?_⟩1068 · rw [lt_div_iff₀ (by norm_num)]; norm_num1069 · rw [div_lt_iff₀ (by norm_num)]; norm_num10701071end FRC.YangMillsML1072