reproduction/calibration_boundary_counterexample.py

#!/usr/bin/env python3
"""Boundary counterexample to the stated DCF Calibration Convergence theorem.

The theorem permits sup(lambda*T)-inf(lambda*T) <= 1.  Equality allows a
valid threshold and an invalid threshold to have identical limiting utility,
so the final softmax averages them rather than recovering the hard maximum.
"""

import json
import math
from pathlib import Path


GRID = [0.0, 0.5, 1.0]
RISK = 0.5
LAMBDA = 1.0


def softplus(x: float) -> float:
    if x > 0:
        return x + math.log1p(math.exp(-x))
    return math.log1p(math.exp(x))


def row(temperature: float) -> dict:
    tau_s = math.sqrt(temperature)
    beta = 1.0 / math.sqrt(temperature)
    utilities = []
    violations = []
    for tau in GRID:
        z = (tau - RISK + math.sqrt(temperature)) / temperature
        # One false node and no ancestors: q=p and Q=1-p.
        log_q_valid = -softplus(z)
        scaled = log_q_valid / tau_s
        violation = 1.0 if scaled < -745 else -math.expm1(scaled)
        violations.append(violation)
        utilities.append(LAMBDA * tau - violation)

    logits = [beta * value for value in utilities]
    shift = max(logits)
    weights = [math.exp(value - shift) for value in logits]
    total = sum(weights)
    weights = [value / total for value in weights]
    return {
        "temperature": temperature,
        "tau_s": tau_s,
        "beta": beta,
        "violations": violations,
        "utilities": utilities,
        "weights": weights,
        "soft_score": sum(tau * weight for tau, weight in zip(GRID, weights)),
    }


def main() -> None:
    temperatures = [0.1 / (2**k) for k in range(11)]
    rows = [row(value) for value in temperatures]
    result = {
        "claim": "Theorem 3.1 calibration convergence as written",
        "verdict": "falsified_as_written",
        "theorem_condition": "sup(lambda*T)-inf(lambda*T) <= 1",
        "construction": {
            "graph": "one false node, no edges",
            "risk": RISK,
            "threshold_grid": GRID,
            "lambda": LAMBDA,
            "condition_lhs": max(LAMBDA * x for x in GRID)
            - min(LAMBDA * x for x in GRID),
        },
        "hard_cf_nonconformity": 0.0,
        "sequential_limit": {
            "limiting_violations": [0.0, 1.0, 1.0],
            "limiting_utilities": [0.0, -0.5, 0.0],
            "maximizers": [0.0, 1.0],
            "softmax_limit": 0.5,
        },
        "single_limit_schedule": "tau_s=sqrt(T), beta=1/sqrt(T)",
        "rows": rows,
        "checks": {
            "theorem_assumption_satisfied_at_equality": True,
            "hard_score_is_zero": True,
            "last_soft_score_near_half": abs(rows[-1]["soft_score"] - 0.5) < 1e-8,
            "last_soft_score_not_hard_score": abs(rows[-1]["soft_score"]) > 0.49,
        },
        "minimal_repair": "replace <= 1 by < 1 (plus the theorem's remaining assumptions)",
    }
    if not all(result["checks"].values()):
        raise SystemExit("counterexample check failed")
    output = Path("outputs/calibration_boundary_counterexample.json")
    output.parent.mkdir(parents=True, exist_ok=True)
    output.write_text(json.dumps(result, indent=2) + "\n")
    print(json.dumps(result, indent=2))


if __name__ == "__main__":
    main()