diff --git a/research/cut58-free-address-character-obstruction/PROOF.md b/research/cut58-free-address-character-obstruction/PROOF.md new file mode 100644 index 0000000000..ff020084ce --- /dev/null +++ b/research/cut58-free-address-character-obstruction/PROOF.md @@ -0,0 +1,140 @@ +# A scalar relation across the cut58 ADDRESS adapter + +This contribution was produced by Nick Petalas. Apache-2.0. +Claim type: scoped mathematical proof with exact finite corroboration. + +## Operators and scope + +Use the literal monomials supplied by unpaidmoon in PR #4149, following +Ross Richardson's cut58 source in #4082 and separable floor in #4086. +Those operator definitions are premises, not an audit target. We do not +replay either predecessor's group census, endpoint or 22f calculation. + +Write the active bits as three ordered pairs +`a=(x0,x1)`, `b=(x2,x3)`, `c=(x10,x11)`. +Bits 4 through 9 are spectators. For bit pairs, a bar complements both bits, +and `a.b=a0*b0+a1*b1` is an integer dot product. +The one-coordinate maps send a basis vector at `(a,b,c)` to the stated +address, multiplied by `i^q`: + +```text + output address q modulo 4 +k (bar(a),b,c) 3(a0+a1+b0+b1)+2 a.b+3 +w (b,a,c) 2a1+3(b0+b1)+2 a.b+3 +t (a,b,bar(c)) 3c0+c1 +p (c,b,a) 0 +``` + +The actual families are `K_f=i k^(tensor f)`, `W_f=w^(tensor f)`, +`T_f=i t^(tensor f)` and `P_f=p^(tensor f)` for every positive integer f. +Both displayed factors i are outside the tensor powers. Optional identity +spectators do not change any statement below. Products act right to left. + +## New exact relation + +For every positive integer f, + +```text +P_f W_f K_f P_f W_f = -T_f W_f K_f P_f K_f. (1) +``` + +Here is a direct symbolic proof, without closing the generated group. +The left one-coordinate word `p w k p w` sends + +```text +(a,b,c) -> (b,a,c) -> (c,a,b) -> (bar(c),a,b) + -> (a,bar(c),b) -> (b,bar(c),a). +``` + +The right one-coordinate word `t w k p k` sends + +```text +(a,b,c) -> (bar(a),b,c) -> (c,b,bar(a)) + -> (bar(c),b,bar(a)) -> (b,bar(c),bar(a)) + -> (b,bar(c),a). +``` + +Substitute the phases from the table at the input of each successive map. +On both sides their sum modulo four reduces to the same multilinear polynomial + +```text +q = 3+2a1+3(b0+b1)+3c0+c1+2(a0*b0+a1*b1). (2) +``` + +For example, the left sum is `q_w(a,b)+q_k(c,a)+q_w(bar(c),a)`. +The right sum is `q_k(a,b)+q_k(c,b)+q_w(bar(c),b)+q_t(bar(a))`. +Expanding each complemented bit as `1-x` proves (2) over Z/4Z. +Thus the one-coordinate operators are exactly equal, including their phase. +The actual left word has outer factor i from its single K. The right word +has outer factor `i^3=-i` from its two K factors and one T. Tensoring the +one-coordinate equality and retaining these outer factors proves (1). +The minus sign is independent of f, including even f. + +## Consequence for the tariff characters + +Let chi be a homomorphism from the actual generated operator group to +`{+1,-1}` that fixes scalar operators. This requirement also holds for a +scalar-linear represented-algebra sign twist. Put + +```text +chi(K)=(-1)^A, chi(W)=(-1)^B, chi(T)=(-1)^C, chi(P)=(-1)^D. +``` + +Apply chi to (1). Its left side has sign `chi(K)` because W and P each +occur twice. Its right side has sign `chi(T) chi(W) chi(P)` because K +occurs twice and chi fixes the scalar -I. Necessarily + +```text +A+B+C+D = 0 modulo 2. (3) +``` + +In particular, if the rank-zero ADDRESS adapter is required to have sign +`chi(P)=+1`, then `A+B+C=0`. The predecessor's three tests restrict to + +```text +chi_W: (A,B,C)=(0,1,0) impossible with chi(P)=+1 +chi_KW: (A,B,C)=(1,1,0) not excluded by this relation +chi_T: (A,B,C)=(0,0,1) impossible with chi(P)=+1. +``` + +Indeed, every scalar-fixing extension of either chi_W or chi_T, if an +extension exists at all, must give `chi(P)=-1`. This is the obstruction +needed for native tariff counting. A one-bank P response is free in polar +rank. A twist odd on P gives a nonzero full-bank gate defect at zero native +rank, so its odd-response count cannot retain the predecessor's positive +native-charge inequality. P's separate scalar or physical costs are not +claimed zero by this argument. + +Equation (3) is necessary, not a presentation or a sufficiency theorem. +It leaves four of the eight sign assignments with D=0 unexcluded. +No extension of chi_KW or any other surviving assignment is constructed. +We do not claim that the full generated group has four such characters. + +## Research consequence and limits + +The separable 22f theorem of #4086 remains a cited result in its own +alphabet. A per-response tariff for the one-P sandwiches, proved in #4149, +does not extend its character count to arbitrary words in the enlarged +alphabet. Relation (1) proves a specific failure of that attempted route: +two of its three sign tests cannot keep the new free adapter even. + +This supplies neither a cheaper six-bank word nor a counterexample to any +published lower bound. Other characters, invariants, changed tariffs or +explicit synthesis could still settle the enlarged problem. There is no +new supplier, native admission, kappa or selected-frontier change. Native, +compiler, ownership, precision/tape, BIT and analytic obligations remain. +Independent human and formal proof-kernel review are unclaimed. + +## Executable evidence + +The new verifier derives both word phases as Boolean multilinear +polynomials over Z/4Z, compares their coefficients with (2), and independently +applies the ten literal primitive occurrences to every one of the 4,096 +twelve-bit basis addresses. It enumerates all 16 sign assignments and checks +(3). These are new relation checks, not a replay of the old response census. + +Controls distinguish unsigned equality from (1), omitted P, discarded +global phases, moving those phases inside even tensor powers, and the +change that permits P to have a negative sign. Normal and optimized Python +use explicit exceptions. The all-f result follows from the proof above; +the finite basis check establishes the exact one-coordinate identity. diff --git a/research/cut58-free-address-character-obstruction/README.md b/research/cut58-free-address-character-obstruction/README.md new file mode 100644 index 0000000000..f7c214f0d7 --- /dev/null +++ b/research/cut58-free-address-character-obstruction/README.md @@ -0,0 +1,128 @@ +# A cut58 relation obstructs free-ADDRESS tariff characters + +This contribution was produced by Nick Petalas. Apache-2.0. + +Claim type: scoped mathematical proof with exact finite corroboration. +For the actual cut58 families, at every positive tensor multiplicity f, + +```text +P W K P W = -T W K P K. +``` + +Consequently every scalar-fixing sign character satisfies +`chi(K) chi(W) chi(T) chi(P)=1`. Two of the three characters used in Ross +Richardson's separable 22f proof, `chi_W` and `chi_T`, therefore cannot +extend while keeping the rank-zero ADDRESS swap P even. Any extension of +either, if it exists, must be odd on P. Its odd-response count would then +have nonzero defect on a zero-native-rank adapter. + +This answers a concrete part of Open next question 1 in unpaidmoon's +[PR #4149](https://github.com/CrocSwap/integer-mult-bounds/pull/4149). +That package leaves extension of the three characters to the enlarged +alphabet open. The new relation blocks the two stated extensions under +the free-adapter condition that native tariff counting requires. The +remaining `chi_KW` is not excluded by this relation; its extension is not +established here. No complete character classification is claimed. + +[PROOF.md](PROOF.md) derives the relation by six-bit polynomial algebra, +with the scalar i factors kept outside the tensor powers. The minus sign +is independent of f. The relation holds with all six original spectator +bits and arbitrary further identity spectators. + +This result changes the available proof strategy for the enlarged menu. +It supplies no cheaper six-bank cleanup and does not refute #4086's +separable 22f theorem. Physical ADDRESS costs, a complete native invoice, +BIT compatibility, ownership, compiler, precision/tape and analytic +obligations remain open. There is no new kappa or selected-frontier change. +Independent human and formal proof-kernel review are unclaimed. + +## Reproduce + +From the repository root with CPython 3.12 and the standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -I -B research/cut58-free-address-character-obstruction/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -I -O -B research/cut58-free-address-character-obstruction/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/cut58-free-address-character-obstruction +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/cut58-free-address-character-obstruction --check-source-history +``` + +Any CPython 3.12 installation can replace the local interpreter path. +Expected marker: `PASS_CUT58_FREE_ADDRESS_CHARACTER_OBSTRUCTION`. +The new verifier independently composes both words in two ways: + +- Boolean multilinear polynomial arithmetic over Z/4Z derives their exact + coordinate maps and phase coefficients. +- Literal action visits all 4,096 twelve-bit basis columns, including every + spectator setting, and compares the complete address and Gaussian phase. + +All 16 generator sign assignments are enumerated. Exactly eight satisfy +this relation, including four with P even. These are assignments not +excluded by this relation, not a count of actual group characters. +Boundary controls reject unsigned equality, omission of P, and moving the +outer phases inside even tensor powers. They also show why allowing P to +be odd escapes the specific obstruction. Checks remain active under -O. + +Each run emits a generated JSON receipt bound to SHA256 hashes of all six +package files and the sole source input. It writes no files. No receipt is +handwritten. No predecessor executable, old group census, 22f endpoint, +selected cold replay, Lean or Docker check is run. + +## Provenance and task scope + +The base is canonical main `721c03822c421b7f7fcbb2598993b947c4d88419`, +priority revision 8. Source bindings are in [SOURCES.json](SOURCES.json). +The literal operator JSON from #4149 is the sole live input. Its README +and Ross Richardson's #4086 proof are historical provenance. No frozen +predecessor file or selected record is changed. + +The picker suggested verifier engineering. The mathematical contribution +assignment instead takes a distinct explicit handoff under +`joint-query-controller`, with changed scope recorded in TASK.json. The +selected orientation passed `PASS_RESEARCH_BASELINE_BINDINGS_ONLY` after +materializing its sparse inputs. That is metadata orientation only. +The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19241949) +precedes the relation search. The first exact relation ended that search. + +Overlap checks read live open PRs, this account's 200 latest PRs, recent +handoffs and active Discussions, current-main READMEs, merged PRs and the +card's cached overlap report. Sparse local-note coverage was incomplete; +direct Git searches supplemented it. Arbitrary diffs and unpublished work +are outside that coverage. No equivalent relation was found in those checks. + +Credit unpaidmoon / #4149 for the ADDRESS menu and explicit character +extension question; Ross Richardson / #4082 and #4086 for the actual +operators, physical family conventions and separable tariff proof; and +icekylinx / #531, Rohan Arun / kernel92, Chris R / Clear1nsight and ToikY +for the retained native, phase and interface lineage. The predecessor +results are cited, not independently rechecked as the deliverable. + +## Open next questions + +1. Does `chi_KW` extend with P even and fix every represented-algebra + relation at the needed tensor multiplicities? Start with a structural + formula for that character or one new relation that excludes it. + This matters because it is the retained test unexcluded here. Equation + (3) alone is only a necessary condition, and tensor faithfulness remains + a separate issue. +2. Can another invariant or an explicit word settle the enlarged six-bank + cleanup price? Start with the exact cut58 matrix and a fully charged + alphabet containing P. The present relation supplies no shorter word, + complete enlarged-alphabet floor or physical implementation. + +## Implementation bounds + +Build the Lever supplies the rerunnable relation verifier. Prove It Works +supplies its separate polynomial and complete basis-action paths. The +Power of Ten scope is this one Python file. It has no recursion, external +process, dynamic source import or persistent mutable state. Loops have +fixed bounds: five letters per compared word, 12 address bits, 4,096 basis +columns, six symbolic variables with at most 64 monomials, and 16 sign +assignments. Functions are below 60 physical lines. + +Python's managed allocation is an explicit rule 3 deviation. The fixed +polynomial, word and basis domains bound live collections; basis columns +are streamed. Source reads are limited to the fixed hash-bound input and +six package files. Warning-strict normal and optimized registered checks +provide diagnostics. No separate static type analyzer or formal proof +kernel is configured or claimed. diff --git a/research/cut58-free-address-character-obstruction/SOURCES.json b/research/cut58-free-address-character-obstruction/SOURCES.json new file mode 100644 index 0000000000..5485b4229a --- /dev/null +++ b/research/cut58-free-address-character-obstruction/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419", + "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/cut58-address-swap-menu/operators.json", + "usage": "input", + "git_blob": "08a931062c410793af8f707ddcb8c65230990ce9", + "sha256": "9704ae3c0c1fbb93526970b05a63f486f376961edd019ba526249477d2aa0ab3" + }, + { + "path": "research/cut58-address-swap-menu/README.md", + "usage": "provenance", + "git_blob": "cc0769c62eb195b8add476767ee69df5da040e53", + "sha256": "c62dc20ed8cf1c0a2fbf9212adeeb9225811d69c61d8d6a53b374fe164f53853" + }, + { + "path": "research/cut58-separable-query-floor/PROOF.md", + "usage": "provenance", + "git_blob": "740dc7f9a41b302100c61b293a9b0ca67b0dac27", + "sha256": "88bbe1ca0fb0892f048ca3b3a3b245c5a7de1a77c5a43b34fad3437c45526da4" + } + ] +} diff --git a/research/cut58-free-address-character-obstruction/TASK.json b/research/cut58-free-address-character-obstruction/TASK.json new file mode 100644 index 0000000000..d89928d388 --- /dev/null +++ b/research/cut58-free-address-character-obstruction/TASK.json @@ -0,0 +1,90 @@ +{ + "schema_version": 1, + "task_id": "joint-query-controller", + "priority_revision": 8, + "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419", + "original_card": { + "id": "joint-query-controller", + "question": "Can a changed query demand or caller remove real work while satisfying native chronology and restoration?", + "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" + ], + "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": "Choose an exact caller and a new demand/interface hypothesis. Read the scoped #5617/#5631/#5649/#5747 and #5720/#5745 objections before rebuilding an excluded schedule. Compare the complete matched source/consumer protocols including all retained helper outputs. For an active-mode injection, first check #5745: its canonical delivery claim repays the eight removed centre jobs. Audit that exact claim or change its channel/feedback hypothesis; do not repeat the same free-injection search. Stop if the full favorable budget fails or the required restored output is unobservable.", + "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": [ + "query demand", + "active mode", + "5720", + "5745", + "5747", + "caller" + ], + "existing_checks": [ + { + "scope": "PR #4166: author-checked installed producer/service/return/bridge connection; native-component comparison loses.", + "evidence": "research/qq16-caller-install/README.md", + "remaining": "Complete matched physical protocol bill, or changed source-compatible demand/circuit; no affordable supplier yet.", + "status": "author-checked", + "source_commit": "0b082d22a0e9a442d264ab0633e35ef26c790630", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "status": "reviewed", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Prove one new all-positive-tensor-size relation in the cut58 K/W/T/P alphabet and its obstruction to scalar-fixing tariff characters that keep rank-zero ADDRESS even.", + "scope_change_reason": "The picker suggested verifier engineering, while the explicit assignment requires an original mathematical step. PR4149 Open next question 1 asks for character extensions past its ADDRESS menu. This package supplies a new relation and an obstruction to two free-ADDRESS extensions, rather than auditing an existing result or constructing a complete supplier.", + "bottleneck_link": "Side result for a changed recursive interface: the separable 22f proof cannot transfer its chi_W and chi_T counts to arbitrary ADDRESS-interleaved words with P even. A complete enlarged-alphabet bill remains open.", + "budget_minutes": 60, + "stop_rule": "Stop at the first new verified phase-correct relation. Do not extend the group search or claim a complete character classification, cheaper caller or new kappa.", + "outcome": "negative-result", + "evidence": "PROOF.md, the standalone symbolic/literal verifier and its generated stdout receipt.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Does chi_KW extend with P even and respect all represented-algebra relations at the required tensor multiplicities?", + "why_it_matters": "It is the predecessor tariff test unexcluded by the new relation.", + "first_step": "Give a structural character formula or a new exact relation with odd K+W parity and even P parity.", + "blocked_by": "The new relation is necessary only; neither character existence nor represented-algebra faithfulness is proved." + }, + { + "question": "Can another invariant or an explicit word determine the enlarged six-bank cleanup price?", + "why_it_matters": "Losing two proof tests does not establish a native gain or a new lower bound.", + "first_step": "Use the exact cut58 matrix and an explicitly priced alphabet containing the ADDRESS swap.", + "blocked_by": "No complete new word, extended tariff theorem or physical/recursive invoice is supplied." + } + ] +} diff --git a/research/cut58-free-address-character-obstruction/VERIFY.json b/research/cut58-free-address-character-obstruction/VERIFY.json new file mode 100644 index 0000000000..6c95d7f90d --- /dev/null +++ b/research/cut58-free-address-character-obstruction/VERIFY.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/cut58-address-swap-menu/operators.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "New word relation via Boolean polynomials and all 4096 literal basis columns; all 16 generator sign assignments; outer-phase, omitted-ADDRESS and free-sign boundary controls." + }, + { + "argv": [ + "{python}", + "-W", + "error", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "New word relation via Boolean polynomials and all 4096 literal basis columns; all 16 generator sign assignments; outer-phase, omitted-ADDRESS and free-sign boundary controls." + } + ] +} diff --git a/research/cut58-free-address-character-obstruction/verify.py b/research/cut58-free-address-character-obstruction/verify.py new file mode 100644 index 0000000000..78444eabea --- /dev/null +++ b/research/cut58-free-address-character-obstruction/verify.py @@ -0,0 +1,207 @@ +"""Exact cut58 relation. No predecessor executable or census is run. + +Produced by Nick Petalas. Apache-2.0. +""" + +from hashlib import sha256 +from itertools import product +import json +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +INPUT = "research/cut58-address-swap-menu/operators.json" +INPUT_SHA256 = "9704ae3c0c1fbb93526970b05a63f486f376961edd019ba526249477d2aa0ab3" +ACTIVE = (0, 1, 2, 3, 10, 11) +LEFT = "PWKPW" +RIGHT = "TWKPK" +FILES = ("README.md", "PROOF.md", "TASK.json", "SOURCES.json", "VERIFY.json", "verify.py") + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def load_source(): + data = (ROOT / INPUT).read_bytes() + require(len(data) <= 65536, "source capacity") + require(sha256(data).hexdigest() == INPUT_SHA256, "source SHA256") + source = json.loads(data) + for name in "KWTP": + entry = source[name] + require(len(entry["rows"]) == len(entry["alpha"]) == len(entry["quad"]) == 12, + "twelve-bit operator") + require(all(row.bit_count() == 1 for row in entry["rows"]), "bit permutation") + require(sorted(entry["rows"]) == [1 << i for i in range(12)], "invertible permutation") + return source + + +def scalar_phase(entry, point): + linear = sum(entry["alpha"][i] for i in range(12) if point >> i & 1) + quadratic = sum((entry["quad"][i] & point).bit_count() & 1 + for i in range(12) if point >> i & 1) + return (entry["constant"] + linear + 2 * quadratic) % 4 + + +def literal(word, point, source): + require(0 <= point < 4096 and 1 <= len(word) <= 10, "literal domain") + phase = global_phase = 0 + for name in reversed(word): + entry = source[name] + phase += scalar_phase(entry, point) + global_phase += entry["global_phase"] + point = sum(((row & point).bit_count() & 1) << i + for i, row in enumerate(entry["rows"])) ^ entry["offset"] + return point, phase % 4, global_phase % 4 + + +def add(left, right, scale=1): + result = left.copy() + for mask, coefficient in right.items(): + result[mask] = (result.get(mask, 0) + scale * coefficient) % 4 + return {mask: coefficient for mask, coefficient in result.items() if coefficient} + + +def multiply(left, right): + require(len(left) <= 64 and len(right) <= 64, "polynomial capacity") + result = {} + for a, x in left.items(): + for b, y in right.items(): + result[a | b] = (result.get(a | b, 0) + x * y) % 4 + return {mask: coefficient for mask, coefficient in result.items() if coefficient} + + +def polynomial_phase(entry, coordinates): + result = {0: entry["constant"]} + for index, bit in enumerate(ACTIVE): + result = add(result, coordinates[index], entry["alpha"][bit]) + for other, other_bit in enumerate(ACTIVE): + if entry["quad"][bit] >> other_bit & 1: + result = add(result, multiply(coordinates[index], coordinates[other]), 2) + return result + + +def compile_word(word, source): + coordinates = [{1 << i: 1} for i in range(6)] + phase = {} + global_phase = 0 + for name in reversed(word): + entry = source[name] + phase = add(phase, polynomial_phase(entry, coordinates)) + updated = [] + for bit in ACTIVE: + input_bit = entry["rows"][bit].bit_length() - 1 + require(input_bit in ACTIVE, "active permutation closure") + value = coordinates[ACTIVE.index(input_bit)] + updated.append(add({0: 1}, value, -1) if entry["offset"] >> bit & 1 + else value.copy()) + coordinates = updated + global_phase = (global_phase + entry["global_phase"]) % 4 + return coordinates, phase, global_phase + + +def closed_form(point): + bits = tuple((point >> bit) & 1 for bit in ACTIVE) + a0, a1, b0, b1, c0, c1 = bits + output_bits = (b0, b1, 1 - c0, 1 - c1, a0, a1) + output = point & sum(1 << bit for bit in range(4, 10)) + output += sum(value << bit for value, bit in zip(output_bits, ACTIVE)) + phase = (3 + 2 * a1 + 3 * (b0 + b1) + 3 * c0 + c1 + + 2 * (a0 * b0 + a1 * b1)) % 4 + return output, phase + + +def check_relation(source): + expected_coordinates = [{4: 1}, {8: 1}, {0: 1, 16: 3}, + {0: 1, 32: 3}, {1: 1}, {2: 1}] + expected_phase = {0: 3, 2: 2, 4: 3, 8: 3, 16: 3, 32: 1, 5: 2, 10: 2} + left = compile_word(LEFT, source) + right = compile_word(RIGHT, source) + require(left[:2] == right[:2], "symbolic projective relation") + require(left[0] == expected_coordinates and left[1] == expected_phase, "closed form") + require((left[2], right[2]) == (1, 3), "global phases outside tensor powers") + for point in range(4096): + a = literal(LEFT, point, source) + b = literal(RIGHT, point, source) + require(a[:2] == b[:2] == closed_form(point), "literal basis and closed form") + require((a[2] - b[2]) % 4 == 2, "literal negative sign") + return left[2], right[2] + + +def word_sign(word, assignment): + exponent = sum(assignment["KWTP".index(name)] for name in word) + return exponent % 2 + + +def check_characters(): + permitted = [] + free_permitted = [] + for assignment in product(range(2), repeat=4): + compatible = word_sign(LEFT, assignment) == word_sign(RIGHT, assignment) + require(compatible == (sum(assignment) % 2 == 0), "parity relation") + if compatible: + permitted.append(assignment) + if assignment[3] == 0: + free_permitted.append(assignment) + for assignment in ((0, 1, 0, 0), (0, 0, 1, 0)): + require(word_sign(LEFT, assignment) != word_sign(RIGHT, assignment), + "free-ADDRESS extension must reject chi_W and chi_T") + survivor = (1, 1, 0, 0) + require(word_sign(LEFT, survivor) == word_sign(RIGHT, survivor), + "this relation does not decide chi_KW") + return permitted, free_permitted + + +def check_boundaries(source, global_phases): + a = literal(LEFT, 0, source) + b = literal(RIGHT, 0, source) + require((a[1] + a[2] - b[1] - b[2]) % 4 != 0, "unsigned identity is false") + require(literal(LEFT.replace("P", "", 1), 1, source)[:2] + != literal(LEFT, 1, source)[:2], + "omitting ADDRESS changes the new word") + require(a[:2] == b[:2], "discarding outer phase would lose the negative sign") + for multiplicity in range(1, 9): + actual = (global_phases[0] - global_phases[1]) % 4 + misplaced = multiplicity * actual % 4 + require(actual == 2, "all-f scalar sign") + if multiplicity % 2 == 0: + require(misplaced != actual, "global phase cannot move inside tensor") + for assignment in ((0, 1, 0, 1), (0, 0, 1, 1)): + require(word_sign(LEFT, assignment) == word_sign(RIGHT, assignment), + "a nontrivial ADDRESS sign escapes this obstruction") + + +def receipt_hashes(): + result = {INPUT: INPUT_SHA256} + for name in FILES: + data = (HERE / name).read_bytes() + require(len(data) <= 1048576, "package file capacity") + result[name] = sha256(data).hexdigest() + return result + + +def main(): + source = load_source() + phases = check_relation(source) + permitted, free_permitted = check_characters() + check_boundaries(source, phases) + result = { + "status": "PASS_CUT58_FREE_ADDRESS_CHARACTER_OBSTRUCTION", + "relation": "PWKPW = -TWKPK", + "claim_type": "scoped proof with exact finite corroboration", + "literal_basis_columns": 4096, + "character_assignments": 16, + "assignments_not_excluded_by_this_relation": permitted, + "free_ADDRESS_assignments_not_excluded": free_permitted, + "excluded_free_ADDRESS_characters": ["chi_W", "chi_T"], + "chi_KW_extension": "not decided", + "tensor_multiplicity": "every positive integer, by the written proof", + "new_kappa": False, + "sha256": receipt_hashes(), + } + print(json.dumps(result, sort_keys=True, indent=2)) + + +if __name__ == "__main__": + main()