From 5d9b3d792358bc423fd64cf3a15c2f46dbf91a97 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Thu, 29 Oct 2026 22:19:58 +0000 Subject: [PATCH] feat(research): exclude unrestricted helper-572 seam recoding --- research/p104-unrestricted-572-seam/PROOF.md | 173 +++++++++++++ research/p104-unrestricted-572-seam/README.md | 118 +++++++++ .../p104-unrestricted-572-seam/SOURCES.json | 30 +++ research/p104-unrestricted-572-seam/TASK.json | 123 +++++++++ .../p104-unrestricted-572-seam/VERIFY.json | 36 +++ research/p104-unrestricted-572-seam/verify.py | 235 ++++++++++++++++++ 6 files changed, 715 insertions(+) create mode 100644 research/p104-unrestricted-572-seam/PROOF.md create mode 100644 research/p104-unrestricted-572-seam/README.md create mode 100644 research/p104-unrestricted-572-seam/SOURCES.json create mode 100644 research/p104-unrestricted-572-seam/TASK.json create mode 100644 research/p104-unrestricted-572-seam/VERIFY.json create mode 100644 research/p104-unrestricted-572-seam/verify.py diff --git a/research/p104-unrestricted-572-seam/PROOF.md b/research/p104-unrestricted-572-seam/PROOF.md new file mode 100644 index 0000000000..03795ffa98 --- /dev/null +++ b/research/p104-unrestricted-572-seam/PROOF.md @@ -0,0 +1,173 @@ +# Arbitrary linear recoding cannot repair the frozen helper-572 seam + +This scoped proof was produced by Nick Petalas. All scalars are rational. +The finite certificate establishes the boundary facts below from the pinned +selected PR6030 word. It does not replay a predecessor's exclusion theorem. + +## 1. Contract + +Keep the original word, its public inputs, frames, owned lifetimes and event +order. Event indices are zero based; a window is immediately after its event. +After event 13637, `COPY 778 <- 572` in chart 595, overwrite field 572 with a +new independent scalar input z. Every original public input remains arbitrary. + +Allow any finite number of homogeneous linear operations, with arbitrary +rational coefficients, within these banks: + +- Chart 595 after events 13637 through 13651, on fields + `(127,572,581,582,731,778)`. +- Chart 603 after event 13652 or 13654, on `(572,740)`, and after event 13655, + on `(572,709,740)`. + +Operations may change original-input rows temporarily. They need not preserve +an original-zero carrier. No extra field, new MOVE or changed prefix/suffix is +permitted. We grant arbitrary linear bank maps, including singular ones, so the +exclusion also covers ADD/SCALE programs of unbounded finite length in these +regions. COPY or erasure within the granted banks cannot evade it. + +Put V equal to field 572's original final chart, 127. The necessary condition is +that every public output whose original final chart differs from V equal its +original unsplit value, on all original inputs and z. There are 186 such outputs. +The desired additional target would require nonzero public dependence on z. + +**Theorem.** Under this contract, satisfying the protected-output condition +forces every final public output to have zero z coefficient. Thus no nonzero +independent target can be supplied by these corrections, regardless of their +number or coefficients. + +## 2. Collapse the chronology to two matrices + +The first bank remains exactly the six listed fields through event 13651. +All intervening operations in other charts are unaffected. Absorb the retained +`582 += 2*731` and every allowed first-bank operation into one arbitrary 6 by 6 +map A at the first bank's exit. + +At event 13652, only field 572 moves from chart 595 to 603. Field 740 is already +there. The retained `740 -= 572` at event 13654 and every allowed operation on +these two fields are linear. Field 709 enters from chart 597 at event 13655; +its value has not been changed by any allowed operation. Extend the earlier +2 by 2 maps by the identity on that entering field and absorb them with the +last operations into one arbitrary 3 by 3 map B. + +Consequently only one scalar form r from the first bank reaches the second. +The second bank's three values are linear combinations of `(r,h,k)`, where h +and k are the original cut values of fields 740 and 709. Five first-bank fields +remain in chart 595. CLEAR 778 immediately follows, at event 13656. + +This is a relaxation: arbitrary A and B need not be realizable by reversible +scalar gates. Proving failure in this larger class suffices. + +## 3. The exact source and suffix certificates + +Let u be the eight-component vector of cut forms in this order: + +```text +u = (old127, z, old581, old582, old731, ell, h, k), +ell = old572 = old778 after the retained COPY. +``` + +These eight forms are linearly independent in the original 770 inputs and z. +The exact minor on input columns +`(0,2,34,572,581,582,740,770)` has determinant `1/32`; column 770 denotes z. +The verifier derives the forms from the prefix and checks this determinant +by the Leibniz formula, separately from its pivot selection. + +Use the following order for state differences immediately after event 13655: + +```text +(127,581,582,731,778,572,740,709). +``` + +Propagating their eight unit perturbations through the unchanged suffix shows: + +1. The perturbation on 778 reaches no final public output. +2. The perturbation on 740 reaches only final public output 740, with coefficient 1. +3. Output 740 is V-final. The six outputs below are protected. + +After deleting columns 778 and 740, the suffix rows on protected outputs +`(116,120,127,134,138,176)` are exactly + +```text + 127 581 582 731 572 709 +116 0 1 0 2 0 0 +120 0 0 0 0 -1 2 +127 1 0 0 0 0 0 +134 0 0 0 -2 0 0 +138 0 0 0 0 -1 -2 +176 0 0 -1 0 0 0 +``` + +Its determinant is 8. Therefore preserving these six outputs alone forces the +six corresponding state forms `(127,581,582,731,572,709)` to equal their original +unsplit forms. This deduction is an identity in all original input columns and +z, not just a statement about the new input's leakage. + +For completeness, the original eight post-seam state forms are, in the same +order as the eight state differences, + +```text +(old127, old581, old582+2*old731, old731, ell, ell, h-ell, k). +``` + +The verifier checks every coefficient of these identities against the prefix. +It also checks the two exceptional suffix columns at every public output. +Together the two nonzero minors and these identities are a finite certificate +of all source-specific premises used in the argument. + +## 4. The single-channel obstruction + +Write the transmitted form as `r = a*u_first`, where `u_first` consists of the +first six entries of u. Since second-bank values are B applied to `(r,h,k)`, +there are rational coefficients d,e,f with + +```text +post572 = d*r + e*h + f*k. +``` + +Section 3 forces `post572 = ell`. Independence of u therefore gives + +```text +d*a = (0,0,0,0,0,1), e=f=0. +``` + +The right side is nonzero, so d is nonzero. Thus a is a scalar multiple of the +ell coordinate vector. In particular r has zero z coefficient. Neither h nor +k contains z, so no second-bank field can contain z, including field 740. + +The other four non-erased first-bank forms are forced to their original values +by the same minor and hence contain no z. The remaining first-bank field, 778, +has identically zero public suffix response. Every other state field is +unchanged by the allowed corrections. Therefore every final public z +coefficient vanishes, proving the theorem. + +Equivalently, the second stage's first-six-input coefficient block has rank at most one. +It must contain the ell row; a nonzero z coordinate in its 740 row would raise +its rank to at least two. A second independent transported scalar could change +that conclusion. No price or physical realization for such a transport is +asserted here. + +## 5. What is new and what remains + +JoyboyBrian's PR6088 excludes two added ADDs in these regions by inconsistent +endpoint equations. The present result removes the scalar-operation-count +bound and permits arbitrary linear bank recoding. It uses a protected-output +minor and a one-channel factorization rather than the predecessor's pair +census or bilinear relaxation. The predecessor's counts are not rerun. + +The carrier-only theorems of apoursh PR6067 and Jonathan Capalbo PR6069 require +original-zero correction sources. This proof permits original-input changes. +JosieElliston PR6108 distinguishes the remaining cross-time problem and supplies +a different scalar witness on PR5907. Nick Petalas PR6040 is the earlier +unit-injection census, not an arbitrary-input recoding theorem. + +The exclusion fixes the overwrite, these two chart regions and all later +original events. Later correction windows, a pre-cut save, a second transported +form, changed routes or storage, nonlinear encodings, and another word are +outside scope. There is no physical/native supplier, productive normalization, +complete signed invoice, compiler/precision/caller/outer proof, new kappa or +complete multiplication theorem. The five selected framework assumptions +remain. Independent human and formal proof-kernel review are unclaimed. + +Credit JoyboyBrian, apoursh, Jonathan Capalbo, JosieElliston, Matarener, +flyingviper, Ali Romman, DreamingOfClouds and the retained P104 lineage. +Apache-2.0. diff --git a/research/p104-unrestricted-572-seam/README.md b/research/p104-unrestricted-572-seam/README.md new file mode 100644 index 0000000000..aa0a8aadb4 --- /dev/null +++ b/research/p104-unrestricted-572-seam/README.md @@ -0,0 +1,118 @@ +# Unlimited linear corrections cannot repair the frozen helper-572 seam + +This contribution was produced by Nick Petalas. It proves a scoped obstruction +on the selected PR6030 word: after overwriting helper 572 at cut 13637, arbitrary +finite linear recoding inside the declared chart-595 and chart-603 regions +cannot preserve the protected original outputs and retain any nonzero public +response to the new independent input. + +This extends JoyboyBrian's [PR6088](https://github.com/CrocSwap/integer-mult-bounds/pull/6088) +from two added ADDs to arbitrary linear bank maps. Increasing the scalar +correction count in these regions cannot repair the split. A changed transport, +window, prefix or storage contract is needed. No new kappa is claimed. + +## Result and evidence + +[PROOF.md](PROOF.md) specifies the complete contract and proves the theorem. +The first bank has six fields. Only field 572 moves to the second bank before +field 709 enters. Six protected output equations force the transmitted form to +recover the displaced old helper value; a single linear channel then cannot +also carry the new independent input. + +The exact standard-library certificate derives eight independent source forms +from the prefix, with a minor determinant `1/32`, and a six-row protected suffix +minor of determinant `8`. It checks the complete original-input boundary +identities, every public response of the erased 778 and V-final 740 columns, +and the source chronology. The proof uses these finite facts to cover every +finite correction length and arbitrary rational coefficients. + +The verifier also enumerates 722 rank-one products over the fields of orders +2, 3 and 5, checks a two-channel positive scope control and a singular minor, +and rejects four changed schedule/original-input fixtures and changed source +bytes. These controls corroborate the rank argument; the universal rational +statement is the written proof. No predecessor census or theorem is replayed. +The generated JSON receipt binds the package files and exact source hash. +Default execution writes nothing. + +## Reproduce + +From the repository root, using the standard-library CPython 3.12 interpreter: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/p104-unrestricted-572-seam/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/p104-unrestricted-572-seam/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/p104-unrestricted-572-seam +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/p104-unrestricted-572-seam --check-source-history --check-modes +``` + +Another CPython 3.12 path may be substituted. Expected scientific marker: +`PASS_P104_UNRESTRICTED_572_SEAM`. The registered normal and optimized checks +have separate 60-second limits. Metadata and committed-byte checks require a +Git checkout. The direct verifier requires only its package and declared word. + +## Scope and sources + +Scientific base: canonical main `a5bff3bf133e482541c09eba4e773884bdb2b1b7`, +priority revision 8. The selected record gives conditional kappa `0.003125804`. +The current source-binding orientation passes; it is not a selected cold replay. +[SOURCES.json](SOURCES.json) pins the exact selected word and historical task +provenance. [TASK.json](TASK.json) records the changed scope and next questions. + +The immediate question source is JoyboyBrian's PR6088 at +`6e6236ec763d2aa3eac40201c9634051c583320c`, +`research/p104-noncarrier-two-add-seam/PROOF.md`. Its finite pair result is cited +context. The general carrier exclusions of apoursh PR6067 and Jonathan Capalbo +PR6069 are distinct because they preserve original rows at each atomic update. +JosieElliston PR6108 documents the remaining cross-time gap. The earlier PR6040 +unit-injection census is retained as lineage. This contribution changes the +correction model; it does not retarget that census to another word or group. + +[Advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19279693). +Live handoffs, open/account PRs and local reservations were checked. Merged PR +and main-tree searches included helper 572, unrestricted recoding, two-chart +seams and arbitrary correction lengths. The overlap helper reported complete +remote pagination with 338 open PRs and 5,959 Discussion records, but only +78 of 8,623 local note paths were materialized. Direct main-tree searches +supplemented that sparse coverage. Unpublished work and historical code diffs +remain outside this bounded check; no global novelty certificate is claimed. + +No selected native/compiler/caller/outer cold replay, Lean or Docker run is +needed for this scalar obstruction. No physical construction, cost improvement, +new supplier or complete multiplication theorem is supplied. All five selected +framework assumptions remain. Independent human and formal proof-kernel review +are unclaimed. + +## Open next questions + +- Can a second independent transferred form repair this split at favorable + complete cost? First specify its legal source/destination frames and solve + all original-input equations. The missing transport, normalization, + restoration and full paid/target invoice are blockers. +- Can a pre-cut save or changed chronological window avoid the obstruction? + First pin that changed boundary and its owned lifetime, then derive its + independent source forms and protected-output minor. The present frozen + two-region certificate does not transfer automatically. + +## Engineering limits + +The verifier uses Build the Lever and Prove It Works: the two source-bound +minors and all boundary equations are reproducible from one declared input. +No recursive call exists. Loops are bounded by the fixed 22,803 events, 799 +fields, 771 input columns, eight response columns, 722 finite-field products +and at most `8!` determinant summands. Every function is below 60 lines. +Explicit failure checks remain enabled under optimization. + +Power-of-Ten rule 3 has a managed-runtime deviation in `verify.py`: Python's +Fraction, JSON and dictionary operations allocate during execution. The scope +is this offline fixed-input certificate. The authenticated dimensions bound +state and snapshots by fewer than ten `799*771` coefficient entries, plus the +fixed word and eight-column suffix. No concurrent work or growing input stream +is accepted. Warning-strict normal/optimized registered replay is the diagnostic +check. A fixed-capacity rational representation would be required before reuse +in a runtime that forbids dynamic allocation. + +Credit JoyboyBrian for the seam and question, apoursh, Jonathan Capalbo, +JosieElliston, Matarener, flyingviper, Ali Romman, DreamingOfClouds and their +retained P104/native/caller predecessors. The fixed-word chronology and rank +factorization methods are standard; the new contribution is this source-bound +unbounded-length obstruction and its compact certificate. Apache-2.0. diff --git a/research/p104-unrestricted-572-seam/SOURCES.json b/research/p104-unrestricted-572-seam/SOURCES.json new file mode 100644 index 0000000000..8eb788ceeb --- /dev/null +++ b/research/p104-unrestricted-572-seam/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "a5bff3bf133e482541c09eba4e773884bdb2b1b7", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/p104-helper470-twin-rung-removal/WORD.json.gz", + "usage": "input", + "git_blob": "22f9ab02d1b73ea0aa4b07ce445a14cc2602c760", + "sha256": "7834725d9e34ee846a9ccc615221ea81e0201613938afa185d2eda0c9a6c232f" + }, + { + "path": "research/p104-noncarrier-two-add-seam/PROOF.md", + "usage": "provenance", + "git_blob": "089d6b55e1e02b85afd7467582b5dcaa2b0d9b2a", + "sha256": "0a74f3e08165e92f89be8fe3b72e57c9766daa77ecae8e6a470c2d7ae00d9362" + } + ] +} diff --git a/research/p104-unrestricted-572-seam/TASK.json b/research/p104-unrestricted-572-seam/TASK.json new file mode 100644 index 0000000000..281360fd53 --- /dev/null +++ b/research/p104-unrestricted-572-seam/TASK.json @@ -0,0 +1,123 @@ +{ + "schema_version": 1, + "task_id": "p104-side-correction", + "priority_revision": 8, + "base_commit": "a5bff3bf133e482541c09eba4e773884bdb2b1b7", + "original_card": { + "id": "p104-side-correction", + "question": "Can joint helper bases and a legal causal split improve the complete P104 productive/paid invoice?", + "starting_points": [ + "docs/research/current-priorities.md", + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "research/p104-helper-subspace-splits/README.md", + "research/dyadic-helper-channel-capacity/README.md" + ], + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "acceptance_gate": "An exact arbitrary-input identity, source/target frame availability and restoration at the chosen cut, plus the complete channel+correction+idle/hosting bill or an explicit favorable bound. The native channel alone is not a supplier. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "first_experiment": "Start with the selected #5599 emitted word and review pending #5718 distinct input/output bases plus #5717/#5719 coverage before claiming work. Pick one uncovered source word, helper group and cut region. Prove the arbitrary-input relation and legal entry/exit corrections, then compare full target and paid profiles. Reject if completion, owned lifetimes or consumer costs repay the gain. A static pairing rank alone is not a physical split.", + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "allowed_variations": [ + "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes." + ], + "scope_change_triggers": [ + "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.", + "Treating an archived proposal or local numerical pass as complete supplier admission." + ], + "overlap_terms": [ + "P104", + "helper basis", + "helper split", + "5718", + "dyadic capacity" + ], + "existing_checks": [ + { + "scope": "PR #4133: literal-slot defect", + "evidence": "research/p104-literal-slot-defect/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "status": "author-checked", + "source_commit": "88666f1dee93fbd85b31fd5d6f91a219e111b5f4", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4136: uniform commutation gap", + "evidence": "research/p104-uniform-commutation-gap/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "status": "author-checked", + "source_commit": "281ce601a8be9db470de630759179c23e1dfaa88", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4140: uniform encoding gap", + "evidence": "research/p104-uniform-encoding-gap/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "status": "author-checked", + "source_commit": "de25c6525aa866962309df5d107b32d55e6e5628", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4153: source-chart shortcut exhausts its optimistic allowance", + "evidence": "research/p104-source-chart-shortcut/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "status": "author-checked", + "source_commit": "9123241fea53df77e51ffe30d9aca1625d4bf3a8", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4154: fiber-tag seam mismatch", + "evidence": "research/p104-fiber-tag-seam/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "status": "author-checked", + "source_commit": "4ffcdaee5d6255a9cea1fe53a5424435068089d0", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "status": "reviewed", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Exclude arbitrary finite rational linear recodings across the fixed helper-572 chart-595/chart-603 seam of selected PR6030, preserving every outside-V original-input output and requiring a nonzero independent z response.", + "scope_change_reason": "Extend JoyboyBrian PR6088 beyond two added scalar gates to arbitrary linear bank maps. This is a source-bound obstruction before the physical supplier/budget gate, not an audit of predecessor exclusions or a new invoice.", + "bottleneck_link": "Shows that increasing scalar correction length alone cannot legalize this fixed candidate helper split. A second independent transport, changed window, prefix, route or storage contract is needed.", + "budget_minutes": 60, + "stop_rule": "Ship the first verified source-bound obstruction; do not enlarge the seam or seek a new supplier.", + "outcome": "completed", + "evidence": "PROOF.md and the generated hash-bound verify.py receipt.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can a second independently transported scalar direction legalize this helper split at a favorable complete paid cost?", + "why_it_matters": "The proved obstruction is a one-channel rank deficit; arbitrary additional scalar operations on the same channel do not address it.", + "first_step": "Specify one additional legal transfer and both destination frames, then solve its all-input endpoint equations before pricing.", + "blocked_by": "No physical extra-transfer word, productive-target normalization, restoration or complete signed invoice is supplied." + }, + { + "question": "Can a pre-cut save or a changed chronological window avoid this single-channel obstruction?", + "why_it_matters": "The result fixes the prefix, six-field first bank, second-bank entry and suffix.", + "first_step": "Pin one changed cut and recompute its independent source forms and protected-output suffix minor.", + "blocked_by": "A changed cut and owned lifetime must be justified; no inference transfers this certificate to it." + } + ] +} diff --git a/research/p104-unrestricted-572-seam/VERIFY.json b/research/p104-unrestricted-572-seam/VERIFY.json new file mode 100644 index 0000000000..16db36c1be --- /dev/null +++ b/research/p104-unrestricted-572-seam/VERIFY.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/p104-helper470-twin-rung-removal/WORD.json.gz" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Exact source/prefix/seam/suffix certificate; two independent nonzero minors; all original-input boundary equations; rank-one and mutation controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Same complete certificate and rejecting controls with assertions disabled." + } + ] +} diff --git a/research/p104-unrestricted-572-seam/verify.py b/research/p104-unrestricted-572-seam/verify.py new file mode 100644 index 0000000000..399d7edf91 --- /dev/null +++ b/research/p104-unrestricted-572-seam/verify.py @@ -0,0 +1,235 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Exact certificate for the unrestricted linear helper-572 seam obstruction.""" +from fractions import Fraction as Q +from hashlib import sha256 +from itertools import permutations, product +from pathlib import Path +import gzip +import json + +HERE = Path(__file__).resolve().parent +WORD = "research/p104-helper470-twin-rung-removal/WORD.json.gz" +CUT, LEFT_END, RIGHT_END = 13637, 13651, 13655 +FIRST = (127, 572, 581, 582, 731, 778) +EXTRA = (740, 709) +LEFT = (127, 581, 582, 731, 778) +RIGHT = (572, 740, 709) +OUTPUTS = (116, 120, 127, 134, 138, 176) +VISIBLE = (0, 1, 2, 3, 5, 7) +T0 = ((1, 0, 0, 0, 0, 0, 0, 0), + (0, 0, 1, 0, 0, 0, 0, 0), + (0, 0, 0, 1, 2, 0, 0, 0), + (0, 0, 0, 0, 1, 0, 0, 0), + (0, 0, 0, 0, 0, 1, 0, 0), + (0, 0, 0, 0, 0, 1, 0, 0), + (0, 0, 0, 0, 0, -1, 1, 0), + (0, 0, 0, 0, 0, 0, 0, 1)) + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def add(row, other, scale): + result = row.copy() + for column, value in other.items(): + value = result.get(column, Q(0)) + scale * value + if value: + result[column] = value + else: + result.pop(column, None) + return result + + +def apply(rows, event): + operation, target = event[:2] + if operation in ("ADD", "COPY"): + old = rows[target] if operation == "ADD" else {} + rows[target] = add(old, rows[event[2]], Q(event[3])) + elif operation == "SCALE": + rows[target] = {i: Q(event[2]) * v for i, v in rows[target].items() + if Q(event[2]) * v} + elif operation in ("INIT", "CLEAR"): + rows[target] = {} + else: + need(operation == "MOVE", "known scalar opcode") + + +def prefix(word): + n, size = word["public"], word["public"] + word["owned_fields"] + rows = [{i: Q(1)} if i < n else {} for i in range(size)] + charts = word["initial"] + [None] * word["owned_fields"] + snapshots, inventories = {}, {} + for index in range(RIGHT_END + 1): + event = word["program"][index] + operation, target = event[:2] + if operation == "INIT": + need(charts[target] is None, "INIT ownership") + charts[target] = event[2] + elif operation == "MOVE": + need(charts[target] == event[2], "MOVE entry chart") + charts[target] = event[3] + elif operation == "CLEAR": + need(charts[target] == event[2], "CLEAR entry chart") + charts[target] = None + else: + need(charts[target] == event[-1], "scalar target chart") + if operation in ("ADD", "COPY"): + need(charts[event[2]] == event[-1], "scalar source chart") + apply(rows, event) + if index in (CUT, RIGHT_END): + snapshots[index] = [row.copy() for row in rows] + if CUT <= index <= RIGHT_END: + inventories[index] = tuple(tuple(r for r, c in enumerate(charts) if c == f) + for f in (595, 603)) + return snapshots, inventories + + +def suffix(word): + size = word["public"] + word["owned_fields"] + roles = LEFT + RIGHT + rows = [{roles.index(r): Q(1)} if r in roles else {} for r in range(size)] + for index in range(RIGHT_END + 1, len(word["program"])): + apply(rows, word["program"][index]) + return rows[:word["public"]] + + +def pivot_columns(rows): + """At most eight rows; exact row elimination, with no input-column bound hidden.""" + basis = {} + for original in rows: + row = original.copy() + for pivot in sorted(basis): + if pivot in row: + row = add(row, basis[pivot], -row[pivot]) + if row: + pivot = min(row) + scale = row[pivot] + basis[pivot] = {i: value / scale for i, value in row.items()} + return tuple(sorted(basis)) + + +def determinant(matrix): + """Independent Leibniz determinant; callers enforce size at most eight.""" + n = len(matrix) + need(1 <= n <= 8 and all(len(row) == n for row in matrix), "small square minor") + total = Q(0) + for order in permutations(range(n)): + value = Q(1) + for i in range(n): + value *= matrix[i][order[i]] + inversions = sum(order[i] > order[j] for i in range(n) for j in range(i + 1, n)) + total += (-1 if inversions % 2 else 1) * value + return total + + +def chronology(word, inventories): + need(word["program"][CUT] == ["COPY", 778, 572, "1", 595], "cut COPY") + need(word["program"][13652] == ["MOVE", 572, 595, 603, False], "single channel MOVE") + need(word["program"][13654] == ["ADD", 740, 572, "-1", 603], "retained second-stage ADD") + need(word["program"][RIGHT_END] == ["MOVE", 709, 597, 603, False], "external 709 entry") + need(word["program"][13656] == ["CLEAR", 778, 595], "retained owned erasure") + for index in range(CUT, LEFT_END + 1): + need(inventories[index][0] == FIRST, "fixed first bank") + for index in (13652, 13654): + need(inventories[index][1] == (572, 740), "second bank before 709") + need(inventories[RIGHT_END][1] == (572, 709, 740), "second bank after 709") + for event in word["program"][CUT + 1:RIGHT_END + 1]: + if event[0] in ("ADD", "COPY", "SCALE") and event[-1] == 595: + need(event[1] in FIRST, "all first-stage scalar targets stay inside bank") + need(not (event[0] in ("ADD", "COPY", "SCALE") and event[1] == 709), + "external 709 value fixed before entry") + + +def certify(word): + snapshots, inventories = prefix(word) + chronology(word, inventories) + n = word["public"] + sources = [snapshots[CUT][r].copy() if r != 572 else {n: Q(1)} + for r in FIRST + EXTRA] + pivots = pivot_columns(sources) + need(len(pivots) == 8, "eight independent source forms") + need(pivots == (0, 2, 34, 572, 581, 582, 740, 770), "source witness columns") + source_minor = [[row.get(i, Q(0)) for i in pivots] for row in sources] + source_det = determinant(source_minor) + need(source_det == Q(1, 32), "independent source minor") + for role, coefficients in zip(LEFT + RIGHT, T0): + reconstructed = {} + for row, coefficient in zip(sources, coefficients): + reconstructed = add(reconstructed, row, Q(coefficient)) + need(reconstructed == snapshots[RIGHT_END][role], "complete unsplit boundary identity") + responses = suffix(word) + need(all(not row.get(4, 0) for row in responses), "778 is erased at every public output") + need(all(row.get(6, 0) == (1 if i == 740 else 0) + for i, row in enumerate(responses)), "740 reaches only its own public output") + outside = [i for i, chart in enumerate(word["final"]) if chart != word["final"][572]] + need(740 not in outside and all(i in outside for i in OUTPUTS), "protected output witnesses") + minor = [[responses[i].get(j, Q(0)) for j in VISIBLE] for i in OUTPUTS] + need(determinant(minor) == 8, "six protected rows force all six visible boundary forms") + return {"source_pivots": pivots, "source_minor_det": str(source_det), + "protected_outputs": OUTPUTS, "protected_minor_det": "8", + "protected_output_count": len(outside), "new_input_column": n, + "first_bank": FIRST, "post_bank": LEFT + RIGHT, + "protected_minor": [[str(x) for x in row] for row in minor]} + + +def controls(word): + trials = 0 + for prime in (2, 3, 5): + for a0, a1, d0, d1 in product(range(prime), repeat=4): + q00, q01 = d0 * a0 % prime, d0 * a1 % prime + q10, q11 = d1 * a0 % prime, d1 * a1 % prime + need(q00 * q11 % prime == q01 * q10 % prime, "single channel has rank at most one") + need(not (q00 == 1 and q01 == 0 and q11 != 0), "recovered old value forbids new signal") + trials += 1 + need(determinant([[1, 0], [0, 1]]) == 1, "two-channel scope escape accepted") + need(determinant([[1, 1], [1, 1]]) == 0, "dependent source forms rejected") + mutations = ((CUT, 3, "2"), (13652, 3, 597), + (13655, 1, 740), (13656, 1, 740)) + for index, position, value in mutations: + changed = dict(word) + changed["program"] = [event.copy() for event in word["program"]] + changed["program"][index][position] = value + try: + certify(changed) + except ValueError: + pass + else: + raise ValueError("changed seam or erasure accepted") + return {"rank_one_products": trials, "changed_schedule_rejections": len(mutations), + "two_channel_positive": True, "dependent_forms_control": True, + "original_input_control": True} + + +def decode(raw, expected): + need(sha256(raw).hexdigest() == expected, "source SHA256") + word = json.loads(gzip.decompress(raw)) + need(word["public"] == 770 and word["owned_fields"] == 29, "bounded source dimensions") + need(len(word["program"]) == 22803, "bounded source event count") + return word + + +def main(): + manifest = json.loads((HERE / "SOURCES.json").read_text()) + pin = next(row for row in manifest["files"] if row["path"] == WORD) + raw = (HERE.parents[1] / WORD).read_bytes() + word = decode(raw, pin["sha256"]) + result = certify(word) + result["controls"] = controls(word) + try: + decode(raw + b"changed", pin["sha256"]) + except ValueError: + result["controls"]["changed_source_rejected"] = True + else: + raise ValueError("changed source accepted") + result["package_sha256"] = {p.name: sha256(p.read_bytes()).hexdigest() + for p in sorted(HERE.iterdir()) if p.is_file()} + result["source_sha256"] = pin["sha256"] + result["status"] = "PASS_P104_UNRESTRICTED_572_SEAM" + print(json.dumps(result, indent=2, sort_keys=True)) + + +if __name__ == "__main__": + main()