diff --git a/research/p104-correction-support-floor/ORIGIN.json b/research/p104-correction-support-floor/ORIGIN.json new file mode 100644 index 0000000000..d5d518429f --- /dev/null +++ b/research/p104-correction-support-floor/ORIGIN.json @@ -0,0 +1,13 @@ +{ + "repository": "aliromman/integer-mult-bounds", + "pull_request": "https://github.com/CrocSwap/integer-mult-bounds/pull/6537", + "head": "8bc9f991afe9fde83700ff86e520230eaa4595e7", + "path": "research/p104-sparse-output-correction/RESULT.json", + "git_blob": "ed1c1b586b68c0e9d04b716ff46d75b5379c66e1", + "sha256": "4b95cc8cc0de0413ac8dcca49b13cb13abb85aad67e28bc988a55f1483f53a2e", + "retained_file": "inputs/pr6537-RESULT.json", + "used_fields": [ + "correction" + ], + "author": "Ali Romman" +} diff --git a/research/p104-correction-support-floor/PROOF.md b/research/p104-correction-support-floor/PROOF.md new file mode 100644 index 0000000000..78d7ea472b --- /dev/null +++ b/research/p104-correction-support-floor/PROOF.md @@ -0,0 +1,102 @@ +# A 38-ADD floor for the sparse P104 correction + +This contribution was produced by Nick Petalas. Apache-2.0. + +## Model and result + +Let C be the exact 799-coordinate rational operator defined by the 74 ADDs in +Ali Romman's PR6537, head `8bc9f991afe9fde83700ff86e520230eaa4595e7`. +The original RESULT.json is retained byte for byte in `inputs/`. Its construction, +factorization, upper bound and relationship to PR6529 are credited premises. +This package does not replay the old correction or the whole supplier. + +Registers initially contain independent scalar inputs. A circuit uses +`r_i <- r_i + c*r_j`, with i distinct from j, and nonzero scalar SCALEs. +The ADD coefficient may be any rational number. SCALEs are free for this lower +bound. The circuit must finish with C on the original coordinates and restore +every additional dirty register. Any finite number of additional dirty or +zero-initialized registers is permitted. They initially contain no precomputed +linear combinations of the original inputs. Register names are fixed. + +**Theorem.** Every such circuit uses at least 38 ADDs. + +Thus the predecessor's 28 to 74 ADD gap becomes 38 to 74. This does not prove +that 38 or 74 is the optimum. It does not lower the source's scalar allowance +or change any productive or paid recursive rank. + +## General first-final-ADD lemma + +Suppose B specified output registers each have final coefficient support at +least s, where B is positive and s is at least two. Support means the number +of independent initial input coordinates with nonzero coefficient. Then any +circuit in the model above uses at least + +`B + s - 2` + +ADDs. No restrictions on cancellation, feedback, coefficient magnitudes, +interleaving or workspace size are needed. + +Each specified register must receive an ADD: its initial support is at most +one, and SCALE cannot increase support. For each, mark its last ADD. These B +marked events are distinct because an ADD changes only its destination. +Let t be the earliest marked event. Subsequent SCALEs of its destination +have nonzero coefficients and preserve its support. Its row immediately +after t therefore already has support at least s. + +Consider the arithmetic dependency graph of that row at this prefix. Give +each initial scalar coordinate one leaf, each SCALE one unary vertex, and +each ADD one binary vertex. Retain only ancestors of the row. The underlying +undirected graph is connected. If it has L input leaves, U unary vertices and +A binary vertices, it has at most U+2A edges and L+U+A vertices. Connectedness +gives `U+2A >= L+U+A-1`, hence `A >= L-1`. At least s distinct input leaves +occur because the row has s nonzero coefficients. Cancellation can introduce +additional leaves but cannot remove this requirement. Thus the prefix through +t contains at least s-1 ADDs. + +The other B-1 marked events lie strictly after t. They are not among those +prefix ADDs. The total is at least `(s-1)+(B-1)=B+s-2`. + +The argument includes workspace leaves, even if their final coefficients +cancel. It actually does not need workspace restoration, so imposing that +requirement cannot weaken the bound. Clean registers contribute zero-valued +leaves and do not reduce the number of independent leaves needed by the row. + +As a function of B and s alone the lemma is sharp. Form a sum of s inputs +in one of those input registers using s-1 ADDs. Add that register to each of +B-1 other input registers. Exactly B outputs have support at least s; their +support sizes are s and s+1. The circuit uses B+s-2 ADDs. This is a generic +attainment example, not an implementation of C. + +## Exact specialization + +The verifier reads only the `correction` array of the retained source result. +It extracts its rational rows in two ways: forward row operations and backward +propagation of one output covector. It compares all 799 rows. This computes +the new support statistic; it does not check the predecessor's supplier claims. + +There are 28 rows different from the corresponding identity row. Their complete +support histogram is `{12:3, 13:19, 25:6}`. Rows 3, 372 and 382 have support 12. +The verifier prints every changed row and its support. Hence B=28 and s=12, +giving `28+12-2=38`. + +The written argument proves the lower bound for every permitted circuit. +The finite replay corroborates the specialization and checks the lemma on +all 9,331 three-register binary ADD words of lengths zero through five and +56 attaining examples. Six malformed-support controls and three source-byte +corruption controls reject. These finite checks are not an exhaustive search +for rational circuits implementing C. + +## Boundaries + +Free register permutations, multi-target operations, COPY, INIT/CLEAR inside +the circuit, native maps, nonlinear operations, precomputed input encodings +and approximate or rounded implementation are outside this model. A circuit +with such operations needs a separate lower-bound argument. SCALEs are +nonzero; every actual scalar and routing cost remains payable by a consumer. +The theorem requires the complete operator C on independent coordinates. +Matching C only on states reachable from a particular preceding supplier +word is a different problem and is not covered by this bound. + +This local arithmetic floor does not prove supplier admission, a complete +multiplication theorem or a new kappa. All five selected framework assumptions +remain. Independent human and formal proof-kernel review are unclaimed. diff --git a/research/p104-correction-support-floor/README.md b/research/p104-correction-support-floor/README.md new file mode 100644 index 0000000000..e32b7c80a3 --- /dev/null +++ b/research/p104-correction-support-floor/README.md @@ -0,0 +1,91 @@ +# The sparse P104 correction needs at least 38 ADDs + +This contribution was produced by Nick Petalas. Apache-2.0. + +The exact correction operator constructed by Ali Romman in +[PR6537](https://github.com/CrocSwap/integer-mult-bounds/pull/6537) needs at least +38 one-target ADDs, even with free nonzero SCALEs, arbitrary rational ADD +coefficients and arbitrary restored dirty workspace. This raises the prior +target-write lower bound from 28 to 38. The credited 74-ADD construction remains +the upper bound. Claim type: scoped written proof with exact finite support +evidence. No new kappa or selected-frontier change is claimed. + +[PROOF.md](PROOF.md) gives the general lemma. If B specified outputs each have +support at least s>=2, the first output to receive its final ADD needs at least +s-1 ADDs in its dependency graph; the other B-1 final ADDs come later. Thus +there are at least B+s-2 ADDs. The source operator has 28 changed rows and +minimum support 12. The complete histogram is `{12:3,13:19,25:6}`. + +This settles a bounded part of PR6537's open unrestricted circuit gap. It +changes the task card from productive helper splitting to a local correction +obstruction. The result constrains scalar resynthesis after a changed native +boundary; it does not change the recursive moment or provide an actual supplier. + +## Reproduction + +From the repository root: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B research/p104-correction-support-floor/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/p104-correction-support-floor +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/p104-correction-support-floor --check-source-history +``` + +Any CPython 3.12 standard-library installation can run the direct verifier. +It writes only stdout. Normal and optimized registered checks extract all +799 rows independently, print every changed support, examine all 9,331 binary +words through length five, check 56 sharp examples and reject six invalid +support declarations and three actual byte corruptions. The success marker is +`PASS_P104_CORRECTION_SUPPORT_FLOOR`. The replay does not run or audit a +predecessor verifier. + +The original source RESULT.json and NOTICE are retained byte for byte at the +head named in ORIGIN.json. The original blob and SHA256 are checked directly; +no unmerged Git commit, network access or predecessor executable is required. +SOURCES.json pins the task catalogue and selected record as historical +provenance. The retained source data is authenticated by ORIGIN.json rather +than an unavailable side-branch ancestry pin. Only its `correction` array is +used. Other numbers in the imported result are neither recomputed nor adopted +as new claims here. + +## Limitations and verification scope + +The exact optimum remains between 38 and the credited 74. The model uses fixed +register names and ADD/SCALE operations. Free permutations, multi-target calls, +native maps, COPY and in-circuit resets need different arguments. The theorem +requires the complete operator on independent coordinates; a restriction to +states reachable from a preceding word is outside the claim. The theorem +is a written proof, not a proof-kernel result. Native/compiler, ownership, +physical scalar and tape costs, rounding, stock and analytic recovery remain +outside the result. All five selected framework assumptions remain. + +The verifier uses bounded Python allocations, a managed-runtime deviation from +Power of Ten rule 3. Live symbolic storage is at most 799 rows of 799 rational +entries and one backward row; gate count is fixed at 74. Binary enumeration +uses three integer rows and a word of length at most five. Rational sizes are +bounded by those 74 pinned coefficients. Functions stay below 60 lines, loops +have explicit finite domains, and explicit exceptions preserve checks under +optimization. Warning-strict normal and optimized replay supply the available +Python diagnostics. No shared configuration or historical verifier is changed. + +## Open next questions + +- Can a cancellation-sensitive circuit invariant raise 38? Start with the + dependency graph of one of the three support-12 rows. The support lemma + alone is sharp and cannot settle this operator's optimum. +- Can interleaved synthesis lower 74? Start with a new exact ADD/SCALE word + and prove its arbitrary-input endpoint, then charge every scalar operation + and any changed physical boundary. This lower bound supplies no such word. + +## Credit and related work + +Ali Romman supplied PR6537's correction, factorization and open circuit gap. +Credit PR6529, Rohan Arun's PR6399, Erwan L.'s PR6453 and the retained P104 +lineage. The imported NOTICE is unchanged. Arithmetic dependency-graph +counting is classical; the new contribution is its first-final-ADD application +and the 38 floor for this exact operator. + +PR6542 gives a rounded implementation of the same correction; it asks a +different precision question. PR6529 is its native-transport predecessor. +Neither is replayed here. Independent human and formal proof-kernel review +are unclaimed. diff --git a/research/p104-correction-support-floor/SOURCES.json b/research/p104-correction-support-floor/SOURCES.json new file mode 100644 index 0000000000..594089b9c7 --- /dev/null +++ b/research/p104-correction-support-floor/SOURCES.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "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" + } + ] +} diff --git a/research/p104-correction-support-floor/TASK.json b/research/p104-correction-support-floor/TASK.json new file mode 100644 index 0000000000..8e35b5637d --- /dev/null +++ b/research/p104-correction-support-floor/TASK.json @@ -0,0 +1,137 @@ +{ + "schema_version": 1, + "task_id": "p104-side-correction", + "priority_revision": 8, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "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": "Prove a new lower bound of 38 ADDs for the exact PR6537 output correction, with arbitrary rational coefficients, free nonzero SCALEs and restored arbitrary dirty workspace.", + "scope_change_reason": "Take PR6537's explicit open circuit gap instead of constructing another helper split. This is a local scalar obstruction on a changed native boundary, not a recursive moment improvement.", + "bottleneck_link": "Correction synthesis is part of the complete boundary bill. This limits one exact correction operator without treating physical delivery or scalar costs as zero.", + "budget_minutes": 60, + "stop_rule": "Ship the first verified original lower-bound improvement; stop research once 38 is proved.", + "outcome": "completed", + "evidence": "PROOF.md; verify.py prints all changed supports, complete 799-row forward/backward agreement, 9331 small binary words, 56 sharp examples and nine rejection controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can cancellation-sensitive information raise the 38-ADD floor for this exact operator?", + "why_it_matters": "The generic support bound is sharp but leaves a 36-ADD optimum gap.", + "first_step": "Analyze a dependency graph completing one of rows 3, 372 or 382 and the later required outputs.", + "blocked_by": "Support sizes alone do not distinguish this operator from the generic attaining family." + }, + { + "question": "Can an interleaved exact scalar circuit lower the 74-ADD upper bound?", + "why_it_matters": "A smaller correction can reduce ordinary boundary work without changing the recursive profile.", + "first_step": "Construct one literal word, prove its arbitrary-input operator, and price every scalar operation.", + "blocked_by": "No attaining circuit below 74 or physical replacement is supplied." + } + ], + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19371027", + "environment": { + "python": "3.12.15", + "platform": "macOS-27.0.1-arm64-arm-64bit", + "executable": "/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12" + }, + "overlap": { + "checked_at": "2026-11-03T09:57:49Z", + "main": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "open_prs": 521, + "discussion_records": 6526, + "local_notes": 8917, + "limitations": "Open bodies, discussion comments and tracked local notes are searched; arbitrary diffs, unpublished work and later updates are outside the snapshot." + } +} diff --git a/research/p104-correction-support-floor/VERIFY.json b/research/p104-correction-support-floor/VERIFY.json new file mode 100644 index 0000000000..6cc1241b90 --- /dev/null +++ b/research/p104-correction-support-floor/VERIFY.json @@ -0,0 +1,32 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact source-specific supports, written lower-bound specialization and bounded theorem controls." + }, + { + "argv": [ + "{python}", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Same checks under optimization, including all rejection paths." + } + ] +} diff --git a/research/p104-correction-support-floor/inputs/pr6529-NOTICE b/research/p104-correction-support-floor/inputs/pr6529-NOTICE new file mode 100644 index 0000000000..3d9b7e4c8b --- /dev/null +++ b/research/p104-correction-support-floor/inputs/pr6529-NOTICE @@ -0,0 +1,21 @@ +Scaled transport fusion +Copyright 2026 Ali Romman. Apache-2.0. + +New construction and package: Ali Romman, with substantial OpenAI Codex +assistance. No subagents were used. + +The method extends Rohan Arun's PR6399 donor transport merge to intervals +with a scalar rescaling. His PR6417 supplies the clean mixed composition. +Erwan L., with the assistance disclosed in PR6453, supplies the third-anchor +stack used as the exact source. DreamingOfClouds supplies the PR6375 lifts +and retained native optimizations. Those contributions are not new here. + +Ali Romman's earlier contact basis and mixed caller retain their prior credit. +Cinna Davis, David Arias, Gareth Davidson, Jacob Alan Sussman, zxv, Cao Yifan, +Douglas Colkitt, and all retained native, helper, BIT, compiler and analytic +authors keep their credit. Tekalign's package exporter supplies source.tar. +The complete original notices and source attributions remain unchanged inside +that archive and its nested source archives. + +The exact source is CrocSwap/integer-mult-bounds PR6453, +b1a3e525793eca35c56324aa7ffd0b714cf606d4. diff --git a/research/p104-correction-support-floor/inputs/pr6537-NOTICE b/research/p104-correction-support-floor/inputs/pr6537-NOTICE new file mode 100644 index 0000000000..41f10930ae --- /dev/null +++ b/research/p104-correction-support-floor/inputs/pr6537-NOTICE @@ -0,0 +1,4 @@ +New correction and verification: Ali Romman with substantial OpenAI Codex assistance. +Apache-2.0. No subagents. +PR6529, Rohan Arun PR6399, Erwan L. PR6453 and all predecessor authors retain credit. +Read inputs/pr6529-NOTICE and the original inputs/local.py header for source attribution. diff --git a/research/p104-correction-support-floor/inputs/pr6537-RESULT.json b/research/p104-correction-support-floor/inputs/pr6537-RESULT.json new file mode 100644 index 0000000000..ed1c1b586b --- /dev/null +++ b/research/p104-correction-support-floor/inputs/pr6537-RESULT.json @@ -0,0 +1,660 @@ +{ + "changed_rows": 28, + "complete_after": { + "endpoint_coefficients": 638401, + "helpers": { + "1": 14, + "2": 8, + "3": 4, + "4": 107, + "5": 15, + "6": 3, + "7": 9, + "8": 39, + "9": 363 + }, + "owned_fields": 29, + "owned_lifetimes": 45, + "paid": { + "1": 2234, + "2": 453, + "3": 491, + "4": 107, + "5": 153, + "6": 8, + "7": 9, + "8": 1 + }, + "paid_rank_mass": 5925, + "peak_owned_fields": 13, + "public_inputs": 770, + "real_scalar_allowance": 132256 + }, + "complete_before": { + "endpoint_coefficients": 638401, + "helpers": { + "1": 14, + "2": 8, + "3": 4, + "4": 107, + "5": 15, + "6": 3, + "7": 9, + "8": 39, + "9": 363 + }, + "owned_fields": 29, + "owned_lifetimes": 45, + "paid": { + "1": 2234, + "2": 453, + "3": 491, + "4": 107, + "5": 153, + "6": 8, + "7": 9, + "8": 1 + }, + "paid_rank_mass": 5925, + "peak_owned_fields": 13, + "public_inputs": 770, + "real_scalar_allowance": 137218 + }, + "complete_growth_after": { + "first_event": 15828, + "maximum_entry": "17", + "maximum_row_l1": "838" + }, + "complete_growth_before": { + "first_event": 15828, + "maximum_entry": "17", + "maximum_row_l1": "838" + }, + "correction": [ + [ + "ADD", + 372, + 3, + "1", + 127 + ], + [ + "ADD", + 372, + 8, + "1", + 127 + ], + [ + "ADD", + 372, + 26, + "-1", + 127 + ], + [ + "ADD", + 372, + 66, + "1", + 127 + ], + [ + "ADD", + 372, + 67, + "-1", + 127 + ], + [ + "ADD", + 372, + 80, + "1", + 127 + ], + [ + "ADD", + 372, + 88, + "-1", + 127 + ], + [ + "ADD", + 372, + 95, + "-1", + 127 + ], + [ + "ADD", + 372, + 368, + "-1", + 127 + ], + [ + "ADD", + 372, + 382, + "1", + 127 + ], + [ + "ADD", + 372, + 383, + "-3", + 127 + ], + [ + "ADD", + 1, + 6, + "-1", + 127 + ], + [ + "ADD", + 1, + 28, + "-1", + 127 + ], + [ + "ADD", + 1, + 58, + "1", + 127 + ], + [ + "ADD", + 1, + 75, + "-1", + 127 + ], + [ + "ADD", + 1, + 82, + "1", + 127 + ], + [ + "ADD", + 1, + 86, + "1", + 127 + ], + [ + "ADD", + 1, + 93, + "-1", + 127 + ], + [ + "ADD", + 1, + 336, + "1", + 127 + ], + [ + "ADD", + 1, + 340, + "-1", + 127 + ], + [ + "ADD", + 1, + 350, + "-1", + 127 + ], + [ + "ADD", + 1, + 351, + "3", + 127 + ], + [ + "ADD", + 3, + 372, + "1", + 127 + ], + [ + "ADD", + 146, + 372, + "-1/4", + 127 + ], + [ + "ADD", + 151, + 1, + "1/4", + 127 + ], + [ + "ADD", + 205, + 1, + "-1/4", + 127 + ], + [ + "ADD", + 256, + 372, + "1/4", + 127 + ], + [ + "ADD", + 257, + 372, + "-1/4", + 127 + ], + [ + "ADD", + 258, + 1, + "1/4", + 127 + ], + [ + "ADD", + 261, + 372, + "-1/4", + 127 + ], + [ + "ADD", + 262, + 1, + "-1/4", + 127 + ], + [ + "ADD", + 265, + 1, + "-1/4", + 127 + ], + [ + "ADD", + 266, + 1, + "-1/4", + 127 + ], + [ + "ADD", + 269, + 372, + "1/4", + 127 + ], + [ + "ADD", + 270, + 372, + "-1/4", + 127 + ], + [ + "ADD", + 342, + 1, + "1/2", + 127 + ], + [ + "ADD", + 343, + 1, + "-1", + 127 + ], + [ + "ADD", + 344, + 1, + "-1/2", + 127 + ], + [ + "ADD", + 348, + 1, + "-1/2", + 127 + ], + [ + "ADD", + 374, + 372, + "1/2", + 127 + ], + [ + "ADD", + 380, + 372, + "1/2", + 127 + ], + [ + "ADD", + 382, + 372, + "-1/2", + 127 + ], + [ + "ADD", + 711, + 1, + "1/4", + 127 + ], + [ + "ADD", + 372, + 1, + "-1", + 127 + ], + [ + "ADD", + 173, + 372, + "1/4", + 127 + ], + [ + "ADD", + 263, + 372, + "1/4", + 127 + ], + [ + "ADD", + 271, + 372, + "-1/4", + 127 + ], + [ + "ADD", + 734, + 372, + "1/2", + 127 + ], + [ + "ADD", + 372, + 1, + "2", + 127 + ], + [ + "ADD", + 133, + 372, + "1/4", + 127 + ], + [ + "ADD", + 268, + 372, + "1/4", + 127 + ], + [ + "ADD", + 372, + 1, + "-1", + 127 + ], + [ + "ADD", + 1, + 351, + "-3", + 127 + ], + [ + "ADD", + 1, + 350, + "1", + 127 + ], + [ + "ADD", + 1, + 340, + "1", + 127 + ], + [ + "ADD", + 1, + 336, + "-1", + 127 + ], + [ + "ADD", + 1, + 93, + "1", + 127 + ], + [ + "ADD", + 1, + 86, + "-1", + 127 + ], + [ + "ADD", + 1, + 82, + "-1", + 127 + ], + [ + "ADD", + 1, + 75, + "1", + 127 + ], + [ + "ADD", + 1, + 58, + "-1", + 127 + ], + [ + "ADD", + 1, + 28, + "1", + 127 + ], + [ + "ADD", + 1, + 6, + "1", + 127 + ], + [ + "ADD", + 372, + 383, + "3", + 127 + ], + [ + "ADD", + 372, + 382, + "-1", + 127 + ], + [ + "ADD", + 372, + 368, + "1", + 127 + ], + [ + "ADD", + 372, + 95, + "1", + 127 + ], + [ + "ADD", + 372, + 88, + "1", + 127 + ], + [ + "ADD", + 372, + 80, + "-1", + 127 + ], + [ + "ADD", + 372, + 67, + "1", + 127 + ], + [ + "ADD", + 372, + 66, + "-1", + 127 + ], + [ + "ADD", + 372, + 26, + "1", + 127 + ], + [ + "ADD", + 372, + 8, + "-1", + 127 + ], + [ + "ADD", + 372, + 3, + "-1", + 127 + ] + ], + "correction_after": { + "gates": 74, + "prefix_l1": "28", + "scalar": 696 + }, + "correction_before": { + "gates": 569, + "prefix_l1": "21", + "scalar": 5658 + }, + "doubled_controls": 74, + "forms": [ + { + "26": "-1", + "3": "1", + "368": "-1", + "372": "1", + "382": "1", + "383": "-3", + "66": "1", + "67": "-1", + "8": "1", + "80": "1", + "88": "-1", + "95": "-1" + }, + { + "1": "1", + "28": "-1", + "336": "1", + "340": "-1", + "350": "-1", + "351": "3", + "58": "1", + "6": "-1", + "75": "-1", + "82": "1", + "86": "1", + "93": "-1" + } + ], + "independent_correction_columns": 799, + "invalid_controls": 5, + "invariant_pairings": 4, + "minimizing_programs": 44, + "omission_controls": 74, + "programs_searched": 78408, + "rank": 2, + "saved_eighteen_calls": 89316, + "saved_real_scalar_per_native": 4962, + "scope": "Exact source-bound ordinary correction reduction. Native paid profile and kappa are unchanged.", + "selected": [ + 372, + 1, + "1", + "1", + -1 + ], + "source_corruptions": 6, + "source_head": "44b0d0e8961201ac1656490b4384a7752e1cd9c5", + "status": "PASS_P104_74_GATE_CORRECTION", + "transpose": { + "arithmetic": "Dense integer rows with binary denominators; reverse chronology", + "coefficients": 638401, + "columns": 799 + }, + "whole_word_controls": 3 +} diff --git a/research/p104-correction-support-floor/verify.py b/research/p104-correction-support-floor/verify.py new file mode 100644 index 0000000000..f3ed3ef5d7 --- /dev/null +++ b/research/p104-correction-support-floor/verify.py @@ -0,0 +1,161 @@ +"""Exact support evidence for the first-final-ADD lower bound. + +Produced by Nick Petalas. Apache-2.0. +The imported correction operator is Ali Romman's PR6537 construction. +""" + +import hashlib +import itertools +import json +from collections import Counter +from fractions import Fraction +from pathlib import Path + + +PACKAGE = Path(__file__).resolve().parent +DIMENSION = 799 + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def authenticate(raw, origin): + require(len(raw) <= 1024 * 1024, "Source exceeds one MiB") + require(hashlib.sha256(raw).hexdigest() == origin["sha256"], "Source hash") + blob = hashlib.sha1(b"blob " + str(len(raw)).encode() + b"\0" + raw).hexdigest() + require(blob == origin["git_blob"], "Source Git blob") + + +def load_program(): + origin = json.loads((PACKAGE / "ORIGIN.json").read_text(encoding="utf-8")) + source = PACKAGE / "inputs/pr6537-RESULT.json" + require(source.stat().st_size <= 1024 * 1024, "Source size") + raw = source.read_bytes() + authenticate(raw, origin) + program = json.loads(raw)["correction"] + require(isinstance(program, list) and len(program) == 74, "74 source gates") + for gate in program: + require(isinstance(gate, list) and len(gate) == 5, "Gate shape") + op, dst, src, coefficient, frame = gate + require(op == "ADD" and frame == 127, "Exact common-frame ADD") + require(type(dst) is int and type(src) is int, "Integer register") + require(0 <= dst < DIMENSION and 0 <= src < DIMENSION, "Register range") + require(dst != src and isinstance(coefficient, str), "ADD operands") + require(len(coefficient) <= 32 and Fraction(coefficient) != 0, "Coefficient") + return program, raw, origin + + +def forward_rows(program): + rows = [{i: Fraction(1)} for i in range(DIMENSION)] + for _, dst, src, coefficient, _ in program: + scale = Fraction(coefficient) + for column, value in tuple(rows[src].items()): + total = rows[dst].get(column, Fraction(0)) + scale * value + if total: + rows[dst][column] = total + else: + rows[dst].pop(column, None) + return rows + + +def backward_row(program, output): + row = {output: Fraction(1)} + for _, dst, src, coefficient, _ in reversed(program): + total = row.get(src, Fraction(0)) + row.get(dst, Fraction(0)) * Fraction(coefficient) + if total: + row[src] = total + else: + row.pop(src, None) + return row + + +def support_floor(sizes): + require(len(sizes) <= DIMENSION, "Output count bound") + require(all(type(s) is int and 2 <= s <= DIMENSION for s in sizes), "Dense rows") + return len(sizes) + min(sizes) - 2 if sizes else 0 + + +def binary_controls(): + gates = tuple((dst, src) for dst in range(3) for src in range(3) if dst != src) + checked = 0 + for length in range(6): + for word in itertools.product(gates, repeat=length): + rows = [1, 2, 4] + for dst, src in word: + rows[dst] ^= rows[src] + dense = [row.bit_count() for row in rows if row.bit_count() >= 2] + require(support_floor(dense) <= length, "Binary circuit violates bound") + checked += 1 + require(checked == sum(6**length for length in range(6)), "Complete word count") + return checked + + +def sharp_controls(): + checked = 0 + for count in range(1, 9): + for size in range(2, 9): + rows = [1 << i for i in range(size + count - 1)] + for src in range(1, size): + rows[0] ^= rows[src] + for dst in range(size, size + count - 1): + rows[dst] ^= rows[0] + dense = [row.bit_count() for row in rows if row.bit_count() >= 2] + require(len(dense) == count and min(dense) == size, "Attaining supports") + require(support_floor(dense) == count + size - 2, "Sharp general bound") + checked += 1 + return checked + + +def rejection_controls(raw, origin): + rejected = 0 + for sizes in ([1], [0], [-1], [800], [True], [2] * 800): + try: + support_floor(sizes) + except ValueError: + rejected += 1 + else: + raise ValueError("Invalid support accepted") + for changed in (raw + b"\n", raw[:-1], raw.replace(b"ADD", b"SUB", 1)): + require(changed != raw, "Actual byte corruption") + try: + authenticate(changed, origin) + except ValueError: + rejected += 1 + else: + raise ValueError("Changed source accepted") + return rejected + + +def main(): + program, raw, origin = load_program() + rows = forward_rows(program) + changed = [i for i in range(DIMENSION) if rows[i] != {i: Fraction(1)}] + for output in range(DIMENSION): + require(rows[output] == backward_row(program, output), "Independent row extraction") + sizes = [len(rows[i]) for i in changed] + histogram = dict(sorted(Counter(sizes).items())) + require(histogram == {12: 3, 13: 19, 25: 6}, "Complete support histogram") + floor = support_floor(sizes) + require(floor == 38 and len(changed) == 28, "Source-specific lower bound") + result = { + "status": "PASS_P104_CORRECTION_SUPPORT_FLOOR", + "claim_type": "scoped written circuit lower bound with exact finite support evidence", + "source_sha256": origin["sha256"], + "changed_rows": changed, + "row_supports": {str(i): len(rows[i]) for i in changed}, + "support_histogram": histogram, + "minimum_support": min(sizes), + "add_lower_bound": floor, + "credited_add_upper_bound": len(program), + "independent_rows": DIMENSION, + "binary_words": binary_controls(), + "sharp_fixtures": sharp_controls(), + "rejection_controls": rejection_controls(raw, origin), + } + print(json.dumps(result, indent=2, sort_keys=True)) + + +if __name__ == "__main__": + main()