diff --git a/research/moving-stage-restoration-tariff/PROOF.md b/research/moving-stage-restoration-tariff/PROOF.md new file mode 100644 index 0000000000..a571bb602a --- /dev/null +++ b/research/moving-stage-restoration-tariff/PROOF.md @@ -0,0 +1,113 @@ +# Exact restoration tariff for positive moving stages + +This scoped proof is produced by Nick Petalas. Apache-2.0. + +## Contract + +Take finitely many coordinate blocks indexed by `0,1,...,m-1`, each of +the same positive width `w`. Block 0 is the anchor. Let `D_j` be the +normalized Gaussian on block j. The `D_j` commute, and `D_j^2` is a +block-local monomial. Let `P_s` exchange blocks 0 and s, with `P_0=I`. +The only charged stages are the positive operators + + E_s = P_s D_0, s=0,...,m-1. + +This is Cinna Davis's #5113 moving-coordinate interface, with the terminal +anchor stage used by Chris R / Clear1nsight's #5133. These premises are +cited, not independently audited here. Their native and coded-owner +semantics remain their premises. + +Write an endpoint in the exact normal form + + P_pi product_j D_j^(a_j), a_j >= 0. + +The requested boundary requires `pi=identity`. It requests odd Gaussian +exponent on precisely a set S of nonanchor blocks and anchor parity b +in `{0,1}`. All other blocks must have even exponent. The whole-block +permutation must restore inside the charged word. The even powers are +explicit residual block-local monomials. They are not removed for free. +This is a Gaussian-support quotient with internal block-permutation +restoration, not exact identity restoration of every address and phase. + +## Theorem + +For `k=|S|`, the least number of positive stages is + + L(S,b) = 2k + ((k+b) mod 2). + +It is independent of the number of unrequested spectator blocks. +For all m blocks requested, the value is `2m-2+(m mod 2)`. + +## Lower bound + +In any prefix normal form, left multiplication by `E_s` adds one to +`a_(pi^-1(0))`, then replaces `pi` by `(0 s) pi`. This follows by moving +`D_0` through `P_pi`. Consequently `sum_j a_j` is exactly the word length. +Its parity at the requested endpoint is `k+b` modulo two. + +Every requested nonanchor label j must occur among the stage indices. +If it never occurs, every block permutation fixes j, so `pi^-1(0)` +can never be j. Its Gaussian exponent stays zero, contradicting the +requested odd exponent. + +Moreover j cannot occur exactly once when the final permutation is the +identity. Before that occurrence the coordinate initially at j is still +at j. That occurrence moves it to block 0. No later transposition touches +position j, so that coordinate cannot return to j. Thus every member of +S needs at least two nonanchor stages. The length is at least `2k` and +has parity `k+b`. These two conditions give the displayed bound. The +argument allows arbitrarily many additional unrequested blocks and visits. + +## Attaining word and its exact residual + +For every j in S, use the consecutive pair `E_j E_j`. Since +`D_0 P_j = P_j D_j`, this pair is exactly + + E_j^2 = D_j D_0. + +Each pair restores its entire block permutation. Use all k pairs, then +append `delta=((k+b) mod 2)` copies of `E_0`. The exact endpoint is + + D_0^(k+delta) product_(j in S) D_j + = M_0 D_0^b product_(j in S) D_j, + M_0 = (D_0^2)^((k+delta-b)/2). + +The exponent of `M_0` is a nonnegative integer. Thus the word meets +every requested parity and restores all block permutations, with exactly +`2k+delta` charged stages. All unrequested nonanchor coordinates are +untouched. `M_0` is part of the explicit endpoint, not a waived fee. +This proves equality for every block width w and every finite number of +spectators. For w=8 it applies to #5113's eight-axis Gaussian blocks. + +## Consequence for an internally restored three-block word + +Request all three blocks, with `k=2,b=1`. The exact minimum is five +stages. The three-stage word `E_0 E_2 E_1` in #5133 obtains the same +Gaussian support after an external block permutation is removed. Its +permutation is `P_2 P_1`, not identity, so it is outside this theorem's +return boundary. This is a changed requirement, not a disagreement with +that source. The five-stage constructor has residual `D_0^2`. + +The theorem prices stage occurrences only. It does not establish a +minimal physical tape tariff or compare stages against the price of an +external permutation. It gives no main-owner independence, helper-target +credit, legal consumer, new signed invoice, supplier admission, new kappa +or complete multiplication theorem. Arbitrary nonmonomial free maps, +independently available `D_j`, and a boundary accepting a residual block +permutation change the model. + +## Finite corroboration + +The verifier implements the constructor and exact nonnegative exponent +normal form. An independent breadth-first search instead stores the +output-frame representation `D_mask P_pi`. It enumerates the full finite +quotient for one through six blocks, permits every stage at every state, +and obtains the distances to every permutation-restored support. It +imports no predecessor implementation. + +A separate literal address-array interpreter uses the Gaussian +`[[a,b],[b,a]]` over F_65537 with `a=(1+i)/2`, `b=(1-i)/2`, `i=256`. +Here `i^2=-1`, `D^2=X` and `D^4=I`. It checks every operator column for +all support requests on the declared one-axis and two-axis block fixtures, +including the explicit `M_0`. This is finite-field corroboration; the +all-width theorem is the algebraic argument above. diff --git a/research/moving-stage-restoration-tariff/README.md b/research/moving-stage-restoration-tariff/README.md new file mode 100644 index 0000000000..4574915a16 --- /dev/null +++ b/research/moving-stage-restoration-tariff/README.md @@ -0,0 +1,109 @@ +# Sharp positive moving-stage restoration count + +Scoped mathematical proof with exact finite corroboration. For the moving +Gaussian stages `E_s=P_(0,s) D_0`, including `E_0=D_0`, request Gaussian +parity on k nonanchor blocks and anchor parity b. If the entire block +permutation must restore inside the charged word, the exact minimum is + +```text +L(k,b) = 2k + ((k+b) mod 2). +``` + +Unused spectator blocks cannot shorten it. In particular, requesting all +m blocks costs `2m-2+(m mod 2)` stages. The internally restored three-block +boundary needs five stages. This gives an explicit cost for one restoration +method; it does not establish an improved recursive invoice or kappa. + +[PROOF.md](PROOF.md) gives the lower bound and an attaining word. Each +requested nonanchor stage is used twice. At most one anchor stage corrects +parity. The exact residual is an explicitly stated block-local monomial +`(D_0^2)^((k+delta-b)/2)`, with `delta=(k+b) mod 2`. That monomial remains +part of the output contract and is not a free cleanup operation. + +## Relation to predecessors + +Cinna Davis / 1337isnot1337's [PR #5113](https://github.com/CrocSwap/integer-mult-bounds/pull/5113) +supplies the common-code moving-coordinate interface and its native/caller +limitations. Chris R / Clear1nsight's [PR #5133](https://github.com/CrocSwap/integer-mult-bounds/pull/5133) +uses a terminal anchor stage and rejects a fixed optimistic three-stage +invoice. Its three-stage word accepts an external whole-block permutation. +This result imposes internal permutation restoration instead and proves +the exact count for every target support and every number of blocks. +It does not replay, audit or claim either predecessor's result. + +Credit Dillon #4933, Dugongue #4929, Cao Yifan, Cayden Burkart, JoyboyBrian, +zxv, Jacob Alan Sussman and the retained native/compiler/precision lineage +through #5113. Elementary permutation and tensor-product identities are +standard. The new scoped tariff, proof and verifier are produced by Nick Petalas. +Independent human and formal proof-kernel review are unclaimed. Apache-2.0. + +## Reproduce + +From the repository root, use CPython 3.12 and the standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -I -B research/moving-stage-restoration-tariff/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -I -O -B research/moving-stage-restoration-tariff/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/moving-stage-restoration-tariff +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/moving-stage-restoration-tariff --check-source-history +``` + +Both direct modes print `PASS_MOVING_STAGE_RESTORATION_TARIFF` with +50,362 quotient states, 126 permutation-restored endpoints, 916 literal +operator columns and 12 controls. The independent BFS uses an output-frame +state rather than the constructor's input-frame exponent representation. +Every stage is allowed at every quotient state. Literal finite-field +operators check every basis column on the declared fixtures, including +two-axis blocks and the residual local monomial. No predecessor executable +is imported. These are checks of the new theorem, not source replays. + +Default verification writes nothing and needs no Git or network. Optional +`--receipt NEW_PATH` creates a receipt bound to the six package file hashes +and refuses an occupied path. The registered commands time out at 120 +seconds each. All controls remain active under optimized Python. + +## Scope and limits + +The theorem covers every positive block width and finite spectator count. +The executable constructor and quotient oracle are bounded to six blocks; +the literal operator fixtures use one-axis blocks through four blocks and +two-axis blocks through three blocks. Finite enumeration corroborates the +written proof and does not replace it. + +Only positive stages of this stated alphabet are charged. The endpoint +permits explicit block-local monomials and requires internal restoration +of the permutation of whole blocks. A caller accepting an external +permutation has a different contract. Full local-monomial cleanup, physical +movement, owner independence, helper targets, native/caller/compiler and +precision costs remain unpriced. No selected cold replay, Lean proof, +complete supplier, new kappa or complete multiplication theorem is claimed. +The selected frontier is unchanged. + +Base is canonical main `19fdb086ea96af9a9f87936a2b888e10af4ed810`, priority +revision 8. The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19226084) +and [TASK.json](TASK.json) state the changed boundary and overlap coverage. +[SOURCES.json](SOURCES.json) pins both predecessor texts and the historical +card/selected record. Live open PRs, recent account PRs, handoffs, main +README terms and merged searches were checked; unpublished work and notes +outside those searches are not excluded. + +## Open next questions + +- Price internal restoration against an external block permutation in one + actual complete caller. Start with that caller's exact endpoints and + paid/target inventories, including the residual local monomial. The + physical permutation tariff and consumer are missing here. +- Determine the minimum under a stricter contract that eliminates every + residual local monomial. Start with exponents modulo four and fix whether + inverse stages are legal. That different alphabet/endpoint contract is + not answered by the present parity theorem. + +## Implementation bounds + +All loops have finite bounds from the declared block domains. The BFS has +at most `6! * 2^6` states and six outgoing stages per state. Literal vectors +have at most 64 entries. No function recurses and every function fits within +60 lines. Explicit exceptions enforce contracts in both Python modes. +Python integers and collections allocate dynamically; this is a bounded +managed-runtime verifier, not a fixed-allocation physical implementation. +Warning-strict normal and optimized replay provide interpreter diagnostics. diff --git a/research/moving-stage-restoration-tariff/SOURCES.json b/research/moving-stage-restoration-tariff/SOURCES.json new file mode 100644 index 0000000000..002577ed4a --- /dev/null +++ b/research/moving-stage-restoration-tariff/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8", + "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/common-code-moving-stages/PROOF.md", + "usage": "input", + "git_blob": "60fecc67b7847e2f40d31710e49de3a4c23eeab2", + "sha256": "46b427b0834aa513bba6244e3b44a089597fdb0546d0fda8c5e41130e6881eeb" + }, + { + "path": "research/moving-anchor-no-q-ceiling/README.md", + "usage": "input", + "git_blob": "130f7b7c638be69b88f0ad83181027b082b59ac4", + "sha256": "40673b8a0561c2fcd690ab7d10ac44269361b5fd3d788b84e44dbbf44374e1aa" + } + ] +} diff --git a/research/moving-stage-restoration-tariff/TASK.json b/research/moving-stage-restoration-tariff/TASK.json new file mode 100644 index 0000000000..4cd930bee4 --- /dev/null +++ b/research/moving-stage-restoration-tariff/TASK.json @@ -0,0 +1,91 @@ +{ + "schema_version": 1, + "task_id": "complex-rank-shape-decoder", + "priority_revision": 8, + "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "original_card": { + "id": "complex-rank-shape-decoder", + "question": "Can a legal decoder or coframe change improve the full signed moment, including changed helper targets?", + "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", + "docs/research/recursive-invoice-preflight.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 source-bound arbitrary-input identity and legal producer/consumer boundary with the complete paid and productive target invoice, including restoration, ownership, native alignment and extra charges. Price under the actual current model; historical ceiling.py assumptions must be established before use. A favorable optimistic relaxation keeps a route open but is not a completed supplier. A scoped local result remains useful; expansion requires the family-level budget gate.", + "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": "Price one complete changed itinerary with both paid and productive histograms. Check #5693/#5698 for overlap and their exact hypotheses before another coframe search. Use the signed invoice preflight where its boundary contract agrees; an inconclusive concave comparison is not a power crossing. Stop if an optimistic complete budget fails at the chosen target or native delivery remains unspecified.", + "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": [ + "coframe", + "signed moment", + "5693", + "5698" + ], + "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": "Exact minimum positive moving-stage count with internally restored whole-block permutation and specified Gaussian parity support, modulo explicit block-local monomials.", + "scope_change_reason": "Original restoration-boundary question building on the moving-coordinate interface of PR5113. No full signed-moment improvement is asserted; stage count isolates a previously unpriced return obligation.", + "bottleneck_link": "The current new-decoder track requires complete restoration. This theorem prices stage-only internal block-permutation return instead of assuming an external whole-field permutation is free. Local monomial and caller costs remain unknown.", + "budget_minutes": 60, + "stop_rule": "Stop research at the first verified original scoped result; package this exact tariff without seeking a larger result.", + "outcome": "completed", + "evidence": "PROOF.md supplies an all-width proof. verify.py checks 50362 quotient states, 126 restored endpoints, 916 literal finite-field operator columns and 12 controls in normal and optimized modes.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "For one actual moving-coordinate caller, is an external block permutation cheaper than the extra internally restoring stages?", + "why_it_matters": "The exact stage count alone cannot choose a physical restoration method or establish a recursive gain.", + "first_step": "Pin a complete caller and charge its external block permutation, the additional stages, residual local monomial and all productive helper targets on the same boundary.", + "blocked_by": "No complete caller or physical permutation tariff is supplied here." + }, + { + "question": "What is the minimum if every residual block-local monomial must also be eliminated by the charged alphabet?", + "why_it_matters": "The present optimum permits a specified anchor monomial at the output, which a stricter consumer may reject.", + "first_step": "Retain Gaussian exponents modulo four and specify whether inverse stages are available before deriving a new bound.", + "blocked_by": "A stricter endpoint contract and native stage alphabet must be fixed first." + } + ], + "claim_type": "scoped mathematical proof with exact finite corroboration", + "coordination": { + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19226084", + "overlap": "Live open PR list, latest 30 handoff comments, active Discussions, recent account PRs, merged PR searches and main README searches consulted. Cached local note coverage is sparse; no exhaustive novelty claim." + }, + "environment": { + "python": "3.12.15 (main, Oct 14 2026, 00:55:37) [Clang 23.1.3 ]", + "platform": "macOS-27.0.1-arm64-arm-64bit", + "dependencies": "standard library only" + } +} diff --git a/research/moving-stage-restoration-tariff/VERIFY.json b/research/moving-stage-restoration-tariff/VERIFY.json new file mode 100644 index 0000000000..d1464a0c8c --- /dev/null +++ b/research/moving-stage-restoration-tariff/VERIFY.json @@ -0,0 +1,37 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/common-code-moving-stages/PROOF.md", + "research/moving-anchor-no-q-ceiling/README.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Full finite quotient BFS, explicit attaining words, all operator columns and malformed-input/endpoint controls." + }, + { + "argv": [ + "{python}", + "-W", + "error", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Same complete checks with Python assertions disabled; all contracts use explicit exceptions." + } + ] +} diff --git a/research/moving-stage-restoration-tariff/verify.py b/research/moving-stage-restoration-tariff/verify.py new file mode 100644 index 0000000000..0128ceefd6 --- /dev/null +++ b/research/moving-stage-restoration-tariff/verify.py @@ -0,0 +1,209 @@ +#!/usr/bin/env python3 +"""Exact positive moving-stage tariff. Produced by Nick Petalas; Apache-2.0.""" + +import argparse +from collections import deque +import hashlib +import json +from math import factorial +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parent.parent +PRIME = 65537 +MAX_BLOCKS = 6 + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def validate(blocks, support, anchor): + require(type(blocks) is int and 1 <= blocks <= MAX_BLOCKS, "block bound") + require(type(anchor) is int and anchor in (0, 1), "anchor parity") + require(type(support) is frozenset, "support representation") + require(all(type(s) is int and 1 <= s < blocks for s in support), "support") + + +def construct(blocks, support, anchor): + validate(blocks, support, anchor) + correction = (len(support) + anchor) % 2 + word = tuple(s for s in sorted(support) for _ in range(2)) + return word + (0,) * correction + + +def normal_form(word, blocks): + """P_perm times product D_j^exponent, with exact integer exponents.""" + require(1 <= blocks <= MAX_BLOCKS and len(word) <= 2 * blocks, "word bound") + require(all(type(s) is int and 0 <= s < blocks for s in word), "stage") + permutation = list(range(blocks)) + exponents = [0] * blocks + for s in word: + exponents[permutation.index(0)] += 1 + permutation = [s if x == 0 else 0 if x == s else x for x in permutation] + require(sum(exponents) == len(word), "one Gaussian per stage") + return tuple(permutation), tuple(exponents) + + +def quotient_oracle(blocks): + """BFS in the independent output-frame form D_mask P_perm.""" + identity = tuple(range(blocks)) + start = (identity, 0) + distances = {start: 0} + queue = deque([start]) + capacity = factorial(blocks) * (1 << blocks) + for _ in range(capacity): + if not queue: + break + permutation, mask = queue.popleft() + for s in range(blocks): + moved = mask ^ 1 + if s and (moved & 1) != ((moved >> s) & 1): + moved ^= 1 | (1 << s) + p = tuple(s if x == 0 else 0 if x == s else x for x in permutation) + state = (p, moved) + if state not in distances: + require(len(distances) < capacity, "finite quotient capacity") + distances[state] = distances[(permutation, mask)] + 1 + queue.append(state) + require(not queue and len(distances) == capacity, "complete quotient") + for mask in range(1 << blocks): + support = frozenset(s for s in range(1, blocks) if mask >> s & 1) + word = construct(blocks, support, mask & 1) + require(distances[(identity, mask)] == len(word), "shortest tariff") + p, exponents = normal_form(word, blocks) + require(p == identity, "constructor restores permutation") + actual_mask = sum((e % 2) << s for s, e in enumerate(exponents)) + require(actual_mask == mask, "constructor Gaussian support") + return capacity, 1 << blocks + + +def gaussian(values, axis): + imaginary = 256 + a = (1 + imaginary) * pow(2, -1, PRIME) % PRIME + b = (1 - imaginary) * pow(2, -1, PRIME) % PRIME + out = list(values) + bit = 1 << axis + for x in range(len(values)): + if not x & bit: + y = x | bit + out[x] = (a * values[x] + b * values[y]) % PRIME + out[y] = (b * values[x] + a * values[y]) % PRIME + return out + + +def swap_blocks(values, stage, width): + out = [0] * len(values) + block_mask = (1 << width) - 1 + for x, value in enumerate(values): + difference = ((x >> (stage * width)) ^ x) & block_mask + y = x ^ difference ^ (difference << (stage * width)) + out[y] = value + return out + + +def execute(word, initial, width): + values = list(initial) + for s in word: + for axis in range(width): + values = gaussian(values, axis) + values = swap_blocks(values, s, width) + return values + + +def target(initial, support_mask, blocks, width, anchor_flip): + values = list(initial) + for s in range(blocks): + if support_mask >> s & 1: + for axis in range(s * width, (s + 1) * width): + values = gaussian(values, axis) + if anchor_flip: + values = [values[x ^ ((1 << width) - 1)] for x in range(len(values))] + return values + + +def literal_checks(): + require(pow(256, 2, PRIME) == PRIME - 1, "imaginary unit") + columns = 0 + for blocks, width in ((1, 1), (2, 1), (3, 1), (4, 1), (2, 2), (3, 2)): + dimension = 1 << (blocks * width) + for mask in range(1 << blocks): + support = frozenset(s for s in range(1, blocks) if mask >> s & 1) + anchor = mask & 1 + word = construct(blocks, support, anchor) + delta = (len(support) + anchor) % 2 + even_exponent = len(support) + delta - anchor + require(even_exponent >= 0 and even_exponent % 2 == 0, "local monomial") + for column in range(dimension): + initial = [int(x == column) for x in range(dimension)] + actual = execute(word, initial, width) + expected = target(initial, mask, blocks, width, (even_exponent // 2) % 2) + require(actual == expected, "literal full operator column") + columns += 1 + return columns + + +def rejection_controls(): + invalid = ((0, frozenset(), 0), (7, frozenset(), 0), + (2, frozenset({2}), 0), (2, frozenset({0}), 0), + (2, frozenset({1}), 2), (True, frozenset(), 0), + (2, {1}, 0), (2, frozenset({True}), 0)) + for args in invalid: + rejected = False + try: + construct(*args) + except ValueError: + rejected = True + require(rejected, "invalid constructor accepted") + p, exponents = normal_form((1, 2, 0), 3) + require(all(e % 2 == 1 for e in exponents), "externally normalized positive control") + require(p != (0, 1, 2), "external permutation is still unpaid") + p, exponents = normal_form((1, 1), 2) + require(p == (0, 1) and exponents == (1, 1), "anchor correction omission") + p, _ = normal_form((1,), 2) + require(p != (0, 1), "return omission") + initial = [1] + [0] * 15 + word = construct(4, frozenset({1, 2, 3}), 1) + require(execute(word, initial, 1) != target(initial, 15, 4, 1, 0), + "residual local monomial must not be omitted") + return len(invalid) + 4 + + +def authenticate(): + manifest = json.loads((HERE / "SOURCES.json").read_text()) + inputs = [row for row in manifest["files"] if row["usage"] == "input"] + require(len(inputs) == 2, "two predecessor text inputs") + for row in inputs: + data = (ROOT / row["path"]).read_bytes() + require(hashlib.sha256(data).hexdigest() == row["sha256"], "source hash") + + +def run(): + authenticate() + states = targets = 0 + for blocks in range(1, MAX_BLOCKS + 1): + count, endpoints = quotient_oracle(blocks) + states += count + targets += endpoints + return {"status": "PASS_MOVING_STAGE_RESTORATION_TARIFF", + "quotient_states": states, "restored_endpoints": targets, + "literal_columns": literal_checks(), "controls": rejection_controls()} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--receipt", type=Path, help="create a new hash-bound receipt") + args = parser.parse_args() + result = run() + if args.receipt is not None: + names = ("README.md", "PROOF.md", "TASK.json", "SOURCES.json", "VERIFY.json", "verify.py") + result["package_sha256"] = { + name: hashlib.sha256((HERE / name).read_bytes()).hexdigest() for name in names} + with args.receipt.open("x") as stream: + stream.write(json.dumps(result, indent=2, sort_keys=True) + "\n") + print(json.dumps(result, sort_keys=True)) + + +if __name__ == "__main__": + main()