The numeric consequences of the budget (`segReg_num`)
ProvedJ6Seg.segReg_numThe numeric consequences of the budget.
The following holds (Lean statement, in the scope of module Solutions.J6SegJPre1):
theorem J6Seg.segReg_num (h : SegReg P R s t lam w α) :
200 * (3 * (lam : ℝ) + 1) ≤ 2 ^ P ∧
100 * (((lam : ℝ) + 1) * (3 * lam + 3) + 1) ≤ 2 ^ P ∧
(lam : ℝ) * (2 * w + 1) * (15 * ddR (α : ℝ) ((t : ℝ) / s) (lam - 1) *
(((lam : ℝ) + 1) * (3 * lam + 3) + 1) / 2 ^ P) ≤ 1 / 100 ∧
8 * ((s : ℝ) + 1) ^ 2 ≤ 2 ^ P ∧ 1 ≤ P
Context. J kernel precondition (JPre), part 1: the regime and the capacitance of a line
SegReg P R s t λ w α bundles the hypotheses of segInvFullS_err (with Bu = 1/2, as used by
B0seg): 0 < s ≤ t, 2 ≤ α, 3 ≤ xθ, 1 ≤ λ, w ≤ s, D_{λ-1} ≤ 2^R,
1000 · fullG λ w s t α (1/2) ≤ 2^P.
segReg_cap: in this regime the capacitance capI P (TT P R s t α) (BB s t λ w) on the line
LJ s t λ w has row sums |C/2^P - I| ≤ η ≤ 1/4, vanishes off the pattern
bandS (λ+w) (s-λ-w), and (|LJ|+1)²/2^P ≤ 1/8 (so also η + |LJ|²/2^P ≤ 1/2).
Formalization Note. Part of the Lean formalization of the round-six κ-improvement (integer-multiplication-kappa campaign, target IntMul.Kappa.jain_round6_framework). The statement is copied verbatim from the Lean development; the platform node carries the same declaration name. Definitions it mentions live in the IntMul_Kappa_R6_Defs* bundles (on top of the published κ bundles IntMul_Kappa_K_Defs*).
-- Round-six κ development (integer-multiplication-kappa), generated by skeleton subtraction.
import Definitions.Def_IntMul_Kappa_R6_Defs67
set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000
open J6Seg
open Finset Real
open IntMul.HvdH IntMul.HvdH.JPf J6QLU
variable {P R s t lam w α : ℕ}
theorem J6Seg.segReg_num (h : SegReg P R s t lam w α) :
200 * (3 * (lam : ℝ) + 1) ≤ 2 ^ P ∧
100 * (((lam : ℝ) + 1) * (3 * lam + 3) + 1) ≤ 2 ^ P ∧
(lam : ℝ) * (2 * w + 1) * (15 * ddR (α : ℝ) ((t : ℝ) / s) (lam - 1) *
(((lam : ℝ) + 1) * (3 * lam + 3) + 1) / 2 ^ P) ≤ 1 / 100 ∧
8 * ((s : ℝ) + 1) ^ 2 ≤ 2 ^ P ∧ 1 ≤ P := by sorry