diff --git a/research/nonlinear-role-recoding/PROOF.md b/research/nonlinear-role-recoding/PROOF.md new file mode 100644 index 0000000000..9a92c8f8d9 --- /dev/null +++ b/research/nonlinear-role-recoding/PROOF.md @@ -0,0 +1,176 @@ +# Rigidity of independent scalar-role recodings + +This scoped written proof was produced by Nick Petalas. Apache-2.0. +The finite checker corroborates the statements; it is not their universal +proof or a proof-kernel certificate. + +## 1. Exact contract + +Let F be any field. Let G be a finite directed graph with at least two +vertices, no loops, and connected underlying undirected graph. An edge +e=(j,i) means that role i is updated from the distinct role j. Assign a +fixed coefficient b_e in F\{0} to each edge. + +For every vertex v choose a bijection f_v:F->F with f_v(0)=0. These maps +are fixed throughout the program. The input to each gate ranges over all +of F^2, including arbitrary dirty values. Let Phi act on a state by applying +f_v to each scalar in role v. Require the conjugacy + +```text +Phi ADD_{i<-j}(1) Phi^-1 = ADD_{i<-j}(b_e) (1) +``` + +for every specified edge, where ADD_{i<-j}(b) updates x_i by b*x_j and +preserves every other coordinate. Equivalently, + +```text +f_i(x+y) = f_i(x) + b_e*f_j(y) for every x,y in F. (2) +``` + +The maps need not be continuous, measurable, differentiable or polynomial. +Equation (2) is a gatewise requirement on independent values, not a finite +trajectory test. An instruction graph records required gate compatibilities; +its edges need not occur in every orientation or at every time. + +## 2. Classification + +**Theorem 1.** Equation (2) holds for every edge if and only if there are +nonzero weights s_v in F and one additive bijection H:F->F such that + +```text +f_v(z) = s_v*H(z), b_(j,i) = s_i/s_j. (3) +``` + +Choose a root r and normalize s_r=1. Then H=f_r and every s_v is unique. +Equivalently, compatible maps exist exactly when the product of edge labels +along every undirected closed walk is one. Reverse traversal uses b_e^-1. + +*Proof.* In (2) put x=0. Zero preservation gives f_i(y)=b_e*f_j(y). +Substitution into (2) gives f_i(x+y)=f_i(x)+f_i(y). Thus f_i is additive, +and f_j=b_e^-1*f_i is additive. Every vertex is incident with an edge, +because the graph is connected and has at least two vertices. + +Starting at r, traverse any undirected path. The equality f_i=b_e*f_j +gives f_v=s_v*f_r, with s_v equal to the product of b_e or b_e^-1 on that +path. Each f_r is onto and nonzero, so two scalars multiplying f_r give the +same function only when the scalars agree. Therefore path products are +independent of the path; every closed-walk product is one. This proves +necessity, uniqueness and (3). + +Conversely, closed-walk consistency defines the nonzero s_v by path +products, and makes every edge label s_i/s_j. Choose any additive bijection +H, for example the identity. Then + +```text +s_i*H(x+y) = s_i*H(x) + (s_i/s_j)*s_j*H(y), +``` + +which is (2). This also proves the converse for every prescribed family +of the form (3). A spanning tree suffices to compute the weights; each +remaining edge is a scalar consistency check. No nonlinear search is needed. + +The characterization applies separately to every nontrivial connected +component. An isolated vertex has no ADD constraint and may have an arbitrary +zero-preserving bijection. Strong connectivity is unnecessary. + +## 3. One phase compatibility fixes the coefficient field + +Now let F=C. Suppose, in addition, that one role r satisfies the unchanged +quarter-turn compatibility + +```text +f_r(i*z) = i*f_r(z) for every z in C. (4) +``` + +The role need not be the chosen root. From f_r=s_r*H and s_r!=0, (4) +implies H(i*z)=i*H(z). Additivity implies integer homogeneity and rational +homogeneity: n*H(z/n)=H(z) for every nonzero integer n. Hence + +```text +H(a*z) = a*H(z) for every a in Q(i). (5) +``` + +Thus H is Q(i)-linear. This is an algebraic conclusion; it does not assert +complex linearity or that H is multiplication by a complex scalar. + +The distinction is real. On Q(i,sqrt(2)), the automorphism +H(a+b*sqrt(2))=a-b*sqrt(2), a,b in Q(i), is Q(i)-linear and bijective, +but is not multiplication by a scalar. A Q(i)-basis containing 1,sqrt(2) +extends this to a Q(i)-linear bijection of C by fixing the other basis +vectors. This existence example requires no computable encoding of arbitrary +complex numbers, and is not a proposed physical operation. + +## 4. Consequence for Gaussian-dyadic native programs + +Apply f_v pointwise to the scalar entries of each finite role array. +The same function is used at every address of that role. For every finite +matrix M with entries in Q(i), (5) and additivity give + +```text +H(M*x) = M*H(x), +``` + +where H acts entrywise. This includes Gaussian-dyadic coefficients and +every finite tensor power of such a matrix. Multiplication by s_v also +commutes with M within role v. Therefore every one-role native instruction +M is unchanged by its role recoding f_v. + +**Corollary 2.** Consider a fixed exact word of unit ADDs and one-role +Q(i)-matrix instructions. Suppose its ADD graph is connected, (1) holds, +and one role has (4). Replace the recoding f_v by the scalar recoding +z->s_v*z. The resulting recoded word has exactly the same native operators, +the same scalar ADD coefficients b_e, the same chronology and the same +all-input endpoint as with the original f_v. + +*Proof.* Theorem 1 gives the ADD coefficients. The preceding commutation +identity gives the native operators. Thus the two conjugated words have +identical instructions. Equivalently, if A is the original whole linear +endpoint, D repeats s_v on every address of role v, and Phi is the nonlinear +pointwise recoding, then + +```text +Phi A Phi^-1 = D A D^-1. (6) +``` + +Indeed H commutes with A entrywise, since the finite whole endpoint is a +Q(i)-matrix. This calculation also covers every finite array width and +tensor multiplicity. It does not infer a uniform physical implementation +from finite computations. + +In particular, arbitrary dirty restoration x_v->x_v remains restoration, +zero owned fields remain zero, and all native paid labels are unchanged. +Every recoded word in this class has a scalar-gauge counterpart with the +same endpoint and native profile. Scalar gauges themselves are allowed +recodings, so the sets of attainable endpoints/profiles are equal. + +This is a native-profile statement. Ordinary scalar coefficient costs, +encoding/decoding, precision, storage and movement retain their own costs. +If allowed coefficients are restricted, the counterpart uses exactly the +same b_e as the proposed recoded word. Boundary weights do not become free +physical instructions. No productive target or recursive invoice gain +follows merely from the conjugacy. + +## 5. Boundaries and exact counterexamples + +- Without zero preservation, translations on a sink survive. Over F5, take + f_source(x)=x and f_target(x)=x+1. Equation (2) holds with b=1, but (3) + fails at zero. An affine version would require a separate statement. +- Without connectedness, an isolated role can carry a nonadditive bijection. + Independent nontrivial components may also use different additive maps. +- Additivity does not imply (4). Complex conjugation preserves ADD but sends + i to -i. Over F9, Frobenius x->x^3 gives a finite counterpart. +- Phase compatibility does not imply additivity. The F9 checker enumerates + every zero-preserving permutation and supplies phase-only witnesses. +- Pointwise recoding matters. Swapping two addresses is Q(i)-linear but + does not commute with the address operator diag(1,2). +- Changing the recoding at different occurrences, changing a native + instruction, using input-dependent coefficients, approximate identities, + nonzero translations, or restricting reachable inputs changes the contract. + General nonlinear circuits and finite-grid rounded implementations are + outside the theorem. + +The shared-map scalar condition in Cinna Davis's PR #4983 is a predecessor, +not a new claim here. The new application permits independent maps on every +role and changed edge coefficients, then identifies their complete residual +freedom and the Gaussian-native consequence. Cauchy's functional equation, +spanning-tree gauge consistency and linear-map commutation are classical. diff --git a/research/nonlinear-role-recoding/README.md b/research/nonlinear-role-recoding/README.md new file mode 100644 index 0000000000..a13e9f1c5a --- /dev/null +++ b/research/nonlinear-role-recoding/README.md @@ -0,0 +1,132 @@ +# Independent nonlinear scalar-role recodings reduce to scalar gauges + +This contribution was produced by Nick Petalas. Apache-2.0. + +**Claim type: scoped written obstruction, with exact finite corroboration.** +Fixed arbitrary zero-preserving bijections on separate scalar roles add no +native-profile freedom to the declared connected ADD/native interface. +No continuity, measurability or differentiability is assumed. + +For a connected directed ADD graph, write an edge as source j to target i. +Every family satisfying + +```text +f_i(x+y) = f_i(x) + b_(j,i)*f_j(y) for all independent x,y +``` + +has exactly the form f_v=s_v*H, with one common additive bijection H and +b_(j,i)=s_i/s_j. Existence is equivalent to multiplicative consistency around +every undirected closed walk. Reverse traversal uses the reciprocal label. +The graph need only be weakly connected. + +If one role also preserves multiplication by i, H is Q(i)-linear. Applied +pointwise, it commutes with every Gaussian-dyadic native matrix and all its +finite tensor powers. For every fixed word in this gate class, + +```text +Phi A Phi^-1 = D A D^-1, D=diag(s_v), +``` + +with the weights repeated over each role's addresses. Thus every proposed +nonlinear recoding has a scalar-gauge counterpart with the identical native +operators, scalar ADD coefficients, chronology and endpoint, including dirty +restoration. The native paid profiles attainable in the two classes are equal. +Boundary adapters and ordinary scalar work retain their costs. + +[PROOF.md](PROOF.md) states and proves the universal classification and +its exact contract. This identifies an escape route that cannot improve +the current helper mechanism under unchanged gatewise compatibility. It does +not exclude nonlinear arithmetic with a different instruction contract. + +## Evidence and reproduction + +The standalone checker imports no predecessor executable and writes only +standard output. Its generated receipt hashes all six package files. +It enumerates: + +- 5,632 map/label assignments over F3 on all 54 connected directed three-role + graphs. Exactly 432 satisfy the literal gate equations and the classification. +- 1,105,920 map/label assignments over F5 on a directed path and directed + triangle, including every zero-preserving role permutation and every nonzero + edge label. Exactly 128 are compatible. +- All 40,320 zero-preserving permutations of F9. There are 48 additive maps, + 32 maps commuting with multiplication by i, and eight satisfying both. + Phase compatibility and additivity are independently necessary. +- 48 complete seven-event word fixtures over Q(i,sqrt(2)), including all + 24 rational basis columns and 24 mixed dirty inputs. A genuinely non-scalar + Q(i)-linear recoding gives the same 288 scalar outputs as direct scalar + gauges and the recoded gate word. These compare 1,152 rational components. +- Nine graph/domain/ratio and hypothesis controls. The extension census also + supplies explicit phase-only and additive-but-not-phase witnesses. + +From the repository root, use CPython 3.12 with the standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/nonlinear-role-recoding/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -O -B research/nonlinear-role-recoding/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/nonlinear-role-recoding +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/nonlinear-role-recoding --check-source-history --check-modes +``` + +Any CPython 3.12 path may replace the local interpreter path. Expected markers +are `PASS_NONLINEAR_ROLE_RECODING`, `PASS_REGISTERED_RESEARCH_PACKAGE` and +`PASS_RESEARCH_COMMIT_BYTES`. The registered commands run the complete same +finite domains in normal and optimized modes, each with a 60-second limit. +The written proof, rather than these finite fields, establishes the result +over C and every finite address width. + +## Scope and credit + +Cinna Davis's [PR #4983](https://github.com/CrocSwap/integer-mult-bounds/pull/4983) +proves additivity for a shared frame potential commuting with unchanged ADDs +and binds that condition to a source word. Its result and source audit are +cited, not rechecked here. The new application classifies independent role +maps and changed coefficients, then removes their nonlinear freedom from the +Gaussian-native interface. Cauchy's functional equation, scalar gauge +consistency and linear commutation are classical. No general literature +priority is claimed for those methods. + +[SOURCES.json](SOURCES.json) pins the predecessor statements and assignment +provenance at canonical main `19fdb086ea96af9a9f87936a2b888e10af4ed810`, +priority revision 8. No scientific external input is executed. The selected +source-binding orientation passed; it is not a supplier replay. +The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19228562) +records this original scope. The first classification ended the research. + +Maps are fixed per role, scalar, pointwise and zero-preserving; the equations +hold on arbitrary independent values. One phase compatibility and connected +ADD graph are explicit hypotheses. Occurrence-dependent maps, non-pointwise +address operations, changed nonlinear gates, restricted reachable inputs, +finite-grid rounding and approximate identities remain outside the claim. + +No physical encoding, source-specific paid deletion, complete signed invoice, +precision bound, compiler/hosting admission, new kappa, selected-frontier +change or complete multiplication theorem is supplied. Independent human +and formal proof-kernel review are unclaimed. The five retained framework +assumptions remain. + +## Verifier bounds and diagnostics + +All domains are fixed. The largest role-permutation table contains 24 maps; +the F9 permutation iterator holds one eight-entry permutation at a time. +There are at most 64 label tuples for one graph, and graph propagation uses +exactly n edge scans. The native fixture contains three roles and two +addresses per role, with four rational components per scalar. Every function +is shorter than 60 physical lines, there is no recursion, and failures use +exceptions that remain active under `-O`. Both modes enable warnings as errors. + +Power-of-ten managed-runtime deviation, rules 3 and 9: Python tuples, +fractions, dictionaries and standard-library iterators allocate dynamically. +The fixed domains above bound live data; there are no input-provided callbacks, +subprocesses or external scientific files. Python does not provide a static +fixed-allocation guarantee. Repository replay diagnostics cover the isolated +package; no repository-wide analyzer configuration is changed. + +## Open next questions + +Can occurrence-dependent recodings improve a complete helper invoice? That +changes the fixed-map hypothesis and could avoid this obstruction. Start with +one pair of consecutive recodings, write the changed scalar/native instructions +and every boundary adapter, then price restoration, storage and the complete +signed bill. No such physical construction or bill is supplied here. +The structured question is retained in [TASK.json](TASK.json). diff --git a/research/nonlinear-role-recoding/SOURCES.json b/research/nonlinear-role-recoding/SOURCES.json new file mode 100644 index 0000000000..264d5d5629 --- /dev/null +++ b/research/nonlinear-role-recoding/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/coherent-frame-additivity/README.md", + "usage": "provenance", + "git_blob": "5c72c03ba7887aedad30acf4c20f40346da2fee5", + "sha256": "cf6889e806a9b4fa9a75beccefaa998627a9b35b77be529f0fe26718f60b9d67" + }, + { + "path": "research/coherent-frame-additivity/PROOF.md", + "usage": "provenance", + "git_blob": "67dd02c9d31d77be390a9e3fdfc09c7dd8de56c2", + "sha256": "0f72ad943e6f1803d6cdc5749f6b6880463fc8dba8ce57e8de3c3550a8eaea79" + } + ] +} diff --git a/research/nonlinear-role-recoding/TASK.json b/research/nonlinear-role-recoding/TASK.json new file mode 100644 index 0000000000..b8b7334aac --- /dev/null +++ b/research/nonlinear-role-recoding/TASK.json @@ -0,0 +1,86 @@ +{ + "schema_version": 1, + "task_id": "complex-new-helper-inventory", + "priority_revision": 8, + "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "original_card": { + "id": "complex-new-helper-inventory", + "question": "Can a changed helper inventory earn productive credit that survives completion, compilation and the actual caller?", + "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": "Specify all arbitrary inputs, owned fields, restored outputs and a physically legal consumer. Compare complete P and T, including target debits and precision/stock costs. #5599 is a positive control for target refinement, not permission to split every helper for free. #5614 is a hypothetical compiler budget, not an emitted 145-split word. Stop at the first unpaid boundary or a failing optimistic full bill.", + "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": [ + "productive helper", + "target refinement", + "5599", + "5614" + ], + "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": "Classify independent zero-preserving scalar-role bijections conjugating connected unit ADDs to scalar ADDs, and prove the Gaussian-native consequence of one phase compatibility.", + "scope_change_reason": "The construction card is changed to an original obstruction for a precise nonlinear recoding escape route. No source word or supplier admission is claimed.", + "bottleneck_link": "The complex helper supplier binds. Independent nonlinear role encodings preserving the declared ADD/native interface cannot improve on scalar gauges; a different scalar or native contract is required.", + "budget_minutes": 60, + "stop_rule": "Stop at the first proved classification with exact finite corroboration. Do not expand to other nonlinear circuit models.", + "outcome": "negative-result", + "evidence": "PROOF.md Theorem 1 and Corollary 2; verify.py graph/permutation/native checks and hypothesis controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can occurrence-dependent scalar-role recodings reduce a complete helper invoice while preserving all boundaries?", + "why_it_matters": "Fixed role recodings have only scalar-gauge freedom under the stated gates. Time-dependent recodings change that premise.", + "first_step": "Specify one changed pair of consecutive recodings, its exact scalar/native gate replacements and every endpoint adapter.", + "blocked_by": "No physical changed-gate construction, restoration proof or complete bill is supplied." + } + ], + "coordination": { + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19228562", + "source": "original", + "checked_main": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "priority_revision": 8, + "coverage_limit": "Main README searches, bounded merged/open PR searches, latest handoffs and local reservations; arbitrary diffs and unpublished work remain unsearched." + }, + "environment": { + "python": "CPython 3.12.15", + "platform": "macOS arm64", + "dependencies": "standard library only" + } +} diff --git a/research/nonlinear-role-recoding/VERIFY.json b/research/nonlinear-role-recoding/VERIFY.json new file mode 100644 index 0000000000..0a2ee36c17 --- /dev/null +++ b/research/nonlinear-role-recoding/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": 60, + "checks": "Exact independent graph/gate classification, all F9 permutations, Gaussian-extension endpoint conjugacy and hypothesis controls." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "The same complete finite domains with assertions disabled; all scientific checks use explicit exceptions." + } + ] +} diff --git a/research/nonlinear-role-recoding/verify.py b/research/nonlinear-role-recoding/verify.py new file mode 100644 index 0000000000..e36a8bc4c8 --- /dev/null +++ b/research/nonlinear-role-recoding/verify.py @@ -0,0 +1,287 @@ +"""Exact finite corroboration. Produced by Nick Petalas. Apache-2.0.""" + +from fractions import Fraction as F +from hashlib import sha256 +from itertools import permutations, product +import json +from pathlib import Path +import sys + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def connected(n, edges): + seen = {0} + for _ in range(n): + for source, target in edges: + if source in seen or target in seen: + seen.update((source, target)) + return len(seen) == n + + +def vertex_gauges(n, p, edges, labels): + """Return root-normalized gauges, or None for inconsistent labels.""" + require(2 <= n <= 4 and p in (3, 5), "unsupported finite domain") + require(len(edges) == len(labels) <= n*(n-1), "edge count") + require(len(set(edges)) == len(edges), "duplicate edge") + require(all(0 <= a < n and 0 <= b < n and a != b for a, b in edges), + "invalid directed edge") + require(all(1 <= b < p for b in labels), "invalid label") + require(connected(n, edges), "disconnected graph") + weights = [None] * n + weights[0] = 1 + for _ in range(n): + for (source, target), b in zip(edges, labels): + if weights[source] is not None: + candidate = b * weights[source] % p + if weights[target] is not None and weights[target] != candidate: + return None + weights[target] = candidate + elif weights[target] is not None: + weights[source] = pow(b, -1, p) * weights[target] % p + require(all(w is not None for w in weights), "propagation incomplete") + require(all(weights[t] == b * weights[s] % p + for (s, t), b in zip(edges, labels)), "bad gauge output") + return tuple(weights) + + +def additive(table, addition): + q = len(table) + return all(table[addition[x][y]] == addition[table[x]][table[y]] + for x in range(q) for y in range(q)) + + +def gate_table(p, maps): + # Exhaust the literal equation independently of graph propagation. + return tuple(tuple(tuple(all(target[(x+y) % p] + == (target[x]+b*source[y]) % p + for x in range(p) for y in range(p)) + for b in range(1, p)) for source in maps) + for target in maps) + + +def graph_census(p, graphs): + maps = tuple((0,) + tail for tail in permutations(range(1, p))) + addition = tuple(tuple((x+y) % p for y in range(p)) for x in range(p)) + is_additive = tuple(additive(f, addition) for f in maps) + gates = gate_table(p, maps) + counts = {"graphs": 0, "cases": 0, "compatible": 0} + for edges in graphs: + candidates = tuple((labels, vertex_gauges(3, p, edges, labels)) + for labels in product(range(1, p), repeat=len(edges))) + successes = 0 + for ids in product(range(len(maps)), repeat=3): + chosen = tuple(maps[k] for k in ids) + h = chosen[0] + for labels, weights in candidates: + actual = all(gates[ids[t]][ids[s]][b-1] + for (s, t), b in zip(edges, labels)) + predicted = weights is not None and is_additive[ids[0]] and all( + chosen[v][x] == weights[v]*h[x] % p + for v in range(3) for x in range(p)) + require(actual == predicted, "graph classification mismatch") + counts["cases"] += 1 + successes += actual + require(successes == (p-1)**3, "unexpected compatible count") + counts["graphs"] += 1 + counts["compatible"] += successes + return counts + + +def f9_tables(): + # a+3b denotes a+b*i, i^2=-1 over F3. + add = tuple(tuple((x % 3+y % 3) % 3 + 3*((x//3+y//3) % 3) + for y in range(9)) for x in range(9)) + mul = tuple(tuple(((x % 3)*(y % 3)-(x//3)*(y//3)) % 3 + + 3*(((x % 3)*(y//3)+(x//3)*(y % 3)) % 3) + for y in range(9)) for x in range(9)) + return add, mul + + +def extension_census(): + add, mul = f9_tables() + counts = {"permutations": 0, "additive": 0, "phase": 0, "both": 0} + phase_only = None + for tail in permutations(range(1, 9)): + f = (0,) + tail + a = additive(f, add) + phase = all(f[mul[3][x]] == mul[3][f[x]] for x in range(9)) + counts["permutations"] += 1 + counts["additive"] += a + counts["phase"] += phase + counts["both"] += a and phase + if a and phase: + require(all(f[x] == mul[f[1]][x] for x in range(9)), + "phase-compatible additive map is not scalar") + if phase and not a: + phase_only = f + require(tuple(counts.values()) == (40320, 48, 32, 8), "F9 census") + require(phase_only is not None, "missing phase-only witness") + frobenius = tuple(mul[mul[x][x]][x] for x in range(9)) + require(additive(frobenius, add), "Frobenius not additive") + require(frobenius[3] != mul[3][frobenius[1]], "missing phase counterexample") + return counts, phase_only, frobenius + + +def q(a=0, b=0, c=0, d=0): + """Exact a+b*i+c*sqrt(2)+d*i*sqrt(2).""" + return tuple(F(x) for x in (a, b, c, d)) + + +def plus(x, y): + return tuple(a+b for a, b in zip(x, y)) + + +def times(x, y): + a, b, c, d = x + e, f, g, h = y + return (a*e-b*f+2*(c*g-d*h), a*f+b*e+2*(c*h+d*g), + a*g-b*h+c*e-d*f, a*h+b*g+c*f+d*e) + + +def common_h(x): + return x[0], x[1], -x[2], -x[3] + + +def algebra_controls(): + # Independent monomial multiplication modulo i^2+1 and sqrt(2)^2-2. + basis = ((0, 0), (1, 0), (0, 1), (1, 1)) + values = (q(), q(1), q(0, 1), q(c=1), q(d=1), q(1, 1), + q(F(1, 2), F(-1, 2)), q(2, -3, 5, -7), q(F(1, 3), 0, F(-2, 5))) + pairs = 0 + for x, y in product(values, repeat=2): + expected = [F(0)] * 4 + for a, (i, r) in enumerate(basis): + for b, (j, s) in enumerate(basis): + at = basis.index(((i+j) % 2, (r+s) % 2)) + expected[at] += x[a]*y[b]*(-1)**((i+j)//2)*2**((r+s)//2) + require(times(x, y) == tuple(expected), "extension multiplication") + pairs += 1 + return pairs + + +def recode(state, inverse=False, nonlinear=True): + weights = (q(1, 1), q(2), q(0, -1)) + inverses = (q(F(1, 2), F(-1, 2)), q(F(1, 2)), q(0, 1)) + out = [] + for v in range(3): + row = [] + for x in state[v]: + value = times(inverses[v], x) if inverse else x + if nonlinear: + value = common_h(value) + row.append(value if inverse else times(weights[v], value)) + out.append(tuple(row)) + return tuple(out) + + +def run_word(state, changed_coefficients=False): + weights = (q(1, 1), q(2), q(0, -1)) + inverses = (q(F(1, 2), F(-1, 2)), q(F(1, 2)), q(0, 1)) + c = q(F(1, 2), F(-1, 2)) + zero = q() + word = (("add", 0, 1), ("native", 1, ((c, c), (c, times(q(-1), c)))), + ("add", 1, 2), ("native", 0, ((q(1), zero), (zero, q(0, 1)))), + ("add", 2, 0), ("native", 2, ((q(1), zero), (zero, q(F(1, 2))))), + ("add", 0, 1)) + current = list(state) + for kind, source, target in word: + if kind == "add": + b = times(weights[target], inverses[source]) if changed_coefficients else q(1) + current[target] = tuple(plus(x, times(b, y)) + for x, y in zip(current[target], current[source])) + else: + old = current[source] + current[source] = tuple(plus(times(row[0], old[0]), times(row[1], old[1])) + for row in target) + return tuple(current) + + +def exact_native_census(): + require(common_h(q(1)) == q(1) and common_h(q(c=1)) == q(c=-1), + "non-scalar additive fixture") + fixtures = [] + for position in range(6): + for component in range(4): + state = [q()] * 6 + basis = [0] * 4 + basis[component] = 1 + state[position] = q(*basis) + fixtures.append(tuple((state[2*v], state[2*v+1]) for v in range(3))) + for k in range(24): + row = tuple(q(F(k-j, j+1), F(k+j, 3), F(j-2*k, 5), F(k*j-1, 7)) + for j in range(6)) + fixtures.append(tuple((row[2*v], row[2*v+1]) for v in range(3))) + for state in fixtures: + nonlinear = recode(run_word(recode(state, inverse=True))) + scalar = recode(run_word(recode(state, inverse=True, nonlinear=False)), + nonlinear=False) + direct = run_word(state, changed_coefficients=True) + require(nonlinear == scalar == direct, "native conjugacy mismatch") + require(recode(recode(state), inverse=True) == state, "inverse recoding") + return {"fixtures": len(fixtures), "output_scalars": 6*len(fixtures), + "rational_components": 24*len(fixtures), "events_per_fixture": 7} + + +def controls(): + cases = ((3, 5, (), ()), (3, 5, ((0, 0),), (1,)), + (2, 5, ((0, 1),), (0,)), (2, 5, ((0, 1), (0, 1)), (1, 1))) + count = 0 + for args in cases: + try: + vertex_gauges(*args) + except ValueError: + count += 1 + else: + raise ValueError("invalid graph accepted") + cycle = ((0, 1), (1, 2), (2, 0)) + require(vertex_gauges(3, 5, cycle, (1, 1, 2)) is None, "cycle obstruction") + count += 1 + # Removing zero preservation permits a translation on a sink. + require(all((x+y+1) % 5 == ((x+1) % 5+y) % 5 + for x in range(5) for y in range(5)), "sink translation") + count += 1 + nonadditive = (0, 2, 1, 3, 4) + add = tuple(tuple((x+y) % 5 for y in range(5)) for x in range(5)) + require(not connected(3, ((0, 1),)) and not additive(nonadditive, add), + "disconnected nonadditive fixture") + count += 1 + maps = ((0, 1, 2, 3, 4), (0, 2, 4, 1, 3)) + require(not gate_table(5, maps)[1][0][2], "reversed edge ratio accepted") + count += 1 + # A non-pointwise address swap does not commute with diag(1,2). + x = (1, 2) + left = (2*x[1], x[0]) + right = (x[1], 2*x[0]) + require(left != right, "block-map boundary control") + count += 1 + return count + + +def main(): + require(len(sys.argv) == 1, "no command-line arguments are supported") + arcs = tuple((s, t) for s in range(3) for t in range(3) if s != t) + graphs = tuple(tuple(arcs[j] for j in range(6) if mask >> j & 1) + for mask in range(64)) + graphs = tuple(g for g in graphs if connected(3, g)) + f3 = graph_census(3, graphs) + f5 = graph_census(5, (((0, 1), (1, 2)), ((0, 1), (1, 2), (2, 0)))) + f9, phase_only, frobenius = extension_census() + arithmetic_pairs = algebra_controls() + exact = exact_native_census() + boundary_controls = controls() + files = ("README.md", "PROOF.md", "TASK.json", "SOURCES.json", "VERIFY.json", "verify.py") + root = Path(__file__).resolve().parent + receipt = {"status": "PASS_NONLINEAR_ROLE_RECODING", "F3": f3, "F5": f5, + "F9": f9, "phase_only_witness": phase_only, "frobenius": frobenius, + "arithmetic_pairs": arithmetic_pairs, + "exact_native": exact, "boundary_controls": boundary_controls, + "sha256": {name: sha256((root/name).read_bytes()).hexdigest() for name in files}} + print(json.dumps(receipt, sort_keys=True)) + + +if __name__ == "__main__": + main()