#!/usr/bin/env python3
"""
verify_P149.py -- Addendum 149: Plateau convergence and local consistency.

P149 is mainly a proof-scope addendum. This verifier checks the concrete
formula content that can be tested directly, then flags the places where the
paper promotes analytical or geometric statements into first-order real-closed
field/Tarski claims too quickly.
"""

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 adapter: identical tolerance logic, modern output 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)
        desc, info = label, detail
        i = detail.find("Expected")
        if i >= 0:
            desc = f"{label} -- {detail[i:]}"
            info = 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 info:
            print(f"        {info}")
        return bool(ok)

    def summary(self) -> int:
        passed = sum(bool(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("P149 -- Plateau Consistency / Tarski Fragment")

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

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


def rho_prime(x: float) -> float:
    # rho(x)=16*pi^3*x^3 + 3*pi^2*x^2 + 2*pi*x in the core density papers.
    return 48.0 * PI**3 * x**2 + 6.0 * PI**2 * x + 2.0 * PI


def v_sl(x: float) -> float:
    return rho_prime(x) ** 2 / (2.0 * MU0**2) + E_SELF * x**2 * (1.0 - x) ** 2


def heat_after_plateau(q_already_centroid: bool, h: float) -> str:
    if q_already_centroid:
        return "0"
    if h > 0:
        return "some h' with 0 <= h' < h, not specified as zero"
    return "0"


grid = [i / 200.0 for i in range(201)]
min_rho_prime = min(rho_prime(x) for x in grid)
min_v = min(v_sl(x) for x in grid)

v.record(
    "P146 O3 separation is explicitly stated",
    "\\mathrm{Con}(\\mathrm{TOE})" in TEX
    and "Fixed-point convergence" in TEX
    and "formal consistency are therefore orthogonal" in TEX,
    computed="operational Plateau convergence separated from formal consistency",
    claimed="P149 resolves what convergence proves",
)
v.record(
    "Con(TOE) is correctly identified as arithmetical/meta-theoretic",
    "\\mathrm{Prov}_{\\rm TOE}(n)" in TEX and "\\mathbb{N}" in TEX,
    computed="Con(TOE) described via quantification over proof codes",
    claimed="formal consistency is not a real-variable Plateau statement",
)
v.check("mu0 inherited density integral", MU0, 137.036303776, rel=2e-9)
v.check("rho prime lower endpoint", rho_prime(0.0), 2.0 * PI, rel=1e-12)
v.record(
    "rho prime is positive on [0,1]",
    min_rho_prime > 0.0,
    computed=f"grid min rho'(x)={min_rho_prime:.12f}; coefficients are positive so the analytic minimum is at x=0",
    claimed="rho'(x)^2 term is nonnegative",
)
v.record(
    "quartic heat-well term is nonnegative on [0,1]",
    all(x**2 * (1.0 - x) ** 2 >= 0.0 for x in grid),
    computed="x^2(1-x)^2 >= 0 on sampled grid and algebraically as a square product",
    claimed="E_self*x^2(1-x)^2 >= 0",
)
v.record(
    "V_sl is nonnegative on [0,1]",
    min_v > 0.0,
    computed=f"grid min V_sl={min_v:.12g}; analytic lower bound includes rho'(0)^2/(2*mu0^2)>0",
    claimed="V_sl(x) >= 0",
)
v.record(
    "bounded-below observation operator follows conditionally",
    min_v >= 0.0,
    computed="-d^2/dx^2 plus nonnegative regular potential is bounded below under standard boundary conditions",
    claimed="O_hat has bounded-below spectrum",
    detail="This checks the analytical direction, not the formal Tarski-fragment claim.",
)
v.record(
    "Type-1 fixed point equation is tautological under the given definition",
    "Plateau}(W^*_k) = W^*_k" in TEX and "(q^*_k, 0, \\emptyset" in TEX,
    computed="if q=q*_k and h=0, the displayed Plateau rule leaves the state fixed",
    claimed="W*_k is a Plateau fixed point",
)
v.record(
    "paper keeps local consistency distinct from global consistency",
    "face-by-face" in TEX and "globally stable" in TEX,
    computed="local geometric statement is explicitly scoped",
    claimed="local consistency at face k",
)
v.record(
    "limited provenance caveat is present",
    "does not uniquely reconstruct the full orbit" in TEX,
    computed="P149 says post-Weld geometry only constrains the orbit",
    claimed="partial, not complete, provenance",
)
v.record(
    "O1 admits spectral coverage is not proved",
    "Spectral coverage of Hopf faces" in TEX and "should" in TEX and "made precise" in TEX,
    computed="open item found",
    claimed="counting argument needs direct calculation",
)
v.record(
    "O3 states the eigenvalue-family assignment is arithmetical",
    "fermion family" in TEX and "family assignment is arithmetic" in TEX,
    computed="P149 separates analytic eigenvalue existence from arithmetic family assignment",
    claimed="Tarski/Godel boundary for P7 formal status",
)

v.record(
    "compact geodesic region on S3 guarantees unique centroid",
    False,
    computed="compactness/geodesic convexity alone is not enough globally on S3; uniqueness needs radius/hemisphere or strict convexity hypotheses and explicit face geometry",
    claimed="the centroid of a compact geodesically convex region on S3 is unique",
    detail="Expected proof-scope fail.",
)
v.record(
    "Plateau reaches W_f* after one application for welded states",
    False,
    computed=heat_after_plateau(False, 1.0),
    claimed="Plateau(W_comp)=W_f* after one application even when h_c>0",
    detail="The displayed rule only says h'<h for h>0; it does not set heat to zero unless the input is already at q*_k.",
)
v.record(
    "countably many eigenstates force every finite Hopf face to have one",
    False,
    computed="a countable basis and finitely many faces do not imply one eigenstate is supported in each face; support/sector decomposition must be constructed",
    claimed="each face is covered by counting arguments",
    detail="Expected logic fail; P149 also lists this as O1.",
)
v.record(
    "discrete spectrum and eigenbasis are first-order RCF claims",
    False,
    computed="self-adjointness, compact resolvent, discreteness, and orthonormal bases are Hilbert-space/functional-analytic statements, not first-order real-closed-field sentences",
    claimed="Theorem (ii) is provable in the first-order theory of real closed fields",
    detail="Expected formal-fragment fail.",
)
v.record(
    "the whole Plateau theorem is a pure Tarski-fragment sentence",
    False,
    computed="the proof uses geodesic centroids, spectral theorem language, pi/E_self constants, and operator-domain assumptions not encoded as a displayed polynomial RCF formula",
    claimed="all Plateau fixed-point subclaims are sentences of real closed field theory",
    detail="Expected formalization fail.",
)
v.record(
    "post-Weld provenance constraint is necessarily a non-empty arc",
    False,
    computed="on S3, the preimage of a face under q -> geo_mid(q,q*_j) is generally a region requiring explicit face inequalities; an 'arc' is not derived",
    claimed="q_c is constrained to a non-empty arc on S3",
    detail="Expected geometry/provenance fail.",
)
v.record(
    "geodesic midpoint and face membership are fully specified as semi-algebraic",
    False,
    computed="face inequalities and non-antipodal midpoint branch conditions are not supplied in this TeX",
    claimed="composite analysis is entirely a Tarski-fragment argument",
    detail="Expected formalization fail.",
)

sys.exit(v.summary())