#!/usr/bin/env python3
"""
verify_P079.py -- Addendum 79: Spectral-Weight Saturation / OP-B-Mass.

This verifier checks the arithmetic in 79_Addendum_SWSClosure.tex and audits
the proof-status claims.  The basic sector-weight numerics reproduce: mu0,
mu1, MU, A(1)=mu0, the bulk-only competitor EB, and the mu0 gap all check.
The flagged issues are that Tr(Xsec^2) is printed about ten times too large,
the top-energy table is stale at the displayed precision, and the proof still
assumes rather than derives the top/e3 spectral-coordinate identification
needed to turn A(1)=mu0 into mt/mc=mu0.
"""

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 CheckResult, Verifier


class ModernVerifier(Verifier):
    """Local output adapter: inherits Verifier's tolerance logic unchanged,
    emits the corpus's modern check-line format (numbered [PASS]/[FAIL]
    lines, computed/claimed as indented info lines)."""

    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)
        desc = label if (ok or not detail) else f"{label} -- {detail}"
        print(f"  [{'PASS' if ok else 'FAIL'}] {n:>2}. {desc}")
        if computed != "" or claimed != "":
            print(f"        computed: {computed}")
            print(f"        claimed : {claimed}")
        if ok and detail:
            print(f"        {detail}")
        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 = ModernVerifier("P079 -- Spectral-Weight Saturation Closure")

ROOT = Path(__file__).resolve().parents[1]
TEX = (ROOT / "79_Addendum_SWSClosure.tex").read_text()
TEX_WORDS = " ".join(TEX.split())

PI = math.pi
MU0 = 4 * PI**3 + PI**2 + PI
MU1 = 16 * PI**3 / 5 + 3 * PI**2 / 4 + 2 * PI / 3
MU = MU1 / MU0

E_EDGE = PI
E_BOUNDARY = PI**2
E_BULK = 4 * PI**3
E_CHARM = E_EDGE + E_BOUNDARY
GAP_MU0 = math.log(MU0) / MU
E_TOP = E_CHARM + GAP_MU0
GAP_BULK = math.log(E_BULK) / MU
E_TOP_BULK = E_CHARM + GAP_BULK


def A(x: float) -> float:
    return PI * x**2 + PI**2 * x**3 + 4 * PI**3 * x**4


def root_for_accumulation(target: float) -> float:
    lo = 0.0
    hi = 1.0
    for _ in range(200):
        mid = (lo + hi) / 2
        if A(mid) < target:
            lo = mid
        else:
            hi = mid
    return (lo + hi) / 2


def pct(x: float) -> float:
    return 100 * x


v.check("mu0 total spectral weight", MU0, 137.036304, rel=5e-9)
v.check("mu1 first moment", MU1, 108.716684, rel=5e-9)
v.check("MU=mu1/mu0", MU, 0.793342, rel=5e-7)
v.check("edge sector weight", E_EDGE, PI, rel=1e-12)
v.check("boundary sector weight", E_BOUNDARY, PI**2, rel=1e-12)
v.check("bulk sector weight", E_BULK, 124.025, rel=1e-5)
v.check("charm energy pi+pi^2", E_CHARM, 13.011, rel=2e-5)

v.check("A(1)=mu0", A(1.0), MU0, rel=1e-12)
v.check("partial bulk integral", E_BULK, 4 * PI**3, rel=1e-12)
v.check("edge+boundary contribution", E_CHARM, E_EDGE + E_BOUNDARY, rel=1e-12)
v.check("bulk fraction EB/mu0", E_BULK / MU0, 0.9051, rel=6e-5)
v.check("sub-bulk fraction Ec/mu0", E_CHARM / MU0, 0.0949, rel=5e-4)

x_bulk = root_for_accumulation(E_BULK)
x_charm = root_for_accumulation(E_CHARM)
v.check("A^{-1}(EB) is below 1", x_bulk, 0.9746, rel=3e-5)
v.check("A(A^{-1}(EB))=EB", A(x_bulk), E_BULK, rel=1e-12)
v.check("A^{-1}(Ec)", x_charm, 0.53995, rel=2e-5)
v.check("A(A^{-1}(Ec))=Ec", A(x_charm), E_CHARM, rel=1e-12)

v.check("top/charm gap ln(mu0)/MU", GAP_MU0, 6.201, rel=2e-4)
v.check(
    "top energy table value",
    E_TOP,
    19.212,
    rel=2e-5,
    detail="Expected fail: exact Ec+ln(mu0)/MU is about 19.213118, so 19.212 is stale even at three decimals.",
)
v.check("predicted ratio exp(MU gap)=mu0", math.exp(MU * GAP_MU0), MU0, rel=1e-12)
v.check("bulk-only gap ln(EB)/MU", GAP_BULK, 6.077, rel=2e-4)
v.check("bulk-only top energy", E_TOP_BULK, 19.09, rel=2e-4)
v.check("bulk-only ratio", math.exp(MU * GAP_BULK), 124.0, rel=3e-4)
v.check("PDG residual using 137.06", pct((MU0 - 137.06) / 137.06), -0.017, rel=2e-2)

trace2 = E_EDGE**2 + E_BOUNDARY**2 + E_BULK**2
norm = E_EDGE * E_BOUNDARY * E_BULK
v.check(
    "Tr(Xsec^2) printed magnitude",
    trace2,
    150505.0,
    rel=1e-3,
    detail="Expected fail: pi^2+pi^4+16*pi^6 is about 15,489.506, not 150,505.",
)
v.check("cubic norm N(Xsec)", norm, 3848.0, rel=8e-4)

conditional_phrase = "If the top's mass-map image equals this accumulated weight" in TEX_WORDS
placeholder_formula = "^{\\,?}" in TEX or "^{?}" in TEX
rhon_undefined = "\\rho_{\\mathrm{n}}" in TEX and "normalisation factor" in TEX

v.record(
    "SWS proof is unconditional",
    not conditional_phrase,
    computed="conditional mass-map phrase present" if conditional_phrase else "no conditional phrase found",
    claimed="SWS is proved/OP-B-Mass is closed",
    detail="Expected proof-audit fail: Argument I still says mt/mc=mu0 only if the top's mass-map image equals A(1).",
)
v.record(
    "Peirce maximality derives x_t=1 rather than assuming the order-to-depth map",
    False,
    computed="e3 is maximal and rho_B peaks at x=1; no explicit map from top energy/state to x(E_t)=1 is constructed",
    claimed="top as e3 generator forces x_t=1",
    detail="Expected proof-audit fail: maximal idempotent -> endpoint is an added identification, not a derived consequence.",
)
v.record(
    "Z3 equivariance consistently turns an omega-eigenvalue ratio into a scalar invariant",
    False,
    computed="the ratio is assigned eigenvalue omega != 1, then set equal to the invariant trace",
    claimed="Z3 equivariance forces mt/mc=Tr(Xsec)",
    detail="Expected proof-audit fail: an omega-eigenvector is not a nonzero invariant without an additional projection/absolute-value construction.",
)
v.record(
    "Trace is the unique dimension-compatible invariant without extra assumptions",
    False,
    computed="linearity and normalization are asserted; symmetric functions such as sqrt(Tr(Xsec^2)) or rescaled polynomial invariants are not ruled out",
    claimed="only Tr(Xsec) can equal the ratio",
    detail="Expected proof-audit fail: uniqueness holds only after imposing unproved linearity/scale restrictions.",
)
v.record(
    "GON mass accumulation is fully specified",
    not rhon_undefined and not placeholder_formula,
    computed=f"rho_n mentioned={rhon_undefined}; placeholder exponents present={placeholder_formula}",
    claimed="GON integral closure proves the ratio",
    detail="Expected proof-audit fail: rho_n is not defined enough for verification and a displayed equation still contains question-mark exponents.",
)
v.record(
    "charm coordinate follows from the stated full-density equation",
    False,
    computed=f"A(x)=Ec has x≈{x_charm:.6f}; the proof cites the edge+boundary full-interval integral instead of deriving this depth from the mass map",
    claimed="x_c is determined by A(x_c)=Ec",
    detail="Expected proof-audit fail: the equation has a numerical solution, but the proof does not derive why charm must occupy that full-density depth.",
)
v.record(
    "P76 lambda=1 saturation can be imported as closed",
    False,
    computed="P76 verifier finds Z(lambda,0)=mu0 for every lambda, so lambda=1 is not selected at t=0",
    claimed="lambda=1 saturation uniquely gives the gap",
    detail="Expected inherited fail: P79 relies on the P76 closure claim as an established input.",
)
v.record(
    "OP-B-Mass closure status follows from the verified steps",
    False,
    computed="arithmetic supports the mu0 candidate, but the top/e3 -> A(1) mass-map step remains conditional",
    claimed="OP-B-Mass CLOSED",
    detail="Expected status fail: the verifier treats this as an unresolved proof gap, not a closed theorem.",
)

sys.exit(v.summary())