diff --git a/research/nilpotent-chain-reflection-compiler/PROOF.md b/research/nilpotent-chain-reflection-compiler/PROOF.md new file mode 100644 index 0000000000..f727eb1e2f --- /dev/null +++ b/research/nilpotent-chain-reflection-compiler/PROOF.md @@ -0,0 +1,148 @@ +# Optimal fixed-involution compilation of a nilpotent chain + +This contribution was produced by Nick Petalas. Apache-2.0. + +## Contract and theorem + +Work over the full formal group algebra F2[C2], where C2={1,g} and g is a +fixed nonidentity involution. Put Q=1+[g], so Q is nonzero and Q^2=0. +Let J_n have ones immediately above its diagonal and zero elsewhere. +The complete endpoint on n arbitrary input roles is + + D_n = I + Q J_n. + +Any finite number of additional arbitrary dirty roles is permitted, but the +endpoint on all roles must be I+Q(J_n direct-sum 0). Every extra role must +be restored without residual couplings. Clean initialization, erasure, +discarded roles, other address labels and address-dependent free maps are +excluded. A paid call is I+Q P for a binary rank-one idempotent P. +Arbitrary constant binary invertible scalar maps may occur freely anywhere. + +For every positive integer n, the exact minimum paid-call count is + + L_n = 2 floor(n/2). + +Thus L_n=n-1 for odd n and L_n=n for even n. This includes L_1=0. +An explicit stream needs no extra role, uses exactly 2(n-1) scalar XORs, +and contains every scalar conjugator and its inverse. Scalar optimality is +not claimed. The executable emits this stream for 1<=n<=64; that bound is +an implementation limit, not a restriction of the proof. + +## Lower bound with arbitrary restored dirty workspace + +The normalization here is the standard register-model argument retained in +PR2716 and the earlier register lineage. Conjugating a paid call by a constant +binary invertible scalar matrix conjugates P, preserving rank-one +idempotence. Commute all scalar maps to one end. Augmentation [g] -> 1 +makes every paid call and the required endpoint the identity, so their +remaining scalar product must be the identity as well. + +Because Q is central and Q^2=0, the complete word now satisfies + + product_j (I+Q P_j) = I+Q sum_j P_j. + +Comparing the coefficient of [g] in the full formal algebra gives + + J_n direct-sum 0 = sum_(j=1)^L P_j. + +Rank subadditivity gives L>=rank(J_n)=n-1. Each rank-one idempotent has trace +one over F2, whereas J_n has trace zero. Consequently L is even. The +smallest even integer at least n-1 is 2 floor(n/2). Dirty padding changes +neither rank nor trace, so the lower bound covers every finite allowed +workspace and every placement of free scalar maps. + +The rank, trace and normalization tools are credited background. The new +step is a matching stream for these non-square-zero chain targets. + +## Pair adjacent edges + +For three consecutive coordinates a,b,c, write e_a,e_b,e_c for the coordinate +columns. The two matrices + + P = (e_a+e_b)e_b^T, + R = e_b(e_b^T+e_c^T) + +are rank-one idempotents. Their defining column/row pairings both equal one. +Their sum is + + P+R = e_a e_b^T + e_b e_c^T. + +The repeated diagonal term e_b e_b^T cancels in characteristic two. +It follows in the complete formal algebra that + + (I+Q R)(I+Q P) = I+Q(e_a e_b^T+e_b e_c^T). + +No commutation of P and R is assumed. Every cross term vanishes because +it contains Q^2. These two adjacent chain edges therefore cost two calls. + +Here is the full chronological coordinate stream, where each addition is +a scalar whole-role XOR and g acts only on the indicated role: + + a += b + b <- g(b) + a += b + b += c + b <- g(b) + b += c + +For arbitrary initial a,b,c, the first three operations leave +(a+b+g(b), g(b), c). The last three leave + + (a+b+g(b), b+c+g(c), c). + +This derives the full dirty-state endpoint without assuming any input is +zero. The stream has exactly two reflections and four scalar additions. + +## Complete chain and invoice + +Partition the n-1 edges into consecutive pairs, starting with edges +(0,1),(1,2), then (2,3),(3,4), and so on. Use the six-operation stream for +each pair. If n is even, one edge (n-2,n-1) remains. For that edge use the +retained factorwise four-operation stream + + a += b; b <- g(b); a += b; b <- g(b). + +It maps (a,b) to (a+b+g(b),b), using two reflections and two scalar additions. +The paired streams can share endpoint roles. Their formal product is still +I+Q times the sum of their edge matrices, since all cross terms contain Q^2. +Thus they compose to D_n in any order and leave every spectator untouched. + +There are floor((n-1)/2) pairs and one remaining edge exactly when n is even. +The reflection total is 2 floor((n-1)/2)+2*1_(n even)=2 floor(n/2). +The scalar total is 4 floor((n-1)/2)+2*1_(n even)=2(n-1). +This attains the lower bound and proves the theorem. Reversing the complete +stream gives its inverse, and D_n^2=I by Q^2=0. + +At complete stationary primitive prices R for a coordinate reflection and +C for a whole-role scalar XOR, the specified local bills are + + factorwise PR2716 lowering: 2(n-1)R + 2(n-1)C; + supplied joint lowering: 2 floor(n/2)R + 2(n-1)C. + +The exact reduction is (n-1)R for odd n and (n-2)R for even n. It is strictly +positive for n>=3 and R>0. These are primitive-count identities, not measured +runtime or admitted recursive supplier prices. A supplied scalar change of +basis S transports the construction to S J_n S^-1, but S and S^-1 must be +charged. No method for finding or physically hosting a favorable S is supplied. + +## Scope and predecessors + +ywz65's PR2716 supplies the arbitrary-coupling motivation, Q^2 product identity +and factorwise dirty lowering. Its dihedral tariff and executable are cited, +not audited or replayed. Adam Gall PR1911 and the retained eumemic PR288, +Ali Romman PR468, woklerx PR1443, Gareth Davidson PR1333, Arham Tahir PR1589 +and Cinna Davis PR2290 register-model lineage retain credit. + +Nick Petalas's older PR4912 proves a different tariff for square-zero +couplings. Its extra rank-saturation obstruction is inapplicable to J_n for +n>=3, because J_n^2 is nonzero. JoyboyBrian's PR5007 changes the workspace +contract to returned clean roles. Nick Petalas's PR5857 reduces scalar work +in that clean square-zero stream. The present result has arbitrary dirty +inputs, requires no clean role, and changes both the endpoint and the +reflection-count question. None of those predecessor executables is imported. + +The universal conclusion rests on the written proof. The finite exact checks +corroborate it. Native legality, complete routing/frame/basis/ownership, +precision/tape/stock costs, recursive child admission and the multiplication +theorem remain open. No new kappa, selected-frontier change, independent human +review or formal proof-kernel acceptance is claimed. diff --git a/research/nilpotent-chain-reflection-compiler/README.md b/research/nilpotent-chain-reflection-compiler/README.md new file mode 100644 index 0000000000..668d81efa2 --- /dev/null +++ b/research/nilpotent-chain-reflection-compiler/README.md @@ -0,0 +1,129 @@ +# Optimal reflection compilation of a nilpotent chain + +This contribution was produced by Nick Petalas. + +For a binary nilpotent Jordan chain J_n, the exact fixed-involution +reflection-call minimum is **2 floor(n/2)**, with arbitrary free binary scalar +mixing and any finite restored dirty workspace. An explicit stream attains +it without extra roles, using exactly 2(n-1) scalar XORs. Claim type: scoped +written algebraic proof with exact finite corroboration. + +The first new case, n=3, costs two reflections and four XORs. Applying +ywz65's [PR2716](https://github.com/CrocSwap/integer-mult-bounds/pull/2716) +factorwise lowering to its two edges costs four reflections and four XORs. +Pairing adjacent edges saves address work without adding scalar operations. +The improvement stops here; multiple-block optimization is left open. + +The endpoint is I+(1+[g])J_n over full formal F2[C2], for one fixed nonidentity +involution g. A paid call has a binary rank-one idempotent coupling. Every +input is arbitrary dirty data; spectators must be restored. [PROOF.md](PROOF.md) +derives the full endpoint, its rank/trace lower bound and the complete +chronological primitive invoice. [compiler.py](compiler.py) emits the literal +stream for 1<=n<=64; the written theorem covers every positive n. + +At complete stationary primitive prices R,C, the supplied local bill is +2 floor(n/2)R+2(n-1)C instead of 2(n-1)R+2(n-1)C. Common basis transport +must be charged separately. No native prices or scalar-network optimum are +claimed. The result gives no new kappa or selected-frontier change. + +## Reproduce and evidence + +From the repository root with CPython 3.12 and the standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/nilpotent-chain-reflection-compiler/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/nilpotent-chain-reflection-compiler/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/nilpotent-chain-reflection-compiler +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/nilpotent-chain-reflection-compiler --check-source-history +``` + +Substitute another CPython 3.12 interpreter elsewhere. Direct replay prints +`PASS_NILPOTENT_CHAIN_REFLECTION_COMPILER` in a generated JSON receipt bound +to the package-file hashes. Normal verification writes nothing. Registered +normal and optimized modes use explicit checks that remain active under -O. + +The verifier checks 64 complete formal endpoints and their inverses, 2,048 +rank-one idempotent summands, and every primitive invoice. A separate literal +bit-array interpreter checks all 87,380 two-address states at chain lengths +1 through 8, another 21,504 states with two dirty spectators, and 52,083 +complete input columns across every involutory permutation on one through +six addresses. This last domain contains 119 permutations, including identity +actions as upper-bound controls. Literal checks compare against simultaneous +updates of immutable original inputs, so an in-place ordering error is exposed. + +Separate complete two-call domains contain 784 ordered projector pairs on +three roles and 14,400 on four roles. Each has exactly two witnesses for the +new J_3 endpoint and no one-call witness. These small enumerations corroborate +the construction; the universal minimum comes from the written rank/parity +argument. All 84 single-primitive omissions at n=3 through 8 fail. Six invalid +compiler boundaries, a noninvolutory address substitution and a wrong reflection +role are rejected. No predecessor executable or census is imported or replayed. + +## Scope and provenance + +The `bit-new-register-model` card is changed to this constructive compiler side +question. It does not satisfy the card's native-supplier admission gate. +The prescribed current selected-baseline metadata command passed before work; +that check is not a mathematical premise. Canonical base is +7c49fe32c55de02c2c873655c804b16e4c3fef0a, priorities revision 8, selected PR6030 +with conditional kappa 0.003125804 and all five framework assumptions retained. +[TASK.json](TASK.json) records the scope change and source diversity. +[SOURCES.json](SOURCES.json) pins cited proof context as historical provenance; +the verifier needs no predecessor input, Git, network or third-party package. + +The [advance CLAIM](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19370175) +followed live PR bodies, recent account submissions, handoffs, local reservations, +all-main README searches and merged distinctive-term searches. The overlap +helper's initial local coverage was 133 of 8,917 HEAD notes, so sparse no-match +results were supplemented by full main-tree searches. Its complete remote +pagination covered 506 open PR bodies at 09:05:30 UTC and 6,500 Discussion +records at 09:06:46 UTC on November 3, 2026. Remote text snapshots, +unpublished work and arbitrary historical diffs limit novelty coverage. + +Only the fixed-involution formal endpoint and the supplied primitive stream +are settled. Several Jordan blocks, other paid labels, clean or discarded +workspace, native reflection legality, complete routing/frame/basis/ownership, +precision/tape/stock, recursive admission and the multiplication theorem remain +outside scope. No selected cold scientific replay, Lean or Docker run is supplied. +Independent human and formal proof-kernel review are unclaimed. + +## Open next questions + +- Determine the exact joint tariff for several nilpotent Jordan blocks. Start + with one specified partition and its rank/trace lower bound; independent + block compilation can leave parity or sharing opportunities. This proof + supplies no general minimum over all nilpotent matrices. +- Bind one actual native caller to the two-edge stream. Price the coordinate + reflection, every scalar XOR, basis transport and all movement, ownership, + restoration, precision and stock obligations before drawing a supplier or + multiplication-bound consequence. Those native contracts remain unknown. + +## Credit and implementation limits + +Credit ywz65/PR2716 for the arbitrary-coupling interface, square-zero coefficient +product and factorwise dirty lowering; Adam Gall/PR1911 and the retained +eumemic/PR288, Ali Romman/PR468, woklerx/PR1443, Gareth Davidson/PR1333, +Arham Tahir/PR1589 and Cinna Davis/PR2290 register-model lineage. Rank, trace, +Jordan chains and elementary conjugation are classical. Nick Petalas/PR4912 +settles square-zero couplings, JoyboyBrian/PR5007 supplies a returned-clean +compiler, and Nick Petalas/PR5857 optimizes that clean stream's scalar work. +Their results and credits are retained. The new result is the non-square-zero +single-chain compiler and its exact reflection tariff. Apache-2.0. + +Build the Lever led to the literal stream emitter and repeatable checker. +Prove It Works led to full dirty-column execution and omission controls. +Power of Ten bounds the emitter to 64 roles and the census to 87,380 main +states, 21,504 spectator states, 720 candidate permutations per size and +14,400 ordered projector pairs per case. Functions are below 60 physical +lines; there is no recursion, subprocess, network or runtime code generation. +The one-shot verifier reads at most one MiB per package file. + +Rule 3 has a managed-runtime deviation at compiler.py and verify.py: CPython +allocates bounded lists, tuples and integers dynamically. There is no +fixed-pool or steady-service claim. Live state is bounded by 64 role rows, +at most 190 operation records and 120 four-role projectors; exhaustive input +states are streamed. A fixed-storage runtime would require a separate port. +Rule 9 has one fixed local import and standard sorting of the seven local +file names; no unknown callback or dynamic target is accepted. Warning-strict +normal and optimized execution provide interpreter diagnostics. No unavailable +external static analyzer or formal kernel is claimed. diff --git a/research/nilpotent-chain-reflection-compiler/SOURCES.json b/research/nilpotent-chain-reflection-compiler/SOURCES.json new file mode 100644 index 0000000000..44961f6576 --- /dev/null +++ b/research/nilpotent-chain-reflection-compiler/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/dihedral-arbitrary-couplings/README.md", + "usage": "provenance", + "git_blob": "66027d2a8856d931e7b1c8fa9811a65196d01637", + "sha256": "17bc49fd6215c155aacb0e4a8ce4a8e33e83226b8a1b937a638256a39b99f8ee" + } + ] +} diff --git a/research/nilpotent-chain-reflection-compiler/TASK.json b/research/nilpotent-chain-reflection-compiler/TASK.json new file mode 100644 index 0000000000..a2cbd2f9bb --- /dev/null +++ b/research/nilpotent-chain-reflection-compiler/TASK.json @@ -0,0 +1,81 @@ +{ + "schema_version": 1, + "task_id": "bit-new-register-model", + "priority_revision": 8, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "original_card": { + "id": "bit-new-register-model", + "question": "Can an explicitly larger or nonabelian register model escape the scoped three-register obstruction?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/bit-three-register-lower-bound/README.md", + "certificates/selected-result.json", + "research/bit-gl3-mixed-targets-length10/README.md", + "docs/research/community-efficient1000-review.md" + ], + "methods": [ + "Construct the smallest exact identity in a newly specified legal operation alphabet.", + "Derive a target-specific relaxation bound for that same explicit alphabet." + ], + "acceptance_gate": "Name the changed hypothesis, all counted roles and a uniform identity; finite column tests alone do not certify it. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.", + "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse." + }, + "first_experiment": "First compare the alphabet, role count and length with the fully replayed #1974 census and #2027 mixed-root tariff. Identify a changed premise and a legal native implementation; then price one smallest completed instance before searching larger words.", + "bottleneck_link": "A small-width completed saving changes the bit primitive; a finite-address identity alone is insufficient.", + "allowed_variations": [ + "Choose a fixed larger register count or a specified nonabelian operation family." + ], + "scope_change_triggers": [ + "Remaining inside the already-excluded three-register abelian model.", + "Repeating the two-register GL3 census or a covered three-register length without changing a hypothesis; a formal group-algebra word without native conversion is a partial result." + ], + "overlap_terms": [ + "three-register", + "nonabelian", + "group algebra" + ] + }, + "scope_status": "changed", + "actual_scope": "Exact reflection-call tariff and literal scalar invoice for one binary nilpotent Jordan chain in the fixed-involution dirty-workspace compiler.", + "scope_change_reason": "The drawn larger-register/nonabelian track is narrowed to a constructive compiler side result in PR2716. The new target has adjacent non-square-zero chain edges; it is not a diagonal group-word census or supplier admission.", + "bottleneck_link": "The compiler separates an optimistic coupling-rank price from actual coordinate reflection invocations. Pairing adjacent edges removes paid address calls without shifting work into extra scalar XORs. No current native supplier is bound.", + "budget_minutes": 60, + "stop_rule": "Stop at the first verified adjacent-edge improvement, package its uniform single-chain formula, and leave multiple-block and native-caller questions open.", + "outcome": "completed", + "evidence": "PROOF.md; compiler.py; independent full-formal and literal-bit-array checks in verify.py; hash-bound generated stdout receipts.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "What is the exact joint tariff for several nilpotent Jordan blocks?", + "why_it_matters": "Compiling each block separately may leave parity or workspace-sharing savings.", + "first_step": "Specify the full block partition and compare its rank/trace lower bound with an explicit projector sum.", + "blocked_by": "The present construction pairs adjacent edges within one chain only; no general minimal decomposition is proved." + }, + { + "question": "Can a literal native caller realize this local stream at favorable complete prices?", + "why_it_matters": "A formal reflection-call saving alone does not improve the selected multiplication bound.", + "first_step": "Choose one non-square-zero chain coupling and bind its coordinate reflection and every scalar XOR to actual source operations.", + "blocked_by": "Native legality, basis transport, routing, ownership, precision, tapes, stock and recursive pricing remain unbound." + } + ], + "coordination": { + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19370175", + "source_pr": 2716, + "source_author": "ywz65", + "source_head": "74c96ae917fe16160db357c361058b3a6417a440", + "checked_main": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "priority_revision": 8, + "scope_diversity": "PR5857 optimizes a returned-clean square-zero stream; this theorem changes both the dirty-workspace contract and the non-square-zero coupling, and minimizes reflection calls rather than scalar gates. PR4912 is older than seven days and its square-zero theorem is cited only for scope comparison.", + "coverage_limits": "Live PR bodies, recent handoff comments, merged distinctive terms and all-main README searches supplement a sparse overlap cache. Arbitrary diffs and unpublished work are not exhausted." + }, + "claim_type": "scoped written algebraic proof with exact finite corroboration" +} diff --git a/research/nilpotent-chain-reflection-compiler/VERIFY.json b/research/nilpotent-chain-reflection-compiler/VERIFY.json new file mode 100644 index 0000000000..3b3ce8baf7 --- /dev/null +++ b/research/nilpotent-chain-reflection-compiler/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Full formal endpoints, primitive invoices, complete dirty-input fixtures, literal permutation columns, shortest rank-two-chain pair domains and rejection controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "The same exact checks with assertions disabled; explicit contracts remain active." + } + ] +} diff --git a/research/nilpotent-chain-reflection-compiler/compiler.py b/research/nilpotent-chain-reflection-compiler/compiler.py new file mode 100644 index 0000000000..50ef24741d --- /dev/null +++ b/research/nilpotent-chain-reflection-compiler/compiler.py @@ -0,0 +1,41 @@ +"""Literal binary Jordan-chain compiler, produced by Nick Petalas. + +Apache-2.0. The executable caps roles at 64; the written theorem is uniform. +""" + +MAX_ROLES = 64 + + +def compile_chain(length, roles=None): + """Return chronological (operation, target, source) primitive records. + + ``xor`` adds one whole source role to a target. ``reflect`` applies the + same supplied linear involution to one role; its source equals its target. + Extra roles start arbitrary and are untouched. No clean role is needed. + """ + if type(length) is not int or not 1 <= length <= MAX_ROLES: + raise ValueError("chain length must be an integer from 1 through 64") + if roles is None: + roles = length + if type(roles) is not int or not length <= roles <= MAX_ROLES: + raise ValueError("role count must be an integer between length and 64") + program = [] + for first in range(0, length - 2, 2): + middle, last = first + 1, first + 2 + program.extend(( + ("xor", first, middle), + ("reflect", middle, middle), + ("xor", first, middle), + ("xor", middle, last), + ("reflect", middle, middle), + ("xor", middle, last), + )) + if length % 2 == 0: + first, last = length - 2, length - 1 + program.extend(( + ("xor", first, last), + ("reflect", last, last), + ("xor", first, last), + ("reflect", last, last), + )) + return tuple(program) diff --git a/research/nilpotent-chain-reflection-compiler/verify.py b/research/nilpotent-chain-reflection-compiler/verify.py new file mode 100644 index 0000000000..fb9546ae5c --- /dev/null +++ b/research/nilpotent-chain-reflection-compiler/verify.py @@ -0,0 +1,240 @@ +"""Exact bounded checks, produced by Nick Petalas. Apache-2.0.""" + +import hashlib +import itertools +import json +from pathlib import Path +import sys + +PACKAGE = Path(__file__).resolve().parent +sys.path.insert(0, str(PACKAGE)) +from compiler import compile_chain + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def rank(rows): + basis = [0] * len(rows) + result = 0 + for row in rows: + value = row + for column in range(len(rows) - 1, -1, -1): + if (value >> column) & 1: + if basis[column]: + value ^= basis[column] + else: + basis[column] = value + result += 1 + break + return result + + +def formal(program, roles): + """Propagate every dirty input in the basis 1,g of the full F2[C2].""" + ordinary = [1 << index for index in range(roles)] + reflected = [0] * roles + for operation, target_role, source in program: + require(0 <= target_role < roles and 0 <= source < roles, "bad role") + if operation == "xor": + require(target_role != source, "noninvertible scalar addition") + ordinary[target_role] ^= ordinary[source] + reflected[target_role] ^= reflected[source] + else: + require(operation == "reflect" and target_role == source, "bad opcode") + ordinary[target_role], reflected[target_role] = reflected[target_role], ordinary[target_role] + return tuple(ordinary), tuple(reflected) + + +def target(length, roles): + ordinary = [1 << index for index in range(roles)] + reflected = [0] * roles + for index in range(length - 1): + ordinary[index] ^= 1 << (index + 1) + reflected[index] = 1 << (index + 1) + return tuple(ordinary), tuple(reflected) + + +def projectors(length, roles): + """Construct the proof's summands independently of the primitive stream.""" + result = [] + for first in range(0, length - 2, 2): + middle, last = first + 1, first + 2 + left, right = [0] * roles, [0] * roles + left[first] = left[middle] = 1 << middle + right[middle] = (1 << middle) | (1 << last) + result.extend((tuple(left), tuple(right))) + if length % 2 == 0: + first, last = length - 2, length - 1 + left, right = [0] * roles, [0] * roles + left[first] = left[last] = right[last] = 1 << last + result.extend((tuple(left), tuple(right))) + return result + + +def matrix_product(left, right): + result = [] + for row in left: + value = 0 + for column, other in enumerate(right): + if (row >> column) & 1: + value ^= other + result.append(value) + return tuple(result) + + +def formal_checks(): + summands = 0 + for length in range(1, 65): + roles = min(64, length + 3) + program = compile_chain(length, roles) + require(formal(program, roles) == target(length, roles), "formal endpoint") + require(formal(program[::-1], roles) == target(length, roles), "inverse endpoint") + turns = sum(operation == "reflect" for operation, _, _ in program) + scalar = sum(operation == "xor" for operation, _, _ in program) + require(turns == 2 * (length // 2), "reflection tariff") + require(scalar == 2 * (length - 1), "scalar invoice") + total = [0] * roles + factors = projectors(length, roles) + require(len(factors) == turns, "summand invoice") + for factor in factors: + require(rank(factor) == 1, "summand rank") + require(matrix_product(factor, factor) == factor, "idempotence") + require(sum((row >> i) & 1 for i, row in enumerate(factor)) % 2 == 1, + "summand trace") + total = [a ^ b for a, b in zip(total, factor, strict=True)] + summands += 1 + require(tuple(total) == target(length, roles)[1], "projector sum") + require(rank(total) == length - 1, "chain rank") + return {"formal_chain_lengths": 64, "projector_summands": summands} + + +def literal(program, values, permutation): + """Execute whole bit arrays, independently of formal matrix coefficients.""" + state = list(values) + for operation, destination, source in program: + if operation == "xor": + state[destination] ^= state[source] + elif operation == "reflect": + image = 0 + for address, moved in enumerate(permutation): + image |= ((state[destination] >> address) & 1) << moved + state[destination] = image + else: + raise ValueError("unknown literal primitive") + return tuple(state) + + +def expected(values, length, permutation): + result = list(values) + for destination in range(length - 1): + source = values[destination + 1] + image = sum(((source >> i) & 1) << moved + for i, moved in enumerate(permutation)) + result[destination] ^= source ^ image + return tuple(result) + + +def exhaustive_states(): + counts = {"two_address_states": 0, "dirty_spectator_states": 0} + domains = [(n, n, "two_address_states") for n in range(1, 9)] + domains += [(n, n + 2, "dirty_spectator_states") for n in range(3, 6)] + for length, roles, key in domains: + program = compile_chain(length, roles) + for code in range(1 << (2 * roles)): + values = tuple((code >> (2 * i)) & 3 for i in range(roles)) + result = literal(program, values, (1, 0)) + require(result == expected(values, length, (1, 0)), "dirty state") + counts[key] += 1 + return counts + + +def basis_checks(): + columns = permutations = 0 + for size in range(1, 7): + for permutation in itertools.permutations(range(size)): + if any(permutation[permutation[i]] != i for i in range(size)): + continue + permutations += 1 + for length in (3, 4, 5, 8, 17, 32): + roles = length + 2 + program = compile_chain(length, roles) + for column in range(roles * size): + values = [0] * roles + values[column // size] = 1 << (column % size) + result = literal(program, values, permutation) + require(result == expected(values, length, permutation), "literal column") + columns += 1 + return {"involutory_permutations": permutations, "literal_basis_columns": columns} + + +def pair_census(): + """Check the new rank-two chain's complete shortest two-call domain.""" + counts = [] + for roles in (3, 4): + factors = [] + for vector in range(1, 1 << roles): + for functional in range(1, 1 << roles): + if (vector & functional).bit_count() % 2: + factors.append(tuple(functional if (vector >> i) & 1 else 0 + for i in range(roles))) + goal = target(3, roles)[1] + require(goal not in factors, "unexpected one-call endpoint") + hits = 0 + for left in factors: + for right in factors: + hits += tuple(a ^ b for a, b in zip(left, right, strict=True)) == goal + require(hits > 0, "complete two-call domain has no witness") + counts.append({"roles": roles, "ordered_pairs": len(factors) ** 2, "hits": hits}) + return {"rank_two_chain_pair_censuses": counts} + + +def rejection_checks(): + omissions = 0 + for length in range(3, 9): + program = compile_chain(length) + for index in range(len(program)): + mutant = program[:index] + program[index + 1:] + require(formal(mutant, length) != target(length, length), "unrejected omission") + omissions += 1 + failures = 0 + for args in ((True,), (0,), (65,), (3, 2), (3, True), (3, 65)): + try: + compile_chain(*args) + except ValueError: + failures += 1 + else: + raise ValueError("invalid compiler boundary admitted") + program = compile_chain(3) + bad_label = any(literal(program, (0, 1 << i, 0), (1, 2, 0)) != + expected((0, 1 << i, 0), 3, (1, 2, 0)) for i in range(3)) + require(bad_label, "noninvolutory-label control") + wrong = tuple((op, 0, 0) if op == "reflect" else (op, a, b) + for op, a, b in program) + require(formal(wrong, 3) != target(3, 3), "wrong reflection role") + return {"primitive_omissions_rejected": omissions, "invalid_boundaries_rejected": failures, + "semantic_controls_rejected": 2} + + +def main(): + report = {"marker": "PASS_NILPOTENT_CHAIN_REFLECTION_COMPILER", + "claim_type": "scoped proof with exact finite corroboration", + "python": sys.version.split()[0], "no_new_kappa": True} + report.update(formal_checks()) + report.update(exhaustive_states()) + report.update(basis_checks()) + report.update(pair_census()) + report.update(rejection_checks()) + files = sorted(PACKAGE.iterdir()) + report["sha256"] = {} + for path in files: + if path.is_file(): + require(path.stat().st_size <= 1_048_576, "oversized package file") + report["sha256"][path.name] = hashlib.sha256(path.read_bytes()).hexdigest() + print(json.dumps(report, sort_keys=True, indent=2)) + + +if __name__ == "__main__": + main()