#!/usr/bin/env python3 """Warning-strict independent validation of the additive Claim 5 certificate.""" from __future__ import annotations import hashlib import json import subprocess import sys import tempfile from pathlib import Path ROOT = Path(__file__).resolve().parent def digest(path: Path) -> str: return hashlib.sha256(path.read_bytes()).hexdigest() def main() -> None: source = ROOT / "source_pins" / "4limitations.tex" assert digest(source) == "d90bf1cd0c280c2d36f37ae5bd336b9df275060cd2b2f73c12d2d181569687e9" source_text = source.read_text(encoding="utf-8") assert "M := I_{T \\times T} + E^{T,1}" in source_text assert "\\rank(QK^\\top) \\le \\rank(Q) \\le N" in source_text sealed = ROOT / "outputs_claim5" result = json.loads((sealed / "claim5_non_diagonal_witness_results.json").read_text()) assert result["all_literal_kernels_exact"] is True assert result["all_transitions_non_diagonal_rank_one"] is True assert result["all_width_matched_duals_ruled_out"] is True assert result["all_destructive_controls_pass"] is True assert [row["T"] for row in result["cases"]] == [4, 8, 16, 32, 64] assert all(row["required_attention_score_rank_lower_bound"] > 2 for row in result["cases"]) with tempfile.TemporaryDirectory(prefix="claim5-replay-") as directory: replay = Path(directory) subprocess.run( [ sys.executable, str(ROOT / "code" / "claim5_non_diagonal_witness.py"), "--output-dir", str(replay), ], check=True, ) for name in ( "OUTPUT_SHA256SUMS.txt", "claim5_non_diagonal_witness_cases.csv", "claim5_non_diagonal_witness_results.json", ): assert (replay / name).read_bytes() == (sealed / name).read_bytes(), name page = (ROOT / "pages" / "02-claim-5-softmax-rank-explosion" / "page.md").read_text() assert "upper triangular" in page assert "does not construct a proof" not in page print("claim5 evidence validation passed: exact source, certificate, control, and replay") if __name__ == "__main__": main()