/-
  第1112コマ — 尾のチャンク 4：段 29〜38（10 個・葉 4000）。`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 tailG4 : List ((ℕ × ℕ × ℕ × ℕ) × ℕ × ℕ) :=
  [(((400, 26, 171391, 196757416051559516487773301279436234237141671464227932769987452097334437671), 240, 1)),
   (((400, 26, 171391, 3319123689419327725198645826366780336138745299520434744163388161825582607851), 240, 1)),
   (((400, 26, 171391, 9563856236154864142620390876541468539941952555632848366950189581282078948211), 240, 1)),
   (((400, 26, 171391, 22053321329625936977463880976890844947548367067857675612523792420195071628931), 240, 1)),
   (((400, 26, 171391, 47032251516568082647150861177589597762761196092307330103670998098021056990371), 240, 1)),
   (((400, 26, 171391, 96990111890452373986524821578987103393186854141206639085965409453673027713251), 240, 1)),
   (((400, 26, 171391, 196905832638220956665272742381782114654038170239005257050554232164976969159011), 240, 1)),
   (((400, 26, 171391, 396737274133758122022768583987372137175740802434602492979731877587584852050531), 240, 1)),
   (((400, 26, 171391, 796400157124832452737760267198552182219146066825796964838087168432800617833571), 240, 1)),
   (((400, 26, 171391, 1595725923106981114167743633620912272305956595608185908554797750123232149399651), 240, 1))]

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

theorem tailG4_num : 11054434605836150429163428041334209138782164345005523248237601395277942978288098580889600 ≤ totLoP (10 ^ 100) tailG4 := by
  decide +kernel

theorem tailG4_lower : (11054434605836150429163428041334209138782164345005523248237601395277942978288098580889600 : ℚ) / 10 ^ 100 ≤ sumWin (tailG4.map Prod.fst) := by
  have h := totLoP_le (10 ^ 100) (by norm_num) tailG4 tailG4_ok
  have hc : ((10 ^ 100 : ℕ) : ℚ) = 10 ^ 100 := by norm_num
  rw [hc] at h
  refine le_trans ?_ h
  gcongr
  exact_mod_cast tailG4_num

end Shiori1112