From d0d8ae85a23b338f437ab0402126c7e5e1fc7ff7 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Tue, 3 Nov 2026 10:11:20 +0000 Subject: [PATCH] feat(research): prove exact shared atom-power crossover --- research/shared-atom-crossover/PROOF.md | 173 ++++++++++++++++++++ research/shared-atom-crossover/README.md | 132 +++++++++++++++ research/shared-atom-crossover/SOURCES.json | 30 ++++ research/shared-atom-crossover/TASK.json | 106 ++++++++++++ research/shared-atom-crossover/VERIFY.json | 32 ++++ research/shared-atom-crossover/oracle.py | 45 +++++ research/shared-atom-crossover/verify.py | 139 ++++++++++++++++ 7 files changed, 657 insertions(+) create mode 100644 research/shared-atom-crossover/PROOF.md create mode 100644 research/shared-atom-crossover/README.md create mode 100644 research/shared-atom-crossover/SOURCES.json create mode 100644 research/shared-atom-crossover/TASK.json create mode 100644 research/shared-atom-crossover/VERIFY.json create mode 100644 research/shared-atom-crossover/oracle.py create mode 100644 research/shared-atom-crossover/verify.py diff --git a/research/shared-atom-crossover/PROOF.md b/research/shared-atom-crossover/PROOF.md new file mode 100644 index 0000000000..120d115870 --- /dev/null +++ b/research/shared-atom-crossover/PROOF.md @@ -0,0 +1,173 @@ +# Exact crossover at fixed total exponent + +This scoped proof was produced by Nick Petalas. Apache-2.0. + +## 1. Contract and cited premise + +Fix integers I>=1 and w>=1. Three distinct owned Count outputs have borrowed, +canonical, unsigned I-bit exponents e_0,e_1,e_2, each in [0,2^I-1]. The fixed +radix is q and the admitted modulus is q^w. Compare the original and shared +atom-power methods of Tekalign / tekuuu's PR4077, at +90b658330f0357975337b41d67927ae84b72c851. Their successful-input equivalence, +blank-counter lifecycle and complete source-action difference in PROOF.md +sections 3 and 4 are cited premises. This proof does not verify those premises. + +An action here is one record, residue-Word or index-Word read, write or unit +move, with unit weight for each of those nine kinds. Let rho be the sum of +one complete radix validator's residue actions, including its cleanup. It is +an input to the theorem, not an estimated or newly measured source cost. +No physical exchange rate among the action kinds is assumed. + +Write E=sum e_j, k=#{j:e_j>0}, S=sum popcount(e_j), and +B=sum bitlength(e_j), using bitlength(0)=0. The main theorem concerns E>=2; +sections 2 and 4 also treat E=0 and E=1. + +## 2. Complete scalar cost identity + +For a positive exponent e with b=bitlength(e), the cited construction tariff +J, rundown R, probe P and index-copy C have the following scalar totals: + +``` +J(e,I) = 9I - 4b + 8, +R(e,I) = 15e - 5 popcount(e) + 9I + 29, +P(e,I) = 9I + b + 20, +C(I) = 5I + 7. +``` + +These follow by adding the three components of each cited vector. In R, +the +4b from the decrement sum cancels the -4b in J. A positive probe +closes its unconsumed counter, with scalar cost 5b+12. For e=0, the cited +R(0,I)=P(0,I), so the original rundown and new probe cancel exactly. + +For E>0, PR4077 section 4 therefore gives the exact old-minus-new scalar +saving + +``` +Delta = (E-1) rho - H(e_0,e_1,e_2;I,w), +H = 15(w-1)E - 5(w-1)S + B + k(14wI + 36w - 9). (1) +``` + +Indeed the non-radix overhead is +sum_(e_j>0) [(w-1)R(e_j,I) + P(e_j,I) + w C(I)]. Substitution yields (1). +This retains every negative savings lane in the original difference before +summing. Output Count operations cancel by the cited successful-input +contract. The identity adds no uncharged runtime selector. + +For E=0 both methods have the same probes/rundowns, no radix traversal and +no new index copies, hence Delta=0. Formula (1)'s (E-1)rho term must not be +used in that case. For E=1, exactly one exponent is one, and +H=14wI+46w-18>0; Delta=-H. Strict saving is impossible in both cases. + +## 3. An exact maximum with at most 24 states per bit + +Let H_max(I,w,E) maximize H over all ordered I-bit triples with sum E. +Every integer E in [0,3(2^I-1)] has such a triple. Put + +``` +C = 14wI + 36w - 9, +Q(e) = B - 5(w-1)S + Ck. +``` + +The first term 15(w-1)E in H is fixed. The following maximum-weight +binary carry calculation computes max Q and one attaining triple. + +Process bit positions i=I-1,...,0 from most significant to least +significant. A state is (c,A), where c in {0,1,2} is the outgoing carry +from bit i to bit i+1, and A is the three-bit mask of exponents with an +already nonzero higher prefix. Start at (floor(E/2^I),0), with score zero. +For each proposed operand-bit mask u in {0,...,7}, put + +``` +c' = E_i + 2c - popcount(u), +A' = A OR u. +``` + +Discard c' outside {0,1,2}. Otherwise move to (c',A') with added score + +``` +popcount(A') - 5(w-1)popcount(u) + + C [popcount(A')-popcount(A)]. (2) +``` + +Keep the largest score per new state and an attaining prefix. After the +last bit accept only carry zero; maximize over its active masks. Add +15(w-1)E to obtain H_max. Ties may retain any attaining prefix. + +To prove the arithmetic constraint, ordinary column addition says +popcount(u)+c'=E_i+2c. The initial high carry and final zero low carry +make these equations equivalent to the exact unreduced sum of the three +I-bit operands. Conversely, every such triple supplies a unique path of +bit masks and carries. Thus this procedure omits no triple and adds none. + +For each operand e, its active flag after processing bit i is one exactly +when e>=2^i. Summing that flag over all I positions gives bitlength(e). +The bit-mask populations sum to S. Newly active flags telescope to k. +Consequently the total of (2) is exactly Q(e). + +Two prefixes with the same (c,A) have the same legal suffixes and the +same additional scores. Keeping only the larger prefix score therefore +preserves a global optimum. Induction on the processed positions proves +exactness. The stored witness attains it. There are at most 3*8=24 states +and at most 8 proposed masks per state at every bit, so at most 192I mask +trials suffice. This is an arithmetic-operation bound. Integer bit costs, +witness storage and execution of the encoded source caller are separate. +The reference retains at most two state layers, each with 24 records and +three I-bit witness integers per record. + +## 4. Sharp uniform affordability criterion + +For E>=2, the shared method strictly saves scalar source actions for +EVERY ordered I-bit exponent triple of sum E if and only if + +``` +(E-1)rho > H_max(I,w,E). (3) +``` + +Sufficiency follows from (1) and the maximum. Necessity follows by +substituting its attaining triple. In particular, for integral rho the +least admissible threshold is + +``` +rho_min = floor(H_max(I,w,E)/(E-1)) + 1. (4) +``` + +Equality in (3) is not strict saving. The theorem is parametric in rho; +it does not assert that every small integer rho is realized by an actual +radix validator. + +The actual child-extent exponents of PR4077 section 5 are +(a,b-a-c,2n-b-c), whose sum is E=2(n-c). When all three fit I bits, +substituting this E into (3) gives a uniform sufficient condition without +knowing their placement. Its necessity is over ALL sum-E triples. Actual +Layout guards, the external gap and native child placements can restrict +that set, so no sharpness claim for those narrower geometries follows. + +## 5. First explicit strict improvement + +At I=4,w=1,E=10, formula (1) reduces to H=B+83k. If k<=2, then H<=174. +For k=3, having B>=9 would require either lengths at least (3,3,3), +(4,3,2), or (4,4,1), up to order. Their minimum positive sums are 12, +14 and 17 respectively. All exceed 10. Thus B<=8. The triple (4,4,2) +has B=8,k=3, so H_max=257. Equation (4) gives rho_min=29. + +At rho=29 the minimum saving is 9*29-257=4 actions. At rho=28 the same +witness loses five actions. The elementary separate bounds k<=3 and +B<=3I instead give H<=261 and only certify integral rho>=30. The exact +sum constraint therefore certifies the additional value rho=29. That +coarse comparison is derived here; it is not a previously published +PR4077 threshold or a newly measured physical speedup. + +## 6. Scope and next obligations + +The new result is the exact sum-conditioned cost maximum and crossover, +conditional on the cited lane tariffs. Classical binary digit dynamic +programming supplies the method. Finite checks corroborate its new maximum; +they neither audit PR4077's implementation nor replace this all-size proof. + +A runtime guard would have to obtain or encode rho and pay for selection. +A physical tariff would have to price the nine action kinds. A complete +caller still needs Context/directory composition, storage and backing, +source admission, payload, control, precision and restoration obligations. +All five selected framework assumptions remain. No complete multiplication +theorem, supplier admission or new kappa is claimed. Independent human and +formal proof-kernel review are unclaimed. diff --git a/research/shared-atom-crossover/README.md b/research/shared-atom-crossover/README.md new file mode 100644 index 0000000000..7838ef9af9 --- /dev/null +++ b/research/shared-atom-crossover/README.md @@ -0,0 +1,132 @@ +# Exact affordability of shared atom powers at fixed total exponent + +This contribution was produced by Nick Petalas. Apache-2.0. +Claim type: scoped written cost proof with exact finite corroboration. +No new kappa or selected-frontier change is claimed. + +For Tekalign / tekuuu's [PR4077](https://github.com/CrocSwap/integer-mult-bounds/pull/4077) +shared atom-power interface, the total exponent alone can certify that every +placement saves source actions. The new result computes the sharp threshold +for all three equal-width exponents with that total. It answers the package's +open parameter-region question using its exact tariffs as cited premises. +No predecessor executable or scientific replay is run. + +For I-bit exponents, radix width w, sum E>0, positive count k, total binary +population S and total bitlength B, the exact old-minus-new scalar saving is + +``` +Delta = (E-1)rho - H, +H = 15(w-1)E - 5(w-1)S + B + k(14wI+36w-9). +``` + +Here rho is the complete residue read/write/move total of one radix traversal. +Every record, residue and index action has unit weight. For E>=2, a binary +carry maximum with at most 24 states per bit computes H_max and an attaining +triple. Strict saving for every sum-E triple holds exactly when +`rho > H_max/(E-1)`. The all-zero case ties, and total one always loses. +[PROOF.md](PROOF.md) establishes the uniform theorem, carry invariant and +strict endpoint. The operation count is at most 192I mask trials, with +integer arithmetic and witness costs stated separately. + +The first explicit case has I=4,w=1,E=10. Its exact maximum is 257, attained +by (4,4,2), so integral rho>=29 suffices and is sharp. The simpler separate +bounds on k and B only certify rho>=30. At rho=29 every such triple saves +at least four actions; at rho=28 the attaining triple loses five. These are +parametric tariffs, not claims that a validator of cost 29 was executed. + +For actual child extents, E=2(n-c), where n is the parent width and c is +the child width. The theorem supplies a sufficient condition for every +admitted placement fitting I bits. Exact necessity concerns the larger +sum-conditioned triple domain; actual source geometry may exclude a witness. +No runtime dispatch, physical action exchange rate or full caller improvement +is supplied. Count output work cancels by the cited source contract. + +## Reproduce + +From the repository root, using CPython 3.12 and the standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/shared-atom-crossover +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/shared-atom-crossover/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -O -W error -B research/shared-atom-crossover/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/shared-atom-crossover --check-source-history +``` + +Any CPython 3.12 executable can replace the absolute interpreter path. Expected +markers are `PASS_SHARED_ATOM_CROSSOVER`, `PASS_REGISTERED_RESEARCH_PACKAGE` +and `PASS_RESEARCH_COMMIT_BYTES`. The final command needs committed bytes and +full Git history. The direct checker also works in a Git-free package export. +It writes nothing and prints a freshly generated receipt bound to all seven +package source/metadata files. No success receipt is handwritten. + +The new carry algorithm is compared with direct tariff maximization over all +149,792 ordered triples at I=1..5 and w in {1,2,3,7}. All 704 maxima, including +zero totals, agree. `oracle.py` applies the cited vector costs directly, +without importing the new carry algorithm. These checks establish agreement +on the stated finite domain, not independent review of the inherited tariffs. +The sharp strict boundary, E=0/E=1, an undercut maximum, an unattainable +combination of separate bounds, larger-width attaining witnesses and twelve +invalid arguments are checked. Explicit exceptions retain every check under +optimized Python. The written proof supplies the universal quantifiers. + +## Scope, sources and credit + +Canonical base is 7c49fe32c55de02c2c873655c804b16e4c3fef0a, priority revision 8, +selected PR6030 at kappa .003125804. The selected source-binding orientation +passed; it is metadata orientation, not a scientific selected replay. +The formal-interface-lemma card explicitly changes to this written cost +criterion rather than a proof-assistant theorem or discharge of a selected +assumption. [TASK.json](TASK.json) records that change. + +Credit Tekalign / tekuuu for PR4077's shared encoded atom powers, actual +child-extents adapter, exact vector tariffs and open affordability question. +David Arias / PR2753, Jose Manuel / jmbarrancoml, ToikY / PR4025, +ywz65 / PR2590, Chris R / Clear1nsight / PR4062 and their retained caller, +record and source contributors retain credit. Binary digit dynamic programming +and scalar tariff algebra are classical; no global literature-priority claim +is made. The new result is this exact sum-conditioned maximum and its sharp +application to the stated interface. + +[SOURCES.json](SOURCES.json) binds the unchanged main-tree predecessor proof +and README as historical provenance. They are not executable dependencies. +[Advance CLAIM](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19371189). +Live open/account PRs, handoffs, active Discussions, main-tree object/formula +searches and merged searches were checked. The broader cache covered 521 open +PRs and 6,530 Discussion records, while local notes were sparse. Unpublished +work, arbitrary historical diffs and global literature priority remain outside +that coverage. Search absence is not a novelty certificate. + +The theorem is conditional on the cited successful-input source tariffs. +Physical allocator/control costs, an encoded selector, actual validator +prices, full Context/payload composition, stock, precision and supplier/outer +admission are unrun obligations. No predecessor audit, selected cold replay, +Lean or Docker run is part of this contribution. All five selected assumptions +remain. Independent human and formal proof-kernel review are unclaimed. + +## Open next questions + +- Can actual source geometry reduce the sum-conditioned maximum further? + Start with one pinned native child family, its legal placements and external + gap constraints. The present attaining triple need not be a legal child. +- Can an encoded caller use the crossover without spending its gain on + selection? Start with a source-bound lower bound for rho and a fixed + parameter region. A host calculation of the threshold is not a paid + runtime decision or a complete physical caller. + +## Code bounds + +The mathematical proof permits all positive I,w; the reference API caps I at +4096 and w below 2^64. The exhaustive oracle caps I at five and four fixed w +values. Carry layers have at most 24 records and at most 192 transitions per +bit; each record holds three bounded-width witness integers. Source reads are +capped at 128 KiB per file. Functions are below 60 lines. There is no recursion, +subprocess, network, dynamic code generation or mutable shared state. The +checker uses normal and optimized warning-strict execution as its available +Python diagnostics; no separate type checker is claimed as run. + +Power-of-Ten rule 3 deviation: Python and its standard library allocate managed +integers, tuples, dictionaries and JSON. The fixed API limits, two bounded state +layers, a 94-entry oracle maximum table and streamed triple enumeration bound +live collections. This is not a fixed-pool, allocator-internals or real-time +claim. Larger domains must revise those caps before use. Standard-library +iterator and JSON dispatch have fixed targets; the code defines no callbacks. diff --git a/research/shared-atom-crossover/SOURCES.json b/research/shared-atom-crossover/SOURCES.json new file mode 100644 index 0000000000..cf13a1b086 --- /dev/null +++ b/research/shared-atom-crossover/SOURCES.json @@ -0,0 +1,30 @@ +{ + "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" + }, + { + "path": "research/encoded-child-spectators/PROOF.md", + "usage": "provenance", + "git_blob": "0e4bbcf04f1a2502bae7f47d5376a72de74fb36a", + "sha256": "cf439a2ffe2bc8521377225400306df7c829af194dc6d8614a4383c7741616a2" + }, + { + "path": "research/encoded-child-spectators/README.md", + "usage": "provenance", + "git_blob": "c4373db5f3f22b91f51a13df62a0a5329580cc83", + "sha256": "05ab321b1ec220375115ca28fc1113edafd530d4e147e09e8534b7172661df77" + } + ] +} diff --git a/research/shared-atom-crossover/TASK.json b/research/shared-atom-crossover/TASK.json new file mode 100644 index 0000000000..11cbcca580 --- /dev/null +++ b/research/shared-atom-crossover/TASK.json @@ -0,0 +1,106 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 8, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "original_card": { + "id": "formal-interface-lemma", + "question": "Can one uncovered interface implication be formalized with exact caller and certificate bindings?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/gate-operand-parity-lean/README.md", + "research/staged544-certified-endpoint/README.md", + "research/unconditional-batched-crt/README.md" + ], + "methods": [ + "Formalize a missing boundary lemma identified by the selected review.", + "Audit a formal theorem-to-certificate binding independently." + ], + "acceptance_gate": "State the exact formalized proposition and remaining assumptions; avoid duplicate arithmetic formalizations already present.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.", + "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse." + }, + "first_experiment": "Write one missing statement with quantified hypotheses, actual caller and existing coverage. A compact-switch lemma is a candidate only after its mathematical contract is reviewed. Establish a bounded proof plan before a separately budgeted proof-assistant build; do not rerun large Lean jobs as orientation.", + "bottleneck_link": "A missing interface proof can reduce the conditional gap even if it does not change kappa.", + "allowed_variations": [ + "Narrow to one formal lemma or one theorem-to-certificate binding." + ], + "scope_change_triggers": [ + "Formalizing already-covered arithmetic and claiming the full multiplication theorem." + ], + "overlap_terms": [ + "hyperplane end", + "formal interface", + "Lean binding", + "3807", + "3857", + "4100", + "gate-operand-parity-lean", + "staged544-certified-endpoint", + "unconditional-batched-crt" + ], + "existing_checks": [ + { + "scope": "PR #3807: scoped gate-operand parity formalization.", + "evidence": "research/gate-operand-parity-lean/README.md", + "remaining": "Exact theorem-to-caller binding and genuinely uncovered interface lemmas.", + "status": "author-checked", + "source_commit": "4c3530f42a6abcc48e7a6bcffd6c901911dc8269", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #3857: certified real-power moment/endpoint arithmetic.", + "evidence": "research/staged544-certified-endpoint/README.md", + "remaining": "Uniform algorithmic implications, not another endpoint digit.", + "status": "author-checked", + "source_commit": "ef4315b8caa605e47a2515004845eb2d2ed71a86", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4100: compact-switch formalization proposed as future validation.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Audit the statement and assumptions before a formal proof campaign.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Exact sum-conditioned complete source-action crossover for three shared encoded atom powers, with a 24-state carry maximum and attaining witnesses.", + "scope_change_reason": "PR4077 poses an unresolved source-coupled affordability question. This is a written interface cost theorem using its tariffs as premises, rather than proof-assistant binding or re-verification.", + "bottleneck_link": "Interface side result: avoids an overly conservative shared-power affordability test. It does not change a paid recursive profile or discharge a selected assumption.", + "budget_minutes": 60, + "stop_rule": "Stop at the first exact threshold improvement and package it; no source replay or broader optimization campaign.", + "outcome": "completed", + "evidence": "Written all-size proof; 149792 literal ordered triples, 704 exact maximum comparisons, strict boundary and twelve invalid-argument checks.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can actual child geometry reduce this maximum?", + "why_it_matters": "The current sufficient test covers more triples than a particular native child may reach.", + "first_step": "Pin one child family and enumerate its legal placement and gap constraints.", + "blocked_by": "No source-bound geometry domain is included here." + }, + { + "question": "Can an encoded caller select the shared path profitably?", + "why_it_matters": "A host threshold calculation does not supply a paid runtime optimization.", + "first_step": "Prove a source-bound lower bound for rho on one fixed region and charge the selector.", + "blocked_by": "Physical selector, control and complete caller costs remain unknown." + } + ], + "environment": { + "python": "3.12.15", + "platform": "Darwin 27.0.0", + "dependencies": "Python standard library" + } +} diff --git a/research/shared-atom-crossover/VERIFY.json b/research/shared-atom-crossover/VERIFY.json new file mode 100644 index 0000000000..63c580893e --- /dev/null +++ b/research/shared-atom-crossover/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 carry maxima versus exhaustive cited-tariff applications; attaining witnesses, strict threshold, zero/one totals and invalid arguments." + }, + { + "argv": [ + "{python}", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact carry maxima versus exhaustive cited-tariff applications; attaining witnesses, strict threshold, zero/one totals and invalid arguments." + } + ] +} diff --git a/research/shared-atom-crossover/oracle.py b/research/shared-atom-crossover/oracle.py new file mode 100644 index 0000000000..9a4dc56121 --- /dev/null +++ b/research/shared-atom-crossover/oracle.py @@ -0,0 +1,45 @@ +"""Literal application of the cited PR4077 tariffs, without carry optimization.""" + +from itertools import product + + +def inherited_overhead(exponents, width, radix_width): + """Additional non-radix actions in the shared method, from PR4077 §3–4.""" + overhead = 0 + for exponent in exponents: + if exponent == 0: + continue + length = exponent.bit_length() + zeros = width - length + population = exponent.bit_count() + construction = (2 * width + 3, width + 1 + 2 * zeros, + 2 * width + 4 + 2 * zeros) + decrements = (7 * exponent - 2 * population + 1, + 2 * exponent - population + 2 * length + 1, + 6 * exponent - 2 * population + 2 * length + 2) + consumed_close = (7, 2, 8) + unconsumed_close = (2 * length + 5, length + 1, 2 * length + 6) + index_copy = (3 * width + 3, 0, 2 * width + 4) + rundown = sum(construction) + sum(decrements) + sum(consumed_close) + probe = sum(construction) + sum(unconsumed_close) + overhead += (radix_width - 1) * rundown + probe + radix_width * sum(index_copy) + return overhead + + +def exhaustive_maxima(width, radix_width): + """Enumerate each ordered triple once in the fixed corroboration domain.""" + if type(width) is not int or not 1 <= width <= 5: + raise ValueError("oracle width outside 1..5") + if radix_width not in (1, 2, 3, 7): + raise ValueError("oracle radix width outside the fixed fixture") + limit = 1 << width + maxima = [-1] * (3 * (limit - 1) + 1) + visited = 0 + for exponents in product(range(limit), repeat=3): + total = sum(exponents) + value = inherited_overhead(exponents, width, radix_width) + maxima[total] = max(maxima[total], value) + visited += 1 + if visited != limit**3 or min(maxima) < 0: + raise ValueError("incomplete triple inventory") + return maxima, visited diff --git a/research/shared-atom-crossover/verify.py b/research/shared-atom-crossover/verify.py new file mode 100644 index 0000000000..699e550466 --- /dev/null +++ b/research/shared-atom-crossover/verify.py @@ -0,0 +1,139 @@ +"""Exact sum-conditioned shared-power cost certificate. Apache-2.0.""" + +import hashlib +import json +from pathlib import Path + +from oracle import exhaustive_maxima, inherited_overhead + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def validate(width, radix_width, total): + require(type(width) is int and 1 <= width <= 4096, "width outside 1..4096") + require(type(radix_width) is int and 1 <= radix_width < 2**64, + "radix width outside 1..2^64-1") + require(type(total) is int and 0 <= total <= 3 * ((1 << width) - 1), + "total outside the three-word domain") + + +def advance(states, bit_index, target_bit, width, radix_width): + coefficient = 14 * radix_width * width + 36 * radix_width - 9 + following = {} + transitions = 0 + for (outgoing, active), (score, exponents) in sorted(states.items()): + for bits in range(8): + incoming = target_bit + 2 * outgoing - bits.bit_count() + if not 0 <= incoming <= 2: + continue + used = active | bits + added = used.bit_count() - 5 * (radix_width - 1) * bits.bit_count() + added += coefficient * (used.bit_count() - active.bit_count()) + witness = tuple(exponents[j] + (((bits >> j) & 1) << bit_index) + for j in range(3)) + key = incoming, used + candidate = score + added, witness + if key not in following or candidate > following[key]: + following[key] = candidate + transitions += 1 + require(len(following) <= 24 and transitions <= 192, "state capacity") + return following + + +def maximum_overhead(width, radix_width, total): + """Return the exact overhead maximum and one attaining ordered triple.""" + validate(width, radix_width, total) + states = {(total >> width, 0): (0, (0, 0, 0))} + for bit_index in range(width - 1, -1, -1): + states = advance(states, bit_index, (total >> bit_index) & 1, + width, radix_width) + terminals = [value for (carry, _), value in states.items() if carry == 0] + require(bool(terminals), "a valid sum must have a terminal state") + score, witness = max(terminals) + overhead = 15 * (radix_width - 1) * total + score + require(sum(witness) == total, "witness sum") + require(all(0 <= e < 1 << width for e in witness), "witness width") + require(inherited_overhead(witness, width, radix_width) == overhead, + "attaining witness tariff") + return overhead, witness + + +def strict_threshold(width, radix_width, total): + """None means strict saving is impossible, including the all-zero tie.""" + overhead, witness = maximum_overhead(width, radix_width, total) + threshold = None if total < 2 else overhead // (total - 1) + 1 + return threshold, overhead, witness + + +def finite_comparison(): + triples = comparisons = 0 + stream = hashlib.sha256() + for width in range(1, 6): + for radix_width in (1, 2, 3, 7): + maxima, visited = exhaustive_maxima(width, radix_width) + triples += visited + for total, expected in enumerate(maxima): + actual, witness = maximum_overhead(width, radix_width, total) + require(actual == expected, "carry maximum differs from enumeration") + row = [width, radix_width, total, actual, witness] + stream.update((json.dumps(row, separators=(",", ":")) + "\n").encode()) + comparisons += 1 + require(triples == 149792 and comparisons == 704, "finite domain inventory") + return {"enumerated_triples": triples, "maximum_comparisons": comparisons, + "maximum_stream_sha256": stream.hexdigest()} + + +def boundary_checks(): + threshold, overhead, witness = strict_threshold(4, 1, 10) + require((threshold, overhead, witness) == (29, 257, (4, 4, 2)), "sharp case") + require(9 * 29 - overhead == 4 and 9 * 28 - overhead == -5, + "strict integer boundary") + require((3 * (14 * 4 + 27) + 3 * 4) // 9 + 1 == 30, + "independent-statistic sufficient threshold") + require(strict_threshold(4, 3, 0)[:2] == (None, 0), "all-zero tie") + require(strict_threshold(4, 3, 1)[0] is None, "one-atom loss") + for width, radix_width, total in ((64, 3, 2**63 + 100), (4096, 1, 2)): + h, attaining = maximum_overhead(width, radix_width, total) + require(h == inherited_overhead(attaining, width, radix_width), "large witness") + require(inherited_overhead((4, 4, 2), 4, 1) > 256, "undercut maximum control") + require(inherited_overhead((4, 4, 2), 4, 1) != 3 * 83 + 3 * 4, + "independent maxima cannot all be attained here") + return {"width": 4, "radix_width": 1, "total": 10, "maximum_overhead": overhead, + "attaining_exponents": witness, "exact_minimum_radix_invoice": threshold, + "separate_statistic_sufficient_invoice": 30, "minimum_gain_at_29": 4, + "attained_gain_at_28": -5} + + +def invalid_checks(): + cases = ((0, 1, 0), (4097, 1, 0), (True, 1, 0), (1.0, 1, 0), + (2, 0, 0), (2, True, 0), (2, 2**64, 0), (2, 1.0, 0), + (2, 1, -1), (2, 1, 10), (2, 1, True), (2, 1, 1.0)) + for arguments in cases: + try: + maximum_overhead(*arguments) + except ValueError: + continue + raise ValueError("invalid argument accepted") + return len(cases) + + +def receipt(): + package = Path(__file__).resolve().parent + names = ("README.md", "PROOF.md", "TASK.json", "SOURCES.json", "VERIFY.json", + "verify.py", "oracle.py") + sources = {} + for name in names: + with (package / name).open("rb") as handle: + payload = handle.read(131073) + require(len(payload) <= 131072, "source read capacity") + sources[name] = hashlib.sha256(payload).hexdigest() + return {"status": "PASS_SHARED_ATOM_CROSSOVER", "claim_type": "scoped proof", + "finite": finite_comparison(), "sharp_case": boundary_checks(), + "invalid_arguments_rejected": invalid_checks(), "source_sha256": sources} + + +if __name__ == "__main__": + print(json.dumps(receipt(), sort_keys=True, indent=2))