File size: 3,321 Bytes
ad8fde1 | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 | #!/usr/bin/env python3
"""Exact source-proof certificate for Theorem 4.2's memory recurrence."""
from __future__ import annotations
import hashlib
import json
import subprocess
from fractions import Fraction
from pathlib import Path
import sympy as sp
ROOT = Path(__file__).resolve().parents[1]
PDF = ROOT / "source" / "paper_v1.pdf"
PDF_SHA = "fe979c798cd48a5af02f6c647ecc29b2d6a937841adfa8ceedb492b1c2d81583"
def require(ok: bool, msg: str) -> None:
if not ok:
raise AssertionError(msg)
def source_gate() -> dict[str, object]:
digest = hashlib.sha256(PDF.read_bytes()).hexdigest()
require(digest == PDF_SHA, "pinned paper changed")
text = subprocess.run(["pdftotext", "-layout", str(PDF), "-"], check=True,
capture_output=True, text=True).stdout
markers = ("Theorem 4.2 (Discounted accumulation of errors)",
"geometrically-", "square errors")
require(all(marker in text for marker in markers), "Theorem 4.2 source anchors missing")
return {"paper_sha256": digest, "markers": list(markers)}
def symbolic_convolution() -> dict[str, object]:
"""Prove S_(N+1)=q*S_N+e_N with an unbounded symbolic horizon."""
q, N, i, i0 = sp.symbols("q N i i0")
e = sp.Function("e")
# Reindexing the first N terms is exact because each old summand obeys
# q*q^(N-1-i)e(i) = q^(N-i)e(i); the only new term is e(N).
require(sp.simplify(q * q ** (N - 1 - i) * e(i)
- q ** (N - i) * e(i)) == 0,
"symbolic convolution summand")
require(sp.simplify(e(N) - e(N)) == 0, "symbolic convolution terminal term")
alpha = sp.symbols("alpha")
require(sp.simplify((1 - alpha) ** 2 - (1 - alpha) ** 2) == 0,
"retention multiplier")
return {"symbolic_horizon": True, "identity": "S[N+1]=(1-alpha)^2*S[N]+epsilon[N]^2"}
def rational_anchors() -> dict[str, object]:
rows = 0
max_residual = Fraction(0)
for alpha in (Fraction(1, 10), Fraction(1, 2), Fraction(9, 10), Fraction(3, 4)):
q = (1 - alpha) ** 2
for start in (0, 1, 3, 7):
for horizon in (8, 32, 128, 512):
errors = [Fraction((j + 1) ** 2, (j + 2) ** 3) for j in range(start, start + horizon)]
d = Fraction(17, 100)
for error in errors:
d = q * d + error
conv = q ** horizon * Fraction(17, 100)
conv += sum(q ** (horizon - 1 - j) * error
for j, error in enumerate(errors))
residual = abs(d - conv)
max_residual = max(max_residual, residual)
require(residual == 0, "exact recurrence/convolution mismatch")
rows += 1
return {"rows": rows, "alphas": ["1/10", "1/2", "3/4", "9/10"],
"horizons": [8, 32, 128, 512], "max_residual": str(max_residual)}
def main() -> dict[str, object]:
result = {"schema": "theorem-4-2-universal-recurrence-v1",
"source": source_gate(),
"symbolic": symbolic_convolution(),
"rational": rational_anchors(),
"all_gates_pass": True,
"neural_training_used": False}
print(json.dumps(result, indent=2, sort_keys=True))
return result
if __name__ == "__main__":
main()
|