#!/usr/bin/env python3
"""
verify_P146.py -- Addendum 146: observer inside the system.

This verifier checks the concrete operator/state-schema claims and flags the
places where existence of fixed/eigenstates is promoted to a full measurement
theory or Wheel implementation theorem without enough transition equations.
"""

from __future__ import annotations

import math
import sys
from pathlib import Path

sys.path.insert(0, str(Path(__file__).resolve().parent))

PASS = FAIL = 0
_N = 0


def check(n, desc, cond):
    global PASS, FAIL
    ok = bool(cond)
    PASS += ok
    FAIL += not ok
    print(f"  [{'PASS' if ok else 'FAIL'}] {n:>2}. {desc}")
    return ok


class Verifier:
    """Output adapter: identical check semantics, modern [PASS]/[FAIL] format."""

    def __init__(self, name):
        print(name)

    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}%"
        return self.record(label, ok, computed, claimed, detail, err_detail)

    def record(self, label, ok, computed="", claimed="", detail="", err_detail=""):
        global _N
        _N += 1
        desc = label + (f" -- {detail}" if detail else "")
        check(_N, desc, ok)
        if computed != "" or claimed != "":
            print(f"        computed: {computed}")
            print(f"        claimed : {claimed}")
        if err_detail:
            print(f"        {err_detail}")
        return ok

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


v = Verifier("P146 -- Observer Inside the System")

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

PI = math.pi
MU0 = 4.0 * PI**3 + PI**2 + PI


def rho_prime(x: float) -> float:
    return 48.0 * PI**3 * x**2 + 6.0 * PI**2 * x + 2.0 * PI


def v_sl(x: float) -> float:
    # E_self is positive in the corpus; its exact value is irrelevant for
    # non-negativity because both summands are non-negative on [0,1].
    e_self = 13.1767
    return rho_prime(x) ** 2 / (2.0 * MU0**2) + e_self * x**2 * (1.0 - x) ** 2


sample_points = [i / 20.0 for i in range(21)]

v.record(
    "WheelState schema has five visible components",
    "\\Sp \\times \\mathbb{R}_{\\geq 0} \\times \\mathcal{F} \\times \\{e, b, B\\} \\times \\{+,-\\}" in TEX,
    computed="q, heat, face proposals, layer, orientation",
    claimed="Wheel state space W",
)
v.record(
    "operator list has five named Wheel operators",
    all(name in TEX for name in ["Fork", "Weld", "Plateau", "Oscillate", "Perturb"]),
    computed="Fork/Weld/Plateau/Oscillate/Perturb present",
    claimed="five operators act on W",
)
v.record(
    "P7 boundary conditions are stated",
    "\\psi(0)=0" in TEX and "\\psi'(1)=0" in TEX,
    computed="mixed Dirichlet-Neumann boundary conditions present",
    claimed="operator domain is fixed enough for a Sturm-Liouville check",
)
v.record(
    "self-lensing potential is non-negative on sampled interval",
    all(v_sl(x) >= 0 for x in sample_points),
    computed=min(v_sl(x) for x in sample_points),
    claimed="V_sl(x) >= 0",
)
v.record(
    "bounded-interval Sturm-Liouville spectrum claim is plausible",
    "self-adjoint operator on $L^2([0,1])$" in TEX and "spectrum is discrete, real" in TEX,
    computed="regular finite-interval second-order operator with separated boundary conditions, assuming the stated domain",
    claimed="discrete real bounded-below spectrum",
)
v.record(
    "Type-2 provenance is absent from WheelState schema",
    "\\WS' = \\WS \\times \\Pi" in TEX and "does not carry a provenance field" in TEX,
    computed="provenance requires extension W x Pi",
    claimed="operator-provenance encoding is blocked by current schema",
)
v.record(
    "Con(TOE) and fixed-point convergence are separated",
    "Fixed-point convergence and formal consistency are orthogonal" in TEX,
    computed="P146 explicitly separates operational convergence from Con(TOE)",
    claimed="Type-1 self-observation is not an internal Con(TOE) proof",
)
v.record(
    "open composite-trajectory problem is acknowledged",
    "The most precise open question" in TEX and "combined\nstate" in TEX,
    computed="O4 states the remaining composite self-observation gap",
    claimed="closed Oscillate/Weld provenance is open",
)

v.record(
    "Plateau fixed points are constructed for every Hopf face",
    False,
    computed="P146 names centroids q_c^(k), layers, and orientations, but does not define the Hopf tiling, centroid formula, face set, or Plateau update map precisely enough to enumerate fixed points",
    claimed="W*_k are fixed points of Plateau for each face k",
    detail="Expected construction gap.",
)
v.record(
    "Fork/Weld heat conservation is proved from update equations",
    False,
    computed="the paper states a conservation law but gives no Fork/Weld heat update equations or invariant calculation",
    claimed="Fork-Weld cycle conserves heat like unitarity",
    detail="Expected proof-status fail.",
)
v.record(
    "one-clock argument proves Type-2 blocking is principled",
    False,
    computed="absence of a provenance field is a schema fact; the claim that any provenance component creates an impermissible second time axis is argued verbally, not derived from breath_period dynamics",
    claimed="operator-history provenance conflicts with the Ride Shai-Hulud pin",
    detail="Expected architecture-proof fail.",
)
v.record(
    "eigenstate discreteness solves the measurement problem",
    False,
    computed="existence of a discrete spectrum does not by itself supply Born probabilities, a collapse/update law for arbitrary states, decoherence behavior, or a link from eigenvalues to observed outcomes",
    claimed="TOE measurement problem dissolves with no external observer",
    detail="Expected interpretation-to-physics fail.",
)
v.record(
    "Hopf phase resolution is shown to be a Plateau fixed point",
    False,
    computed="the Hopf S1 phase and Plateau centroid map are not connected by an explicit map or contraction proof",
    claimed="trajectory's S1 component reaches a Plateau fixed point",
    detail="Expected derivation fail.",
)
v.record(
    "superpositions collapse on the next breath cycle",
    False,
    computed="no linear/nonlinear evolution rule is given for a superposition of observation eigenstates under Plateau, and no timescale theorem derives one-breath collapse",
    claimed="superposition is unstable and will Plateau-collapse on the next breath cycle",
    detail="Expected dynamics fail.",
)
v.record(
    "Butlerian line follows from kernel equations",
    False,
    computed="the kernel/witness boundary is asserted from Paper 29; P146 does not formalize the witness selection function or prove the kernel cannot select an operator from F_t",
    claimed="self-observation sustains rather than violates the Butlerian line",
    detail="Expected architecture-status fail.",
)
v.record(
    "closed Oscillate cycles are proven observers",
    False,
    computed="P146 explicitly leaves whether closed cycles of different periods constitute distinct observers as unresolved",
    claimed="closed trajectory = closed observer",
    detail="Expected open-item fail.",
)

sys.exit(v.summary())