From b05e864cd2420a1c03402e03c3d3930469501414 Mon Sep 17 00:00:00 2001 From: Sagar Thakrar Date: Tue, 13 Oct 2026 10:07:52 +0530 Subject: [PATCH 1/2] research: certify R420 adjacent A-gate frame rigidity --- .../r420-adjacent-a-seed00/CERTIFICATE.json | 28 +++ research/r420-adjacent-a-seed00/CLAIM.json | 18 ++ research/r420-adjacent-a-seed00/README.md | 187 ++++++++++++++ research/r420-adjacent-a-seed00/SOURCES.json | 22 ++ .../r420-adjacent-a-seed00/VALIDATION.json | 54 ++++ .../independent_check.py | 166 +++++++++++++ research/r420-adjacent-a-seed00/verify.py | 233 ++++++++++++++++++ 7 files changed, 708 insertions(+) create mode 100644 research/r420-adjacent-a-seed00/CERTIFICATE.json create mode 100644 research/r420-adjacent-a-seed00/CLAIM.json create mode 100644 research/r420-adjacent-a-seed00/README.md create mode 100644 research/r420-adjacent-a-seed00/SOURCES.json create mode 100644 research/r420-adjacent-a-seed00/VALIDATION.json create mode 100644 research/r420-adjacent-a-seed00/independent_check.py create mode 100644 research/r420-adjacent-a-seed00/verify.py diff --git a/research/r420-adjacent-a-seed00/CERTIFICATE.json b/research/r420-adjacent-a-seed00/CERTIFICATE.json new file mode 100644 index 0000000000..f1ee3aee90 --- /dev/null +++ b/research/r420-adjacent-a-seed00/CERTIFICATE.json @@ -0,0 +1,28 @@ +{ + "controls": 8, + "counts": { + "commuting": 1735, + "noncommuting": 328, + "same_destination": 726 + }, + "forced_dimension_census": { + "1": 479, + "2": 360, + "4": 2140, + "6": 480, + "8": 11 + }, + "forced_gate_occurrences": 3470, + "full_local_paid_profile": { + "1": 1320, + "2": 1440, + "4": 60, + "5": 120, + "8": 9 + }, + "positions": 2063, + "rank_mass": 5112, + "rational_frame_gaps": 0, + "status": "PASS_R420_ADJACENT_A_RIGIDITY", + "witness_rows_sha256": "1e3a96692cd65a757280149946f40f63ea1e1a63ae978f5daf8c8796087e67c0" +} diff --git a/research/r420-adjacent-a-seed00/CLAIM.json b/research/r420-adjacent-a-seed00/CLAIM.json new file mode 100644 index 0000000000..13b2a5daae --- /dev/null +++ b/research/r420-adjacent-a-seed00/CLAIM.json @@ -0,0 +1,18 @@ +{ + "track": "bit supplier", + "assignment_seed": 0, + "randomness": "Node.js crypto.randomInt(100), operating-system-backed, drawn 2026-10-13T04:23:45Z", + "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "object": "PR543 R420 phase-A adjacent commuting gate exchanges with joint frame reassignment", + "method": "Exhaust every adjacent pair of original A gate records, including single-source gates and multi-source totals, whose destinations do not occur in each other's sources. Reverse their order and jointly reframe subject to exact nesting and unchanged A-boundary frames. Mirror the swap in full-frame C to preserve H4. Initially enumerate the existing catalogue; then certify lower-span/upper-intersection equality over Q to cover unlisted frames too.", + "expected_deliverable": "One verified local supplier improvement, or a reproducible scoped negative result with exact coverage and controls; no automatic kappa claim", + "expected_finish_utc": "2026-10-13T05:03:45Z", + "coordination": "GitHub pinnedIssues was empty; local claim per sprint instructions. Open PR metadata checked through #700 before claiming.", + "candidates": [ + "R420 adjacent A-gate exchange with joint reframing, selected by seed 0 modulo 3", + "P111 coordinated changes outside the PR589 greedy fixed point", + "R420 decoder/COPY-cost change" + ], + "overlap": "PR661 fixes B gate order. PR589 single-operation transport on P111 differs in word and simultaneous search class. PR691 changes a quad circuit; PR694 changes helper basis. This task preserves each original A gate and its sources.", + "status": "claimed locally" +} diff --git a/research/r420-adjacent-a-seed00/README.md b/research/r420-adjacent-a-seed00/README.md new file mode 100644 index 0000000000..c2893773df --- /dev/null +++ b/research/r420-adjacent-a-seed00/README.md @@ -0,0 +1,187 @@ +# R420 adjacent A-gate exchanges have no frame freedom + +**Scoped negative result. No new bit exponent or κ.** In eumemic's PR543 R420 +word, each of the 1,735 commuting adjacent A-gate pairs can be reversed, but +neither gate can change its frame. This holds even if the two new frames may +be arbitrary rational subspaces, beyond the existing catalogue. Every such +single exchange preserves the local paid recursive profile. + +The base is `66849e1475c930fd7732b1a0067ffee7e1e95f60`. At that commit the +[selected record](../../certificates/selected-result.json) uses #626 with +#543 and has conditional κ = `51110230636731/31250000000000000`, or +`0.001635527380375392`. Its +[maintainer review](../../docs/research/community-k492-review.md) identifies +the retained assumptions. Larger numbers in open PRs are pending claims. +This package changes no selected artifact or file under `upstream/`. + +## Reproduce + +From the repository root, with Python 3.11+ and the standard library: + +```sh +python3 -B research/r420-adjacent-a-seed00/verify.py +python3 -B research/r420-adjacent-a-seed00/independent_check.py +``` + +The first command checks the pinned predecessor's exact labels, 660 symbolic +dirty-input columns and H1–H5, checks every frame-rigidity obligation, recounts +the complete local paid profile, runs eight controls and compares the result +with `CERTIFICATE.json`. Its final line is: + +```text +PASS_R420_ADJACENT_A_RIGIDITY positions=2063 commuting=1735 forced=3470 gaps=0 rank_mass=5112 controls=8 +``` + +The second implementation imports no project checker. It independently checks +the 672 frame closures and exact orthogonal complements, recomputes all +dimension equalities, and replays the entire A phase after every one of the +1,735 swaps on all 660 symbolic inputs. It also checks that every excluded +dependency pair changes the A operator when swapped. Expected final census: + +```text +Forced-frame rank census: {"1": 479, "2": 360, "4": 2140, "6": 480, "8": 11} +A rank-jump histogram: {"1": 600, "2": 989, "4": 60} +``` + +`verify.py --print-certificate` prints the freshly computed certificate without +overwriting it. The witness digest covers canonical JSON rows +`[pair_index, [[original_frame, prior_frame_ids, next_frame_ids, lower_rank, +upper_rank], ...]]`, sorted by original pair index. Frame-ID sets are sorted. +The verifier regenerates the rows from the pinned word; the digest is a +reproduction checksum, not a substitute for the dimension checks. + +## Exact search class + +Choose one index `i` in `0..2062` of the original 2,064-gate A list. Gates are +original records, including single-source gates and the nine multi-source +totals. They are not flattened, factored or synthesized. A gate acts as +`destination ^= XOR(sources)` and every operand uses its gate frame. + +Only pairs with neither destination in the other gate's source list are +admitted. This includes 726 pairs with the same destination. Reverse the two +records and choose both replacement frames jointly. All other A records, +the exact entry and end-of-A frames, D, scatter, B, final frames, registers, +retained totals and decoder remain fixed. Preserve H4 by mirroring the +exchange in the literal reverse cleanup C, at the full frame. + +All 2,063 positions are classified: 1,735 commute and 328 have a dependency. +For the admitted pairs there are 3,470 gate-occurrences to check. The stopping +rule is completion of this finite list, with no random search or timeout. +OS assignment seed 00 selected this object from the three candidates in +`CLAIM.json`; the resulting enumeration is deterministic. + +The first experiment found exactly one feasible catalogue-frame pair at each +commuting position, always the original two frames. The delivered argument +strengthens that observation to all rational subspaces, using exact lower +spans and upper intersections. No claim of catalogue completeness is needed. + +## Why the frames are forced + +For a chosen pair and an operand register `r`, let `P_r` be its frame immediately +before the pair. Let `N_r` be the frame at its first later A use outside the +pair, or its prescribed end-of-A frame if it has no later A use. These are +fixed independently of the two proposed replacement frames. + +For either gate `g`, define subspaces of the eight-dimensional rational label +space: + +```text +L_g = sum of P_r over every operand r of g +U_g = intersection of N_r over every operand r of g +``` + +Monotone frame paths necessarily imply `L_g ⊆ F_g ⊆ U_g`, regardless of which +gate goes first. Even when a register also visits the other gate, nesting +still puts its earlier `P_r` below `F_g` and its later `N_r` above `F_g`. +These are necessary bounds, so omitting the coupling between gates only +relaxes the proposed schedule. + +For every gate-occurrence the checker establishes both containments for the +original frame `F_old` and the exact equalities +`dim L_g = dim F_old = dim U_g`. Hence `L_g = F_old = U_g` and any admissible +new frame equals `F_old`. The table gives the completed obligations: + +| Forced dimension | Gate-occurrences | +| --- | ---: | +| 1 | 479 | +| 2 | 360 | +| 4 | 2,140 | +| 6 | 480 | +| 8 | 11 | + +All ranks use exact rational elimination. In particular, the upper dimension +is computed as `8 - rank(sum of orthogonal complements of N_r)`. Intersecting +the sets of listed root lines would be insufficient: an intersection can +contain a direction absent from those lists. A synthetic two-plane control +explicitly exercises this case. + +Every shared operand in an admitted pair uses equal original frames in the +two gates. Once those frames are forced, exchanging the gates preserves that +register's frame path after repeated equal-frame visits are removed. An +operand used in only one gate also keeps its frame path. Thus all rank jumps +and retained COPY ranks remain equal, with no numerical comparison of powers. + +## Complete local cost and boundary obligations + +The complete local paid profile remains +`{1:1320, 2:1440, 4:60, 5:120, 8:9}`, with rank mass 5,112. Its moment is +unchanged for every positive exponent, as an equality of profiles. There are +still 420 helpers, nine retained COPYs of rank 8, and 26,916 binary ADDs. +D's dirty compensation, source accesses, all other climbs, scatter, B, +restoration and final climbs have not been omitted from that profile. + +The two XOR maps commute because neither reads the other's destination. +For a common destination both add unchanged source parities to the same row. +The rest of A therefore sees exactly the same values, including arbitrary +helper dirt. B and scatter keep the same input. Mirroring the two records in +C preserves its literal-reverse interface, with the same full-frame operands +and number of ADDs. Leaving C bytewise fixed would preserve the scalar inverse +but violate the syntactic H4 check; a control catches this distinction. + +This is a local paid-profile statement. It does not optimize changed owner +maps, call windows, scalar prefix bounds or other nonrecursive costs. Under +the same replication and idle remainder, the global recursive moment cannot +improve from this equal local profile. We did not rerun or change the full +assembly, and do not infer a new κ. + +## Controls and limits + +The main verifier checks a non-root intersection, a deliberately flexible +interval, a noncommuting dependency, an accepted same-destination pair, an +unmirrored cleanup rejection, an accepted mirrored full-word swap, a +noncommuting full-word rejection, and an equal-rank wrong-frame rejection. +The independent checker additionally rejects all 328 actual dependency swaps +by comparing their exact symbolic A operators. + +The conclusion covers one exchange in the original word. It does not cover +sequences of exchanges, nonadjacent transport, splitting a source list, +changed circuits, altered boundaries, other words, or improved hosting. This +is an exact finite-instance certificate with a written subspace argument, +not formal verification of the full multiplication theorem. The inherited +uniform compiler, mutable-basis/common-label realization, physical hosting, +precision, tape and analytic assumptions remain open as recorded upstream. + +## Relation to concurrent work and attribution + +PR661 proves a fixed-order phase-B moment bound for the same R420 word. This +package treats A, permits an order change and proves frame uniqueness rather +than comparing different rank partitions. No PR661 code is imported. PR589 +searches elementary-operation transports and reframing on the punctured P111 +word. Its circuit and search class differ. PR691 resynthesizes an R420 quad; +PR694 changes the frame-zero helper basis. Concurrent PR708 shares restored +operands while resynthesizing the decoder totals. Those mechanisms are outside this +gate-preserving class and are not contradicted by this result. + +The source construction and independent predecessor audit are eumemic's +PR543, head `2065fe4f72a914d907f1046603f5a36f17018535`. Credit also belongs to +Dylan Crow for the PR370 format, DreamingOfClouds for the nine-stage chain +and PR589 frame-transport work, Dugongue for PR541/548 transport mechanisms, +and Rohan Arun for PR542 least-frame work. The complete earlier source lineage +remains in the predecessor's notices. `SOURCES.json` records exact input pins, +the selected context and related PR heads; context hashes are historical and +are not enforced as runtime dependencies. + +Contribution by Sagar Thakrar / `thakrarsagar`, with substantial OpenAI Codex +assistance for the experiment, proof, implementation, independent second +implementation and review. New work is under the repository's Apache-2.0 +license; predecessor notices and source files are unchanged. diff --git a/research/r420-adjacent-a-seed00/SOURCES.json b/research/r420-adjacent-a-seed00/SOURCES.json new file mode 100644 index 0000000000..cfed5bf021 --- /dev/null +++ b/research/r420-adjacent-a-seed00/SOURCES.json @@ -0,0 +1,22 @@ +{ + "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "pr543_head": "2065fe4f72a914d907f1046603f5a36f17018535", + "selected_pr626_head": "660de893d27bb7abd1d5b01b1640207528a5c851", + "selected_kappa": "51110230636731/31250000000000000", + "inputs_sha256": { + "research/e8-bit-r420/data/bitE8mut-r420.json.gz": "9721a3819efd68307f66f00d84a952eb28eb7c3ad2ce79653ce295c98a764784", + "research/e8-bit-r420/code/xcheck.py": "5737d18a7826fd51e131035f2d7bebba2e2868af91dd7672a5f11208b036d424", + "research/e8-bit-r420/EXPECTED.json": "06eccee9f6b77e140833df83407e7996dc948c17d49b0779ab171fbe463fd28d" + }, + "context_sha256_at_base": { + "research/e8-bit-r420/README.md": "9807be57c6adf26b30e4f54e2f8160075bbc05091f1a6d157e43d2a4620c1c9f", + "certificates/selected-result.json": "b3bf402f31a69bde0629936a9b569bed48281568d7b16d5fba120b5311ea1f53", + "docs/research/community-k492-review.md": "3b731d30e80010b15408a289b0b32192700885474c8b36d48ee3320a7a8c5c47" + }, + "related_heads_not_imported": { + "589": "a5afc8c6169ea61ba7c51dfd3cade02cc7b13b46", + "661": "9ca7aa3ab0a3260a2f36ac86b9911a31fd88bd89", + "691": "ee6b9175fe006c11871802866c487b5ecc1a93a4", + "694": "9732ac127dd4bef98a846aaa904c20b5a84e72c1" + } +} diff --git a/research/r420-adjacent-a-seed00/VALIDATION.json b/research/r420-adjacent-a-seed00/VALIDATION.json new file mode 100644 index 0000000000..6bf5a6b3a0 --- /dev/null +++ b/research/r420-adjacent-a-seed00/VALIDATION.json @@ -0,0 +1,54 @@ +{ + "date_utc": "2026-10-13", + "platform": "macOS arm64", + "python_versions": ["3.11.15", "3.14.8"], + "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "checks": [ + { + "command": "python3 -I -B research/r420-adjacent-a-seed00/verify.py", + "result": "PASS, all 3470 exact frame bounds, complete local profile, predecessor labels/660-column/H1-H5 audit and eight controls" + }, + { + "command": "python3 -I -B research/r420-adjacent-a-seed00/independent_check.py", + "result": "PASS, 672 closed frames, all 1735 symbolic A replays, 328 dependency swaps change A's operator" + }, + { + "command": "python3 -I -O -B research/r420-adjacent-a-seed00/verify.py", + "result": "PASS with optimized Python 3.14.8" + }, + { + "command": "python3 -I -O -B research/r420-adjacent-a-seed00/independent_check.py", + "result": "PASS with optimized Python 3.14.8" + }, + { + "command": "python3.11 -I -B research/r420-adjacent-a-seed00/verify.py", + "result": "PASS on Python 3.11.15" + }, + { + "command": "python3.11 -I -B research/r420-adjacent-a-seed00/independent_check.py", + "result": "PASS on Python 3.11.15" + }, + { + "command": "python3 -B scripts/verify_selected_result.py", + "result": "PASS selected record, exact kappa, original source inventory and proof supplement" + } + ], + "provenance_checks": { + "PR543_word_git_blob": "0c63ca62759dc63d302be6552aeeee1ede70350f", + "PR543_xcheck_git_blob": "fbff8607e4c61e18481f696b99dd38a32444e90d", + "result": "Local git hash-object results matched GitHub contents metadata at PR543 head 2065fe4f72a914d907f1046603f5a36f17018535" + }, + "independent_review": "A separate Codex worker wrote the second checker without importing verify.py, then reviewed the main checker, proof, boundary accounting and scope; no blocking finding.", + "overlap_refresh": { + "open_prs_examined": 528, + "latest_pr": 709, + "main_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "finding": "No duplicate of this single adjacent A-record exchange class. #661 fixes B order; #691/#694/#708 resynthesize circuits or change helper basis; #707/#709 are tooling. These are not excluded by this bound." + }, + "not_run": [ + "Repository-wide make verify, which regenerates unrelated historical constructions", + "Full frontier626-verify cold replay; the selected construction and its assembly are unchanged", + "Remote Linux CI or Lean formalization" + ], + "scope": "One adjacent transposition in the original pinned word with jointly chosen rational frames and fixed surrounding constraints. No repeated-swap or full multiplication theorem claim." +} diff --git a/research/r420-adjacent-a-seed00/independent_check.py b/research/r420-adjacent-a-seed00/independent_check.py new file mode 100644 index 0000000000..794e89c484 --- /dev/null +++ b/research/r420-adjacent-a-seed00/independent_check.py @@ -0,0 +1,166 @@ +#!/usr/bin/env python3 +"""Independent exact check of R420 adjacent A-gate frame rigidity. Apache-2.0. + +Uses Fraction elimination, closed-root sets and full symbolic A replays. +Imports no other project checker. +Prepared for Sagar Thakrar with substantial OpenAI Codex assistance. +""" + +import gzip +import hashlib +import json +from collections import Counter +from fractions import Fraction +from pathlib import Path + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def echelon(rows): + basis = {} + for row in rows: + row = list(map(Fraction, row)) + for pivot in sorted(basis): + scale = row[pivot] + if scale: + row = [a - scale * b for a, b in zip(row, basis[pivot])] + pivot = next((j for j, value in enumerate(row) if value), None) + if pivot is not None: + scale = row[pivot] + basis[pivot] = [value / scale for value in row] + return basis + + +def inside(row, basis): + row = list(map(Fraction, row)) + for pivot in sorted(basis): + scale = row[pivot] + if scale: + row = [a - scale * b for a, b in zip(row, basis[pivot])] + return not any(row) + + +def orthogonal(basis, dimension): + result = [] + for free in range(dimension): + if free in basis: + continue + vector = [Fraction(int(j == free)) for j in range(dimension)] + for pivot in sorted(basis, reverse=True): + vector[pivot] = -sum( + basis[pivot][j] * vector[j] for j in range(pivot + 1, dimension) + ) + result.append(vector) + return result + + +def main(): + path = Path(__file__).resolve().parents[1] / "e8-bit-r420/data/bitE8mut-r420.json.gz" + raw = path.read_bytes() + require( + hashlib.sha256(raw).hexdigest() + == "9721a3819efd68307f66f00d84a952eb28eb7c3ad2ce79653ce295c98a764784", + "source word SHA256 differs from pinned PR543 R420 word", + ) + word = json.loads(gzip.decompress(raw)) + gates = word["A"] + frames = list(map(frozenset, word["frames"])) + lines = word["lines"] + dimension = word["h"] + bases = [echelon(lines[line] for line in frame) for frame in frames] + ranks = list(map(len, bases)) + perpendiculars = [orthogonal(basis, dimension) for basis in bases] + require(len(set(frames)) == len(frames), "duplicate catalogue frames") + for index, frame in enumerate(frames): + closure = frozenset(j for j, line in enumerate(lines) if inside(line, bases[index])) + require(closure == frame, f"frame {index} is not closed") + require( + all(sum(a * b for a, b in zip(row, normal)) == 0 + for row in bases[index].values() for normal in perpendiculars[index]), + f"frame {index} has an invalid orthogonal basis", + ) + require( + len(echelon(perpendiculars[index])) + ranks[index] == dimension, + f"frame {index} has an incomplete orthogonal basis", + ) + + operands = [set([destination] + sources) for _, destination, sources in gates] + before = [] + current = word["start"][:] + for gate, registers in zip(gates, operands): + before.append(current[:]) + for register in registers: + current[register] = gate[0] + end = current[:] + after = [] + current = end[:] + for gate, registers in zip(reversed(gates), reversed(operands)): + after.append(current[:]) + for register in registers: + current[register] = gate[0] + after.reverse() + + def replay(sequence, check_frames=True): + values = [1 << register for register in range(len(word["start"]))] + current = word["start"][:] + jumps = Counter() + for frame, destination, sources in sequence: + if check_frames: + for register in [destination] + sources: + old = current[register] + if old != frame: + require(frames[old] < frames[frame] and ranks[old] < ranks[frame], + f"illegal ascent for register {register}: {old} to {frame}") + jumps[ranks[frame] - ranks[old]] += 1 + current[register] = frame + for source in sources: + values[destination] ^= values[source] + return values, current, jumps + + baseline = replay(gates) + census = Counter() + commuting = rejected = same_destination = 0 + for index in range(len(gates) - 1): + left, right = gates[index:index + 2] + swapped = gates[:index] + [right, left] + gates[index + 2:] + if left[1] in right[2] or right[1] in left[2]: + require(replay(swapped, check_frames=False)[0] != baseline[0], + f"dependency negative control {index} did not change the symbolic map") + rejected += 1 + continue + commuting += 1 + same_destination += left[1] == right[1] + for gate_index in (index, index + 1): + registers = operands[gate_index] + lower = set().union(*(frames[before[index][r]] for r in registers)) + upper_ids = [after[index + 1][r] for r in registers] + low_rank = len(echelon(lines[line] for line in lower)) + upper_rank = dimension - len(echelon( + vector for frame in upper_ids for vector in perpendiculars[frame] + )) + original = gates[gate_index][0] + require(lower <= frames[original] + and all(frames[original] <= frames[frame] for frame in upper_ids), + f"original frame not between pair {index} gate {gate_index} boundaries") + require(low_rank == upper_rank == ranks[original], + f"pair {index} gate {gate_index} has subspace freedom") + census[low_rank] += 1 + require(replay(swapped) == baseline, + f"pair {index} changed the A map, boundary frames or rank-jump histogram") + + require((commuting, rejected, same_destination) == (1735, 328, 726), + "adjacent-pair census changed") + require(census == {1: 479, 2: 360, 4: 2140, 6: 480, 8: 11}, + "forced-frame dimension census changed") + require(baseline[2] == {1: 600, 2: 989, 4: 60}, "A rank-jump histogram changed") + print("PASS independent exact check: 672 closed frames; 1735 rigid commuting pairs;") + print("1735 equal symbolic maps, A-end frames and histograms; 328 dependency controls rejected.") + print("Forced-frame rank census:", json.dumps(dict(sorted(census.items())))) + print("A rank-jump histogram:", json.dumps(dict(sorted(baseline[2].items())))) + + +if __name__ == "__main__": + main() diff --git a/research/r420-adjacent-a-seed00/verify.py b/research/r420-adjacent-a-seed00/verify.py new file mode 100644 index 0000000000..f54169b640 --- /dev/null +++ b/research/r420-adjacent-a-seed00/verify.py @@ -0,0 +1,233 @@ +#!/usr/bin/env python3 +"""Exact R420 adjacent A-gate frame rigidity. Apache-2.0. + +Prepared for Sagar Thakrar with substantial OpenAI Codex assistance. +The predecessor word and its full audit are eumemic's PR543 contribution. +""" +import copy +import gzip +import hashlib +import importlib.util +import json +import sys +from collections import Counter +from fractions import Fraction +from functools import lru_cache +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +WORD = "research/e8-bit-r420/data/bitE8mut-r420.json.gz" + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def canonical(value): + return json.dumps(value, sort_keys=True, separators=(",", ":")).encode() + + +def basis(rows): + """Exact row-echelon basis in Q^8, indexed by leading coordinate.""" + out = {} + for vector in rows: + row = list(map(Fraction, vector)) + for col, pivot in sorted(out.items()): + multiple = row[col] + row = [a - multiple * b for a, b in zip(row, pivot)] + col = next((i for i, x in enumerate(row) if x), None) + if col is not None: + divisor = row[col] + out[col] = tuple(x / divisor for x in row) + return out + + +def perpendicular(rows): + pivots = basis(rows) + out = [] + for free in range(8): + if free in pivots: + continue + row = [Fraction(0)] * 8 + row[free] = 1 + for col in sorted(pivots, reverse=True): + row[col] = -sum(pivots[col][j] * row[j] for j in range(col + 1, 8)) + out.append(tuple(row)) + return out + + +def operands(gate): + return {gate[1], *gate[2]} + + +def commute(a, b): + return a[1] not in b[2] and b[1] not in a[2] + + +def boundaries(word): + current = word["start"][:] + for frame, target, sources in word["D"]: + for reg in {target, *sources}: + current[reg] = frame + before = [] + for gate in word["A"]: + before.append(current[:]) + for reg in operands(gate): + current[reg] = gate[0] + after = [None] * len(word["A"]) + for i in reversed(range(len(word["A"]))): + after[i] = current[:] + for reg in operands(word["A"][i]): + current[reg] = word["A"][i][0] + return before, after + + +def paid(word, masks, dims): + current = word["start"][:] + histogram = Counter() + + def climb(reg, frame): + old = current[reg] + need(not masks[old] & ~masks[frame], "illegal frame descent") + delta = dims[frame] - dims[old] + if delta: + histogram[delta] += 1 + current[reg] = frame + + for section in "DABC": + for gate in word[section]: + for reg in operands(gate): + climb(reg, gate[0]) + if section == "A": + histogram.update(dims[current[reg]] for reg in word["ret"]) + for reg, frame in enumerate(word["final"]): + climb(reg, frame) + need(0 not in histogram, "zero-rank copy") + return dict(sorted(histogram.items())) + + +def mirror_cleanup(word): + full = next(i for i, f in enumerate(word["frames"]) if len(f) == word["v"]) + z = [g for g in word["A"] + word["B"] + if not word["v"] <= g[1] < 2 * word["v"]] + word["C"] = [[full, t, list(ss)] for _, t, ss in reversed(z)] + + +def controls(word, audit, masks, dims, baseline): + # These planes meet in a line absent from the supplied list of root lines. + e = [tuple(int(i == j) for j in range(8)) for i in range(8)] + u = [e[0], e[1]] + v = [tuple(a + b for a, b in zip(e[0], e[2])), + tuple(a + b for a, b in zip(e[1], e[2]))] + need(8 - len(basis(perpendicular(u) + perpendicular(v))) == 1, + "lost non-root intersection") + need(len(basis([e[0]])) < 8 - len(basis(perpendicular(u))), + "control must expose a flexible, nonrigid interval") + need(not commute([0, 1, [0]], [0, 2, [1]]), "dependency control") + need(commute([0, 2, [0]], [0, 2, [1]]), "same-destination control") + + def rejected(candidate, message): + try: + checked = audit.check(candidate) + except audit.Reject: + return + need(not all(checked[3].values()) or not all(checked[4].values()), message) + + changed = copy.deepcopy(word) + changed["A"][0], changed["A"][1] = changed["A"][1], changed["A"][0] + rejected(changed, "unmirrored cleanup accepted") + mirror_cleanup(changed) + result = audit.check(changed) + need(all(result[3].values()) and all(result[4].values()), "legal mirrored swap rejected") + need(paid(changed, masks, dims) == baseline, "mirrored swap changed full price") + + bad = copy.deepcopy(word) + bad["A"][240], bad["A"][241] = bad["A"][241], bad["A"][240] + mirror_cleanup(bad) + rejected(bad, "noncommuting swap accepted") + bad = copy.deepcopy(word) + bad["A"][0][0] = 3 # Wrong line, with the same rank as frame 2. + rejected(bad, "equal-rank wrong subspace accepted") + return 8 + + +def verify(): + sources = json.loads((HERE / "SOURCES.json").read_text()) + for path, expected in sources["inputs_sha256"].items(): + need(hashlib.sha256((ROOT / path).read_bytes()).hexdigest() == expected, + "source pin mismatch: " + path) + word = json.loads(gzip.decompress((ROOT / WORD).read_bytes())) + spec = importlib.util.spec_from_file_location("r420_audit", ROOT / "research/e8-bit-r420/code/xcheck.py") + audit = importlib.util.module_from_spec(spec) + spec.loader.exec_module(audit) + checked = audit.check(word) + need(all(checked[3].values()) and all(checked[4].values()), "baseline interface failed") + frames = [tuple(basis(word["lines"][i] for i in frame).values()) for frame in word["frames"]] + normals = [perpendicular(frame) for frame in frames] + dims = [len(frame) for frame in frames] + masks = [sum(1 << i for i in frame) for frame in word["frames"]] + before, after = boundaries(word) + + @lru_cache(None) + def lower_rank(ids): + return len(basis(row for f in ids for row in frames[f])) + + @lru_cache(None) + def upper_rank(ids): + return 8 - len(basis(row for f in ids for row in normals[f])) + + counts = Counter() + census = Counter() + rows = [] + for i, (a, b) in enumerate(zip(word["A"], word["A"][1:])): + if not commute(a, b): + counts["noncommuting"] += 1 + continue + counts["commuting"] += 1 + counts["same_destination"] += int(a[1] == b[1]) + witnesses = [] + for gate in (a, b): + pre = tuple(sorted({before[i][r] for r in operands(gate)})) + post = tuple(sorted({after[i + 1][r] for r in operands(gate)})) + frame = gate[0] + need(all(not masks[f] & ~masks[frame] for f in pre), "lower containment") + need(all(not masks[frame] & ~masks[f] for f in post), "upper containment") + low, high = lower_rank(pre), upper_rank(post) + need(low == dims[frame] == high, "frame freedom at pair %d" % i) + census[low] += 1 + witnesses.append([frame, list(pre), list(post), low, high]) + # Only shared operands could reverse their frame path when the gates swap. + need(not operands(a) & operands(b) or masks[a[0]] == masks[b[0]], + "swapped pair descends") + rows.append([i, witnesses]) + + histogram = paid(word, masks, dims) + expected = json.loads((ROOT / "research/e8-bit-r420/EXPECTED.json").read_text()) + need(histogram == {int(k): v for k, v in expected["word"]["local_histogram"].items()}, + "full paid profile mismatch") + control_count = controls(word, audit, masks, dims, histogram) + return { + "status": "PASS_R420_ADJACENT_A_RIGIDITY", + "positions": len(word["A"]) - 1, + "counts": dict(sorted(counts.items())), + "forced_gate_occurrences": sum(census.values()), + "forced_dimension_census": dict(sorted(census.items())), + "rational_frame_gaps": 0, + "witness_rows_sha256": hashlib.sha256(canonical(rows)).hexdigest(), + "full_local_paid_profile": histogram, + "rank_mass": sum(k * v for k, v in histogram.items()), + "controls": control_count, + } + + +if __name__ == "__main__": + result = verify() + if sys.argv[1:] == ["--print-certificate"]: + print(json.dumps(result, indent=2, sort_keys=True)) + else: + need(not sys.argv[1:], "usage: verify.py [--print-certificate]") + expected = json.loads((HERE / "CERTIFICATE.json").read_text()) + need(json.loads(canonical(result)) == expected, "certificate mismatch") + print("PASS_R420_ADJACENT_A_RIGIDITY positions=2063 commuting=1735 forced=3470 gaps=0 rank_mass=5112 controls=8") From ebd567a22d26fadc1c8292b5c57056fb52331266 Mon Sep 17 00:00:00 2001 From: Sagar Thakrar Date: Tue, 13 Oct 2026 10:09:13 +0530 Subject: [PATCH 2/2] docs: complete sprint claim with research result and PR link --- research/r420-adjacent-a-seed00/CLAIM.json | 6 +++++- research/r420-adjacent-a-seed00/README.md | 2 +- research/r420-adjacent-a-seed00/verify.py | 2 +- 3 files changed, 7 insertions(+), 3 deletions(-) diff --git a/research/r420-adjacent-a-seed00/CLAIM.json b/research/r420-adjacent-a-seed00/CLAIM.json index 13b2a5daae..f5a28641e7 100644 --- a/research/r420-adjacent-a-seed00/CLAIM.json +++ b/research/r420-adjacent-a-seed00/CLAIM.json @@ -14,5 +14,9 @@ "R420 decoder/COPY-cost change" ], "overlap": "PR661 fixes B gate order. PR589 single-operation transport on P111 differs in word and simultaneous search class. PR691 changes a quad circuit; PR694 changes helper basis. This task preserves each original A gate and its sources.", - "status": "claimed locally" + "status": "completed: scoped negative result", + "result": "All 1735 commuting adjacent A-gate pairs have both frames forced by exact lower-span/upper-intersection equality over Q. All 3470 gate-occurrences checked; no local paid-profile improvement in this single-exchange class. Independent full A replays agree; all 328 dependency swaps change the operator.", + "pull_request": "https://github.com/CrocSwap/integer-mult-bounds/pull/711", + "completed_utc": "2026-10-13T04:38:46Z", + "final_overlap_check": "528 open PRs through #709 inspected before submission; later arrivals #708 and #709 change decoder circuits or tooling, not this fixed-gate search class. Main remained the exact base." } diff --git a/research/r420-adjacent-a-seed00/README.md b/research/r420-adjacent-a-seed00/README.md index c2893773df..81f6418688 100644 --- a/research/r420-adjacent-a-seed00/README.md +++ b/research/r420-adjacent-a-seed00/README.md @@ -181,7 +181,7 @@ remains in the predecessor's notices. `SOURCES.json` records exact input pins, the selected context and related PR heads; context hashes are historical and are not enforced as runtime dependencies. -Contribution by Sagar Thakrar / `thakrarsagar`, with substantial OpenAI Codex +Contribution by `thakrarsagar`, with substantial OpenAI Codex assistance for the experiment, proof, implementation, independent second implementation and review. New work is under the repository's Apache-2.0 license; predecessor notices and source files are unchanged. diff --git a/research/r420-adjacent-a-seed00/verify.py b/research/r420-adjacent-a-seed00/verify.py index f54169b640..016cb99b2e 100644 --- a/research/r420-adjacent-a-seed00/verify.py +++ b/research/r420-adjacent-a-seed00/verify.py @@ -1,7 +1,7 @@ #!/usr/bin/env python3 """Exact R420 adjacent A-gate frame rigidity. Apache-2.0. -Prepared for Sagar Thakrar with substantial OpenAI Codex assistance. +Prepared for GitHub contributor thakrarsagar with substantial OpenAI Codex assistance. The predecessor word and its full audit are eumemic's PR543 contribution. """ import copy