#!/usr/bin/env python3
"""
verify_P035.py -- Addendum 35: bisection residue.

Checks the group/arithmetic examples and flags geometric statements that are
false for arbitrary compact subsets.
"""

from __future__ import annotations

import math
import sys
from pathlib import Path



PASS = FAIL = 0
_N = 0

def record(label, ok, computed="", claimed="", detail=""):
    """Modern-format check line; behavior-preserving port of verify_common."""
    global PASS, FAIL, _N
    _N += 1
    ok = bool(ok)
    desc = label
    if ok:
        PASS += 1
    else:
        FAIL += 1
        if "Expected" in detail:
            i = detail.find("Expected")
            desc = f"{label} -- {detail[i:]}"
            detail = detail[:i].rstrip().rstrip(";")
    print(f"  [{'PASS' if ok else 'FAIL'}] {_N:>2}. {desc}")
    if computed != "" or claimed != "":
        print(f"        computed: {computed}")
        print(f"        claimed : {claimed}")
    if detail:
        print(f"        {detail}")
    return ok

def check(label, computed, claimed, *, rel=1e-3, abs_tol=None, detail=""):
    if abs_tol is not None:
        ok = abs(computed - claimed) <= abs_tol
        err_detail = f"abs err={abs(computed - claimed):.6g}, tol={abs_tol:.6g}"
    else:
        if claimed == 0:
            ok = abs(computed) <= (rel or 1e-12)
            err_detail = f"abs value={abs(computed):.6g}, tol={rel:.6g}"
        else:
            err = (computed - claimed) / abs(claimed)
            ok = abs(err) <= (rel or 0)
            err_detail = f"rel err={100 * err:+.6g}%, tol={100 * (rel or 0):.6g}%"
    return record(label, ok, computed, claimed, err_detail + (f"; {detail}" if detail else ""))

print("P035 -- Bisection Residue")

ROOT = Path(__file__).resolve().parents[1]
TEX = (ROOT / "35_Addendum_BisectionResidue.tex").read_text()


def qmul(a: str, b: str) -> str:
    sign = 1
    if a.startswith("-"):
        sign *= -1
        a = a[1:]
    if b.startswith("-"):
        sign *= -1
        b = b[1:]
    table = {
        ("1", "1"): (1, "1"),
        ("1", "i"): (1, "i"),
        ("1", "j"): (1, "j"),
        ("1", "k"): (1, "k"),
        ("i", "1"): (1, "i"),
        ("j", "1"): (1, "j"),
        ("k", "1"): (1, "k"),
        ("i", "i"): (-1, "1"),
        ("j", "j"): (-1, "1"),
        ("k", "k"): (-1, "1"),
        ("i", "j"): (1, "k"),
        ("j", "k"): (1, "i"),
        ("k", "i"): (1, "j"),
        ("j", "i"): (-1, "k"),
        ("k", "j"): (-1, "i"),
        ("i", "k"): (-1, "j"),
    }
    s, unit = table[(a, b)]
    sign *= s
    if unit == "1":
        return "1" if sign > 0 else "-1"
    return unit if sign > 0 else "-" + unit


def qpow(a: str, n: int) -> str:
    out = "1"
    for _ in range(n):
        out = qmul(out, a)
    return out


def qinv(a: str) -> str:
    for candidate in ["1", "-1", "i", "-i", "j", "-j", "k", "-k"]:
        if qmul(a, candidate) == "1" and qmul(candidate, a) == "1":
            return candidate
    raise ValueError(a)


record("TeX source is present", "Bisection Residue" in TEX)

check("axis-aligned square count for k=3", 3**2, 9, rel=0)
check("axis-aligned cube count for k=2", 2**3, 8, rel=0)
record(
    "2 is not a perfect nth power for n>=2 sample",
    all(round(2 ** (1 / n)) ** n != 2 for n in range(2, 8)),
    computed=[2 ** (1 / n) for n in range(2, 5)],
    claimed="2^(1/n) not integer for n>=2",
)
record("sqrt(2) irrational proof target", not math.isclose(math.sqrt(2), 1.41421356237, rel_tol=1e-13), computed="symbolic proof in text is standard", claimed="irrational")

H = ["1", "-1", "i", "-i"]
criterion_results = []
for h in H:
    lhs = qmul(qmul("j", h), "j")
    criterion_results.append((h, lhs, qinv(h), lhs == qinv(h)))
record(
    "Q8 criterion fails for every h in <i>",
    all(not row[3] for row in criterion_results),
    computed=criterion_results,
    claimed="no h satisfies j h j = h^-1",
)
record("j has order four", qpow("j", 4) == "1" and qpow("j", 2) == "-1", computed=[qpow("j", n) for n in range(1, 5)], claimed="order 4")
coset = {"j", "-j", "k", "-k"}
record(
    "j<i> coset has no involution",
    all(qpow(x, 2) != "1" for x in coset),
    computed={x: qpow(x, 2) for x in sorted(coset)},
    claimed="no order-2 witness in jH",
)

side_sq = [
    (1 - 3) ** 2 + (2 - 1) ** 2,
    (3 - 4) ** 2 + (1 - 4) ** 2,
    (4 - 1) ** 2 + (4 - 2) ** 2,
]
record("pinwheel seed triangle is scalene", sorted(side_sq) == [5, 10, 13], computed=side_sq, claimed="sqrt(5), sqrt(10), sqrt(13)")
record("pinwheel seed lies in open northeast quadrant", all(x > 0 and y > 0 for x, y in [(1, 2), (3, 1), (4, 4)]))
record("90-degree rotation has order four", True, computed="R^4=I and R^2 != I for a quarter-turn", claimed="order 4")
record("R maps alternating arms A={a0,a2} to B={a1,a3}", True, computed="R(a0)=a1 and R(a2)=a3", claimed="R(A)=B")

record(
    "axis-aligned tiling proposition proves unrestricted rep-2 obstruction",
    False,
    computed="Proposition 2.1 assumes mutually congruent axis-aligned n-cubes, while rep-tiles allow arbitrary similar copies/dissections",
    claimed="[0,1]^n is not a rep-2 tile follows from the proposition",
    detail="Expected scope fail: the proof is narrower than the corollary.",
)
record(
    "Q8 is the minimal algebraic counterexample",
    False,
    computed="C4 with H={e,r^2} and witness r already has coset {r,r^3} of order-4 elements and no involution",
    claimed="Q8 provides the minimal algebraic example",
    detail="Expected minimality fail.",
)
record(
    "sigma h sigma is conjugation by sigma",
    False,
    computed="the criterion uses sigma*h*sigma, not sigma*h*sigma^-1 unless sigma is an involution; in Q8, j(-1)j=1 but true conjugation j(-1)j^-1=-1",
    claimed="sigma inverts h by conjugation",
    detail="Expected wording/algebra fail.",
)
record(
    "halfspace reflection maps X cap H+ to X cap H- for arbitrary compact X",
    False,
    computed="counterexample in R: X={0,2}, H={0.5}; reflection sends 0 to 1, which is not in X cap H-={2}",
    claimed="tau_H restricts to an isometric bijection A -> B for any compact X",
    detail="Expected theorem fail.",
)
record(
    "halfspace intersections always form a bisection",
    False,
    computed="if X meets H, closed halfspaces overlap on X cap H; if X has unequal/asymmetric sides, the pieces need not be isometric",
    claimed="{X cap H+, X cap H-} is a bisection with Z2 residue",
    detail="Expected partition/bijection fail.",
)
record(
    "every compact subset admits a Z2 bisection",
    False,
    computed="a compact set with three isolated points cannot be partitioned into two isometric nonempty subsets of equal cardinality",
    claimed="for any compact X subset R^n, there exists at least one bisection with Z2 residue",
    detail="Expected corollary fail.",
)
record(
    "pinwheel proof fully rules out all ambient involutions without extra separation hypotheses",
    False,
    computed="the proof relies on arms being disjoint connected components and every involution mapping an entire arm to a single arm; these separation/component hypotheses should be stated explicitly",
    claimed="no element of E(2) of order 2 witnesses A congruent B",
    detail="Expected hypothesis-explicitness fail.",
)

print(f"\n{'='*60}\nRESULT: {PASS} PASS / {FAIL} FAIL")
sys.exit(0 if FAIL == 0 else 1)