← Mathematical handbook

Identification of the explicit certificates with the manuscript's potentials.

theorem Papers.Rockel2026ExactBlest.hasDerivAt_cubic (A B C D x : ℝ) : HasDerivAt (fun (y : ℝ) => A * y ^ 3 + B * y ^ 2 + C * y + D) (3 * A * x ^ 2 + 2 * B * x + C) x

theorem Papers.Rockel2026ExactBlest.hasDerivAt_antiPhi (k x : ℝ) : HasDerivAt (antiPhi k) ((1 - x) * (2 * x - k * (1 - x))) x

theorem Papers.Rockel2026ExactBlest.hasDerivAt_linearPsi (k m b z : ℝ) : HasDerivAt (linearPsi k m b) ((m * z + b) * (m * z + b - 2 * k * z)) z

theorem Papers.Rockel2026ExactBlest.hasDerivAt_graphPhi (w x : ℝ) : HasDerivAt (graphPhi w) ((x - w) * (2 * x - kA w * (x - w))) x

theorem Papers.Rockel2026ExactBlest.hasDerivAt_splitPhi (a x : ℝ) (ha : a ≠ 0) : HasDerivAt (splitPhi a) ((x - a) / (2 * a) * (2 * x - kB a * ((x - a) / (2 * a)))) x

theorem Papers.Rockel2026ExactBlest.continuous_phiA (w : ℝ) : Continuous (phiA w)

theorem Papers.Rockel2026ExactBlest.continuous_psiA (w : ℝ) : Continuous (psiA w)

theorem Papers.Rockel2026ExactBlest.potentialsA_normalized (w : ℝ) (hw : w ≤ 1) : phiA w w = 0 ∧ psiA w 0 = 0

theorem Papers.Rockel2026ExactBlest.hasDerivAt_phiA (w x : ℝ) (hx : x ≠ w) : HasDerivAt (phiA w) (if x ≤ w then (1 - x) * (2 * x - kA w * (1 - x)) else (x - w) * (2 * x - kA w * (x - w))) x

theorem Papers.Rockel2026ExactBlest.hasDerivAt_psiA (w z : ℝ) (hz : z ≠ 1 - w) : HasDerivAt (psiA w) (if z ≤ 1 - w then (z + w) * (z + w - 2 * kA w * z) else (1 - z) * (1 - z - 2 * kA w * z)) z

theorem Papers.Rockel2026ExactBlest.cutB_bounds (a : ℝ) (ha : 1 / 2 < a) (ha1 : a < 1) : 0 < cutB a ∧ cutB a < 1 - a

theorem Papers.Rockel2026ExactBlest.continuous_phiB (a : ℝ) : Continuous (phiB a)

theorem Papers.Rockel2026ExactBlest.continuous_psiB (a : ℝ) (ha : 1 / 2 < a) (ha1 : a < 1) : Continuous (psiB a)

theorem Papers.Rockel2026ExactBlest.potentialsB_normalized (a : ℝ) (ha : 1 / 2 < a) (ha1 : a < 1) : phiB a a = 0 ∧ psiB a 0 = 0

theorem Papers.Rockel2026ExactBlest.hasDerivAt_phiB (a x : ℝ) (ha : a ≠ 0) (hx : x ≠ a) : HasDerivAt (phiB a) (if x ≤ a then (1 - x) * (2 * x - kB a * (1 - x)) else (x - a) / (2 * a) * (2 * x - kB a * ((x - a) / (2 * a)))) x

theorem Papers.Rockel2026ExactBlest.hasDerivAt_psiB1 (a z : ℝ) : HasDerivAt (psiB1 a) (a * (1 - 2 * z) / (2 * a - 1) * (a * (1 - 2 * z) / (2 * a - 1) - 2 * kB a * z)) z

theorem Papers.Rockel2026ExactBlest.hasDerivAt_psiB2 (a z : ℝ) : HasDerivAt (psiB2 a) ((1 - z) * (1 - z - 2 * kB a * z)) z

theorem Papers.Rockel2026ExactBlest.hasDerivAt_psiB (a z : ℝ) (hzc : z ≠ cutB a) (hza : z ≠ 1 - a) : HasDerivAt (psiB a) (randomRankReal a z * (randomRankReal a z - 2 * kB a * z)) z

theorem Papers.Rockel2026ExactBlest.random_branches_root_sum (a x : ℝ) (ha : a ≠ 0) : (x - a) / (2 * a) + (a + x - 2 * a * x) / (2 * a) = x * (1 - a) / a

theorem Papers.Rockel2026ExactBlest.random_branches_same_derivative (a x : ℝ) (ha : a ≠ 0) (ha1 : a ≠ 1) : (x - a) / (2 * a) * (2 * x - kB a * ((x - a) / (2 * a))) = (a + x - 2 * a * x) / (2 * a) * (2 * x - kB a * ((a + x - 2 * a * x) / (2 * a)))

theorem Papers.Rockel2026ExactBlest.hasDerivAt_etaB (a : ℝ) (ha : a ≠ 0) : HasDerivAt etaB (-((1 - a) ^ 2 * (1 + a) * (3 * a ^ 2 + 2 * a + 1)) / (4 * a ^ 3)) a

theorem Papers.Rockel2026ExactBlest.deriv_etaB_neg (a : ℝ) (ha : 1 / 2 ≤ a) (ha1 : a < 1) : deriv etaB a < 0