diff --git a/research/rank1-center-delta-seeddfc2/CERTIFICATE.json b/research/rank1-center-delta-seeddfc2/CERTIFICATE.json new file mode 100644 index 0000000000..9d96cbebdd --- /dev/null +++ b/research/rank1-center-delta-seeddfc2/CERTIFICATE.json @@ -0,0 +1,140 @@ +{ + "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea", + "dirty_state_replay": { + "all_match_direct_map": true, + "field_domain": "x,y,p,q,scratch independently range over F2^2", + "inputs_and_scratch_preserved": true, + "states_checked": 1024, + "target_update_is_involution": true + }, + "general_rank_one_extension": { + "assumption": "The rank model charges bilinear products; linear output coefficient vectors are part of each tensor atom. Frame changes, copying, precision, hosting and restoration are outside this local lemma.", + "saving_when_r_at_least_2": "at least r-1 children in the common-frame bilinear-rank model", + "statement": "If F and F+H each have bilinear rank r in one common frame, and H(x,y)=alpha(x)*beta(y)*c has rank one, then the paired dirty-target map (p,q)->(p+F,q+F+H) has rank at most r+1, versus separate rank 2r." + }, + "joint_rank_certificate": { + "child_count_saved": 1, + "flattening_rank_lower_bound": 3, + "independent_center_ranks": [ + 2, + 2 + ], + "input_monomial_order": [ + "x0*y0", + "x0*y1", + "x1*y0", + "x1*y1" + ], + "joint_rank": 3, + "output_slices": [ + "p0:E00", + "p1:E11", + "q0:E00+E01", + "q1:E11+E01" + ], + "rank_one_atoms": [ + { + "output_vector_(p0,p1,q0,q1)": [ + 1, + 0, + 1, + 0 + ], + "product": "x0*y0" + }, + { + "output_vector_(p0,p1,q0,q1)": [ + 0, + 1, + 0, + 1 + ], + "product": "x1*y1" + }, + { + "output_vector_(p0,p1,q0,q1)": [ + 0, + 0, + 1, + 1 + ], + "product": "x0*y1" + } + ] + }, + "limitations": [ + "No eligible occurrence is identified in the selected supplier.", + "No E8 frame, source/target hosting, recursive precision, or restoration integration is instantiated.", + "The all-pairs profile is a favorable sensitivity screen, not an admitted paid-word change." + ], + "maps": { + "F0": [ + "x0*y0", + "x1*y1" + ], + "F1": [ + "x0*y0 + x0*y1", + "x1*y1 + x0*y1" + ], + "difference": [ + "x0*y1", + "x0*y1" + ], + "joint_update": "(p,q) -> (p+F0(x,y), q+F1(x,y)) over F2" + }, + "negative_controls": { + "omitted_rank_one_correction": "rejected by x=01,y=10,p=q=00,scratch=11", + "omitted_second_output_coefficient": "rejected by same witness" + }, + "optimistic_selected_profile_screen": { + "assumption": "All 72 two-call pairs are eligible; no source/frame/hosting/precision/restoration overhead beyond the rank-one correction.", + "candidate_center_per_call": 32, + "candidate_fixed_word_a_cap": [ + "50198000463/15625000000000", + "3212672029633/1000000000000000" + ], + "candidate_profile_per_call": { + "1": "4825/2", + "2": 418, + "3": 432, + "4": 142, + "5": 82, + "8": 4 + }, + "candidate_relaxation_at_1_over_99": [ + "29535762929197842580139084756942546247213159665611190253617762246073046446723/28948022309329048855892746252171976963317496166410141009864396001978282409984", + "59071525858395685160278169513885092494426319331222380507235524492146092893467/57896044618658097711785492504343953926634992332820282019728792003956564819968" + ], + "families": 896, + "m": 73, + "rank_mass_saved_per_pair": 63, + "reaches_1_over_99": false, + "selected_center_per_call": 64, + "selected_fixed_word_a_cap": [ + "52814190909/31250000000000", + "1690054109089/1000000000000000" + ], + "selected_profile_per_call": { + "1": 2412, + "2": 418, + "3": 432, + "4": 142, + "5": 82, + "8": 8 + }, + "stages": 9, + "supplier_or_kappa_claim": false + }, + "scope": "Two explicit F2^2 bilinear centers with a rank-one difference; arbitrary dirty output panels and untouched scratch. No selected occurrence or kappa claim.", + "selected_record_sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32", + "source_sha256": { + "certificates/selected-result.json": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32", + "docs/research/agent-task-catalog.json": "6686ad58f1fbdbc87134a78901b60fd53a20d3984355e91defbbebc9e9fa8075", + "docs/research/community-batch1099-review.md": "7e76d2c38e5fce30587835b7251df1430488ae4dd372611ef69a3f03f476b6cb", + "research/community-frontier1094-audit/ASSEMBLY.json": "1122cb3a575f8c788345fc1bf4c108ac7c3250fb81a5988671f5eb04b3ab3045", + "research/community-frontier1094-audit/SELECTED-SOURCE.json": "79b3de5db3dbcb9829789ba58e9e45758926031e2a7d80667a08429d369be53b", + "research/complex-local-word-ceiling/RESULT.json": "d91d6c46509875abf1f61de67c2609656d3dc685451299f83caa6f922493692d", + "research/complex-local-word-ceiling/ceiling.py": "86a1432870b3b21d8454106ec9162fddc0471472d9214c590a1420f2426cedfc" + }, + "status": "PASS_RANK1_CENTER_DELTA_EXACT_LOCAL_CONSTRUCTION" +} diff --git a/research/rank1-center-delta-seeddfc2/README.md b/research/rank1-center-delta-seeddfc2/README.md new file mode 100644 index 0000000000..10f60e2d10 --- /dev/null +++ b/research/rank1-center-delta-seeddfc2/README.md @@ -0,0 +1,88 @@ +# Rank-one difference between dirty-output centers + +**Result:** an exact local construction on two-bit sources. Two rank-two bilinear +centers whose difference has rank one admit a joint rank-three tensor. This saves +one rank-one child against separate evaluation while preserving arbitrary dirty +output panels and an untouched scratch panel. The claim is local to this map pair; +it does not identify a compatible pair in the selected supplier. + +## Scope and evidence + +This refines the `persistent-boundary` card to the explicit pair in +[TASK.json](TASK.json). The three products are `x0*y0`, `x1*y1`, and `x0*y1`, +with output coefficient vectors `(1,0,1,0)`, `(0,1,0,1)`, `(0,0,1,1)` in target +order `(p0,p1,q0,q1)`. The output-slice span has dimension three, so no two-atom +joint decomposition exists. Each center separately has rank two, making the +four-versus-three child comparison exact for this pair. + +The same construction gives a general local lemma: if `F` and `F+H` both have +bilinear rank `r` in a common frame, and `H(x,y)=alpha(x) beta(y) c` is one +rank-one tensor, the paired dirty-target map has rank at most `r+1`, versus +`2r` for separate evaluation. It saves at least `r-1` bilinear children for +`r >= 2` in this rank model. The output coefficient vectors are part of each +tensor atom; frame changes, copying, precision, hosting and restoration remain +outside the lemma and must be priced at a concrete occurrence. + +For the proof, write `F = sum_i alpha_i(x) beta_i(y) c_i`. Route each product +to the paired output vector `(c_i,c_i)`, then evaluate the single correction +product once with output vector `(0,c)`. This computes `(F,F+H)` with `r+1` +rank-one bilinear atoms. Applying the same atom updates to arbitrary dirty +target panels is legal because every update is XOR and therefore involutive. + +The verifier exhausts all 1,024 states with `x,y,p,q,scratch` independently in +`F2^2`, compares the atom circuit to the direct bilinear map, checks the target +update is an involution, and preserves both source inputs and scratch. Negative +controls omit the correction or one of its two output coefficients. The exact +receipt is [CERTIFICATE.json](CERTIFICATE.json); pinned source hashes and Git +blobs are in [SOURCES.json](SOURCES.json). + +The second result is only a favorable selected-profile screen. It assumes all 72 +candidate pairs exist and every cost outside the rank-one correction is zero. +The exact fixed-word ceiling improves from the selected upper bound +`1690054109089/10^15` to the interval in the certificate, but remains below the +`1/99` saving target. No supplier occurrence, frame realization, new `kappa`, or +frontier change is established. + +The focused package PR is [#1838](https://github.com/CrocSwap/integer-mult-bounds/pull/1838). +The claim and live coordination record are at +[Discussion #1166, comment 18922942](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-18922942). +Related work includes identical-center sharing (#1708, #1748, #1791), idle-axis +hosting (#1516), and restoration batching (#1155). The tested distinction is +the explicitly charged rank-one tensor difference. + +## Reproduce + +From the repository root, with the pinned source tree available: + +```sh +python3 -B research/rank1-center-delta-seeddfc2/verify.py +python3 scripts/research_package.py --package research/rank1-center-delta-seeddfc2 --check-only +python3.12 -B scripts/research_package.py --package research/rank1-center-delta-seeddfc2 +``` + +The verifier uses exact `F2` operations and rational ceiling intervals. It is +read-only. Python 3.12 is the repository's registered replay target; a local +Python 3.14 replay may be used when 3.12 is unavailable, with that limitation +reported separately. + +## Open next questions + +1. Does a pinned selected-supplier pair of same-source center tensors have an + exact rank-one difference? This determines whether the local child saving + can affect a paid profile. First step: extract one candidate pair's center + maps in a common source/output frame and compute the difference tensor. + Blocker: no occurrence is named or routed by this bounded prototype. +2. What is the native frame, copy rank, precision, and restoration cost of the + correction child at a real occurrence? These determine whether the abstract + one-child correction retains its cost advantage. First step: instantiate one + source-pinned occurrence and count every interface operation. Blocker: this + package contains no selected E8 frame realization. + +## Credit + +Prepared by Cinna / commdata2338 with substantial OpenAI Codex assistance. No +independent human review is claimed. Identical-center sharing is attributed to +the related work linked above; this package supplies a rank-one-difference +construction and exact dirty-state receipt. The selected profile and fixed-word +ceiling inputs are attributed to their pinned repository packages in +`SOURCES.json`. New work is Apache-2.0. diff --git a/research/rank1-center-delta-seeddfc2/SOURCES.json b/research/rank1-center-delta-seeddfc2/SOURCES.json new file mode 100644 index 0000000000..ad03a1f461 --- /dev/null +++ b/research/rank1-center-delta-seeddfc2/SOURCES.json @@ -0,0 +1,48 @@ +{ + "schema_version": 1, + "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "06c96f5579bb67ed1b86d334e78fbed7da6945f1", + "sha256": "6686ad58f1fbdbc87134a78901b60fd53a20d3984355e91defbbebc9e9fa8075" + }, + { + "path": "docs/research/community-batch1099-review.md", + "usage": "provenance", + "git_blob": "6cb6ec061a071a06a2d18cd4dc3e9a2b05d28099", + "sha256": "7e76d2c38e5fce30587835b7251df1430488ae4dd372611ef69a3f03f476b6cb" + }, + { + "path": "research/community-frontier1094-audit/ASSEMBLY.json", + "usage": "provenance", + "git_blob": "5fd676df060f3b450782fdf5ff5f6beb63a5eeb0", + "sha256": "1122cb3a575f8c788345fc1bf4c108ac7c3250fb81a5988671f5eb04b3ab3045" + }, + { + "path": "research/community-frontier1094-audit/SELECTED-SOURCE.json", + "usage": "provenance", + "git_blob": "6a75493790b4eff9c4a98051ef8b01d6aad0d5a8", + "sha256": "79b3de5db3dbcb9829789ba58e9e45758926031e2a7d80667a08429d369be53b" + }, + { + "path": "research/complex-local-word-ceiling/RESULT.json", + "usage": "input", + "git_blob": "77f55043a679dd722330f1e2499863e36376d9f9", + "sha256": "d91d6c46509875abf1f61de67c2609656d3dc685451299f83caa6f922493692d" + }, + { + "path": "research/complex-local-word-ceiling/ceiling.py", + "usage": "input", + "git_blob": "6c0f54527d879396f689523bfde19928a9b6157c", + "sha256": "86a1432870b3b21d8454106ec9162fddc0471472d9214c590a1420f2426cedfc" + } + ] +} diff --git a/research/rank1-center-delta-seeddfc2/TASK.json b/research/rank1-center-delta-seeddfc2/TASK.json new file mode 100644 index 0000000000..4a950da884 --- /dev/null +++ b/research/rank1-center-delta-seeddfc2/TASK.json @@ -0,0 +1,195 @@ +{ + "schema_version": 1, + "task_id": "persistent-boundary", + "scope_key": "026be4b6e61971d51838", + "seed": "dfc23508bf1e7396ebe28345f5c0b834", + "track": "recursive-interfaces", + "priority_revision": 3, + "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea", + "selected_record_sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32", + "discarded_draws": [ + { + "seed": "5a3b8aa97b5898f36de4fb89ce4679ae", + "track": "consolidation", + "reason": "excluded non-construction track" + } + ], + "original_card": { + "id": "persistent-boundary", + "question": "Can a specified pair of consecutive calls eliminate a restoration that the next call reconstructs?", + "starting_points": [ + "research/heterogeneous-owner-assembly/README.md", + "certificates/selected-result.json" + ], + "methods": [ + "Write typed entry/exit contracts and a contracting multitype recurrence.", + "Derive a lower bound for the compulsory transitions of one proposed typed interface." + ], + "acceptance_gate": "Show actual eliminated work and legal composition; changing a scalar recurrence into a matrix is insufficient.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Find a concrete consecutive-call boundary in the selected review and list its entry/exit obligations.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Specify two call types and one operation actually removed by composition; derive the normalized recurrence.", + "bottleneck_link": "Eliminating compulsory boundary work can lower recursive cost beyond packing gains.", + "allowed_variations": [ + "A two-type pilot or one explicit deferred restoration." + ], + "scope_change_triggers": [ + "Rewriting the old scalar recurrence as a matrix without eliminating work." + ], + "overlap_terms": [ + "persistent boundary", + "deferred restoration", + "multitype" + ] + }, + "scope_status": "refined", + "actual_scope": "Two dirty-output center computations share one common rank-2 bilinear center; the second center differs by one rank-one bilinear tensor. Construct the joint output map exactly and price the shared rank-2 child plus the rank-1 correction, then screen the corresponding all-pairs selected-profile upper envelope.", + "scope_change_reason": "The catalogue card is broad. This refinement changes the identical-center premise of current fanout constructions to a fixed rank-one tensor difference, while keeping the same arbitrary dirty source/target contract. The bounded object is one explicit two-bit bilinear pair and its complete recursive child-rank invoice; no selected call pair is assumed.", + "object": { + "source_inputs": "x,y in F2^2, arbitrary and read-only", + "outputs": "Two arbitrary dirty two-bit target panels p,q", + "first_center": [ + "x0*y0", + "x1*y1" + ], + "second_center": [ + "x0*y0 + x0*y1", + "x1*y1 + x0*y1" + ], + "difference": "(x0*y1, x0*y1), a rank-one bilinear tensor", + "question": "Can the shared first-center products plus one charged rank-one correction implement both panels with fewer recursive children while restoring every private interface?" + }, + "changed_assumption": "Allow the two center tensors to differ by one rank-one bilinear term instead of requiring identical centers.", + "method_domain": "Exact enumeration of every x,y,p,q in (F2^2)^4; explicit output-vector tensor decomposition; no optimizer or search over other maps.", + "overlap": { + "checked_utc": "2026-10-14T11:47:28Z", + "tool": "scripts/find_overlap.py --offline --json --limit 1000 'rank-one center perturbation' 'low-rank center difference' 'center tensor update' 'rank-one center correction' 'shared-center perturbation' 'tensor-difference fanout'", + "coverage": { + "open_prs": 492, + "discussions": 478, + "complete_pagination": true, + "warnings": [ + "PR snapshot fetched 2026-10-14T11:34:46Z and Discussions snapshot fetched 2026-10-14T11:37:27Z; complete cached pagination. A later full refresh stalled during discussion pagination. Targeted live PR and Discussion searches and direct reads of related PR heads completed at 11:47Z." + ] + }, + "related": [ + { + "pr": 1708, + "head": "4d163c04c0980c5b0e9092fbd5864c7cfadc125d", + "relation": "shared exact center across same-source panels; this scope pays a rank-one tensor difference" + }, + { + "pr": 1748, + "head": "ea14f191752c9901bf6684763534d2d248fb2ad2", + "relation": "backward shared-center return and precision guard; identical-center premise" + }, + { + "pr": 1791, + "head": "00d05a64898571cf57a14310fbcd3507ca99c5ec", + "relation": "prices center sharing overhead on selected profiles; no low-rank center-difference construction" + }, + { + "discussion": 1516, + "relation": "active claim to host center paths on idle coordinates; different mechanism" + }, + { + "pr": 1155, + "head": "d7d50406fbdc7ac4141ba454b2e2440dc74942db", + "relation": "general recursion-batch restoration coalescing; operator defect/composition question" + } + ], + "final_targeted_checks": { + "checked_utc": "2026-10-14T11:47:28Z", + "open_pr_searches": { + "\"rank-one center\"": [], + "\"low-rank center\"": [] + }, + "discussion_searches": { + "\"rank-one center\"": "one result, this task claim #1166 comment 18922942", + "\"low-rank center\"": [] + }, + "related_open_pr_heads": { + "1708": "4d163c04c0980c5b0e9092fbd5864c7cfadc125d", + "1748": "ea14f191752c9901bf6684763534d2d248fb2ad2", + "1791": "00d05a64898571cf57a14310fbcd3507ca99c5ec", + "1155": "d7d50406fbdc7ac4141ba454b2e2440dc74942db" + }, + "full_refresh": "Attempted at 2026-10-14T11:44Z; canceled after remaining blocked on GitHub discussion comment pagination. Used the complete cached census from 11:37Z plus these direct live searches." + } + }, + "optimistic_full_cost_screen": { + "selected_profile_per_call": { + "1": 2412, + "2": 418, + "3": 432, + "4": 142, + "5": 82, + "8": 8 + }, + "candidate_profile_per_call_if_all_72_pairs_eligible": { + "1": "4825/2", + "2": 418, + "3": 432, + "4": 142, + "5": 82, + "8": 4 + }, + "centre_per_call": 32, + "families": 896, + "stages": 9, + "m": 73, + "per_pair_baseline_center_children": { + "8": 16 + }, + "per_pair_candidate_center_children": { + "8": 8, + "1": 1 + }, + "rank_mass_saved_per_pair": 63, + "selected_fixed_word_a_upper": "1690054109089/1000000000000000", + "candidate_fixed_word_a_cap_lower": "50198000463/15625000000000", + "scope": "All 72 pairs favorable bound only. The rank-one difference child is fully counted; source/frame/output-pair availability and non-rank overhead are not established. The 1/99 primitive target remains above this cap.", + "candidate_fixed_word_a_interval": [ + "50198000463/15625000000000", + "3212672029633/1000000000000000" + ], + "candidate_reaches_1_over_99": false, + "screen_replay": "research/rank1-center-delta-seeddfc2/verify.py" + }, + "stop_rule": "Implement only the explicit two-bit dirty-state instance. Stop if any dirty-state control fails or if the exact charged profile does not beat the selected fixed-word ceiling. Do not search the selected word for eligible invocation pairs in this cycle.", + "bottleneck_link": "An exact rank-one difference between two centers could extend center sharing beyond identical map pairs while charging the correction as a rank-one child; this may create additional paid center-path savings if eligible same-source panels exist.", + "budget_minutes": 60, + "success_evidence": "Exact proof of the joint map, exhaustive dirty-state replay, negative controls, and a certified moment ceiling for the all-pairs optimistic profile; clearly state that no selected pair, hosting, or new kappa is established.", + "outcome": "completed", + "evidence": "Exact three-atom joint decomposition of the two specified F2^2 centers; output-slice flattening rank exactly 3, versus separate center ranks 2+2. Exhaustive reversible target-update replay over all 1,024 source, dirty-target, and scratch states passes; omitting the correction or either fanout coefficient is rejected. Pinned exact ceiling replay changes the favorable all-72-pair profile cap from selected upper 1690054109089/10^15 to [50198000463/15625000000000,3212672029633/10^15], still below 1/99. This is a local construction and sensitivity screen only; no eligible selected occurrence, native interface bill, supplier change, or kappa is established.", + "author": "commdata2338", + "ai_assistance": "Substantial OpenAI Codex assistance in mechanism formulation, exact verification, cost screening and package writing; no independent human review claimed.", + "open_questions": [ + { + "question": "Does the selected supplier contain an eligible pair of same-source center tensors whose difference has exact bilinear rank one?", + "why_it_matters": "Only a pinned occurrence can convert this local mechanism into a supplier-level profile change.", + "first_step": "Inspect a source-pinned pair of forward center phases and compute the exact tensor difference in the common source/output frames.", + "blocked_by": "No actual selected-call pair has been named or routed in this bounded prototype." + }, + { + "question": "What is the exact copy rank and native precision charge of the rank-one correction when its output direction is hosted in the selected frames?", + "why_it_matters": "The rank-one child may need extra ports, output copies, frame changes or restoration beyond the ideal one-child bill.", + "first_step": "Build one candidate correction in a pinned local frame and recount source, output and scratch interfaces.", + "blocked_by": "The finite F2 prototype does not instantiate the selected E8 frame or its native local word." + } + ], + "coordination": "Claim and finding are in Discussion #1166 comments 18922942 and 18923124. Focused PR #1838 is open at https://github.com/CrocSwap/integer-mult-bounds/pull/1838; initial submitted head f6dd3a43a6b026b085a77aa9acb06cbd6a2bcb52. PR checks were pending when checked at 2026-10-14T11:48Z.", + "submitted_pr": { + "number": 1838, + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1838", + "head_commit_at_submission": "f6dd3a43a6b026b085a77aa9acb06cbd6a2bcb52" + } +} diff --git a/research/rank1-center-delta-seeddfc2/VERIFY.json b/research/rank1-center-delta-seeddfc2/VERIFY.json new file mode 100644 index 0000000000..c4b6a7f758 --- /dev/null +++ b/research/rank1-center-delta-seeddfc2/VERIFY.json @@ -0,0 +1,22 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/complex-local-word-ceiling/RESULT.json", + "research/complex-local-word-ceiling/ceiling.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact rank-three decomposition and slice-span lower bound; exhaustive 1,024 dirty source/target/scratch states; involution and preservation; correction/fanout negative controls; replayed exact fixed-word ceiling interval and 1/99 obstruction. No selected occurrence or kappa claim." + } + ] +} diff --git a/research/rank1-center-delta-seeddfc2/verify.py b/research/rank1-center-delta-seeddfc2/verify.py new file mode 100644 index 0000000000..4347aaebeb --- /dev/null +++ b/research/rank1-center-delta-seeddfc2/verify.py @@ -0,0 +1,253 @@ +#!/usr/bin/env python3 +"""Exact two-bit rank-one center-difference construction and cost screen.""" + +from __future__ import annotations + +import hashlib +import importlib.util +import json +from fractions import Fraction as Q +from pathlib import Path +import sys + + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parents[1] + + +def need(condition: bool, message: str) -> None: + if not condition: + raise RuntimeError(message) + + +def source_bytes(path: str) -> bytes: + target = ROOT / path + need(target.is_file(), f"missing pinned source: {path}") + return target.read_bytes() + + +def check_source_pins() -> dict[str, str]: + inventory = json.loads((PACKAGE / "SOURCES.json").read_text(encoding="utf-8")) + need(inventory["base_commit"] == json.loads((PACKAGE / "TASK.json").read_text(encoding="utf-8"))["base_commit"], + "task/source base mismatch") + rows = {row["path"]: row for row in inventory["files"]} + inputs = [row for row in inventory["files"] if row["usage"] == "input"] + for row in inventory["files"]: + data = source_bytes(row["path"]) + need(hashlib.sha256(data).hexdigest() == row["sha256"], f"source SHA256 mismatch: {row['path']}") + need(inputs, "no live inputs are pinned") + return {row["path"]: row["sha256"] for row in rows.values()} + + +def bits2(value: int) -> tuple[int, int]: + return value & 1, (value >> 1) & 1 + + +def vector2(value: int) -> tuple[int, int]: + return bits2(value) + + +def xor2(left: int, right: tuple[int, int]) -> int: + return left ^ right[0] ^ (right[1] << 1) + + +def reference_update(x: int, y: int, p: int, q: int, scratch: int) -> tuple[int, int, int, int, int]: + x0, x1 = bits2(x) + y0, y1 = bits2(y) + f0 = (x0 * y0, x1 * y1) + correction = x0 * y1 + f1 = (f0[0] ^ correction, f0[1] ^ correction) + return x, y, xor2(p, f0), xor2(q, f1), scratch + + +def atom_update( + x: int, + y: int, + p: int, + q: int, + scratch: int, + include_delta: bool = True, + delta_q1: bool = True, +) -> tuple[int, int, int, int, int]: + """Apply atoms u=x0*y0, v=x1*y1, w=x0*y1 to dirty output panels.""" + x0, x1 = bits2(x) + y0, y1 = bits2(y) + u, v, w = x0 * y0, x1 * y1, x0 * y1 + p = xor2(p, (u, v)) + q0, q1 = bits2(q) + q0 ^= u + q1 ^= v + if include_delta: + q0 ^= w + if delta_q1: + q1 ^= w + return x, y, p, q0 | (q1 << 1), scratch + + +def gf2_rank(rows: list[int], columns: int) -> int: + pivot = 0 + rows = list(rows) + for col in range(columns): + found = next((r for r in range(pivot, len(rows)) if (rows[r] >> col) & 1), None) + if found is None: + continue + rows[pivot], rows[found] = rows[found], rows[pivot] + for r in range(len(rows)): + if r != pivot and ((rows[r] >> col) & 1): + rows[r] ^= rows[pivot] + pivot += 1 + if pivot == len(rows): + break + return pivot + + +def load_ceiling(): + path = ROOT / "research/complex-local-word-ceiling/ceiling.py" + spec = importlib.util.spec_from_file_location("pinned_local_word_ceiling", path) + need(spec is not None and spec.loader is not None, "cannot load pinned ceiling module") + module = importlib.util.module_from_spec(spec) + spec.loader.exec_module(module) + return module + + +def build_certificate() -> dict: + pins = check_source_pins() + task = json.loads((PACKAGE / "TASK.json").read_text(encoding="utf-8")) + selected = json.loads(source_bytes("research/complex-local-word-ceiling/RESULT.json")) + selected_record_sha = hashlib.sha256(source_bytes("certificates/selected-result.json")).hexdigest() + need(selected_record_sha == task["selected_record_sha256"], "selected-record hash differs from the task pin") + + # Slice rows use input monomial order (x0*y0, x0*y1, x1*y0, x1*y1). + slices = [0b0001, 0b1000, 0b0011, 0b1010] + slice_rank = gf2_rank(slices, 4) + need(slice_rank == 3, "joint slice-span flattening no longer has rank three") + + # Exhaust all 4^5 states: shared read-only inputs, two arbitrary dirty outputs, + # and arbitrary private scratch, then check exact action and restoration. + checked = 0 + for x in range(4): + for y in range(4): + for p in range(4): + for q in range(4): + for scratch in range(4): + state = (x, y, p, q, scratch) + got = atom_update(*state) + expected = reference_update(*state) + need(got == expected, f"decomposition mismatch at state {state}") + need(atom_update(*got) == state, f"target update is not an involution at {state}") + need(got[0] == x and got[1] == y and got[4] == scratch, + f"input or scratch changed at {state}") + checked += 1 + need(checked == 1024, "incomplete dirty-state domain") + + # Two load-bearing negative controls: the delta contributes to both q lanes. + witness = (1, 2, 0, 0, 3) # x0=y1=1, all other input bits zero. + expected_witness = reference_update(*witness) + omit_delta = atom_update(*witness, include_delta=False) + omit_q1 = atom_update(*witness, delta_q1=False) + need(expected_witness != omit_delta, "negative control failed to detect omitted correction") + need(expected_witness != omit_q1, "negative control failed to detect missing fanout coefficient") + + # A rank-r bilinear decomposition spans all output slices by at most r + # product matrices. The three independent slices therefore force r >= 3. + # The listed atoms attain r=3. Each separate center has slice-span rank 2, + # so independent evaluation costs 2+2=4 rank-one products. + need(gf2_rank([0b0001, 0b1000], 4) == 2, "first center rank control") + need(gf2_rank([0b0011, 0b1010], 4) == 2, "second center rank control") + + # Favorable all-72-pairs scenario from the selected profile. This is a + # sensitivity screen, not a witnessed word transformation. + ceiling = load_ceiling() + selected_profile = {int(r): int(n) for r, n in selected["selected"]["local_profile_per_call"].items()} + selected_cap = Q(selected["ceiling"]["a_ceiling"]) + need(selected_profile == {1: 2412, 2: 418, 3: 432, 4: 142, 5: 82, 8: 8}, + "selected profile differs from pinned result") + selected_replay_cap = ceiling.ceiling(selected_profile, 73, 896, 9, 64) + need(selected_replay_cap[1] == selected_cap, "pinned selected ceiling no longer replays") + + candidate_profile = {1: Q(4825, 2), 2: 418, 3: 432, 4: 142, 5: 82, 8: 4} + candidate_cap = ceiling.ceiling(candidate_profile, 73, 896, 9, 32) + at_target = ceiling.relax(candidate_profile, 73, 896, 9, 32, Q(1, 99)) + need(candidate_cap[0] > selected_cap, "favorable candidate profile does not improve the selected ceiling") + need(candidate_cap[1] < Q(1, 99), "screen incorrectly reaches the 1/99 target") + need(at_target[0] > 1, "target obstruction is not certified by the pinned relaxation") + need(sum(Q(n) * r for r, n in candidate_profile.items()) == Q(11109, 2), + "candidate paid local mass mismatch") + + return { + "status": "PASS_RANK1_CENTER_DELTA_EXACT_LOCAL_CONSTRUCTION", + "scope": "Two explicit F2^2 bilinear centers with a rank-one difference; arbitrary dirty output panels and untouched scratch. No selected occurrence or kappa claim.", + "selected_record_sha256": task["selected_record_sha256"], + "base_commit": task["base_commit"], + "source_sha256": pins, + "maps": { + "F0": ["x0*y0", "x1*y1"], + "F1": ["x0*y0 + x0*y1", "x1*y1 + x0*y1"], + "difference": ["x0*y1", "x0*y1"], + "joint_update": "(p,q) -> (p+F0(x,y), q+F1(x,y)) over F2", + }, + "general_rank_one_extension": { + "statement": "If F and F+H each have bilinear rank r in one common frame, and H(x,y)=alpha(x)*beta(y)*c has rank one, then the paired dirty-target map (p,q)->(p+F,q+F+H) has rank at most r+1, versus separate rank 2r.", + "saving_when_r_at_least_2": "at least r-1 children in the common-frame bilinear-rank model", + "assumption": "The rank model charges bilinear products; linear output coefficient vectors are part of each tensor atom. Frame changes, copying, precision, hosting and restoration are outside this local lemma.", + }, + "joint_rank_certificate": { + "input_monomial_order": ["x0*y0", "x0*y1", "x1*y0", "x1*y1"], + "output_slices": ["p0:E00", "p1:E11", "q0:E00+E01", "q1:E11+E01"], + "flattening_rank_lower_bound": slice_rank, + "rank_one_atoms": [ + {"product": "x0*y0", "output_vector_(p0,p1,q0,q1)": [1, 0, 1, 0]}, + {"product": "x1*y1", "output_vector_(p0,p1,q0,q1)": [0, 1, 0, 1]}, + {"product": "x0*y1", "output_vector_(p0,p1,q0,q1)": [0, 0, 1, 1]}, + ], + "joint_rank": 3, + "independent_center_ranks": [2, 2], + "child_count_saved": 1, + }, + "dirty_state_replay": { + "field_domain": "x,y,p,q,scratch independently range over F2^2", + "states_checked": checked, + "all_match_direct_map": True, + "target_update_is_involution": True, + "inputs_and_scratch_preserved": True, + }, + "negative_controls": { + "omitted_rank_one_correction": "rejected by x=01,y=10,p=q=00,scratch=11", + "omitted_second_output_coefficient": "rejected by same witness", + }, + "optimistic_selected_profile_screen": { + "assumption": "All 72 two-call pairs are eligible; no source/frame/hosting/precision/restoration overhead beyond the rank-one correction.", + "selected_profile_per_call": {str(r): n for r, n in selected_profile.items()}, + "candidate_profile_per_call": {str(r): str(n) if isinstance(n, Q) else n for r, n in candidate_profile.items()}, + "selected_center_per_call": 64, + "candidate_center_per_call": 32, + "families": 896, + "stages": 9, + "m": 73, + "rank_mass_saved_per_pair": 63, + "selected_fixed_word_a_cap": [str(v) for v in selected_replay_cap], + "candidate_fixed_word_a_cap": [str(v) for v in candidate_cap], + "candidate_relaxation_at_1_over_99": [str(v) for v in at_target], + "reaches_1_over_99": False, + "supplier_or_kappa_claim": False, + }, + "limitations": [ + "No eligible occurrence is identified in the selected supplier.", + "No E8 frame, source/target hosting, recursive precision, or restoration integration is instantiated.", + "The all-pairs profile is a favorable sensitivity screen, not an admitted paid-word change.", + ], + } + + +def main() -> None: + expected = build_certificate() + if "--emit-certificate" in sys.argv[1:]: + print(json.dumps(expected, indent=2, sort_keys=True)) + return + actual = json.loads((PACKAGE / "CERTIFICATE.json").read_text(encoding="utf-8")) + need(actual == expected, "certificate differs from exact replay") + print(f"PASS_RANK1_CENTER_DELTA_EXACT_LOCAL_CONSTRUCTION states={expected['dirty_state_replay']['states_checked']} rank=3/4") + + +if __name__ == "__main__": + main()