diff --git a/research/r16-independent-cycle-tariff/PROOF.md b/research/r16-independent-cycle-tariff/PROOF.md new file mode 100644 index 0000000000..d56d70c675 --- /dev/null +++ b/research/r16-independent-cycle-tariff/PROOF.md @@ -0,0 +1,179 @@ +# Exact independent-radical tariff on a cheap directed cycle + +This scoped written proof was produced by Nick Petalas. Apache-2.0. + +## Contract and result + +Let `R = F2[e,h,z]/(e,h,z)^2`, with maximal ideal `m=(e,h,z)`. +The three independent dirty rows and disjoint preserved source belong to +`R^w`, for any positive width w. Require + + A_i = a_i + lambda_i p, lambda=(e,h,e+h+z). + +The only gates are fixed input-independent operations + + P_i(b): A_i += b p, price mu_i > 0; + E_ij(a): A_i += a A_j, price c_ij > 0, i != j. + +All coefficients are available, with coefficient-independent, stationary +prices. Zero gates may be deleted. Every original dirt column must return. +There are no extra rows, observations, clearing or free basis changes. +The three cycle edges `0 -> 1 -> 2 -> 0` cost c. Set `mu=min_i mu_i`. +Assume `mu >= 6c` and every reverse edge costs at least `6c`. + +**Theorem.** The exact complete abstract price is `2mu+6c`. +In particular, insertion prices 100, cycle prices 1 and reverse prices 100 +have optimum 206. This is not a physical tariff or a multiplication theorem. + +The demand, contract, incoming-row return lemma and two-unit-insertion +argument are credited to lee-phys #6210. We restate those short arguments +for a self-contained proof. The new step is the six-ADD lower bound with +cycle edges, its matching word and the resulting price cone. No predecessor +numerical result or verifier is rechecked. + +## Preliminary facts + +Every element of R is uniquely `a+u`, with `a in F2` and `u in m`. +Its units have a=1; every nonzero nonunit lies in m. For `u in m`, +`R u={0,u}`, and units act on u as the identity. In particular `m^2=0`. +The three demands form a basis of m over F2. + +Track the three dirt columns and source column in a 3-by-4 matrix. Its dirt +part is invertible at every cut and returns to identity. A nonzero incoming +ADD cannot occur exactly once at a row. Indeed, before that sole ADD its +dirt row is the original standard row. Restoration would force the added +multiple of the sender's current dirt row to be zero. Multiplication by the +inverse current dirt matrix would then force its nonzero coefficient to +be zero. Thus a used receiving row has at least two incoming ADDs. + +A one-insertion word is impossible. Its final source column is an invertible +matrix column times the inserted coefficient beta. If beta is in m, the +three demand coordinates lie in the one-dimensional space `{0,beta}`. +If beta is a unit, reduction modulo m gives a nonzero column, whereas every +demand is in m. Both contradict the target. + +With exactly two insertions, both inserted coefficients must be units. +If just one were a unit, reduction modulo m would again give a single +nonzero invertible-matrix column. If neither were a unit, the final demand +coordinates would lie in the F2-span of their two radical coefficients, +contradicting the three independent demands. These are #6210's arguments +specialized to this ring. + +## Two insertions require at least six cycle ADDs + +Suppose a two-insertion, cycle-only word has at most five nonzero ADDs. +By the incoming-row lemma, some row receives no ADD. + +If the insertions enter different rows, every insertion row needs an ADD: +otherwise its final source coefficient is its sole unit insertion. The +third row also needs an ADD, since its demand is nonzero. Each then needs +at least two, a contradiction. Hence both insertions enter the same root i. + +The other two rows j,k must receive ADDs. If i also receives any, the total +is at least six. Thus i receives none. Relabel cyclically so the only +remaining directions are `i -> j -> k`. Write beta,gamma for the inserted +units. Root i's source coefficient takes values `0,beta,lambda_i`, since +`beta+gamma=lambda_i`. Row j's dirt is always `e_j+a(t)e_i`. +Both j and k receive at least two ADDs. + +### If j receives exactly two ADDs + +Their coefficients are equal to some nonzero a, by restoration of j. +Its final source is `a(s+t)`, where s,t are the root source coefficients +at its two ADDs. Their sum is one of `0,beta,gamma,lambda_i`. + +The first value gives zero. The last gives either zero or lambda_i. +Neither is lambda_j. The remaining values are units, so obtaining the +radical lambda_j requires `a in m`, and then `a=lambda_j`. Every intermediate +source coefficient at j is consequently in `{0,lambda_j}`. Every source +contribution delivered to k is in the same ideal. This cannot give the +independent lambda_k. Thus j cannot receive exactly two ADDs. + +### The only remaining case is three ADDs at j and two at k + +Let the three nonzero coefficients at j be a,b,d, with `a+b+d=0`. +No proper nonempty subset of these three coefficients sums to zero: +a singleton would be a zero gate, and a zero pair would force the third +to be zero. + +The two coefficients at k are equal to a nonzero v, since the coefficient +of the original dirt j is always one in row j. Between the two k ADDs, +let Delta a be the change in j's dirt coefficient of i and Delta s its +change in source coefficient. Restoration and the target require + + v Delta a=0, v Delta s=lambda_k. + +If v is a unit, `Delta a=0`. The preceding subset observation means either +none or all three j ADDs occur between the k ADDs. In the former case +Delta s=0. In the latter Delta s=lambda_j. Thus k gets zero or lambda_j, +not lambda_k. + +If v is a nonunit, it is a nonzero radical. The two equations force +`Delta a mod m=0` and `Delta s mod m=1`. But the three j ADDs contain either +zero or two unit coefficients, because their total is zero modulo m. +Root i's residue is one exactly between its two insertions. Final j has +residue zero, so either both unit j ADDs fall in that insertion interval, +or neither does. Over any time interval, j's source-residue change is +therefore either zero or equal to its dirt-residue change. In the interval +between the k ADDs that change is zero, contradicting `Delta s mod m=1`. + +These cases exhaust every cycle-only word with two insertions and at most +five ADDs, regardless of their interleaving or coefficient values. + +## An attaining word + +Choose any root i and put `j=i+1 mod 3`, `k=i+2 mod 3`. In chronological +order define + + Q_i = E_ji(1+lambda_j), E_kj(lambda_k), E_ji(1). + +Its matrix is `I+N`, where + + N = lambda_j E_ji + lambda_k E_kj + lambda_k E_ki. + +All entries of N lie in m, so `N^2=0`, `Q_i^2=I`, and +`Q_i e_i=e_i+lambda_j e_j+lambda_k e_k`. The word + + P_i(1+lambda_i), Q_i, P_i(1), Q_i + +restores every original dirt column. Its source column is + + (1+lambda_i) Q_i^2 e_i + Q_i e_i + = lambda_i e_i + lambda_j e_j + lambda_k e_k. + +Every coefficient is nonzero. The word has two source insertions and six +cycle ADDs, for price `2mu_i+6c`. For root zero it is + + P_0(1+e), E_10(1+h), E_21(e+h+z), E_10(1), + P_0(1), E_10(1+h), E_21(e+h+z), E_10(1). + +The unused third cycle edge is still available to competing words. + +## Complete tariff + +A correct word needs at least two insertions. With at least three, +its cost is at least `3mu >= 2mu+6c`. With exactly two and a reverse ADD, +its cost is at least `2mu+6c`. With exactly two and only cycle ADDs, +the proved six-ADD lower bound gives the same price. Choosing a root +with minimum insertion price attains it. This proves the theorem. + +## Exact finite corroboration + +The verifier independently enumerates all order-zero gate skeletons with +at most five cycle ADDs and exactly two unit insertions, including arbitrary +zero-residue ADD coefficients. No symmetry or heuristic pruning is used. +A 3-by-4 binary matrix is the order-zero state. Each gate's radical part +adds a linear generator to its first-order response; existing generators +propagate by the binary row operation. Since `m^2=0`, this expansion is exact. +Each radical coordinate has an independent copy of the same linear system. +The target's three radical coordinate columns span the entire pure-source +subspace. A closing skeleton can realize the target if and only if all +three pure-source basis matrices lie in its response span. + +A layer is merged only when its constant matrix, response subspace and +both gate counts coincide. These determine every future transition and +solvability. The search allows zero-valued nonunit ADD coefficients, an +overapproximation harmless for exclusion. All two-unit insertion locations +and all six cycle ADD residue types are included. Seven finite transition +rounds cover all such words. None is solvable. This corroborates the written +five-ADD exclusion; it is not a proof-kernel certificate. diff --git a/research/r16-independent-cycle-tariff/README.md b/research/r16-independent-cycle-tariff/README.md new file mode 100644 index 0000000000..d9932bd238 --- /dev/null +++ b/research/r16-independent-cycle-tariff/README.md @@ -0,0 +1,125 @@ +# Exact independent-radical dirty fanout on a directed cycle + +This contribution was produced by Nick Petalas. Apache-2.0. + +Claim type: scoped written proof with exact finite corroboration. For the +three independent demands `(e,h,e+h+z)` over +`R16=F2[e,h,z]/(e,h,z)^2`, the exact complete abstract tariff is + + OPT = 2 min_i(mu_i) + 6c, + min_i(mu_i) >= 6c, reverse-edge prices >= 6c. + +Here the cycle ADDs `0 -> 1 -> 2 -> 0` cost c>0, and insertion into row i +costs mu_i. All coefficients are available at stationary coefficient-independent +prices. Three arbitrary dirty rows and one preserved disjoint source are +required; every dirt column returns. There are no other rows, observations, +free basis changes or clearing operations. The theorem holds at every +positive data width under this algebraic contract. + +At insertion and reverse prices 100 and cycle price 1, the optimum is +**206**. The destination-row relaxation from lee-phys's +[#6210](https://github.com/CrocSwap/integer-mult-bounds/pull/6210) gives 204 +when every incoming ADD is priced one. This new directed-edge obligation +costs two additional ADDs. Three direct insertions cost 300. + +The new eight-gate word, in chronological order, is + + P_0(1+e), E_10(1+h), E_21(e+h+z), E_10(1), + P_0(1), E_10(1+h), E_21(e+h+z), E_10(1). + +Cyclic relabeling gives an attaining word at any minimum-price insertion +root. [PROOF.md](PROOF.md) proves that every two-insertion cycle word needs +at least six ADDs, with arbitrary interleaving and coefficients, and proves +the complete price-cone result. The proof does not infer an all-word optimum +from a bounded search alone. The first improvement was retained without +expanding to a broader price classification. + +## Reproduce + +From the repository root, CPython 3.12 and the standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/r16-independent-cycle-tariff/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/r16-independent-cycle-tariff/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/r16-independent-cycle-tariff +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/r16-independent-cycle-tariff --check-source-history +``` + +Other machines may substitute their CPython 3.12 path. No predecessor +executable is imported or replayed. Each invocation writes no files and +prints a generated JSON receipt bound to all six package-file hashes. +The expected marker is `PASS_R16_INDEPENDENT_CYCLE_TARIFF`. + +The checker tests 504 words, one for every independent radical demand triple +and root, forward and inverse on their entire dirt/source matrices. It also +checks 393,216 literal forward/inverse scalar evaluations for the stated +demand, ten price fixtures and sixteen rejection controls. Its separate +exact first-order enumeration excludes every two-unit-insertion cycle word +with at most five ADDs. Layer sizes are +`[1,9,57,283,1186,4201,11842,18061]`, with 95,562 transitions and 2,481 +closing transitions. These are enumeration counts, not distinct literal +word counts. The written proof supplies the all-word argument. + +## Credit, scope and overlap + +Credit lee-phys / #6210 for this demand, the arbitrary-dirty contract, +incoming-row return lemma, two-unit insertion argument and directed-price +open question. Retain lee-phys's #5259/#5163, Ali Romman's #5310/#5266, +Krzysztof Wojt's #5045, Ross Richardson's #3063/#3121, Nick Petalas's +#4916/#5208 and the retained fanout lineage. The first-order subspace +method is adapted from Nick Petalas's older #6693; its receiving-row +frontier is cited, not rechecked. The new bit packing and bounded cycle +search are standalone. The older #5933 and #6663 solve other directed +cycle demands, not this independent radical triple. No general priority +is claimed for square-zero expansion, elementary matrices or dirty echoes. + +This takes Open next question 2 of #6210. The historical `bit-helper-contract` +card is marked changed to this algebraic interface side result in +[TASK.json](TASK.json). It supplies a sharp local directed-price obstruction, +not an emitted BIT word or a selected assumption discharge. The selected +binding baseline passed at main `e54523517d0f03e58352e647c403a5af3e525a57`, +κ `0.00363005817`, with priority revision 8 predating that selection. + +Entry overlap covered 477 open PRs and 7,122 Discussion records with complete +reported remote pagination. Its sparse local note scan omitted 9,973 HEAD +note paths. Targeted all-main README searches and all-state/merged searches +for R16, radical fanout, independent demands and directed cycle supplemented +that scan. No equivalent result was found in that coverage. Historical +diffs, unpublished work and later changes remain coverage limits. +[Advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19538457). + +No arbitrary-price classification, larger ring theorem, extra-workspace +optimum, physical coefficient preparation, routing, precision/tape, stock, +supplier admission, new kappa or complete multiplication theorem is claimed. +Independent human and formal proof-kernel review are unclaimed. No selected +cold replay, native suite, Lean or Docker run was required for this local +result. Exact source provenance is in [SOURCES.json](SOURCES.json). + +## Open next questions + +- Determine the exact tariff outside this price cone. Start with the same + independent radical demand and one cheap reverse edge; count every directed + edge separately. The six-ADD lower bound alone does not price unequal edges. +- Find a physical caller with these independent radical demands and complete + source/ADD prices. First identify the actual coefficient algebra and its + routing, precision and restoration charges. None is supplied here. + +Structured first steps and blockers are in [TASK.json](TASK.json). + +## Verifier constraints + +There is no recursion, subprocess, network, dynamic code execution or external +scientific input in the verifier. Seven transition rounds and a 200,000-state +per-layer cap bound the search; exhaustion raises an error. Each search basis has +at most seven 12-bit vectors. Finite word fixtures have eight gates; the +literal domain is exactly three roots and 16^4 scalar inputs. Functions are +below 60 lines. Explicit exceptions preserve all checks under optimization; +both registered commands make warnings errors. SHA256 receipts are generated +only after the actual checks pass. + +Power of Ten rule 3 deviation: CPython allocates integers, tuples and sets +while checking. The fixed finite domains, per-layer capacity check and +serial execution bound live collections; there is no growing service or +unbounded input. Package-file reads are at most one MiB each. A fixed-allocation +embedded implementation would need a separate runtime. Normal and optimized +replay exercise these controls; no external static analyzer is claimed. diff --git a/research/r16-independent-cycle-tariff/SOURCES.json b/research/r16-independent-cycle-tariff/SOURCES.json new file mode 100644 index 0000000000..a7283a5a65 --- /dev/null +++ b/research/r16-independent-cycle-tariff/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "75d77b328ea02ded535e7f23aee5b1e55d0bb1a8", + "sha256": "154c3d30455d778fd3343b6b4851f0fa4665f0f7625b0adb3675e2bafbbf6bf1" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/r16-radical-pareto-frontier/README.md", + "usage": "provenance", + "git_blob": "5f8c256651e278355d9a57cce2c6f511b3e22ad1", + "sha256": "001e1e1ff5432678d4f487a14b579bda19718ed3df38a263bd6324bf5d69dff6" + }, + { + "path": "research/r16-radical-triple-fanout/README.md", + "usage": "provenance", + "git_blob": "a122a5de58e72d9b126fe6bf3085c3852813d204", + "sha256": "291eef5b1b08c1560660cdc9ac6891274477a2f0c9b505c22f66c986abbad3f9" + } + ] +} diff --git a/research/r16-independent-cycle-tariff/TASK.json b/research/r16-independent-cycle-tariff/TASK.json new file mode 100644 index 0000000000..91d1491575 --- /dev/null +++ b/research/r16-independent-cycle-tariff/TASK.json @@ -0,0 +1,89 @@ +{ + "schema_version": 1, + "task_id": "bit-helper-contract", + "priority_revision": 8, + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "original_card": { + "id": "bit-helper-contract", + "question": "Can a changed G20 helper path or independent-target split improve the complete BIT moment without losing its physical endpoint?", + "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/g20-helper-split/README.md", + "research/g20-conjugation-admission/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": "A full boundary contract and paid profile; unchanged scalar counts alone are insufficient. 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": "First read #5679/#5708 and their audits as pending component proposals. Choose one uncovered helper group/cut on an exact word; compare arbitrary-input native action, targets, owned storage, both orientations and full signed bill. Stop if the gain is only a scalar count or repaid by lost targets. Do not rerun the frozen #5609 common-frame domain without changing its hypothesis.", + "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": [ + "G20", + "helper split", + "5679", + "5708", + "independent target" + ], + "existing_checks": [ + { + "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": "Determine the exact directed-cycle price cone for #6210 independent radical demand (e,h,e+h+z) over R16.", + "scope_change_reason": "The historical card concerns an emitted G20 helper path. This is the explicit directed-price open question from #6210, a scoped algebraic interface side result with no supplier or kappa claim.", + "bottleneck_link": "Dirty restoration can make directed transport dearer than its receiving-row relaxation. The sharp six-ADD obligation prices one complete local contract; native realization and supplier costs remain unknown.", + "budget_minutes": 60, + "stop_rule": "Ship the first verified new word and sharp scoped price; do not expand to arbitrary directed prices.", + "outcome": "completed", + "evidence": "PROOF.md and verify.py; exact price 2 min(mu_i)+6c on the declared cone; no new kappa.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "What is the exact tariff outside this cone?", + "why_it_matters": "Unequal directed prices can change the optimal word.", + "first_step": "Use the same R16 demand and one cheap reverse edge, retaining every dirt column and per-edge count.", + "blocked_by": "No all-positive directed-edge price classification is supplied." + }, + { + "question": "Can a physical caller realize this contract?", + "why_it_matters": "An abstract directed price theorem does not improve a multiplication supplier.", + "first_step": "Identify the actual coefficient algebra and complete source, routing, precision and restoration prices.", + "blocked_by": "No physical caller or full supplier invoice is supplied." + } + ], + "verification_environment": { + "implementation": "CPython", + "python": "3.12.15", + "platform": "macOS-27.0.1-arm64-arm-64bit", + "interpreter": "/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12" + } +} diff --git a/research/r16-independent-cycle-tariff/VERIFY.json b/research/r16-independent-cycle-tariff/VERIFY.json new file mode 100644 index 0000000000..e58ef62f9a --- /dev/null +++ b/research/r16-independent-cycle-tariff/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Full dirt/source identities, exact five-ADD exclusion, literal inputs and rejection controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Same exact checks with optimization enabled." + } + ] +} diff --git a/research/r16-independent-cycle-tariff/verify.py b/research/r16-independent-cycle-tariff/verify.py new file mode 100644 index 0000000000..4e6c5b61b9 --- /dev/null +++ b/research/r16-independent-cycle-tariff/verify.py @@ -0,0 +1,238 @@ +#!/usr/bin/env python3 +"""Exact cycle-fanout certificate, without predecessor executable imports.""" +from hashlib import sha256 +from itertools import product +import json +from pathlib import Path + +IDENTITY = 1 | (2 << 4) | (4 << 8) +SOURCE_BITS = (8, 128, 2048) +CYCLE = ((1, 0), (2, 1), (0, 2)) +TARGET = (2, 4, 14) +MAX_LAYER = 200_000 + + +def require(condition, message): + if not condition: + raise RuntimeError(message) + + +def multiply(a, b): + require(0 <= a < 16 and 0 <= b < 16, 'ring element outside R16') + return (a & 1) * b ^ (b & 1) * (a & 14) + + +def independent(demand): + basis = () + for value in demand: + if value == 0 or value & 1: + return False + basis = extend(basis, value) + return len(basis) == 3 + + +def extend(basis, vector): + for pivot in basis: + vector = min(vector, vector ^ pivot) + if not vector: + return basis + high = 1 << (vector.bit_length() - 1) + result = [x ^ vector if x & high else x for x in basis] + return tuple(sorted(result + [vector], reverse=True)) + + +def contains(basis, vector): + for pivot in basis: + vector = min(vector, vector ^ pivot) + return vector == 0 + + +def row_add(matrix, receiver, sender): + return matrix ^ (((matrix >> (4 * sender)) & 15) << (4 * receiver)) + + +def symbolic_step(state, basis, gate): + kind, receiver, sender, residue = gate + if kind == 'E': + generator = ((state >> (4 * sender)) & 15) << (4 * receiver) + if residue: + state = row_add(state, receiver, sender) + changed = () + for vector in basis: + changed = extend(changed, row_add(vector, receiver, sender)) + basis = changed + else: + generator = SOURCE_BITS[receiver] + state ^= residue * generator + return state, extend(basis, generator) + + +def symbolic_solution(sequence): + state, basis = IDENTITY, () + for gate in sequence: + state, basis = symbolic_step(state, basis, gate) + return state == IDENTITY and all(contains(basis, x) for x in SOURCE_BITS) + + +def exclude_five(): + """Every residue skeleton with <=5 ADDs and exactly two unit insertions.""" + additions = tuple(('E', a, b, u) for a, b in CYCLE for u in (0, 1)) + insertions = tuple(('P', a, -1, 1) for a in range(3)) + layer = {(IDENTITY, (), 0, 0)} + sizes, finals, transitions = [1], 0, 0 + for _depth in range(7): + following = set() + for state, basis, inserted, added in layer: + moves = (additions if added < 5 else ()) + moves += insertions if inserted < 2 else () + for gate in moves: + ns, nb = symbolic_step(state, basis, gate) + ni = inserted + (gate[0] == 'P') + na = added + (gate[0] == 'E') + transitions += 1 + if ni == 2 and ns == IDENTITY: + finals += 1 + require(not all(contains(nb, x) for x in SOURCE_BITS), + 'two-insertion five-ADD counterexample') + key = (ns, nb, ni, na) + require(key in following or len(following) < MAX_LAYER, + 'exhaustion, no certificate') + following.add(key) + layer = following + sizes.append(len(layer)) + return {'layer_sizes': sizes, 'transitions': transitions, + 'closing_transitions': finals} + + +def word(demand, root): + require(independent(demand) and root in range(3), 'invalid demand or root') + i, j, k = root, (root + 1) % 3, (root + 2) % 3 + q = [('E', j, i, 1 ^ demand[j]), ('E', k, j, demand[k]), + ('E', j, i, 1)] + return [('P', i, -1, 1 ^ demand[i])] + q + [('P', i, -1, 1)] + q + + +def matrix(word_gates): + require(len(word_gates) <= 8, 'word exceeds eight gates') + rows = [[int(i == j) for j in range(4)] for i in range(3)] + for kind, a, b, coefficient in word_gates: + require(0 < coefficient < 16, 'zero or invalid coefficient') + require(a in range(3), 'invalid receiver') + if kind == 'P': + rows[a][3] ^= coefficient + else: + require(kind == 'E' and (a, b) in CYCLE, 'noncycle ADD') + rows[a] = [x ^ multiply(coefficient, y) + for x, y in zip(rows[a], rows[b], strict=True)] + return rows + + +def target(demand): + return [[int(i == j) for j in range(3)] + [demand[i]] for i in range(3)] + + +def scalar_run(gates, values): + rows, source = list(values[:3]), values[3] + for kind, a, b, coefficient in gates: + rows[a] ^= multiply(coefficient, source if kind == 'P' else rows[b]) + return tuple(rows) + (source,) + + +def check_words(): + demands = [d for d in product(range(0, 16, 2), repeat=3) if independent(d)] + checked = 0 + for demand in demands: + for root in range(3): + gates = word(demand, root) + require(matrix(gates) == target(demand), 'forward matrix') + require(matrix(gates[::-1]) == target(demand), 'inverse matrix') + require(sum(g[0] == 'P' for g in gates) == 2, 'insertion count') + require(sum(g[0] == 'E' for g in gates) == 6, 'ADD count') + sequence = [(t, a, b, c & 1) for t, a, b, c in gates] + require(symbolic_solution(sequence), 'positive symbolic control') + checked += 1 + require(len(demands) == 168 and checked == 504, 'demand enumeration') + return checked + + +def check_scalars(): + checked = 0 + for root in range(3): + gates = word(TARGET, root) + for values in product(range(16), repeat=4): + expected = tuple(values[i] ^ multiply(TARGET[i], values[3]) + for i in range(3)) + (values[3],) + actual = scalar_run(gates, values) + require(actual == expected, 'literal forward input') + require(scalar_run(gates[::-1], actual) == values, 'literal inverse') + checked += 2 + return checked + + +def check_controls(): + gates = word(TARGET, 0) + mutations = [gates[:i] + gates[i + 1:] for i in range(8)] + changed = list(gates) + changed[2] = ('E', 2, 1, 2) + mutations.append(changed) + changed = list(gates) + changed[0] = ('P', 0, -1, 2) + mutations.append(changed) + for altered in mutations: + require(matrix(altered) != target(TARGET), 'mutant escaped') + require(not independent((2, 4, 6)), 'dependent demand accepted') + require(not independent((3, 4, 14)), 'unit demand accepted') + require(not symbolic_solution([('P', 0, -1, 1)]), 'open residue accepted') + require(not symbolic_solution([]), 'empty basis accepted') + for gates_bad in ([('E', 0, 1, 1)], [('P', 0, -1, 0)]): + try: + matrix(gates_bad) + except RuntimeError: + continue + raise RuntimeError('invalid gate accepted') + return len(mutations) + 6 + + +def check_prices(): + checked = 0 + for c in (1, 2, 5): + for extra in (0, 1, 17): + prices = (6 * c + extra, 9 * c + extra, 11 * c + extra) + optimum = 2 * min(prices) + 6 * c + require(3 * min(prices) >= optimum, 'three-insertion price gate') + require(2 * min(prices) + 6 * c == optimum, 'reverse-edge price gate') + for root in range(3): + cost = sum(prices[a] if kind == 'P' else c + for kind, a, _b, _x in word(TARGET, root)) + require(cost == 2 * prices[root] + 6 * c, 'complete word bill') + checked += 1 + example = sum(100 if kind == 'P' else 1 + for kind, _a, _b, _x in word(TARGET, 0)) + require(example == 206 and min(300, 200 + 4) == 204, 'displayed prices') + return checked + 1 + + +def main(): + # R16 multiplication independently checked against the monomial definition. + for a, b in product(range(16), repeat=2): + expanded = ((a & 1) & (b & 1)) + for bit in (2, 4, 8): + expanded ^= (a & 1) * (b & bit) ^ (b & 1) * (a & bit) + require(multiply(a, b) == expanded, 'ring multiplication') + evidence = {'exclusion': exclude_five(), 'words': check_words(), + 'literal_forward_inverse': check_scalars(), + 'controls': check_controls(), 'price_fixtures': check_prices()} + package = Path(__file__).resolve().parent + hashes = {} + for name in ('README.md', 'PROOF.md', 'TASK.json', 'SOURCES.json', + 'VERIFY.json', 'verify.py'): + path = package / name + require(path.stat().st_size <= 1_048_576, 'package-file size bound') + data = path.read_bytes() + hashes[name] = sha256(data).hexdigest() + print(json.dumps({'result': 'PASS_R16_INDEPENDENT_CYCLE_TARIFF', + 'evidence': evidence, 'sha256': hashes}, sort_keys=True)) + + +if __name__ == '__main__': + main()