#!/usr/bin/env python3
# -*- coding: utf-8 -*-
"""第1112コマ — **f(4) の記録（第111便）を Lean に閉じるためのデータと Lean ファイルを作る。**

  python3 erdos1112.py stages     尾の 38 段の証明書（最大元の桁）と詰め込み幅・深さ別の取りこぼしを
                                  計算して erdos1112-stages.json に書く（Rows の構築が重い。数分）
  python3 erdos1112.py gen        頭の塊（685 個）と尾のチャンクを設計し、Lean を生成する

Lean 側の骨組み（手書き）：
  Erdos1112h  Walker の Theorem 1.2（K(S,b)+1 の 4-AP-free 性）
  Erdos1112k  KF / モーメント / 4 項の葉 / loK / 塊の合併（totK_le）
  Erdos1112p  |B(p,n,r)| の詰め込み計算（cfP_le）と totLoP_le
  Erdos1112c  倍加税の鎖（core_strong）
生成するもの：
  Erdos1112k1..k3  頭の塊のチャンク（totK の kernel 評価）
  Erdos1112kd      頭の塊の一覧・並び・桁・箱・下界
  Erdos1112w       38 段の証明書つきデータ・鎖の検査
  Erdos1112t0..t4  尾のチャンク（totLoP の kernel 評価）
  Erdos1112z       集合 A と Σ 1/x の下界
  Erdos1112y       主定理（4-AP-free ∧ Walker 超え）
  Chk1112          #print axioms
"""
import sys, time, json, math
import os
# [配布版の変更点 / changed for distribution] 元は書き手の機体の絶対パスを指していた箇所を、このディレクトリからの相対に変えた。計算の中身は無改変。
_HERE = os.path.dirname(os.path.abspath(__file__))
sys.path.insert(0, _HERE)
from erdos1110f4 import S55, SC, rlo, rhi, show, Kempner
from erdos834 import T, mxv

OUT = os.path.join(os.getcwd(), "out-lean") + "/"
os.makedirs(OUT, exist_ok=True)   # 生成した Lean の出力先（カレントの out-lean/）
STAGES = os.path.join(_HERE, 'f4-stages-38.txt')
JSON = os.path.join(_HERE, 'f4-stages-38.json')
S = list(S55); b = 55; NS = 21
R0 = 2263764388957216127282601815683
KMAX = R0 - 1
HEAD_LO = 44397531920675126186775585628510434944906304888509272247729289069894909151385343251671413662859973374
H_HI = 44397533692545406486665245035292911782402757776276251647961459126196844458413889864303120794793560150
WALKER15 = 4439753369254541   # > H_hi / 10^100（Walker の H(K+1) の上界を 15 桁で切り上げたもの）

def read_stages():
    st = []
    for l in open(STAGES):
        if l.startswith('#'): continue
        f = l.split()
        st.append(dict(j=int(f[0]), p=int(f[1]), q=int(f[2]), r=int(f[3]), t=int(f[4]), a=int(f[5]),
                       n=int(f[6]), d=int(f[7]), lo=int(f[8]), hi=int(f[9])))
    return st

def wrap(items, per=3, ind="   "):
    lines, cur = [], []
    for it in items:
        cur.append(it)
        if len(cur) == per:
            lines.append(", ".join(cur)); cur = []
    if cur: lines.append(", ".join(cur))
    return "[" + (",\n" + ind).join(lines) + "]"

# ---------------- 尾：証明書・幅・深さ ----------------
def maxelt_digits(R, r):
    p = R.p; digs = []
    for m in range(R.q, 0, -1):
        for k in range(p - 1, -1, -1):
            t = T(p, k)
            if t <= r and R.ok(m - 1, r - t): digs.append(k); r -= t; break
        else: raise ValueError
    assert r == 0
    return digs

def check_cert(p, q, r, digits):
    V = [T(p, k) for k in range(p)]; Tmax = max(V); assert Tmax == V[0]
    fails = []; budget = r
    for idx, k in enumerate(digits):
        n = q - idx - 1
        for d in range(k + 1, p):
            if V[d] > budget: pass
            elif budget - V[d] > n * Tmax: pass
            else: fails.append((idx, n, k, d))
        budget -= V[k]
    return fails

def mode_stages():
    from erdos1110f4 import Rows
    t0 = time.time(); st = read_stages(); RW = {}; out = []
    for s in st:
        p, q, r = s['p'], s['q'], s['r']
        if (p, q) not in RW: RW[(p, q)] = Rows(p, q)
        R = RW[(p, q)]
        assert R.cf(q, r) == s['n']
        digs = maxelt_digits(R, r); v = 0
        for k in digs: v = v * (2 * p - 1) + k
        assert v == s['t']
        fails = check_cert(p, q, r, digs)
        W = (p ** q).bit_length() // 8 * 8 + 16
        assert p ** q < 2 ** W
        res = []
        for d in range(0, 3):
            lv = R.leaves(d, q, r); lo, hi = R.bracket(d, s['a'], q, r)
            res.append((d, lv, lo))
        s.update(digs=digs, W=W, fails=len(fails), res=res)
        print("j%2d B(%d,%d,%d) W=%d fails=%d | %s  [%.0fs]" % (s['j'], p, q, r, W, len(fails),
              " ".join("d%d:%d lv loss %.2e" % (d, lv, (s['hi'] - lo) / SC) for (d, lv, lo) in res),
              time.time() - t0), flush=True)
    json.dump(st, open(JSON, 'w'))
    print("wrote", JSON, "%.0fs" % (time.time() - t0))

# ---------------- 頭：塊・モーメント・4 項の葉 ----------------
def head_pieces():
    d = []; v = KMAX
    while v > 0: d.append(v % b); v //= b
    d.reverse(); N = len(d)
    assert N == 18 and all(x in S for x in d)
    pieces = [(0, 0)]                                # {0} → 元 1
    for n in range(1, N):
        for e in S:
            if e: pieces.append((e, n - 1))        # 桁数 n、先頭 e ≠ 0
    Pt = 0
    for i in range(N):
        m = N - 1 - i
        for e in S:
            if e < d[i] and not (i == 0 and e == 0): pieces.append((Pt * b + e, m))
        Pt = Pt * b + d[i]
    assert Pt == KMAX
    pieces.append((KMAX, 0))
    pieces.sort(key=lambda w: 1 + w[0] * b ** w[1])
    return pieces

PS = [sum(e ** j for e in S) for j in range(4)]       # 21, 433, 13899, 518857
MOM = [[1, 0, 0, 0]]
for m in range(0, 40):
    B = b ** m; M0, M1, M2, M3 = MOM[-1]
    MOM.append([NS * M0, PS[1] * B * M0 + NS * M1, PS[2] * B * B * M0 + 2 * PS[1] * B * M1 + NS * M2,
                PS[3] * B ** 3 * M0 + 3 * PS[2] * B * B * M1 + 3 * PS[1] * B * M2 + NS * M3])
def mxK(m): return 47 * (b ** m - 1) // 54
def leafK(a, m):
    M0, M1, M2, M3 = MOM[m]; c = M1 // M0; D = a + c
    a0 = D ** 3 + D * D * c + D * c * c + c ** 3; a1 = D * D + 2 * D * c + 3 * c * c; a2 = D + 3 * c
    Num = a0 * M0 - a1 * M1 + a2 * M2 - M3
    return max((Num * SC) // D ** 4, 0)
def loK(j, a, m):
    if j == 0 or m == 0: return leafK(a, m)
    return sum(loK(j - 1, a + e * b ** (m - 1), m - 1) for e in S)

def head_design(depth=1):
    pieces = head_pieces()
    # 並び（隣接の分離）と箱
    for i in range(len(pieces) - 1):
        (P, m), (P2, m2) = pieces[i], pieces[i + 1]
        assert 1 + P * b ** m + mxK(m) < 1 + P2 * b ** m2
    assert all(1 + P * b ** m + mxK(m) <= R0 for (P, m) in pieces)
    # 検算：Python の厳密な挟み込みと一致するか
    K = Kempner(S55, 55, 40); lo = 0
    for (P, m) in pieces:
        if m == 0: lo += rlo(1 + P)
        else: l, h = K.free_block(P, m); lo += l
    assert abs(lo - HEAD_LO) < 10 ** 60, (lo - HEAD_LO)
    items = []; tot = 0; leaves = 0
    for (P, m) in pieces:
        j = min(depth, m); v = loK(j, 1 + P * b ** m, m); tot += v; leaves += NS ** j
        items.append((P, m, j, v, NS ** j))
    return items, tot, leaves

# ---------------- Lean 生成 ----------------
HDR = "/-\n  第1112コマ — %s\n  `erdos1112.py` が生成。sorry 0・native_decide 不使用。\n-/\n"

def mode_gen():
    t0 = time.time()
    st = json.load(open(JSON))
    assert len(st) == 38 and all(s['fails'] == 0 for s in st)
    # ---- 頭 ----
    items, htot, hleaves = head_design(1)
    print("[頭] 塊 %d、葉 %d、下界 %s（Python の head_lo との差 %.3e）" % (len(items), hleaves, show(htot, 14), (htot - HEAD_LO) / SC))
    chunks = []; cur = []; curL = 0
    for it in items:
        if cur and curL + it[4] > 4800: chunks.append(cur); cur = []; curL = 0
        cur.append(it); curL += it[4]
    if cur: chunks.append(cur)
    knames = []; ktags = []
    for k, ch in enumerate(chunks):
        name = "piecesK%d" % (k + 1); tag = "1112k%d" % (k + 1); knames.append(name); ktags.append(tag)
        Nk = sum(it[3] for it in ch); Lk = sum(it[4] for it in ch)
        src = (HDR % ("頭の塊のチャンク %d（%d 個・葉 %d）。`totK`（4 項の葉・深さ 1）の kernel 評価。" % (k + 1, len(ch), Lk))
               + "import Shioriproofs.Erdos1112k\n\nnamespace Shiori1112\n\nset_option maxRecDepth 100000\n\n"
               + "/-- 塊 `(P, m, j)`：集合 `1 + P·55^m + KF 55 S55 m`、深さ `j`。 -/\n"
               + "def %s : List (ℕ × ℕ × ℕ) :=\n  %s\n\n" % (name, wrap(["(%d, %d, %d)" % (it[0], it[1], it[2]) for it in ch], per=2))
               + "theorem %s_num : %d ≤ totK 55 (10 ^ 100) 21 433 13899 518857 S55 %s := by\n  decide +kernel\n\nend Shiori1112\n" % (name, Nk, name))
        open(OUT + "Erdos%s.lean" % tag, "w").write(src)
        print("   頭チャンク %d: %d 個 葉 %d" % (k + 1, len(ch), Lk))
    # kd
    src = (HDR % ("頭 `A₀ = (K(S,55)+1) ∩ [1, r₀]` を塊の合併として置き、並び・桁・箱・下界を閉じる。")
           + "".join("import Shioriproofs.Erdos%s\n" % t for t in ktags)
           + """
namespace Shiori1112

set_option maxRecDepth 100000

/-- 切り所 `r₀`（第110・111便）。`r₀ − 1 = max{k ∈ K(S,55) : k ≤ 10^30.5}`。 -/
def r0 : ℕ := %d

/-- 頭の塊の一覧（%d 個。左端の昇順）。 -/
def pieces4 : List (ℕ × ℕ × ℕ) := %s

theorem pieces4_length : pieces4.length = %d := by decide

/-- **塊は互いに素**（隣接の右端 < 次の左端）。 -/
theorem pieces4_ord : ordK 55 47 pieces4 = true := by decide +kernel

/-- **全塊の接頭辞の桁は S**。 -/
theorem pieces4_dig : pieces4.all (fun w => digB 55 S55 40 w.1) = true := by decide +kernel

/-- **全塊は `[1, r₀]` に収まる**。 -/
theorem pieces4_ub : pieces4.all (fun w => decide (hiK 55 47 w ≤ r0)) = true := by decide +kernel

theorem S55_s1 : ∑ e ∈ S55, e = 433 := by decide
theorem S55_s2 : ∑ e ∈ S55, e ^ 2 = 13899 := by decide
theorem S55_s3 : ∑ e ∈ S55, e ^ 3 = 518857 := by decide

/-- 頭 `A₀`（Finset）。 -/
def head4 : Finset ℕ := unionK 55 S55 pieces4

theorem head4_num : %d ≤ totK 55 (10 ^ 100) 21 433 13899 518857 S55 pieces4 := by
  have h : totK 55 (10 ^ 100) 21 433 13899 518857 S55 pieces4 = %s := by
    simp only [pieces4, totK_append]
  rw [h]
%s
  omega

/-- **頭の逆数和の下界**：%s（Python の挟み込み 4.4397531920675 との差 %.2e）。 -/
theorem head4_lower : (%d : ℚ) / 10 ^ 100 ≤ ∑ x ∈ head4, (1 : ℚ) / x := by
  have h := totK_le 55 S55 S55_lt 47 S55_le 21 433 13899 518857 S55_card S55_s1 S55_s2 S55_s3
    (10 ^ 100) (by norm_num) pieces4 pieces4_ord
  refine le_trans ?_ h
  have hc : ((10 ^ 100 : ℕ) : ℚ) = 10 ^ 100 := by norm_num
  rw [hc]
  gcongr
  exact_mod_cast head4_num

theorem head4_mem : ∀ x ∈ head4, 1 ≤ x ∧ x ≤ r0 ∧ DigIn 55 S55 (x - 1) := by
  intro x hx
  have h1 := unionK_digIn 55 S55 (by norm_num) S55_lt S55_zero 40 pieces4 pieces4_dig x hx
  have h2 := unionK_ub 55 S55 47 S55_le r0 pieces4 pieces4_ub x hx
  exact ⟨h1.1, h2, h1.2⟩

/- 以後 `head4` は展開しない（`x ∈ head4` の defeq 検査で elaborator が集合を評価しに行き、
   再帰の深さを使い切る——第112便の実測）。kernel の評価には影響しない。 -/
attribute [irreducible] head4

end Shiori1112
""" % (R0, len(items), " ++ ".join(knames), len(items), htot,
       " + ".join("totK 55 (10 ^ 100) 21 433 13899 518857 S55 %s" % n for n in knames),
       "\n".join("  have h%d := %s_num" % (k, n) for k, n in enumerate(knames)),
       show(htot, 13), (htot - HEAD_LO) / SC, htot))
    open(OUT + "Erdos1112kd.lean", "w").write(src)
    # ---- 尾 ----
    DEPTH = {j: (2 if j <= 6 else 1) for j in range(1, 39)}
    groups = [(1, 3), (4, 6), (7, 16), (17, 28), (29, 38)]
    tnames = []; ttags = []; tsum = 0; tleaves = 0; loss = 0; Nks = []
    for gi, (lo_j, hi_j) in enumerate(groups):
        ch = [s for s in st if lo_j <= s['j'] <= hi_j]
        name = "tailG%d" % gi; tag = "1112t%d" % gi; tnames.append(name); ttags.append(tag)
        items_t = []; Nk = 0; Lk = 0
        for s in ch:
            d = DEPTH[s['j']]; (dd, lv, lo) = s['res'][d]; assert dd == d
            items_t.append("(((%d, %d, %d, %d), %d, %d))" % (s['p'], s['q'], s['r'], s['a'], s['W'], d))
            Nk += lo; Lk += lv; loss += s['hi'] - lo
        tsum += Nk; tleaves += Lk; Nks.append(Nk)
        src = (HDR % ("尾のチャンク %d：段 %d〜%d（%d 個・葉 %d）。`totLoP`（詰め込み個数 `cfP`）の kernel 評価。" % (gi, lo_j, hi_j, len(ch), Lk))
               + "import Shioriproofs.Erdos1112p\n\nnamespace Shiori1112\n\nopen Shiori814\n\nset_option maxRecDepth 100000\n\n"
               + "/-- 窓 `((p, q, r, a), W, d)`：詰め込み幅 `W`（`p^q < 2^W`）、深さ `d`。 -/\n"
               + "def %s : List ((ℕ × ℕ × ℕ × ℕ) × ℕ × ℕ) :=\n  %s\n\n" % (name, wrap(items_t, per=1))
               + "theorem %s_ok : ∀ w ∈ %s, 1 ≤ w.1.1 ∧ 0 < w.1.2.2.2 := by decide\n\n" % (name, name)
               + "theorem %s_num : %d ≤ totLoP (10 ^ 100) %s := by\n  decide +kernel\n\n" % (name, Nk, name)
               + """theorem %s_lower : (%d : ℚ) / 10 ^ 100 ≤ sumWin (%s.map Prod.fst) := by
  have h := totLoP_le (10 ^ 100) (by norm_num) %s %s_ok
  have hc : ((10 ^ 100 : ℕ) : ℚ) = 10 ^ 100 := by norm_num
  rw [hc] at h
  refine le_trans ?_ h
  gcongr
  exact_mod_cast %s_num

end Shiori1112
""" % (name, Nk, name, name, name, name))
        open(OUT + "Erdos%s.lean" % tag, "w").write(src)
        print("   尾チャンク %d: 段 %d〜%d 葉 %d" % (gi, lo_j, hi_j, Lk))
    print("[尾] 下界 %.6e、取りこぼし %.3e、葉 %d" % (tsum / SC, loss / SC, tleaves))
    # ---- w：段の証明書と鎖 ----
    stage_items = []
    for s in ch_all(st):
        stage_items.append("(((%d, %d, %d, %d, %s), %d))" % (s['p'], s['q'], s['r'], s['t'], "[" + ", ".join(str(k) for k in s['digs']) + "]", s['a']))
    src = (HDR % ("38 段のデータ（ブロックの最大元の証明書 `(p,q,r,t,桁)` と offset `a`）と、倍加税の鎖の検査。")
           + "import Shioriproofs.Erdos1112c\nimport Shioriproofs.Erdos1112kd\n\nnamespace Shiori1112\n\nset_option maxRecDepth 100000\n\n"
           + "/-- 38 段。`a₁ = 2r₀+1`、`a_{j+1} = 2(a_j + t_j) + 1`（`bin-111-f4-stages.txt`）。 -/\n"
           + "def stages4 : List Stage :=\n  %s\n\n" % wrap(stage_items, per=1)
           + "theorem stages4_length : stages4.length = 38 := by decide\n\n"
           + "/-- **鎖の機械検査**：全段で `2·r_{j−1} < a_j`、`t_j = max B(p_j,q_j,r_j)`（証明書）。 -/\n"
           + "theorem chain4 : chainChk4 stages4 (r0 : ℤ) = true := by decide +kernel\n\n"
           + "/-- 38 段の窓 `(p, q, r, a)`。 -/\ndef wins4 : List (ℕ × ℕ × ℕ × ℕ) := stages4.map winOf\n\n"
           + "theorem wins4_length : wins4.length = 38 := by decide\n\n"
           + "/- 以後 `wins4` は展開しない（`head4` と同じ理由。窓の `BlkF` を評価されると終わらない）。 -/\n"
           + "attribute [irreducible] wins4\n\nend Shiori1112\n")
    open(OUT + "Erdos1112w.lean", "w").write(src)
    # ---- z：集合 A と下界 ----
    L = htot + tsum
    L15 = L // 10 ** 85          # 15 桁で切り捨て（真に小さい）
    a1 = st[0]['a']
    src = (HDR % ("集合 `A = A₀ ∪ ⋃ (a_j + B_j)` と、その上の Σ 1/x の下界。Walker の `H(K(S,55)+1)` の上界を超える。")
           + "".join("import Shioriproofs.Erdos%s\n" % t for t in ttags)
           + "import Shioriproofs.Erdos1112w\n\nnamespace Shiori1112\n\nopen Shiori814 Shiori838\n\nset_option maxRecDepth 100000\n\n"
           + "theorem tailG_map : %s = wins4 := by\n  unfold wins4; rfl\n\n" % " ++ ".join("%s.map Prod.fst" % n for n in tnames)
           + """theorem wins4_lower : (%d : ℚ) / 10 ^ 100 ≤ sumWin wins4 := by
  have h : sumWin wins4 = %s := by
    rw [← tailG_map%s]
  rw [h]
  have he : (%d : ℚ) / 10 ^ 100 = %s := by norm_num
  rw [he]
%s
  exact %s

/-- **構成そのもの**：頭 `A₀` と 38 段の窓の合併。 -/
def setA4 : Finset ℕ := head4 ∪ unionW wins4

theorem wins4_p : ∀ w ∈ wins4, 1 ≤ w.1 := by decide +kernel

/-- **窓は互いに素**（38 窓、右端は `a + mxv p q`）。 -/
theorem wins4_ord : ordWB wins4 = true := by decide +kernel

theorem wins4_lb : ∀ w ∈ wins4, %d ≤ w.2.2.2 := by decide +kernel

theorem head4_disj : Disjoint head4 (unionW wins4) := by
  rw [Finset.disjoint_left]
  intro x hx hx2
  have h1 : x ≤ %d := (head4_mem x hx).2.1
  have h2 : %d ≤ x := unionW_lb wins4 _ wins4_lb x hx2
  clear hx hx2
  omega

theorem sum_setA4 :
    ∑ x ∈ setA4, (1 : ℚ) / x = (∑ x ∈ head4, (1 : ℚ) / x) + sumWin wins4 := by
  rw [setA4, Finset.sum_union head4_disj, sum_set_eq wins4 wins4_p wins4_ord]

/-- **集合 `A` の上の Σ 1/x の下界**（SC = 10^100 の整数で）。 -/
theorem setA4_lower_full : (%d : ℚ) / 10 ^ 100 ≤ ∑ x ∈ setA4, (1 : ℚ) / x := by
  rw [sum_setA4]
  have h1 := head4_lower
  have h2 := wins4_lower
  have h3 : (%d : ℚ) / 10 ^ 100 = (%d : ℚ) / 10 ^ 100 + (%d : ℚ) / 10 ^ 100 := by norm_num
  rw [h3]
  exact add_le_add h1 h2

/-- **本コマの結論**：`A` の逆数和は **%s を超える**。 -/
theorem setA4_lower : (%d : ℚ) / 10 ^ 15 < ∑ x ∈ setA4, (1 : ℚ) / x := by
  have h := setA4_lower_full
  have : (%d : ℚ) / 10 ^ 15 < (%d : ℚ) / 10 ^ 100 := by norm_num
  linarith

/-- **Walker の集合を超える**：`H(K(S,55)+1) < 4.439753369254541`（Walker 2025 の値の上界、
    Python の厳密な挟み込み `H_hi = 4.43975336925454064…`）に対し、`A` の逆数和は
    4.439753369254541 を超える。 -/
theorem setA4_beats_walker : (%d : ℚ) / 10 ^ 15 < ∑ x ∈ setA4, (1 : ℚ) / x := by
  have h := setA4_lower
  have : (%d : ℚ) / 10 ^ 15 < (%d : ℚ) / 10 ^ 15 := by norm_num
  linarith

end Shiori1112
""" % (tsum, " + ".join("sumWin (%s.map Prod.fst)" % n for n in tnames),
       "".join(", sumWin_append" for _ in range(len(tnames) - 1)),
       tsum, " + ".join("(%d : ℚ) / 10 ^ 100" % Nk for Nk in Nks),
       "\n".join("  have h%d := %s_lower" % (k, n) for k, n in enumerate(tnames)),
       add_chain(len(tnames)),
       a1, R0, a1, L, L, htot, tsum, show(L15 * 10 ** 85, 15), L15, L15, L, WALKER15, WALKER15, L15))
    open(OUT + "Erdos1112z.lean", "w").write(src)
    # ---- y：主定理 ----
    src = (HDR % ("**主定理**：`A` は 4-AP-free であり、その逆数和は Walker の `H(K(S,55)+1)` を超える。")
           + """import Shioriproofs.Erdos1112z

namespace Shiori1112

open Shiori712 Shiori844 Shiori1109

set_option maxRecDepth 100000

/-- 頭 `A₀`（ℤ の部分集合として）。 -/
def headZ : Set ℤ := {x : ℤ | ∃ n ∈ head4, x = (n : ℤ)}

/-- 頭は `K(S,55) + 1` の部分集合。 -/
theorem headZ_sub : headZ ⊆ KSet 55 S55 := by
  rintro x ⟨n, hn, rfl⟩
  obtain ⟨h1, _, h3⟩ := head4_mem n hn
  refine ⟨n - 1, h3, ?_⟩
  push_cast [h1]
  ring

/-- **頭は 4-AP-free**（Walker の Theorem 1.2）。 -/
theorem headZ_apfree : APFreeK 4 headZ := apFreeK_mono headZ_sub KSet55_apfree

theorem headZ_box : ∀ x ∈ headZ, (0 : ℤ) < x ∧ x ≤ (r0 : ℤ) := by
  rintro x ⟨n, hn, rfl⟩
  obtain ⟨h1, h2, _⟩ := head4_mem n hn
  constructor <;> omega

theorem grow_eq_setA4 :
    growZ4 headZ stages4 = {x : ℤ | ∃ n ∈ setA4, x = (n : ℤ)} := by
  rw [growZ4_eq]
  have hw : stages4.map winOf = wins4 := by unfold wins4; rfl
  rw [hw, unionWZ_eq_coe wins4 wins4_p]
  ext x
  simp only [headZ, setA4, Set.mem_union, Set.mem_setOf_eq, Finset.mem_union]
  constructor
  · rintro (⟨n, hn, rfl⟩ | ⟨n, hn, rfl⟩)
    · exact ⟨n, Or.inl hn, rfl⟩
    · exact ⟨n, Or.inr hn, rfl⟩
  · rintro ⟨n, (hn | hn), rfl⟩
    · exact Or.inl ⟨n, hn, rfl⟩
    · exact Or.inr ⟨n, hn, rfl⟩

/-- **構成 `A` は 4-AP を含まない**（Walker の Theorem 1.2 ＋ Wróblewski の Lemma 1 ＋
    第107便 補題 2（`core_strong`）＋ 38 段の鎖）。 -/
theorem setA4_apfree : APFreeK 4 {x : ℤ | ∃ n ∈ setA4, x = (n : ℤ)} := by
  rw [← grow_eq_setA4]
  exact grow4_apfree stages4 headZ (r0 : ℤ) headZ_apfree headZ_box chain4

/-- **主定理（第111便の記録を単一の型に）**：`A` は 4-AP-free であり、かつその逆数和は
    **4.439753369254541 を超える**——Walker 2025 の `H(K(S,55)+1) = 4.43975336925454064…` より大きい。 -/
theorem setA4_apfree_and_beats_walker :
    APFreeK 4 {x : ℤ | ∃ n ∈ setA4, x = (n : ℤ)} ∧
      (%d : ℚ) / 10 ^ 15 < ∑ x ∈ setA4, (1 : ℚ) / x :=
  ⟨setA4_apfree, setA4_beats_walker⟩

/-- 下界そのものを添えた形（%s）。 -/
theorem setA4_apfree_and_lower :
    APFreeK 4 {x : ℤ | ∃ n ∈ setA4, x = (n : ℤ)} ∧
      (%d : ℚ) / 10 ^ 15 < ∑ x ∈ setA4, (1 : ℚ) / x :=
  ⟨setA4_apfree, setA4_lower⟩

end Shiori1112
""" % (WALKER15, show(L15 * 10 ** 85, 15), L15))
    open(OUT + "Erdos1112y.lean", "w").write(src)
    chk = ("import Shioriproofs.Erdos1112y\n\n"
           + "#print axioms Shiori1112.setA4_apfree_and_beats_walker\n#print axioms Shiori1112.setA4_apfree_and_lower\n"
           + "#print axioms Shiori1112.setA4_apfree\n#print axioms Shiori1112.setA4_lower_full\n#print axioms Shiori1112.chain4\n"
           + "#print axioms Shiori1112.head4_lower\n#print axioms Shiori1112.KSet55_apfree\n"
           + "".join("#print axioms Shiori1112.%s_num\n" % n for n in knames + tnames))
    open(OUT + "Chk1112.lean", "w").write(chk)
    print("[総和] L = %s（Python の TOTAL_LO 4.439753474496394 との差 %.3e）" % (show(L, 15), (L - 44397534744963946614334638832870612476299827177484180612010192792690711619599583977538060005655401214) / SC))
    print("[主張] %d / 10^15 = %s > Walker %d / 10^15" % (L15, show(L15 * 10 ** 85, 15), WALKER15))
    print("経過 %.1f 秒" % (time.time() - t0))

def ch_all(st): return st

def add_chain(n):
    expr = "h0"
    for k in range(1, n):
        expr = "add_le_add (%s) h%d" % (expr, k) if k > 1 else "add_le_add h0 h1"
    return expr

if __name__ == '__main__':
    mode = sys.argv[1] if len(sys.argv) > 1 else 'gen'
    if mode == 'stages': mode_stages()
    else: mode_gen()