#!/usr/bin/env python3
"""
verify_P143.py -- Addendum 143: Gödel incompleteness and TOE scope.

This verifier checks the concrete logical/numeric claims that can be inspected
locally and flags proof-scope issues in the mapping from Gödel/Tarski facts to
the current TOE corpus.
"""

from __future__ import annotations

import math
import re
import sys
from pathlib import Path



PASS = FAIL = 0
_N = 0

def record(label, ok, computed="", claimed="", detail=""):
    """Modern-format check line; behavior-preserving port of verify_common."""
    global PASS, FAIL, _N
    _N += 1
    ok = bool(ok)
    desc = label
    if ok:
        PASS += 1
    else:
        FAIL += 1
        if "Expected" in detail:
            i = detail.find("Expected")
            desc = f"{label} -- {detail[i:]}"
            detail = 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 detail:
        print(f"        {detail}")
    return ok

def check(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 record(label, ok, computed, claimed, err_detail + (f"; {detail}" if detail else ""))

print("P143 -- Godel Incompleteness Scope")

ADDENDA_ROOT = Path(__file__).resolve().parents[1]   # .../corpus/addenda
CORPUS_ROOT  = Path(__file__).resolve().parents[2]   # .../corpus
TEX = (ADDENDA_ROOT / "143_Addendum_GodelIncompleteness.tex").read_text()
P7 = (CORPUS_ROOT / "toe" / "07_Paper_SelfReferentialObservation.tex").read_text()
RESULTS = (ADDENDA_ROOT / "VERIFY_RESULTS.md").read_text() if (ADDENDA_ROOT / "VERIFY_RESULTS.md").exists() else ""

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


def current_flagged_count() -> int | None:
    match = re.search(r"- Flagged:\s+(\d+)", RESULTS)
    return int(match.group(1)) if match else None


record(
    "Godel first theorem preconditions are stated",
    "consistent, recursively axiomatizable formal system" in TEX and "interprets\n$Q$" in TEX,
    computed="consistency + recursive axiomatizability + Q interpretation stated",
    claimed="standard G1 preconditions",
)
record(
    "Godel second theorem is stated conditionally",
    "cannot prove its own consistency" in TEX and "\\mathrm{Con}(F)" in TEX,
    computed="conditional second incompleteness statement present",
    claimed="F cannot prove Con(F) under same hypotheses",
)
record(
    "Tarski RCF escape route is stated",
    "real closed fields" in TEX and "complete\nand decidable" in TEX,
    computed="Tarski completeness/decidability statement present",
    claimed="pure RCF does not satisfy Godel arithmetic precondition",
)
record(
    "Paper 7 number-theory overlay exists locally",
    all(fragment in P7 for fragment in ["Prime triplets", "Mersenne", "p \\times \\kappa"]),
    computed="P7 contains prime triplets and Mersenne resonance text",
    claimed="P7 imports number-theoretic content",
)
check("alpha inverse formula", ALPHA_INV, 137.0363037759, rel=2e-12)
check("alpha inverse rounded", ALPHA_INV, 137.036, rel=3e-6)
record(
    "candidate Con(TOE) is correctly identified as second-theorem-shaped",
    "\\mathrm{Con}(\\TOE)" in TEX and "canonical Gödel sentence" in TEX,
    computed="Con(TOE) candidate present",
    claimed="if extended TOE interprets Q, Con(TOE) is not internally provable",
)
record(
    "physical/formal completeness distinction is explicitly drawn",
    "Physical completeness" in TEX and "Formal completeness" in TEX and "orthogonal" in TEX,
    computed="semantic model vs syntactic proof-system distinction present",
    claimed="physical completeness and formal completeness are separate notions",
)
record(
    "G4 residual risk is acknowledged",
    "formal incompleteness touches physical completeness" in TEX and "not\nruled out" in TEX,
    computed="operational G4 caveat present",
    claimed="some formal incompleteness could affect a physical optimization claim",
)

flagged = current_flagged_count()
record(
    "no internal contradictions have been identified in the corpus",
    False,
    computed=f"current verifier report has {flagged} flagged scripts" if flagged is not None else "current verifier report unavailable",
    claimed="No internal contradictions have been identified across the 140-addendum corpus",
    detail="Expected corpus-status fail.",
)
record(
    "recursive axiomatization of TOE is actually supplied",
    False,
    computed="P143 asserts constructibility but gives no formal language, axiom schema, coding, or decision procedure for axiom membership",
    claimed="TOE is recursively axiomatizable in any reasonable formalization",
    detail="Expected formalization gap.",
)
record(
    "geometric fragment completeness follows directly from Tarski",
    False,
    computed="S3/quaternion/Jordan polynomial fragments can often be encoded over RCF, but P1-P6 and P27-P30 include named constants, analytic/spectral claims, and physical interpretation layers not reduced here to first-order RCF formulas",
    claimed="purely geometric TOE fragment is likely complete by Tarski's theorem",
    detail="Expected conditional-scope fail.",
)
record(
    "P7 self-referential eigenproblem is fully grounded by supplied hypotheses",
    False,
    computed="self-adjointness, operator domain, boundary conditions, potential normalization, and compact-resolvent/discrete-spectrum proof are not supplied in P143 and are not reproducible from P7 alone",
    claimed="P7 loop terminates because O is self-adjoint, bounded below, and has a discrete real spectrum",
    detail="Expected solver/proof-status fail.",
)
record(
    "alpha uniqueness claim is literally a Godel sentence",
    False,
    computed="the uniqueness statement is not a diagonal fixed point asserting its own unprovability; it may be an open independence/rigidity claim, but P143 does not construct a G_F for it",
    claimed="sharpest candidate undecidable/Godel sentence is uniqueness of alpha^-1",
    detail="Expected logic-scope fail.",
)
record(
    "all admissible TOE variants are formalized for Candidate G1",
    False,
    computed="no grammar or decidable enumeration of admissible densities/geometries is defined, so the universal quantifier over TOE variants is not a formal sentence yet",
    claimed="G1 quantifies over all consistent (B^n,S^{n-1})-type densities",
    detail="Expected formal-language fail.",
)
record(
    "J3(O) classification proves Wheel-operator uniqueness",
    False,
    computed="P143 itself says the connection from exceptional Jordan-algebra classification to the specific Wheel operator map requires extra structural arguments not currently axiomatized",
    claimed="Candidate G2 may settle assembly uniqueness",
    detail="Expected acknowledged-open fail.",
)
record(
    "formal incompleteness cannot affect any physical prediction",
    False,
    computed="P143 later acknowledges the G4 case where full-pipeline theta* isolation could be operationally physical and internally unprovable",
    claimed="physical predictions are unaffected by whether asserting sentences are formally provable",
    detail="Expected overstatement fail.",
)

print(f"\n{'='*60}\nRESULT: {PASS} PASS / {FAIL} FAIL")
sys.exit(0 if FAIL == 0 else 1)