/-
  第1112コマ — 尾のチャンク 2：段 7〜16（10 個・葉 2554）。`totLoP`（詰め込み個数 `cfP`）の kernel 評価。
  `erdos1112.py` が生成。sorry 0・native_decide 不使用。
-/
import Shioriproofs.Erdos1112p

namespace Shiori1112

open Shiori814

set_option maxRecDepth 100000

/-- 窓 `((p, q, r, a), W, d)`：詰め込み幅 `W`（`p^q < 2^W`）、深さ `d`。 -/
def tailG2 : List ((ℕ × ℕ × ℕ × ℕ) × ℕ × ℕ) :=
  [(((172, 16, 19363, 1150142759163591787290971055682296790491), 128, 1)),
   (((152, 17, 16078, 39003653735619540138161174219059141187941), 136, 1)),
   (((190, 17, 25129, 1607419980562407035214283413237333760127603), 144, 1)),
   (((240, 17, 40093, 71900578045456278641736670356294654939637969), 144, 1)),
   (((200, 18, 29509, 3822580404800494631307352588671061709550264401), 152, 1)),
   (((240, 18, 42494, 73337106075717533227873250718114584363595931993), 152, 1)),
   (((280, 18, 57839, 1908809472283331589035590905188240625976366403175), 160, 1)),
   (((360, 18, 95614, 32223779797367613639945610015466270812312093818501), 168, 1)),
   (((320, 19, 79814, 2701507654638741322839880421697182949729744918382107), 168, 1)),
   (((400, 19, 124715, 207014981487166860166671390073062850504845021681371415), 176, 1))]

theorem tailG2_ok : ∀ w ∈ tailG2, 1 ≤ w.1.1 ∧ 0 < w.1.2.2.2 := by decide

theorem tailG2_num : 226933485434956862296603917489669847369452280131312141724488924095633220682834155720006270976 ≤ totLoP (10 ^ 100) tailG2 := by
  decide +kernel

theorem tailG2_lower : (226933485434956862296603917489669847369452280131312141724488924095633220682834155720006270976 : ℚ) / 10 ^ 100 ≤ sumWin (tailG2.map Prod.fst) := by
  have h := totLoP_le (10 ^ 100) (by norm_num) tailG2 tailG2_ok
  have hc : ((10 ^ 100 : ℕ) : ℚ) = 10 ^ 100 := by norm_num
  rw [hc] at h
  refine le_trans ?_ h
  gcongr
  exact_mod_cast tailG2_num

end Shiori1112