#!/usr/bin/env python3
"""
verify_P145.py -- Addendum 145: scope theorem.

This verifier checks the inherited P141 budget arithmetic and flags places
where the scope theorem's "if and only if" / non-derivability claims need
more formal definitions than the TeX supplies.
"""

from __future__ import annotations

import math
import sys
from pathlib import Path

sys.path.insert(0, str(Path(__file__).resolve().parent))
class Verifier:
    """Output shim: identical tolerance semantics to verify_common.Verifier,
    modern [PASS]/[FAIL] check-line output format."""

    def __init__(self, name):
        self.PASS = 0
        self.FAIL = 0
        self.n = 0
        print(name)

    def _mark(self, ok, desc):
        self.n += 1
        if ok:
            self.PASS += 1
        else:
            self.FAIL += 1
        print(f"  [{'PASS' if ok else 'FAIL'}] {self.n:>2}. {desc}")

    def check(self, 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}%"
        self._mark(ok, label + (f" -- {detail}" if detail else ""))
        print(f"        computed: {computed}   claimed: {claimed}   ({err_detail})")
        return ok

    def record(self, label, ok, computed="", claimed="", detail=""):
        ok = bool(ok)
        self._mark(ok, label + (f" -- {detail}" if detail else ""))
        if computed != "" or claimed != "":
            print(f"        computed: {computed}   claimed: {claimed}")
        return ok

    def summary(self):
        print(f"\n{'='*60}\nRESULT: {self.PASS} PASS / {self.FAIL} FAIL")
        return 0 if self.FAIL == 0 else 1


v = Verifier("P145 -- Scope Theorem")

ROOT = Path(__file__).resolve().parents[1]
TEX = (ROOT / "145_Addendum_ScopeTheorem.tex").read_text()
P141 = (ROOT / "141_Addendum_MultiPionContinuum.tex").read_text()

DA_HAD_TOE = 4.11e-3
DA_HAD_PDG = 0.02750
M_MU_GEV = 0.1057
M_RHO_GEV = 0.770
MU_CONF_GEV = 0.313
N_RESONANCES = 5
N_PARAMS = 2 * N_RESONANCES

alg_fraction = DA_HAD_TOE / DA_HAD_PDG
dyn_fraction = 1.0 - alg_fraction
muon_ratio = (M_MU_GEV / M_RHO_GEV) ** 2


v.check("P141 algebraic fraction", 100.0 * alg_fraction, 14.9, rel=4e-3)
v.check("P141 decoupled fraction", 100.0 * dyn_fraction, 85.1, rel=8e-4)
v.check("PDG/algebraic factor", DA_HAD_PDG / DA_HAD_TOE, 6.69, rel=2e-3)
v.check("five resonance pole parameter count", N_PARAMS, 10, rel=0)
v.check("muon g-2 scale ratio m_mu^2/M_rho^2", muon_ratio, 1.0 / 53.0, rel=3e-2)
v.check("confinement scale in GeV", MU_CONF_GEV, 0.313, rel=0)
v.record(
    "rho-pole / pion-continuum split is inherited from P141",
    "approximately $72\\%$" in P141 and "\\approx 28\\%" in TEX,
    computed="P141/P145 contain 28% rho-pole and 72% sub-threshold split",
    claimed="muon HVP is mostly dynamical",
)
v.record(
    "TOE declines to adjudicate lattice vs dispersive g-2",
    "neither adjudicates nor contributes to its resolution" in TEX,
    computed="explicit limitation present",
    claimed="g-2 lattice/dispersive dispute is outside algebraic sector",
)

v.record(
    "PEW-projectability is a formal decidable criterion",
    False,
    computed="the definition uses 'well-approximated', 'dominant support', and 'effectively supported' without a norm, tolerance, or computable support functional",
    claimed="boundary criterion classifies observables iff they are PEW-projectable",
    detail="Expected formal-definition fail.",
)
v.record(
    "scale criterion is an iff theorem from Q_eff >= M_rho",
    False,
    computed="a single peak scale does not determine a dispersive integral with low-energy tails and 1/s^n weights; no theorem bounds tail contributions or defines Q_eff uniquely",
    claimed="O is TOE-algebraic iff K_O has effective peak scale at or above M_rho",
    detail="Expected proof-status fail.",
)
v.record(
    "equation (alg) covers every listed algebraic observable",
    False,
    computed="alpha^-1, CKM angles, G_F, and sin^2(theta_W) are listed as algebraic but are not hadronic dispersion sums over the five vector-pole M_V,C_V data via equation (alg)",
    claimed="every algebraic observable is determined by the ten pole numbers plus JO data via eq. (alg) and O-hat",
    detail="Expected scope mismatch.",
)
v.record(
    "dimension argument proves non-derivability from JO dynamics",
    False,
    computed="R^10 and L2(R+) have the same set-theoretic cardinality; a dimension/non-surjectivity theorem needs a specified regularity class such as linear, smooth, algebraic, or continuous maps and a target topology",
    claimed="no map R^10 -> L2(R+) is surjective onto any open set",
    detail="Expected mathematical-hypothesis fail.",
)
v.record(
    "finite extensions can never derive QCD dynamics",
    False,
    computed="the proof rules out only the current finite-pole parameterization under extra regularity assumptions; it does not prove all future TOE extensions must add only finitely many algebraic parameters or cannot add a beta-function/dynamical equation",
    claimed="completing the corpus cannot change non-derivability of dynamics",
    detail="Expected overstatement fail.",
)
v.record(
    "generic QCD spectral functions are arbitrary non-negative L2 functions",
    False,
    computed="physical hadronic spectral functions obey analyticity, unitarity, thresholds, asymptotic QCD, and sum-rule constraints; treating them as arbitrary L2 functions overstates the target space",
    claimed="rho_had(s) is arbitrary non-negative function subject only to QCD unitarity",
    detail="Expected model-space fail.",
)
v.record(
    "algebraic-observable submanifold is explicitly constructed",
    False,
    computed="the corollary asserts a 10-dimensional submanifold and relations among EW observables, but no explicit embedding, rank calculation, or relation R is derived",
    claimed="two off-submanifold algebraic measurements falsify TOE",
    detail="Expected falsifiability-construction fail.",
)
v.record(
    "algebraic/dynamical independence is proved for physical observables",
    False,
    computed="Peirce-block orthogonality of model sectors does not by itself prove statistical/physical independence between measured algebraic and dynamical observables once shared SM inputs, running, and BSM effects are allowed",
    claimed="no universal relation exists between A and D observables",
    detail="Expected proof-status fail.",
)
v.record(
    "muon g-2 discrepancy cannot originate in algebraic sector",
    False,
    computed="the conclusion is conditional on the algebraic EW inputs and their TOE identifications; P145 does not propagate uncertainties or show that all algebraic-sector deformations are excluded",
    claimed="any g-2 tension must be in HVP/HLbL or BSM, not algebraic EW",
    detail="Expected conditional-scope fail.",
)
v.record(
    "scope theorem is independent of flagged upstream assumptions",
    False,
    computed="P145 relies on P136-P141 pole budgets and Peirce orthogonality; the current suite treats that chain as mostly arithmetic-consistent but still model-dependent rather than a fully formal non-derivability theorem",
    claimed="structural theorem follows from upstream addenda",
    detail="Expected dependency-status fail.",
)

sys.exit(v.summary())