Trilinear Hilbert transform: leaf_final

theorem TrilinearHT.Auto.leaf_final (κ : LocalKernelClass) {q : ℝ} (hq2 : 2 < q) (hq3 : q < 3) (Nd : ℕ) {Cg : ℕ} {Msch : ℝ} (hMsch : 0 < Msch) {g : ℕ} {cT cL cK cMc cm ce ce2 cQ : ℝ} {CΛ eΛ CM1 t3 Cb Cl k cc : ℕ} (hconst : g = 8192 * (cc + 1) * (1024 * (cc + 1) + cc + 7) + cc ^ 2 + 8 ∧ cT = 10 ^ 22 * (1 + localFormUniformConstant κ) ^ 2 ∧ cL = 159 + 32 * ↑g + 8 * Real.log cT ∧ cK = (1 + 7 * 10 ^ 9 + cT) * (cL + 2) ∧ cMc = (C4c κ + 4 * C3c κ) * cL ^ 4 * cK ^ 2 ∧ cm = 196608 * cT + 83 * (1 + 81 * localFormUniformConstant κ * (30000 + √cT)) * (1 + cT) ^ 3 + cMc ∧ ce = 6642 * localFormUniformConstant κ * (60000 + √cT) ^ 3 * 288 + 9 * (16 * fourErrC κ 3 + 648 * threeErrC κ 3 1 + 324 * threeErrC κ 3 1 * √cT) ∧ ce2 = K1c * (2 * fourKC κ 3 * 12 ^ 4) + 4 * (K1c * (8 * entryCU κ 3 1 * 2 ^ (1 + 4) * 12 ^ 3)) * 501 ∧ cQ = 65536 * (8 + 80 * 9 ^ cc * ↑cc) * (80 * 9 ^ cc * ↑cc) * (4 * ↑cc ^ 2) * (17 * 10 ^ 7) ∧ CΛ = 2 * Cg + 12 ∧ eΛ = Cg + 3 * cc ∧ CM1 = (⌈Msch⌉₊ + 1) * CΛ ^ 16 ∧ t3 = 3 ^ cc ∧ Cb = CM1 + 501 * Cg + t3 + 2 * cc + 20 + 16 * eΛ ∧ Cl = ⌈cm * ↑Cb ^ 59 + ce * ↑Cb ^ 18 + ce2 + 3 * 10 ^ 11 * cQ⌉₊ + 59 * Cb + 4 * g + 8 * cc + 8) (hcc : 1 ≤ cc) (hk2 : 2 ≤ ↑k) {kD : ℝ} (hkD : ↑k ^ cc ≤ kD) {P : ℕ} (hP : 1 ≤ P) {cb Nl : ℝ} {Mp V : ℕ} (hcb : 2 ≤ cb) (hNl4 : 4 ≤ Nl) (hkB : Real.log (2 * (8 * cb + (1 + ↑Mp) * Nl)) ≤ ↑k ^ cc) (hkb : Real.log (2 * cb) ≤ ↑k ^ cc) (hVle : ↑V ≤ 8 * cb + 1) {famFuel : ℕ} (hkF : ↑(2 * famFuel + 2) ≤ ↑cc * (Real.log ↑k + 1)) {dB : ℕ} (hdB1 : 1 ≤ dB) (hdBk : ↑dB ≤ ↑k ^ cc) {E ρ δ η η₀ τ₃ R : ℝ} (hE0 : 0 ≤ E) (hEk : E ≤ ↑k ^ cc) (hρ : 0 < ρ) (hρ1 : ρ < 1) (hρk : ρ⁻¹ ≤ ↑k ^ cc) (hδ : 0 < δ) (hδ8 : δ ≤ 1 / 8) (hη0 : 0 ≤ η) (hη₀ : 0 < η₀) (hτ₃ : 0 < τ₃) (hRl0 : 0 < R) (S : ModeSchedule) (hD2 : 2 ≤ S.Dstar) (hH2 : 2 ≤ S.H) (hK1 : 1 ≤ S.K) (hSd : S.dmax = 2 * dB + 2) (hSDm : S.Dm = max 2 Nl) (hJH : ↑S.Jstar ≤ Real.log S.H) {Λ : ℝ} (hΛ0 : 0 ≤ Λ) (hΛ : Λ ≤ ↑CΛ * (kD * ↑P) ^ eΛ) (hK : ↑S.K ≤ Msch * Λ ^ 16) (hlogH : Real.log S.H ≤ Msch * Λ ^ 12) (hlD : Real.log S.Dstar ≤ ↑Cg * (kD * ↑P) ^ Cg) (hexpD : Real.exp kD ≤ S.Dstar) {Iw : ℕ} (hIw : Iw = ⌊Real.logb 2 (S.Dstar ^ 250)⌋₊) {Vl0 : ℝ} (hVl0 : Vl0 = 24 * (↑⌊180 * ↑S.dmax * Real.log (2 * S.Dm) / (1 / 1024)⌋₊ + 1) * (Real.exp ((6144 * (↑cc + 1) * (1024 * (↑cc + 1) + ↑cc + 7) + 4) * (1 + Real.log (2 * ↑k)) ^ 2) + 2 * 1 / S.Dstar ^ 394)) {TT : ℝ} (hT0 : 0 ≤ TT) (hTTle : TT ≤ 10 ^ 14 * (1 + localFormUniformConstant κ) ^ 2 * ↑(2 ^ famFuel) ^ 4 * (1 + ↑(2 * famFuel + 2)) ^ 2 * (1 + ↑S.K) ^ 2 * (Real.exp ((4096 * (↑cc + 1) * (1024 * (↑cc + 1) + ↑cc + 7) + ↑cc ^ 2 + 3) * (1 + Real.log (2 * ↑k)) ^ 2) + E + Vl0 + 1) / ρ) {U : ℝ} (hUdef : U = max (2 * (cb + 2) * S.Dstar ^ 2) √TT) {MV : ℝ} (hMV : MV = ↑Mp * ↑V) {ε : ℝ} (hεdef : ε = (U ^ 3 * S.Dstar ^ 5 * Real.exp ↑k * (1 + MV))⁻¹) {Mt : ℝ} (hMt : Mt = 24 * (2 * Real.exp ((6144 * (↑cc + 1) * (1024 * (↑cc + 1) + ↑cc + 7) + 4) * (1 + Real.log (2 * ↑k)) ^ 2) + 2 * ↑S.K * Vl0) * ↑(Finset.range (S.Jstar + 1) ×ˢ (Finset.range (Nat.log 2 ⌊S.Dstar⌋₊ + 1) ×ˢ Finset.range (Nat.log 2 ⌊S.Dstar⌋₊ + 1)) ×ˢ dyThr ε U S.Dstar).card / ρ) {T2v : ℝ} (hT2le : T2v ≤ 4 * (↑S.K * (20 * Real.exp ((4096 * (↑cc + 1) * (1024 * (↑cc + 1) + ↑cc + 7) + ↑cc ^ 2 + 3) * (1 + Real.log (2 * ↑k)) ^ 2) + 32) + ↑S.K * Vl0) / ρ) {B0 cB eB : ℝ} (hB0 : B0 = 2) (hcBdef : cB = coreBd B0 T2v) (heBdef : eB = errBd B0 T2v) {cM4 cM3 : ℝ} (hcM4 : cM4 = coreM4F κ S (1 / 1024) 3 U ε (max (max 1 Mt) TT)) (hcM3 : cM3 = ∑ l : Fin 4, coreM3F κ S (1 / 1024) 3 1 Iw U ε (max (max 1 Mt) TT) l) {nearS Γ : ℝ} {Os : Finset (Fin 4 × Fin 4 × ℕ × ℕ × ℕ × ℕ)} (hOs : Os = ActiveSetup.BasicFamilies.FamParams.SideLeafM.nOs (2 ^ famFuel) (2 * famFuel + 2)) (hΓle : Γ ≤ 2000 * ↑Os.card * (↑(Nat.log 2 S.K + 1) ^ 3 * ((↑(2 * famFuel + 2) + 1) ^ 2 * Real.exp (2 * (1024 * (↑cc + 1) * (1024 * (↑cc + 1) + ↑cc + 7) * (1 + Real.log (2 * ↑k)) ^ 2)))) * (Real.exp ((4096 * (↑cc + 1) * (1024 * (↑cc + 1) + ↑cc + 7) + ↑cc ^ 2 + 3) * (1 + Real.log (2 * ↑k)) ^ 2) + Vl0 + E + 1)) (hnearS : nearS ≤ 64 * (4 * ((nbCM κ hq2 hq3 + nbCUM κ hq2 hq3) * (1 + finiteDepthConstant κ q Nd) * (1 + Real.log (↑S.K + 2)) * (↑S.K + 2) ^ (2 * (q - 2) / (q - 1)) * (64 * (2 * (2 * √1)) * (2 * (2 * √1)))) * (hullCutConstant (ρ / 64 / 2) * ↑(Nat.log 2 S.K + 1 + 1) * (1 + Real.log (2 + ↑(Nat.log 2 S.K + 1 + 1) * ↑(Nat.log 2 S.K + 1 + 1) * (↑Os.card * ↑Mp * ↑V)))) * Γ / √↑P * R)) {cE : ℝ} (hcEsum : cE ≤ (16 * fourErrC κ 3 * ((S.Dstar ^ 100)⁻¹ * S.Dstar ^ 10) + K1c * (2 * fourKC κ 3 * 12 ^ 4 * ε * U ^ 3 * S.Dstar ^ 4) + 4 * (81 * threeErrC κ 3 1 * ((S.Dstar ^ 100)⁻¹ * S.Dstar ^ 10) * U + K1c * (8 * entryCU κ 3 1 * 2 ^ (1 + 4) * 12 ^ 3 * ε * U ^ 3 * (S.Dstar ^ 3 * (↑Iw + 1))))) * (↑(Mp * V) * R)) {Ee : ℝ} (hEe0 : 0 ≤ Ee) (hEeb : Ee ≤ (8 * ↑dB * δ + 2 * δ ^ 2) * (4 * Nl * cb ^ 2 * 1) * ↑(4 * (Mp * V)) * R) {fc : ℝ} (hfc : fc = (2 * ↑famFuel + 2) * ((↑P + 1) ^ 2 * (16 * τ₃ * 2 ^ 2))) : 6 * 256 * (2 ^ famFuel) ^ 2 * (2 * η₀ + fc) * TT * R + 6 * nearS + η ^ (1 - (1 - 1 / 1200)) * (TT ^ ((1 - 1 / 1200) / 2) * TT ^ ((1 - 1 / 1200) / 2) * TT ^ ((1 - 1 / 1200) / 2) * R) + 82 * (81 * (localFormUniformConstant κ * (cB + eB + √TT) ^ 3) * (√(4 * (↑(Mp * V) * R)) * √Ee)) + 82 * (η ^ (1 - (1 - 1 / 1200)) * (81 * localFormUniformConstant κ * max cB √TT) ^ (1 - 1 / 1200) * (TT ^ ((1 - 1 / 1200) / 2) * TT ^ ((1 - 1 / 1200) / 2) * TT ^ ((1 - 1 / 1200) / 2) * R)) + (η ^ (1 / 1200) * (R * (cM4 + cM3)) + cE) ≤ leafBnd Cl kD P k cc η η₀ τ₃ δ (finiteDepthConstant κ q Nd) (nbCM κ hq2 hq3 + nbCUM κ hq2 hq3) q R

The arithmetic of the explicit leaf bound (eq:before-absorption on one leaf): the right side of leaf_bound (in the shape of leaf_raw_le), with the side caps, core bounds, near bands, core errors and physical errors of a leaf given by their explicit forms or bounds, is at most leafBnd. All sizes are reduced to the size parameter B = C_b (k_D P)^{C_b} and the unit G = e^{g (1 + log 2k)²}.

Steps of leaf_estimate. Each lemma below is one step of that proof, stated over the hypotheses and local definitions (as lets) of the proof that it uses, so that it is elaborated in a small local context instead of the long context of the whole proof.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.leaf_estimate_hn_mono (κ : LocalKernelClass) (c₀ : ℕ) (A : ActiveSetup κ c₀) (bf : A.BasicFamilies) (p : Fin 3) (AD : bf.AttemptData p) : 2 ≤ A.colBudget → Monotone AD.n

Step hn_mono of leaf_estimate, over the part of its context that it uses.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.leaf_estimate_hpathU (κ : LocalKernelClass) (c₀ : ℕ) (A : ActiveSetup κ c₀) (bf : A.BasicFamilies) (p : Fin 3) (AD : bf.AttemptData p) (s : ℕ) : have fp := AD.fp; have Lf := leafAt A.famFuel fp.Lc (A.basicSlot p) s; have ks := Lf.k; have S0 := {I ∈ AD.Tc | ¬∃ c ∈ fp.failRoots, dyadicGridCell A.G I.1 I.2 ⊆ dyadicGridCell A.G c.1 c.2}; S0 ⊆ AD.Tc → have gs := fun (I : ℤ × ℤ) => fp.groupsAt I ks; have gset := S0.biUnion gs; have U := fun (x : Fin 4) (G : bf.Grp) => {I ∈ S0 | G ∈ gs I}; (U = fun (x : Fin 4) (G : bf.Grp) => {I ∈ S0 | G ∈ gs I}) → ∀ (y : ℝ), ∑ l : Fin 4, ∑ G ∈ gset, {I ∈ U l G | y ∈ dyadicGridCell A.G I.1 I.2}.card ≤ 4 * (AD.Mp * A.famVtxBound)

Step hpathU of leaf_estimate, over the part of its context that it uses.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.leaf_estimate_hU16 (κ : LocalKernelClass) (c₀ : ℕ) (A : ActiveSetup κ c₀) : 2 ≤ A.colBudget → ∀ (S : ModeSchedule), 2 ≤ S.Dstar → ∀ (U : ℝ), 2 * (A.colBudget + 2) * S.Dstar ^ 2 ≤ U → 16 ≤ U

Step hU16 of leaf_estimate, over the part of its context that it uses.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.leaf_estimate_hMV0 (κ : LocalKernelClass) (c₀ : ℕ) (A : ActiveSetup κ c₀) (bf : A.BasicFamilies) (p : Fin 3) (AD : bf.AttemptData p) (MV : ℝ) : MV = ↑AD.Mp * ↑A.famVtxBound → 0 ≤ MV

Step hMV0 of leaf_estimate, over the part of its context that it uses.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.leaf_estimate_hε0 (k : ℕ) (S : ModeSchedule) : 2 ≤ S.Dstar → ∀ (U : ℝ), 16 ≤ U → ∀ (MV : ℝ), 0 ≤ MV → ∀ (ε : ℝ), ε = (U ^ 3 * S.Dstar ^ 5 * Real.exp ↑k * (1 + MV))⁻¹ → 0 < ε

Step hε0 of leaf_estimate, over the part of its context that it uses.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.leaf_estimate_hτb (κ : LocalKernelClass) (c₀ : ℕ) (A : ActiveSetup κ c₀) (bf : A.BasicFamilies) (p : Fin 3) (AD : bf.AttemptData p) : have fp := AD.fp; have Nl := AD.n (fp.Lc + 5); have BN := ⌈8 * A.colBudget + Nl⌉₊; have τb := 1 / (1 + ↑BN * A.colBudget ^ 2); 0 < τb

Step hτb of leaf_estimate, over the part of its context that it uses.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.leaf_estimate_hτb1 (κ : LocalKernelClass) (c₀ : ℕ) (A : ActiveSetup κ c₀) (bf : A.BasicFamilies) (p : Fin 3) (AD : bf.AttemptData p) : have fp := AD.fp; have Nl := AD.n (fp.Lc + 5); have BN := ⌈8 * A.colBudget + Nl⌉₊; have τb := 1 / (1 + ↑BN * A.colBudget ^ 2); τb = 1 / (1 + ↑BN * A.colBudget ^ 2) → τb ≤ 1

Step hτb1 of leaf_estimate, over the part of its context that it uses.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.leaf_estimate_hτbN (κ : LocalKernelClass) (c₀ : ℕ) (A : ActiveSetup κ c₀) (bf : A.BasicFamilies) (p : Fin 3) (AD : bf.AttemptData p) : have fp := AD.fp; have Nl := AD.n (fp.Lc + 5); have BN := ⌈8 * A.colBudget + Nl⌉₊; have τb := 1 / (1 + ↑BN * A.colBudget ^ 2); τb = 1 / (1 + ↑BN * A.colBudget ^ 2) → τb * ↑BN * A.colBudget ^ 2 ≤ 1

Step hτbN of leaf_estimate, over the part of its context that it uses.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.leaf_estimate_hNq (κ : LocalKernelClass) (c₀ : ℕ) (A : ActiveSetup κ c₀) (bf : A.BasicFamilies) : ∀ (a : ℝ) (p : Fin 3) (AD : bf.AttemptData p) (d : bf.Vtx) (s : ℕ), have fp := AD.fp; have Nl := AD.n (fp.Lc + 5); 0 ≤ Nl → have Lf := leafAt A.famFuel fp.Lc (A.basicSlot p) s; have ks := Lf.k; have S0 := {I ∈ AD.Tc | ¬∃ c ∈ fp.failRoots, dyadicGridCell A.G I.1 I.2 ⊆ dyadicGridCell A.G c.1 c.2}; have gs := fun (I : ℤ × ℤ) => fp.groupsAt I ks; have gset := S0.biUnion gs; (∀ (l : Fin 4), (AD.cat l).length ≤ fp.Mc) → have BN := ⌈8 * A.colBudget + Nl⌉₊; (∀ (G : ↥gset), (↑G).1 = ks) → (∀ (l : Fin 4), fp.bbase (Lf.role l) + fp.P ≤ fp.Hmax) → ∀ (l : Fin 4) (y : ℝ), {q : ↥gset × (bf.Lab ⊕ Fin fp.Mc) | ∃ I ∈ A.cells, (∃ (k' : ℕ), fp.Cert k' (↑q.1) I) ∧ ∃ (p_1 : Fin fp.P), y ∈ dyadicGridCell A.G I.1 I.2 ∧ q.2 ∈ mainLabelsM A.G fp.Mc (bf.origCols l) (AD.cat l) I (fp.brank (Lf.role l)) (fp.bmask I (↑q.1) (Lf.role l) (↑p_1 + 1)) d}.card ≤ BN

Step hNq of leaf_estimate, over the part of its context that it uses.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.leaf_estimate_hden (κ : LocalKernelClass) (c₀ : ℕ) (A : ActiveSetup κ c₀) (bf : A.BasicFamilies) (p : Fin 3) (AD : bf.AttemptData p) : have fp := AD.fp; have Nl := AD.n (fp.Lc + 5); 2 ≤ A.colBudget → 4 ≤ Nl → have NH := 2 * A.colBudget + (1 + ↑AD.Mp) * Nl; 0 < 1 + A.colBudget * √(AD.n (fp.Lc + 4)) * (A.colBudget * √NH)

Step hden of leaf_estimate, over the part of its context that it uses.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.leaf_estimate_hτ₂1 (κ : LocalKernelClass) (c₀ : ℕ) (A : ActiveSetup κ c₀) (bf : A.BasicFamilies) (p : Fin 3) (AD : bf.AttemptData p) : have fp := AD.fp; have Nl := AD.n (fp.Lc + 5); 2 ≤ A.colBudget → 4 ≤ Nl → have NH := 2 * A.colBudget + (1 + ↑AD.Mp) * Nl; have τ₂ := AD.τ₃ / (1 + A.colBudget * √(AD.n (fp.Lc + 4)) * (A.colBudget * √NH)); τ₂ = AD.τ₃ / (1 + A.colBudget * √(AD.n (fp.Lc + 4)) * (A.colBudget * √NH)) → 0 < 1 + A.colBudget * √(AD.n (fp.Lc + 4)) * (A.colBudget * √NH) → τ₂ ≤ 1

Step hτ₂1 of leaf_estimate, over the part of its context that it uses.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.leaf_estimate_hτ₂' (κ : LocalKernelClass) (c₀ : ℕ) (A : ActiveSetup κ c₀) (bf : A.BasicFamilies) (p : Fin 3) (AD : bf.AttemptData p) : have fp := AD.fp; have Nl := AD.n (fp.Lc + 5); 2 ≤ A.colBudget → 4 ≤ Nl → have NH := 2 * A.colBudget + (1 + ↑AD.Mp) * Nl; have τ₂ := AD.τ₃ / (1 + A.colBudget * √(AD.n (fp.Lc + 4)) * (A.colBudget * √NH)); τ₂ = AD.τ₃ / (1 + A.colBudget * √(AD.n (fp.Lc + 4)) * (A.colBudget * √NH)) → 0 < 1 + A.colBudget * √(AD.n (fp.Lc + 4)) * (A.colBudget * √NH) → τ₂ * (A.colBudget * √(AD.n (fp.Lc + 4)) * (A.colBudget * √NH)) ≤ AD.τ₃

Step hτ₂' of leaf_estimate, over the part of its context that it uses.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.leaf_estimate_hcapV0 (κ : LocalKernelClass) (c₀ cc : ℕ) (A : ActiveSetup κ c₀) (k : ℕ) : 0 < dyadicGridLength A.G A.R.1 → 0 ≤ FamParams.capV A cc ↑k

Step hcapV0 of leaf_estimate, over the part of its context that it uses.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.leaf_estimate_hVl00 (cc k : ℕ) (S : ModeSchedule) (Vl0 : ℝ) : Vl0 = 24 * (↑⌊180 * ↑S.dmax * Real.log (2 * S.Dm) / (1 / 1024)⌋₊ + 1) * (Real.exp ((6144 * (↑cc + 1) * (1024 * (↑cc + 1) + ↑cc + 7) + 4) * (1 + Real.log (2 * ↑k)) ^ 2) + 2 * 1 / S.Dstar ^ 394) → 0 ≤ Vl0

Step hVl00 of leaf_estimate, over the part of its context that it uses.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.leaf_estimate_hB00 (κ : LocalKernelClass) (c₀ cc : ℕ) (A : ActiveSetup κ c₀) (k : ℕ) (Vl0 : ℝ) : 0 < dyadicGridLength A.G A.R.1 → 0 ≤ Vl0 → 0 ≤ FamParams.SideInput.sideB0 A cc (↑k) Vl0

Step hB00 of leaf_estimate, over the part of its context that it uses.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.leaf_estimate_hbig (κ : LocalKernelClass) (c₀ cc : ℕ) (A : ActiveSetup κ c₀) (bf : A.BasicFamilies) (k : ℕ) (p : Fin 3) (AD : bf.AttemptData p) : have fp := AD.fp; have Nl := AD.n (fp.Lc + 5); Real.log (2 * (8 * A.colBudget + (1 + ↑AD.Mp) * Nl)) ≤ ↑k ^ cc → 2 ≤ A.colBudget → 4 ≤ Nl → 2 * (8 * A.colBudget + (1 + ↑AD.Mp) * Nl) ≤ Real.exp (↑k ^ cc)

Step hbig of leaf_estimate, over the part of its context that it uses.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.leaf_estimate_h64D (cc : ℕ) : 1 ≤ cc → ∀ (kD : ℝ), 1 ≤ kD → 2 ≤ kD → 64 * kD ≤ kD ^ (cc + 6)

Step h64D of leaf_estimate, over the part of its context that it uses.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.leaf_estimate_hlogHm (κ : LocalKernelClass) (c₀ cc : ℕ) (A : ActiveSetup κ c₀) (k : ℕ) (δ kD : ℝ) : 0 < δ → have dB := A.dBnd; have Hm := max (max A.Hsrc (Real.exp ↑dB)) (max (5832 * max A.H padW ^ 4) (↑dB * (bumpConst * 8 ^ 32 * (2 / δ)))); 1 ≤ Hm → ↑dB ≤ ↑k ^ cc → Real.log A.Hsrc ≤ ↑k ^ cc → Real.log (max A.H padW) ≤ ↑k ^ cc → δ⁻¹ ≤ Real.exp kD → ↑k ^ cc ≤ kD → 1 ≤ kD → 1 ≤ ↑k ^ cc → kD ≤ kD ^ (cc + 6) → ↑k ^ cc ≤ kD ^ (cc + 6) → 64 * kD ≤ kD ^ (cc + 6) → 64 * ↑k ^ cc ≤ kD ^ (cc + 6) → Real.log bumpConst + 68 ≤ ↑k ^ cc → Real.log Hm ≤ kD ^ (cc + 6)

Step hlogHm of leaf_estimate, over the part of its context that it uses.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.leaf_estimate_hQ0l (κ : LocalKernelClass) (c₀ cc : ℕ) (A : ActiveSetup κ c₀) (bf : A.BasicFamilies) (k : ℕ) (p : Fin 3) (AD : bf.AttemptData p) : 1 ≤ ↑k → have fp := AD.fp; have dB := A.dBnd; 1 ≤ dB → ↑dB ≤ ↑k ^ cc → Real.log fp.Hed ≤ ↑k ^ cc → Real.log ↑(fp.Q0bd dB) ≤ ↑k ^ (3 * cc) + 1

Step hQ0l of leaf_estimate, over the part of its context that it uses.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.leaf_estimate_hΛ0 (κ : LocalKernelClass) (c₀ Dm0 : ℕ) (A : ActiveSetup κ c₀) (bf : A.BasicFamilies) (p : Fin 3) (AD : bf.AttemptData p) (δ kD : ℝ) : have fp := AD.fp; have dB := A.dBnd; have Nl := AD.n (fp.Lc + 5); have Hm := max (max A.Hsrc (Real.exp ↑dB)) (max (5832 * max A.H padW ^ 4) (↑dB * (bumpConst * 8 ^ 32 * (2 / δ)))); 1 ≤ dB → 0 ≤ Real.log (max 2 Nl) → Real.log (fp.Bst Dm0 dB Hm δ Nl kD δ) = Real.log ↑(fp.Q0bd dB) + Real.log (2 ^ (fp.Kstar Dm0 dB Hm δ Nl kD δ + 1)) → 0 ≤ Real.log (2 ^ (fp.Kstar Dm0 dB Hm δ Nl kD δ + 1)) → 0 ≤ Real.log (fp.modeStarG Dm0 dB Hm δ Nl kD δ) → have Λ := ↑(2 * dB + 2) + Real.log (fp.modeStarG Dm0 dB Hm δ Nl kD δ) + Real.log (fp.Bst Dm0 dB Hm δ Nl kD δ) + Real.log (max 2 Nl) + Real.log ↑(fp.Q0bd dB) + 1; Λ = ↑(2 * dB + 2) + Real.log (fp.modeStarG Dm0 dB Hm δ Nl kD δ) + Real.log (fp.Bst Dm0 dB Hm δ Nl kD δ) + Real.log (max 2 Nl) + Real.log ↑(fp.Q0bd dB) + 1 → 0 ≤ Λ

Step hΛ0 of leaf_estimate, over the part of its context that it uses.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.leaf_estimate_hE0 (κ : LocalKernelClass) (c₀ : ℕ) (A : ActiveSetup κ c₀) (η₀ E : ℝ) : A.SubRootProps η₀ E → 0 < dyadicGridLength A.G A.R.1 → 0 ≤ E

Step hE0 of leaf_estimate, over the part of its context that it uses.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.leaf_estimate_hT0 (κ : LocalKernelClass) (c₀ cc : ℕ) (A : ActiveSetup κ c₀) (bf : A.BasicFamilies) (k : ℕ) (E : ℝ) (p : Fin 3) (AD : bf.AttemptData p) (ρ : ℝ) : 0 < ρ → have fp := AD.fp; ∀ (S : ModeSchedule), 1 ≤ S.K → ∀ (Vl0 : ℝ), 0 < dyadicGridLength A.G A.R.1 → 0 ≤ Vl0 → 1 ≤ ↑fp.P → 0 ≤ E → have TT := TsideF A fp.P S.K (A.uslot p) (2 ^ A.famFuel) (2 * A.famFuel + 2) 1 E cc (↑k) (fun (x : Fin 4) => Vl0) ρ; TT = TsideF A fp.P S.K (A.uslot p) (2 ^ A.famFuel) (2 * A.famFuel + 2) 1 E cc (↑k) (fun (x : Fin 4) => Vl0) ρ → 0 ≤ TT

Step hT0 of leaf_estimate, over the part of its context that it uses.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.leaf_estimate_h3pow (S : ModeSchedule) : 0 < S.Dstar → 1 ≤ S.Dstar → √(4 * S.Dstar ^ 2 * 1) = 2 * S.Dstar → √S.Dstar ^ 2 = S.Dstar → 1 ≤ √S.Dstar → (S.Dstar * (√S.Dstar * √(4 * S.Dstar ^ 2 * 1) + 1)) ^ 4 ≤ 81 * S.Dstar ^ 10

Step h3pow of leaf_estimate, over the part of its context that it uses.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.leaf_estimate_hQe0 (κ : LocalKernelClass) (S : ModeSchedule) : 2 ≤ S.Dstar → ∀ (U : ℝ), 16 ≤ U → ∀ (ε : ℝ), 0 < ε → have Iw := ⌊Real.logb 2 (S.Dstar ^ 250)⌋₊; have ι := (S.Dstar ^ 100)⁻¹ * S.Dstar ^ 10; have Qe := 16 * fourErrC κ 3 * ι + K1c * (2 * fourKC κ 3 * 12 ^ 4 * ε * U ^ 3 * S.Dstar ^ 4) + 4 * (81 * threeErrC κ 3 1 * ι * U + K1c * (8 * entryCU κ 3 1 * 2 ^ (1 + 4) * 12 ^ 3 * ε * U ^ 3 * (S.Dstar ^ 3 * (↑Iw + 1)))); Qe = 16 * fourErrC κ 3 * ι + K1c * (2 * fourKC κ 3 * 12 ^ 4 * ε * U ^ 3 * S.Dstar ^ 4) + 4 * (81 * threeErrC κ 3 1 * ι * U + K1c * (8 * entryCU κ 3 1 * 2 ^ (1 + 4) * 12 ^ 3 * ε * U ^ 3 * (S.Dstar ^ 3 * (↑Iw + 1)))) → 0 ≤ Qe

Step hQe0 of leaf_estimate, over the part of its context that it uses.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.leaf_estimate_hCjg1 (κ : LocalKernelClass) (c₀ cc : ℕ) (A : ActiveSetup κ c₀) (k : ℕ) : have Cjg := (↑(2 * A.famFuel + 2) + 1) ^ 2 * Real.exp (2 * (1024 * (↑cc + 1) * (1024 * (↑cc + 1) + ↑cc + 7) * (1 + Real.log (2 * ↑k)) ^ 2)); Cjg = (↑(2 * A.famFuel + 2) + 1) ^ 2 * Real.exp (2 * (1024 * (↑cc + 1) * (1024 * (↑cc + 1) + ↑cc + 7) * (1 + Real.log (2 * ↑k)) ^ 2)) → 1 ≤ Cjg

Step hCjg1 of leaf_estimate, over the part of its context that it uses.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.leaf_estimate_hΓa0 (κ : LocalKernelClass) (c₀ cc : ℕ) (A : ActiveSetup κ c₀) (k : ℕ) (E : ℝ) (S : ModeSchedule) (Vl0 : ℝ) : have Nb := Nat.log 2 S.K + 1; 0 ≤ Vl0 → have Os := FamParams.SideLeafM.nOs (2 ^ A.famFuel) (2 * A.famFuel + 2); have Cjg := (↑(2 * A.famFuel + 2) + 1) ^ 2 * Real.exp (2 * (1024 * (↑cc + 1) * (1024 * (↑cc + 1) + ↑cc + 7) * (1 + Real.log (2 * ↑k)) ^ 2)); have Γa := fun (x : Fin 4) => ↑Os.card * (↑Nb * (2 * FamParams.capV A cc ↑k + 16 * (Cjg * FamParams.SideInput.sideB0 A cc (↑k) Vl0) + 16 * (↑Nb * (Cjg * (↑Nb * FamParams.capV A cc ↑k)))) + FamParams.SideInput.sideB0 A cc (↑k) Vl0) / dyadicGridLength A.G A.R.1; have G0e := Real.exp ((4096 * (↑cc + 1) * (1024 * (↑cc + 1) + ↑cc + 7) + ↑cc ^ 2 + 3) * (1 + Real.log (2 * ↑k)) ^ 2); 1 ≤ G0e → have W := G0e + Vl0 + E + 1; 1 ≤ W → have n := ↑Nb; (Γa = fun (x : Fin 4) => ↑Os.card * (n * (2 * FamParams.capV A cc ↑k + 16 * (Cjg * FamParams.SideInput.sideB0 A cc (↑k) Vl0) + 16 * (n * (Cjg * (n * FamParams.capV A cc ↑k)))) + FamParams.SideInput.sideB0 A cc (↑k) Vl0) / dyadicGridLength A.G A.R.1) → have P3 := n ^ 3 * Cjg; P3 = n ^ 3 * Cjg → 1 ≤ P3 → n ≤ P3 → n * Cjg ≤ P3 → 0 ≤ ↑Os.card → FamParams.capV A cc ↑k = G0e * (4 * dyadicGridLength A.G A.R.1) → FamParams.SideInput.sideB0 A cc (↑k) Vl0 = 2 * ((20 * G0e + 32) * dyadicGridLength A.G A.R.1) + 2 * (Vl0 * dyadicGridLength A.G A.R.1) → dyadicGridLength A.G A.R.1 ≠ 0 → G0e ≤ W → 40 * G0e + 64 + 2 * Vl0 ≤ 106 * W → Γa 0 ≤ 1874 * ↑Os.card * P3 * W

Step hΓa0 of leaf_estimate, over the part of its context that it uses.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.leaf_estimate_hΓb0 (κ : LocalKernelClass) (c₀ cc : ℕ) (A : ActiveSetup κ c₀) (k : ℕ) (E : ℝ) (S : ModeSchedule) (Vl0 : ℝ) : have Nb := Nat.log 2 S.K + 1; have Os := FamParams.SideLeafM.nOs (2 ^ A.famFuel) (2 * A.famFuel + 2); have Cjg := (↑(2 * A.famFuel + 2) + 1) ^ 2 * Real.exp (2 * (1024 * (↑cc + 1) * (1024 * (↑cc + 1) + ↑cc + 7) * (1 + Real.log (2 * ↑k)) ^ 2)); have Γb := fun (x : Fin 4) => ↑Os.card * (↑Nb * FamParams.capV A cc ↑k + FamParams.SideInput.sideB0 A cc (↑k) Vl0) / dyadicGridLength A.G A.R.1; have G0e := Real.exp ((4096 * (↑cc + 1) * (1024 * (↑cc + 1) + ↑cc + 7) + ↑cc ^ 2 + 3) * (1 + Real.log (2 * ↑k)) ^ 2); 1 ≤ G0e → have W := G0e + Vl0 + E + 1; 1 ≤ W → have n := ↑Nb; (Γb = fun (x : Fin 4) => ↑Os.card * (n * FamParams.capV A cc ↑k + FamParams.SideInput.sideB0 A cc (↑k) Vl0) / dyadicGridLength A.G A.R.1) → have P3 := n ^ 3 * Cjg; 1 ≤ P3 → n ≤ P3 → 0 ≤ ↑Os.card → FamParams.capV A cc ↑k = G0e * (4 * dyadicGridLength A.G A.R.1) → FamParams.SideInput.sideB0 A cc (↑k) Vl0 = 2 * ((20 * G0e + 32) * dyadicGridLength A.G A.R.1) + 2 * (Vl0 * dyadicGridLength A.G A.R.1) → dyadicGridLength A.G A.R.1 ≠ 0 → G0e ≤ W → 40 * G0e + 64 + 2 * Vl0 ≤ 106 * W → Γb 0 ≤ 110 * ↑Os.card * P3 * W

Step hΓb0 of leaf_estimate, over the part of its context that it uses.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.leaf_estimate_hΓa00 (κ : LocalKernelClass) (c₀ cc : ℕ) (A : ActiveSetup κ c₀) (k : ℕ) (S : ModeSchedule) (Vl0 : ℝ) : have Nb := Nat.log 2 S.K + 1; 0 < dyadicGridLength A.G A.R.1 → 0 ≤ Vl0 → have Os := FamParams.SideLeafM.nOs (2 ^ A.famFuel) (2 * A.famFuel + 2); have Cjg := (↑(2 * A.famFuel + 2) + 1) ^ 2 * Real.exp (2 * (1024 * (↑cc + 1) * (1024 * (↑cc + 1) + ↑cc + 7) * (1 + Real.log (2 * ↑k)) ^ 2)); have Γa := fun (x : Fin 4) => ↑Os.card * (↑Nb * (2 * FamParams.capV A cc ↑k + 16 * (Cjg * FamParams.SideInput.sideB0 A cc (↑k) Vl0) + 16 * (↑Nb * (Cjg * (↑Nb * FamParams.capV A cc ↑k)))) + FamParams.SideInput.sideB0 A cc (↑k) Vl0) / dyadicGridLength A.G A.R.1; have G0e := Real.exp ((4096 * (↑cc + 1) * (1024 * (↑cc + 1) + ↑cc + 7) + ↑cc ^ 2 + 3) * (1 + Real.log (2 * ↑k)) ^ 2); have n := ↑Nb; (Γa = fun (x : Fin 4) => ↑Os.card * (n * (2 * FamParams.capV A cc ↑k + 16 * (Cjg * FamParams.SideInput.sideB0 A cc (↑k) Vl0) + 16 * (n * (Cjg * (n * FamParams.capV A cc ↑k)))) + FamParams.SideInput.sideB0 A cc (↑k) Vl0) / dyadicGridLength A.G A.R.1) → 0 ≤ ↑Os.card → FamParams.capV A cc ↑k = G0e * (4 * dyadicGridLength A.G A.R.1) → FamParams.SideInput.sideB0 A cc (↑k) Vl0 = 2 * ((20 * G0e + 32) * dyadicGridLength A.G A.R.1) + 2 * (Vl0 * dyadicGridLength A.G A.R.1) → 0 ≤ Γa 0

Step hΓa00 of leaf_estimate, over the part of its context that it uses.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.leaf_estimate_hΓb00 (κ : LocalKernelClass) (c₀ cc : ℕ) (A : ActiveSetup κ c₀) (k : ℕ) (S : ModeSchedule) (Vl0 : ℝ) : have Nb := Nat.log 2 S.K + 1; 0 < dyadicGridLength A.G A.R.1 → 0 ≤ Vl0 → have Os := FamParams.SideLeafM.nOs (2 ^ A.famFuel) (2 * A.famFuel + 2); have Γb := fun (x : Fin 4) => ↑Os.card * (↑Nb * FamParams.capV A cc ↑k + FamParams.SideInput.sideB0 A cc (↑k) Vl0) / dyadicGridLength A.G A.R.1; have G0e := Real.exp ((4096 * (↑cc + 1) * (1024 * (↑cc + 1) + ↑cc + 7) + ↑cc ^ 2 + 3) * (1 + Real.log (2 * ↑k)) ^ 2); have n := ↑Nb; (Γb = fun (x : Fin 4) => ↑Os.card * (n * FamParams.capV A cc ↑k + FamParams.SideInput.sideB0 A cc (↑k) Vl0) / dyadicGridLength A.G A.R.1) → 0 ≤ ↑Os.card → FamParams.capV A cc ↑k = G0e * (4 * dyadicGridLength A.G A.R.1) → FamParams.SideInput.sideB0 A cc (↑k) Vl0 = 2 * ((20 * G0e + 32) * dyadicGridLength A.G A.R.1) + 2 * (Vl0 * dyadicGridLength A.G A.R.1) → 0 ≤ Γb 0

Step hΓb00 of leaf_estimate, over the part of its context that it uses.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.leaf_estimate_hΓU00 (κ : LocalKernelClass) (c₀ : ℕ) (A : ActiveSetup κ c₀) (E : ℝ) : 0 < dyadicGridLength A.G A.R.1 → have Os := FamParams.SideLeafM.nOs (2 ^ A.famFuel) (2 * A.famFuel + 2); have ΓU := ↑Os.card * (2 * (4 * E * dyadicGridLength A.G A.R.1)) / dyadicGridLength A.G A.R.1; ΓU = ↑Os.card * (2 * (4 * E * dyadicGridLength A.G A.R.1)) / dyadicGridLength A.G A.R.1 → 0 ≤ E → 0 ≤ ↑Os.card → 0 ≤ ΓU

Step hΓU00 of leaf_estimate, over the part of its context that it uses.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.leaf_estimate_hprin (κ : LocalKernelClass) (c₀ Dm0 : ℕ) (A : ActiveSetup κ c₀) (bf : A.BasicFamilies) (p : Fin 3) (AD : bf.AttemptData p) (d : bf.Vtx) (s : ℕ) (δ ρ kD : ℝ) : 0 < δ → δ ≤ 1 / 8 → 0 < ρ → let fp := AD.fp; have dB := A.dBnd; 8 * ↑dB * δ ≤ 1 → let Nl := AD.n (fp.Lc + 5); ∀ (hNl0 : 0 ≤ Nl), have Hm := max (max A.Hsrc (Real.exp ↑dB)) (max (5832 * max A.H padW ^ 4) (↑dB * (bumpConst * 8 ^ 32 * (2 / δ)))); 1 ≤ Hm → (∀ (w : bf.Vtx), (bf.vtag w).dim ≤ dB) → (∀ (w : bf.Vtx) (a c : Fin (bf.vtag w).dim), ↑(rationalHeight ((bf.vtag w).C a c)) ≤ fp.Hed) → ∀ (S : ModeSchedule), S.dmax = 2 * dB + 2 → ↑S.Q0 * 2 ^ (fp.Kstar Dm0 dB Hm δ Nl kD δ + 1) ≤ S.Bstar → ∀ (hK1 : 1 ≤ S.K), have Lf := leafAt A.famFuel fp.Lc (A.basicSlot p) s; have ks := Lf.k; have S0 := {I ∈ AD.Tc | ¬∃ c ∈ fp.failRoots, dyadicGridCell A.G I.1 I.2 ⊆ dyadicGridCell A.G c.1 c.2}; have gs := fun (I : ℤ × ℤ) => fp.groupsAt I ks; have gset := S0.biUnion gs; ∀ (hlenMc : ∀ (l : Fin 4), (AD.cat l).length ≤ fp.Mc), have mbs := fun (l : Fin 4) => MainBudget.ofCounts bf fp.Mc (AD.cat l) ⋯ l ⋯ ⋯ hNl0 ⋯; ∀ (Ms : Fin 4 → bf.Grp → ModeSystem A.G (Fintype.card (bf.Lab ⊕ Fin fp.Mc))), S.Dstar = fp.modeStarG Dm0 dB Hm δ Nl kD δ → (∀ (l : Fin 4), ∀ G ∈ gset, (∀ (q : (Ms l G).Key), (Ms l G).dvOf q + (Ms l G).zc.dim ≤ 2 * dB + 2) ∧ (Ms l G).Λ ≤ S.Dstar ∧ gaugeSqNorm (Ms l G).zc.dim (Ms l G).δc ≤ S.Dstar ∧ 2 * gaugeTail (Ms l G).zc.dim (Ms l G).δc / 2 ^ fp.Kstar Dm0 dB Hm δ Nl kD δ * S.Dstar ^ 300 ≤ 1 ∧ (∀ (m : (Ms l G).Md), S.Dstar⁻¹ ≤ (Ms l G).L.εM m) ∧ (∀ (V : ℤ × ℤ), ↑((Ms l G).alive V).card ≤ S.Dstar) ∧ ∀ (V : ℤ × ℤ), ↑(Finset.image (Ms l G).keyOf ((Ms l G).alive V)).card ≤ Nl) → ∀ (hA6 : 6 ≤ S.A0), have qG := fun (G : bf.Grp) => clearInt (bf.vtag (bf.grpCenter d G)).C; (∀ (G : bf.Grp), 1 ≤ qG G ∧ qG G ≤ S.Q0) → ∀ (c : (l : Fin 4) → (G : ↥gset) → ℤ → ℤ × ℤ → (Ms l ↑G).Md → ℂ), have cf := fun (l : Fin 4) (G : bf.Grp) => if hG : G ∈ gset then c l ⟨G, hG⟩ else fun (x : ℤ) (x_1 : ℤ × ℤ) (x_2 : (Ms l G).Md) => 0; let D₀ := { cat := AD.cat, mbs := mbs, Lf := Lf, u := A.uslot p, S := S, hA := hA6, SP := S.sideParams (1 / 1024), hK := hK1, n := Fintype.card (bf.Lab ⊕ Fin fp.Mc), Ms := Ms, c := cf }; ∀ (hcat : Fin 4 → List (CatCol bf.Vtx)) (hmbb : ∀ (l : Fin 4), ∀ e ∈ AD.cat l ++ hcat l, e.birth ∈ A.cells) (hmbT : ∀ (l : Fin 4) (y : ℝ), 8 * A.colBudget + ↑(bf.tmplPath (AD.cat l ++ hcat l) y) ≤ 8 * A.colBudget + (1 + ↑AD.Mp) * Nl), have mb' := fun (l : Fin 4) => { hb := ⋯, B := 8 * A.colBudget + (1 + ↑AD.Mp) * Nl, hTp := ⋯ }; have D := D₀.appendCat hcat mb'; (∀ (l : Fin 4), ∀ G ∈ gset, (Ms l G).zc = bf.vtag (bf.grpCenter d G)) → (∀ (l : Fin 4), ∀ G ∈ gset, (Ms l G).δc = δ ∧ (Ms l G).cl = slotCoeff l ∧ ∀ (i : Fin (Ms l G).zc.dim), (Ms l G).ρ i ∈ Set.Icc 0 1) → 1 ≤ dB → ∀ G ∈ gset, (D.withQ0 (qG G)).PrinOK G δ fp.Hed (fp.Kstar Dm0 dB Hm δ Nl kD δ) (fp.Kstar Dm0 dB Hm δ Nl kD δ)

Step hprin of leaf_estimate, over the part of its context that it uses.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.leaf_estimate_hUD (κ : LocalKernelClass) (c₀ cc : ℕ) : 1 ≤ cc → ∀ (Dm0 : ℕ) (A : ActiveSetup κ c₀) (bf : A.BasicFamilies) (p : Fin 3) (AD : bf.AttemptData p) (d : bf.Vtx) (s : ℕ) (δ kD : ℝ), let fp := AD.fp; have dB := A.dBnd; let Nl := AD.n (fp.Lc + 5); 2 ≤ A.colBudget → ∀ (hNl0 : 0 ≤ Nl), have Hm := max (max A.Hsrc (Real.exp ↑dB)) (max (5832 * max A.H padW ^ 4) (↑dB * (bumpConst * 8 ^ 32 * (2 / δ)))); ∀ (S : ModeSchedule) (hK1 : 1 ≤ S.K), have Lf := leafAt A.famFuel fp.Lc (A.basicSlot p) s; have ks := Lf.k; have S0 := {I ∈ AD.Tc | ¬∃ c ∈ fp.failRoots, dyadicGridCell A.G I.1 I.2 ⊆ dyadicGridCell A.G c.1 c.2}; have gs := fun (I : ℤ × ℤ) => fp.groupsAt I ks; have gset := S0.biUnion gs; ∀ (hlenMc : ∀ (l : Fin 4), (AD.cat l).length ≤ fp.Mc), have mbs := fun (l : Fin 4) => MainBudget.ofCounts bf fp.Mc (AD.cat l) ⋯ l ⋯ ⋯ hNl0 ⋯; ∀ (Ms : Fin 4 → bf.Grp → ModeSystem A.G (Fintype.card (bf.Lab ⊕ Fin fp.Mc))) (L : (l : Fin 4) → (G : bf.Grp) → LiftData (bf.Lab ⊕ Fin fp.Mc) (Ms l G).Md), (∀ (l : Fin 4), ∀ G ∈ gset, fp.ModeExports l (AD.cat l) G (Lf.role l) d Dm0 dB Hm δ δ Nl (Ms l G) (L l G)) → (∀ (l : Fin 4), ∀ G ∈ gset, (∀ (q : (Ms l G).Key), (Ms l G).dvOf q + (Ms l G).zc.dim ≤ 2 * dB + 2) ∧ (Ms l G).Λ ≤ S.Dstar ∧ gaugeSqNorm (Ms l G).zc.dim (Ms l G).δc ≤ S.Dstar ∧ 2 * gaugeTail (Ms l G).zc.dim (Ms l G).δc / 2 ^ fp.Kstar Dm0 dB Hm δ Nl kD δ * S.Dstar ^ 300 ≤ 1 ∧ (∀ (m : (Ms l G).Md), S.Dstar⁻¹ ≤ (Ms l G).L.εM m) ∧ (∀ (V : ℤ × ℤ), ↑((Ms l G).alive V).card ≤ S.Dstar) ∧ ∀ (V : ℤ × ℤ), ↑(Finset.image (Ms l G).keyOf ((Ms l G).alive V)).card ≤ Nl) → ∀ (hA6 : 6 ≤ S.A0), have qG := fun (G : bf.Grp) => clearInt (bf.vtag (bf.grpCenter d G)).C; ∀ (U : ℝ), 2 * (A.colBudget + 2) * S.Dstar ^ 2 ≤ U → 0 < S.Dstar → 1 ≤ S.Dstar → ∀ (gsc : Fin 4 → ↥gset → ℤ), (∀ (l : Fin 4) (G : ↥gset), fp.MainLiftExports l (AD.cat l) (↑G) (Lf.role l) d Dm0 dB Hm (gsc l G) (L l ↑G) (Ms l ↑G).wave (Ms l ↑G).cellOf) → ∀ (c : (l : Fin 4) → (G : ↥gset) → ℤ → ℤ × ℤ → (Ms l ↑G).Md → ℂ), (∀ (l : Fin 4) (G : ↥gset), ∀ b ∈ Finset.image (fun (β : ℕ) => A.R.1 + ↑(S.K * β)) (Finset.range (A.treeDepth + 1)), ∀ J ∈ fp.retainedV (↑G) b S.K, ∑ m ∈ (Ms l ↑G).alive (ancAt A.G J (b - 4 * ↑S.K)), ‖c l G b J m‖ ^ 2 ≤ 4 * S.Dstar ^ 2 * 1) → ∀ (Cut : Fin 4 → Finset (ℤ × ℤ)), have cf := fun (l : Fin 4) (G : bf.Grp) => if hG : G ∈ gset then c l ⟨G, hG⟩ else fun (x : ℤ) (x_1 : ℤ × ℤ) (x_2 : (Ms l G).Md) => 0; let D₀ := { cat := AD.cat, mbs := mbs, Lf := Lf, u := A.uslot p, S := S, hA := hA6, SP := S.sideParams (1 / 1024), hK := hK1, n := Fintype.card (bf.Lab ⊕ Fin fp.Mc), Ms := Ms, c := cf }; ∀ (hcat : Fin 4 → List (CatCol bf.Vtx)) (hmbb : ∀ (l : Fin 4), ∀ e ∈ AD.cat l ++ hcat l, e.birth ∈ A.cells) (hmbT : ∀ (l : Fin 4) (y : ℝ), 8 * A.colBudget + ↑(bf.tmplPath (AD.cat l ++ hcat l) y) ≤ 8 * A.colBudget + (1 + ↑AD.Mp) * Nl), have mb' := fun (l : Fin 4) => { hb := ⋯, B := 8 * A.colBudget + (1 + ↑AD.Mp) * Nl, hTp := ⋯ }; let D := D₀.appendCat hcat mb'; have S1 := {I ∈ S0 | ∀ (j : Fin 4), ∀ e ∈ Cut j, ¬dyadicGridCell A.G I.1 I.2 ⊆ dyadicGridCell A.G e.1 e.2}; S1 ⊆ S0 → S1 ⊆ A.cells → (∀ (I : ℤ × ℤ), ⋯) → ⋯ → ⋯

Step hUD of leaf_estimate, over the part of its context that it uses.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.leaf_estimate_hΞ (x : ℝ) : 2 ≤ x → 8 * x ≤ x ^ 1000

Step hΞ of leaf_estimate, over the part of its context that it uses.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.leaf_estimate_hcoreE (κ : LocalKernelClass) (c₀ cc : ℕ) : 1 ≤ cc → ∀ (Dm0 : ℕ) (A : ActiveSetup κ c₀) (bf : A.BasicFamilies), A.cells.Nonempty → ∀ (p : Fin 3) (AD : bf.AttemptData p) (d : bf.Vtx) (s : ℕ) (δ kD : ℝ), let fp := AD.fp; have dB := A.dBnd; let Nl := AD.n (fp.Lc + 5); ∀ (hNl0 : 0 ≤ Nl), have Hm := max (max A.Hsrc (Real.exp ↑dB)) (max (5832 * max A.H padW ^ 4) (↑dB * (bumpConst * 8 ^ 32 * (2 / δ)))); ∀ (S : ModeSchedule), 2 ≤ S.Dstar → ∀ (hK1 : 1 ≤ S.K), have Lf := leafAt A.famFuel fp.Lc (A.basicSlot p) s; have ks := Lf.k; have S0 := {I ∈ AD.Tc | ¬∃ c ∈ fp.failRoots, dyadicGridCell A.G I.1 I.2 ⊆ dyadicGridCell A.G c.1 c.2}; have gs := fun (I : ℤ × ℤ) => fp.groupsAt I ks; have gset := S0.biUnion gs; ∀ (hlenMc : ∀ (l : Fin 4), (AD.cat l).length ≤ fp.Mc), have mbs := fun (l : Fin 4) => MainBudget.ofCounts bf fp.Mc (AD.cat l) ⋯ l ⋯ ⋯ hNl0 ⋯; ∀ (Ms : Fin 4 → bf.Grp → ModeSystem A.G (Fintype.card (bf.Lab ⊕ Fin fp.Mc))), (∀ (l : Fin 4), ∀ G ∈ gset, (∀ (q : (Ms l G).Key), (Ms l G).dvOf q + (Ms l G).zc.dim ≤ 2 * dB + 2) ∧ (Ms l G).Λ ≤ S.Dstar ∧ gaugeSqNorm (Ms l G).zc.dim (Ms l G).δc ≤ S.Dstar ∧ 2 * gaugeTail (Ms l G).zc.dim (Ms l G).δc / 2 ^ fp.Kstar Dm0 dB Hm δ Nl kD δ * S.Dstar ^ 300 ≤ 1 ∧ (∀ (m : (Ms l G).Md), S.Dstar⁻¹ ≤ (Ms l G).L.εM m) ∧ (∀ (V : ℤ × ℤ), ↑((Ms l G).alive V).card ≤ S.Dstar) ∧ ∀ (V : ℤ × ℤ), ↑(Finset.image (Ms l G).keyOf ((Ms l G).alive V)).card ≤ Nl) → ∀ (hA6 : 6 ≤ S.A0), have qG := fun (G : bf.Grp) => clearInt (bf.vtag (bf.grpCenter d G)).C; ∀ (U : ℝ), 1 ≤ S.Dstar → 16 ≤ U → ∀ (ε : ℝ) (c : (l : Fin 4) → (G : ↥gset) → ℤ → ℤ × ℤ → (Ms l ↑G).Md → ℂ), (∀ (l : Fin 4) (G : ↥gset), ∀ b ∈ Finset.image (fun (β : ℕ) => A.R.1 + ↑(S.K * β)) (Finset.range (A.treeDepth + 1)), ∀ J ∈ fp.retainedV (↑G) b S.K, ∑ m ∈ (Ms l ↑G).alive (ancAt A.G J (b - 4 * ↑S.K)), ‖c l G b J m‖ ^ 2 ≤ 4 * S.Dstar ^ 2 * 1) → ∀ (Cut : Fin 4 → Finset (ℤ × ℤ)), have cf := fun (l : Fin 4) (G : bf.Grp) => if hG : G ∈ gset then c l ⟨G, hG⟩ else fun (x : ℤ) (x_1 : ℤ × ℤ) (x_2 : (Ms l G).Md) => 0; let D₀ := { cat := AD.cat, mbs := mbs, Lf := Lf, u := A.uslot p, S := S, hA := hA6, SP := S.sideParams (1 / 1024), hK := hK1, n := Fintype.card (bf.Lab ⊕ Fin fp.Mc), Ms := Ms, c := cf }; ∀ (hcat : Fin 4 → List (CatCol bf.Vtx)) (hmbb : ∀ (l : Fin 4), ∀ e ∈ AD.cat l ++ hcat l, e.birth ∈ A.cells) (hmbT : ∀ (l : Fin 4) (y : ℝ), 8 * A.colBudget + ↑(bf.tmplPath (AD.cat l ++ hcat l) y) ≤ 8 * A.colBudget + (1 + ↑AD.Mp) * Nl), have mb' := fun (l : Fin 4) => { hb := ⋯, B := 8 * A.colBudget + (1 + ↑AD.Mp) * Nl, hTp := ⋯ }; let D := D₀.appendCat hcat mb'; have S1 := {I ∈ S0 | ∀ (j : Fin 4), ∀ e ∈ Cut j, ¬dyadicGridCell A.G I.1 I.2 ⊆ dyadicGridCell A.G e.1 e.2}; S1 ⊆ S0 → S1 ⊆ A.cells → (∀ I ∈ A.cells, A.blkStart S.K I.1 ∈ Finset.image (fun (β : ℕ) => A.R.1 + ↑(S.K * β)) (Finset.range (A.treeDepth + 1))) → (∀ (j : Fin 4) (G : ↥gset), ⋯ = c j G) → have Iw := ⌊Real.logb 2 (S.Dstar ^ 250)⌋₊; ∀ (C C₂ : Finset (ℤ × ℤ)), have S₂ := ⋯; ⋯

Step hcoreE of leaf_estimate, over the part of its context that it uses.