#!/usr/bin/env python3
"""TGA 2.1: geometric membership and path-equality certificates.

Extends the frozen TGA 2.0 verifier. It does not rewrite those bytes.
Not a general theorem prover. Numerical checks never mint exact certificates.
Python 3.10+, standard library only. Explicit checks stay active under -O.
"""
from __future__ import annotations

import argparse
import cmath
import hashlib
import html
import importlib.util
import json
import math
import sys
from pathlib import Path
from typing import Any

HERE = Path(__file__).resolve().parent
TGA20_DIR = HERE.parent / "2.0"
PROOFS_PATH = HERE / "PROOFS.md"
HTML_PATH = HERE / "PROOFS.html"

TGA20_FILES = {
    "README.md": (4659, "15c9e0d41de985fc17acdf387451ed9b3bfe63d4c2fd0d0596a3ada7399c2cea"),
    "PROOFS.md": (12388, "b7527c0a59401c2fcd33d4a5823f048583c33b78ea5e6c2d0b0e14dd6fe72393"),
    "tga_verifier.py": (31934, "4339aee9680052fd7e4bf3f6d6b26eba9de62dd9ea7e6a6f947991a8a95646e5"),
    "test_tga.py": (10454, "5abc83184053ccdbed6942064177879c6277c236cfa865120eaef16e7f19c0ed"),
    "graph-report.json": (67008, "0092e5973be596bd74fffddfd267f2de8c03bd18b07bfac7bef472d78782acd5"),
    "execution.json": (1056, "479f0c22d7ea2c446764af1fdbc863a6912bde8be6584e4709c1fe1fc9bd165b"),
    "tests-normal.txt": (3155, "8866056e6f59ec8ff84a8f6939c15586135e2ac2ffc85652b6ffe226d2629a28"),
    "tests-optimized.txt": (3155, "0ea88c02d528207fa69d9fca6a305d697e02ce36aeb12f7b0dfdaf0c9fe34b10"),
    "demo.txt": (24, "2493c6745022b1c4246078013db5f7a29602d2f7c9b4f825b3bb44914d635c41"),
    "SHA256SUMS.txt": (721, "1cf5967a0501bf7ed52c724315257e562e2236bda3ec1fa596d7016f9e0ad783"),
}

PROB_SUM_ABS_TOL = 1e-12
CENTER_FACTOR = 1e-10
GAP_ABS_TOL = 1e-9
GAP_REL_TOL = 1e-8
POSITIVE_SCALE_FLOOR = 1e-9
PATH_TOL = 1e-8
FOURIER_TOL = 1e-8
C0 = math.cos(math.pi / 1296000)
CANONICAL_EPSILON = math.pi / 648000
PHI = (1 + math.sqrt(5)) / 2

SCHEMA_SOFTMAX = "tga.2.1/proof/softmax-scale-power"
SCHEMA_FOURIER = "tga.2.1/proof/fourier-mark-scale"
OP_SCALE = "tga.2.1/M_r"
OP_SOFTMAX = "tga.2.1/S_beta"
OP_LOG = "tga.2.1/L_beta"
OP_POWER = "tga.2.1/P_r"
OP_FOURIER = "tga.2.1/F"
OP_FOURIER_INV = "tga.2.1/F_inverse"
OP_DSCALE = "tga.2.1/D_r"


class Reject(ValueError):
    def __init__(self, message: str, code: str = "REJECTED") -> None:
        super().__init__(message)
        self.code = code


def need(condition: bool, message: str, code: str = "REJECTED") -> None:
    if not condition:
        raise Reject(message, code)


def load_tga20():
    """Load the published TGA 2.0 module after checking its release hashes."""
    for name, (size, digest) in TGA20_FILES.items():
        blob = (TGA20_DIR / name).read_bytes()
        if len(blob) != size or hashlib.sha256(blob).hexdigest() != digest:
            raise SystemExit(f"TGA 2.0 file changed or missing: {name}")
    path = TGA20_DIR / "tga_verifier.py"
    spec = importlib.util.spec_from_file_location("tga20_frozen", path)
    if spec is None or spec.loader is None:
        raise SystemExit("cannot load TGA 2.0 verifier")
    module = importlib.util.module_from_spec(spec)
    sys.modules["tga20_frozen"] = module
    spec.loader.exec_module(module)
    return module


tga20 = load_tga20()
LABELS = tga20.LABELS
LAMBDA = tga20.LAMBDA

POSITIVE = tga20.TypeSpec(
    "PositiveProbabilityVector", 6, LABELS,
    ("sum=1", "strictly positive", "dimensionless", "fixed label order", "beta is not part of this type"),
)
SIX = tga20.TypeSpec(
    "SixMarkProbability", 6, LABELS,
    ("positive probability vector", "six-mark gap conditions", "beta declared separately"),
)
MARKED = tga20.TypeSpec(
    "MarkedFourierImage", 6, LABELS,
    ("W0=6*c0", "W_{6-k}=-conjugate(W_k) for k=1..5", "full complex phase retained", "unnormalized DFT"),
)
GAPS = tga20.TypeSpec(
    "SixMarkGapConditions", 5, ("g1", "g2", "g3", "g4", "g5"),
    ("consecutive log ratios", "exact real statement"),
)
TYPE_BY_NAME = {
    "CenteredMarks": tga20.CENTER,
    "PositiveProbabilityVector": POSITIVE,
    "SixMarkProbability": SIX,
    "MarkedFourierImage": MARKED,
    "SixMarkGapConditions": GAPS,
}

TOLERANCE_POLICY = {
    "gap_absolute": GAP_ABS_TOL,
    "gap_relative": GAP_REL_TOL,
    "positive_scale_floor": POSITIVE_SCALE_FLOOR,
    "probability_sum_absolute": PROB_SUM_ABS_TOL,
    "centering": "abs(sum) <= 1e-10 * max(1, max abs coordinate)",
    "s_band": "1e-9 + 1e-8 * max(1, abs(s)); s is never rewritten into (0, 1]. An excess over 1 of at most 1e-12 is endpoint roundoff at epsilon=pi.",
    "phi": "binary64 (1+sqrt(5))/2, not a Q(sqrt(5)) certificate",
    "exact_membership_certificate": "never issued from binary64 agreement",
}


def as_tuple(value: Any) -> tuple:
    if isinstance(value, list):
        return tuple(value)
    return value


def resolve_beta(beta: Any) -> tuple[float, str]:
    if beta is None:
        return float(LAMBDA), "phi/(phi+pi)"
    if isinstance(beta, bool) or not isinstance(beta, (int, float)):
        raise Reject("beta must be a real number", "PARAMETER_REJECTED")
    beta = float(beta)
    if not math.isfinite(beta) or beta <= 0:
        raise Reject("beta must be finite and > 0", "PARAMETER_REJECTED")
    return beta, "numeric"


def resolve_r(r: Any) -> float:
    if isinstance(r, bool) or not isinstance(r, (int, float)):
        raise Reject("r must be a real number", "PARAMETER_REJECTED")
    r = float(r)
    if not math.isfinite(r) or r <= 0:
        raise Reject("r must be finite and > 0", "PARAMETER_REJECTED")
    return r


def configuration(beta: float, declaration: str, *, r: float | None = None, extra: dict | None = None) -> dict:
    cfg = {
        "beta": beta,
        "beta_declaration": declaration,
        "coordinate_units": "dimensionless",
        "label_order": list(LABELS),
    }
    if r is not None:
        cfg["r"] = r
    if extra:
        cfg.update(extra)
    return cfg


def as_centered(value: Any) -> tuple[float, ...]:
    value = as_tuple(value)
    need(isinstance(value, tuple) and len(value) == 6, "six ordered components required", "CONTRACT_VIOLATION")
    need(all(type(v) in (int, float) and not isinstance(v, bool) for v in value), "real components required", "CONTRACT_VIOLATION")
    need(all(math.isfinite(v) for v in value), "nonfinite centered coordinates", "NONFINITE")
    coords = tuple(float(v) for v in value)
    scale = max(1.0, max(abs(v) for v in coords))
    need(abs(math.fsum(coords)) <= CENTER_FACTOR * scale, "centering precondition", "CONTRACT_VIOLATION")
    return coords


def as_probability(value: Any) -> tuple[float, ...]:
    value = as_tuple(value)
    need(isinstance(value, tuple) and len(value) == 6, "six ordered probabilities required", "CONTRACT_VIOLATION")
    need(all(type(v) in (int, float) and not isinstance(v, bool) for v in value), "real probabilities required", "CONTRACT_VIOLATION")
    need(all(math.isfinite(v) for v in value), "nonfinite probability", "NONFINITE")
    if not all(v > 0 for v in value):
        raise Reject("strictly positive probabilities required", "NOT_STRICTLY_POSITIVE")
    coords = tuple(float(v) for v in value)
    if abs(math.fsum(coords) - 1.0) > PROB_SUM_ABS_TOL:
        raise Reject("malformed normalization; probabilities are not rescaled", "MALFORMED_NORMALIZATION")
    return coords


def as_spectrum(value: Any) -> tuple[complex, ...]:
    value = as_tuple(value)
    need(isinstance(value, tuple) and len(value) == 6, "six Fourier bins required", "CONTRACT_VIOLATION")
    out = []
    for item in value:
        if isinstance(item, bool) or not isinstance(item, (int, float, complex)):
            raise Reject("complex Fourier bins required", "CONTRACT_VIOLATION")
        number = complex(item)
        if not (math.isfinite(number.real) and math.isfinite(number.imag)):
            raise Reject("nonfinite Fourier bin", "NONFINITE")
        out.append(number)
    return tuple(out)


def require_marked_image(spectrum: tuple[complex, ...]) -> tuple[complex, ...]:
    if abs(spectrum[0] - 6 * C0) > FOURIER_TOL * max(1.0, abs(spectrum[0])):
        raise Reject("DC bin is not 6 c0 for a centered marked image", "CONTRACT_VIOLATION")
    for k in range(1, 6):
        left = spectrum[6 - k]
        right = -spectrum[k].conjugate()
        if abs(left - right) > FOURIER_TOL * max(1.0, abs(spectrum[k]), abs(left)):
            raise Reject("marked Fourier conjugate symmetry failed", "CONTRACT_VIOLATION")
    return spectrum


def logsumexp(values: tuple[float, ...]) -> tuple[float, ...]:
    if any(not math.isfinite(v) for v in values):
        raise Reject("nonfinite exponential input", "NONFINITE")
    top = max(values)
    terms = []
    for value in values:
        term = math.exp(value - top)
        if term == 0.0 or not math.isfinite(term):
            raise Reject("numerical result has left the supported positive domain", "LEFT_POSITIVE_DOMAIN")
        terms.append(term)
    total = math.fsum(terms)
    if not math.isfinite(total) or total <= 0:
        raise Reject("numerical result has left the supported positive domain", "LEFT_POSITIVE_DOMAIN")
    out = []
    for term in terms:
        prob = term / total
        if prob <= 0.0 or not math.isfinite(prob):
            raise Reject("numerical result has left the supported positive domain", "LEFT_POSITIVE_DOMAIN")
        out.append(prob)
    return tuple(out)


def softmax(z: Any, beta: Any) -> tuple[float, ...]:
    beta_value, _declaration = resolve_beta(beta)
    return logsumexp(tuple(beta_value * v for v in as_centered(z)))


def centered_log(p: Any, beta: Any) -> tuple[float, ...]:
    beta_value, _declaration = resolve_beta(beta)
    probs = as_probability(p)
    logs = tuple(math.log(v) for v in probs)
    if any(not math.isfinite(v) for v in logs):
        raise Reject("nonfinite logarithm", "NONFINITE")
    mean = math.fsum(logs) / 6
    return as_centered(tuple((v - mean) / beta_value for v in logs))


def scale_marks(z: Any, r: Any) -> tuple[float, ...]:
    factor = resolve_r(r)
    scaled = tuple(factor * v for v in as_centered(z))
    if any(not math.isfinite(v) for v in scaled):
        raise Reject("nonfinite scaling", "NONFINITE")
    return as_centered(scaled)


def power_probability(p: Any, r: Any) -> tuple[float, ...]:
    probs = as_probability(p)
    factor = resolve_r(r)
    if factor == 1.0:
        return probs
    logs = []
    for value in probs:
        log_value = math.log(value)
        if not math.isfinite(log_value):
            raise Reject("nonfinite logarithm", "NONFINITE")
        powered = factor * log_value
        if not math.isfinite(powered):
            raise Reject("nonfinite power", "NONFINITE")
        logs.append(powered)
    return logsumexp(tuple(logs))


def dft(values: tuple[complex, ...], inverse: bool = False) -> tuple[complex, ...]:
    sign = 1 if inverse else -1
    scale = 6 if inverse else 1
    out = []
    for k in range(6):
        total = 0j
        for j in range(6):
            total += values[j] * cmath.exp(sign * 2j * math.pi * j * k / 6)
        out.append(total / scale)
    return tuple(out)


def marked_fourier(z: Any) -> tuple[complex, ...]:
    coords = as_centered(z)
    baseline = tuple(complex(C0, v) for v in coords)
    return require_marked_image(dft(baseline))


def marked_fourier_inverse(spectrum: Any) -> tuple[float, ...]:
    image = require_marked_image(as_spectrum(spectrum))
    restored = dft(image, inverse=True)
    for value in restored:
        if abs(value.real - C0) > 1e-6:
            raise Reject("inverse left the complex-mark image", "CONTRACT_VIOLATION")
    return as_centered(tuple(value.imag for value in restored))


def scale_fourier(spectrum: Any, r: Any) -> tuple[complex, ...]:
    factor = resolve_r(r)
    image = require_marked_image(as_spectrum(spectrum))
    scaled = (image[0],) + tuple(factor * image[k] for k in range(1, 6))
    if any(not (math.isfinite(v.real) and math.isfinite(v.imag)) for v in scaled):
        raise Reject("nonfinite Fourier scaling", "NONFINITE")
    return require_marked_image(scaled)


def geometry_marks(a: Any, epsilon: Any) -> tuple[float, ...]:
    if isinstance(a, bool) or isinstance(epsilon, bool) or not isinstance(a, (int, float)) or not isinstance(epsilon, (int, float)):
        raise Reject("invalid geometry parameters", "PARAMETER_REJECTED")
    if not math.isfinite(a) or not math.isfinite(epsilon):
        raise Reject("nonfinite geometry", "NONFINITE")
    if not (a > 0 and 0 < float(epsilon) <= math.pi):
        raise Reject("invalid geometry parameters; require a > 0 and 0 < epsilon <= pi", "PARAMETER_REJECTED")
    s = math.sin(float(epsilon) / 2)
    big_a = s + PHI * PHI
    big_b = s + 1.0
    return as_centered(tuple(float(a) * v for v in (-big_a, -big_b, -s, s, big_b, big_a)))


def _gap_band(magnitude: float) -> float:
    return GAP_ABS_TOL + GAP_REL_TOL * abs(magnitude)


def _s_band(s: float) -> float:
    return GAP_ABS_TOL + GAP_REL_TOL * max(1.0, abs(s))


def _close(left: float, right: float) -> bool:
    return abs(left - right) <= _gap_band(max(abs(left), abs(right)))


def six_mark_membership(p: Any, beta: Any = None, mode: str = "family") -> dict:
    """Numerical six-mark test. Never returns an exact membership certificate."""
    base = {
        "exact_membership_certificate": None,
        "reversible_badge": False,
        "label_order": list(LABELS),
        "tolerance_policy": TOLERANCE_POLICY,
        "framework": "Centered log-ratio coordinates and Aitchison powering are the general equivalence. They are not six-mark membership.",
    }
    if mode not in ("family", "canonical"):
        return {**base, "probability_type": None, "six_mark_type": None, "numerical_status": "PARAMETER_REJECTED",
                "recovered": None, "detail": "mode must be family or canonical"}
    try:
        beta_value, declaration = resolve_beta(beta)
    except Reject as exc:
        return {**base, "probability_type": None, "six_mark_type": None, "numerical_status": exc.code,
                "recovered": None, "detail": str(exc)}
    try:
        probs = as_probability(p)
    except Reject as exc:
        return {**base, "probability_type": "not_a_positive_probability_vector", "probability_rejection": exc.code,
                "six_mark_type": "not_applicable", "numerical_status": exc.code, "recovered": None,
                "conditions": [], "residuals": None, "detail": str(exc)}
    gaps = tuple(math.log(probs[i + 1] / probs[i]) for i in range(5))
    g1, g2, g3, g4, g5 = gaps
    s_value = None if g2 == 0 else g3 / (2 * g2)
    canonical_target = 2 * math.sin(math.pi / 1296000) * g2
    residuals = {
        "g2_minus_g4": g2 - g4,
        "g1_minus_phi_g2": g1 - PHI * g2,
        "g5_minus_phi_g2": g5 - PHI * g2,
        "g2": g2,
        "g3": g3,
        "s_unclamped": s_value,
        "canonical_gap_residual": g3 - canonical_target,
    }
    result = {
        **base,
        "probability_type": "valid_positive_probability_vector",
        "mode": mode,
        "beta": beta_value,
        "beta_declaration": declaration,
        "gaps": list(gaps),
        "residuals": residuals,
        "recovered": None,
        "diagnostics": {
            "a_estimate": (g2 / beta_value) if g2 > 0 and math.isfinite(g2) else None,
            "s_unclamped": s_value,
            "epsilon": None,
        },
    }

    def conditions(statuses: dict[str, str]) -> list[dict]:
        return [
            {"id": "g2_eq_g4", "statement": "g2 = g4", "residual": g2 - g4, "status": statuses["g2_eq_g4"]},
            {"id": "g2_positive", "statement": "g2 = g4 > 0", "residual": g2, "status": statuses["g2_positive"]},
            {"id": "g1_eq_phi_g2", "statement": "g1 = phi g2", "residual": g1 - PHI * g2, "status": statuses["g1"]},
            {"id": "g5_eq_phi_g2", "statement": "g5 = phi g2", "residual": g5 - PHI * g2, "status": statuses["g5"]},
            {"id": "g3_range", "statement": "0 < g3 <= 2 g2", "residual": s_value, "status": statuses["g3"]},
            {"id": "canonical_angle", "statement": "g3 = 2 sin(pi/1296000) g2", "residual": g3 - canonical_target,
             "status": statuses["canonical"]},
        ]

    if g2 <= 0:
        result.update(numerical_status="not_positive_scale", six_mark_type="not_the_positive_scale_family",
                      detail="Valid probability data, but g2 is not a positive scale. Uniform data is in this class.")
        result["conditions"] = conditions({"g2_eq_g4": "fail" if not _close(g2, g4) else "not_applicable",
                                            "g2_positive": "fail", "g1": "not_applicable", "g5": "not_applicable",
                                            "g3": "not_applicable", "canonical": "not_applicable"})
        return result
    if g2 <= POSITIVE_SCALE_FLOOR:
        result.update(numerical_status="uncertain_boundary", six_mark_type="uncertain_boundary",
                      detail="g2 is positive but inside the tolerance of zero. s is not forced into (0, 1].")
        result["conditions"] = conditions({"g2_eq_g4": "uncertain", "g2_positive": "uncertain", "g1": "uncertain",
                                            "g5": "uncertain", "g3": "uncertain", "canonical": "not_applicable"})
        return result

    equal = _close(g2, g4) and _close(g1, PHI * g2) and _close(g5, PHI * g2)
    if not math.isfinite(s_value):
        result.update(numerical_status="NONFINITE", six_mark_type="not_applicable", detail="nonfinite gap ratio")
        result["conditions"] = conditions({"g2_eq_g4": "fail", "g2_positive": "pass", "g1": "fail", "g5": "fail",
                                            "g3": "fail", "canonical": "not_applicable"})
        return result
    band = _s_band(s_value)
    endpoint_roundoff = False
    if s_value > 1 and s_value - band > 1:
        s_status = "fail"
    elif s_value > 1 and s_value - 1 <= 1e-12:
        s_status = "pass"
        endpoint_roundoff = True
    elif s_value > 1:
        s_status = "uncertain"
    elif s_value <= 0 and s_value + band <= 0:
        s_status = "fail"
    elif s_value <= 0:
        s_status = "uncertain"
    elif s_value <= band:
        s_status = "uncertain"
    else:
        s_status = "pass"
    canonical_ok = _close(g3, canonical_target)
    statuses = {
        "g2_eq_g4": "pass" if _close(g2, g4) else "fail",
        "g2_positive": "pass",
        "g1": "pass" if _close(g1, PHI * g2) else "fail",
        "g5": "pass" if _close(g5, PHI * g2) else "fail",
        "g3": s_status,
        "canonical": "pass" if canonical_ok else "fail",
    }
    result["conditions"] = conditions(statuses)
    if not equal or s_status == "fail":
        result.update(numerical_status="not_member", six_mark_type="not_the_six_mark_family",
                      detail="Valid positive probability vector. The six-mark gap conditions fail. s was not clamped.")
        return result
    if s_status == "uncertain":
        result.update(numerical_status="uncertain_boundary", six_mark_type="uncertain_boundary",
                      detail="Gap equalities are close, but s is too close to a boundary to force it into (0, 1].")
        return result
    epsilon = math.pi if endpoint_roundoff else 2 * math.asin(s_value)
    result["diagnostics"]["epsilon"] = epsilon
    result["diagnostics"]["endpoint_roundoff"] = endpoint_roundoff
    recovered = {"a": g2 / beta_value, "s": s_value, "epsilon": epsilon, "beta": beta_value,
                 "beta_declaration": declaration, "label_order": list(LABELS),
                 "endpoint_roundoff": endpoint_roundoff}
    if mode == "canonical" and not canonical_ok:
        result.update(numerical_status="not_canonical_angle", six_mark_type="six_mark_family_not_canonical_angle",
                      family_numerical_status="numerically_consistent", recovered=recovered,
                      detail="Numerically consistent with the wider family, not with the canonical angle. This is not an exact certificate.")
        return result
    result.update(numerical_status="numerically_consistent", six_mark_type="numerically_consistent_six_mark_family",
                  recovered=recovered, canonical_angle=bool(canonical_ok),
                  detail="Binary64 consistency only. Not an exact membership certificate.")
    return result


def _ok(operation: str, cfg: dict, value: Any, detail: str) -> dict:
    return {"status": "ok", "operation": operation, "configuration": cfg, "value_raw": value,
            "value": public_value(value), "reversible_badge": True, "detail": detail, "arithmetic": "binary64"}


def _fail(operation: str, exc: Reject, cfg: dict | None = None) -> dict:
    return {"status": exc.code, "operation": operation, "configuration": cfg, "value_raw": None, "value": None,
            "reversible_badge": False, "detail": str(exc), "arithmetic": "binary64"}


def run_operation(operation: str, value: Any, *, r: Any = None, beta: Any = None) -> dict:
    if operation not in {OP_SCALE, OP_SOFTMAX, OP_LOG, OP_POWER, OP_FOURIER, OP_FOURIER_INV, OP_DSCALE}:
        return {"status": "PATH_UNDEFINED", "operation": operation, "configuration": None, "value_raw": None,
                "value": None, "reversible_badge": False, "detail": "undefined operation " + operation,
                "arithmetic": "binary64"}
    try:
        beta_value, declaration = resolve_beta(beta)
        factor = None if operation in {OP_SOFTMAX, OP_LOG, OP_FOURIER, OP_FOURIER_INV} else resolve_r(r)
        cfg = configuration(beta_value, declaration, r=factor)
        if operation == OP_SCALE:
            return _ok(operation, cfg, scale_marks(value, factor), "centered scaling stayed finite")
        if operation == OP_SOFTMAX:
            return _ok(operation, cfg, softmax(value, beta_value), "softmax stayed in the positive simplex")
        if operation == OP_LOG:
            return _ok(operation, cfg, centered_log(value, beta_value), "centered log-ratio stayed centered")
        if operation == OP_POWER:
            return _ok(operation, cfg, power_probability(value, factor), "Aitchison power stayed positive")
        if operation == OP_FOURIER:
            cfg = configuration(beta_value, declaration, extra={"fourier_bin_order": ["k0", "k1", "k2", "k3", "k4", "k5"]})
            return _ok(operation, cfg, marked_fourier(value), "marked Fourier image validated; phase retained")
        if operation == OP_FOURIER_INV:
            return _ok(operation, cfg, marked_fourier_inverse(value), "inverse recovered centered coordinates")
        cfg = configuration(beta_value, declaration, r=factor, extra={"fourier_bin_order": ["k0", "k1", "k2", "k3", "k4", "k5"]})
        return _ok(operation, cfg, scale_fourier(value, factor), "DC fixed; nonzero phases preserved; no magnitude projection")
    except Reject as exc:
        cfg = None
        try:
            beta_value, declaration = resolve_beta(beta)
            cfg = configuration(beta_value, declaration)
        except Reject:
            cfg = None
        return _fail(operation, exc, cfg)


def run_path(operations: list[str], value: Any, *, r: Any, beta: Any) -> dict:
    current = value
    steps = []
    for operation in operations:
        step = run_operation(operation, current, r=r, beta=beta)
        steps.append(step)
        if step["status"] != "ok":
            return {"status": step["status"], "detail": step["detail"], "steps": steps, "value_raw": None,
                    "reversible_badge": False}
        current = step["value_raw"]
    badge = all(step["reversible_badge"] for step in steps)
    return {"status": "ok", "detail": "path stayed inside its contracts", "steps": steps, "value_raw": current,
            "reversible_badge": badge}


def max_abs_diff(left: Any, right: Any) -> float:
    worst = 0.0
    for a, b in zip(left, right):
        worst = max(worst, abs(complex(a) - complex(b)))
    return worst


def public_value(value: Any) -> Any:
    if isinstance(value, tuple):
        return [public_value(item) for item in value]
    if isinstance(value, complex):
        return {"real": value.real, "imag": value.imag}
    return value


def _step_public(step: dict) -> dict:
    return {key: step[key] for key in ("status", "operation", "configuration", "value", "reversible_badge", "detail", "arithmetic")}


PATH_SCHEMAS = {
    SCHEMA_SOFTMAX: {
        "heading": "softmax-scale-power",
        "edge": "path_softmax_scale",
        "source": "CenteredMarks",
        "target": "PositiveProbabilityVector",
        "left": [OP_SCALE, OP_SOFTMAX],
        "right": [OP_SOFTMAX, OP_POWER],
        "source_domain": "finite centered real six-vectors; r > 0; declared beta > 0",
        "intermediate_requirements": [
            "M_r output is a finite centered six-vector",
            "S_beta output is a strictly positive normalized probability vector",
            "P_r stays in that positive simplex",
        ],
    },
    SCHEMA_FOURIER: {
        "heading": "fourier-mark-scale",
        "edge": "path_fourier_scale",
        "source": "CenteredMarks",
        "target": "MarkedFourierImage",
        "left": [OP_SCALE, OP_FOURIER],
        "right": [OP_FOURIER, OP_DSCALE],
        "source_domain": "finite centered real six-vectors; r > 0; declared beta > 0 retained as context",
        "intermediate_requirements": [
            "M_r output is a finite centered six-vector",
            "F output has W0 = 6 c0 and W_{6-k} = -conjugate(W_k)",
            "D_r leaves W0 unchanged, multiplies the other bins by r, and keeps phase",
        ],
    },
}


def _non_certificate(condition: str, detail: str, **extra: Any) -> dict:
    body = {"admitted": False, "condition": condition, "detail": detail, "certificate": None, "reversible_badge": False}
    body.update(extra)
    return body


def path_certificate(schema_id: str, source: Any, *, r: Any, beta: Any = None, paths: dict | None = None,
                     proofs_path: Path | None = None) -> dict:
    if schema_id not in PATH_SCHEMAS:
        return _non_certificate("UNSUPPORTED_PROOF_SCHEMA", "an arbitrary equation or sample comparison is not a certificate")
    schema = PATH_SCHEMAS[schema_id]
    if paths is not None:
        left = list(paths.get("left", []))
        right = list(paths.get("right", []))
        if left != schema["left"] or right != schema["right"]:
            return _non_certificate("INCOMPATIBLE_PATH_TYPES", "submitted paths are not the schema's ordered paths")
    proof_file = Path(proofs_path) if proofs_path else PROOFS_PATH
    text = proof_file.read_text(encoding="utf-8") if proof_file.exists() else ""
    if f"## {schema['heading']}\n" not in text:
        return _non_certificate("DERIVATION_MISSING", "the written derivation heading is not in the proof source")
    try:
        verify_local(make_local(schema["edge"]), proofs_path=proof_file)
        factor = resolve_r(r)
        beta_value, declaration = resolve_beta(beta)
        as_centered(source)
    except Reject as exc:
        return _non_certificate(exc.code, str(exc))
    left_path = run_path(schema["left"], source, r=factor, beta=beta)
    right_path = run_path(schema["right"], source, r=factor, beta=beta)
    path_results = {"left": [_step_public(step) for step in left_path["steps"]],
                    "right": [_step_public(step) for step in right_path["steps"]]}
    if left_path["status"] != "ok" or right_path["status"] != "ok":
        condition = left_path["status"] if left_path["status"] != "ok" else right_path["status"]
        detail = left_path["detail"] if left_path["status"] != "ok" else right_path["detail"]
        return _non_certificate(condition, detail, path_results=path_results)
    residual = max_abs_diff(left_path["value_raw"], right_path["value_raw"])
    scale = 1.0
    for item in tuple(left_path["value_raw"]) + tuple(right_path["value_raw"]):
        scale = max(scale, abs(complex(item)))
    numerical = {
        "arithmetic": "binary64",
        "max_abs_residual": residual,
        "tolerance": PATH_TOL,
        "left_output": public_value(left_path["value_raw"]),
        "right_output": public_value(right_path["value_raw"]),
        "meaning": "execution comparison only; not a proof and not an exact certificate",
    }
    if residual > PATH_TOL * scale:
        return _non_certificate("NUMERICAL_DIVERGENCE", "this execution did not instantiate the schema",
                                numerical_execution=numerical, path_results=path_results)
    badge = bool(left_path["reversible_badge"] and right_path["reversible_badge"])
    certificate = {
        "schema": "TGA_PATH_EQUALITY_CERTIFICATE/2.1",
        "proof_schema": schema_id,
        "mathematical_justification": "trusted analytic schema; derivation PROOFS.md#" + schema["heading"] + "; not a numerical sample",
        "support": "TRUSTED_ANALYTIC_SCHEMA",
        "common_source": schema["source"],
        "common_target": schema["target"],
        "paths": {"left": schema["left"], "right": schema["right"]},
        "path_steps": path_results,
        "parameters": {"r": factor, "beta": beta_value, "beta_declaration": declaration},
        "retained_context": configuration(beta_value, declaration, r=factor),
        "source_domain": schema["source_domain"],
        "intermediate_requirements": schema["intermediate_requirements"],
        "derivation": "PROOFS.md#" + schema["heading"],
        "arithmetic_mode": "binary64",
        "numerical_execution": numerical,
        "reversible_badge": badge,
    }
    return {"admitted": True, "condition": None, "detail": "certificate admitted by the implemented schema",
            "certificate": certificate, "reversible_badge": badge}


ROWS: dict[str, dict] = {
    "scale_centered": dict(implementation=OP_SCALE, source="CenteredMarks", target="CenteredMarks", relation="EQUIVALENCE",
        formula="M_r(z) = r z for r > 0 on centered six-vectors. beta, dimensionless units, and label order stay in the configuration.",
        left="M_r(z)", right="r z", checker="scale_centered", heading="softmax-scale-power", reversible=True, inverse="scale_centered",
        exact=True, arithmetic="binary64 preview", preserves=("label_order", "centered_coordinates", "coordinate_units"), loses=(),
        requires=("r>0", "finite centered input", "declared beta>0 retained", "dimensionless units", "fixed label order"),
        domain="centered real six-vectors, r>0",
        left_inverse="M_{1/r} on centered marks", right_inverse="M_r on the centered image"),
    "softmax_beta": dict(implementation=OP_SOFTMAX, source="CenteredMarks", target="PositiveProbabilityVector", relation="EQUIVALENCE",
        formula="S_beta(z)_i = exp(beta z_i) / sum_j exp(beta z_j), beta>0, default beta=lambda.",
        left="S_beta(z)", right="positive probability vector", checker="softmax_beta", heading="centered-log-ratio", reversible=True,
        inverse="centered_log", exact=True, arithmetic="binary64 preview",
        preserves=("label_order", "centered_contrast_information", "coordinate_units"), loses=(),
        requires=("beta>0", "centered finite input", "fixed label order", "strictly positive image"),
        domain="centered real six-vectors", left_inverse="L_beta on the positive simplex", right_inverse="S_beta on centered marks"),
    "centered_log": dict(implementation=OP_LOG, source="PositiveProbabilityVector", target="CenteredMarks", relation="EQUIVALENCE",
        formula="L_beta(p)_i = (log p_i - mean log p) / beta. General centered equivalence, not six-mark membership.",
        left="L_beta(p)", right="centered coordinates", checker="centered_log", heading="centered-log-ratio", reversible=True,
        inverse="softmax_beta", exact=True, arithmetic="binary64 preview",
        preserves=("label_order", "centered_contrast_information", "coordinate_units"), loses=(),
        requires=("beta>0", "strictly positive normalized probabilities", "fixed label order"),
        domain="positive probability vectors", left_inverse="S_beta", right_inverse="L_beta on the centered image"),
    "power_probability": dict(implementation=OP_POWER, source="PositiveProbabilityVector", target="PositiveProbabilityVector", relation="EQUIVALENCE",
        formula="P_r(p)_i = p_i^r / sum_j p_j^r for r>0. Aitchison power. P_1 is the identity and P_r inverse is P_{1/r}.",
        left="P_r(p)", right="powered probability vector", checker="power_probability", heading="softmax-scale-power", reversible=True,
        inverse="power_probability", exact=True, arithmetic="binary64 preview",
        preserves=("label_order", "positive_simplex", "coordinate_units"), loses=(),
        requires=("r>0", "strictly positive normalized probabilities", "no clipping of underflow"),
        domain="positive probability vectors, r>0", left_inverse="P_{1/r} on the positive simplex", right_inverse="P_r on the positive simplex"),
    "marked_fourier": dict(implementation=OP_FOURIER, source="CenteredMarks", target="MarkedFourierImage", relation="EQUIVALENCE",
        formula="F(z) = DFT(c0 + i z), c0=cos(pi/1296000), unnormalized, phase retained.",
        left="F(z)", right="marked Fourier image", checker="marked_fourier", heading="fourier-mark-scale", reversible=True,
        inverse="marked_fourier_inverse", exact=True, arithmetic="binary64 preview",
        preserves=("label_order", "complex_phase", "coordinate_units"), loses=(),
        requires=("centered real input", "W0=6 c0", "conjugate symmetry", "full complex coefficients"),
        domain="centered real six-vectors", left_inverse="inverse DFT then imaginary part on the marked image",
        right_inverse="F on centered marks"),
    "marked_fourier_inverse": dict(implementation=OP_FOURIER_INV, source="MarkedFourierImage", target="CenteredMarks", relation="EQUIVALENCE",
        formula="Inverse DFT, require real part c0, return the centered imaginary part.",
        left="marked Fourier image", right="centered coordinates", checker="marked_fourier_inverse", heading="fourier-mark-scale",
        reversible=True, inverse="marked_fourier", exact=True, arithmetic="binary64 preview",
        preserves=("label_order", "complex_phase", "coordinate_units"), loses=(),
        requires=("marked image constraints", "centered imaginary part"),
        domain="marked Fourier image", left_inverse="F", right_inverse="inverse DFT on the marked image"),
    "scale_marked_fourier": dict(implementation=OP_DSCALE, source="MarkedFourierImage", target="MarkedFourierImage", relation="EQUIVALENCE",
        formula="D_r leaves W0 unchanged and multiplies W1..W5 by r>0. Phase is not replaced by magnitude.",
        left="D_r(W)", right="scaled marked spectrum", checker="scale_marked_fourier", heading="fourier-mark-scale", reversible=True,
        inverse="scale_marked_fourier", exact=True, arithmetic="binary64 preview",
        preserves=("label_order", "complex_phase", "dc_bin", "coordinate_units"), loses=(),
        requires=("r>0", "marked image", "phase retained"),
        domain="marked Fourier image, r>0", left_inverse="D_{1/r}", right_inverse="D_r on the marked image"),
    "path_softmax_scale": dict(implementation="alignment", source="CenteredMarks", target="PositiveProbabilityVector", relation="IDENTITY",
        formula="S_beta ∘ M_r = P_r ∘ S_beta. Proof: the common softmax denominator cancels after exponentiation.",
        left="S_beta ∘ M_r", right="P_r ∘ S_beta", checker="path_softmax_scale", heading="softmax-scale-power", reversible=False,
        inverse=None, exact=True, arithmetic="not a state execution; numerical execution is a separate record",
        preserves=("identity_on_the_declared_domain",), loses=(),
        requires=("implemented proof schema", "r>0", "beta>0", "positive intermediate image"),
        domain="centered real six-vectors to positive probabilities"),
    "path_fourier_scale": dict(implementation="alignment", source="CenteredMarks", target="MarkedFourierImage", relation="IDENTITY",
        formula="F ∘ M_r = D_r ∘ F. DC stays 6 c0. Off-DC bins scale by r. Phase is kept.",
        left="F ∘ M_r", right="D_r ∘ F", checker="path_fourier_scale", heading="fourier-mark-scale", reversible=False,
        inverse=None, exact=True, arithmetic="not a state execution; numerical execution is a separate record",
        preserves=("identity_on_the_marked_image", "complex_phase"), loses=(),
        requires=("implemented proof schema", "centered source", "marked intermediate image", "r>0"),
        domain="centered real six-vectors to the marked Fourier image"),
    "power_composition": dict(implementation="alignment", source="PositiveProbabilityVector", target="PositiveProbabilityVector", relation="IDENTITY",
        formula="P_r ∘ P_t = P_{r t} for r>0 and t>0, by cancellation of the power denominator.",
        left="P_r ∘ P_t", right="P_{rt}", checker="power_composition", heading="power-composition", reversible=False, inverse=None,
        exact=True, arithmetic="not a path-equality certificate schema",
        preserves=("positive_simplex", "label_order"), loses=(),
        requires=("r>0", "t>0", "strictly positive probabilities"),
        domain="positive probability vectors"),
    "power_unit": dict(implementation="alignment", source="PositiveProbabilityVector", target="PositiveProbabilityVector", relation="IDENTITY",
        formula="P_1 is the identity on normalized positive probabilities.",
        left="P_1(p)", right="p", checker="power_unit", heading="power-composition", reversible=False, inverse=None, exact=True,
        arithmetic="not a path-equality certificate schema", preserves=("positive_simplex", "label_order"), loses=(),
        requires=("normalized strictly positive probabilities",), domain="positive probability vectors"),
    "power_inverse_law": dict(implementation="alignment", source="PositiveProbabilityVector", target="PositiveProbabilityVector", relation="IDENTITY",
        formula="The inverse of P_r on the positive simplex is P_{1/r}.",
        left="P_r inverse", right="P_{1/r}", checker="power_inverse_law", heading="power-composition", reversible=False, inverse=None,
        exact=True, arithmetic="not a path-equality certificate schema", preserves=("positive_simplex", "label_order"), loses=(),
        requires=("r>0", "strictly positive probabilities", "no clipped underflow"),
        domain="positive probability vectors"),
    "six_mark_gap_criterion": dict(implementation="alignment", source="PositiveProbabilityVector", target="SixMarkProbability", relation="EQUIVALENCE",
        formula="g2=g4>0, g1=g5=phi g2, and 0<g3<=2 g2 are necessary and sufficient for the positive-scale six-mark family. Zero mean fixes the six coordinates. Canonical angle adds g3=2 sin(pi/1296000) g2.",
        left="five geometric gap conditions", right="six-mark family probability", checker="six_mark_gap_criterion",
        heading="six-mark-membership", reversible=False, inverse=None, exact=True,
        arithmetic="exact statement; binary64 membership is a separate numerical report",
        preserves=("necessity_and_sufficiency_on_exact_positive_reals",), loses=(),
        requires=("a>0", "0<epsilon<=pi", "beta>0", "strictly positive probabilities", "fixed label order"),
        domain="exact positive probability vectors; not a binary64 certificate"),
}
LOCAL_ORDER = tuple(ROWS)


def make_local(edge_id: str):
    if edge_id not in ROWS:
        raise Reject("unsupported map or witness schema: " + str(edge_id))
    row = ROWS[edge_id]
    source = TYPE_BY_NAME[row["source"]]
    target = TYPE_BY_NAME[row["target"]]
    relation = tga20.Relation[row["relation"]]
    inverse = None
    if row["inverse"]:
        inverse = tga20.InverseContract(row["inverse"], target, source, target.name + " satisfying its image constraints",
                                         row["left_inverse"], row["right_inverse"])
    contract = tga20.Contract(tuple(row["preserves"]), tuple(row["loses"]), tuple(row["requires"]),
                              row["exact"], row["reversible"], row["domain"])
    unsigned = {"id": edge_id, "source": source, "target": target, "formula": row["formula"],
                "implementation": row["implementation"], "arithmetic": row["arithmetic"], "inverse": inverse,
                "left": row["left"], "right": row["right"], "relation": relation, "contract": contract,
                "checker": row["checker"], "support": tga20.Support.TRUSTED_ANALYTIC_SCHEMA, "heading": row["heading"]}
    payload = tga20.canonical({"schema": row["checker"], "heading": row["heading"], "derivation": "PROOFS.md#" + row["heading"]})
    witness = tga20.Witness(row["checker"], tga20.Support.TRUSTED_ANALYTIC_SCHEMA, tga20.digest(unsigned), payload)
    return tga20.MapSpec(edge_id, source, target, row["formula"], row["implementation"], row["arithmetic"], inverse,
                         tga20.Alignment(row["left"], row["right"], relation, witness, contract))


def verify_local(spec, proofs_path: Path | None = None):
    need(type(spec) is tga20.MapSpec, "a MapSpec is required")
    need(spec.id in ROWS, "unsupported map or witness schema: " + str(getattr(spec, "id", "")))
    expected = make_local(spec.id)
    need(spec == expected, "claim, implementation, contract, inverse, type or witness differs from supported schema")
    need(spec.alignment.witness is not None, "NO EDGE WITHOUT A WITNESS")
    need(spec.alignment.witness.support not in {tga20.Support.NUMERICAL_TEST_ONLY, tga20.Support.EXTERNAL_REFERENCE_ONLY},
         "insufficient evidence for admission")
    need((not spec.alignment.contract.reversible) or spec.inverse is not None, "NO REVERSIBILITY WITHOUT INVERSE CONTRACT")
    if spec.inverse:
        other = make_local(spec.inverse.map_id)
        need(other.source == spec.target and other.target == spec.source, "inverse types disagree")
    payload = json.loads(spec.alignment.witness.payload)
    proof_file = Path(proofs_path) if proofs_path else PROOFS_PATH
    text = proof_file.read_text(encoding="utf-8") if proof_file.exists() else ""
    need(f"## {payload['heading']}\n" in text, "written derivation heading missing", "DERIVATION_MISSING")
    detail = "Checked instantiation of " + payload["heading"] + ". Numerical samples are not this witness."
    status = "trusted analytic schema; derivation supplied in PROOFS.md; not a binary64 certificate"
    return tga20.Certificate(spec.id, spec.alignment.witness.support, spec.alignment.witness.claim_digest, detail, status)


def execute_local(edge_id: str, value: Any, *, r: Any = None, beta: Any = None) -> Any:
    spec = make_local(edge_id)
    verify_local(spec)
    if spec.implementation == "alignment":
        raise Reject("this edge is an identity statement, not a state-execution map")
    result = run_operation(spec.implementation, value, r=r, beta=beta)
    if result["status"] != "ok":
        raise Reject(result["detail"], result["status"])
    return result["value_raw"]


def _relation_names(edges: list[dict]) -> list[str]:
    return sorted({edge["alignment"]["relation"] for edge in edges})


def build_report() -> dict:
    edges = []
    certificates = []
    graph = tga20.Graph()
    for name in tga20.MAP_IDS:
        spec = tga20.make_spec(name)
        certificate = graph.admit(spec)
        edge = tga20.plain(spec)
        edge["introduced_in"] = "2.0"
        edges.append(edge)
        record = tga20.plain(certificate)
        record["introduced_in"] = "2.0"
        certificates.append(record)
    for edge_id in LOCAL_ORDER:
        spec = make_local(edge_id)
        certificate = verify_local(spec)
        edge = tga20.plain(spec)
        edge["introduced_in"] = "2.1"
        edges.append(edge)
        record = tga20.plain(certificate)
        record["introduced_in"] = "2.1"
        certificates.append(record)
    categories = _relation_names(edges)
    count = len(edges)
    if count != len(certificates):
        raise Reject("relationship count drifted from the certificate list")
    sample = (-3.0, -2.0, -1.0, 1.0, 2.0, 3.0)
    canonical_z = geometry_marks(1.0, CANONICAL_EPSILON)
    comparisons = []
    examples = []
    for factor in (0.5, 1.0, 2.0):
        for schema_id, source, label in (
            (SCHEMA_SOFTMAX, sample, "sample-centered"),
            (SCHEMA_FOURIER, canonical_z, "canonical-geometry"),
        ):
            issued = path_certificate(schema_id, source, r=factor, beta=None)
            comparisons.append({"id": schema_id + ":" + label + ":r=" + str(factor), "kind": "path_certificate",
                                "admitted": issued["admitted"], "condition": issued["condition"],
                                "max_abs_residual": None if not issued["admitted"] else issued["certificate"]["numerical_execution"]["max_abs_residual"],
                                "reversible_badge": issued["reversible_badge"]})
            if factor == 2.0 and label == "sample-centered":
                examples.append(issued)
    claims = (
        tga20.Claim("phi_A", "constant", "(1+sqrt5)/2", ("sqrt5",)),
        tga20.Claim("phi_B", "constant", "1/2+sqrt5/2", ("sqrt5",)),
        tga20.Claim("wrong_phi", "constant", "1+sqrt5", ("sqrt5",)),
    )
    vectors = browser_vectors()
    return {
        "schema": "TGA_RUN/2.1",
        "supplementary": True,
        "extends": "TGA_RUN/2.0",
        "source_sha256": hashlib.sha256(Path(__file__).read_bytes()).hexdigest(),
        "publication": {
            "status": "supplementary release",
            "version": "2.1",
            "date": "2026-10-01",
            "classified_as": "supplementary work",
            "not": ["source paper", "general theorem prover", "replacement of TGA 2.0",
                    "replacement of production geometry or field decoders", "exact binary64 membership certificate"],
            "preserves_tga_2_0": {
                "verifier_sha256": TGA20_FILES["tga_verifier.py"][1],
                "report_sha256": TGA20_FILES["graph-report.json"][1],
                "note": "Published TGA 2.0 files are inputs. This release does not rewrite them.",
            },
        },
        "mathematical_justification": {
            "source": "PROOFS.md",
            "rendered": "PROOFS.html",
            "path_schemas": list(PATH_SCHEMAS),
            "note": "Written derivations and trusted schema instantiation. Separate from publication, execution logs, and numerical residuals.",
        },
        "graph": {
            "schema": "TGA_WITNESS_GRAPH/2.1",
            "edges": edges,
            "certificates": certificates,
            "relationship_count": count,
            "relationship_count_meaning": "equal to the length of edges; do not maintain a second count",
            "relation_categories": categories,
            "trust": "TGA 2.0 closed schemas plus TGA 2.1 schemas whose headings are in PROOFS.md. No general theorem proving.",
        },
        "path_equality_certificates": {
            "schema": "TGA_PATH_EQUALITY_CERTIFICATE/2.1",
            "supported_schemas": list(PATH_SCHEMAS),
            "examples": examples,
            "note": "Only these two schemas admit a certificate. Power laws are proved and checked, but they are not additional certificate schemas.",
        },
        "execution_results": {
            "record": "execution.json",
            "commands": ["python3 -m unittest -v test_tga", "python3 -O -m unittest -v test_tga",
                         "python3 tga_verifier.py --report graph-report.json"],
            "note": "Versions, timestamps, and exit statuses belong to the execution record. They are not mathematical status.",
        },
        "numerical_comparisons": {
            "meaning": "Binary64 comparisons. Not exact certificates and not six-mark membership certificates.",
            "tolerance_policy": TOLERANCE_POLICY,
            "cases": comparisons,
            "browser_vectors": vectors,
        },
        "proposals_only": [tga20.plain(item) for item in tga20.propose(claims)],
        "limits": [
            "No shared symbol admits an edge.",
            "A numerical residual does not admit a path certificate.",
            "Binary64 six-mark agreement is not an exact membership certificate.",
            "General centered log-ratio equivalence is not six-mark membership.",
            "Underflow out of the positive domain is rejected rather than clipped.",
            "TGA 2.0 bytes stay on their published hashes.",
            "This is not a general theorem prover and not a source paper.",
        ],
    }


def browser_vectors() -> list[dict]:
    """Inputs and outputs the site calculator must reproduce. Not certificates."""
    sample = [-3.0, -2.0, -1.0, 1.0, 2.0, 3.0]
    rows = []
    for factor in (0.5, 1.0, 2.0):
        scaled = scale_marks(sample, factor)
        rows.append({"id": f"scale-{factor}", "op": "M_r", "input": sample, "r": factor, "beta": None,
                     "status": "ok", "output": list(scaled)})
    probs = softmax(sample, None)
    rows.append({"id": "softmax-default", "op": "S_beta", "input": sample, "r": None, "beta": None,
                 "status": "ok", "output": list(probs)})
    rows.append({"id": "power-2", "op": "P_r", "input": list(probs), "r": 2.0, "beta": None,
                 "status": "ok", "output": list(power_probability(probs, 2))})
    rows.append({"id": "power-1", "op": "P_r", "input": list(probs), "r": 1.0, "beta": None,
                 "status": "ok", "output": list(probs)})
    for schema_id, factor in ((SCHEMA_SOFTMAX, 0.5), (SCHEMA_SOFTMAX, 1.0), (SCHEMA_SOFTMAX, 2.0), (SCHEMA_FOURIER, 2.0)):
        issued = path_certificate(schema_id, sample, r=factor, beta=None)
        rows.append({"id": schema_id + f"-r{factor}", "op": "path", "schema": schema_id, "input": sample,
                     "r": factor, "beta": None, "status": "admitted" if issued["admitted"] else issued["condition"],
                     "max_abs_residual": issued["certificate"]["numerical_execution"]["max_abs_residual"],
                     "left": issued["certificate"]["numerical_execution"]["left_output"],
                     "right": issued["certificate"]["numerical_execution"]["right_output"]})
    canonical = geometry_marks(1.0, CANONICAL_EPSILON)
    canonical_p = softmax(canonical, None)
    member = six_mark_membership(canonical_p, mode="canonical")
    rows.append({"id": "canonical-member", "op": "membership", "input": list(canonical_p), "r": None, "beta": None,
                 "mode": "canonical", "status": member["numerical_status"], "recovered": member["recovered"]})
    interior = softmax(geometry_marks(2.0, 1.0), 4.0)
    interior_report = six_mark_membership(interior, beta=4.0, mode="family")
    rows.append({"id": "interior-member", "op": "membership", "input": list(interior), "r": None, "beta": 4.0,
                 "mode": "family", "status": interior_report["numerical_status"], "recovered": interior_report["recovered"]})
    generic = [0.05, 0.10, 0.15, 0.20, 0.22, 0.28]
    generic_report = six_mark_membership(generic)
    rows.append({"id": "generic-outside", "op": "membership", "input": generic, "r": None, "beta": None,
                 "mode": "family", "status": generic_report["numerical_status"], "recovered": None})
    uniform = six_mark_membership((1 / 6,) * 6)
    rows.append({"id": "uniform", "op": "membership", "input": [1 / 6] * 6, "r": None, "beta": None,
                 "mode": "family", "status": uniform["numerical_status"], "recovered": None})
    rejected = run_operation(OP_SOFTMAX, [-1e6, -1e6, -1e6, 1e6, 1e6, 1e6], r=1, beta=1)
    rows.append({"id": "underflow", "op": "S_beta", "input": [-1e6, -1e6, -1e6, 1e6, 1e6, 1e6], "r": 1, "beta": 1,
                 "status": rejected["status"], "reversible_badge": False, "output": None})
    return rows


def inline_markup(text: str) -> str:
    escaped = html.escape(text)
    parts = escaped.split("`")
    out = []
    for index, part in enumerate(parts):
        out.append(f"<code>{part}</code>" if index % 2 else part)
    return "".join(out)


def render_proofs_html(markdown: str) -> str:
    lines = markdown.replace("\r\n", "\n").split("\n")
    body: list[str] = []
    paragraph: list[str] = []
    items: list[str] = []

    def flush_paragraph() -> None:
        nonlocal paragraph
        if paragraph:
            body.append("<p>" + inline_markup(" ".join(part.strip() for part in paragraph)) + "</p>")
            paragraph = []

    def flush_items() -> None:
        nonlocal items
        if items:
            body.append("<ul>" + "".join(f"<li>{inline_markup(item)}</li>" for item in items) + "</ul>")
            items = []

    index = 0
    while index < len(lines):
        line = lines[index]
        if line.startswith("```"):
            flush_paragraph()
            flush_items()
            index += 1
            captured = []
            while index < len(lines) and not lines[index].startswith("```"):
                captured.append(lines[index])
                index += 1
            if index < len(lines):
                index += 1
            body.append("<pre>" + html.escape("\n".join(captured)) + "</pre>")
            continue
        if line.startswith("# "):
            flush_paragraph()
            flush_items()
            body.append("<h1>" + inline_markup(line[2:].strip()) + "</h1>")
        elif line.startswith("## "):
            flush_paragraph()
            flush_items()
            title = line[3:].strip()
            body.append(f'<h2 id="{html.escape(title)}">' + inline_markup(title) + "</h2>")
        elif line.startswith("- "):
            flush_paragraph()
            items.append(line[2:].strip())
        elif not line.strip():
            flush_paragraph()
            flush_items()
        else:
            flush_items()
            paragraph.append(line)
        index += 1
    flush_paragraph()
    flush_items()
    style = """
    :root { color-scheme: light; }
    body { margin: 0; background: #faf9f6; color: #172127; font-family: "IBM Plex Sans", "Segoe UI", sans-serif; line-height: 1.6; }
    main { max-width: 42rem; margin: 0 auto; padding: 2.5rem 1.25rem 4rem; }
    h1, h2 { font-family: "Instrument Serif", "Times New Roman", serif; font-weight: 400; line-height: 1.2; }
    h1 { font-size: 2.4rem; margin-bottom: 0.4rem; }
    h2 { font-size: 1.6rem; margin-top: 2rem; color: #075e58; }
    a { color: #075e58; }
    code, pre { font-family: "IBM Plex Mono", ui-monospace, monospace; }
    pre { background: #f3f1ec; padding: 0.8rem 1rem; overflow: auto; border: 1px solid #71818b; }
    .banner { color: #485760; font-size: 0.95rem; }
    """
    return "<!DOCTYPE html>\n<html lang=\"en\">\n<head>\n<meta charset=\"utf-8\">\n<meta name=\"viewport\" content=\"width=device-width, initial-scale=1\">\n<title>TGA 2.1 proofs</title>\n<style>" + style + "</style>\n</head>\n<body>\n<main>\n<p class=\"banner\">Rendered from <a href=\"PROOFS.md\">PROOFS.md</a>. Supplementary TGA 2.1 derivation, 1 October 2026. Not a source paper and not an execution log. <a href=\"/tga\">TGA page</a>.</p>\n" + "\n".join(body) + "\n</main>\n</body>\n</html>\n"


def main() -> None:
    parser = argparse.ArgumentParser(description=__doc__)
    parser.add_argument("--report", type=Path, help="write the JSON report")
    parser.add_argument("--write-html", action="store_true", help="render PROOFS.html from PROOFS.md")
    args = parser.parse_args()
    if args.write_html:
        HTML_PATH.write_text(render_proofs_html(PROOFS_PATH.read_text(encoding="utf-8")), encoding="utf-8")
        print("WROTE", HTML_PATH)
    report = build_report()
    if args.report:
        args.report.write_text(json.dumps(report, indent=2, sort_keys=True, allow_nan=False) + "\n", encoding="utf-8")
        print("WROTE", args.report)
    else:
        print("TGA 2.1:", report["graph"]["relationship_count"], "admitted relationships")
        print("Relation categories:", len(report["graph"]["relation_categories"]))
        print("Path schemas:", ", ".join(PATH_SCHEMAS))
        print("Not a general theorem prover. Supplementary to frozen TGA 2.0.")


if __name__ == "__main__":
    main()