Trilinear Hilbert transform: leaf_estimate

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.leaf_estimate (κ : LocalKernelClass) (c₀ cc : ℕ) (hcc : 1 ≤ cc) : ∃ (Cl : ℕ) (K₀ : ℝ), 1 ≤ Cl ∧ 2 ≤ K₀ ∧ ∀ {A : ActiveSetup κ c₀} (bf : A.BasicFamilies) (k : ℕ) {η₀ E : ℝ}, A.AncClosed → (∀ I ∈ A.cells, ∀ (s s' : Fin 4), s ≠ s' → PairSmall (dyadicGridLeft A.G I.1 I.2) (dyadicGridLength A.G I.1) (A.w I) s s' (A.Y I s) (A.Y I s') (2 * η₀)) → A.SubRootProps η₀ E → A.S = 2 → A.η = 4 * η₀ → 0 < η₀ → A.cells.Nonempty → ∀ {q : ℝ} (hq2 : 2 < q) (hq3 : q < 3) {Nd : ℕ}, A.DepthWin Nd → ∀ (p : Fin 3) (AD : bf.AttemptData p) (x : bf.Vtx) (s : ℕ) {δ ρ kD : ℝ}, 0 < δ → δ ≤ 1 / 8 → 8 * ↑A.dBnd * δ ≤ 1 → δ ^ 2 * AD.n (AD.fp.Lc + 5) * A.colBudget ^ 2 ≤ 1 → 0 < ρ → ρ < 1 → K₀ ≤ ↑k → ↑k ^ cc ≤ kD → Real.log (2 * (8 * A.colBudget + (1 + ↑AD.Mp) * AD.n (AD.fp.Lc + 5))) ≤ ↑k ^ cc → Real.log (2 * A.colBudget) ≤ ↑k ^ cc → ↑(2 * A.famFuel + 2) ≤ ↑cc * (Real.log ↑k + 1) → ↑AD.fp.Lc + 6 ≤ ↑k ^ cc → ↑AD.fp.Hmax + 1 ≤ (↑k * ↑AD.fp.P) ^ cc → ↑A.dBnd ≤ ↑k ^ cc → Real.log AD.fp.Hed ≤ ↑k ^ cc → Real.log A.Hsrc ≤ ↑k ^ cc → Real.log (max A.H padW) ≤ ↑k ^ cc → δ⁻¹ ≤ Real.exp kD → E ≤ ↑k ^ cc → ρ⁻¹ ≤ ↑k ^ cc → ∃ (F : Fin 6 → Finset (ℤ × ℤ)), (∀ (i : Fin 6), ∀ c ∈ F i, dyadicGridCell A.G c.1 c.2 ⊆ dyadicGridCell A.G A.R.1 A.R.2) ∧ (∀ (i : Fin 6), dyadicRootLength A.G (F i) ≤ 2 * ρ * dyadicGridLength A.G A.R.1) ∧ ∀ cs ⊆ AD.Tc, ⋯ → ⋯

Blueprint lines 2838-2851 on one leaf of the guarded search of an attempt (stages: schedule, offsets and modes, frozen families and first tops, helper catalogs, leaf bound, and the explicit form of eq:before-absorption on the leaf). For a degree c of the standing bounds there are C and K₀ such that, when log of the main counts and of the budget, L + 6, H_max + 1, d_B, log H_ed, log H_src, log max(H, padW), E and ρ⁻¹ are at most k^c (resp. (kP)^c) and k^c ≤ k_D, log δ⁻¹ ≤ k_D, the weighted minima of the leaf over the test cells outside the failure roots and six cut families of root length at most 2ρ|R| are at most C u^C G^C (η^{1/1200} + η₀ + (P+1)² τ₃ + e^{C k^c} (√δ + e^{-k_D})) |R| + C e^{-k} |R| plus the near-band term C (1 + C_N) C_q (C u^C + 2)^{2(q-2)/(q-1)} (2 + log(C u^C + 2))⁶ G^C P^{-1/2} |R|, where u = k_D P, G = exp((1 + log 2k)²) and k_D is the accuracy of the enlarged budget.