"""RUN-002 - Round 00: the external baseline and the support-function interface.

Round 00 claims no bound. What it fixes, and every later round inherits, is
(i) the published interval it measures itself against, with four citations,
and (ii) the support-function interface of its section 9. Both are checked
here. The claimed values are extracted from Round 00's own bytes (read from
the archive through corpus.py), never retyped.

Checks
  A1 claims-extracted   every baseline claim is found in Round 00 exactly once,
                        with no conflicting second value
  A2 claims-match-source  each citation's title, authors, first-version date and
                        quoted numbers/statements match the arXiv record
  A3 gap-arithmetic     the stated gap equals upper minus lower, exactly
  B1 proper-motion-law  h_{gK}(t) = h_K(t - phi) + t.u_t for g = (R_phi, t),
                        verified as a symbolic identity (then sup over K)
  B2 improper-motion-law  for g = (R_phi o sigma, t) the law is h_K(phi - t) + t.u_t;
                        Round 00's formula is shown to differ on a body
                        without mirror symmetry (exact rational witness)
  B3 containment-hypotheses  the interface "h_{gK} <= h_U on S^1 => gK in U" needs
                        U closed and convex; dropping either admits an explicit,
                        exactly verified counterexample

Usage:
  python code/run002_round00_baseline_interface.py [--refresh] [--drill]
    --refresh re-fetches the four arXiv abstract pages into the snapshot
"""
import argparse
import datetime
import hashlib
import html
import json
import re
import sys
import urllib.request
from decimal import Decimal
from fractions import Fraction

import sympy as sp

from corpus import SOURCES, TREE, source_bytes, walk_sources

ROUND00 = "main.zip!/AMRAL_Lebesgue_Finite_Closure_Round_00_Methodology_v0.2.md"
SNAPSHOT = TREE / "data" / "external" / "arxiv-round00-citations.json"
LOG = TREE / "data" / "gate-logs" / "run002-round00-baseline-interface.json"
CITED = ["1810.10089", "2608.30538", "2609.01284", "2606.14625"]
NUM = re.compile(r"0\.8\d{2,}")


# ---------------------------------------------------------------- arXiv snapshot

def fetch_snapshot():
    out = {"retrieved": datetime.date.today().isoformat(), "source": "arxiv.org/abs pages",
           "records": {}}
    for aid in CITED:
        req = urllib.request.Request(f"https://arxiv.org/abs/{aid}",
                                     headers={"User-Agent": "amral-verification", "Accept": "text/html"})
        page = urllib.request.urlopen(req, timeout=60).read().decode("utf-8", "replace")
        meta = lambda n: [html.unescape(x) for x in
                          re.findall(rf'<meta name="{n}" content="(.*?)"', page, re.S)]
        abstract = meta("citation_abstract")[0]
        # every version, not only the current one (which alone is in bold)
        history = re.search(r"Submission history</h2>(.*?)</div>", page, re.S).group(1)
        history = re.sub(r"\s+", " ", re.sub(r"<[^>]+>", " ", history))
        versions = re.findall(r"\[v(\d+)\]\s*\w{3}, (\d{1,2} \w{3} \d{4})", history)
        out["records"][aid] = {
            "title": meta("citation_title")[0],
            "authors": meta("citation_author"),
            "versions": {f"v{v}": datetime.datetime.strptime(d, "%d %b %Y").date().isoformat()
                         for v, d in versions},
            "abstract_sha256": hashlib.sha256(abstract.encode("utf-8")).hexdigest(),
            "abstract_numbers": sorted(set(NUM.findall(abstract))),
            "abstract_statements": {
                "monotone hierarchy": bool(re.search(r"monotone", abstract)),
                "limit equals constant": r"a_{\mathrm{Leb}}=\lim_{M\to\infty}\Lambda_M" in abstract,
                "rate C M^-2": r"0\le a_{\mathrm{Leb}}-\Lambda_M\le C M^{-2}" in abstract,
                "exhaustive subdivision certificate": bool(
                    re.search(r"exhaustive subdivision", abstract) and re.search(r"certificate", abstract)),
            },
        }
    return out


# ---------------------------------------------------------------- Round 00 claims

REF = re.compile(r"^\s*\d+\.\s+(.+?),\s+\*(.+?)\*,\s+arXiv:(\d{4}\.\d{4,5}),\s+(\d{4}(?:-\d{2}-\d{2})?)\.",
                 re.M)


def extract_claims(text):
    """Return (claims, failures). Every pattern must match exactly one value."""
    text = text.replace("\r\n", "\n")
    failures, claims = [], {}

    def one(key, pattern, flags=re.S):
        vals = sorted(set(re.findall(pattern, text, flags)))
        if len(vals) != 1:
            failures.append(f"{key}: {len(vals)} distinct values {vals}")
            return None
        claims[key] = vals[0]
        return vals[0]

    one("upper", r"Gibbs 給出的公開上界：\s*\$\$\s*a_\{\\mathrm\{Leb\}\}\s*\\le\s*(0\.\d+)\.")
    one("lower_date", r"Mishra 於 (\d{4}-\d{2}-\d{2}) 提出的嚴格下界")
    one("lower", r"提出的嚴格下界：\s*\$\$\s*a_\{\\mathrm\{Leb\}\}\s*\\ge\s*(0\.\d+)\.")
    one("hierarchy_date", r"Zeng 於 (\d{4}-\d{2}-\d{2}) 提出 Reuleaux-type variational hierarchy")
    one("rate", r"\\le\s*(CM\^\{-2\})\.")
    one("limit", r"a_\{\\mathrm\{Leb\}\}\s*=\s*(\\lim_\{M\\to\\infty\}\\Lambda_M)")
    one("monotone", r"(\\Lambda_1\s*\\le\s*\\Lambda_2\s*\\le\s*\\cdots\s*\\le\s*a_\{\\mathrm\{Leb\}\})")
    gap = re.findall(r"\$\$\s*(0\.\d+)-(0\.\d+)\s*=\s*(0\.\d+)\.\s*\$\$", text)
    if len(gap) != 1:
        failures.append(f"gap: {len(gap)} gap computations found")
    else:
        claims["gap_minuend"], claims["gap_subtrahend"], claims["gap"] = gap[0]
    interval = re.findall(r"\$\$\s*(0\.\d+)\s*\\le\s*a_\{\\mathrm\{Leb\}\}\s*\\le\s*(0\.\d+)\.\s*\$\$", text)
    if len(interval) != 1:
        failures.append(f"interval: {len(interval)} interval statements found")
    else:
        claims["interval_lower"], claims["interval_upper"] = interval[0]
    refs = {}
    for authors, title, aid, date in REF.findall(text):
        if aid in refs:
            failures.append(f"reference {aid} listed twice")
        refs[aid] = {"authors": [a.strip() for a in authors.split(" and ")],
                     "title": title, "date": date}
    for aid in CITED:
        if aid not in refs:
            failures.append(f"reference {aid} not found")
    for aid in sorted(set(refs) - set(CITED)):
        failures.append(f"unexpected reference {aid}")
    claims["references"] = refs
    for a, b in (("interval_lower", "lower"), ("interval_upper", "upper"),
                 ("gap_minuend", "upper"), ("gap_subtrahend", "lower")):
        if a in claims and b in claims and Decimal(claims[a]) != Decimal(claims[b]):
            failures.append(f"{a}={claims[a]} disagrees with {b}={claims[b]}")
    return claims, failures


def norm_title(s):
    return re.sub(r"\s+", " ", html.unescape(s).replace("\u2019", "'")).strip()


def norm_author(s):
    last, _, first = s.partition(", ")
    return f"{first} {last}".strip() if first else s.strip()


# ---------------------------------------------------------------- checks A

def a1_claims_extracted(w):
    return w["extract_failures"]


def a2_claims_match_source(w):
    failures, c, recs = [], w["claims"], w["snapshot"]["records"]
    for aid, ref in c.get("references", {}).items():
        r = recs.get(aid)
        if r is None:
            failures.append(f"{aid}: no arXiv record")
            continue
        if norm_title(ref["title"]) != norm_title(r["title"]):
            failures.append(f"{aid}: title differs")
        if [a.strip() for a in ref["authors"]] != [norm_author(a) for a in r["authors"]]:
            failures.append(f"{aid}: authors {ref['authors']} vs {r['authors']}")
        v1 = r["versions"].get("v1", "")
        if (ref["date"] != v1) if len(ref["date"]) == 10 else (ref["date"] != v1[:4]):
            failures.append(f"{aid}: dated {ref['date']}, first version {v1}")
    nums = lambda aid: {Decimal(n) for n in recs.get(aid, {}).get("abstract_numbers", [])}
    st = lambda aid: recs.get(aid, {}).get("abstract_statements", {})
    if "upper" in c and Decimal(c["upper"]) not in nums("1810.10089"):
        failures.append(f"upper bound {c['upper']} not in Gibbs abstract")
    if "lower" in c and Decimal(c["lower"]) not in nums("2608.30538"):
        failures.append(f"lower bound {c['lower']} not in Mishra abstract")
    if "lower_date" in c and c["lower_date"] != recs.get("2608.30538", {}).get("versions", {}).get("v1"):
        failures.append(f"lower bound dated {c['lower_date']}, Mishra v1 differs")
    if "hierarchy_date" in c and c["hierarchy_date"] != recs.get("2609.01284", {}).get("versions", {}).get("v1"):
        failures.append(f"hierarchy dated {c['hierarchy_date']}, Zeng v1 differs")
    if not st("2608.30538").get("exhaustive subdivision certificate"):
        failures.append("Mishra abstract: no exhaustive-subdivision certificate statement")
    for key, stmt in (("monotone", "monotone hierarchy"), ("limit", "limit equals constant"),
                      ("rate", "rate C M^-2")):
        if key in c and not st("2609.01284").get(stmt):
            failures.append(f"Zeng abstract: '{stmt}' not found")
    return failures


def a3_gap_arithmetic(w):
    c = w["claims"]
    if not all(k in c for k in ("gap_minuend", "gap_subtrahend", "gap")):
        return ["gap not extracted"]
    exact = Decimal(c["gap_minuend"]) - Decimal(c["gap_subtrahend"])
    return [] if exact == Decimal(c["gap"]) else [f"{c['gap_minuend']} - {c['gap_subtrahend']} = {exact}, stated {c['gap']}"]


# ---------------------------------------------------------------- checks B

TH, PH, T1, T2, X1, X2 = sp.symbols("theta phi t1 t2 x1 x2", real=True)
X = sp.Matrix([X1, X2])
T = sp.Matrix([T1, T2])
u = lambda a: sp.Matrix([sp.cos(a), sp.sin(a)])
R = lambda a: sp.Matrix([[sp.cos(a), -sp.sin(a)], [sp.sin(a), sp.cos(a)]])
SIGMA = sp.Matrix([[1, 0], [0, -1]])

# a candidate law maps (x, t, phi, theta) to the claimed value of (g x).u_theta
# for one point x; the sup over K then carries it to support functions exactly.
ROUND00_LAW = lambda x, t, ph, th: (x.T * u(th - ph))[0] + (t.T * u(th))[0]
IMPROPER_LAW = lambda x, t, ph, th: (x.T * u(ph - th))[0] + (t.T * u(th))[0]


def identity_holds(law, motion):
    lhs = ((motion * X + T).T * u(TH))[0]
    return sp.simplify(sp.expand_trig(lhs - law(X, T, PH, TH))) == 0


def b1_proper_motion_law(w):
    return [] if identity_holds(w["law_proper"], R(PH)) else ["law fails for g = (R_phi, t)"]


def chirality(tri):
    """For a triangle with three distinct side lengths: the orientation sign of
    its vertices listed by increasing opposite side. Proper motions preserve
    side lengths and orientation, so a triangle whose mirror image has the
    opposite sign is not properly congruent to it. None if not scalene."""
    sq = lambda p, q: (p[0] - q[0]) ** 2 + (p[1] - q[1]) ** 2
    a, b, c = tri
    opposite = sorted([(sq(b, c), a), (sq(c, a), b), (sq(a, b), c)])
    if len({d for d, _ in opposite}) < 3:
        return None
    p, q, r = (v for _, v in opposite)
    cross = (q[0] - p[0]) * (r[1] - p[1]) - (q[1] - p[1]) * (r[0] - p[0])
    return (cross > 0) - (cross < 0)


def b2_improper_motion_law(w):
    """Evidence for the E(2)/SE(2) observation: the orientation-reversing half
    of E(2) obeys a different law, and it is not redundant - a scalene
    triangle's mirror image is no proper motion of it."""
    failures = []
    if not identity_holds(IMPROPER_LAW, R(PH) * SIGMA):
        failures.append("the improper-motion law fails")
    if identity_holds(ROUND00_LAW, R(PH) * SIGMA):
        failures.append("Round 00's law also holds for improper motions - nothing to report")
    body = w["b2_body"]
    mirrored = [(x, -y) for x, y in body]
    s, s_m = chirality(body), chirality(mirrored)
    if s is None or s_m is None or s == s_m:
        failures.append(f"body {body} gives no chirality witness")
    else:
        w["b2_witness"] = {"body": [[str(x), str(y)] for x, y in body],
                           "orientation_sign": s, "mirror_orientation_sign": s_m}
    return failures


def b3_containment_hypotheses(w):
    """Both hypotheses of 'h_{gK} <= h_U on S^1 => gK in U' are load-bearing:
    with either dropped, an exact counterexample exists."""
    failures = []
    # (i) convex, not closed: U = the unit disc, closed iff ce_open["closed"];
    #     K = closed unit disc. h_K = h_U = 1 in every direction (for the open
    #     disc as a supremum), so the support inequality holds; the boundary
    #     point p is in K and must be outside U for a counterexample.
    ce = w["ce_open"]
    p = ce["point"]
    r2 = p[0] ** 2 + p[1] ** 2
    in_K = r2 <= 1
    in_U = r2 <= 1 if ce["closed"] else r2 < 1
    if not (in_K and not in_U):
        failures.append("unclosed U: no point of K outside U - the open-disc counterexample fails")
    # (ii) closed, not convex: U = annulus inner_sq <= |x|^2 <= 1, whose support
    #     function is 1 (attained on the outer circle); K = {p}, h_K <= 1.
    ce = w["ce_annulus"]
    p = ce["point"]
    r2 = p[0] ** 2 + p[1] ** 2
    if not (r2 <= 1 and not (ce["inner_sq"] <= r2 <= 1)):
        failures.append("nonconvex U: K is inside U - the annulus counterexample fails")
    return failures


CHECKS = {"A1": a1_claims_extracted, "A2": a2_claims_match_source, "A3": a3_gap_arithmetic,
          "B1": b1_proper_motion_law, "B2": b2_improper_motion_law, "B3": b3_containment_hypotheses}


SCALENE = [(Fraction(0), Fraction(0)), (Fraction(3), Fraction(0)), (Fraction(1), Fraction(2))]


def build_world(text, snapshot):
    claims, failures = extract_claims(text)
    return {"text": text, "claims": claims, "extract_failures": failures, "snapshot": snapshot,
            "law_proper": ROUND00_LAW, "b2_body": list(SCALENE),
            "ce_open": {"point": (Fraction(1), Fraction(0)), "closed": False},
            "ce_annulus": {"point": (Fraction(0), Fraction(0)), "inner_sq": Fraction(1, 4)}}


def run_checks(w):
    return {cid: fn(w) for cid, fn in CHECKS.items()}


# ---------------------------------------------------------------- drill

def drill(text, snapshot):
    import copy

    def doc(fn):
        return lambda: build_world(fn(text), copy.deepcopy(snapshot))

    def snap(fn):
        def make():
            s = copy.deepcopy(snapshot)
            fn(s)
            return build_world(text, s)
        return make

    def law(fn):
        def make():
            w = build_world(text, copy.deepcopy(snapshot))
            w["law_proper"] = fn
            return w
        return make

    def world(**changes):
        def make():
            w = build_world(text, copy.deepcopy(snapshot))
            for k, v in changes.items():
                w[k] = v
            return w
        return make

    recs = lambda s: s["records"]
    cases = [
        ("K0-unmodified", "control", lambda: build_world(text, copy.deepcopy(snapshot)), set()),
        ("K1-crlf-document", "control", doc(lambda t: t.replace("\n", "\r\n")), set()),
        ("K2-title-html-entity", "control",
         snap(lambda s: recs(s)["1810.10089"].update(title=recs(s)["1810.10089"]["title"].replace("'", "&#39;"))), set()),
        ("K3-trailing-zero-number", "control",
         snap(lambda s: recs(s)["2608.30538"].update(abstract_numbers=[n + "0" for n in recs(s)["2608.30538"]["abstract_numbers"]])), set()),
        ("K4-law-periodic-rewrite", "control",
         law(lambda x, t, ph, th: (x.T * u(th - ph + 2 * sp.pi))[0] + (t.T * u(th))[0]), set()),
        ("K5-law-as-inverse-rotation", "control",
         law(lambda x, t, ph, th: (x.T * (R(-ph) * u(th)))[0] + (t.T * u(th))[0]), set()),
        ("M1-lower-bound-edited", "mutation", doc(lambda t: t.replace("0.8344", "0.8345")), {"A2", "A3"}),
        ("M2-gap-edited", "mutation", doc(lambda t: t.replace("0.0096935944", "0.0096935945")), {"A3"}),
        ("M3-lower-date-is-v2", "mutation", doc(lambda t: t.replace("Mishra 於 2026-08-31", "Mishra 於 2026-09-01")), {"A2"}),
        ("M4-title-one-char", "mutation", doc(lambda t: t.replace("Curves of constant width", "Curves of constant widths")), {"A2"}),
        ("M5-arxiv-id-edited", "mutation", doc(lambda t: t.replace("arXiv:2606.14625", "arXiv:2606.14626")), {"A1", "A2"}),
        ("M6-rate-removed", "mutation", doc(lambda t: t.replace("CM^{-2}.", "CM^{-1}.")), {"A1"}),
        ("M7-conflicting-lower", "mutation",
         doc(lambda t: t.replace("# 2. 過去研究的繼承原則", "提出的嚴格下界：\n\n$$\na_{\\mathrm{Leb}}\n\\ge\n0.8350.\n$$\n\n# 2. 過去研究的繼承原則")), {"A1"}),
        ("M8-upper-edited-in-interval-only", "mutation",
         doc(lambda t: t.replace("\\le\n0.8440935944.\n$$\n\n目前差距", "\\le\n0.8440935945.\n$$\n\n目前差距")), {"A1"}),
        ("M9-source-number-changed", "mutation",
         snap(lambda s: recs(s)["1810.10089"].update(abstract_numbers=["0.8440935945"])), {"A2"}),
        ("M10-source-rate-missing", "mutation",
         snap(lambda s: recs(s)["2609.01284"]["abstract_statements"].update({"rate C M^-2": False})), {"A2"}),
        ("M11-source-authors-reordered", "mutation",
         snap(lambda s: recs(s)["2606.14625"].update(authors=list(reversed(recs(s)["2606.14625"]["authors"])))), {"A2"}),
        ("M12-law-sign-of-phi", "mutation", law(lambda x, t, ph, th: (x.T * u(th + ph))[0] + (t.T * u(th))[0]), {"B1"}),
        ("M13-law-translation-sign", "mutation", law(lambda x, t, ph, th: (x.T * u(th - ph))[0] - (t.T * u(th))[0]), {"B1"}),
        ("M14-law-translation-rotated", "mutation", law(lambda x, t, ph, th: (x.T * u(th - ph))[0] + (t.T * u(th - ph))[0]), {"B1"}),
        ("M15-law-rotation-dropped", "mutation", law(lambda x, t, ph, th: (x.T * u(th))[0] + (t.T * u(th))[0]), {"B1"}),
        ("M16-law-improper-used-for-proper", "mutation", law(IMPROPER_LAW), {"B1"}),
        ("K6-other-scalene-body", "control",
         world(b2_body=[(Fraction(0), Fraction(0)), (Fraction(4), Fraction(0)), (Fraction(1), Fraction(1))]), set()),
        ("K7-interior-point-of-annulus-hole", "control",
         world(ce_annulus={"point": (Fraction(1, 10), Fraction(1, 10)), "inner_sq": Fraction(1, 4)}), set()),
        ("M17-isosceles-body-has-no-chirality", "mutation",
         world(b2_body=[(Fraction(0), Fraction(0)), (Fraction(2), Fraction(0)), (Fraction(1), Fraction(3))]), {"B2"}),
        ("M18-disc-taken-closed", "mutation",
         world(ce_open={"point": (Fraction(1), Fraction(0)), "closed": True}), {"B3"}),
        ("M19-annulus-hole-closed-up", "mutation",
         world(ce_annulus={"point": (Fraction(0), Fraction(0)), "inner_sq": Fraction(0)}), {"B3"}),
        ("M20-point-inside-open-disc", "mutation",
         world(ce_open={"point": (Fraction(1, 2), Fraction(0)), "closed": False}), {"B3"}),
    ]
    results = []
    for cid, kind, make, expected in cases:
        got = run_checks(make())
        tripped = {c for c, f in got.items() if f}
        results.append({"case": cid, "kind": kind, "expected": sorted(expected),
                        "tripped": sorted(tripped), "ok": tripped == expected})
    return results


# ---------------------------------------------------------------- main

def main():
    ap = argparse.ArgumentParser()
    ap.add_argument("--refresh", action="store_true")
    ap.add_argument("--drill", action="store_true")
    ap.add_argument("--blind", metavar="CID")
    args = ap.parse_args()
    if args.refresh:
        SNAPSHOT.parent.mkdir(parents=True, exist_ok=True)
        SNAPSHOT.write_text(json.dumps(fetch_snapshot(), ensure_ascii=False, indent=1) + "\n",
                            encoding="utf-8")
    snapshot = json.loads(SNAPSHOT.read_text(encoding="utf-8"))
    blobs = {n: source_bytes(n) for n in SOURCES}
    text = next(d for leaf, d in walk_sources(blobs, keep=lambda l: l.id == ROUND00)
                if leaf.id == ROUND00).decode("utf-8")
    if args.blind:
        CHECKS[args.blind] = lambda w: []
        args.drill = True

    w = build_world(text, snapshot)
    results = run_checks(w)
    for cid, f in results.items():
        print(f"{cid} {'PASS' if not f else 'FAIL'}", *(f"\n     {x}" for x in f[:6]))
    log = {
        "run": "RUN-002",
        "subject": "Round 00 v0.2: external baseline and support-function interface",
        "document": ROUND00,
        "snapshot_retrieved": snapshot["retrieved"],
        "claims": w["claims"],
        "checks": {cid: {"pass": not f, "failures": f} for cid, f in results.items()},
        "b2_witness": w.get("b2_witness"),
    }
    if args.drill:
        d = drill(text, snapshot)
        plants = [x for x in d if x["kind"] == "mutation"]
        controls = [x for x in d if x["kind"] == "control"]
        held = sum(1 for x in d for c in CHECKS if c not in x["expected"] and c not in x["tripped"])
        quiet = sum(1 for x in d for c in CHECKS if c not in x["expected"])
        log["drill"] = {"plants": len(plants), "plants_caught_by_named_checks": sum(x["ok"] for x in plants),
                        "controls": len(controls), "controls_undisturbed": sum(x["ok"] for x in controls),
                        "must_stay_green_assertions": quiet, "must_stay_green_held": held, "cases": d}
        print(f"drill: {log['drill']['plants_caught_by_named_checks']}/{len(plants)} plants caught by exactly "
              f"the named checks; {log['drill']['controls_undisturbed']}/{len(controls)} controls "
              f"undisturbed; {held}/{quiet} must-stay-green assertions held")
        for x in d:
            if not x["ok"]:
                print("   DRILL FAIL", x)
        if args.blind:
            n = sum(1 for x in d if args.blind in x["expected"] and args.blind not in x["tripped"])
            print(f"blind {args.blind}: drill reported it blind in {n} cases (log not written)")
            return
    LOG.write_text(json.dumps(log, ensure_ascii=False, indent=1) + "\n", encoding="utf-8")


if __name__ == "__main__":
    main()