/-
  第1112コマ — 尾のチャンク 3：段 17〜28（12 個・葉 4480）。`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 tailG3 : List ((ℕ × ℕ × ℕ × ℕ) × ℕ × ℕ) :=
  [(((360, 20, 106415, 14487098637500631232003344738223869016106271257867172219), 184, 1)),
   (((320, 21, 88355, 1392231421069045819745655374121998345386612794196667674731), 184, 1)),
   (((400, 21, 138050, 85106862483860060427019609816730879498163862044664020024627), 192, 1)),
   (((360, 22, 117221, 9154474839853982986381286028956172346357798586703668719264409), 200, 1)),
   (((400, 22, 144726, 723059767349501034918933277619014689410484129253710790680553423), 200, 1)),
   (((360, 23, 122622, 8624544165493126099885169724523280898469103988564426846969538635), 208, 1)),
   (((400, 23, 151386, 523964926235567468772719847329737217671838958374182484157602011341), 208, 1)),
   (((360, 24, 128022, 6783491132475640037556757460865654909248598369586706837891798215195), 216, 1)),
   (((400, 24, 158052, 377895669718345174791421159114682797235884093070284230533683526247335), 224, 1)),
   (((360, 25, 133428, 5338504802160289924494036595609008973709451310683096976998983829725049), 224, 1)),
   (((400, 25, 164727, 272629335883310790150050844058622712309755658179041077797323015637875747), 232, 1)),
   (((360, 26, 138828, 4206846728482777640654415799737085326861195079515526996182883283026297683), 232, 1))]

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

theorem tailG3_num : 3469481382592216008602529943488395056054404076720217939660329864599283822337523682324250624 ≤ totLoP (10 ^ 100) tailG3 := by
  decide +kernel

theorem tailG3_lower : (3469481382592216008602529943488395056054404076720217939660329864599283822337523682324250624 : ℚ) / 10 ^ 100 ≤ sumWin (tailG3.map Prod.fst) := by
  have h := totLoP_le (10 ^ 100) (by norm_num) tailG3 tailG3_ok
  have hc : ((10 ^ 100 : ℕ) : ℚ) = 10 ^ 100 := by norm_num
  rw [hc] at h
  refine le_trans ?_ h
  gcongr
  exact_mod_cast tailG3_num

end Shiori1112