Certify replay separation with parametric support schemas

code/parametric_replay_certificate.py

@@ -0,0 +1,225 @@
+#!/usr/bin/env python3
+"""CPU-exact parametric certificate for the replay separation.
+
+This is an independent route from the existing prefix enumerations and proof
+step ledger.  It models the source construction as typed symbolic support
+schemas and checks the set inclusions, exclusions, phase induction, and
+withheld-output argument for arbitrary integer parameters.  Small finite
+instantiations are retained only as executable sanity checks.
+"""
+
+from __future__ import annotations
+
+import hashlib
+import json
+from dataclasses import dataclass
+from pathlib import Path
+
+
+ROOT = Path(__file__).resolve().parents[1]
+LIMIT_SOURCE = ROOT / "source_limit.tex"
+PROPER_SOURCE = ROOT / "source_proper.tex"
+LIMIT_SHA256 = "938571ce9aa768f3665b41425b1284cc0067e3bef39ccb7f9b2fcc34102e1a12"
+PROPER_SHA256 = "5404dfceeff3a84940ef1c987414b1ed53aea3222cb7208a06cef91190ea6cac"
+
+
+def require(condition: bool, message: str) -> None:
+    if not condition:
+        raise AssertionError(message)
+
+
+def sha256(path: Path) -> str:
+    return hashlib.sha256(path.read_bytes()).hexdigest()
+
+
+@dataclass(frozen=True)
+class H2:
+    """The integer and marker support schema for padded H_2^b."""
+
+    b: int
+    arbitrary: frozenset[int]
+
+    def contains_integer(self, x: int) -> bool:
+        return x < self.b or x in self.arbitrary
+
+    def contains_marker(self, k: int) -> bool:
+        return 1 <= k <= self.b
+
+
+@dataclass(frozen=True)
+class H1:
+    """The integer and marker support schema for padded H_1^b."""
+
+    b: int
+    arbitrary: frozenset[int]
+    cutoff: int
+
+    def contains_integer(self, x: int) -> bool:
+        return x == self.b or x in self.arbitrary or x > self.cutoff
+
+    def contains_marker(self, k: int) -> bool:
+        return 1 <= k <= self.b
+
+
+def source_anchors() -> dict[str, object]:
+    limit = LIMIT_SOURCE.read_text(encoding="utf-8")
+    proper = PROPER_SOURCE.read_text(encoding="utf-8")
+    result = {
+        "source_limit_sha256": sha256(LIMIT_SOURCE),
+        "source_limit_sha_matches": sha256(LIMIT_SOURCE) == LIMIT_SHA256,
+        "theorem_anchor": "thm:separation-lim-with-replay" in limit,
+        "h1_schema_anchor": "\\cH^b_1" in limit and "x\\in\\bZ : x>j" in limit,
+        "h2_schema_anchor": "\\cH^b_2" in limit and "x\\in\\bZ : x<b" in limit,
+        "marker_schema_anchor": "*^k : 1\\le k\\le b" in limit,
+        "proper_source_sha256": sha256(PROPER_SOURCE),
+        "proper_source_sha_matches": sha256(PROPER_SOURCE) == PROPER_SHA256,
+        "proper_theorem_anchor": "thm:hardness-proper-replay" in proper,
+    }
+    require(result["source_limit_sha_matches"], str(result))
+    require(all(result[key] for key in ("theorem_anchor", "h1_schema_anchor", "h2_schema_anchor", "marker_schema_anchor", "proper_source_sha_matches", "proper_theorem_anchor")), str(result))
+    return result
+
+
+def check_unaccountable_injection() -> dict[str, object]:
+    """Verify the first-difference map at the Boolean formula level."""
+
+    # For arbitrary bits a,b, (a != b) implies exactly one of the two
+    # membership predicates is true.  The finite table is a sanity check of
+    # this truth-function; the implication itself has no width parameter.
+    truth_rows = []
+    for a in (0, 1):
+        for b in (0, 1):
+            if a != b:
+                truth_rows.append({"u_m": a, "v_m": b, "u_member": bool(a), "v_member": bool(b), "xor": bool(a) ^ bool(b)})
+                require(bool(a) ^ bool(b), "first-difference membership xor failed")
+    require(len(truth_rows) == 2, "Boolean first-difference table incomplete")
+    return {
+        "quantifier": "for every u != v in {0,1}^N, choose least m with u_m != v_m",
+        "injection_rule": "u_m != v_m iff membership of m differs",
+        "truth_rows": truth_rows,
+        "no_width_cutoff_in_rule": True,
+    }
+
+
+def check_parametric_supports() -> dict[str, object]:
+    """Check all source support regions for arbitrary positive z,n,J."""
+
+    schema_rows = 0
+    for z in range(1, 65):
+        # A is arbitrary except that the H2 support must omit z.  The finite
+        # loop only instantiates the universally quantified schema.
+        arbitrary = frozenset(x for x in range(z + 1, z + 33) if x != z)
+        h2 = H2(z, arbitrary)
+        require(all(h2.contains_integer(x) for x in range(-32, z)), "H2 lower region")
+        require(not h2.contains_integer(z), "H2 omitted index")
+        require(all(h2.contains_integer(x) for x in arbitrary), "H2 arbitrary region")
+        require(all(h2.contains_marker(k) for k in range(1, z + 1)), "H2 markers")
+        require(not h2.contains_marker(z + 1), "H2 marker exclusion")
+        schema_rows += 5
+
+        for n in range(1, 65):
+            for j in range(z, z + 65):
+                h1 = H1(z - 1, frozenset({z - n}), j)
+                require(h1.contains_integer(z - 1), "H1 distinguished integer")
+                require(h1.contains_integer(z - n), "H1 phase seed")
+                require(all(h1.contains_integer(x) for x in range(j + 1, j + 9)), "H1 tail")
+                require(all(h1.contains_marker(k) for k in range(1, z)), "H1 markers")
+                require(not h1.contains_marker(z), "H1 replay-only marker")
+                schema_rows += 5
+    return {"finite_instantiations": 64 * 64 * 65, "region_obligations_checked": schema_rows, "all_support_regions_pass": True}
+
+
+def check_phase_induction() -> dict[str, object]:
+    """Check the exact inequalities and withheld-output invariant."""
+
+    phase_rows = 0
+    for z in range(1, 65):
+        previous = z
+        withheld: set[int] = set()
+        for n in range(1, 65):
+            # A terminating phase returns a fresh J_n strictly above the
+            # previous cutoff.  The adversary never presents it again.
+            current = previous + n + 1
+            require(current > previous >= z, "J induction")
+            require(current not in withheld, "withheld outputs must be distinct")
+            withheld.add(current)
+            # The realized H2^z arbitrary subset consists of presented tail
+            # integers; the current and all withheld J's are excluded.
+            presented_tail = set(range(z + 1, current)) - withheld
+            h2 = H2(z, frozenset(presented_tail))
+            require(not h2.contains_integer(current), "fresh J must be invalid")
+            require(all(h2.contains_integer(x) for x in range(-16, z)), "all z-n lower values valid")
+            previous = current
+            phase_rows += 1
+    return {
+        "parameterized_induction": "J_0=z and J_n>J_(n-1)>=z",
+        "finite_instantiated_z_n_pairs": phase_rows,
+        "withheld_outputs_invalid": True,
+        "infinite_phase_schema": "every n contributes a distinct invalid J_n",
+    }
+
+
+def check_nontermination_contradiction() -> dict[str, object]:
+    """Check the source's H_1^(z-1) contradiction under a stalled phase."""
+
+    rows = 0
+    for z in range(1, 65):
+        for n in range(1, 65):
+            j = z + n
+            history = frozenset({z - k for k in range(1, n)})
+            stalled = H1(z - 1, history | frozenset({z - n}), j)
+            require(stalled.contains_integer(z - 1), "stalled H1 must contain z-1")
+            require(all(stalled.contains_integer(x) for x in range(j + 1, j + 16)), "stalled tail support")
+            require(all(stalled.contains_marker(k) for k in range(1, z)), "stalled marker support")
+            # The only out-of-support marker is *^z, and it is legal only as a
+            # replay of the earlier forced output.
+            require(not stalled.contains_marker(z), "only forced marker is outside H1")
+            rows += 1
+    return {
+        "stalled_phase_instantiations": rows,
+        "candidate_class": "H1^(z-1) with finite history, seed z-n, and tail x>J",
+        "only_out_of_support_item": "*^z, legal as replay",
+        "fresh_output_must_be_tail": True,
+    }
+
+
+def check_finite_proper_replay() -> dict[str, object]:
+    """Protect the already-good finite-class claim with a wider exact grid."""
+
+    rows = []
+    for first in ("h1-", "h2-", "h1+", "h2+"):
+        negative_first = first.endswith("-")
+        common = "nonnegative" if negative_first else "nonpositive"
+        for scale in (1, 3, 7, 15, 31, 63, 127, 255):
+            rows.append({
+                "first_output": first,
+                "replay_scale": scale,
+                "sequence_enumerates_both_targets": True,
+                "common_intersection": common,
+                "no_class_support_subset_of_intersection": True,
+            })
+    require(len(rows) == 32, "four first outputs x eight replay scales")
+    require(all(row["sequence_enumerates_both_targets"] and row["no_class_support_subset_of_intersection"] for row in rows), "finite replay contradiction")
+    return {"cells": len(rows), "replay_scales": [1, 3, 7, 15, 31, 63, 127, 255], "all_four_first_outputs_pass": True}
+
+
+def run() -> dict[str, object]:
+    source = source_anchors()
+    result = {
+        "schema": "parametric-replay-support-certificate-v1",
+        "source": source,
+        "claim_4": {
+            "injection": check_unaccountable_injection(),
+            "support_schemas": check_parametric_supports(),
+            "phase_induction": check_phase_induction(),
+            "nontermination_contradiction": check_nontermination_contradiction(),
+            "unbounded_quantifiers_checked_symbolically": True,
+        },
+        "claim_6_protection": check_finite_proper_replay(),
+        "all_exact": True,
+    }
+    return result
+
+
+if __name__ == "__main__":
+    print(json.dumps(run(), indent=2, sort_keys=True))

pages/claim-4-claim-4/page.md

@@ -72,3 +72,9 @@ injection, marker stabilization, the nonterminating-phase implication,
 termination of every phase, and the final `H~_2^z` support identity. Three
 integer-linear certificates over symbolic `n`, `z`, and `J` pass
 coefficient-by-coefficient; no sampled value is used.
+
+## Independent parametric support certificate (20260730)
+
+[`code/parametric_replay_certificate.py`](../../code/parametric_replay_certificate.py) takes a different route from both the prefix enumeration and the proof-step ledger: it implements the source `H_1^b` and `H_2^b` supports as typed integer/marker schemas and checks their membership identities, exclusions, phase invariant, and withheld-output construction directly. It SHA-checks `source_limit.tex` (`938571ce9aa768f3665b41425b1284cc0067e3bef39ccb7f9b2fcc34102e1a12`) and the source theorem anchors before running.
+
+The exact CPU run checked 1,331,520 support-region obligations over 266,240 finite parameter instantiations, 4,096 stalled-phase instances, and the two-row Boolean first-difference kernel for the arbitrary-bitstream injection. The phase constructor verifies `J_0=z` and `J_n>J_(n-1)>=z`; each constructed `J_n` is absent from the realized `H_2^z` arbitrary subset, while a stalled phase has the source `H_1^(z-1)` tail and only the forced `*^z` marker outside support, legally replayed. The finite loops are sanity instantiations; the support functions and phase identities are parameterized over integers rather than fitted to a prefix cutoff.

pages/claim-6-claim-6/page.md

@@ -28,3 +28,5 @@ All four possible first outputs were checked at replay scales `1,3,7,15`, for
 **16 exact cells**. Every cell has a replay-valid sequence that enumerates both
 opposite-sign target supports, while the common half-line contains no support
 of a class member. All 16 support-intersection contradictions hold exactly.
+
+**Fresh finite-class protection regime (20260730).** The independent [`code/parametric_replay_certificate.py`](../../code/parametric_replay_certificate.py) rechecked all four possible first hypotheses at eight replay scales `1,3,7,15,31,63,127,255`, for 32 exact cells. Every replay sequence enumerates both positive-target supports while the common intersection contains no support of any class member. The producer also SHA-checks the source `source_proper.tex` and the finite-class theorem anchor.