From 1866c2f3ee2d4cf5bf3e8f008883a6605ab10ed3 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Fri, 30 Oct 2026 11:34:07 +0000 Subject: [PATCH] feat(research): prove the P104 wire dirty-entry obstruction --- research/p104-wire-dirty-entry/PROOF.md | 132 +++++++++++ research/p104-wire-dirty-entry/README.md | 142 +++++++++++ research/p104-wire-dirty-entry/SOURCES.json | 36 +++ research/p104-wire-dirty-entry/TASK.json | 123 ++++++++++ research/p104-wire-dirty-entry/VERIFY.json | 40 ++++ research/p104-wire-dirty-entry/verify.py | 249 ++++++++++++++++++++ 6 files changed, 722 insertions(+) create mode 100644 research/p104-wire-dirty-entry/PROOF.md create mode 100644 research/p104-wire-dirty-entry/README.md create mode 100644 research/p104-wire-dirty-entry/SOURCES.json create mode 100644 research/p104-wire-dirty-entry/TASK.json create mode 100644 research/p104-wire-dirty-entry/VERIFY.json create mode 100644 research/p104-wire-dirty-entry/verify.py diff --git a/research/p104-wire-dirty-entry/PROOF.md b/research/p104-wire-dirty-entry/PROOF.md new file mode 100644 index 0000000000..e4c7029d88 --- /dev/null +++ b/research/p104-wire-dirty-entry/PROOF.md @@ -0,0 +1,132 @@ +# Correlated dirt at a three-register wire meeting + +This contribution was produced by Nick Petalas. Apache-2.0. + +## Boundary and claim type + +This is a scoped response-space proof and a finite local response construction. +It partially answers Matarener's PR6217 one-helper wire question. It neither +supplies nor excludes a complete one-helper program. + +We cite PR6217's premises, without replaying its proof or census. For an A2 +pair x,y the common seven-frame G has 24 retained ports. Its required rows +are proportional except at the third vertex z, where their ratio changes +sign. Every incoming six-frame contains at most 16 of these ports. The +content-in-frame rule confines incoming live coefficients to those ports. + +The boundary has three incoming registers, one independent dirty scalar h, +and no further live reads, allocation, erasure or incoming registers during +the local meeting. Arbitrarily many rational linear local operations are +allowed. Two outputs must have the prescribed live responses and zero h +coefficient. Other initial public and helper columns are projected away. +This projection is necessary for a full program; sufficiency is not claimed. + +## General kernel statement + +Let K have characteristic different from two. Let C contain m ports with +distinguished z. Let e be a nonzero row supported only at z. Let c_z=0 and +c_t be nonzero for every t different from z. Put W=span(c,e). Suppose the +incoming registers are + + R_i = A_i X + b_i h, i=0,1,2, + +where b is nonzero, X has independent live coordinates, and each A_i has +support strictly smaller than m-1. Suppose local linear processing produces +c+e and c-e, both with zero h coefficient. Then: + +1. At least two entries of b are nonzero. An isolated dirty helper with two + h-free public inputs cannot suffice, regardless of the helper's live row. +2. If exactly two entries of b are nonzero, the sole h-free live row is a + nonzero multiple of e. The dirty pair's live supports jointly cover all + m-1 nonexceptional ports. If each support has size at most s, each dirty + row contains at least m-1-s nonexceptional ports. + +These are necessary conditions. They do not characterize the case where all +three inputs carry h. The support restriction is essential. + +*Proof.* Every eventual register is a linear combination of the incoming +registers. Its h coefficient vanishes precisely when the combination lies +in ker(b^T), of dimension two. The rows c+e and c-e are independent because +2 is nonzero. Therefore the live-image map + + L: ker(b^T) -> K^C, lambda -> sum_i lambda_i A_i + +has image exactly W and is injective. If b_i=0, its coordinate vector lies +in the kernel. Thus A_i belongs to W and is nonzero. Every alpha*c+beta*e +with alpha nonzero has at least m-1 support positions, so such A_i must be +a nonzero multiple of e. Two h-free rows would make L noninjective. This +proves the first assertion. + +For the second, let i be the clean index and j,k the dirty indices. A kernel +basis consists of the i-th coordinate vector and b_k times the j-th minus +b_j times the k-th. Their live images A_i and b_k A_j-b_j A_k span W. The +latter must have a nonzero c coefficient. At every t different from z, +at least one of A_jt,A_kt is consequently nonzero. Their union covers m-1 +positions, giving each stated support lower bound. QED. + +The proof even permits arbitrary linear readouts, without invertibility. +For PR6217, m=24 and s=16. Correlated dirt on at least two incoming rows is +necessary. If exactly two carry dirt, the clean row must already isolate z, +and each dirty row carries at least seven of the other 23 coordinates. This +is a concrete entry condition, not a claim that it can be prepared cheaply. + +## Local response construction + +The correlated-dirt escape is nonempty. Use literal port labels +x=11, y=19, z=487. Let G be the kernel of normals 11 and 19 in F2^9. +Add respectively normals 455 and 56 for six-frames H_0,H_1. Both normal +triples have rank three. Their port sections are complementary because +455 XOR 56=511 and every port has odd weight. The sections have sizes 16 +and 8; z belongs to the former. + +In the canonical gauge take the required rows G_x/2 and G_y/2 on these +24 ports. Here G_xy=1. Write these as c+e and c-e, where +e=(G_xz/2)e_z. Put a=c restricted to H_0 and d=c restricted to H_1. +Their support sizes are 15 and 8, and a+d=c. Supply + + R_0=eX, R_1=aX-h, R_2=dX+h. + +Their live parts lie in the declared six-frames. Once they meet at G, use +these four scalar events: + + R_1 += R_2 + R_1 -= R_0 + R_0 *= 2 + R_0 += R_1 + +The exact endpoint is + + R_0=(c+e)X, R_1=(c-e)X, R_2=dX+h. + +The scalar matrix has determinant 2. Reverse the four events, replacing +doubling by halving, to restore every incoming value. The helper may have +any h and retains its entrance value. This proves attainability of this +response projection with two dirty carriers and a singleton clean input. + +The helper still contains dX at exit. This meeting preserves dX+h; it does +not restore the original h. Preparation of aX-h, dX+h and the singleton, +preservation of omitted public/dirty columns and later removal of dX are +not supplied. In particular, the scalar construction is not a complete +arbitrary-public-input endpoint or a favorable physical invoice. + +## Decision and remaining obligations + +Stop at this local result. Before expanding the architecture, identify the +pre-cut contact depositing -h into a public register, the singleton source, +all other dirty columns and the helper cleanup path. Preparation, native +delivery, restoration, precision, stock, compiler and caller costs are +unknown. None is treated as zero. There is no new kappa, supplier admission, +all-size theorem or selected-frontier change. + +The proof holds over every field of characteristic different from two. +The P104 witness is rational and dyadic. A small F3 domain is finite +corroboration, not a formal proof-kernel certification. + +## Credit + +Matarener's PR6217 supplies the question, sign/capacity/two-source premises +and E8 interpretation. DreamingOfClouds's PR6170 supplies frame-contract +context. Retain the P104 carrier-code, native, helper, controller and caller +lineage credited there. Kernel dimension, support arguments and reversible +row operations are classical. The new contribution is their local +correlated-dirt consequence and explicit response construction. diff --git a/research/p104-wire-dirty-entry/README.md b/research/p104-wire-dirty-entry/README.md new file mode 100644 index 0000000000..1ba5ce4e17 --- /dev/null +++ b/research/p104-wire-dirty-entry/README.md @@ -0,0 +1,142 @@ +# A dirty-entry obstruction for a one-helper P104 wire meeting + +This contribution was produced by Nick Petalas. Apache-2.0. + +A dirty helper cannot supply PR6217's missing third effective source when +its dirt is confined to that helper at the meeting entrance. At least two +of the three incoming registers must carry the same independent dirt. If +exactly two carry it, the remaining clean live row must already isolate the +exceptional third root. The two dirty live supports must cover the other +23 ports, so each contains at least seven of them under the 16-port cap. + +Claim type: **scoped response-space proof with a finite local construction**. +The result refines Matarener's explicit one-helper wire question. It does +not decide the cost or existence of a complete one-helper program. + +The new kernel argument permits arbitrary finite local rational processing, +even arbitrary linear readouts. PR6217's sign, capacity and content-in-frame +facts are cited premises. They are not audited or replayed here. +[PROOF.md](PROOF.md) states every hypothesis and the proof over every field +of characteristic different from two. + +## Local escape and its limit + +At the common seven-frame for labels 11 and 19, the third root is 487. +Two complementary six-frame sections split the live coefficients into +parts a,d of support 15 and 8. Let e isolate the third root and c=a+d. +The normalized Gram response rows are c+e,c-e. With prepared inputs + +```text +(R0,R1,R2) = (eX, aX-h, dX+h), h arbitrary, +R1 += R2; R1 -= R0; R0 *= 2; R0 += R1 +(R0,R1,R2) = ((c+e)X, (c-e)X, dX+h). +``` + +The exact scalar map has determinant 2 and a four-event literal inverse. +The helper retains its entrance value dX+h. Its original h is not restored +by this meeting. Preparing the correlated pair and singleton, preserving +all omitted public/dirty columns, legal native access and later removal +of dX remain open. No complete signed invoice, physical saving, supplier, +new kappa or full multiplication theorem is claimed. + +This is the first local result, so construction stops here. The complete +preparation, movement, restoration, precision, compiler and caller charges +are unknown. Their omission grants no productive credit or free operation. +The selected record and its five framework assumptions are unchanged. + +## Evidence and reproduction + +From the repository root with CPython 3.12, standard library only: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -X dev -B research/p104-wire-dirty-entry/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -X dev -B -O research/p104-wire-dirty-entry/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/p104-wire-dirty-entry +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/p104-wire-dirty-entry --check-source-history +``` + +Another CPython 3.12 interpreter can replace the absolute path. Expected +markers are `PASS_P104_WIRE_DIRTY_ENTRY`, +`PASS_REGISTERED_RESEARCH_PACKAGE` and `PASS_RESEARCH_COMMIT_BYTES`. +The final command requires committed bytes and full source history. + +The checker reconstructs this one new witness from the hash-bound port +fixture, checks both complete 25-column projected endpoints and the +literal inverse, and executes 625 scalar cases with arbitrary tested dirt. +It checks all 251,559 normalized F3 cases with four live coordinates, +three incoming rows of support at most two and nonzero dirt. Nonzero dirt +entries are normalized to one by row scaling. A separately implemented +augmented-matrix elimination checks every case against the kernel test. +The feasible counts by dirt-support size 1,2,3 are 0,288,108. These are +counts in this small normalized domain, not a census of P104 programs. + +Eleven rejecting controls cover each omitted event, lost doubling, isolated +or wrong-sign dirt, changed singleton, aliasing, zero scaling and invalid +operations. Two positive controls outside the hypotheses show why the +support cap and nonzero dirt premise cannot be dropped. The JSON receipt +is generated at execution and binds all six package files and the exact +external port input by SHA256. No receipt is handwritten. + +No predecessor scientific executable is imported. Local normal/optimized +and registered replay results are recorded in the submission. Hosted CI +is a separate check, and no hosted pass is asserted before it completes. +No Lean, Docker, native, full supplier or selected cold replay was run. +Independent human and formal proof-kernel review are unclaimed. + +## Provenance and overlap + +Base `2485805a6d47f36ea83ddde6327d453ac82d44dc`, priority revision 8, +selected conditional kappa .003125804. The baseline command authenticated +source bindings only. [SOURCES.json](SOURCES.json) pins the original card, +selected record, PR6217 proof context and runtime port fixture. +[TASK.json](TASK.json) records the narrowed local obligation. + +The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19292022) +reserves the local dirty-entry question. Live open PRs, recent account +contributions, handoffs, active Discussions, main README terms, merged PR +searches and local reservations were checked. Those searches omit arbitrary +historical diffs and unpublished work; empty results are not novelty proofs. +PR6219's A2 packing and PR6218's decoder floor address different obligations. +No predecessor mathematical number is reverified as this deliverable. + +## Open next questions + +Can a legal pre-cut contact prepare the correlated pair and the exceptional +singleton? Start with actual public/helper trajectories and track every +original input column. The required dirt preload and full public endpoint +are still missing. + +Can that prepared helper be cleaned while beating the matched two-helper +route? First name its later access to dX and price all paid and productive +histograms together. Native delivery, cleanup and a complete caller are +blockers. These questions are also structured in TASK.json. + +## Credit + +Credit Matarener / PR6217 for the question, sign/capacity/two-source premises +and E8 port interpretation, DreamingOfClouds / PR6170 for frame-contract +context, and the retained P104 carrier-code, native, helper, controller and +caller lineage. Kernel dimension, support arguments and reversible row +operations are classical. The new material is the correlated-dirt necessity, +its singleton consequence and the explicit local response construction. +All predecessor files and credit lines remain unchanged. + +## Verifier bounds + +The direct call graph is acyclic. The verifier has no subprocess, network, +write path or dynamically loaded predecessor code. There are 251,559 census +iterations; each elimination has at most five rows and five columns. The +P104 pass uses three rows of 25 coordinates. Scalar fixtures use four events +in each direction, and every collection has a finite fixed bound. Functions +are below 60 physical lines. Explicit exceptions keep checks active under +optimized Python. Warning-strict development-mode runs and source compilation +provide the available Python diagnostics; no external static analyzer was +available in the selected environment. + +Power of Ten rule 3 requires a managed-runtime deviation. CPython allocates +objects during execution. The fixed domains above bound live collections; +no census results are accumulated. Each file is limited to 256 KiB, +with one guard byte read, and file handles close on all exits. Dynamic integer +and Fraction allocation is bounded by the fixed fixtures and operation +counts. This is not a fixed-allocation runtime claim. A future compiled +verifier could use fixed-capacity arrays if that becomes necessary. diff --git a/research/p104-wire-dirty-entry/SOURCES.json b/research/p104-wire-dirty-entry/SOURCES.json new file mode 100644 index 0000000000..5e43ad1399 --- /dev/null +++ b/research/p104-wire-dirty-entry/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "2485805a6d47f36ea83ddde6327d453ac82d44dc", + "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-carrier-code-uniqueness/e8/ports.json", + "usage": "input", + "git_blob": "b964c3ae2ea54d3763d74639d691ea9f5b02920e", + "sha256": "ba6a0b9cf76b7cccc1ce8b3d1aa78a4aa329b34d45aded694648f0cf43fc9fce" + }, + { + "path": "research/p104-wire-routing-obstructions/PROOF.md", + "usage": "provenance", + "git_blob": "47df6ab141de73bf253b3bbceb6f09bbc7535c9b", + "sha256": "cbb7a9d71155f31e68eaf708ce6d0d5731914ab4777c9fd806991723ab44b223" + }, + { + "path": "research/p104-wire-routing-obstructions/README.md", + "usage": "provenance", + "git_blob": "76dd916fc6527ceeeebedcf99c87198209bbaa39", + "sha256": "4de7e994de623359a9cb91319d71575965dcd2e8059b911672b1e788774f2cce" + } + ] +} diff --git a/research/p104-wire-dirty-entry/TASK.json b/research/p104-wire-dirty-entry/TASK.json new file mode 100644 index 0000000000..1131acec1c --- /dev/null +++ b/research/p104-wire-dirty-entry/TASK.json @@ -0,0 +1,123 @@ +{ + "schema_version": 1, + "task_id": "p104-side-correction", + "priority_revision": 8, + "base_commit": "2485805a6d47f36ea83ddde6327d453ac82d44dc", + "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": "refined", + "actual_scope": "Necessary correlated-dirt entry and singleton support for the three-register response projection of a PR6217 A2 wire meeting, with an explicit local attaining response word.", + "scope_change_reason": "Resolve a source-relative local boundary obligation of the one-helper question, without claiming preparation, full public columns, helper cleanup or a complete signed invoice.", + "bottleneck_link": "The proposed complex wire route needs a third effective source at its seven-frame meeting. This proof identifies the required dirt-cancellation entry condition and a local escape; it does not grant a free clean helper.", + "budget_minutes": 60, + "stop_rule": "Ship this first verified local obstruction and response construction; do not expand to a complete one-helper program.", + "outcome": "partial", + "evidence": "PROOF.md and verify.py: exact 25-column response/inverse identity, 625 dirty scalar fixtures, full 251559-case F3 oracle domain, 11 rejecting controls and two scope controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can one legal pre-cut contact prepare the correlated dirty pair and exceptional singleton at an A2 meeting?", + "why_it_matters": "An isolated dirty helper cannot supply the missing response direction.", + "first_step": "Choose actual public and helper trajectories, deposit -h before the cut, and track all independent public and helper columns.", + "blocked_by": "The response construction omits the preparation, complete original-input endpoint and native costs." + }, + { + "question": "Can the prepared helper be cleaned and the completed word beat the two-helper route?", + "why_it_matters": "The local helper exits with dX+h, so its live content and transport cannot be discarded.", + "first_step": "Name a legal later source access for removing dX and compare the complete paid and productive histograms with the matched original route.", + "blocked_by": "No cleanup path, physical caller or favorable complete invoice is currently supplied." + } + ] +} diff --git a/research/p104-wire-dirty-entry/VERIFY.json b/research/p104-wire-dirty-entry/VERIFY.json new file mode 100644 index 0000000000..bd943986e7 --- /dev/null +++ b/research/p104-wire-dirty-entry/VERIFY.json @@ -0,0 +1,40 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/p104-carrier-code-uniqueness/e8/ports.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-X", + "dev", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact source-bound P104 response/inverse, full F3 kernel versus augmented-rank domain, rejecting and outside-scope controls; generated source-hash receipt." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-X", + "dev", + "-B", + "-O", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact source-bound P104 response/inverse, full F3 kernel versus augmented-rank domain, rejecting and outside-scope controls; generated source-hash receipt." + } + ] +} diff --git a/research/p104-wire-dirty-entry/verify.py b/research/p104-wire-dirty-entry/verify.py new file mode 100644 index 0000000000..dbf05e4a68 --- /dev/null +++ b/research/p104-wire-dirty-entry/verify.py @@ -0,0 +1,249 @@ +#!/usr/bin/env python3 +"""Check the new response boundary, not the predecessor's scientific claims. + +This contribution was produced by Nick Petalas. Apache-2.0. +""" + +import hashlib +import itertools +import json +from fractions import Fraction as Q +from pathlib import Path + +HERE = Path(__file__).resolve().parent +PORT_PATH = "research/p104-carrier-code-uniqueness/e8/ports.json" +PORT_SHA = "ba6a0b9cf76b7cccc1ce8b3d1aa78a4aa329b34d45aded694648f0cf43fc9fce" +WORD = (("add", 1, 2, 1), ("add", 1, 0, -1), + ("scale", 0, 0, 2), ("add", 0, 1, 1)) + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def read_limited(path): + with path.open("rb") as stream: + data = stream.read(262145) + require(len(data) <= 262144, "file size limit") + return data + + +def load_ports(): + data = read_limited(HERE.parents[1] / PORT_PATH) + require(hashlib.sha256(data).hexdigest() == PORT_SHA, "port source hash") + ports = json.loads(data) + require(isinstance(ports, list) and len(ports) == 104, "port shape") + require(all(type(p) is int and 0 < p < 512 for p in ports), "port range") + require(len(set(ports)) == 104, "port uniqueness") + return ports + + +def binary_rank(rows): + basis = [0] * 9 + for initial in rows: + value = initial + for bit in range(8, -1, -1): + if value >> bit & 1: + if basis[bit]: + value ^= basis[bit] + else: + basis[bit] = value + break + return sum(bool(v) for v in basis) + + +def scaled_root(port): + weight = port.bit_count() + if weight == 3: + return tuple(2 if port >> bit & 1 else -1 for bit in range(9)) + require(weight == 7, "root weight") + zeros = [bit for bit in range(9) if not port >> bit & 1] + return tuple(3 if bit == zeros[0] else -3 if bit == zeros[1] else 0 + for bit in range(9)) + + +def gram(left, right): + return Q(sum(a * b for a, b in zip(scaled_root(left), scaled_root(right), + strict=True)), 9) + + +def witness(ports): + x, y, z = 11, 19, 487 + require(all(p in ports for p in (x, y, z)), "triangle membership") + common = [p for p in ports if not (p & x).bit_count() % 2 + and not (p & y).bit_count() % 2] + require(len(common) == 24 and z in common, "common section") + require(binary_rank((x, y)) == 2, "seven-frame rank") + require(all(binary_rank((x, y, n)) == 3 for n in (455, 56)), "six-frame rank") + first = [not (p & 455).bit_count() % 2 for p in common] + second = [not (p & 56).bit_count() % 2 for p in common] + require(all(a != b for a, b in zip(first, second, strict=True)), "complement") + require(sum(first) == 16 and sum(second) == 8, "section sizes") + plus = tuple(gram(x, p) / 2 for p in common) + minus = tuple(gram(y, p) / 2 for p in common) + c = tuple(Q(0) if p == z else value for p, value in zip(common, plus, strict=True)) + e = tuple(value - base for value, base in zip(plus, c, strict=True)) + require(minus == tuple(a - b for a, b in zip(c, e, strict=True)), "Gram targets") + require(all(c[i] for i, p in enumerate(common) if p != z), "broad support") + a = tuple(value if inside else Q(0) for value, inside in zip(c, first, strict=True)) + d = tuple(value - part for value, part in zip(c, a, strict=True)) + incoming = [list(e) + [Q(0)], list(a) + [Q(-1)], list(d) + [Q(1)]] + expected = [list(plus) + [Q(0)], list(minus) + [Q(0)], incoming[2][:]] + require([sum(bool(v) for v in row[:-1]) for row in incoming] == [1, 15, 8], + "incoming live supports") + return common, incoming, expected + + +def execute(rows, word): + require(len(rows) == 3 and 1 <= len(rows[0]) <= 25, "register shape") + require(all(len(row) == len(rows[0]) for row in rows), "register widths") + require(len(word) <= 4, "word bound") + result = [row[:] for row in rows] + for operation, target, source, coefficient in word: + require(0 <= target < 3 and 0 <= source < 3, "event index") + if operation == "add": + require(target != source, "ADD alias") + result[target] = [a + coefficient * b for a, b in + zip(result[target], result[source], strict=True)] + else: + require(operation == "scale" and coefficient != 0, "SCALE contract") + result[target] = [coefficient * a for a in result[target]] + return result + + +def local_checks(incoming, expected): + result = execute(incoming, WORD) + require(result == expected, "response endpoint") + inverse = tuple((op, target, source, -Q(coef) if op == "add" else 1 / Q(coef)) + for op, target, source, coef in reversed(WORD)) + require(execute(result, inverse) == incoming, "literal inverse") + cases = 0 + for clean, left, right, dirt in itertools.product(range(-2, 3), repeat=4): + start = [[Q(clean)], [Q(left - dirt)], [Q(right + dirt)]] + end = [[Q(left + right + clean)], [Q(left + right - clean)], start[2][:]] + require(execute(start, WORD) == end, "dirty scalar endpoint") + require(execute(end, inverse) == start, "dirty scalar inverse") + cases += 1 + return {"symbolic_input_columns": 25, "dirty_scalar_cases": cases, + "forward_events": len(WORD), "inverse_events": len(inverse)} + + +def mod_rank(rows): + matrix = [[entry % 3 for entry in row] for row in rows] + pivot = 0 + for column in range(len(matrix[0])): + candidates = [i for i in range(pivot, len(matrix)) if matrix[i][column]] + if not candidates: + continue + index = candidates[0] + matrix[pivot], matrix[index] = matrix[index], matrix[pivot] + factor = pow(matrix[pivot][column], -1, 3) + matrix[pivot] = [(factor * v) % 3 for v in matrix[pivot]] + for row in range(len(matrix)): + if row != pivot: + factor = matrix[row][column] + matrix[row] = [(a - factor * b) % 3 for a, b in + zip(matrix[row], matrix[pivot], strict=True)] + pivot += 1 + if pivot == len(matrix): + break + return pivot + + +def kernel_image(rows, dirt): + pivot = next(i for i in range(3) if dirt[i]) + return [tuple((rows[j][k] - dirt[j] * rows[pivot][k]) % 3 for k in range(4)) + for j in range(3) if j != pivot] + + +def small_census(): + # F3^4, support <=2. Normalize nonzero dirt entries to one by row scaling. + pool = [r for r in itertools.product(range(3), repeat=4) if sum(bool(x) for x in r) <= 2] + patterns = [b for b in itertools.product(range(2), repeat=3) if any(b)] + target = [(1, 1, 1, 1, 0), (2, 1, 1, 1, 0)] + require(len(pool) == 33 and len(patterns) == 7, "small-domain bounds") + totals, feasible = [0, 0, 0], [0, 0, 0] + oracle_cases = 0 + for rows in itertools.product(pool, repeat=3): + for dirt in patterns: + image = kernel_image(rows, dirt) + in_space = all(r[1] == r[2] == r[3] for r in image) + determinant = (image[0][0] * image[1][1] - image[1][0] * image[0][1]) % 3 + succeeds = in_space and determinant != 0 + weight = sum(dirt) + totals[weight - 1] += 1 + if succeeds: + feasible[weight - 1] += 1 + require(weight >= 2, "isolated-dirt theorem") + if weight == 2: + clean = dirt.index(0) + require(rows[clean][0] != 0 and rows[clean][1:] == (0, 0, 0), + "clean singleton theorem") + dirty = [i for i in range(3) if dirt[i]] + require(all(any(rows[i][k] for i in dirty) for k in range(1, 4)), + "dirty union theorem") + # Full augmented-row elimination does not use the kernel formula. + augmented = [tuple(row) + (b,) for row, b in zip(rows, dirt, strict=True)] + direct = mod_rank(augmented + target) == mod_rank(augmented) + require(direct == succeeds, "independent augmented-rank oracle") + oracle_cases += 1 + return {"F3_cases": sum(totals), "F3_cases_by_dirty_weight": totals, + "F3_feasible_by_dirty_weight": feasible, "independent_rank_cases": oracle_cases} + + +def rejection_controls(incoming, expected): + failures = [] + for index in range(4): + failures.append((incoming, WORD[:index] + WORD[index + 1:])) + failures.append((incoming, WORD[:2] + (("scale", 0, 0, 1),) + WORD[3:])) + bad_dirt = [row[:] for row in incoming] + bad_dirt[1][-1] = Q(0) + failures.append((bad_dirt, WORD)) + same_sign = [row[:] for row in incoming] + same_sign[1][-1] = Q(1) + failures.append((same_sign, WORD)) + bad_singleton = [row[:] for row in incoming] + bad_singleton[0][0] += 1 + failures.append((bad_singleton, WORD)) + for rows, word in failures: + require(execute(rows, word) != expected, "endpoint mutant escaped") + invalid = ((("add", 0, 0, 1),), (("scale", 0, 0, 0),), (("other", 0, 0, 1),)) + for word in invalid: + try: + execute(incoming, word) + except ValueError: + continue + raise ValueError("invalid event escaped") + return len(failures) + len(invalid) + + +def scope_controls(): + # The isolated-dirt conclusion fails once a clean row may carry all of c. + rows = [(0, 1, 1, 1, 0), (1, 0, 0, 0, 0), (0, 0, 0, 0, 1)] + targets = [(1, 1, 1, 1, 0), (2, 1, 1, 1, 0)] + require(mod_rank(rows + targets) == mod_rank(rows), "support-limit escape") + # The full-rank argument also requires a nonzero dirt vector. + clean = [(1, 0, 0, 0, 0), (0, 1, 1, 0, 0), (0, 0, 0, 1, 0)] + require(mod_rank(clean + targets) == mod_rank(clean), "zero-dirt escape") + return 2 + + +def main(): + ports = load_ports() + common, incoming, expected = witness(ports) + result = {"marker": "PASS_P104_WIRE_DIRTY_ENTRY", "claim_type": "scoped-response-proof", + "triangle": [11, 19, 487], "common_ports": common, + "incoming_live_supports": [1, 15, 8], "source_sha256": PORT_SHA} + result.update(local_checks(incoming, expected)) + result.update(small_census()) + result["rejecting_controls"] = rejection_controls(incoming, expected) + result["outside_scope_positive_controls"] = scope_controls() + names = ("README.md", "PROOF.md", "verify.py", "TASK.json", "SOURCES.json", "VERIFY.json") + result["package_sha256"] = {name: hashlib.sha256(read_limited(HERE / name)).hexdigest() + for name in names} + print(json.dumps(result, indent=2, sort_keys=True)) + + +if __name__ == "__main__": + main()