/-
  第1112コマ — 頭の塊のチャンク 1（248 個・葉 4788）。`totK`（4 項の葉・深さ 1）の kernel 評価。
  `erdos1112.py` が生成。sorry 0・native_decide 不使用。
-/
import Shioriproofs.Erdos1112k

namespace Shiori1112

set_option maxRecDepth 100000

/-- 塊 `(P, m, j)`：集合 `1 + P·55^m + KF 55 S55 m`、深さ `j`。 -/
def piecesK1 : List (ℕ × ℕ × ℕ) :=
  [(0, 0, 0), (1, 0, 0),
   (2, 0, 0), (4, 0, 0),
   (5, 0, 0), (9, 0, 0),
   (10, 0, 0), (11, 0, 0),
   (14, 0, 0), (16, 0, 0),
   (17, 0, 0), (18, 0, 0),
   (21, 0, 0), (24, 0, 0),
   (30, 0, 0), (37, 0, 0),
   (39, 0, 0), (41, 0, 0),
   (42, 0, 0), (45, 0, 0),
   (47, 0, 0), (1, 1, 1),
   (2, 1, 1), (4, 1, 1),
   (5, 1, 1), (9, 1, 1),
   (10, 1, 1), (11, 1, 1),
   (14, 1, 1), (16, 1, 1),
   (17, 1, 1), (18, 1, 1),
   (21, 1, 1), (24, 1, 1),
   (30, 1, 1), (37, 1, 1),
   (39, 1, 1), (41, 1, 1),
   (42, 1, 1), (45, 1, 1),
   (47, 1, 1), (1, 2, 1),
   (2, 2, 1), (4, 2, 1),
   (5, 2, 1), (9, 2, 1),
   (10, 2, 1), (11, 2, 1),
   (14, 2, 1), (16, 2, 1),
   (17, 2, 1), (18, 2, 1),
   (21, 2, 1), (24, 2, 1),
   (30, 2, 1), (37, 2, 1),
   (39, 2, 1), (41, 2, 1),
   (42, 2, 1), (45, 2, 1),
   (47, 2, 1), (1, 3, 1),
   (2, 3, 1), (4, 3, 1),
   (5, 3, 1), (9, 3, 1),
   (10, 3, 1), (11, 3, 1),
   (14, 3, 1), (16, 3, 1),
   (17, 3, 1), (18, 3, 1),
   (21, 3, 1), (24, 3, 1),
   (30, 3, 1), (37, 3, 1),
   (39, 3, 1), (41, 3, 1),
   (42, 3, 1), (45, 3, 1),
   (47, 3, 1), (1, 4, 1),
   (2, 4, 1), (4, 4, 1),
   (5, 4, 1), (9, 4, 1),
   (10, 4, 1), (11, 4, 1),
   (14, 4, 1), (16, 4, 1),
   (17, 4, 1), (18, 4, 1),
   (21, 4, 1), (24, 4, 1),
   (30, 4, 1), (37, 4, 1),
   (39, 4, 1), (41, 4, 1),
   (42, 4, 1), (45, 4, 1),
   (47, 4, 1), (1, 5, 1),
   (2, 5, 1), (4, 5, 1),
   (5, 5, 1), (9, 5, 1),
   (10, 5, 1), (11, 5, 1),
   (14, 5, 1), (16, 5, 1),
   (17, 5, 1), (18, 5, 1),
   (21, 5, 1), (24, 5, 1),
   (30, 5, 1), (37, 5, 1),
   (39, 5, 1), (41, 5, 1),
   (42, 5, 1), (45, 5, 1),
   (47, 5, 1), (1, 6, 1),
   (2, 6, 1), (4, 6, 1),
   (5, 6, 1), (9, 6, 1),
   (10, 6, 1), (11, 6, 1),
   (14, 6, 1), (16, 6, 1),
   (17, 6, 1), (18, 6, 1),
   (21, 6, 1), (24, 6, 1),
   (30, 6, 1), (37, 6, 1),
   (39, 6, 1), (41, 6, 1),
   (42, 6, 1), (45, 6, 1),
   (47, 6, 1), (1, 7, 1),
   (2, 7, 1), (4, 7, 1),
   (5, 7, 1), (9, 7, 1),
   (10, 7, 1), (11, 7, 1),
   (14, 7, 1), (16, 7, 1),
   (17, 7, 1), (18, 7, 1),
   (21, 7, 1), (24, 7, 1),
   (30, 7, 1), (37, 7, 1),
   (39, 7, 1), (41, 7, 1),
   (42, 7, 1), (45, 7, 1),
   (47, 7, 1), (1, 8, 1),
   (2, 8, 1), (4, 8, 1),
   (5, 8, 1), (9, 8, 1),
   (10, 8, 1), (11, 8, 1),
   (14, 8, 1), (16, 8, 1),
   (17, 8, 1), (18, 8, 1),
   (21, 8, 1), (24, 8, 1),
   (30, 8, 1), (37, 8, 1),
   (39, 8, 1), (41, 8, 1),
   (42, 8, 1), (45, 8, 1),
   (47, 8, 1), (1, 9, 1),
   (2, 9, 1), (4, 9, 1),
   (5, 9, 1), (9, 9, 1),
   (10, 9, 1), (11, 9, 1),
   (14, 9, 1), (16, 9, 1),
   (17, 9, 1), (18, 9, 1),
   (21, 9, 1), (24, 9, 1),
   (30, 9, 1), (37, 9, 1),
   (39, 9, 1), (41, 9, 1),
   (42, 9, 1), (45, 9, 1),
   (47, 9, 1), (1, 10, 1),
   (2, 10, 1), (4, 10, 1),
   (5, 10, 1), (9, 10, 1),
   (10, 10, 1), (11, 10, 1),
   (14, 10, 1), (16, 10, 1),
   (17, 10, 1), (18, 10, 1),
   (21, 10, 1), (24, 10, 1),
   (30, 10, 1), (37, 10, 1),
   (39, 10, 1), (41, 10, 1),
   (42, 10, 1), (45, 10, 1),
   (47, 10, 1), (1, 11, 1),
   (2, 11, 1), (4, 11, 1),
   (5, 11, 1), (9, 11, 1),
   (10, 11, 1), (11, 11, 1),
   (14, 11, 1), (16, 11, 1),
   (17, 11, 1), (18, 11, 1),
   (21, 11, 1), (24, 11, 1),
   (30, 11, 1), (37, 11, 1),
   (39, 11, 1), (41, 11, 1),
   (42, 11, 1), (45, 11, 1),
   (47, 11, 1), (1, 12, 1),
   (2, 12, 1), (4, 12, 1),
   (5, 12, 1), (9, 12, 1),
   (10, 12, 1), (11, 12, 1)]

theorem piecesK1_num : 44397343278916623347964724118595232873169603198412036835684204962235309943642119420289024134670115480 ≤ totK 55 (10 ^ 100) 21 433 13899 518857 S55 piecesK1 := by
  decide +kernel

end Shiori1112