#!/usr/bin/env python3
"""
verify_P147.py -- Addendum 147: incommensurate Oscillate subsystems.

This verifier checks the CRT/period arithmetic and worked S3 distance examples,
then flags where geodesic proximity, MDL score margin, Plateau firing, and P27
cross-coherence are identified without explicit bridge lemmas.
"""

from __future__ import annotations

import math
import sys
from pathlib import Path

sys.path.insert(0, str(Path(__file__).resolve().parent))
from verify_common import Verifier as _BaseVerifier, CheckResult


class Verifier(_BaseVerifier):
    """Output-layer normalization only: same checks, modern [PASS]/[FAIL] format."""

    def __init__(self, name: str):
        self.name = name
        self.results = []
        print(name)

    def record(self, label, ok, computed="", claimed="", detail=""):
        self.results.append(CheckResult(label, ok, computed, claimed, detail))
        n = len(self.results)
        note, info = "", detail
        if not ok and "Expected" in detail:
            i = detail.find("Expected")
            note = " -- " + detail[i:]
            info = detail[:i].rstrip().rstrip(";")
        print(f"  [{'PASS' if ok else 'FAIL'}] {n:>2}. {label}{note}")
        if computed != "" or claimed != "":
            print(f"        computed: {computed}")
            print(f"        claimed : {claimed}")
        if info:
            print(f"        {info}")
        return ok

    def summary(self):
        passed = sum(r.ok for r in self.results)
        failed = len(self.results) - passed
        print(f"\n{'='*60}\nRESULT: {passed} PASS / {failed} FAIL")
        return 1 if failed else 0


v = Verifier("P147 -- Incommensurate Oscillate")

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

EPS_P = 0.02


def ds3(p: tuple[float, float, float, float], q: tuple[float, float, float, float]) -> float:
    dot = abs(sum(a * b for a, b in zip(p, q)))
    return math.acos(max(-1.0, min(1.0, dot)))


q0 = (1.0, 0.0, 0.0, 0.0)
q1 = (0.0, 1.0, 0.0, 0.0)
q2 = (0.0, 0.0, 1.0, 0.0)
q3 = (0.0, 0.0, 0.0, 1.0)
q4 = (1.0 / math.sqrt(2.0), 0.0, 0.0, 1.0 / math.sqrt(2.0))

case_a = [(q0, q0), (q1, q2), (q0, q3), (q1, q0), (q0, q2), (q1, q3)]
case_b = [(a, b) for a in (q0, q1) for b in (q2, q3, q4)]


v.check("lcm for coprime 2 and 3", math.lcm(2, 3), 6, rel=0)
v.check("coprime product period", 2 * 3, 6, rel=0)
v.record(
    "CRT visits all pairs for k1=2,k2=3",
    sorted((t % 2, t % 3) for t in range(6)) == sorted((i, j) for i in range(2) for j in range(3)),
    computed=[(t % 2, t % 3) for t in range(6)],
    claimed="all six state-pairs exactly once",
)
v.check("case-a shared point distance", ds3(q0, q0), 0.0, abs_tol=0.0)
v.check("orthogonal quaternion distance", ds3(q1, q2), math.pi / 2.0, rel=1e-14)
v.check("case-b q0-q4 distance", ds3(q0, q4), math.pi / 4.0, rel=1e-14)
v.check("case-b minimum delta", min(ds3(a, b) for a, b in case_b), math.pi / 4.0, rel=1e-14)
v.record(
    "case-a is below Plateau threshold",
    min(ds3(a, b) for a, b in case_a) < EPS_P,
    computed=min(ds3(a, b) for a, b in case_a),
    claimed="delta < epsP",
)
v.record(
    "case-b is above Plateau threshold",
    min(ds3(a, b) for a, b in case_b) > EPS_P,
    computed=min(ds3(a, b) for a, b in case_b),
    claimed="delta >> epsP",
)
v.record(
    "heat depletion caveat is acknowledged",
    "h_0 \\cdot \\delta_h^{t^*}" in TEX and "boundary surface" in TEX,
    computed="open item O2 includes heat at resonance",
    claimed="large periods require a joint heat/coherence constraint",
)

v.record(
    "coprime integer periods are literally incommensurate",
    False,
    computed="integer periods with gcd(k1,k2)=1 are still commensurate because their ratio k1/k2 is rational and the lcm period is finite",
    claimed="incommensurate periods k1,k2 with gcd(k1,k2)=1",
    detail="Expected terminology fail.",
)
v.record(
    "geodesic proximity is equivalent to MDL score margin",
    False,
    computed="the definition uses MDL score difference against a shared goal; the theorem uses S3 pair-distance delta. Equal or close pair-distance does not generally imply a small score margin without a Lipschitz/monotonicity theorem tied to the same goal",
    claimed="joint Plateau exists iff delta(CA,CB) < epsP",
    detail="Expected bridge-lemma fail.",
)
v.record(
    "minimising resonance step is always unique",
    False,
    computed="CRT gives a unique t for a chosen pair (i*,j*), but multiple pairs can attain the same minimum delta, producing multiple resonance steps per period",
    claimed="when it exists, it occurs at the unique step t*",
    detail="Expected uniqueness fail.",
)
v.record(
    "P27 cross-coherence is equivalent to joint Plateau",
    False,
    computed="P27's C_A P_B = I and C_B P_A = I operator equalities are replaced by a proximity/MDL threshold, but no construction of C_A,C_B,P_A,P_B from the cycles proves the equivalence",
    claimed="P27 cross-coherence holds iff joint Plateau fixed point exists",
    detail="Expected proof-status fail.",
)
v.record(
    "Plateau firing produces a fixed point q* from proximity alone",
    False,
    computed="the Weld and Plateau update maps are not specified, so close proposals do not by themselves prove the post-Weld state is a fixed point",
    claimed="q* approximately equals both proposals and is a joint Plateau fixed point",
    detail="Expected dynamics fail.",
)
v.record(
    "commensurability is irrelevant without the gcd=1 assumption",
    False,
    computed="if gcd(k1,k2)>1, the combined trajectory visits only a subset of index pairs, so the closest geometric pair may be unreachable at any common step",
    claimed="commensurability governs when resonance occurs, not whether cycles are close enough",
    detail="Expected scope fail outside the theorem's coprime assumption.",
)
v.record(
    "irrational-winding limit guarantees any two subsystems cohere",
    False,
    computed="Weyl equidistribution applies only after specifying the same torus/flow and a target set of positive measure; arbitrary cycles or separated tori in S3 need not approach within epsP, and the O(1/epsP^2) waiting time is not derived",
    claimed="in the irrational-winding limit, any two Oscillate subsystems eventually achieve P27 coherence",
    detail="Expected ergodic-limit fail.",
)
v.record(
    "momentary Weld collapse is derived",
    False,
    computed="the paper states that the initial Weld forces a collapse to a single quaternion, but gives no Weld selection/update rule for that claim",
    claimed="initial Weld event forced momentary collapse",
    detail="Expected implementation gap.",
)

sys.exit(v.summary())