diff --git a/research/complex-decoder-field-extension-seed44/CERTIFICATE.json b/research/complex-decoder-field-extension-seed44/CERTIFICATE.json index 704c869752..c9724c438c 100644 --- a/research/complex-decoder-field-extension-seed44/CERTIFICATE.json +++ b/research/complex-decoder-field-extension-seed44/CERTIFICATE.json @@ -5422,9 +5422,10 @@ "files": { "research/complex-frame-pair-decoders/PROOF.md": "ba53c1d8a9bc2d935d546bde46ca7341bd65f8515013e07b073296b4db2a9a74", "research/complex-frame-pair-decoders/README.md": "edd848b0177dc73a6e2646d4fd82f0b2ceae37e642bf19d6af602579a041a57e", - "research/complex-frame-pair-decoders/verify.py": "bdf7ee497dc04dfc634ee5b7848f6a2b39b0169668fb1a60a9715111dbd15395" + "research/frame-pair-enumeration-production/baseline.py": "bdf7ee497dc04dfc634ee5b7848f6a2b39b0169668fb1a60a9715111dbd15395" }, - "hash_policy": "SHA256 with CRLF normalized to LF" + "hash_policy": "SHA256 with CRLF normalized to LF", + "note": "After research/frame-pair-enumeration-production/, pairwise verify.py bytes are pinned via that package baseline.py." }, "status": "PASS_COMPLEX_DECODER_FIELD_EXTENSION_S44", "theorem": "For arbitrary complex D,T with exactly eight columns and D T^transpose = 2G on all live pairs, p<=24 implies cost>=max(72-p,56). Existing real attainments show sharpness over puncture sets of each size." diff --git a/research/complex-decoder-field-extension-seed44/SOURCES.json b/research/complex-decoder-field-extension-seed44/SOURCES.json index 63ca3fed7f..8dbc2c430f 100644 --- a/research/complex-decoder-field-extension-seed44/SOURCES.json +++ b/research/complex-decoder-field-extension-seed44/SOURCES.json @@ -3,7 +3,8 @@ "files": { "research/complex-frame-pair-decoders/PROOF.md": "ba53c1d8a9bc2d935d546bde46ca7341bd65f8515013e07b073296b4db2a9a74", "research/complex-frame-pair-decoders/README.md": "edd848b0177dc73a6e2646d4fd82f0b2ceae37e642bf19d6af602579a041a57e", - "research/complex-frame-pair-decoders/verify.py": "bdf7ee497dc04dfc634ee5b7848f6a2b39b0169668fb1a60a9715111dbd15395" + "research/frame-pair-enumeration-production/baseline.py": "bdf7ee497dc04dfc634ee5b7848f6a2b39b0169668fb1a60a9715111dbd15395" }, - "hash_policy": "SHA256 with CRLF normalized to LF" + "hash_policy": "SHA256 with CRLF normalized to LF", + "note": "After research/frame-pair-enumeration-production/, pairwise verify.py bytes are pinned via that package baseline.py." } diff --git a/research/complex-decoder-field-extension-seed44/replay_source.py b/research/complex-decoder-field-extension-seed44/replay_source.py index 759fccae73..91989529a6 100644 --- a/research/complex-decoder-field-extension-seed44/replay_source.py +++ b/research/complex-decoder-field-extension-seed44/replay_source.py @@ -13,7 +13,8 @@ if not __debug__:raise SystemExit('predecessor assertions must be enabled') sys.dont_write_bytecode=True here=Path(__file__).resolve().parent -source=here.parents[1]/'research/complex-frame-pair-decoders/verify.py' +# Pairwise-era PR968 model; production verify.py ships the neighborhood enumerator. +source=here.parents[1]/'research/frame-pair-enumeration-production/baseline.py' spec=importlib.util.spec_from_file_location('credited_pr968',source) m=importlib.util.module_from_spec(spec);spec.loader.exec_module(m) with contextlib.redirect_stdout(io.StringIO()) as captured: diff --git a/research/complex-decoder-field-extension-seed44/verify.py b/research/complex-decoder-field-extension-seed44/verify.py index 2edd4ad1d5..732c051110 100644 --- a/research/complex-decoder-field-extension-seed44/verify.py +++ b/research/complex-decoder-field-extension-seed44/verify.py @@ -18,7 +18,9 @@ HERE=Path(__file__).resolve().parent ROOT=HERE.parents[1] BASE='2921874911956718fcaaaf9396fe8267b3cfa9f0' -SOURCES={'research/complex-frame-pair-decoders/'+name for name in ('PROOF.md','README.md','verify.py')} +SOURCES={'research/complex-frame-pair-decoders/PROOF.md', + 'research/complex-frame-pair-decoders/README.md', + 'research/frame-pair-enumeration-production/baseline.py'} spec=importlib.util.spec_from_file_location('gaussian_exact',HERE/'exact.py') ex=importlib.util.module_from_spec(spec);spec.loader.exec_module(ex) G=ex.G diff --git a/research/complex-frame-pair-decoders/verify.py b/research/complex-frame-pair-decoders/verify.py index 57dd8993e8..82469892e9 100644 --- a/research/complex-frame-pair-decoders/verify.py +++ b/research/complex-frame-pair-decoders/verify.py @@ -371,30 +371,45 @@ def rec(clique, cand): def frame_pair_solutions(F0, F1): """All splits: row normals S (from F0) and T (from F1); every column partner is a cross-frame line with - odd inner product and orthogonal to all other row normals.""" + odd inner product and orthogonal to all other row normals. + + Eight-bit neighborhood masks (woklerx #1099 / frame-pair-enumeration-fast-seed93) + preserve the exact search domain, acceptance condition, multiplicity and order. + """ + if len(F0) != 8 or len(F1) != 8 or len(set(F0 + F1)) != 16: + raise ValueError('two disjoint ordered eight-element frames required') + neighbors = [sum(bool(IP[g][f]) << j for j, f in enumerate(F0)) for g in F1] + reverse_neighbors = [sum(bool(IP[f][g]) << j for j, g in enumerate(F1)) for f in F0] sols = [] - for smask in range(256): - S = [F0[j] for j in range(8) if smask >> j & 1] - need = 8 - len(S) - # g in F1 is usable as the partner of f in S iff N(g) cap S == {f} - part = {f: [g for g in F1 if [x for x in S if IP[g][x]] == [f]] for f in S} - if any(not part[f] for f in S): + for selected in range(256): + left = [j for j in range(8) if selected >> j & 1] + partners = [[] for _ in range(8)] + for g, adjacent in enumerate(neighbors): + hit = adjacent & selected + if hit and hit & (hit - 1) == 0: + partners[hit.bit_length() - 1].append(g) + if any(not partners[f] for f in left): continue - for choice in itertools.product(*[part[f] for f in S]): - if len(set(choice)) != len(S): + for choice in itertools.product(*(partners[f] for f in left)): + # Retain the reference injectivity guard even though singleton + # neighborhoods already partition these first-partner lists. + if len(set(choice)) != len(left): continue - Tset = [g for g in F1 if g not in choice] - if len(Tset) != need: + chosen = sum(1 << g for g in choice) + right = [g for g in range(8) if not chosen >> g & 1] + remainder = [f for f in range(8) if not selected >> f & 1] + second = [[] for _ in range(8)] + for f in remainder: + hit = reverse_neighbors[f] & (255 ^ chosen) + if hit and hit & (hit - 1) == 0: + second[hit.bit_length() - 1].append(f) + if any(not second[g] for g in right): continue - rest = [f for f in F0 if f not in S] - part2 = {g: [f for f in rest if [x for x in Tset if IP[f][x]] == [g]] for g in Tset} - if any(not part2[g] for g in Tset): - continue - for choice2 in itertools.product(*[part2[g] for g in Tset]): - if len(set(choice2)) != len(Tset): + for choice2 in itertools.product(*(second[g] for g in right)): + if len(set(choice2)) != len(right): continue - pairs = list(zip(S, choice)) + list(zip(Tset, choice2)) - sols.append(pairs) + sols.append([(F0[f], F1[g]) for f, g in zip(left, choice)] + + [(F1[g], F0[f]) for g, f in zip(right, choice2)]) return sols diff --git a/research/complex-general-normal-boundary/SOURCES.json b/research/complex-general-normal-boundary/SOURCES.json index ebb466bff8..331e1cf8e7 100644 --- a/research/complex-general-normal-boundary/SOURCES.json +++ b/research/complex-general-normal-boundary/SOURCES.json @@ -28,9 +28,10 @@ }, { "path": "research/complex-frame-pair-decoders/verify.py", - "usage": "input", + "usage": "provenance", "git_blob": "57dd8993e8ac016e8a92a9a885392b58014137bb", - "sha256": "bdf7ee497dc04dfc634ee5b7848f6a2b39b0169668fb1a60a9715111dbd15395" + "sha256": "bdf7ee497dc04dfc634ee5b7848f6a2b39b0169668fb1a60a9715111dbd15395", + "note": "Pairwise-era digest retained as provenance after research/frame-pair-enumeration-production/; working verify.py ships eight-bit neighborhood enumeration." }, { "path": "research/root-pair-first-drop-seed48/CERTIFICATE.json", diff --git a/research/complex-general-normal-boundary/VERIFY.json b/research/complex-general-normal-boundary/VERIFY.json index 633dd494b2..644d429640 100644 --- a/research/complex-general-normal-boundary/VERIFY.json +++ b/research/complex-general-normal-boundary/VERIFY.json @@ -6,7 +6,6 @@ "inputs": [ "research/complex-decoder-field-extension-seed44/PROOF.md", "research/complex-frame-pair-decoders/PROOF.md", - "research/complex-frame-pair-decoders/verify.py", "research/root-pair-first-drop-seed48/CERTIFICATE.json", "research/root-pair-first-drop-seed48/PROOF.md", "research/root-pair-first-drop-seed48/explore.py" diff --git a/research/complex-puncture-depth-ceiling/SOURCES.json b/research/complex-puncture-depth-ceiling/SOURCES.json index f53e98e237..8e0287981c 100644 --- a/research/complex-puncture-depth-ceiling/SOURCES.json +++ b/research/complex-puncture-depth-ceiling/SOURCES.json @@ -34,9 +34,10 @@ }, { "path": "research/complex-frame-pair-decoders/verify.py", - "usage": "input", + "usage": "provenance", "git_blob": "57dd8993e8ac016e8a92a9a885392b58014137bb", - "sha256": "bdf7ee497dc04dfc634ee5b7848f6a2b39b0169668fb1a60a9715111dbd15395" + "sha256": "bdf7ee497dc04dfc634ee5b7848f6a2b39b0169668fb1a60a9715111dbd15395", + "note": "Pairwise-era digest retained as provenance after research/frame-pair-enumeration-production/; working verify.py ships eight-bit neighborhood enumeration." }, { "path": "research/complex-local-word-ceiling/RESULT.json", diff --git a/research/complex-puncture-depth-ceiling/VERIFY.json b/research/complex-puncture-depth-ceiling/VERIFY.json index ae9632b96b..8f73c3d9d2 100644 --- a/research/complex-puncture-depth-ceiling/VERIFY.json +++ b/research/complex-puncture-depth-ceiling/VERIFY.json @@ -8,7 +8,6 @@ "research/community-frontier1094-audit/ASSEMBLY.json", "research/community-frontier1094-audit/INDEPENDENT1094.json", "research/complex-frame-pair-decoders/README.md", - "research/complex-frame-pair-decoders/verify.py", "research/complex-local-word-ceiling/RESULT.json", "research/complex-local-word-ceiling/ceiling.py" ], diff --git a/research/e8-connectivity-incidence-boundary/SOURCES.json b/research/e8-connectivity-incidence-boundary/SOURCES.json index b525be1c0a..68cc223086 100644 --- a/research/e8-connectivity-incidence-boundary/SOURCES.json +++ b/research/e8-connectivity-incidence-boundary/SOURCES.json @@ -22,9 +22,10 @@ }, { "path": "research/complex-frame-pair-decoders/verify.py", - "usage": "input", + "usage": "provenance", "git_blob": "57dd8993e8ac016e8a92a9a885392b58014137bb", - "sha256": "bdf7ee497dc04dfc634ee5b7848f6a2b39b0169668fb1a60a9715111dbd15395" + "sha256": "bdf7ee497dc04dfc634ee5b7848f6a2b39b0169668fb1a60a9715111dbd15395", + "note": "Pairwise-era digest retained as provenance after research/frame-pair-enumeration-production/; working verify.py ships eight-bit neighborhood enumeration." } ] } diff --git a/research/e8-connectivity-incidence-boundary/VERIFY.json b/research/e8-connectivity-incidence-boundary/VERIFY.json index d4e95db8ce..9695465a85 100644 --- a/research/e8-connectivity-incidence-boundary/VERIFY.json +++ b/research/e8-connectivity-incidence-boundary/VERIFY.json @@ -4,8 +4,7 @@ "python": "3.12", "requirements": [], "inputs": [ - "research/complex-frame-pair-decoders/PROOF.md", - "research/complex-frame-pair-decoders/verify.py" + "research/complex-frame-pair-decoders/PROOF.md" ], "commands": [ { @@ -20,7 +19,13 @@ "checks": "Regenerate genuine E8 frames, 28 connected graphs, exact upper/lower rank bounds, extra kernel independence, full-family and one-frame-repair positive controls; pivot-only rejection." }, { - "argv": ["{python}", "-I", "-O", "-B", "{package}/test_verify.py"], + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/test_verify.py" + ], "timeout_seconds": 120, "checks": "Positive optimized CLI replay; deleted pivot, unknown negative support, disconnected signs, false rank and missing graph receipt rejection controls." } diff --git a/research/e8-factor-linear-overcomplete47/SOURCES.json b/research/e8-factor-linear-overcomplete47/SOURCES.json index 97b095cc5b..0f2d8e0a47 100644 --- a/research/e8-factor-linear-overcomplete47/SOURCES.json +++ b/research/e8-factor-linear-overcomplete47/SOURCES.json @@ -2,14 +2,15 @@ "base": "c0e3631dc24e3c24a861f7d3d79e0608481cccec", "files": { "research/complex-decoder-field-extension-seed44/PROOF.md": "a89530576d8a5e1ae8778d601b37140d954212cd46e06b87a3f565294ee251a2", - "research/complex-decoder-field-extension-seed44/SOURCES.json": "788c48817795740df3b997e3bf949298371138c37889d9f6b0c1e8fadffa442a", + "research/complex-decoder-field-extension-seed44/SOURCES.json": "645487fef9fcc9795f49ae900f00dcc8b8aaa6e2eb0394a0103945d67d45343b", "research/complex-decoder-field-extension-seed44/exact.py": "68902522a71053059f94d8f71ce9eed720fbe08603acbe5a4735d2c9305ac0ee", - "research/complex-decoder-field-extension-seed44/replay_source.py": "304c41e52b37270f3ed82aef5bc401737499aa8864959100475904d2ffd0b409", - "research/complex-decoder-field-extension-seed44/verify.py": "1c26de9d6a91ec1dc605ca4e9de7a05da3b44709b2efa9d1d6e285b783db89e0", + "research/complex-decoder-field-extension-seed44/replay_source.py": "9f585f714c71764100c0ffede9933284d856709316466b43337df30dcb847433", + "research/complex-decoder-field-extension-seed44/verify.py": "2ab6f1aad7b8e7c94899756c09940029a3d23433c65fc48ae73a462f126e7500", "research/complex-frame-pair-decoders/PROOF.md": "ba53c1d8a9bc2d935d546bde46ca7341bd65f8515013e07b073296b4db2a9a74", "research/complex-frame-pair-decoders/README.md": "edd848b0177dc73a6e2646d4fd82f0b2ceae37e642bf19d6af602579a041a57e", - "research/complex-frame-pair-decoders/verify.py": "bdf7ee497dc04dfc634ee5b7848f6a2b39b0169668fb1a60a9715111dbd15395" + "research/frame-pair-enumeration-production/baseline.py": "bdf7ee497dc04dfc634ee5b7848f6a2b39b0169668fb1a60a9715111dbd15395" }, "selected_sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32", - "hash_domain": "SHA256 source bytes after CRLF-to-LF normalization" + "hash_domain": "SHA256 source bytes after CRLF-to-LF normalization", + "note": "After research/frame-pair-enumeration-production/, pairwise verify.py bytes are pinned via that package baseline.py; complex-decoder pins refreshed after the same retarget." } diff --git a/research/e8-factor-linear-overcomplete47/verify.py b/research/e8-factor-linear-overcomplete47/verify.py index 6fc2229c3e..682d8f4b8c 100644 --- a/research/e8-factor-linear-overcomplete47/verify.py +++ b/research/e8-factor-linear-overcomplete47/verify.py @@ -11,7 +11,9 @@ BASE='c0e3631dc24e3c24a861f7d3d79e0608481cccec' OLD='research/complex-decoder-field-extension-seed44/' PAIR='research/complex-frame-pair-decoders/' -PATHS={OLD+x for x in ('PROOF.md','verify.py','exact.py','replay_source.py','SOURCES.json')}|{PAIR+x for x in ('PROOF.md','README.md','verify.py')} +PATHS={OLD+x for x in ('PROOF.md','verify.py','exact.py','replay_source.py','SOURCES.json')}|{ + PAIR+'PROOF.md', PAIR+'README.md', + 'research/frame-pair-enumeration-production/baseline.py'} def need(ok,msg): if not ok:raise ValueError(msg) diff --git a/research/frame-pair-enumeration-fast-seed93/README.md b/research/frame-pair-enumeration-fast-seed93/README.md index 39c72a3333..f77982610e 100644 --- a/research/frame-pair-enumeration-fast-seed93/README.md +++ b/research/frame-pair-enumeration-fast-seed93/README.md @@ -1,5 +1,8 @@ # Faster exact frame-pair enumeration +After `research/frame-pair-enumeration-production/`, the pairwise checker bytes live in [`baseline.py`](baseline.py); production `complex-frame-pair-decoders/verify.py` ships the neighborhood enumerator. + + Precomputed eight-bit neighborhoods accelerate PR968's complete frame-split search while preserving every ordered solution and its existing exact checks. On the recorded Windows CPython run, the enumeration median is **4.57x faster**; diff --git a/research/frame-pair-enumeration-fast-seed93/SOURCES.json b/research/frame-pair-enumeration-fast-seed93/SOURCES.json index 724455078e..e1ddc45355 100644 --- a/research/frame-pair-enumeration-fast-seed93/SOURCES.json +++ b/research/frame-pair-enumeration-fast-seed93/SOURCES.json @@ -1,8 +1,9 @@ { "base_commit": "abdc6a7002abdbcd9e21bfc5e1a795784deacfdf", "files": { - "research/complex-frame-pair-decoders/verify.py": "bdf7ee497dc04dfc634ee5b7848f6a2b39b0169668fb1a60a9715111dbd15395" + "research/frame-pair-enumeration-fast-seed93/baseline.py": "bdf7ee497dc04dfc634ee5b7848f6a2b39b0169668fb1a60a9715111dbd15395" }, "hash_convention": "SHA256 after CRLF to LF normalization; all other bytes retained", - "predecessor": "themilkman216 PR968, Apache-2.0; exact source split order and checks retained" + "predecessor": "themilkman216 PR968, Apache-2.0; exact source split order and checks retained", + "note": "After research/frame-pair-enumeration-production/, pairwise bytes are vendored in baseline.py." } diff --git a/research/frame-pair-enumeration-fast-seed93/baseline.py b/research/frame-pair-enumeration-fast-seed93/baseline.py new file mode 100644 index 0000000000..57dd8993e8 --- /dev/null +++ b/research/frame-pair-enumeration-fast-seed93/baseline.py @@ -0,0 +1,740 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Frame-pair decoders and the exact 8-term copy-cost floor on punctured complex E8 units. + +Standard library only. Exact integer, F2 and rational arithmetic throughout. + +Model (PR717 B14, D2/D3 scope): the 120 E8 root lines; a puncture P removes lines; an exact +8-term decoder is D = R A, T = R B with A B^T = 2 I, so that D T^T = 2G on the live lines +(G the integer inner products). Term k costs the F2 rank of the label pairing between its row +support (live lines not orthogonal to a_k) and column support (live lines not orthogonal to b_k). +The label pairing of two lines is ( + 1) mod 2, which this script uses directly; it +never constructs PR717's simple-root coordinates. + +Sections (each prints PASS/FAIL lines): + A model facts: 120 lines, nondegenerate rank-9 pairing, distinct pairing rows + B violator census for the eight W(E8) hyperplane-flat types (all 511 hyperplanes and all + 130,305 codimension-2 pairs of F2^9 functionals) + C the D7 orbit: 1080 directions, unique 14-line violator sets, pairwise unions >= 21, no + coincidence with a root functional + D frame-pair census: all 1260 frames disjoint from the coordinate frame, all (S, T) splits; + every solution is built and checked exactly + E attaining chain: explicit exact decoders for every puncture size p = 0..24 + F replay of the three vendored PR717 D3 hits and their root-pair structure + G favorable-budget pricing on the selected (U8/T37) profile with the pinned moment and outer + engines, and the PR589 bit-supplier cap + H negative controls +""" +import argparse +import hashlib +import importlib.util +import itertools +import json +import math +import sys +from collections import Counter +from fractions import Fraction as Q +from pathlib import Path + +HERE = Path(__file__).resolve().parent +FAILS = [] +LOG = [] + + +def check(tag, cond, info=''): + line = ('PASS ' if cond else 'FAIL ') + tag + (' | ' + info if info else '') + print(line, flush=True) + LOG.append(line) + if not cond: + FAILS.append(tag) + + +# ---------------------------------------------------------------- A. E8 lines and pairing +def e8_roots(): + """240 roots in doubled coordinates; same enumeration order as PR717's e8model (adapter only).""" + roots = [] + for i, j in itertools.combinations(range(8), 2): + for si in (1, -1): + for sj in (1, -1): + v = [0] * 8 + v[i], v[j] = 2 * si, 2 * sj + roots.append(tuple(v)) + for s in itertools.product((1, -1), repeat=8): + if s.count(-1) % 2 == 0: + roots.append(tuple(s)) + return roots + + +def dot(x, y): + return sum(a * b for a, b in zip(x, y)) + + +def ip(x, y): + """True inner product of doubled-coordinate vectors.""" + d = dot(x, y) + assert d % 4 == 0 + return d // 4 + + +def neg(v): + return tuple(-a for a in v) + + +ROOTS = e8_roots() +LINES = [] +_seen = set() +for r in ROOTS: + key = r if r > neg(r) else neg(r) + if key not in _seen: + _seen.add(key) + LINES.append(r) +NL = len(LINES) +IP = [[ip(LINES[i], LINES[j]) for j in range(NL)] for i in range(NL)] +# Label pairing as a 120-bit row mask: bit j of NROW[i] is ( + 1) mod 2. +NROW = [sum(((IP[i][j] + 1) & 1) << j for j in range(NL)) for i in range(NL)] +ALL = (1 << NL) - 1 +FRAME0 = [] +for a in range(4): + for s in (1, -1): + v = [0] * 8 + v[2 * a], v[2 * a + 1] = 2, 2 * s + FRAME0.append(LINES.index(tuple(v))) +P112 = [i for i in range(NL) if i not in FRAME0] + + +def popcount(x): + return bin(x).count('1') + + +def f2_rank(rows): + basis = {} + rank = 0 + for v in rows: + while v: + h = v.bit_length() - 1 + if h in basis: + v ^= basis[h] + else: + basis[h] = v + rank += 1 + break + return rank + + +def mask(idx): + m = 0 + for i in idx: + m |= 1 << i + return m + + +def pair_rank(rows, cols): + """F2 rank of the label pairing between the lines in `rows` and the lines in `cols`.""" + cm = mask(cols) + return f2_rank([NROW[i] & cm for i in rows]) + + +def span_dim(idx): + return f2_rank([NROW[i] for i in idx]) + + +def section_a(): + check('A.lines', NL == 120 and len(ROOTS) == 240, '120 lines from 240 roots') + check('A.pairing-values', all(IP[i][i] == 2 for i in range(NL)) and + {IP[i][j] for i in range(NL) for j in range(NL) if i != j} == {-1, 0, 1}, + 'line inner products are 2 on the diagonal and 0/+-1 off it') + check('A.pairing-rank-9', f2_rank(NROW) == 9, 'the 120x120 label pairing has F2 rank 9 (nondegenerate on the 9-dim label span)') + check('A.distinct-rows', len(set(NROW)) == 120, 'distinct lines have distinct pairing rows (distinct label functionals)') + check('A.frame0', len(FRAME0) == 8 and all(IP[a][b] == 0 for a in FRAME0 for b in FRAME0 if a != b), + 'coordinate frame e_{2a} +- e_{2a+1}: eight mutually orthogonal lines; P112 has %d lines' % len(P112)) + + +# Dual coordinates: phi_i = (pairing with nine basis lines). An F2-linear isomorphism of the label span, +# so the 511 nonzero functionals lambda . phi_i are exactly the 511 hyperplanes of the label space. +def dual_coordinates(): + basis = [] + for i in range(NL): + if f2_rank([NROW[b] for b in basis] + [NROW[i]]) == len(basis) + 1: + basis.append(i) + if len(basis) == 9: + break + phi = [sum(((NROW[i] >> b) & 1) << k for k, b in enumerate(basis)) for i in range(NL)] + return basis, phi + + +BASIS9, PHI = dual_coordinates() +LAMBDAS = list(range(1, 512)) +VMASK = {lam: mask(i for i in range(NL) if popcount(lam & PHI[i]) & 1) for lam in LAMBDAS} +ROOT_FUNCTIONAL = {} +for _i in range(NL): + # the functional of line i: lambda with lambda . phi_j = pairing(i, j) for all j + _cands = [lam for lam in LAMBDAS if VMASK[lam] == NROW[_i]] + assert len(_cands) == 1 + ROOT_FUNCTIONAL[_i] = _cands[0] + + +# ---------------------------------------------------------------- B. violator census +def solve_rational(M, rhs): + """Solve M x = rhs exactly (M square, invertible) with Fractions.""" + n = len(M) + A = [[Q(x) for x in row] + [Q(b)] for row, b in zip(M, rhs)] + for c in range(n): + p = next(r for r in range(c, n) if A[r][c] != 0) + A[c], A[p] = A[p], A[c] + for r in range(n): + if r != c and A[r][c] != 0: + f = A[r][c] / A[c][c] + A[r] = [x - f * y for x, y in zip(A[r], A[c])] + return [A[i][n] / A[i][i] for i in range(n)] + + +SIMPLE = [(1, -1, -1, -1, -1, -1, -1, 1), (2, 2, 0, 0, 0, 0, 0, 0), (-2, 2, 0, 0, 0, 0, 0, 0)] + \ + [tuple(-2 if t == k else 2 if t == k + 1 else 0 for t in range(8)) for k in range(1, 6)] + + +def fundamental_weights(): + """omega_i with = delta_ij, as integer doubled-coordinate directions.""" + out = [] + for i in range(8): + # unknown x (true coordinates): sum_t x_t * alpha_j[t]/2 = delta_ij + M = [[Q(a, 2) for a in alpha] for alpha in SIMPLE] + x = solve_rational(M, [1 if j == i else 0 for j in range(8)]) + den = 1 + for v in x: + den = den * v.denominator // math.gcd(den, v.denominator) + vec = tuple(int(v * den) for v in x) + out.append(vec) + return out + + +def support_mask(a): + return mask(i for i in range(NL) if dot(a, LINES[i]) != 0) + + +def census_type(a): + C = support_mask(a) + sizes = sorted(popcount(VMASK[lam] & C) for lam in LAMBDAS) + vm = [VMASK[lam] & C for lam in LAMBDAS] + pi7 = min(popcount(vm[x] | vm[y]) for x in range(511) for y in range(x + 1, 511)) + span = f2_rank([NROW[i] for i in range(NL) if C >> i & 1]) + return dict(support=popcount(C), flat_lines=NL - popcount(C), span=span, pi8=sizes[0], pi8_second=sizes[1], pi7=pi7) + + +EXPECTED_TYPES = { # flat lines -> (subsystem, |C|, pi8, second pi8, pi7) + 63: ('E7', 57, 1, 24, 25), 42: ('D7', 78, 14, 34, 42), 37: ('E6+A1', 83, 27, 28, 51), + 28: ('A7', 92, 28, 35, 56), 23: ('D5+A2', 97, 33, 41, 61), 22: ('A6+A1', 98, 35, 35, 62), + 16: ('A4+A3', 104, 40, 43, 68), 14: ('A4+A2+A1', 106, 43, 43, 70)} + + +def section_b(): + weights = fundamental_weights() + check('B.weights', all(sum(Q(dot(w, a), 4) == 0 for a in SIMPLE) == 7 for w in weights), + 'eight fundamental-weight directions, each orthogonal to seven simple roots') + rows = {} + for w in weights: + info = census_type(w) + rows[info['flat_lines']] = info + ok = set(rows) == set(EXPECTED_TYPES) and all( + (rows[f]['support'], rows[f]['pi8'], rows[f]['pi8_second'], rows[f]['pi7']) == EXPECTED_TYPES[f][1:] + and rows[f]['span'] == 9 for f in rows) + table = '; '.join('%s flat %d: |C|=%d pi8=%d (next %d) pi7=%d' % (EXPECTED_TYPES[f][0], f, rows[f]['support'], + rows[f]['pi8'], rows[f]['pi8_second'], rows[f]['pi7']) for f in sorted(rows, reverse=True)) + check('B.census', ok, table) + nonroot = min(rows[f]['pi8'] for f in rows if f != 63) + check('B.thresholds', nonroot == 14 and rows[63]['pi8_second'] == 24 and min(r['pi7'] for r in rows.values()) == 25, + 'only E7 (root) normals drop to an 8-dim span with one puncture (their own line); every other type needs >= 14; ' + 'a root normal by another hyperplane needs >= 24; any 7-dim span needs >= 25 punctures') + # the root type's unique one-line violator set is the line itself, through its own functional + alpha = next(i for i in range(NL) if LINES[i] == (2, 2, 0, 0, 0, 0, 0, 0)) + C = support_mask(LINES[alpha]) + check('B.root-self-line', VMASK[ROOT_FUNCTIONAL[alpha]] & C == 1 << alpha, + 'for a root normal alpha the 1-line violator set is {alpha}, via the functional of alpha itself') + allroots = True + for i in range(NL): + C = support_mask(LINES[i]) + sizes = sorted((popcount(VMASK[lam] & C), lam) for lam in LAMBDAS) + allroots &= sizes[0] == (1, ROOT_FUNCTIONAL[i]) and VMASK[ROOT_FUNCTIONAL[i]] & C == 1 << i and sizes[1][0] == 24 + check('B.root-all-120', allroots, 'checked directly for all 120 root normals: unique 1-line set {alpha}; every other hyperplane >= 24') + return rows, weights + + +# ---------------------------------------------------------------- C. D7 orbit +def canon(v): + g = 0 + for a in v: + g = math.gcd(g, abs(a)) + v = tuple(a // g for a in v) + first = next(a for a in v if a) + return v if first > 0 else neg(v) + + +def orbit(start): + seen = {canon(start)} + frontier = [canon(start)] + while frontier: + nxt = [] + for v in frontier: + for r in LINES: + d = dot(v, r) + u = tuple(4 * a - d * b for a, b in zip(v, r)) # 4 * reflection, integral + c = canon(u) + if c not in seen: + seen.add(c) + nxt.append(c) + frontier = nxt + return sorted(seen) + + +def section_c(weights): + d7 = next(w for w in weights if NL - popcount(support_mask(w)) == 42) + dirs = orbit(d7) + check('C.orbit', len(dirs) == 1080, 'W(E8) orbit of the D7 normal: %d directions' % len(dirs)) + v14 = {} + root_funcs = set(ROOT_FUNCTIONAL.values()) + coincide = 0 + inflat_all = True + rank_ok = True + for d in dirs: + C = support_mask(d) + sizes = sorted((popcount(VMASK[lam] & C), lam) for lam in LAMBDAS) + assert sizes[0][0] == 14 and sizes[1][0] >= 34 + lam = sizes[0][1] + v14[d] = VMASK[lam] & C + coincide += lam in root_funcs + flat = [i for i in range(NL) if not C >> i & 1] + inflat_all &= all(popcount(VMASK[lam] >> i & 1) for i in flat) + # removing any one flat line leaves a rank-7 set: a flat of rank <= 6 misses >= 2 of the 42 lines + # (not needed by the main argument; recorded as a cross-check of D7 rigidity) + if d == dirs[0]: + rank_ok = all(rank_q([LINES[j] for j in flat if j != i]) == 7 for i in flat) + sets = list(v14.values()) + check('C.unique-14', len(set(sets)) == 1080, 'each D7 direction has a unique 14-line violator set (next >= 34); 1080 distinct sets') + mn = min(popcount(a | b) for a, b in itertools.combinations(sets, 2)) + check('C.unions', mn == 21, 'any two distinct D7 violator sets have union >= %d > 15' % mn) + check('C.no-root-coincidence', coincide == 0, 'no D7 minimizing functional equals a root functional') + check('C.flat-lines-violate', inflat_all and rank_ok, 'all 42 flat lines violate the minimizing functional; flat minus any line has rank 7') + return len(dirs) + + +def rank_q(vectors): + rows = [[Q(x) for x in v] for v in vectors] + r = 0 + ncol = len(rows[0]) if rows else 0 + for c in range(ncol): + p = next((i for i in range(r, len(rows)) if rows[i][c] != 0), None) + if p is None: + continue + rows[r], rows[p] = rows[p], rows[r] + for i in range(len(rows)): + if i != r and rows[i][c] != 0: + f = rows[i][c] / rows[r][c] + rows[i] = [x - f * y for x, y in zip(rows[i], rows[r])] + r += 1 + return r + + +# ---------------------------------------------------------------- decoders +def decoder_cost(rowvecs, colvecs, live): + """Exactness of D T^T = 2G on `live` and the per-term costs.""" + live = list(live) + D = [[ip(LINES[i], a) for a in rowvecs] for i in live] + T = [[ip(LINES[i], b) for b in colvecs] for i in live] + exact = all(sum(x * y for x, y in zip(D[p], T[q])) == 2 * IP[live[p]][live[q]] + for p in range(len(live)) for q in range(len(live))) + costs = [] + for k in range(len(rowvecs)): + R = [live[p] for p in range(len(live)) if D[p][k]] + A = [live[p] for p in range(len(live)) if T[p][k]] + costs.append(pair_rank(R, A)) + return exact, costs + + +def frames_in(pool): + pool = list(pool) + orth = {i: mask(j for j in pool if j != i and IP[i][j] == 0) for i in pool} + out = [] + + def rec(clique, cand): + if len(clique) == 8: + out.append(tuple(clique)) + return + c = cand + while c: + j = c.bit_length() - 1 + c &= ~(1 << j) + rec(clique + [j], cand & orth[j] & ((1 << j) - 1)) + + for i in pool: + rec([i], orth[i] & ((1 << i) - 1)) + return sorted(tuple(sorted(f)) for f in out) + + +def frame_pair_solutions(F0, F1): + """All splits: row normals S (from F0) and T (from F1); every column partner is a cross-frame line with + odd inner product and orthogonal to all other row normals.""" + sols = [] + for smask in range(256): + S = [F0[j] for j in range(8) if smask >> j & 1] + need = 8 - len(S) + # g in F1 is usable as the partner of f in S iff N(g) cap S == {f} + part = {f: [g for g in F1 if [x for x in S if IP[g][x]] == [f]] for f in S} + if any(not part[f] for f in S): + continue + for choice in itertools.product(*[part[f] for f in S]): + if len(set(choice)) != len(S): + continue + Tset = [g for g in F1 if g not in choice] + if len(Tset) != need: + continue + rest = [f for f in F0 if f not in S] + part2 = {g: [f for f in rest if [x for x in Tset if IP[f][x]] == [g]] for g in Tset} + if any(not part2[g] for g in Tset): + continue + for choice2 in itertools.product(*[part2[g] for g in Tset]): + if len(set(choice2)) != len(Tset): + continue + pairs = list(zip(S, choice)) + list(zip(Tset, choice2)) + sols.append(pairs) + return sols + + +def pair_decoder(pairs, live): + """Root-pair decoder (a_k = alpha_k, b_k = 2 beta_k). Exactness on every live set is + equivalent to = 2 delta_kl, i.e. A^T B = 2I, hence A B^T = 2I and D T^T = R (A B^T) R^T = 2G.""" + dual = all((IP[a][b] in (1, -1)) if k == l else IP[a][b] == 0 + for k, (a, _) in enumerate(pairs) for l, (_, b) in enumerate(pairs)) + costs = [pair_rank([i for i in live if IP[a][i]], [i for i in live if IP[b][i]]) for a, b in pairs] + return dual, costs + + +def build_pairs(pairs): + rows, cols = [], [] + for a, b in pairs: + e = IP[a][b] + assert e in (1, -1) + rows.append(LINES[a]) + cols.append(tuple(2 * e * x for x in LINES[b])) + return rows, cols + + +def relative_type(F0, F1): + common = Counter(sum(1 for f in F0 if IP[g][f] and IP[h][f]) for g, h in itertools.combinations(F1, 2)) + return tuple(sorted(common.items())) + + +def section_d(): + F1s = frames_in(P112) + check('D.frames', len(F1s) == 1260, '%d frames inside P112 (disjoint from the coordinate frame)' % len(F1s)) + hist = Counter() + types = Counter() + built = 0 + allgood = True + example = None + for F1 in F1s: + sols = frame_pair_solutions(FRAME0, list(F1)) + hist[len(sols)] += 1 + types[(len(sols) > 0, relative_type(FRAME0, F1))] += 1 + live = [i for i in range(NL) if i not in FRAME0 and i not in F1] + for pairs in sols: + exact, costs = pair_decoder(pairs, live) + built += 1 + allgood &= exact and costs == [7] * 8 + if example is None: + example = dict(F1=list(F1), pairs=pairs) + check('D.census', hist == Counter({8: 896, 0: 364}), 'solutions per frame: %s' % dict(sorted(hist.items()))) + tdesc = {str(k): v for k, v in sorted(types.items(), key=lambda kv: -kv[1])} + check('D.types', len(types) == 3 and all(ok == (dict(t).get(4, 0) == 0) for ok, t in types), + 'relative position (common F0-neighbours of F1 pairs) -> admissible: %s' % tdesc) + check('D.exact-56', allgood and built == 7168, '%d frame-pair decoders built; every one satisfies A^T B = 2I and has eight cost-7 terms on its P104 (cst 56)' % built) + F1 = example['F1'] + live = [i for i in range(NL) if i not in FRAME0 and i not in F1] + rows, cols = build_pairs(example['pairs']) + exact, costs = decoder_cost(rows, cols, live) + check('D.full-exactness-crosscheck', exact and costs == [7] * 8, 'one decoder rechecked entrywise: D T^T = 2G on all 104 x 104 live pairs') + return F1s, example, hist, types + + +def section_e(F1s, example): + F1 = example['F1'] + pairs = example['pairs'] + # ordering of F1 lines: each F1 line is the self-line of exactly one term + f1order = [b if b in F1 else a for a, b in pairs] + chain = {} + extra = [i for i in range(NL) if i not in FRAME0 and i not in F1] + coord_rows = [LINES[f] for f in FRAME0] + for p in range(0, 25): + if p <= 8: + P = FRAME0[:p] + rows, cols = coord_rows, coord_rows + kind = 'coordinate frame, %d of its lines punctured' % p + else: + j = min(p - 8, 8) + P = FRAME0 + f1order[:j] + extra[:max(0, p - 16)] + rows, cols = build_pairs(pairs) + kind = 'frame pair, %d partner lines + %d extra lines punctured' % (j, max(0, p - 16)) + live = [i for i in range(NL) if i not in P] + exact, costs = decoder_cost(rows, cols, live) + bound = max(72 - p, 56) + chain[p] = dict(live=len(live), exact=exact, cost=sum(costs), lower_bound=bound, kind=kind, + ratio=str(Q(sum(costs), len(live))), punctured=sorted(P), live_rank=rank_q([LINES[i] for i in live])) + ok = all(c['exact'] and c['cost'] == c['lower_bound'] and c['live_rank'] == 8 and len(c['punctured']) == p + for p, c in chain.items()) + check('E.chain', ok, 'p=0..24: exact decoders with cst = max(72-p, 56) at every p (attaining the theorem)') + best = min(chain, key=lambda p: Q(chain[p]['cost'], chain[p]['live'])) + check('E.best-ratio', best == 16 and Q(chain[16]['cost'], chain[16]['live']) == Q(7, 13) and + Q(chain[8]['cost'], chain[8]['live']) == Q(4, 7), + 'minimum copy ratio along the chain is 56/104 = 7/13 at p = 16 (P112: 64/112 = 4/7)') + return chain + + +# ---------------------------------------------------------------- F. PR717 hit replay +def load_hit(path): + D, T = [], [] + for line in path.read_text().splitlines(): + s = line.strip() + if s.startswith('d:'): + D.append([int(x) for x in s[2:].split()]) + if s.startswith('t:'): + T.append([int(x) for x in s[2:].split()]) + return [list(c) for c in zip(*D)], [list(c) for c in zip(*T)] # live x n + + +def recover(live, col): + """Exact vector a with = col[p] for every live line; returns doubled coordinates or None.""" + idx = [] + for p, i in enumerate(live): + if rank_q([LINES[live[q]] for q in idx] + [LINES[i]]) == len(idx) + 1: + idx.append(p) + if len(idx) == 8: + break + M = [[Q(x, 4) for x in LINES[live[p]]] for p in idx] + a = solve_rational(M, [col[p] for p in idx]) + ok = all(sum(Q(x, 4) * y for x, y in zip(LINES[i], a)) == col[p] for p, i in enumerate(live)) + return a if ok else None + + +def as_line(a): + """Index of the root line parallel to a, or None.""" + for i, r in enumerate(LINES): + ratio = None + good = True + for x, y in zip(r, a): + if x == 0: + good &= y == 0 + else: + q = Q(y) / x + good &= ratio is None or q == ratio + ratio = q + if good and ratio: + return i + return None + + +def section_f(): + p112 = P112 + results = {} + vend = json.loads((HERE / 'SOURCES.json').read_text())['vendored'] + check('F.vendored-pins', all(sha(HERE / rel) == meta['sha256'] for rel, meta in vend.items()) and len(vend) == 3, + 'three PR717 decoder files match their SHA-256 pins (PR717 head %s)' % next(iter(vend.values()))['head'][:7]) + clique717 = [9, 15, 24, 46, 52, 66, 94, 104] # PR717 d3_punctures.py, P112 indexing + cases = [('P104_HIT_flip_3a.txt', [p112[q] for q in clique717]), ('P111_HIT_g0.txt', [p112[0]]), + ('P111_HIT_g111.txt', [p112[111]])] + for name, extra in cases: + punct = FRAME0 + extra + live = [i for i in range(NL) if i not in punct] + D, T = load_hit(HERE / 'inputs/pr717' / name) + recorded = [int(l.split()[3]) for l in (HERE / 'inputs/pr717' / name).read_text().splitlines() if l.startswith('term ')] + exact = all(sum(x * y for x, y in zip(D[p], T[q])) == 2 * IP[live[p]][live[q]] + for p in range(len(live)) for q in range(len(live))) + terms = [] + for k in range(len(D[0])): + a = recover(live, [row[k] for row in D]) + b = recover(live, [row[k] for row in T]) + R = [live[p] for p in range(len(live)) if D[p][k]] + A = [live[p] for p in range(len(live)) if T[p][k]] + la, lb = as_line(a), as_line(b) + terms.append(dict(cost=pair_rank(R, A), row_root=la, col_root=lb, + odd=(la is not None and lb is not None and IP[la][lb] % 2 != 0), + both_punctured=(la in punct and lb in punct))) + results[name] = dict(exact=exact, costs=[t['cost'] for t in terms], recorded_by_pr717=recorded, terms=terms) + check('F.%s.costs-match-pr717' % name, recorded == [t['cost'] for t in terms], + 'per-term pairing ranks from (+1) mod 2 equal the costs PR717 recorded with its own label model') + seven = [t for t in terms if t['cost'] == 7] + check('F.%s' % name, exact and all(t['row_root'] is not None and t['col_root'] is not None and t['odd'] and + t['both_punctured'] for t in seven) and + all(not (t['odd'] and t['both_punctured']) for t in terms if t['cost'] != 7), + 'exact; costs %s; every cost-7 term is an odd root pair with both lines punctured, and no other term is' + % sorted(Counter(t['cost'] for t in terms).items())) + # PR717's P104 clique is an admissible second frame + F1 = sorted(p112[q] for q in clique717) + sols = frame_pair_solutions(FRAME0, F1) + check('F.P104-clique-is-frame-pair', all(IP[a][b] == 0 for a in F1 for b in F1 if a != b) and len(sols) == 8, + "PR717's random clique is a frame of the admissible relative type with 8 frame-pair decoders") + return results + + +# ---------------------------------------------------------------- G. pricing +def sha(path): + return hashlib.sha256(path.read_bytes()).hexdigest() + + +def load_module(path, name): + spec = importlib.util.spec_from_file_location(name, path) + mod = importlib.util.module_from_spec(spec) + spec.loader.exec_module(mod) + return mod + + +def section_g(repo): + pins = json.loads((HERE / 'SOURCES.json').read_text())['pricing_inputs'] + for rel, h in pins.items(): + check('G.pin.' + rel.split('/')[-1], sha(repo / rel) == h, rel) + eng = repo / 'research/complex-k492-owner-repair/vendor/multicold/engines' + M = load_module(eng / 'moment.py', 'pinned_moment') + B2 = load_module(eng / 'base_two_moment.py', 'pinned_base_two_moment') + A = load_module(eng / 'outer.py', 'pinned_outer') + P = load_module(repo / 'research/complex-t21-owners/vendor/pr870/independent/price_profile_t16.py', 'pinned_t16') + bit = json.loads((repo / 'research/complex-t21-owners/vendor/pr870/inputs/PR589-EXPECTED.json').read_text()) + c = Q(bit['nine']['bit_lower']) + src = json.loads((HERE / 'SOURCES.json').read_text())['selected_record'] + sel = json.loads((repo / 'certificates/selected-result.json').read_text()) + check('G.selected-record', sel['certificate'] == src['certificate'] and sel['certificate_sha256'] == src['certificate_sha256'] + and sha(repo / sel['certificate']) == src['certificate_sha256'] and sel['kappa'] == src['kappa'], + 'pricing uses the selected record %s (%s)' % (sel['certificate'], sel['decimal'])) + asm = json.loads((repo / sel['certificate']).read_text()) + H0 = Counter({int(r): n for r, n in asm['complex_profile'].items()}) + m, cell = 73, (9 - 1) * 112 - 9 * 64 + mass = sum(r * n for r, n in H0.items()) + T = next(t for t in range(1, 1000) if m * 896 * t - mass == cell * t) + W0, D0, calls = 896 * T, cell * T, 9 * T + check('G.identity', m * W0 - mass == D0 and max(H0) == 48, + 'selected profile: %d replicas, 73*%d - mass = %d = %d*((9-1)*112 - 9*64)' % (T, W0, D0, T)) + + def scenario(ports, units): + """PR717 P1 knobs transported to the selected U8 profile: a cst unit lowers one centre cut climb 8 -> 7 in every call; + a port removes one modal source (1,1,1,5) and target (1,1,4,1,1) climb per call and nine idle + rank-48 children per replica.""" + H = Counter(H0) + H[8] -= units * calls + H[7] += units * calls + for _ in range(ports): + for x in (1, 1, 1, 5, 1, 1, 4, 1, 1): + H[x] -= calls + H[48] -= 9 * T + H = Counter({r: n for r, n in H.items() if n}) + W = W0 - T * 8 * ports + D = T * ((9 - 1) * (112 - ports) - 9 * (64 - units)) + assert all(n > 0 for n in H.values()) and m * W - sum(r * n for r, n in H.items()) == D + return H, W, D + + out = {} + for name, (ports, units) in [('selected', (0, 0)), ('P111_knobs', (1, 1)), ('P104_knobs', (8, 8))]: + H, W, D = scenario(ports, units) + native = Q(M.certify(H, m, W, False)['lower']) + conservative = Q(M.certify(H, m, W, True)['lower']) + checks = P.moment_checks(M, B2, H, m, W, native, D, False) + o = P.outer47(c, native, A) + out[name] = dict(W=W, deficit=D, complex_b=str(native), complex_b_decimal=P.decimal(native), + conservative_b_decimal=P.decimal(conservative), + b_change_percent=P.decimal((native / Q(asm['complex_lower']) - 1) * 100), + kappa=o['kappa'], kappa_decimal=o['kappa_decimal'], binding=o['binding'], + outer_controls_rejected=o['controls_rejected'], two_engines=len(checks) == 2) + cap = P.outer47(c, 2 * c, A) + out['bit_cap'] = dict(kappa=cap['kappa'], kappa_decimal=cap['kappa_decimal'], binding=cap['binding'], + gain_over_selected_percent=P.decimal((Q(cap['kappa']) / Q(sel['kappa']) - 1) * 100)) + check('G.gate', out['selected']['complex_b'] == str(Q(asm['complex_lower'])) and + Q(out['selected']['kappa']) == Q(sel['kappa']), + 'pinned engines on the selected profile reproduce b and kappa = %s exactly' % sel['decimal']) + check('G.P111', out['P111_knobs']['binding'] == 'complex', + 'P111 knobs: b %+.4f%%, kappa %s (complex-bound)' % (float(Q(out['P111_knobs']['b_change_percent'])), + out['P111_knobs']['kappa_decimal'])) + check('G.P104', out['P104_knobs']['binding'] == 'bit' and out['P104_knobs']['kappa'] == out['bit_cap']['kappa'], + 'P104 knobs: b %+.4f%% > bit c, kappa capped at %s' % (float(Q(out['P104_knobs']['b_change_percent'])), + out['P104_knobs']['kappa_decimal'])) + check('G.bit-cap', out['bit_cap']['binding'] == 'bit', + 'any complex-only change is capped by PR589 at kappa %s (%+.4f%%)' % ( + out['bit_cap']['kappa_decimal'], float(Q(out['bit_cap']['gain_over_selected_percent'])))) + headroom = Q(out['P104_knobs']['complex_b']) / c - 1 + out['P104_headroom_above_bit_percent'] = P.decimal(headroom * 100) + return out + + +# ---------------------------------------------------------------- H. negative controls +def section_h(example, F1s, hist): + F1 = example['F1'] + pairs = example['pairs'] + live104 = [i for i in range(NL) if i not in FRAME0 and i not in F1] + rows, cols = build_pairs(pairs) + # H1: perturb one column vector -> exactness lost + bad = list(cols) + bad[0] = tuple(x + y for x, y in zip(bad[0], LINES[FRAME0[0]])) + exact, _ = decoder_cost(rows, bad, live104) + check('H.mutated-decoder', not exact, 'adding a frame root to one column vector breaks D T^T = 2G') + # H2: restore one partner line -> that term costs 8 (cst 57 = 72 - 15) + restored = next(b if b in F1 else a for a, b in pairs) + live = live104 + [restored] + exact, costs = decoder_cost(rows, cols, live) + check('H.self-line-live', exact and sum(costs) == 57 and sorted(costs) == [7] * 7 + [8], + 'restoring one self-line raises exactly one term to 8: cst 57 at p = 15') + # H3: even pairing on the same puncture: the coordinate decoder on P104 stays at 64 + exact, costs = decoder_cost([LINES[f] for f in FRAME0], [LINES[f] for f in FRAME0], live104) + check('H.even-pairs', exact and sum(costs) == 64, 'coordinate (even, alpha = beta) decoder on the same P104 costs 64') + # H4: an inadmissible frame admits no frame-pair decoder (and the census is not vacuous) + bad_frames = [F for F in F1s if not frame_pair_solutions(FRAME0, list(F))] + check('H.inadmissible', len(bad_frames) == 364 and hist[0] == 364, '364 frames of the two other relative types have no solution') + # H5: a swapped partner assignment is not dual + swapped = list(pairs) + (a0, b0), (a1, b1) = swapped[0], swapped[1] + swapped[0], swapped[1] = (a0, b1), (a1, b0) + try: + r2, c2 = build_pairs(swapped) + exact, _ = decoder_cost(r2, c2, live104) + except AssertionError: + exact = False + check('H.swapped-partners', not exact, 'swapping two column partners breaks duality or the odd pairing') + # H6: a 25-line puncture can push a support to a 7-dim span (the threshold is sharp) + alpha = FRAME0[0] + C = support_mask(LINES[alpha]) + best = min(((VMASK[x] | VMASK[y]) & C, x, y) for x in LAMBDAS for y in LAMBDAS if x < y + and popcount((VMASK[x] | VMASK[y]) & C) == 25) + killed = [i for i in range(NL) if best[0] >> i & 1] + rest = [i for i in range(NL) if C >> i & 1 and i not in killed] + check('H.pi7-sharp', len(killed) == 25 and span_dim(rest) == 7, + 'puncturing a 25-line codim-2 violator set leaves a root support with a 7-dim label span') + + +def main(): + parser = argparse.ArgumentParser(description=__doc__.split('\n')[0]) + parser.add_argument('--repo', type=Path, default=HERE.parent.parent, help='repository root (for pricing inputs)') + parser.add_argument('--out', type=Path, help='optional JSON certificate output (must not exist)') + args = parser.parse_args() + if not __debug__: + sys.exit('assertions must be enabled') + if args.out and args.out.exists(): + sys.exit('output exists: %s' % args.out) + section_a() + rows, weights = section_b() + orbit_size = section_c(weights) + F1s, example, hist, types = section_d() + chain = section_e(F1s, example) + hits = section_f() + prices = section_g(args.repo.resolve()) + section_h(example, F1s, hist) + status = 'PASS_COMPLEX_FRAME_PAIR_DECODERS' if not FAILS else 'FAIL' + cert = dict(status=status, failures=FAILS, + census={'%s(%d)' % (EXPECTED_TYPES[f][0], f): v for f, v in sorted(rows.items(), reverse=True)}, + d7_orbit=orbit_size, frame_pairs=dict(frames=len(F1s), admissible=hist[8], inadmissible=hist[0], + solutions_per_admissible_frame=8), + chain={str(p): v for p, v in chain.items()}, pr717_hits=hits, pricing=prices, log=LOG, + scope='Exact 8-term decoders (D = R A, T = R A^-T) in the PR717 B14 label-pairing model, punctures of at ' + 'most 24 of the 120 E8 lines. No word is built; pricing uses PR717 P1 knobs on the selected U8 ' + 'profile and is a favorable budget, not a kappa claim.') + if args.out: + args.out.write_text(json.dumps(cert, indent=1, default=str) + '\n') + print('%s: types 8; D7 orbit %d; frames %d (admissible %d); chain p=0..24; P104 7/13; bit cap kappa %s; controls 6' + % (status, orbit_size, len(F1s), hist[8], prices['bit_cap']['kappa_decimal'])) + sys.exit(1 if FAILS else 0) + + +if __name__ == '__main__': + main() diff --git a/research/frame-pair-enumeration-fast-seed93/verify.py b/research/frame-pair-enumeration-fast-seed93/verify.py index 3a778d993c..eefbe5b487 100644 --- a/research/frame-pair-enumeration-fast-seed93/verify.py +++ b/research/frame-pair-enumeration-fast-seed93/verify.py @@ -17,7 +17,7 @@ HERE = Path(__file__).resolve().parent ROOT = HERE.parents[1] -REL = 'research/complex-frame-pair-decoders/verify.py' +REL = 'research/frame-pair-enumeration-fast-seed93/baseline.py' BASE = 'abdc6a7002abdbcd9e21bfc5e1a795784deacfdf' spec = importlib.util.spec_from_file_location('mask_enumerator', HERE/'fast.py') fast = importlib.util.module_from_spec(spec); spec.loader.exec_module(fast) diff --git a/research/frame-pair-enumeration-production/NOTICE.md b/research/frame-pair-enumeration-production/NOTICE.md new file mode 100644 index 0000000000..a62b02908b --- /dev/null +++ b/research/frame-pair-enumeration-production/NOTICE.md @@ -0,0 +1,16 @@ +# Notice + +Production wiring of the exact eight-bit neighborhood frame-pair enumerator into +`research/complex-frame-pair-decoders/verify.py`. + +## Credit + +- themilkman216 / [CrocSwap/integer-mult-bounds#968](https://github.com/CrocSwap/integer-mult-bounds/pull/968) + (`research/complex-frame-pair-decoders/`): retained exact frame-pair census, + attaining chain and controls. +- woklerx / [CrocSwap/integer-mult-bounds#1099](https://github.com/CrocSwap/integer-mult-bounds/pull/1099) + (`research/frame-pair-enumeration-fast-seed93/`): proved opt-in neighborhood + enumerator with identical ordered streams. + +Prepared by Wentao Li (VictorLiwentao, @Is__Victor, wentaol4@illinois.edu) +with substantial AI assistance. Apache-2.0. diff --git a/research/frame-pair-enumeration-production/README.md b/research/frame-pair-enumeration-production/README.md new file mode 100644 index 0000000000..3f7d5c5cd7 --- /dev/null +++ b/research/frame-pair-enumeration-production/README.md @@ -0,0 +1,100 @@ +# Production neighborhood enumeration for PR968 frame-pair decoders + +**Tooling improvement; no new kappa.** At base +`0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2`, +`research/complex-frame-pair-decoders/verify.py:frame_pair_solutions` still +rebuilt partner lists with nested list comprehensions on every mask. woklerx’s +opt-in adapter `research/frame-pair-enumeration-fast-seed93/` (incorporated +[#1099](https://github.com/CrocSwap/integer-mult-bounds/pull/1099)) already +proved exact eight-bit neighborhood masks with identical ordered solution +streams. This package wires that equivalent rewrite into the **production** +PR968 verifier. + +Dependent VERIFY packages that previously live-pinned the production path +demote that pin to provenance. `selected-p104-port-adapter`, +`p104-nullpair-compensated-shear-seed318bd5`, and `p104-term-shear-seed8be7` +retarget their live pairwise model pins to this package’s +[`baseline.py`](baseline.py). Legacy WT-hash loaders +`p104-asynchronous-carrier-bound`, `root-pair-first-drop-seed48`, +`complex-decoder-field-extension-seed44`, and +`e8-factor-linear-overcomplete47` likewise load the vendored baseline instead +of the rewritten production `verify.py`. + +## Reproduce + +Python **3.12**, standard library only, from the repository root: + +```sh +python3.12 -I -B research/frame-pair-enumeration-production/verify.py +python3.12 -I -O -B research/frame-pair-enumeration-production/verify.py +python3.12 -B scripts/research_package.py --package research/frame-pair-enumeration-production +taskset -c 0 python3.12 -I -B research/frame-pair-enumeration-production/benchmark.py --rounds 5 --write-result +``` + +Expected: + +```text +PASS_FRAME_PAIR_ENUMERATION_PRODUCTION frames=1260 decoders=7168 term_ranks=57344 corruption=… certs=0 no_new_kappa +PASS_REGISTERED_RESEARCH_PACKAGE research/frame-pair-enumeration-production outcome=completed +PASS_IDENTICAL_FRAME_PAIR_ENUMERATION_PRODUCTION_RECEIPTS +``` + +Default verify is read-only. Scope is PR968 sections D/E/H (complete frame-pair +census, attaining chain, controls). Section G binds the selected kappa record +and is outside this tooling change. Temp-copy omission foil rejects via +assertion failure or receipt divergence. Package gates under `-O` still compile +loaded checkers with `optimize=0`. Full `make verify`, selected cold replay, +Lean, and multiplication-theorem obligations were not rerun. + +## Result + +On Linux / CPython 3.12.3 with `taskset -c 0`, five alternating fresh-process +pairs gave median complete D/E/H wall time **13.642 → 4.421 s (3.09×)**. +Details are in [`RESULT.json`](RESULT.json). Timing is host-descriptive and is +not a correctness gate. Every ordered solution stream and term-rank receipt +matches between baseline and production (7,168 decoders; 57,344 term ranks). + +## Why the neighborhood masks are equivalent + +For a fixed selected subset S of the first frame, a second-frame member g is a +permitted partner of f in S exactly when its nonzero neighbors inside S are the +singleton {f}. Encoding those neighbors as an eight-bit integer turns this into +`hit != 0 and hit & (hit - 1) == 0`. Iterating g in frame order appends the same +partner lists in the same order. The reverse-neighborhood masks handle the +complementary half. Injectivity guards are retained. See +`research/frame-pair-enumeration-fast-seed93/PROOF.md`. + +## Overlap and credit + +Closest priors: + +- `research/frame-pair-enumeration-fast-seed93/` / [#1099](https://github.com/CrocSwap/integer-mult-bounds/pull/1099) + — opt-in neighborhood adapter; this is the production wiring. +- [CrocSwap/integer-mult-bounds#756](https://github.com/CrocSwap/integer-mult-bounds/pull/756) + — identical-receipt tooling quality bar. +- Open leave-alone tooling on other objects (#1922 joint frames, #2039/#2054 + shared-point, #2100 ternary, #2117 DisjointTensor, #2150 mixed-point, + #2194/#2210/#2231/#2239/#2257/#2263/#2276/#2320/#2329/#2348/#2357 production + rewrites; #1076 quadratic-affine) was not reopened. Fresh overlap refresh + found no competing production rewrite of `frame_pair_solutions`. + +Credit themilkman216 and woklerx. Prepared by Wentao Li +([VictorLiwentao](https://github.com/VictorLiwentao), +[@Is__Victor](https://x.com/Is__Victor)) with substantial AI assistance, under +Apache-2.0. + +## Open next questions + +1. **Question:** Should section G be repinned to the current selected kappa + record in a separate package? + **Why it matters:** At this base the full verifier fails only + `G.selected-record`. + **First step:** Dedicated selected-record refresh for section G only. + **Blocked by:** Outside this identical-receipt tooling stop rule. + +2. **Question:** Should packages that only cite the frame-pair floor in prose + drop their provenance pin entirely? + **Why it matters:** Several packages keep historical verify.py provenance + after demotion. + **First step:** Maintainer preference on provenance retention. + **Blocked by:** Attribution/navigation policy. diff --git a/research/frame-pair-enumeration-production/RESULT.json b/research/frame-pair-enumeration-production/RESULT.json new file mode 100644 index 0000000000..9218858d64 --- /dev/null +++ b/research/frame-pair-enumeration-production/RESULT.json @@ -0,0 +1,81 @@ +{ + "ai_assistance": "Substantial AI assistance for orientation, overlap search, profiling, production wiring, packaging, benchmarking and writing. Not independent human peer review.", + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "baseline_median_seconds": 13.64248858499991, + "implementation_sha256": { + "baseline.py": "bdf7ee497dc04dfc634ee5b7848f6a2b39b0169668fb1a60a9715111dbd15395", + "benchmark.py": "244908b58a7afda2bff638aeabf86370bd2cf3e65b08d0b784c97deffd56e9c3", + "production": "f7a9a39659c179853af3220f83a11b4c3cf52c8f3bccc0911a5629add10fbaff" + }, + "median_ratio": 3.085963956281897, + "no_new_kappa": true, + "platform": "Linux-6.12.94+-x86_64-with-glibc2.39", + "predecessor": "research/frame-pair-enumeration-fast-seed93/", + "production_median_seconds": 4.420819159999837, + "python": "3.12.3 (main, Aug 31 2026, 10:18:26) [GCC 13.3.0]", + "rounds": 5, + "samples": [ + [ + { + "engine": "baseline", + "receipt_sha256": "1be47c90a73a6d89ff1b9b6841b82cd26027212e230f024d96d03d789e0a4eee", + "seconds": 13.64248858499991 + }, + { + "engine": "production", + "receipt_sha256": "1be47c90a73a6d89ff1b9b6841b82cd26027212e230f024d96d03d789e0a4eee", + "seconds": 4.401531963999787 + } + ], + [ + { + "engine": "production", + "receipt_sha256": "1be47c90a73a6d89ff1b9b6841b82cd26027212e230f024d96d03d789e0a4eee", + "seconds": 4.420819159999837 + }, + { + "engine": "baseline", + "receipt_sha256": "1be47c90a73a6d89ff1b9b6841b82cd26027212e230f024d96d03d789e0a4eee", + "seconds": 13.316684685999917 + } + ], + [ + { + "engine": "baseline", + "receipt_sha256": "1be47c90a73a6d89ff1b9b6841b82cd26027212e230f024d96d03d789e0a4eee", + "seconds": 14.835714818000042 + }, + { + "engine": "production", + "receipt_sha256": "1be47c90a73a6d89ff1b9b6841b82cd26027212e230f024d96d03d789e0a4eee", + "seconds": 4.358019388000002 + } + ], + [ + { + "engine": "production", + "receipt_sha256": "1be47c90a73a6d89ff1b9b6841b82cd26027212e230f024d96d03d789e0a4eee", + "seconds": 4.887755986000002 + }, + { + "engine": "baseline", + "receipt_sha256": "1be47c90a73a6d89ff1b9b6841b82cd26027212e230f024d96d03d789e0a4eee", + "seconds": 13.085234235999906 + } + ], + [ + { + "engine": "baseline", + "receipt_sha256": "1be47c90a73a6d89ff1b9b6841b82cd26027212e230f024d96d03d789e0a4eee", + "seconds": 14.937267882000015 + }, + { + "engine": "production", + "receipt_sha256": "1be47c90a73a6d89ff1b9b6841b82cd26027212e230f024d96d03d789e0a4eee", + "seconds": 5.088425197000106 + } + ] + ], + "scope": "PR968 sections D/E/H (complete frame-pair census, attaining chain, controls)", + "status": "PASS_IDENTICAL_FRAME_PAIR_ENUMERATION_PRODUCTION_RECEIPTS" +} diff --git a/research/frame-pair-enumeration-production/SOURCES.json b/research/frame-pair-enumeration-production/SOURCES.json new file mode 100644 index 0000000000..80b67c0e33 --- /dev/null +++ b/research/frame-pair-enumeration-production/SOURCES.json @@ -0,0 +1,44 @@ +{ + "schema_version": 1, + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "files": [ + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "e8870e5917057d59b730eb14721a778639eca050", + "sha256": "d46eb6d5b3e279428753d770653663fbdf1063e55c255ea073d768f344927ef7" + }, + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "research/complex-frame-pair-decoders/verify.py", + "usage": "provenance", + "git_blob": "57dd8993e8ac016e8a92a9a885392b58014137bb", + "sha256": "bdf7ee497dc04dfc634ee5b7848f6a2b39b0169668fb1a60a9715111dbd15395", + "note": "Pairwise-era digest retained as provenance after research/frame-pair-enumeration-production/; working verifier ships eight-bit neighborhood enumeration." + }, + { + "path": "research/frame-pair-enumeration-fast-seed93/fast.py", + "usage": "input", + "git_blob": "cba829092c6a15b7e169b5e63f7e9c7918a5a29b", + "sha256": "1acdcf631d257b9e2b05bf981d565a004112cb7e0262cf6f893a1e0a90a0ec43" + }, + { + "path": "research/frame-pair-enumeration-fast-seed93/PROOF.md", + "usage": "provenance", + "git_blob": "488320e96d76c4ff56069a9f55c51674abcbc734", + "sha256": "584bf7d607cfffe6a85a11184722319dba2da9a82524554e9f2e45ee41dbf7da" + }, + { + "path": "research/frame-pair-enumeration-fast-seed93/README.md", + "usage": "provenance", + "git_blob": "39c72a333335253b4bbf718e5178109d5d7150ba", + "sha256": "5c2063312676549e06bd86f0e85fa72423336cc2c48f37d8c9cc087aa996ddb2", + "note": "Pre-production-wiring README bytes at base_commit; working tree adds a one-line production status note." + } + ] +} diff --git a/research/frame-pair-enumeration-production/TASK.json b/research/frame-pair-enumeration-production/TASK.json new file mode 100644 index 0000000000..63ef9fda11 --- /dev/null +++ b/research/frame-pair-enumeration-production/TASK.json @@ -0,0 +1,70 @@ +{ + "schema_version": 1, + "task_id": "replay-runtime", + "priority_revision": 4, + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "chooser_seed": "3e904229c9b5e68282f0ec716032bbd4", + "original_card": { + "id": "replay-runtime", + "question": "Can one measured replay bottleneck be sped up without dropping coverage?", + "starting_points": [ + "scripts/run_isolated_tests.py", + "scripts/verify_replay_coverage.py", + "certificates/selected-result.json" + ], + "methods": [ + "Profile one isolated replay and optimize the measured bottleneck.", + "Design source-bound reuse with explicit dependency invalidation and negative controls." + ], + "acceptance_gate": "Report before/after wall time on the same fixture, retained checks and invalidation behavior.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read the selected reproduction command and choose a single replay stage for profiling.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Measure one unchanged fixture, preserve check coverage, and test one optimization with invalidation controls.", + "bottleneck_link": "Faster trustworthy replays increase review throughput and let mechanism candidates be checked sooner.", + "allowed_variations": [ + "Profile one stage or design one source-bound cache boundary." + ], + "scope_change_triggers": [ + "Skipping coverage or comparing different fixtures to claim speedup." + ], + "overlap_terms": [ + "replay runtime", + "cache invalidation", + "isolated tests" + ] + }, + "scope_status": "refined", + "actual_scope": "Can the production research/complex-frame-pair-decoders/verify.py:frame_pair_solutions adopt the proved exact eight-bit neighborhood enumerator from research/frame-pair-enumeration-fast-seed93/ so that the shipped PR968 D/E/H frame-pair census is faster while every ordered solution stream and term-rank receipt stays identical?", + "scope_change_reason": "The catalogue card asks for one measured replay bottleneck with before/after wall time and retained checks. Expertise override selected verifier-engineering after profiling leave-alone production rewrites and remaining proved opt-in adapters. Leave-alone objects (joint frames, shared-point, mixed-point, ternary, parity-side, R420 rref/geometry/mutants, frameopt.close, leech_minor, verify_factor, sparse-fusion, joint-dual replay, quadratic-affine for #1076, data_corners, clifford_exact, bit-hosted-digest, emitted-local hpe_audit_local, e8-bit-r420 MANIFEST-only edits) were skipped. A cyclic-zero production probe on this host measured only 1.26x and was deferred. woklerx's merged #1099 opt-in adapter already proved ~4.57x kernel / ~2.97x D/E/H with identical receipts; production frame_pair_solutions still rebuilt partner lists by nested list comprehensions. This session wires that equivalent rewrite into the shipped PR968 verifier, vendors pairwise baselines, demotes dependent VERIFY live pins to provenance, and retargets selected-p104-port-adapter's E8 model pin to the vendored baseline.", + "bottleneck_link": "Side result on review throughput: the PR968 frame-pair census is a retained exact historical check used by later P104/P112 packages. A faster identical receipt does not change kappa or the binding complex supplier.", + "budget_minutes": 60, + "stop_rule": "Ship an equivalence-preserving production frame_pair_solutions neighborhood change with frozen baseline, identical D/E/H receipts, corruption controls, pin discipline, registered replay and a measured before/after median >=~1.5x with non-trivial absolute seconds. Do not invent kappa or reopen leave-alone objects.", + "outcome": "completed", + "evidence": "PASS_FRAME_PAIR_ENUMERATION_PRODUCTION via research/frame-pair-enumeration-production/verify.py (also under -O); PASS_REGISTERED_RESEARCH_PACKAGE; PASS_IDENTICAL_FRAME_PAIR_ENUMERATION_PRODUCTION_RECEIPTS via taskset -c 0 benchmark.py --rounds 5 (median 13.642\u21924.421 s, 3.086\u00d7); dependent VERIFY packages demote the live verify.py pin to provenance; selected-p104-port-adapter, p104-nullpair-compensated-shear-seed318bd5, and p104-term-shear-seed8be7 retarget live pairwise model pins to baseline.py; legacy loaders p104-asynchronous-carrier-bound, root-pair-first-drop-seed48, complex-decoder-field-extension-seed44, and e8-factor-linear-overcomplete47 load baseline.py; frame-pair-enumeration-fast-seed93 vendors baseline.py.", + "author": "Wentao Li", + "github": "VictorLiwentao", + "email": "wentaol4@illinois.edu", + "ai_assistance": "Substantial AI assistance for orientation, overlap search, profiling, production wiring, pin demotions, packaging, benchmarking and writing. Not independent human peer review.", + "open_questions": [ + { + "question": "Should section G of complex-frame-pair-decoders/verify.py be repinned to the current selected kappa record in a separate package?", + "why_it_matters": "At this base the full verifier fails only G.selected-record due to selected kappa drift; D/E/H remain the tooling scope.", + "first_step": "Dedicated selected-record refresh for section G only.", + "blocked_by": "Out of this session's identical-receipt tooling stop rule." + }, + { + "question": "Should other packages that only cite the frame-pair floor in prose drop their provenance pin entirely?", + "why_it_matters": "Several packages keep historical verify.py provenance after demotion.", + "first_step": "Maintainer preference on provenance retention versus deletion.", + "blocked_by": "Attribution/navigation policy." + } + ] +} diff --git a/research/frame-pair-enumeration-production/VERIFY.json b/research/frame-pair-enumeration-production/VERIFY.json new file mode 100644 index 0000000000..36ea4e03ae --- /dev/null +++ b/research/frame-pair-enumeration-production/VERIFY.json @@ -0,0 +1,23 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/frame-pair-enumeration-fast-seed93/fast.py", + "research/frame-pair-enumeration-production/baseline.py", + "research/complex-frame-pair-decoders/verify.py" + ], + "commands": [ + { + "argv": ["{python}", "-I", "-B", "{package}/verify.py"], + "timeout_seconds": 600, + "checks": "Exact baseline copy of the base-commit complex-frame-pair-decoders/verify.py; identical D/E/H receipts and pointwise frame_pair_solutions on all 1260 frames; temp-copy omission foil rejection; opt-in fast.py agreement; duplicate JSON-key check; read-only default." + }, + { + "argv": ["{python}", "-I", "-O", "-B", "{package}/verify.py"], + "timeout_seconds": 600, + "checks": "Same package require() gates under -O; loaded checkers still compile with optimize=0." + } + ] +} diff --git a/research/frame-pair-enumeration-production/baseline.py b/research/frame-pair-enumeration-production/baseline.py new file mode 100644 index 0000000000..57dd8993e8 --- /dev/null +++ b/research/frame-pair-enumeration-production/baseline.py @@ -0,0 +1,740 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Frame-pair decoders and the exact 8-term copy-cost floor on punctured complex E8 units. + +Standard library only. Exact integer, F2 and rational arithmetic throughout. + +Model (PR717 B14, D2/D3 scope): the 120 E8 root lines; a puncture P removes lines; an exact +8-term decoder is D = R A, T = R B with A B^T = 2 I, so that D T^T = 2G on the live lines +(G the integer inner products). Term k costs the F2 rank of the label pairing between its row +support (live lines not orthogonal to a_k) and column support (live lines not orthogonal to b_k). +The label pairing of two lines is ( + 1) mod 2, which this script uses directly; it +never constructs PR717's simple-root coordinates. + +Sections (each prints PASS/FAIL lines): + A model facts: 120 lines, nondegenerate rank-9 pairing, distinct pairing rows + B violator census for the eight W(E8) hyperplane-flat types (all 511 hyperplanes and all + 130,305 codimension-2 pairs of F2^9 functionals) + C the D7 orbit: 1080 directions, unique 14-line violator sets, pairwise unions >= 21, no + coincidence with a root functional + D frame-pair census: all 1260 frames disjoint from the coordinate frame, all (S, T) splits; + every solution is built and checked exactly + E attaining chain: explicit exact decoders for every puncture size p = 0..24 + F replay of the three vendored PR717 D3 hits and their root-pair structure + G favorable-budget pricing on the selected (U8/T37) profile with the pinned moment and outer + engines, and the PR589 bit-supplier cap + H negative controls +""" +import argparse +import hashlib +import importlib.util +import itertools +import json +import math +import sys +from collections import Counter +from fractions import Fraction as Q +from pathlib import Path + +HERE = Path(__file__).resolve().parent +FAILS = [] +LOG = [] + + +def check(tag, cond, info=''): + line = ('PASS ' if cond else 'FAIL ') + tag + (' | ' + info if info else '') + print(line, flush=True) + LOG.append(line) + if not cond: + FAILS.append(tag) + + +# ---------------------------------------------------------------- A. E8 lines and pairing +def e8_roots(): + """240 roots in doubled coordinates; same enumeration order as PR717's e8model (adapter only).""" + roots = [] + for i, j in itertools.combinations(range(8), 2): + for si in (1, -1): + for sj in (1, -1): + v = [0] * 8 + v[i], v[j] = 2 * si, 2 * sj + roots.append(tuple(v)) + for s in itertools.product((1, -1), repeat=8): + if s.count(-1) % 2 == 0: + roots.append(tuple(s)) + return roots + + +def dot(x, y): + return sum(a * b for a, b in zip(x, y)) + + +def ip(x, y): + """True inner product of doubled-coordinate vectors.""" + d = dot(x, y) + assert d % 4 == 0 + return d // 4 + + +def neg(v): + return tuple(-a for a in v) + + +ROOTS = e8_roots() +LINES = [] +_seen = set() +for r in ROOTS: + key = r if r > neg(r) else neg(r) + if key not in _seen: + _seen.add(key) + LINES.append(r) +NL = len(LINES) +IP = [[ip(LINES[i], LINES[j]) for j in range(NL)] for i in range(NL)] +# Label pairing as a 120-bit row mask: bit j of NROW[i] is ( + 1) mod 2. +NROW = [sum(((IP[i][j] + 1) & 1) << j for j in range(NL)) for i in range(NL)] +ALL = (1 << NL) - 1 +FRAME0 = [] +for a in range(4): + for s in (1, -1): + v = [0] * 8 + v[2 * a], v[2 * a + 1] = 2, 2 * s + FRAME0.append(LINES.index(tuple(v))) +P112 = [i for i in range(NL) if i not in FRAME0] + + +def popcount(x): + return bin(x).count('1') + + +def f2_rank(rows): + basis = {} + rank = 0 + for v in rows: + while v: + h = v.bit_length() - 1 + if h in basis: + v ^= basis[h] + else: + basis[h] = v + rank += 1 + break + return rank + + +def mask(idx): + m = 0 + for i in idx: + m |= 1 << i + return m + + +def pair_rank(rows, cols): + """F2 rank of the label pairing between the lines in `rows` and the lines in `cols`.""" + cm = mask(cols) + return f2_rank([NROW[i] & cm for i in rows]) + + +def span_dim(idx): + return f2_rank([NROW[i] for i in idx]) + + +def section_a(): + check('A.lines', NL == 120 and len(ROOTS) == 240, '120 lines from 240 roots') + check('A.pairing-values', all(IP[i][i] == 2 for i in range(NL)) and + {IP[i][j] for i in range(NL) for j in range(NL) if i != j} == {-1, 0, 1}, + 'line inner products are 2 on the diagonal and 0/+-1 off it') + check('A.pairing-rank-9', f2_rank(NROW) == 9, 'the 120x120 label pairing has F2 rank 9 (nondegenerate on the 9-dim label span)') + check('A.distinct-rows', len(set(NROW)) == 120, 'distinct lines have distinct pairing rows (distinct label functionals)') + check('A.frame0', len(FRAME0) == 8 and all(IP[a][b] == 0 for a in FRAME0 for b in FRAME0 if a != b), + 'coordinate frame e_{2a} +- e_{2a+1}: eight mutually orthogonal lines; P112 has %d lines' % len(P112)) + + +# Dual coordinates: phi_i = (pairing with nine basis lines). An F2-linear isomorphism of the label span, +# so the 511 nonzero functionals lambda . phi_i are exactly the 511 hyperplanes of the label space. +def dual_coordinates(): + basis = [] + for i in range(NL): + if f2_rank([NROW[b] for b in basis] + [NROW[i]]) == len(basis) + 1: + basis.append(i) + if len(basis) == 9: + break + phi = [sum(((NROW[i] >> b) & 1) << k for k, b in enumerate(basis)) for i in range(NL)] + return basis, phi + + +BASIS9, PHI = dual_coordinates() +LAMBDAS = list(range(1, 512)) +VMASK = {lam: mask(i for i in range(NL) if popcount(lam & PHI[i]) & 1) for lam in LAMBDAS} +ROOT_FUNCTIONAL = {} +for _i in range(NL): + # the functional of line i: lambda with lambda . phi_j = pairing(i, j) for all j + _cands = [lam for lam in LAMBDAS if VMASK[lam] == NROW[_i]] + assert len(_cands) == 1 + ROOT_FUNCTIONAL[_i] = _cands[0] + + +# ---------------------------------------------------------------- B. violator census +def solve_rational(M, rhs): + """Solve M x = rhs exactly (M square, invertible) with Fractions.""" + n = len(M) + A = [[Q(x) for x in row] + [Q(b)] for row, b in zip(M, rhs)] + for c in range(n): + p = next(r for r in range(c, n) if A[r][c] != 0) + A[c], A[p] = A[p], A[c] + for r in range(n): + if r != c and A[r][c] != 0: + f = A[r][c] / A[c][c] + A[r] = [x - f * y for x, y in zip(A[r], A[c])] + return [A[i][n] / A[i][i] for i in range(n)] + + +SIMPLE = [(1, -1, -1, -1, -1, -1, -1, 1), (2, 2, 0, 0, 0, 0, 0, 0), (-2, 2, 0, 0, 0, 0, 0, 0)] + \ + [tuple(-2 if t == k else 2 if t == k + 1 else 0 for t in range(8)) for k in range(1, 6)] + + +def fundamental_weights(): + """omega_i with = delta_ij, as integer doubled-coordinate directions.""" + out = [] + for i in range(8): + # unknown x (true coordinates): sum_t x_t * alpha_j[t]/2 = delta_ij + M = [[Q(a, 2) for a in alpha] for alpha in SIMPLE] + x = solve_rational(M, [1 if j == i else 0 for j in range(8)]) + den = 1 + for v in x: + den = den * v.denominator // math.gcd(den, v.denominator) + vec = tuple(int(v * den) for v in x) + out.append(vec) + return out + + +def support_mask(a): + return mask(i for i in range(NL) if dot(a, LINES[i]) != 0) + + +def census_type(a): + C = support_mask(a) + sizes = sorted(popcount(VMASK[lam] & C) for lam in LAMBDAS) + vm = [VMASK[lam] & C for lam in LAMBDAS] + pi7 = min(popcount(vm[x] | vm[y]) for x in range(511) for y in range(x + 1, 511)) + span = f2_rank([NROW[i] for i in range(NL) if C >> i & 1]) + return dict(support=popcount(C), flat_lines=NL - popcount(C), span=span, pi8=sizes[0], pi8_second=sizes[1], pi7=pi7) + + +EXPECTED_TYPES = { # flat lines -> (subsystem, |C|, pi8, second pi8, pi7) + 63: ('E7', 57, 1, 24, 25), 42: ('D7', 78, 14, 34, 42), 37: ('E6+A1', 83, 27, 28, 51), + 28: ('A7', 92, 28, 35, 56), 23: ('D5+A2', 97, 33, 41, 61), 22: ('A6+A1', 98, 35, 35, 62), + 16: ('A4+A3', 104, 40, 43, 68), 14: ('A4+A2+A1', 106, 43, 43, 70)} + + +def section_b(): + weights = fundamental_weights() + check('B.weights', all(sum(Q(dot(w, a), 4) == 0 for a in SIMPLE) == 7 for w in weights), + 'eight fundamental-weight directions, each orthogonal to seven simple roots') + rows = {} + for w in weights: + info = census_type(w) + rows[info['flat_lines']] = info + ok = set(rows) == set(EXPECTED_TYPES) and all( + (rows[f]['support'], rows[f]['pi8'], rows[f]['pi8_second'], rows[f]['pi7']) == EXPECTED_TYPES[f][1:] + and rows[f]['span'] == 9 for f in rows) + table = '; '.join('%s flat %d: |C|=%d pi8=%d (next %d) pi7=%d' % (EXPECTED_TYPES[f][0], f, rows[f]['support'], + rows[f]['pi8'], rows[f]['pi8_second'], rows[f]['pi7']) for f in sorted(rows, reverse=True)) + check('B.census', ok, table) + nonroot = min(rows[f]['pi8'] for f in rows if f != 63) + check('B.thresholds', nonroot == 14 and rows[63]['pi8_second'] == 24 and min(r['pi7'] for r in rows.values()) == 25, + 'only E7 (root) normals drop to an 8-dim span with one puncture (their own line); every other type needs >= 14; ' + 'a root normal by another hyperplane needs >= 24; any 7-dim span needs >= 25 punctures') + # the root type's unique one-line violator set is the line itself, through its own functional + alpha = next(i for i in range(NL) if LINES[i] == (2, 2, 0, 0, 0, 0, 0, 0)) + C = support_mask(LINES[alpha]) + check('B.root-self-line', VMASK[ROOT_FUNCTIONAL[alpha]] & C == 1 << alpha, + 'for a root normal alpha the 1-line violator set is {alpha}, via the functional of alpha itself') + allroots = True + for i in range(NL): + C = support_mask(LINES[i]) + sizes = sorted((popcount(VMASK[lam] & C), lam) for lam in LAMBDAS) + allroots &= sizes[0] == (1, ROOT_FUNCTIONAL[i]) and VMASK[ROOT_FUNCTIONAL[i]] & C == 1 << i and sizes[1][0] == 24 + check('B.root-all-120', allroots, 'checked directly for all 120 root normals: unique 1-line set {alpha}; every other hyperplane >= 24') + return rows, weights + + +# ---------------------------------------------------------------- C. D7 orbit +def canon(v): + g = 0 + for a in v: + g = math.gcd(g, abs(a)) + v = tuple(a // g for a in v) + first = next(a for a in v if a) + return v if first > 0 else neg(v) + + +def orbit(start): + seen = {canon(start)} + frontier = [canon(start)] + while frontier: + nxt = [] + for v in frontier: + for r in LINES: + d = dot(v, r) + u = tuple(4 * a - d * b for a, b in zip(v, r)) # 4 * reflection, integral + c = canon(u) + if c not in seen: + seen.add(c) + nxt.append(c) + frontier = nxt + return sorted(seen) + + +def section_c(weights): + d7 = next(w for w in weights if NL - popcount(support_mask(w)) == 42) + dirs = orbit(d7) + check('C.orbit', len(dirs) == 1080, 'W(E8) orbit of the D7 normal: %d directions' % len(dirs)) + v14 = {} + root_funcs = set(ROOT_FUNCTIONAL.values()) + coincide = 0 + inflat_all = True + rank_ok = True + for d in dirs: + C = support_mask(d) + sizes = sorted((popcount(VMASK[lam] & C), lam) for lam in LAMBDAS) + assert sizes[0][0] == 14 and sizes[1][0] >= 34 + lam = sizes[0][1] + v14[d] = VMASK[lam] & C + coincide += lam in root_funcs + flat = [i for i in range(NL) if not C >> i & 1] + inflat_all &= all(popcount(VMASK[lam] >> i & 1) for i in flat) + # removing any one flat line leaves a rank-7 set: a flat of rank <= 6 misses >= 2 of the 42 lines + # (not needed by the main argument; recorded as a cross-check of D7 rigidity) + if d == dirs[0]: + rank_ok = all(rank_q([LINES[j] for j in flat if j != i]) == 7 for i in flat) + sets = list(v14.values()) + check('C.unique-14', len(set(sets)) == 1080, 'each D7 direction has a unique 14-line violator set (next >= 34); 1080 distinct sets') + mn = min(popcount(a | b) for a, b in itertools.combinations(sets, 2)) + check('C.unions', mn == 21, 'any two distinct D7 violator sets have union >= %d > 15' % mn) + check('C.no-root-coincidence', coincide == 0, 'no D7 minimizing functional equals a root functional') + check('C.flat-lines-violate', inflat_all and rank_ok, 'all 42 flat lines violate the minimizing functional; flat minus any line has rank 7') + return len(dirs) + + +def rank_q(vectors): + rows = [[Q(x) for x in v] for v in vectors] + r = 0 + ncol = len(rows[0]) if rows else 0 + for c in range(ncol): + p = next((i for i in range(r, len(rows)) if rows[i][c] != 0), None) + if p is None: + continue + rows[r], rows[p] = rows[p], rows[r] + for i in range(len(rows)): + if i != r and rows[i][c] != 0: + f = rows[i][c] / rows[r][c] + rows[i] = [x - f * y for x, y in zip(rows[i], rows[r])] + r += 1 + return r + + +# ---------------------------------------------------------------- decoders +def decoder_cost(rowvecs, colvecs, live): + """Exactness of D T^T = 2G on `live` and the per-term costs.""" + live = list(live) + D = [[ip(LINES[i], a) for a in rowvecs] for i in live] + T = [[ip(LINES[i], b) for b in colvecs] for i in live] + exact = all(sum(x * y for x, y in zip(D[p], T[q])) == 2 * IP[live[p]][live[q]] + for p in range(len(live)) for q in range(len(live))) + costs = [] + for k in range(len(rowvecs)): + R = [live[p] for p in range(len(live)) if D[p][k]] + A = [live[p] for p in range(len(live)) if T[p][k]] + costs.append(pair_rank(R, A)) + return exact, costs + + +def frames_in(pool): + pool = list(pool) + orth = {i: mask(j for j in pool if j != i and IP[i][j] == 0) for i in pool} + out = [] + + def rec(clique, cand): + if len(clique) == 8: + out.append(tuple(clique)) + return + c = cand + while c: + j = c.bit_length() - 1 + c &= ~(1 << j) + rec(clique + [j], cand & orth[j] & ((1 << j) - 1)) + + for i in pool: + rec([i], orth[i] & ((1 << i) - 1)) + return sorted(tuple(sorted(f)) for f in out) + + +def frame_pair_solutions(F0, F1): + """All splits: row normals S (from F0) and T (from F1); every column partner is a cross-frame line with + odd inner product and orthogonal to all other row normals.""" + sols = [] + for smask in range(256): + S = [F0[j] for j in range(8) if smask >> j & 1] + need = 8 - len(S) + # g in F1 is usable as the partner of f in S iff N(g) cap S == {f} + part = {f: [g for g in F1 if [x for x in S if IP[g][x]] == [f]] for f in S} + if any(not part[f] for f in S): + continue + for choice in itertools.product(*[part[f] for f in S]): + if len(set(choice)) != len(S): + continue + Tset = [g for g in F1 if g not in choice] + if len(Tset) != need: + continue + rest = [f for f in F0 if f not in S] + part2 = {g: [f for f in rest if [x for x in Tset if IP[f][x]] == [g]] for g in Tset} + if any(not part2[g] for g in Tset): + continue + for choice2 in itertools.product(*[part2[g] for g in Tset]): + if len(set(choice2)) != len(Tset): + continue + pairs = list(zip(S, choice)) + list(zip(Tset, choice2)) + sols.append(pairs) + return sols + + +def pair_decoder(pairs, live): + """Root-pair decoder (a_k = alpha_k, b_k = 2 beta_k). Exactness on every live set is + equivalent to = 2 delta_kl, i.e. A^T B = 2I, hence A B^T = 2I and D T^T = R (A B^T) R^T = 2G.""" + dual = all((IP[a][b] in (1, -1)) if k == l else IP[a][b] == 0 + for k, (a, _) in enumerate(pairs) for l, (_, b) in enumerate(pairs)) + costs = [pair_rank([i for i in live if IP[a][i]], [i for i in live if IP[b][i]]) for a, b in pairs] + return dual, costs + + +def build_pairs(pairs): + rows, cols = [], [] + for a, b in pairs: + e = IP[a][b] + assert e in (1, -1) + rows.append(LINES[a]) + cols.append(tuple(2 * e * x for x in LINES[b])) + return rows, cols + + +def relative_type(F0, F1): + common = Counter(sum(1 for f in F0 if IP[g][f] and IP[h][f]) for g, h in itertools.combinations(F1, 2)) + return tuple(sorted(common.items())) + + +def section_d(): + F1s = frames_in(P112) + check('D.frames', len(F1s) == 1260, '%d frames inside P112 (disjoint from the coordinate frame)' % len(F1s)) + hist = Counter() + types = Counter() + built = 0 + allgood = True + example = None + for F1 in F1s: + sols = frame_pair_solutions(FRAME0, list(F1)) + hist[len(sols)] += 1 + types[(len(sols) > 0, relative_type(FRAME0, F1))] += 1 + live = [i for i in range(NL) if i not in FRAME0 and i not in F1] + for pairs in sols: + exact, costs = pair_decoder(pairs, live) + built += 1 + allgood &= exact and costs == [7] * 8 + if example is None: + example = dict(F1=list(F1), pairs=pairs) + check('D.census', hist == Counter({8: 896, 0: 364}), 'solutions per frame: %s' % dict(sorted(hist.items()))) + tdesc = {str(k): v for k, v in sorted(types.items(), key=lambda kv: -kv[1])} + check('D.types', len(types) == 3 and all(ok == (dict(t).get(4, 0) == 0) for ok, t in types), + 'relative position (common F0-neighbours of F1 pairs) -> admissible: %s' % tdesc) + check('D.exact-56', allgood and built == 7168, '%d frame-pair decoders built; every one satisfies A^T B = 2I and has eight cost-7 terms on its P104 (cst 56)' % built) + F1 = example['F1'] + live = [i for i in range(NL) if i not in FRAME0 and i not in F1] + rows, cols = build_pairs(example['pairs']) + exact, costs = decoder_cost(rows, cols, live) + check('D.full-exactness-crosscheck', exact and costs == [7] * 8, 'one decoder rechecked entrywise: D T^T = 2G on all 104 x 104 live pairs') + return F1s, example, hist, types + + +def section_e(F1s, example): + F1 = example['F1'] + pairs = example['pairs'] + # ordering of F1 lines: each F1 line is the self-line of exactly one term + f1order = [b if b in F1 else a for a, b in pairs] + chain = {} + extra = [i for i in range(NL) if i not in FRAME0 and i not in F1] + coord_rows = [LINES[f] for f in FRAME0] + for p in range(0, 25): + if p <= 8: + P = FRAME0[:p] + rows, cols = coord_rows, coord_rows + kind = 'coordinate frame, %d of its lines punctured' % p + else: + j = min(p - 8, 8) + P = FRAME0 + f1order[:j] + extra[:max(0, p - 16)] + rows, cols = build_pairs(pairs) + kind = 'frame pair, %d partner lines + %d extra lines punctured' % (j, max(0, p - 16)) + live = [i for i in range(NL) if i not in P] + exact, costs = decoder_cost(rows, cols, live) + bound = max(72 - p, 56) + chain[p] = dict(live=len(live), exact=exact, cost=sum(costs), lower_bound=bound, kind=kind, + ratio=str(Q(sum(costs), len(live))), punctured=sorted(P), live_rank=rank_q([LINES[i] for i in live])) + ok = all(c['exact'] and c['cost'] == c['lower_bound'] and c['live_rank'] == 8 and len(c['punctured']) == p + for p, c in chain.items()) + check('E.chain', ok, 'p=0..24: exact decoders with cst = max(72-p, 56) at every p (attaining the theorem)') + best = min(chain, key=lambda p: Q(chain[p]['cost'], chain[p]['live'])) + check('E.best-ratio', best == 16 and Q(chain[16]['cost'], chain[16]['live']) == Q(7, 13) and + Q(chain[8]['cost'], chain[8]['live']) == Q(4, 7), + 'minimum copy ratio along the chain is 56/104 = 7/13 at p = 16 (P112: 64/112 = 4/7)') + return chain + + +# ---------------------------------------------------------------- F. PR717 hit replay +def load_hit(path): + D, T = [], [] + for line in path.read_text().splitlines(): + s = line.strip() + if s.startswith('d:'): + D.append([int(x) for x in s[2:].split()]) + if s.startswith('t:'): + T.append([int(x) for x in s[2:].split()]) + return [list(c) for c in zip(*D)], [list(c) for c in zip(*T)] # live x n + + +def recover(live, col): + """Exact vector a with = col[p] for every live line; returns doubled coordinates or None.""" + idx = [] + for p, i in enumerate(live): + if rank_q([LINES[live[q]] for q in idx] + [LINES[i]]) == len(idx) + 1: + idx.append(p) + if len(idx) == 8: + break + M = [[Q(x, 4) for x in LINES[live[p]]] for p in idx] + a = solve_rational(M, [col[p] for p in idx]) + ok = all(sum(Q(x, 4) * y for x, y in zip(LINES[i], a)) == col[p] for p, i in enumerate(live)) + return a if ok else None + + +def as_line(a): + """Index of the root line parallel to a, or None.""" + for i, r in enumerate(LINES): + ratio = None + good = True + for x, y in zip(r, a): + if x == 0: + good &= y == 0 + else: + q = Q(y) / x + good &= ratio is None or q == ratio + ratio = q + if good and ratio: + return i + return None + + +def section_f(): + p112 = P112 + results = {} + vend = json.loads((HERE / 'SOURCES.json').read_text())['vendored'] + check('F.vendored-pins', all(sha(HERE / rel) == meta['sha256'] for rel, meta in vend.items()) and len(vend) == 3, + 'three PR717 decoder files match their SHA-256 pins (PR717 head %s)' % next(iter(vend.values()))['head'][:7]) + clique717 = [9, 15, 24, 46, 52, 66, 94, 104] # PR717 d3_punctures.py, P112 indexing + cases = [('P104_HIT_flip_3a.txt', [p112[q] for q in clique717]), ('P111_HIT_g0.txt', [p112[0]]), + ('P111_HIT_g111.txt', [p112[111]])] + for name, extra in cases: + punct = FRAME0 + extra + live = [i for i in range(NL) if i not in punct] + D, T = load_hit(HERE / 'inputs/pr717' / name) + recorded = [int(l.split()[3]) for l in (HERE / 'inputs/pr717' / name).read_text().splitlines() if l.startswith('term ')] + exact = all(sum(x * y for x, y in zip(D[p], T[q])) == 2 * IP[live[p]][live[q]] + for p in range(len(live)) for q in range(len(live))) + terms = [] + for k in range(len(D[0])): + a = recover(live, [row[k] for row in D]) + b = recover(live, [row[k] for row in T]) + R = [live[p] for p in range(len(live)) if D[p][k]] + A = [live[p] for p in range(len(live)) if T[p][k]] + la, lb = as_line(a), as_line(b) + terms.append(dict(cost=pair_rank(R, A), row_root=la, col_root=lb, + odd=(la is not None and lb is not None and IP[la][lb] % 2 != 0), + both_punctured=(la in punct and lb in punct))) + results[name] = dict(exact=exact, costs=[t['cost'] for t in terms], recorded_by_pr717=recorded, terms=terms) + check('F.%s.costs-match-pr717' % name, recorded == [t['cost'] for t in terms], + 'per-term pairing ranks from (+1) mod 2 equal the costs PR717 recorded with its own label model') + seven = [t for t in terms if t['cost'] == 7] + check('F.%s' % name, exact and all(t['row_root'] is not None and t['col_root'] is not None and t['odd'] and + t['both_punctured'] for t in seven) and + all(not (t['odd'] and t['both_punctured']) for t in terms if t['cost'] != 7), + 'exact; costs %s; every cost-7 term is an odd root pair with both lines punctured, and no other term is' + % sorted(Counter(t['cost'] for t in terms).items())) + # PR717's P104 clique is an admissible second frame + F1 = sorted(p112[q] for q in clique717) + sols = frame_pair_solutions(FRAME0, F1) + check('F.P104-clique-is-frame-pair', all(IP[a][b] == 0 for a in F1 for b in F1 if a != b) and len(sols) == 8, + "PR717's random clique is a frame of the admissible relative type with 8 frame-pair decoders") + return results + + +# ---------------------------------------------------------------- G. pricing +def sha(path): + return hashlib.sha256(path.read_bytes()).hexdigest() + + +def load_module(path, name): + spec = importlib.util.spec_from_file_location(name, path) + mod = importlib.util.module_from_spec(spec) + spec.loader.exec_module(mod) + return mod + + +def section_g(repo): + pins = json.loads((HERE / 'SOURCES.json').read_text())['pricing_inputs'] + for rel, h in pins.items(): + check('G.pin.' + rel.split('/')[-1], sha(repo / rel) == h, rel) + eng = repo / 'research/complex-k492-owner-repair/vendor/multicold/engines' + M = load_module(eng / 'moment.py', 'pinned_moment') + B2 = load_module(eng / 'base_two_moment.py', 'pinned_base_two_moment') + A = load_module(eng / 'outer.py', 'pinned_outer') + P = load_module(repo / 'research/complex-t21-owners/vendor/pr870/independent/price_profile_t16.py', 'pinned_t16') + bit = json.loads((repo / 'research/complex-t21-owners/vendor/pr870/inputs/PR589-EXPECTED.json').read_text()) + c = Q(bit['nine']['bit_lower']) + src = json.loads((HERE / 'SOURCES.json').read_text())['selected_record'] + sel = json.loads((repo / 'certificates/selected-result.json').read_text()) + check('G.selected-record', sel['certificate'] == src['certificate'] and sel['certificate_sha256'] == src['certificate_sha256'] + and sha(repo / sel['certificate']) == src['certificate_sha256'] and sel['kappa'] == src['kappa'], + 'pricing uses the selected record %s (%s)' % (sel['certificate'], sel['decimal'])) + asm = json.loads((repo / sel['certificate']).read_text()) + H0 = Counter({int(r): n for r, n in asm['complex_profile'].items()}) + m, cell = 73, (9 - 1) * 112 - 9 * 64 + mass = sum(r * n for r, n in H0.items()) + T = next(t for t in range(1, 1000) if m * 896 * t - mass == cell * t) + W0, D0, calls = 896 * T, cell * T, 9 * T + check('G.identity', m * W0 - mass == D0 and max(H0) == 48, + 'selected profile: %d replicas, 73*%d - mass = %d = %d*((9-1)*112 - 9*64)' % (T, W0, D0, T)) + + def scenario(ports, units): + """PR717 P1 knobs transported to the selected U8 profile: a cst unit lowers one centre cut climb 8 -> 7 in every call; + a port removes one modal source (1,1,1,5) and target (1,1,4,1,1) climb per call and nine idle + rank-48 children per replica.""" + H = Counter(H0) + H[8] -= units * calls + H[7] += units * calls + for _ in range(ports): + for x in (1, 1, 1, 5, 1, 1, 4, 1, 1): + H[x] -= calls + H[48] -= 9 * T + H = Counter({r: n for r, n in H.items() if n}) + W = W0 - T * 8 * ports + D = T * ((9 - 1) * (112 - ports) - 9 * (64 - units)) + assert all(n > 0 for n in H.values()) and m * W - sum(r * n for r, n in H.items()) == D + return H, W, D + + out = {} + for name, (ports, units) in [('selected', (0, 0)), ('P111_knobs', (1, 1)), ('P104_knobs', (8, 8))]: + H, W, D = scenario(ports, units) + native = Q(M.certify(H, m, W, False)['lower']) + conservative = Q(M.certify(H, m, W, True)['lower']) + checks = P.moment_checks(M, B2, H, m, W, native, D, False) + o = P.outer47(c, native, A) + out[name] = dict(W=W, deficit=D, complex_b=str(native), complex_b_decimal=P.decimal(native), + conservative_b_decimal=P.decimal(conservative), + b_change_percent=P.decimal((native / Q(asm['complex_lower']) - 1) * 100), + kappa=o['kappa'], kappa_decimal=o['kappa_decimal'], binding=o['binding'], + outer_controls_rejected=o['controls_rejected'], two_engines=len(checks) == 2) + cap = P.outer47(c, 2 * c, A) + out['bit_cap'] = dict(kappa=cap['kappa'], kappa_decimal=cap['kappa_decimal'], binding=cap['binding'], + gain_over_selected_percent=P.decimal((Q(cap['kappa']) / Q(sel['kappa']) - 1) * 100)) + check('G.gate', out['selected']['complex_b'] == str(Q(asm['complex_lower'])) and + Q(out['selected']['kappa']) == Q(sel['kappa']), + 'pinned engines on the selected profile reproduce b and kappa = %s exactly' % sel['decimal']) + check('G.P111', out['P111_knobs']['binding'] == 'complex', + 'P111 knobs: b %+.4f%%, kappa %s (complex-bound)' % (float(Q(out['P111_knobs']['b_change_percent'])), + out['P111_knobs']['kappa_decimal'])) + check('G.P104', out['P104_knobs']['binding'] == 'bit' and out['P104_knobs']['kappa'] == out['bit_cap']['kappa'], + 'P104 knobs: b %+.4f%% > bit c, kappa capped at %s' % (float(Q(out['P104_knobs']['b_change_percent'])), + out['P104_knobs']['kappa_decimal'])) + check('G.bit-cap', out['bit_cap']['binding'] == 'bit', + 'any complex-only change is capped by PR589 at kappa %s (%+.4f%%)' % ( + out['bit_cap']['kappa_decimal'], float(Q(out['bit_cap']['gain_over_selected_percent'])))) + headroom = Q(out['P104_knobs']['complex_b']) / c - 1 + out['P104_headroom_above_bit_percent'] = P.decimal(headroom * 100) + return out + + +# ---------------------------------------------------------------- H. negative controls +def section_h(example, F1s, hist): + F1 = example['F1'] + pairs = example['pairs'] + live104 = [i for i in range(NL) if i not in FRAME0 and i not in F1] + rows, cols = build_pairs(pairs) + # H1: perturb one column vector -> exactness lost + bad = list(cols) + bad[0] = tuple(x + y for x, y in zip(bad[0], LINES[FRAME0[0]])) + exact, _ = decoder_cost(rows, bad, live104) + check('H.mutated-decoder', not exact, 'adding a frame root to one column vector breaks D T^T = 2G') + # H2: restore one partner line -> that term costs 8 (cst 57 = 72 - 15) + restored = next(b if b in F1 else a for a, b in pairs) + live = live104 + [restored] + exact, costs = decoder_cost(rows, cols, live) + check('H.self-line-live', exact and sum(costs) == 57 and sorted(costs) == [7] * 7 + [8], + 'restoring one self-line raises exactly one term to 8: cst 57 at p = 15') + # H3: even pairing on the same puncture: the coordinate decoder on P104 stays at 64 + exact, costs = decoder_cost([LINES[f] for f in FRAME0], [LINES[f] for f in FRAME0], live104) + check('H.even-pairs', exact and sum(costs) == 64, 'coordinate (even, alpha = beta) decoder on the same P104 costs 64') + # H4: an inadmissible frame admits no frame-pair decoder (and the census is not vacuous) + bad_frames = [F for F in F1s if not frame_pair_solutions(FRAME0, list(F))] + check('H.inadmissible', len(bad_frames) == 364 and hist[0] == 364, '364 frames of the two other relative types have no solution') + # H5: a swapped partner assignment is not dual + swapped = list(pairs) + (a0, b0), (a1, b1) = swapped[0], swapped[1] + swapped[0], swapped[1] = (a0, b1), (a1, b0) + try: + r2, c2 = build_pairs(swapped) + exact, _ = decoder_cost(r2, c2, live104) + except AssertionError: + exact = False + check('H.swapped-partners', not exact, 'swapping two column partners breaks duality or the odd pairing') + # H6: a 25-line puncture can push a support to a 7-dim span (the threshold is sharp) + alpha = FRAME0[0] + C = support_mask(LINES[alpha]) + best = min(((VMASK[x] | VMASK[y]) & C, x, y) for x in LAMBDAS for y in LAMBDAS if x < y + and popcount((VMASK[x] | VMASK[y]) & C) == 25) + killed = [i for i in range(NL) if best[0] >> i & 1] + rest = [i for i in range(NL) if C >> i & 1 and i not in killed] + check('H.pi7-sharp', len(killed) == 25 and span_dim(rest) == 7, + 'puncturing a 25-line codim-2 violator set leaves a root support with a 7-dim label span') + + +def main(): + parser = argparse.ArgumentParser(description=__doc__.split('\n')[0]) + parser.add_argument('--repo', type=Path, default=HERE.parent.parent, help='repository root (for pricing inputs)') + parser.add_argument('--out', type=Path, help='optional JSON certificate output (must not exist)') + args = parser.parse_args() + if not __debug__: + sys.exit('assertions must be enabled') + if args.out and args.out.exists(): + sys.exit('output exists: %s' % args.out) + section_a() + rows, weights = section_b() + orbit_size = section_c(weights) + F1s, example, hist, types = section_d() + chain = section_e(F1s, example) + hits = section_f() + prices = section_g(args.repo.resolve()) + section_h(example, F1s, hist) + status = 'PASS_COMPLEX_FRAME_PAIR_DECODERS' if not FAILS else 'FAIL' + cert = dict(status=status, failures=FAILS, + census={'%s(%d)' % (EXPECTED_TYPES[f][0], f): v for f, v in sorted(rows.items(), reverse=True)}, + d7_orbit=orbit_size, frame_pairs=dict(frames=len(F1s), admissible=hist[8], inadmissible=hist[0], + solutions_per_admissible_frame=8), + chain={str(p): v for p, v in chain.items()}, pr717_hits=hits, pricing=prices, log=LOG, + scope='Exact 8-term decoders (D = R A, T = R A^-T) in the PR717 B14 label-pairing model, punctures of at ' + 'most 24 of the 120 E8 lines. No word is built; pricing uses PR717 P1 knobs on the selected U8 ' + 'profile and is a favorable budget, not a kappa claim.') + if args.out: + args.out.write_text(json.dumps(cert, indent=1, default=str) + '\n') + print('%s: types 8; D7 orbit %d; frames %d (admissible %d); chain p=0..24; P104 7/13; bit cap kappa %s; controls 6' + % (status, orbit_size, len(F1s), hist[8], prices['bit_cap']['kappa_decimal'])) + sys.exit(1 if FAILS else 0) + + +if __name__ == '__main__': + main() diff --git a/research/frame-pair-enumeration-production/benchmark.py b/research/frame-pair-enumeration-production/benchmark.py new file mode 100644 index 0000000000..61c565eac8 --- /dev/null +++ b/research/frame-pair-enumeration-production/benchmark.py @@ -0,0 +1,194 @@ +#!/usr/bin/env python3 +"""Alternating fresh-process before/after timings for production frame-pair enumeration. + +Timing is host-descriptive and is not a correctness gate. +""" +from __future__ import annotations + +import argparse +import contextlib +import hashlib +import io +import json +import os +from pathlib import Path +import platform +import statistics +import subprocess +import sys +import time +import types + +ROOT = Path(__file__).resolve().parents[2] +PACKAGE = Path(__file__).resolve().parent +BASELINE = PACKAGE / "baseline.py" +PRODUCTION = ROOT / "research/complex-frame-pair-decoders/verify.py" + + +def unique_object(pairs): + out = {} + for key, value in pairs: + if key in out: + raise SystemExit(f"duplicate JSON key: {key}") + out[key] = value + return out + + +WORKER = r""" +import contextlib, hashlib, io, json, sys, time, types +from pathlib import Path + +root = Path(sys.argv[1]) +engine = sys.argv[2] +path = root / ( + "research/frame-pair-enumeration-production/baseline.py" + if engine == "baseline" + else "research/complex-frame-pair-decoders/verify.py" +) + +def load(path): + module = types.ModuleType("frame_pair_bench") + module.__file__ = str(path) + exec(compile(path.read_bytes(), str(path), "exec", optimize=0), module.__dict__) + return module + +def digest(obj): + return hashlib.sha256( + json.dumps(json.loads(json.dumps(obj, allow_nan=False)), sort_keys=True, + separators=(",", ":"), allow_nan=False).encode() + ).hexdigest() + +m = load(path) +stream = [] +rank_records = [] +original = m.frame_pair_solutions +original_pair = m.pair_decoder + +def enumerate_pairs(a, b): + result = original(a, b) + stream.append([a, b, result]) + return result + +def pair_check(pairs, live): + answer = original_pair(pairs, live) + rank_records.append([pairs, live, answer]) + return answer + +m.frame_pair_solutions = enumerate_pairs +m.pair_decoder = pair_check +capture = io.StringIO() +t0 = time.perf_counter() +with contextlib.redirect_stdout(capture): + frames, example, hist, kinds = m.section_d() + chain = m.section_e(frames, example) + m.section_h(example, frames, hist) +elapsed = time.perf_counter() - t0 +if m.FAILS: + raise SystemExit("checks failed: " + str(m.FAILS)) +receipt = { + "frames": len(frames), + "enumerations": len(stream), + "decoder_rank_checks": len(rank_records), + "term_rank_checks": sum(len(record[2][1]) for record in rank_records), + "ordered_solution_stream_sha256": digest(stream), + "rank_stream_sha256": digest(rank_records), + "histogram": sorted(hist.items()), + "types": sorted((str(k), v) for k, v in kinds.items()), + "example": example, + "chain": chain, + "log": capture.getvalue().splitlines(), +} +print(json.dumps({"elapsed": elapsed, "receipt": receipt}, sort_keys=True)) +""" + + +def run_engine(engine: str) -> dict: + env = os.environ.copy() + env.pop("PYTHONOPTIMIZE", None) + env["PYTHONDONTWRITEBYTECODE"] = "1" + proc = subprocess.run( + [sys.executable, "-I", "-B", "-c", WORKER, str(ROOT), engine], + cwd=ROOT, + env=env, + capture_output=True, + text=True, + ) + if proc.returncode != 0: + raise SystemExit(f"engine={engine} failed\n{proc.stderr}\n{proc.stdout}") + return json.loads(proc.stdout.strip().splitlines()[-1], object_pairs_hook=unique_object) + + +def main(argv: list[str] | None = None) -> int: + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--rounds", type=int, default=5) + parser.add_argument("--write-result", action="store_true") + parser.add_argument("--output", type=Path, default=PACKAGE / "RESULT.json") + args = parser.parse_args(argv) + if args.rounds < 1: + raise SystemExit("--rounds must be >= 1") + + samples = [] + baseline_times = [] + production_times = [] + reference = None + for round_index in range(args.rounds): + order = ("baseline", "production") if round_index % 2 == 0 else ("production", "baseline") + pair = [] + for engine in order: + payload = run_engine(engine) + if reference is None: + reference = payload["receipt"] + elif payload["receipt"] != reference: + raise SystemExit(f"receipt mismatch round={round_index} engine={engine}") + pair.append({"engine": engine, "seconds": payload["elapsed"], + "receipt_sha256": hashlib.sha256( + json.dumps(payload["receipt"], sort_keys=True, separators=(",", ":")).encode() + ).hexdigest()}) + if engine == "baseline": + baseline_times.append(payload["elapsed"]) + else: + production_times.append(payload["elapsed"]) + print( + f"round={round_index} engine={engine} seconds={payload['elapsed']:.6f}", + flush=True, + ) + samples.append(pair) + + base_med = statistics.median(baseline_times) + prod_med = statistics.median(production_times) + result = { + "status": "PASS_IDENTICAL_FRAME_PAIR_ENUMERATION_PRODUCTION_RECEIPTS", + "ai_assistance": ( + "Substantial AI assistance for orientation, overlap search, profiling, " + "production wiring, packaging, benchmarking and writing. Not independent " + "human peer review." + ), + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "predecessor": "research/frame-pair-enumeration-fast-seed93/", + "python": sys.version, + "platform": platform.platform(), + "rounds": args.rounds, + "scope": "PR968 sections D/E/H (complete frame-pair census, attaining chain, controls)", + "baseline_median_seconds": base_med, + "production_median_seconds": prod_med, + "median_ratio": base_med / prod_med if prod_med else None, + "samples": samples, + "implementation_sha256": { + "baseline.py": hashlib.sha256(BASELINE.read_bytes()).hexdigest(), + "production": hashlib.sha256(PRODUCTION.read_bytes()).hexdigest(), + "benchmark.py": hashlib.sha256(Path(__file__).read_bytes()).hexdigest(), + }, + "no_new_kappa": True, + } + print(result["status"]) + print(f"median {base_med:.6f} -> {prod_med:.6f} ({result['median_ratio']:.3f}x)") + if args.write_result: + args.output.write_text(json.dumps(result, indent=2, sort_keys=True) + "\n", encoding="utf-8") + print(f"wrote {args.output}") + else: + print(json.dumps(result, indent=2, sort_keys=True)) + return 0 + + +if __name__ == "__main__": + raise SystemExit(main()) diff --git a/research/frame-pair-enumeration-production/verify.py b/research/frame-pair-enumeration-production/verify.py new file mode 100644 index 0000000000..8bf220b6fe --- /dev/null +++ b/research/frame-pair-enumeration-production/verify.py @@ -0,0 +1,229 @@ +#!/usr/bin/env python3 +"""Equivalence, pin and rejection controls for production frame-pair enumeration. + +Read-only by default. Timing is not a pass gate; see benchmark.py / RESULT.json. +""" +from __future__ import annotations + +import argparse +import contextlib +import copy +import hashlib +import io +import json +from pathlib import Path +import subprocess +import sys +import tempfile +import types + +ROOT = Path(__file__).resolve().parents[2] +PACKAGE = Path(__file__).resolve().parent +PRODUCTION = ROOT / "research/complex-frame-pair-decoders/verify.py" +BASELINE = PACKAGE / "baseline.py" +FAST = ROOT / "research/frame-pair-enumeration-fast-seed93/fast.py" + +BASE_COMMIT = "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2" +ORIGINAL_BLOB = "57dd8993e8ac016e8a92a9a885392b58014137bb" +ORIGINAL_SHA256 = "bdf7ee497dc04dfc634ee5b7848f6a2b39b0169668fb1a60a9715111dbd15395" +OPTIMIZED_SHA256 = "f7a9a39659c179853af3220f83a11b4c3cf52c8f3bccc0911a5629add10fbaff" + + +def require(condition, message): + if not condition: + raise AssertionError(message) + + +def digest_file(path: Path) -> str: + return hashlib.sha256(path.read_bytes()).hexdigest() + + +def unique_object(pairs): + out = {} + for key, value in pairs: + require(key not in out, f"duplicate JSON key: {key}") + out[key] = value + return out + + +def load_module(path: Path, name: str): + module = types.ModuleType(name) + module.__file__ = str(path) + # Keep assertions even when this wrapper is launched under -O. + exec(compile(path.read_bytes(), str(path), "exec", optimize=0), module.__dict__) + return module + + +def canonical(obj): + return json.dumps( + json.loads(json.dumps(obj, allow_nan=False)), + sort_keys=True, + separators=(",", ":"), + allow_nan=False, + ) + + +def digest(obj): + return hashlib.sha256(canonical(obj).encode()).hexdigest() + + +def scoped_receipt(module) -> dict: + """Replay PR968 sections D/E/H only (G binds the selected kappa record).""" + stream = [] + rank_records = [] + original = module.frame_pair_solutions + original_pair = module.pair_decoder + + def enumerate_pairs(a, b): + result = original(a, b) + stream.append([a, b, result]) + return result + + def pair_check(pairs, live): + answer = original_pair(pairs, live) + rank_records.append([pairs, live, answer]) + return answer + + module.frame_pair_solutions = enumerate_pairs + module.pair_decoder = pair_check + capture = io.StringIO() + with contextlib.redirect_stdout(capture): + frames, example, hist, kinds = module.section_d() + chain = module.section_e(frames, example) + module.section_h(example, frames, hist) + require(not module.FAILS, f"predecessor checks failed: {module.FAILS}") + require( + len(frames) == 1260 and len(stream) == 2520 and len(rank_records) == 7168, + "complete D/H enumeration/rank coverage", + ) + return { + "frames": len(frames), + "enumerations": len(stream), + "decoder_rank_checks": len(rank_records), + "term_rank_checks": sum(len(record[2][1]) for record in rank_records), + "ordered_solution_stream_sha256": digest(stream), + "rank_stream_sha256": digest(rank_records), + "histogram": sorted(hist.items()), + "types": sorted((str(k), v) for k, v in kinds.items()), + "example": example, + "chain": chain, + "log": capture.getvalue().splitlines(), + } + + +def check_baseline_bytes() -> None: + original = subprocess.check_output( + ["git", "show", f"{BASE_COMMIT}:research/complex-frame-pair-decoders/verify.py"], + cwd=ROOT, + ) + require(hashlib.sha256(original).hexdigest() == ORIGINAL_SHA256, "base verify.py sha256 drift") + blob = ( + subprocess.check_output( + ["git", "rev-parse", f"{BASE_COMMIT}:research/complex-frame-pair-decoders/verify.py"], + cwd=ROOT, + ) + .decode() + .strip() + ) + require(blob == ORIGINAL_BLOB, "base verify.py blob drift") + require(BASELINE.read_bytes() == original, "baseline.py must equal the base-commit verify.py") + require( + digest_file(PRODUCTION) == OPTIMIZED_SHA256, + "production verify.py does not match the claimed optimized digest", + ) + require(PRODUCTION.read_bytes() != original, "production must differ from the pairwise baseline") + text = PRODUCTION.read_text(encoding="utf-8") + require("neighbors = [sum(bool(IP[g][f])" in text, "production missing neighborhood masks") + require("Eight-bit neighborhood masks" in text, "production missing credit comment") + + +def check_equivalence() -> dict: + base = load_module(BASELINE, "frame_pair_baseline") + prod = load_module(PRODUCTION, "frame_pair_production") + base_receipt = scoped_receipt(base) + prod_receipt = scoped_receipt(prod) + require(base_receipt == prod_receipt, "D/E/H receipt mismatch between baseline and production") + # Pointwise census over every second frame. + frames = base.frames_in(base.P112) + require(len(frames) == 1260, "frame count") + for frame in frames: + require( + base.frame_pair_solutions(base.FRAME0, list(frame)) + == prod.frame_pair_solutions(prod.FRAME0, list(frame)), + "pointwise frame_pair_solutions mismatch", + ) + return { + "frames": 1260, + "decoders": 7168, + "term_ranks": base_receipt["term_rank_checks"], + "ordered_solution_stream_sha256": base_receipt["ordered_solution_stream_sha256"], + "rank_stream_sha256": base_receipt["rank_stream_sha256"], + } + + +def check_temp_corruption_rejection() -> dict: + """On-disk mutant that never accepts a singleton neighborhood must fail.""" + honest = scoped_receipt(load_module(PRODUCTION, "frame_pair_honest")) + with tempfile.TemporaryDirectory(prefix="frame-pair-prod-") as tmp: + mutant_path = Path(tmp) / "verify.py" + text = PRODUCTION.read_text(encoding="utf-8") + needle = "if hit and hit & (hit - 1) == 0:" + require(text.count(needle) == 2, "expected two singleton-neighborhood tests") + foil = text.replace(needle, "if False and hit and hit & (hit - 1) == 0:", 1) + mutant_path.write_text(foil, encoding="utf-8") + require(mutant_path.read_bytes() != PRODUCTION.read_bytes(), "mutant must differ on disk") + try: + bad = scoped_receipt(load_module(mutant_path, "frame_pair_mutant")) + except Exception as exc: # noqa: BLE001 — foil may raise AssertionError or census TypeError + return {"rejected": True, "mode": "subprocess_failure", "detail": f"{type(exc).__name__}: {exc}"[:240]} + require(bad != honest, "disabled neighborhood test must change the D/E/H receipt") + return { + "rejected": True, + "mode": "receipt_divergence", + "honest_stream": honest["ordered_solution_stream_sha256"], + "mutant_stream": bad["ordered_solution_stream_sha256"], + } + + +def check_opt_in_fast_module() -> None: + """Historical fast.py still matches production on the live IP table.""" + prod = load_module(PRODUCTION, "frame_pair_prod_fast_check") + spec = types.ModuleType("fast_enum") + exec(compile(FAST.read_bytes(), str(FAST), "exec", optimize=0), spec.__dict__) + for frame in prod.frames_in(prod.P112): + require( + prod.frame_pair_solutions(prod.FRAME0, list(frame)) + == spec.frame_pair_solutions(prod.FRAME0, list(frame), prod.IP), + "production diverges from opt-in fast.py", + ) + + +def main(argv: list[str] | None = None) -> int: + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument( + "--write-result", + action="store_true", + help="unused placeholder; default verify is read-only and never writes certificates", + ) + args = parser.parse_args(argv) + require(not args.write_result, "default verify is read-only; do not pass --write-result") + + check_baseline_bytes() + receipt = check_equivalence() + corruption = check_temp_corruption_rejection() + check_opt_in_fast_module() + # Duplicate-key control on a tiny JSON object used by this package. + json.loads('{"a":1,"b":2}', object_pairs_hook=unique_object) + + print( + "PASS_FRAME_PAIR_ENUMERATION_PRODUCTION " + f"frames={receipt['frames']} decoders={receipt['decoders']} " + f"term_ranks={receipt['term_ranks']} " + f"corruption={corruption['mode']} " + "certs=0 no_new_kappa" + ) + return 0 + + +if __name__ == "__main__": + raise SystemExit(main()) diff --git a/research/p104-asynchronous-carrier-bound/SOURCES.json b/research/p104-asynchronous-carrier-bound/SOURCES.json index 241123a031..af0b9c838c 100644 --- a/research/p104-asynchronous-carrier-bound/SOURCES.json +++ b/research/p104-asynchronous-carrier-bound/SOURCES.json @@ -2,7 +2,7 @@ "base_commit": "abdc6a7002abdbcd9e21bfc5e1a795784deacfdf", "files": { "research/community-frontier942-audit/ASSEMBLY.json": "4b2894956e594e408e111d806c842f2ed2c32aefcadff93fad69ff0b46f1991a", - "research/complex-frame-pair-decoders/verify.py": "bdf7ee497dc04dfc634ee5b7848f6a2b39b0169668fb1a60a9715111dbd15395", + "research/frame-pair-enumeration-production/baseline.py": "bdf7ee497dc04dfc634ee5b7848f6a2b39b0169668fb1a60a9715111dbd15395", "research/complex-frame-pair-decoders/PROOF.md": "ba53c1d8a9bc2d935d546bde46ca7341bd65f8515013e07b073296b4db2a9a74", "research/complex-frame-pair-decoders/README.md": "edd848b0177dc73a6e2646d4fd82f0b2ceae37e642bf19d6af602579a041a57e", "research/complex-k492-owner-repair/vendor/multicold/engines/moment.py": "81cbc864e106418fc7854322746f72180cb8110ff39f74450a3b8d55a82c1482", diff --git a/research/p104-asynchronous-carrier-bound/verify.py b/research/p104-asynchronous-carrier-bound/verify.py index 4bb5ca568b..209806f9ea 100644 --- a/research/p104-asynchronous-carrier-bound/verify.py +++ b/research/p104-asynchronous-carrier-bound/verify.py @@ -146,7 +146,8 @@ def check_poset_certificate(supports, certificate): def census(repo): - source = module(repo / 'research/complex-frame-pair-decoders/verify.py', 'pr968') + # Pairwise-era PR968 model bytes; production verify.py ships the neighborhood enumerator. + source = module(repo / 'research/frame-pair-enumeration-production/baseline.py', 'pr968') require(source.f2_rank(source.NROW) == 9, 'label pairing rank') frames = source.frames_in(range(120)) f0 = tuple(source.FRAME0) diff --git a/research/p104-nullpair-compensated-shear-seed318bd5/SOURCES.json b/research/p104-nullpair-compensated-shear-seed318bd5/SOURCES.json index 5785784a36..2ebcc0b98e 100644 --- a/research/p104-nullpair-compensated-shear-seed318bd5/SOURCES.json +++ b/research/p104-nullpair-compensated-shear-seed318bd5/SOURCES.json @@ -36,7 +36,14 @@ "path": "research/complex-frame-pair-decoders/verify.py", "usage": "provenance", "git_blob": "57dd8993e8ac016e8a92a9a885392b58014137bb", - "sha256": "bdf7ee497dc04dfc634ee5b7848f6a2b39b0169668fb1a60a9715111dbd15395" + "sha256": "bdf7ee497dc04dfc634ee5b7848f6a2b39b0169668fb1a60a9715111dbd15395", + "note": "Pairwise-era digest retained as provenance after research/frame-pair-enumeration-production/; live runtime pin retargeted via e8_model to that package baseline.py." } - ] + ], + "e8_model": { + "path": "research/frame-pair-enumeration-production/baseline.py", + "git_blob": "57dd8993e8ac016e8a92a9a885392b58014137bb", + "sha256": "bdf7ee497dc04dfc634ee5b7848f6a2b39b0169668fb1a60a9715111dbd15395", + "note": "Retargeted pairwise frame-pair predecessor after production rewrite; not a base_commit files[] pin (path did not exist at base_commit)." + } } diff --git a/research/p104-nullpair-compensated-shear-seed318bd5/VERIFY.json b/research/p104-nullpair-compensated-shear-seed318bd5/VERIFY.json index 571413a69a..5446543367 100644 --- a/research/p104-nullpair-compensated-shear-seed318bd5/VERIFY.json +++ b/research/p104-nullpair-compensated-shear-seed318bd5/VERIFY.json @@ -7,7 +7,8 @@ "certificates/selected-result.json", "research/complex-frame-pair-decoders/inputs/pr717/P104_HIT_flip_3a.txt", "research/complex-local-word-ceiling/ceiling.py", - "research/complex-local-word-ceiling/RESULT.json" + "research/complex-local-word-ceiling/RESULT.json", + "research/frame-pair-enumeration-production/baseline.py" ], "commands": [ { diff --git a/research/p104-nullpair-compensated-shear-seed318bd5/verify.py b/research/p104-nullpair-compensated-shear-seed318bd5/verify.py index 9198c66eb3..5882de11fd 100644 --- a/research/p104-nullpair-compensated-shear-seed318bd5/verify.py +++ b/research/p104-nullpair-compensated-shear-seed318bd5/verify.py @@ -181,14 +181,18 @@ def run(): selected_path = ROOT / "certificates/selected-result.json" selected = json.loads(selected_path.read_text()) require(sha(selected_path) == SELECTED, "selected record pin changed") + sources = json.loads((HERE / "SOURCES.json").read_text()) + e8_model = sources["e8_model"] pins = { "P104 decoder": (INPUT, "8e0178db02c14e1b29058cdbdbd50aac22f2b55a1ba21dc82f417610c9932526"), "ceiling engine": (ROOT / "research/complex-local-word-ceiling/ceiling.py", "86a1432870b3b21d8454106ec9162fddc0471472d9214c590a1420f2426cedfc"), "ceiling result": (ROOT / "research/complex-local-word-ceiling/RESULT.json", "d91d6c46509875abf1f61de67c2609656d3dc685451299f83caa6f922493692d"), - "frame-pair predecessor": (ROOT / "research/complex-frame-pair-decoders/verify.py", - "bdf7ee497dc04dfc634ee5b7848f6a2b39b0169668fb1a60a9715111dbd15395"), + # Pairwise-era bytes live in the production package baseline after + # research/frame-pair-enumeration-production/; live verify.py ships the + # eight-bit neighborhood enumerator and no longer matches this digest. + "frame-pair predecessor": (ROOT / e8_model["path"], e8_model["sha256"]), } for name, (path, expected) in pins.items(): require(sha(path) == expected, f"{name} SHA-256 changed: {sha(path)}") diff --git a/research/p104-term-shear-seed8be7/SOURCES.json b/research/p104-term-shear-seed8be7/SOURCES.json index 38d47c7278..06124ad7d7 100644 --- a/research/p104-term-shear-seed8be7/SOURCES.json +++ b/research/p104-term-shear-seed8be7/SOURCES.json @@ -28,9 +28,10 @@ }, { "path": "research/complex-frame-pair-decoders/verify.py", - "usage": "input", + "usage": "provenance", "git_blob": "57dd8993e8ac016e8a92a9a885392b58014137bb", - "sha256": "bdf7ee497dc04dfc634ee5b7848f6a2b39b0169668fb1a60a9715111dbd15395" + "sha256": "bdf7ee497dc04dfc634ee5b7848f6a2b39b0169668fb1a60a9715111dbd15395", + "note": "Pairwise-era digest retained as provenance after research/frame-pair-enumeration-production/; runtime model retargeted via e8_model to that package baseline.py." }, { "path": "research/complex-local-word-ceiling/RESULT.json", @@ -44,5 +45,11 @@ "git_blob": "6c0f54527d879396f689523bfde19928a9b6157c", "sha256": "86a1432870b3b21d8454106ec9162fddc0471472d9214c590a1420f2426cedfc" } - ] + ], + "e8_model": { + "path": "research/frame-pair-enumeration-production/baseline.py", + "git_blob": "57dd8993e8ac016e8a92a9a885392b58014137bb", + "sha256": "bdf7ee497dc04dfc634ee5b7848f6a2b39b0169668fb1a60a9715111dbd15395", + "note": "Retargeted pairwise E8 model after production rewrite; not a base_commit files[] pin (path did not exist at base_commit)." + } } diff --git a/research/p104-term-shear-seed8be7/VERIFY.json b/research/p104-term-shear-seed8be7/VERIFY.json index 2a2aada944..5ebd1df622 100644 --- a/research/p104-term-shear-seed8be7/VERIFY.json +++ b/research/p104-term-shear-seed8be7/VERIFY.json @@ -8,9 +8,9 @@ "research/p104-term-shear-seed8be7/RESULT.json", "research/complex-frame-pair-decoders/SOURCES.json", "research/complex-frame-pair-decoders/inputs/pr717/P104_HIT_flip_3a.txt", - "research/complex-frame-pair-decoders/verify.py", "research/complex-local-word-ceiling/RESULT.json", - "research/complex-local-word-ceiling/ceiling.py" + "research/complex-local-word-ceiling/ceiling.py", + "research/frame-pair-enumeration-production/baseline.py" ], "commands": [ { diff --git a/research/p104-term-shear-seed8be7/verify.py b/research/p104-term-shear-seed8be7/verify.py index 6045a8de67..de9ebc0d0d 100644 --- a/research/p104-term-shear-seed8be7/verify.py +++ b/research/p104-term-shear-seed8be7/verify.py @@ -12,7 +12,6 @@ HERE = Path(__file__).resolve().parent ROOT = HERE.parents[1] -PINNED = ROOT / 'research/complex-frame-pair-decoders/verify.py' HIT = ROOT / 'research/complex-frame-pair-decoders/inputs/pr717/P104_HIT_flip_3a.txt' CEILING = ROOT / 'research/complex-local-word-ceiling/ceiling.py' CLIQUES = [9, 15, 24, 46, 52, 66, 94, 104] @@ -100,7 +99,12 @@ def columns(M): def main(): - model = load_module(PINNED, 'p104_predecessor_model') + # Pairwise-era PR968 model; production verify.py ships the neighborhood enumerator. + sources = json.loads((HERE / 'SOURCES.json').read_text()) + e8_model = sources['e8_model'] + pinned = ROOT / e8_model['path'] + assert hashlib.sha256(pinned.read_bytes()).hexdigest() == e8_model['sha256'], 'E8 model pin mismatch' + model = load_module(pinned, 'p104_predecessor_model') ceiling = load_module(CEILING, 'p104_exact_ceiling') P112 = [i for i in range(model.NL) if i not in model.FRAME0] F1 = [P112[q] for q in CLIQUES] diff --git a/research/p104-two-copy-drops/SOURCES.json b/research/p104-two-copy-drops/SOURCES.json index d49c5434dc..645ede4a9a 100644 --- a/research/p104-two-copy-drops/SOURCES.json +++ b/research/p104-two-copy-drops/SOURCES.json @@ -16,9 +16,10 @@ }, { "path": "research/complex-frame-pair-decoders/verify.py", - "usage": "input", + "usage": "provenance", "git_blob": "57dd8993e8ac016e8a92a9a885392b58014137bb", - "sha256": "bdf7ee497dc04dfc634ee5b7848f6a2b39b0169668fb1a60a9715111dbd15395" + "sha256": "bdf7ee497dc04dfc634ee5b7848f6a2b39b0169668fb1a60a9715111dbd15395", + "note": "Pairwise-era digest retained as provenance after research/frame-pair-enumeration-production/; working verify.py ships eight-bit neighborhood enumeration." } ] } diff --git a/research/p104-two-copy-drops/VERIFY.json b/research/p104-two-copy-drops/VERIFY.json index 1acbe6f83b..b90aa9abd0 100644 --- a/research/p104-two-copy-drops/VERIFY.json +++ b/research/p104-two-copy-drops/VERIFY.json @@ -4,7 +4,8 @@ "python": "3.12", "requirements": [], "inputs": [ - "research/complex-frame-pair-decoders/verify.py" + "research/p104-two-copy-drops/inputs/PREDECESSOR.json", + "research/p104-two-copy-drops/DEPENDENCY.json" ], "commands": [ { diff --git a/research/p112-batch-centre-floor/SOURCES.json b/research/p112-batch-centre-floor/SOURCES.json index c142170a07..4e34dcce5d 100644 --- a/research/p112-batch-centre-floor/SOURCES.json +++ b/research/p112-batch-centre-floor/SOURCES.json @@ -34,9 +34,10 @@ }, { "path": "research/complex-frame-pair-decoders/verify.py", - "usage": "input", + "usage": "provenance", "git_blob": "57dd8993e8ac016e8a92a9a885392b58014137bb", - "sha256": "bdf7ee497dc04dfc634ee5b7848f6a2b39b0169668fb1a60a9715111dbd15395" + "sha256": "bdf7ee497dc04dfc634ee5b7848f6a2b39b0169668fb1a60a9715111dbd15395", + "note": "Pairwise-era digest retained as provenance after research/frame-pair-enumeration-production/; working verify.py ships eight-bit neighborhood enumeration." }, { "path": "research/complex-local-word-ceiling/README.md", diff --git a/research/p112-batch-centre-floor/VERIFY.json b/research/p112-batch-centre-floor/VERIFY.json index e0596aed68..4c33c8da83 100644 --- a/research/p112-batch-centre-floor/VERIFY.json +++ b/research/p112-batch-centre-floor/VERIFY.json @@ -7,7 +7,6 @@ "research/complex-decoder-field-extension-seed44/NOTICE.md", "research/complex-decoder-field-extension-seed44/README.md", "research/complex-frame-pair-decoders/README.md", - "research/complex-frame-pair-decoders/verify.py", "research/complex-local-word-ceiling/README.md", "research/e8-factor-linear-overcomplete47/NOTICE.md", "research/e8-factor-linear-overcomplete47/README.md", diff --git a/research/root-pair-first-drop-seed48/SOURCES.json b/research/root-pair-first-drop-seed48/SOURCES.json index 1b02060723..ca85c8b9d6 100644 --- a/research/root-pair-first-drop-seed48/SOURCES.json +++ b/research/root-pair-first-drop-seed48/SOURCES.json @@ -3,7 +3,8 @@ "files": { "research/complex-frame-pair-decoders/PROOF.md": "ba53c1d8a9bc2d935d546bde46ca7341bd65f8515013e07b073296b4db2a9a74", "research/complex-frame-pair-decoders/README.md": "edd848b0177dc73a6e2646d4fd82f0b2ceae37e642bf19d6af602579a041a57e", - "research/complex-frame-pair-decoders/verify.py": "bdf7ee497dc04dfc634ee5b7848f6a2b39b0169668fb1a60a9715111dbd15395" + "research/frame-pair-enumeration-production/baseline.py": "bdf7ee497dc04dfc634ee5b7848f6a2b39b0169668fb1a60a9715111dbd15395" }, - "normalization": "text CRLF to LF" + "normalization": "text CRLF to LF", + "note": "After research/frame-pair-enumeration-production/, pairwise verify.py bytes are pinned via that package baseline.py." } diff --git a/research/root-pair-first-drop-seed48/check_sources.py b/research/root-pair-first-drop-seed48/check_sources.py index 28bb6eaf5b..6c64c1f2a2 100644 --- a/research/root-pair-first-drop-seed48/check_sources.py +++ b/research/root-pair-first-drop-seed48/check_sources.py @@ -23,7 +23,7 @@ def load(name,path): def main(): check=load('first_drop',HERE/'verify.py') roots,pairing,_,_,_=check.model.setup() - predecessor=load('credited_pr968',check.ROOT/'research/complex-frame-pair-decoders/verify.py') + predecessor=load('credited_pr968',check.ROOT/'research/frame-pair-enumeration-production/baseline.py') mapping={max(r,tuple(-x for x in r)):i for i,r in enumerate(predecessor.LINES)} check.need(set(mapping)==set(roots),'same 120 root lines') order=[mapping[r] for r in roots] diff --git a/research/root-pair-first-drop-seed48/verify.py b/research/root-pair-first-drop-seed48/verify.py index cef6656fef..c29c3ebf29 100644 --- a/research/root-pair-first-drop-seed48/verify.py +++ b/research/root-pair-first-drop-seed48/verify.py @@ -17,7 +17,7 @@ ROOT = HERE.parents[1] BASE = '2921874911956718fcaaaf9396fe8267b3cfa9f0' SOURCES = {'research/complex-frame-pair-decoders/PROOF.md', - 'research/complex-frame-pair-decoders/verify.py', + 'research/frame-pair-enumeration-production/baseline.py', 'research/complex-frame-pair-decoders/README.md'} spec = importlib.util.spec_from_file_location('local_root_model', HERE/'explore.py') model = importlib.util.module_from_spec(spec) diff --git a/research/selected-p104-port-adapter/SOURCES.json b/research/selected-p104-port-adapter/SOURCES.json index 6bbd1a7e04..78724a96bb 100644 --- a/research/selected-p104-port-adapter/SOURCES.json +++ b/research/selected-p104-port-adapter/SOURCES.json @@ -2,16 +2,67 @@ "schema_version": 1, "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea", "files": [ - {"path": "docs/research/agent-task-catalog.json", "usage": "provenance", "git_blob": "06c96f5579bb67ed1b86d334e78fbed7da6945f1", "sha256": "6686ad58f1fbdbc87134a78901b60fd53a20d3984355e91defbbebc9e9fa8075"}, - {"path": "certificates/selected-result.json", "usage": "input", "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32"}, - {"path": "research/community-frontier1094-audit/ASSEMBLY.json", "usage": "input", "git_blob": "5fd676df060f3b450782fdf5ff5f6beb63a5eeb0", "sha256": "1122cb3a575f8c788345fc1bf4c108ac7c3250fb81a5988671f5eb04b3ab3045"}, - {"path": "research/complex-block-rank-optimum/inputs/selected.json.gz", "usage": "input", "git_blob": "5f9ef680983b0b63a4c82a4ed909837b78e690cd", "sha256": "16bc0ebb04b4be6c0ade74badc6a0c0cdba4215eda86e4ff9f13abf8ecebd219"}, - {"path": "research/complex-frame-pair-decoders/verify.py", "usage": "input", "git_blob": "57dd8993e8ac016e8a92a9a885392b58014137bb", "sha256": "bdf7ee497dc04dfc634ee5b7848f6a2b39b0169668fb1a60a9715111dbd15395"}, - {"path": "research/complex-k492-owner-repair/vendor/multicold/engines/moment.py", "usage": "input", "git_blob": "7d697cb45203fe72d97037403d6da41f71f3b7fd", "sha256": "81cbc864e106418fc7854322746f72180cb8110ff39f74450a3b8d55a82c1482"}, - {"path": "research/complex-k492-owner-repair/vendor/multicold/engines/base_two_moment.py", "usage": "input", "git_blob": "14a90fa0e788217856f070382c9e61bd7c603c61", "sha256": "aee70c242a2f1d225528fabe2002e1564d1dc884797c07d28a831c7878ee9098"}, - {"path": "research/complex-k492-owner-repair/vendor/multicold/engines/outer.py", "usage": "input", "git_blob": "43007488ad2c43187c77cc6798beff8b1cd76ad2", "sha256": "c1ebb52163a7219504c728a5c2b098bf1e50bf20148a2879c5a74c3cadc7c03c"}, - {"path": "research/complex-t21-owners/vendor/pr870/independent/price_profile_t16.py", "usage": "input", "git_blob": "8d95804ac8b029a17925a8064395b0b818955651", "sha256": "53f8e62dcf27bee032c1bee0245d126a9c8a12ebcf24f6aaff65ea3122fffe29"}, - {"path": "research/complex-t21-owners/vendor/pr870/inputs/PR589-EXPECTED.json", "usage": "input", "git_blob": "e293ddc557742637f9f679f083a1a282d87b1b13", "sha256": "b9f0e5ca038abe837b0007c8fe006f366a6f02009244ac57705a8a200e2301f4"} + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "06c96f5579bb67ed1b86d334e78fbed7da6945f1", + "sha256": "6686ad58f1fbdbc87134a78901b60fd53a20d3984355e91defbbebc9e9fa8075" + }, + { + "path": "certificates/selected-result.json", + "usage": "input", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "research/community-frontier1094-audit/ASSEMBLY.json", + "usage": "input", + "git_blob": "5fd676df060f3b450782fdf5ff5f6beb63a5eeb0", + "sha256": "1122cb3a575f8c788345fc1bf4c108ac7c3250fb81a5988671f5eb04b3ab3045" + }, + { + "path": "research/complex-block-rank-optimum/inputs/selected.json.gz", + "usage": "input", + "git_blob": "5f9ef680983b0b63a4c82a4ed909837b78e690cd", + "sha256": "16bc0ebb04b4be6c0ade74badc6a0c0cdba4215eda86e4ff9f13abf8ecebd219" + }, + { + "path": "research/complex-frame-pair-decoders/verify.py", + "usage": "provenance", + "git_blob": "57dd8993e8ac016e8a92a9a885392b58014137bb", + "sha256": "bdf7ee497dc04dfc634ee5b7848f6a2b39b0169668fb1a60a9715111dbd15395", + "note": "Pairwise-era digest retained as provenance after research/frame-pair-enumeration-production/; live E8 model retargeted to that package baseline.py." + }, + { + "path": "research/complex-k492-owner-repair/vendor/multicold/engines/moment.py", + "usage": "input", + "git_blob": "7d697cb45203fe72d97037403d6da41f71f3b7fd", + "sha256": "81cbc864e106418fc7854322746f72180cb8110ff39f74450a3b8d55a82c1482" + }, + { + "path": "research/complex-k492-owner-repair/vendor/multicold/engines/base_two_moment.py", + "usage": "input", + "git_blob": "14a90fa0e788217856f070382c9e61bd7c603c61", + "sha256": "aee70c242a2f1d225528fabe2002e1564d1dc884797c07d28a831c7878ee9098" + }, + { + "path": "research/complex-k492-owner-repair/vendor/multicold/engines/outer.py", + "usage": "input", + "git_blob": "43007488ad2c43187c77cc6798beff8b1cd76ad2", + "sha256": "c1ebb52163a7219504c728a5c2b098bf1e50bf20148a2879c5a74c3cadc7c03c" + }, + { + "path": "research/complex-t21-owners/vendor/pr870/independent/price_profile_t16.py", + "usage": "input", + "git_blob": "8d95804ac8b029a17925a8064395b0b818955651", + "sha256": "53f8e62dcf27bee032c1bee0245d126a9c8a12ebcf24f6aaff65ea3122fffe29" + }, + { + "path": "research/complex-t21-owners/vendor/pr870/inputs/PR589-EXPECTED.json", + "usage": "input", + "git_blob": "e293ddc557742637f9f679f083a1a282d87b1b13", + "sha256": "b9f0e5ca038abe837b0007c8fe006f366a6f02009244ac57705a8a200e2301f4" + } ], "selected_record": { "path": "certificates/selected-result.json", @@ -30,13 +81,20 @@ "payload_sha256": "4ddb29fb9bc6f27e0c0fbfcf19a2a93a3496ad900d0f6d89059d0305c9576c0c" }, "e8_model": { - "path": "research/complex-frame-pair-decoders/verify.py", + "path": "research/frame-pair-enumeration-production/baseline.py", "git_blob": "57dd8993e8ac016e8a92a9a885392b58014137bb", "sha256": "bdf7ee497dc04dfc634ee5b7848f6a2b39b0169668fb1a60a9715111dbd15395", "model_predecessors": [ - {"pr": 717, "head": "4a97676294f9fa413b65986e9984fddeda71e4cc"}, - {"pr": 968, "base": "bbc600db2fc15007b7c914f4f2b2ed55fa909c87"} - ] + { + "pr": 717, + "head": "4a97676294f9fa413b65986e9984fddeda71e4cc" + }, + { + "pr": 968, + "base": "bbc600db2fc15007b7c914f4f2b2ed55fa909c87" + } + ], + "note": "Retargeted to frame-pair-enumeration-production/baseline.py after production rewrite." }, "pricing_inputs": { "research/complex-k492-owner-repair/vendor/multicold/engines/moment.py": "81cbc864e106418fc7854322746f72180cb8110ff39f74450a3b8d55a82c1482", diff --git a/research/selected-p104-port-adapter/VERIFY.json b/research/selected-p104-port-adapter/VERIFY.json index c0d3c71184..c257365c9f 100644 --- a/research/selected-p104-port-adapter/VERIFY.json +++ b/research/selected-p104-port-adapter/VERIFY.json @@ -7,16 +7,20 @@ "certificates/selected-result.json", "research/community-frontier1094-audit/ASSEMBLY.json", "research/complex-block-rank-optimum/inputs/selected.json.gz", - "research/complex-frame-pair-decoders/verify.py", "research/complex-k492-owner-repair/vendor/multicold/engines/moment.py", "research/complex-k492-owner-repair/vendor/multicold/engines/base_two_moment.py", "research/complex-k492-owner-repair/vendor/multicold/engines/outer.py", "research/complex-t21-owners/vendor/pr870/independent/price_profile_t16.py", - "research/complex-t21-owners/vendor/pr870/inputs/PR589-EXPECTED.json" + "research/complex-t21-owners/vendor/pr870/inputs/PR589-EXPECTED.json", + "research/frame-pair-enumeration-production/baseline.py" ], "commands": [ { - "argv": ["{python}", "-B", "{package}/verify.py"], + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], "timeout_seconds": 120, "checks": "All 512 functional weights match under the pinned GL(9,2) adapter; selected ports map bijectively to P112; one 104-port frame-pair decoder has exact D*T^T=2G and eight rank-7 terms; exact selected-profile knob price and three negative controls reproduce." } diff --git a/research/selected-p104-port-adapter/verify.py b/research/selected-p104-port-adapter/verify.py index 79b24be235..f632218045 100644 --- a/research/selected-p104-port-adapter/verify.py +++ b/research/selected-p104-port-adapter/verify.py @@ -136,10 +136,13 @@ def construct(): "selected certificate SHA mismatch") require(sha(ROOT / "research/complex-block-rank-optimum/inputs/selected.json.gz") == manifest["selected_ports"]["sha256"], "selected port payload pin mismatch") - require(sha(ROOT / "research/complex-frame-pair-decoders/verify.py") == - manifest["e8_model"]["sha256"], "E8 model pin mismatch") + # After research/frame-pair-enumeration-production/, the pairwise E8 model + # bytes live in that package's baseline.py; production verify.py ships the + # neighborhood enumerator. Geometry and frame_pair_solutions stay equivalent. + e8_path = ROOT / manifest["e8_model"]["path"] + require(sha(e8_path) == manifest["e8_model"]["sha256"], "E8 model pin mismatch") - e8 = load_module(ROOT / "research/complex-frame-pair-decoders/verify.py", "adapter_e8_model") + e8 = load_module(e8_path, "adapter_e8_model") with gzip.open(ROOT / "research/complex-block-rank-optimum/inputs/selected.json.gz", "rt") as stream: selected_word = json.load(stream) ports = selected_word["ports"] diff --git a/tests/test_frame_pair_enumeration_production.py b/tests/test_frame_pair_enumeration_production.py new file mode 100644 index 0000000000..429cc81c8d --- /dev/null +++ b/tests/test_frame_pair_enumeration_production.py @@ -0,0 +1,38 @@ +#!/usr/bin/env python3 +"""Smoke tests for research/frame-pair-enumeration-production.""" +from __future__ import annotations + +from hashlib import sha256 +from pathlib import Path +import subprocess +import sys +import unittest + +ROOT = Path(__file__).resolve().parents[1] +PACKAGE = ROOT / "research/frame-pair-enumeration-production" +PRODUCTION = ROOT / "research/complex-frame-pair-decoders/verify.py" +BASELINE = PACKAGE / "baseline.py" +OPTIMIZED_SHA256 = "f7a9a39659c179853af3220f83a11b4c3cf52c8f3bccc0911a5629add10fbaff" +ORIGINAL_SHA256 = "bdf7ee497dc04dfc634ee5b7848f6a2b39b0169668fb1a60a9715111dbd15395" + + +class FramePairEnumerationProductionTests(unittest.TestCase): + def test_production_differs_from_baseline_and_matches_digest(self): + self.assertEqual(sha256(BASELINE.read_bytes()).hexdigest(), ORIGINAL_SHA256) + self.assertEqual(sha256(PRODUCTION.read_bytes()).hexdigest(), OPTIMIZED_SHA256) + self.assertNotEqual(PRODUCTION.read_bytes(), BASELINE.read_bytes()) + self.assertIn("neighbors = [sum(bool(IP[g][f])", PRODUCTION.read_text(encoding="utf-8")) + + def test_verify_script(self): + proc = subprocess.run( + [sys.executable, "-I", "-B", str(PACKAGE / "verify.py")], + cwd=ROOT, + capture_output=True, + text=True, + ) + self.assertEqual(proc.returncode, 0, proc.stdout + proc.stderr) + self.assertIn("PASS_FRAME_PAIR_ENUMERATION_PRODUCTION", proc.stdout) + + +if __name__ == "__main__": + unittest.main()