Round-six κ development, definitions part 1

-- Round-six κ development (integer-multiplication-kappa), generated by skeleton subtraction.

import Mathlib
import Definitions.Def_IntMul_KappaFramework
import Definitions.Def_IntMul_MultitapeModel

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

section
-- Source module: Solutions.J6QLUBasic
/-!
# q-Pochhammer symbols and Gaussian binomials (algebraic core of the segmented-inverse q-LU)

Over an arbitrary field `K`:
* `qpoch q n = (q;q)_n = ∏_{i<n} (1 - q^(i+1))`,
* `qbin q n k` = Gaussian binomial `[n k]_q`, defined by the q-Pascal recurrence
  `[n+1, k+1] = [n, k] + q^(k+1) [n, k+1]`,
* `qbin_mul_qpoch` : `[n k] (q;q)_k (q;q)_{n-k} = (q;q)_n`,
* `qbin_rothe` (q-binomial theorem / Rothe):
  `∑_{j ≤ h} (-1)^j q^(j choose 2) [h j] y^j = ∏_{i<h} (1 - y q^i)`,
* `qbin_alt_sum` : `∑_{j ≤ h} (-1)^j q^(j choose 2) [h j] = δ_{h0}`,
* `qpascal_identity` (q-Newton type identity behind the LU factor):
  `∑_{k ≤ u} [u k] (q^(v-k+1);q)_k q^((u-k)(v-k)) = 1`.
-/

open Finset

namespace J6QLU

variable {K : Type*} [Field K]

/-- `(q;q)_n`. -/
def qpoch (q : K) (n : ℕ) : K := ∏ i ∈ range n, (1 - q ^ (i + 1))

/-- Gaussian binomial coefficient `[n k]_q` via q-Pascal. -/
def qbin (q : K) : ℕ → ℕ → K
  | _, 0 => 1
  | 0, _ + 1 => 0
  | n + 1, k + 1 => qbin q n k + q ^ (k + 1) * qbin q n (k + 1)

/-- Falling q-product `∏_{i<k} (1 - q^(v-i)) = (q;q)_v / (q;q)_{v-k}` (zero when `k > v`). -/
def qfall (q : K) (v k : ℕ) : K := ∏ i ∈ range k, (1 - q ^ (v - i))

end J6QLU

end

section
-- Source module: Solutions.J6QLUToep
/-!
# Triangular Toeplitz matrices and the coefficient identities

`lowT c` (lower) and `upT c` (upper) are the triangular Toeplitz matrices of a sequence
`c : ℕ → K`; their products are triangular Toeplitz in the Cauchy convolution `conv c d`.
We define the q-LU coefficients
* `bP x z h = x^(h^2) z^h / (q;q)_h`,   (`b^+`; `b^-` is `bP x z⁻¹`)
* `aP x z h = (-(x z))^h / (q;q)_h`,    (`a^+`; `a^-` is `aP x z⁻¹`)
with `q = x^2`, and prove `conv (bP x z) (aP x z) = δ` (Euler / q-binomial).
-/

open Finset Matrix

namespace J6QLU

variable {K : Type*} [Field K]

/-- Lower triangular Toeplitz matrix `L(c)_{ij} = c_{i-j}` (`j ≤ i`). -/
def lowT {n : ℕ} (c : ℕ → K) : Matrix (Fin n) (Fin n) K :=
  fun i j => if (j : ℕ) ≤ i then c (i - j) else 0

/-- Upper triangular Toeplitz matrix `U(c)_{ij} = c_{j-i}` (`i ≤ j`). -/
def upT {n : ℕ} (c : ℕ → K) : Matrix (Fin n) (Fin n) K :=
  fun i j => if (i : ℕ) ≤ j then c (j - i) else 0

/-- Cauchy convolution. -/
def conv (c d : ℕ → K) (h : ℕ) : K := ∑ m ∈ range (h + 1), c m * d (h - m)

/-- Kronecker delta at 0. -/
def delta0 (h : ℕ) : K := if h = 0 then 1 else 0

/-- `b^+_h = x^(h^2) z^h / (q;q)_h`, `q = x^2`. -/
def bP (x z : K) (h : ℕ) : K := x ^ (h ^ 2) * z ^ h / qpoch (x ^ 2) h

/-- `a^+_h = (-1)^h (x z)^h / (q;q)_h`, `q = x^2`. -/
def aP (x z : K) (h : ℕ) : K := (-(x * z)) ^ h / qpoch (x ^ 2) h

end J6QLU

end

section
-- Source module: Solutions.J6QLUMain
/-!
# Exact q-LU factorization and explicit inverse of the Gaussian Toeplitz matrix

For a field `K`, `x z : K` with `z ≠ 0`, `q = x^2`, and `(q;q)_i ≠ 0` for `i < n`:

* `T_{uv} = x^((v-u)^2) z^(v-u)`   (`gaussToep x z n`),
* `Γ = diag((q;q)_0, …, (q;q)_{n-1})`,
* `T = Γ L(b⁻) Γ⁻¹ U(b⁺) Γ`, `b^±_h = x^(h^2) z^(±h) / (q;q)_h`         (`qLU`),
* `T⁻¹ = Γ⁻¹ U(a⁺) Γ L(a⁻) Γ⁻¹`, `a^±_h = (-1)^h (x z^(±1))^h / (q;q)_h`  (`qLU_inv`).

With `x = e^{-πα²σ}`, `z = e^{-2πα²b}` this is the report's
`T^{(b)}_{uv} = e^{-πα²(σh²+2bh)}`, `q = e^{-2πα²σ}` (see `J6QLUReal`).
-/

open Finset Matrix

namespace J6QLU

variable {K : Type*} [Field K]

/-- Gaussian-type Toeplitz matrix `T_{uv} = x^((v-u)^2) · z^(v-u)`. -/
def gaussToep (x z : K) (n : ℕ) : Matrix (Fin n) (Fin n) K :=
  fun u v => x ^ (((v : ℤ) - (u : ℤ)).natAbs ^ 2) * z ^ ((v : ℤ) - (u : ℤ))

/-- `Γ = diag((q;q)_i)`. -/
def Gam (q : K) (n : ℕ) : Matrix (Fin n) (Fin n) K := diagonal fun i => qpoch q i

/-- `Γ⁻¹ = diag((q;q)_i⁻¹)`. -/
def GamInv (q : K) (n : ℕ) : Matrix (Fin n) (Fin n) K := diagonal fun i => (qpoch q i)⁻¹

end J6QLU

end

section
-- Source module: Solutions.J6QLUReal
/-!
# The segmented-inverse q-LU in the report's real parametrization

`T^{(b)}_{uv} = e^{-πα²(σh²+2bh)}`, `h = v - u`, `q = e^{-2πα²σ}`, `Γ = diag((q;q)_i)`:
* `T = Γ L(b⁻) Γ⁻¹ U(b⁺) Γ`,  `b^±_h = e^{-πα²(σh² ± 2bh)}/(q;q)_h`   (`realToep_qLU`)
* `T⁻¹ = Γ⁻¹ U(a⁺) Γ L(a⁻) Γ⁻¹`, `a^±_h = (-1)^h e^{-πα²(σ±2b)h}/(q;q)_h` (`realToep_inv`)
for every block size `n`, whenever `α²σ > 0`.
-/

open Finset Matrix Real

namespace J6QLU

/-- The Gaussian Toeplitz block `T^{(b)}_{uv} = exp(-πα²(σ(v-u)² + 2b(v-u)))`. -/
noncomputable def realToep (α σ b : ℝ) (n : ℕ) : Matrix (Fin n) (Fin n) ℝ :=
  fun u v => exp (-(π * α ^ 2 * (σ * ((v : ℝ) - u) ^ 2 + 2 * b * ((v : ℝ) - u))))

/-- `q = e^{-2πα²σ}`. -/
noncomputable def qR (α σ : ℝ) : ℝ := exp (-(2 * π * α ^ 2 * σ))

noncomputable def bplus (α σ b : ℝ) (h : ℕ) : ℝ :=
  exp (-(π * α ^ 2 * (σ * (h : ℝ) ^ 2 + 2 * b * h))) / qpoch (qR α σ) h
noncomputable def bminus (α σ b : ℝ) (h : ℕ) : ℝ :=
  exp (-(π * α ^ 2 * (σ * (h : ℝ) ^ 2 - 2 * b * h))) / qpoch (qR α σ) h
noncomputable def aplus (α σ b : ℝ) (h : ℕ) : ℝ :=
  (-1) ^ h * exp (-(π * α ^ 2 * (σ + 2 * b) * h)) / qpoch (qR α σ) h
noncomputable def aminus (α σ b : ℝ) (h : ℕ) : ℝ :=
  (-1) ^ h * exp (-(π * α ^ 2 * (σ - 2 * b) * h)) / qpoch (qR α σ) h

section
variable (α σ b : ℝ)

noncomputable abbrev xR : ℝ := exp (-(π * α ^ 2 * σ))
noncomputable abbrev zR : ℝ := exp (-(2 * π * α ^ 2 * b))

end

end J6QLU

end

section
-- Source module: Solutions.J6SieveBonf
/-!
# J6Sieve, part 1: Bonferroni (Brun pure sieve) inequalities

Truncated inclusion–exclusion over subsets of size `≤ m`.
-/

namespace J6Sieve
open Finset

/-- Truncated alternating sum over subsets of `Q` of size at most `m`. -/
def bonf (Q : Finset ℕ) (m : ℕ) : ℤ :=
  ∑ t ∈ Q.powerset.filter (fun t => t.card ≤ m), (-1 : ℤ) ^ t.card

/-- Primes up to `z`. -/
def P (z : ℕ) : Finset ℕ := (range (z + 1)).filter Nat.Prime

/-- `n` has no prime factor `≤ z`. -/
def rough (z n : ℕ) : Prop := ∀ p ∈ P z, ¬ p ∣ n

instance (z n : ℕ) : Decidable (rough z n) := by unfold rough; infer_instance

/-- Index set of the truncated sieve. -/
def T (z m : ℕ) : Finset (Finset ℕ) := (P z).powerset.filter (fun t => t.card ≤ m)

/-- The prime factors `≤ z` of `n`. -/
def Pn (z n : ℕ) : Finset ℕ := (P z).filter (· ∣ n)

end J6Sieve

end

section
-- Source module: Solutions.J6SieveEst
/-!
# J6Sieve, part 2: real-valued sieve bounds

* counting multiples in an interval,
* the sieve inequalities with main term `W z m`,
* Rankin's trick `|W z m - V z| ≤ 2^{-(m+1)} ∏ (1 + 2/p)`,
* `V z ≥ 1/z`, `∏ (1+2/p) ≤ (z+1)(z+2)/2`, `#T z m ≤ (m+1) z^m`.
-/

namespace J6Sieve
open Finset

/-- Truncated main term. -/
noncomputable def W (z m : ℕ) : ℝ :=
  ∑ t ∈ T z m, (-1 : ℝ) ^ t.card * ∏ p ∈ t, ((p : ℝ))⁻¹

/-- The sieve density `∏_{p ≤ z} (1 - 1/p)`. -/
noncomputable def V (z : ℕ) : ℝ := ∏ p ∈ P z, (1 - ((p : ℝ))⁻¹)

end J6Sieve

end

section
-- Source module: Solutions.J6SieveStep
/-!
# J6Sieve, part 3: one greedy step

If `Q` is a set of at most `Ω + 1` primes, all `> z = 4(Ω+1)`, and `H` exceeds the
explicit bound, then every interval `(A, A+H]` contains a `z`-rough integer
divisible by no element of `Q`.
-/

namespace J6Sieve
open Finset

/-- `Ω = d (log₂ X + 1)` bounds the total number of prime factors of `d` numbers `≤ X`. -/
def Om (d X : ℕ) : ℕ := d * (Nat.log 2 X + 1)

/-- Sieving level `z = 4(Ω+1)`. -/
def zz (d X : ℕ) : ℕ := 4 * (Om d X + 1)

/-- `k` with `z < 2^k`. -/
def kk (d X : ℕ) : ℕ := Nat.log 2 (zz d X) + 1

/-- Brun truncation depth (odd). -/
def mm (d X : ℕ) : ℕ := 4 * kk d X + 3

/-- The explicit window-length bound `2 z (Ω+2) (m+2) z^(m+1)`. -/
def sieveBound (d X : ℕ) : ℕ :=
  2 * zz d X * (Om d X + 2) * (mm d X + 2) * zz d X ^ (mm d X + 1)

end J6Sieve

end

section
-- Source module: Solutions.R6Prm
/-!
# Shared parameter record for Jain's round six (`IntMul.Kappa.jain_round6_framework`)

`CrudeAssembly ab ac β ε x C₁ κ mc sc` is stated with real `x, C₁`, arbitrary `ε ∈ (0,1)`
and the savings `ab, ac`.  The normalization `r6_normalize` (file `R6Norm.lean`) turns
it into a `Prm` with

* `τ = 1 - ab`, `σ = 1 - ac` (the bit / complex moment exponents, both in `(0, 1]`),
* `ε ∈ [1/2, 1)` (raising a small `ε` to `1/2` only enlarges the gap),
* natural `x ≥ 1` and natural `C1` (rounded up),
* `lamp` = the `λ'` of `CrudeAssembly` (`lampOf τ σ`).

## Design choice for `lamp`
`Prm.Ok` only requires `lampOf P.τ P.σ ≤ P.lamp` (plus `P.lamp < 1` and the two `ε`-constraints
in terms of `P.lamp`).  So downstream workers may use `D ^ P.lamp` as an *upper* exponent for
every cost term that `CrudeAssembly` bounds by `D ^ λ'` (in particular `lamp ≥ τ, σ, χ, leaf`
with the `10⁻¹⁶` slacks: see `Prm.Ok.tau_lt_lamp`, etc.).  `r6_normalize` produces
`lamp = lampOf τ σ` exactly, but no downstream proof should rely on equality.

`β = 1/1000` is fixed (`R6.beta`).  `Prm.gap` is the minimum of the five cost margins of
`CrudeAssembly`; `r6_normalize` gives `κ < P.gap`.
-/

namespace IntMul.Kappa.R6

/-- The leaf parameter `β = 1/1000` of round six. -/
noncomputable def beta : ℝ := 1 / 1000

/-- The `λ'` of `CrudeAssembly` with `β = 1/1000`, as a function of `τ = 1 - a_b` and
`σ = 1 - a_c`: `χ = τ + (1-β) max(σ-τ,0)`, `leaf = σ + β(1-σ)`,
`λ = max(τ,σ,χ) + 10⁻¹⁶`, `λ' = max(λ, leaf) + 10⁻¹⁶`. -/
noncomputable def lampOf (τ σ : ℝ) : ℝ :=
  max (max (max τ σ) (τ + (1 - beta) * max (σ - τ) 0) + 1 / 10 ^ 16)
    (σ + beta * (1 - σ)) + 1 / 10 ^ 16

/-- Parameters of the round-six machine. -/
structure Prm where
  /-- bit moment exponent `1 - a_b` -/
  τ : ℝ
  /-- complex moment exponent `1 - a_c` -/
  σ : ℝ
  /-- the exponent `ε` (`d = ⌊b^ε⌋`) -/
  ε : ℝ
  /-- an upper bound for the `λ'` of `CrudeAssembly` -/
  lamp : ℝ
  /-- the `x` of `b' = ⌈b^(1+x)⌉` -/
  x : ℕ
  /-- the depth-guard constant `C₁` -/
  C1 : ℕ

namespace Prm

/-- `δ = 10⁻²²/x`. -/
noncomputable def δ (P : Prm) : ℝ := 1 / 10 ^ 22 / P.x

/-- `poly = (1+x) δ`. -/
noncomputable def poly (P : Prm) : ℝ := (1 + P.x) * P.δ

/-- All constraints of `CrudeAssembly` (with `β = 1/1000`), in terms of `τ, σ, λ' = lamp`,
plus the normalizations `1/2 ≤ ε < 1`, `0 < τ ≤ 1`, `0 < σ ≤ 1`, `1 ≤ x`.
(The constraint `2 + m_c log s_c ≤ C1` is network specific and kept outside.) -/
structure Ok (P : Prm) : Prop where
  tau_pos : 0 < P.τ
  tau_le : P.τ ≤ 1
  sigma_pos : 0 < P.σ
  sigma_le : P.σ ≤ 1
  eps_ge : 1 / 2 ≤ P.ε
  eps_lt : P.ε < 1
  x_ge : 1 ≤ P.x
  lampOf_le : lampOf P.τ P.σ ≤ P.lamp
  lamp_lt : P.lamp < 1
  eps_two_sub : P.ε * (2 - P.lamp) < 1
  eps_C1 : P.ε * P.C1 < 1 + P.x
  three_eps : 2 * P.ε + P.ε < 1 + P.x
  two_eps_sub : 2 * P.ε - 1 < P.lamp * P.ε
  delta_pos : 0 < P.δ
  delta_lt : P.δ < 1 / 8

/-- The minimum of the five cost margins `1-ε`, `ε(1-λ')`, `1-ε-poly`, `ε`,
`max(ε,1-ε)(1-τ)` of `CrudeAssembly`. -/
noncomputable def gap (P : Prm) : ℝ :=
  min (min (min (min (1 - P.ε) (P.ε * (1 - P.lamp))) (1 - P.ε - P.poly)) P.ε)
    (max P.ε (1 - P.ε) * (1 - P.τ))

end Prm

end IntMul.Kappa.R6

end

section
-- Source module: Solutions.R6Params
/-!
# Round six: the parameter map `n ↦ (b, b', p, L, T, d, ℓ, r, K, α², V)` and the cost `Ncost6`

Stack parameters (Colkitt/Jain, `stack-notes.tex` §1 Idea D, Idea C):

* `b = lg n` (`bP6`), `b' = b^(1+x)` (`b'P6`; `x : ℕ` so `⌈b^(1+x)⌉ = b^(1+x)`), `p = 6 b'` (`pP6`);
* `L` (`LP6`) = least `L` with `4n ≤ 2^L b'`, `T = 2^L` (`TP6`), so `4n ≤ T b' < 8n`;
* `d = ⌊b^ε⌋` (`dP6`), `ℓ = ⌈L/d⌉ = (L + d - 1)/d` (`ℓP6`), `r = 2^ℓ` (`rP6`),
  `K = ℓ - 1` (`KP6`, one chunk per axis);
* `α² = ⌊p/(48d)⌋ = ⌊b'/(8d)⌋` (`α2P6`, a natural number), `α = √(α²)` (`αP6`),
  `γ = 2 d α²` (`γP6`);
* bit volume `V = T p` (`VP6`), with `24 n ≤ V ≤ 48 n`.

## Normalization (same as OpenAI's `RCost.Ncost`)
`Ncost6` is the **per-bit** cost: the Table-1 cost divided by `V = T p`.  The machine time is
`C₀ (V · Ncost6 · polylog + n)`; since `V ≤ 48 n`, a bound `Ncost6 ≤ C b^(1-gap) polylog`
gives time `O(n lg^(1-gap) polylog)`.

`Ncost6 P n = d + ℓ d^λ' + d p^δ + (ℓ + log₂ p) + p^δ + ℓ (d ln p)^τ + 1`
(rows: prefix moves `1-ε`; butterflies `ε(1-λ')`; fine exposures/Gaussian/chirps/reserved axes
`1-ε-poly`; pointwise products `ε`; precision `p^δ = b^poly`; CRT reversal
`ε(1-τ) = max(ε,1-ε)(1-τ)` as `ε ≥ 1/2`).  Note `ℓ ≈ b^(1-ε)` and `p^δ ≤ 6 b^poly`.
-/

open Real

namespace IntMul.Kappa.R6

noncomputable section

/-! ## 1. The parameter map -/

/-- `b = lg n`. -/
def bP6 (n : ℕ) : ℕ := IntMul.lg n
/-- `b' = b^(1+x)`. -/
def b'P6 (P : Prm) (n : ℕ) : ℕ := bP6 n ^ (1 + P.x)
/-- `p = 6 b'`. -/
def pP6 (P : Prm) (n : ℕ) : ℕ := 6 * b'P6 P n

lemma bP6_pos (n : ℕ) : 1 ≤ bP6 n := le_max_right _ _

lemma b'P6_pos (P : Prm) (n : ℕ) : 1 ≤ b'P6 P n := Nat.one_le_pow _ _ (bP6_pos n)

lemma LP6_exists (P : Prm) (n : ℕ) : ∃ L : ℕ, 4 * n ≤ 2 ^ L * b'P6 P n := ⟨4 * n, by
  have h1 := b'P6_pos P n
  have h2 : 4 * n < 2 ^ (4 * n) := Nat.lt_two_pow_self
  nlinarith⟩

/-- `L`: least exponent with `4n ≤ 2^L b'`. -/
def LP6 (P : Prm) (n : ℕ) : ℕ := Nat.find (LP6_exists P n)
/-- `T = 2^L`. -/
def TP6 (P : Prm) (n : ℕ) : ℕ := 2 ^ LP6 P n
/-- `d = ⌊b^ε⌋`. -/
def dP6 (P : Prm) (n : ℕ) : ℕ := ⌊(bP6 n : ℝ) ^ P.ε⌋₊
/-- `ℓ = ⌈L/d⌉`. -/
def ℓP6 (P : Prm) (n : ℕ) : ℕ := (LP6 P n + dP6 P n - 1) / dP6 P n

/-- `α² = ⌊p/(48d)⌋`. -/
def α2P6 (P : Prm) (n : ℕ) : ℕ := pP6 P n / (48 * dP6 P n)

/-- Bit volume `V = T p`. -/
def VP6 (P : Prm) (n : ℕ) : ℝ := (TP6 P n : ℝ) * (pP6 P n : ℝ)

/-- The per-bit cost rows as a function of real `p, d, ℓ`. -/
def Ncost6R (P : Prm) (p d ℓ : ℝ) : ℝ :=
  d + ℓ * d ^ P.lamp + d * p ^ P.δ + (ℓ + Real.logb 2 p) + p ^ P.δ +
    ℓ * (d * Real.log p) ^ P.τ + 1

/-- **Normalized (per-bit) cost** of the round-six machine. -/
def Ncost6 (P : Prm) (n : ℕ) : ℝ := Ncost6R P (pP6 P n) (dP6 P n) (ℓP6 P n)

/-! ## 2. Elementary facts about `lg` -/

lemma n_le_two_pow_b (n : ℕ) : n ≤ 2 ^ bP6 n :=
  (Nat.le_pow_clog (by norm_num) n).trans (Nat.pow_le_pow_right (by norm_num) (le_max_left _ _))

/-! ## 3. Facts valid as soon as `b ≥ 4` -/

lemma b'_ge_sq (P : Prm) (hP : P.Ok) (n : ℕ) : bP6 n ^ 2 ≤ b'P6 P n :=
  Nat.pow_le_pow_right (bP6_pos n) (by have := hP.x_ge; omega)

lemma L_le_b (P : Prm) (hP : P.Ok) {n : ℕ} (hb : 2 ≤ bP6 n) : LP6 P n ≤ bP6 n := by
  apply Nat.find_min' (LP6_exists P n)
  have h1 := b'_ge_sq P hP n
  have h2 := n_le_two_pow_b n
  have h4 : 4 ≤ bP6 n ^ 2 := by nlinarith
  have : 4 * 2 ^ bP6 n ≤ b'P6 P n * 2 ^ bP6 n := Nat.mul_le_mul_right _ (h4.trans h1)
  nlinarith

lemma beps_ge_two (P : Prm) (hP : P.Ok) {n : ℕ} (hb : 4 ≤ bP6 n) : 2 ≤ (bP6 n : ℝ) ^ P.ε := by
  have hB : (4 : ℝ) ≤ bP6 n := by exact_mod_cast hb
  have hB1 : (1 : ℝ) ≤ bP6 n := by linarith
  have h1 : (bP6 n : ℝ) ^ ((1 : ℝ) / 2) ≤ (bP6 n : ℝ) ^ P.ε :=
    Real.rpow_le_rpow_of_exponent_le hB1 hP.eps_ge
  have h2 : ((bP6 n : ℝ) ^ ((1 : ℝ) / 2)) ^ 2 = bP6 n := by
    rw [← Real.rpow_natCast, ← Real.rpow_mul (by linarith)]; norm_num
  have h3 : 0 ≤ (bP6 n : ℝ) ^ ((1 : ℝ) / 2) := Real.rpow_nonneg (by linarith) _
  nlinarith

lemma d_le_beps (P : Prm) (n : ℕ) : (dP6 P n : ℝ) ≤ (bP6 n : ℝ) ^ P.ε :=
  Nat.floor_le (Real.rpow_nonneg (Nat.cast_nonneg _) _)

lemma d_half (P : Prm) (hP : P.Ok) {n : ℕ} (hb : 4 ≤ bP6 n) :
    (bP6 n : ℝ) ^ P.ε / 2 ≤ (dP6 P n : ℝ) := by
  have h := beps_ge_two P hP hb
  have := Nat.lt_floor_add_one ((bP6 n : ℝ) ^ P.ε)
  unfold dP6; linarith

lemma d_pos (P : Prm) (hP : P.Ok) {n : ℕ} (hb : 4 ≤ bP6 n) : 1 ≤ dP6 P n := by
  have h1 := d_half P hP hb
  have h2 := beps_ge_two P hP hb
  have : (1 : ℝ) ≤ dP6 P n := by linarith
  exact_mod_cast this

lemma beps_le_b (P : Prm) (hP : P.Ok) (n : ℕ) : (bP6 n : ℝ) ^ P.ε ≤ bP6 n := by
  have hb1 : (1 : ℝ) ≤ bP6 n := by exact_mod_cast bP6_pos n
  calc (bP6 n : ℝ) ^ P.ε ≤ (bP6 n : ℝ) ^ (1 : ℝ) :=
        Real.rpow_le_rpow_of_exponent_le hb1 hP.eps_lt.le
    _ = bP6 n := Real.rpow_one _

lemma d_le_b (P : Prm) (hP : P.Ok) (n : ℕ) : dP6 P n ≤ bP6 n := by
  have : (dP6 P n : ℝ) ≤ bP6 n := (d_le_beps P n).trans (beps_le_b P hP n)
  exact_mod_cast this

lemma ell_spec (L d : ℕ) (hd : 0 < d) : L ≤ d * ((L + d - 1) / d) ∧ d * ((L + d - 1) / d) ≤ L + d - 1 := by
  constructor
  · have := Nat.lt_div_mul_add (a := L + d - 1) hd
    rw [mul_comm]; omega
  · have := Nat.div_mul_le_self (L + d - 1) d
    rw [mul_comm]; exact this

lemma dℓ_spec (P : Prm) (hP : P.Ok) {n : ℕ} (hb : 4 ≤ bP6 n) :
    LP6 P n ≤ dP6 P n * ℓP6 P n ∧ dP6 P n * ℓP6 P n ≤ LP6 P n + dP6 P n - 1 :=
  ell_spec _ _ (d_pos P hP hb)

/-- `ℓ ≤ 2b/d`. -/
lemma ell_le (P : Prm) (hP : P.Ok) {n : ℕ} (hb : 4 ≤ bP6 n) :
    (ℓP6 P n : ℝ) ≤ 2 * (bP6 n : ℝ) / dP6 P n := by
  have hs := dℓ_spec P hP hb
  have hL := L_le_b P hP (n := n) (by omega)
  have hdb := d_le_b P hP n
  have hd : (0 : ℝ) < dP6 P n := by exact_mod_cast d_pos P hP hb
  rw [le_div_iff₀ hd]
  have : dP6 P n * ℓP6 P n ≤ 2 * bP6 n := by omega
  have : ((dP6 P n * ℓP6 P n : ℕ) : ℝ) ≤ ((2 * bP6 n : ℕ) : ℝ) := by exact_mod_cast this
  push_cast at this; linarith

/-- `ℓ ≤ 4 b^(1-ε)`. -/
lemma ell_le_rpow (P : Prm) (hP : P.Ok) {n : ℕ} (hb : 4 ≤ bP6 n) :
    (ℓP6 P n : ℝ) ≤ 4 * (bP6 n : ℝ) ^ (1 - P.ε) := by
  have hB0 : (0 : ℝ) < bP6 n := by exact_mod_cast (show 0 < bP6 n by omega)
  have h1 := ell_le P hP hb
  have h2 := d_half P hP hb
  have he : (0 : ℝ) < (bP6 n : ℝ) ^ P.ε := Real.rpow_pos_of_pos hB0 _
  have hd : (0 : ℝ) < dP6 P n := by linarith
  have hsplit : (bP6 n : ℝ) = (bP6 n : ℝ) ^ (1 - P.ε) * (bP6 n : ℝ) ^ P.ε := by
    rw [← Real.rpow_add hB0]; simp
  refine h1.trans ?_
  rw [div_le_iff₀ hd]
  have h0 : 0 ≤ (bP6 n : ℝ) ^ (1 - P.ε) := (Real.rpow_pos_of_pos hB0 _).le
  calc 2 * (bP6 n : ℝ) = 2 * ((bP6 n : ℝ) ^ (1 - P.ε) * (bP6 n : ℝ) ^ P.ε) := by rw [← hsplit]
    _ = 4 * (bP6 n : ℝ) ^ (1 - P.ε) * ((bP6 n : ℝ) ^ P.ε / 2) := by ring
    _ ≤ 4 * (bP6 n : ℝ) ^ (1 - P.ε) * dP6 P n := by gcongr

lemma gamma_le (P : Prm) (n : ℕ) : 4 * (2 * dP6 P n * α2P6 P n) ≤ b'P6 P n := by
  have h := Nat.div_mul_le_self (pP6 P n) (48 * dP6 P n)
  unfold α2P6
  unfold pP6 at h ⊢
  have : 48 * (dP6 P n * (6 * b'P6 P n / (48 * dP6 P n))) ≤ 6 * b'P6 P n := by
    calc 48 * (dP6 P n * (6 * b'P6 P n / (48 * dP6 P n)))
        = 6 * b'P6 P n / (48 * dP6 P n) * (48 * dP6 P n) := by ring
      _ ≤ 6 * b'P6 P n := h
  nlinarith

/-! ## 4. Eventual facts (box exponent and volume) -/

/-- The pointwise parameter conditions of the round-six stack, valid for large `n`. -/
structure Good (P : Prm) (n : ℕ) : Prop where
  b_ge : 4 ≤ bP6 n
  b'_le : 8 * b'P6 P n ≤ 2 ^ (bP6 n / 2)
  T_lo : 4 * n ≤ TP6 P n * b'P6 P n
  T_hi : TP6 P n * b'P6 P n < 8 * n
  L_pos : 1 ≤ LP6 P n
  L_le : LP6 P n ≤ bP6 n
  L_ge : bP6 n ≤ 2 * LP6 P n
  V_lo : 24 * (n : ℝ) ≤ VP6 P n
  V_hi : VP6 P n ≤ 48 * n
  d_pos : 1 ≤ dP6 P n
  d_le_b : dP6 P n ≤ bP6 n
  d_le : (dP6 P n : ℝ) ≤ (bP6 n : ℝ) ^ P.ε
  d_ge : (bP6 n : ℝ) ^ P.ε / 2 ≤ dP6 P n
  dℓ_ge : LP6 P n ≤ dP6 P n * ℓP6 P n
  dℓ_le : dP6 P n * ℓP6 P n ≤ LP6 P n + dP6 P n - 1
  ell_pos : 1 ≤ ℓP6 P n
  ell_le : (ℓP6 P n : ℝ) ≤ 2 * (bP6 n : ℝ) / dP6 P n
  ell_ge : (bP6 n : ℝ) / (2 * dP6 P n) ≤ ℓP6 P n
  ell_le_rpow : (ℓP6 P n : ℝ) ≤ 4 * (bP6 n : ℝ) ^ (1 - P.ε)
  gamma_le : 4 * (2 * dP6 P n * α2P6 P n) ≤ b'P6 P n

/-! ## 5. The cost bound -/

/-- The constant of `Ncost6R_le`. -/
def Cst (P : Prm) : ℝ := 64 + 6 * P.x

end

end IntMul.Kappa.R6

end