The seeded-CL adapter, part 7: the parameter corollary

The reduction of Adapter/Reduction.lean concludes with the canonical-line error lidtError m d q k (3m ε), with k free subject to k ≥ 400 m d. Blueprint thm:lidt-cl-soundness asks instead for

δ_CL(ε, q, m, d, 1) = a (dm)^a (ε^b + q^{-b} + 2^{-bmd}),

for universal a ≥ 1 and 0 < b < 1. rem:lidt-cl-adapter lists turning one into the other as a separate quantitative obligation, to be done "honestly against the explicit constants"; this file does it, and is stated separately from the reduction so that a failure here could not silently weaken the reduction.

The choice is b = 1/40000, a = 2·10^11 and k = 400 m³ d + 400 m. Term by term, with ε' = 3 m ε:

• ε'^b = (3m)^b ε^b ≤ 3m · ε^b, since x^b ≤ x for x ≥ 1 and b ≤ 1;
• (d/q)^b = d^b · q^{-b} ≤ d · q^{-b}, likewise;
• exp(-k / (2560000 m²)) ≤ 2^{-bmd}, which is where k is chosen: it needs k ≥ 2560000 · b · m³ d · ln 2 = 64 (ln 2) m³ d ≈ 44.4 m³ d, and 400 m³ d clears it with room. The 400 m summand is there only so that k > 0 and k ≥ 400 m d hold for every m, d ≥ 1.

The prefactor is then 100000 k² m⁴ · 3md ≤ 1.92·10^11 (dm)^11, using k ≤ 800 m³ d, and (dm)^11 ≤ (dm)^a.

d ≥ 1 is needed and not cosmetic: at d = 0 the blueprint's δ_CL is identically zero, so no positive error can be bounded by it.

The constants

noncomputable def MIPRE.LIDT.clB : ℝ

The exponent of δ_CL.

Equations

• MIPRE.LIDT.clB = 1 / 40000

def MIPRE.LIDT.clA : ℝ

The constant of δ_CL.

Equations

• MIPRE.LIDT.clA = 2 * 10 ^ 11

def MIPRE.LIDT.clK (m d : ℕ) : ℕ

The sampling parameter the corollary chooses for the canonical-line theorem.

Equations

• MIPRE.LIDT.clK m d = 400 * m ^ 3 * d + 400 * m

noncomputable def MIPRE.LIDT.deltaCL (q m d : ℕ) (ε : ℝ) : ℝ

δ_CL at ldc = 1 (blueprint thm:lidt-cl-soundness).

Equations

• MIPRE.LIDT.deltaCL q m d ε = MIPRE.LIDT.clA * ↑(d * m) ^ MIPRE.LIDT.clA * (ε ^ MIPRE.LIDT.clB + ↑q ^ (-MIPRE.LIDT.clB) + 2 ^ (-(MIPRE.LIDT.clB * ↑m * ↑d)))

theorem MIPRE.LIDT.clB_eq : clB = 1 / 40000

theorem MIPRE.LIDT.clB_pos : 0 < clB

theorem MIPRE.LIDT.clB_lt_one : clB < 1

theorem MIPRE.LIDT.one_le_clA : 1 ≤ clA

The sampling parameter

theorem MIPRE.LIDT.le_clK (m d : ℕ) (hm : 1 ≤ m) : 400 * m * d ≤ clK m d

clK clears the canonical-line theorem's hypothesis.

theorem MIPRE.LIDT.clK_pos (m d : ℕ) (_hm : 1 ≤ m) : 0 < clK m d

theorem MIPRE.LIDT.clK_le (m d : ℕ) (_hm : 1 ≤ m) (hd : 1 ≤ d) : clK m d ≤ 800 * m ^ 3 * d

clK is at most 800 m³ d, which is what bounds the prefactor.

The three terms

theorem MIPRE.LIDT.exp_le_two_rpow (m d : ℕ) (hm : 1 ≤ m) : Real.exp (-↑(clK m d) / (2560000 * ↑m ^ 2)) ≤ 2 ^ (-(clB * ↑m * ↑d))

The exponential term. This is where clK is chosen.

theorem MIPRE.LIDT.rpow_mul_le (m : ℕ) (hm : 1 ≤ m) (ε : ℝ) (hε : 0 ≤ ε) : (3 * ↑m * ε) ^ clB ≤ 3 * ↑m * ε ^ clB

The ε term: the adapter's factor 3m comes out of the exponent.

theorem MIPRE.LIDT.rpow_div_le (d q : ℕ) (hd : 1 ≤ d) : (↑d / ↑q) ^ clB ≤ ↑d * ↑q ^ (-clB)

The d/q term.

The prefactor

theorem MIPRE.LIDT.prefactor_le (m d : ℕ) (hm : 1 ≤ m) (hd : 1 ≤ d) : 100000 * ↑(clK m d) ^ 2 * ↑m ^ 4 * (3 * ↑m * ↑d) ≤ clA * ↑(d * m) ^ clA

The prefactor. 100000 k² m⁴ · 3md ≤ 1.92·10^11 (dm)^11 ≤ a (dm)^a.

The corollary

theorem MIPRE.LIDT.lidtError_le_deltaCL (m d q : ℕ) (hm : 1 ≤ m) (hd : 1 ≤ d) (ε : ℝ) (hε : 0 ≤ ε) : lidtError m d q (clK m d) (3 * ↑m * ε) ≤ deltaCL q m d ε

The parameter corollary. At k = clK m d the canonical-line error on the adapter's inflated failure 3 m ε is below the blueprint's δ_CL at ldc = 1, with the explicit constants a = 2·10^11 and b = 1/40000.