diff --git a/research/flagless-kernel-obstruction/PROOF.md b/research/flagless-kernel-obstruction/PROOF.md new file mode 100644 index 0000000000..78a9e1de94 --- /dev/null +++ b/research/flagless-kernel-obstruction/PROOF.md @@ -0,0 +1,131 @@ +# A coordinate-kernel obstruction for flagless span-six words + +This scoped proof was produced by Nick Petalas. Apache-2.0. + +## Model and inherited premises + +Use the formal abelian model of unpaidmoon's PR4119, with four scalar +roles, eight nonzero rank-one rational 3-by-3 frames A_j and binary +rank-one idempotents N_j. A paid call is + + D_N([A]) = I + ([A]-1) N. + +The endpoint is diag([C_0],...,[C_3]); three specified C_i are invertible. +The fourth role is arbitrarily dirty and may have any diagonal monomial +endpoint. Equality is in the full group algebra of the additive rational +matrix group. No clean allocation or extra free address map is allowed. + +The rational frame span has dimension six. We take the following reductions +from PR4119, sections 2, 3 and 5, as cited mathematical premises. + +1. Cube-relation rank at most one is already excluded. +2. Otherwise the relation lattice has a saturated cube basis r,s, independent + modulo two. For fixed independent off-diagonal patterns B,C, + off(N_j) = (r_j mod 2)B + (s_j mod 2)C. +3. If S indexes noncoordinate projectors and T the coordinate projectors, + r and s vanish on T. Thus all relations are on S, the generated group + splits as H_S direct-sum Z^T, and dim_Q span{A_j:j in S}=|S|-2. + +We also cite waynenilsen's PR1882 theorem: two invertible rational 3-by-3 +data targets need at least six calls, with any finite dirty auxiliary +workspace and arbitrary diagonal monomial auxiliary endpoints. It imposes +no lower-triangularity requirement on the two data targets. The present +proof does not replay or independently establish that theorem. + +## New obstruction + +Suppose the occurring noncoordinate pool has a nonzero common right-kernel +vector v and a nonzero common left-kernel vector w. Put + + U = supp(v) union supp(w). + +If |U|>=2, no such eight-call endpoint exists, provided |S|>=3. +Only existence of these vectors is needed; their kernels need not be +exactly one-dimensional. This hypothesis uses the original coordinates. + +First apply the group homomorphism setting every T generator to zero. +Each coordinate factor becomes I. The surviving S word is still diagonal, +with endpoint diag([C_i^S]); the decomposition gives +C_i=C_i^S+C_i^T. Every S factor fixes v on the right and w^T on the left. +Therefore the diagonal endpoint does too. In the full group algebra, + + C_i^S = 0 for every i in U. (1) + +For example, if v_i=1, the i-th coordinate of Dv=v is [C_i^S]=1. +Distinct rational matrices are distinct formal group elements, so C_i^S=0. +The left-kernel argument is identical. Coordinate calls in the original +word need not preserve either kernel. Removing them uses the group split, +not an invariant-subspace claim about the interleaved full word. + +Let s=|S| and t=|T|, so s+t=8 and s>=3. Every C_i^S belongs to the +frame span on S. A basis can be selected from its rank-one paid frames, +so rank subadditivity gives + + rank(C_i^S) <= s-2. (2) + +Let t_i count coordinate calls with projector E_ii. Project instead onto +Z^T, setting every S generator to zero. The coordinate factors commute +and each contributes to exactly one coordinate, hence + + rank(C_i^T) <= t_i, sum_i t_i=t. (3) + +At least one of the three data coordinates lies in U. If at least two do, +(1) and invertibility force t>=6, contradicting s>=3. Thus exactly one data +coordinate lies in U. Call it a. Equations (1) and (3) force t_a>=3. +For the other two data coordinates, (2)-(3) give + + 3 <= (s-2)+t_i. + +Since t>=3, s<=5. Summing the last two inequalities and reserving the +three calls at a gives + + 6 <= 2(s-2)+(t-3) = s+1. + +Consequently s=5, t=3, t_a=3, and neither other data coordinate has a +T contribution. Both corresponding C_i^S are invertible. But the S word +then realizes two invertible targets in five calls, with the other two +arbitrarily dirty roles ending diagonally. This contradicts PR1882's +six-call theorem. The obstruction follows. + +## Application to the exceptional pools + +PR4119 leaves 72 flagless noncoordinate pools with three projectors and +two realized off-diagonal patterns. woklerx's earlier PR1846 already +classifies these into coordinate-permutation/transpose orbits of sizes +24 and 48. Those classification and orbit-size results retain their +credit. The new contribution excludes the 48-pool orbit as a possible +eight-call realization. The finite corroboration retains the original +four coordinate axes throughout. + +The 48 newly excluded pools are exactly the disjoint coordinate-permutation +orbits of the following triple and its transpose: + + X = 1100/0000/0000/0000, packed 0x0003, + Y = 0100/0100/0000/0000, packed 0x0022, + Z = 0000/1011/1011/0000, packed 0x0dd0. + +Row strings list column 0 first; packed bit 4i+j is entry (i,j). +For this triple v=e_2+e_3 and w=e_3. Thus |U|=2. Transpose exchanges +the left and right kernels. Each coordinate-permutation orbit has 24 +pools, their intersection is empty, and every pool meets the obstruction. +This is a finite certificate attached to the universal scoped argument. + +The remaining 24 pools form the coordinate-permutation orbit of +(0x0003,0x0022,0x0550), the representative in PR4119. Their left and +right kernels have the same single-coordinate support. The new hypothesis +fails there. Their eight-call feasibility, and span five, remain open here. + +## Evidence boundary + +The executable checks the new coordinate orbits, kernel supports, formal +kernel identities and all finite rank-budget allocations. Its formal-word +checks use independent integer exponents, without reducing address frames +modulo two. They corroborate the fixed-vector argument and do not enumerate +rational frame relations or settle arbitrary endpoint feasibility. + +The universal exclusion depends on the cited relation-support reduction +and two-target theorem. Their scientific suites are unrun. This result is +neither independent acceptance of those premises nor a proof-kernel theorem. +Native legality, frames, physical costs, precision/tape, stock, compiler, +recursive supplier admission and the full multiplication theorem are outside +scope. No new kappa or selected-frontier change follows. diff --git a/research/flagless-kernel-obstruction/README.md b/research/flagless-kernel-obstruction/README.md new file mode 100644 index 0000000000..de9c651599 --- /dev/null +++ b/research/flagless-kernel-obstruction/README.md @@ -0,0 +1,121 @@ +# Excluding 48 flagless span-six dirty-auxiliary pools + +Scoped mathematical proof with finite exact corroboration. This contribution +was produced by Nick Petalas. No new kappa or selected-frontier change. + +In the four-register abelian bit model, eight nonzero rank-one calls at +rational frame span six cannot realize three invertible 3-by-3 targets when +their noncoordinate projectors belong to any of 48 specified flagless pools. +The fourth role is arbitrarily dirty and may end at any diagonal monomial. +These are 48 of the 72 exceptional pools left by unpaidmoon's +[PR4119](https://github.com/CrocSwap/integer-mult-bounds/pull/4119). +The other 24 pools, and span five, remain open here. +The scalar catalogue and its 24/48 orbit split were already established +by woklerx's [PR1846](https://github.com/CrocSwap/integer-mult-bounds/pull/1846). +The new result rules out realization of its 48-pool orbit. + +The new step keeps the target coordinate-diagonal. A common left or right +kernel supported on two coordinates forces the noncoordinate subword to +contribute zero on both. One invertible data target then consumes three +coordinate calls. The resulting five-call subword would have to realize two +invertible targets, contradicting waynenilsen's six-call theorem with dirty +auxiliaries. [PROOF.md](PROOF.md) gives the quantified argument and names +its inherited mathematical premises. + +The excluded pools are the disjoint coordinate-permutation orbits of +`(0x0003,0x0022,0x0dd0)` and its transpose. Bit `4i+j` is entry `(i,j)`. +The first pool has common right kernel `e_2+e_3` and common left kernel +`e_3`. Each orbit contains 24 pools. The remaining orbit has representative +`(0x0003,0x0022,0x0550)` and both kernels supported on the same coordinate. +No arbitrary change of basis is used to preserve a coordinate target. + +## Evidence and reproduction + +Use CPython 3.12 and the standard library, from the repository root: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/flagless-kernel-obstruction/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/flagless-kernel-obstruction/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/flagless-kernel-obstruction +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/flagless-kernel-obstruction --check-source-history +``` + +Any CPython 3.12 installation can replace the displayed interpreter. +The direct checker emits `PASS_FLAGLESS_KERNEL_OBSTRUCTION` in a generated +JSON receipt bound to the six package-file hashes. It writes only to stdout, +imports no predecessor code, and works in a Git-free package export. +Correctness checks use explicit exceptions and remain active under `-O`. + +The finite evidence includes the three disjoint coordinate orbits and their +kernel supports, independent literal binary matrix products, 1,920 formal +words through length three and 7,632 coefficient matrices, 3,888 diagonal +label assignments, and 96 critical eight-call rank allocations. Every +critical allocation has five noncoordinate calls and would require the +cited two-target theorem's impossible endpoint. The nine-call budget +control survives this relaxation; it is not a nine-call construction in +the excluded pools. Named controls preserve the remaining coordinate-kernel +orbit and distinguish coordinate interleaving from subword kernel invariance. + +The written proof supplies the universal rational-frame exclusion. The +finite word checks corroborate its kernel identity, rather than enumerate +all rational frame relations or certify every possible endpoint. + +## Scope and provenance + +Canonical base is `ec2780e8aeb1c88acaf5e9e470ef8c68e7fbbb6c`, priority +revision 7. The `bit-new-register-model` card is refined to this explicit +four-register handoff. Its current source-binding orientation command, +`scripts/research_selected_baseline.py`, passes. This authenticates selected +metadata only; it is not a selected cold replay. + +[SOURCES.json](SOURCES.json) pins the predecessor statements, catalogue and +selected record as historical provenance. No predecessor implementation or +scientific receipt is imported. The relation-support reduction from PR4119 +and the two-target theorem from PR1882 remain cited proof dependencies. +Their scientific suites were not replayed as this contribution. + +The advance [CLAIM](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19146123) +follows live PR, Discussion, recent-account, main-tree and merged-term checks. +The cached entry scan reports 341 open PRs and 4,446 Discussion records with +complete remote text pagination, but only 162 of 6,996 local notes. Sparse +notes, arbitrary unsearched diffs and unpublished work limit novelty coverage. +Search absence is not a novelty certificate. + +This is a partial formal-register obstruction, not a native supplier or a +complete multiplication theorem. Physical legality, caller/frame/access costs, +dirty restoration in an actual implementation, stock, precision/tape, +compiler and outer admission remain unpriced. Independent human and formal +proof-kernel review are unclaimed. No Lean, Docker, predecessor scientific +suite or selected operator replay was run. + +## Open next questions + +- Can the remaining 24 coordinate-kernel pools realize the eight-call + endpoint? Start with the literal representative and retain both cube + relations and target coordinate projectors. The support union has size + one, so the new rank budget does not decide this branch. +- Can one changed register mechanism occur in a literal native caller with + a favorable complete bill? First specify independent targets, arbitrary + dirty inputs and every frame/access/restoration charge. No such caller + or physical invoice is supplied here. + +## Credit and implementation limits + +Credit woklerx/PR1846 for the exceptional scalar catalogue and orbit split; +unpaidmoon/PR4119 for the relation-support +reduction and open question; JoyboyBrian/PR5075 for the surviving-branch +handoff; waynenilsen/PR1882 for the dirty-auxiliary two-target theorem; and +Ali Romman/PR468 for the formal alphabet and low-span method. The retained +lineage includes eumemic/PR288 and huxint/PR203. Classical kernel and rank +arguments are not claimed as new techniques. The new obstruction and its +48-pool application were produced by Nick Petalas. Apache-2.0. + +The code has no recursion, solver, subprocess or network access. Its matrix +domain is fixed at four binary coordinates; formal words have at most three +letters and eight monomials. Coordinate budgets stop at nine calls, and the +largest allocation loop has at most 7^4 candidates. Functions stay below +60 lines. Power of Ten rule 3 has a managed-runtime deviation: Python exact +integers, dictionaries and standard iterators allocate dynamically within +these fixed domains. No fixed-pool memory implementation is claimed. +Warning-strict normal and optimized replay supplies interpreter diagnostics; +no unavailable external static analyzer or proof kernel is claimed. diff --git a/research/flagless-kernel-obstruction/SOURCES.json b/research/flagless-kernel-obstruction/SOURCES.json new file mode 100644 index 0000000000..ce322b188e --- /dev/null +++ b/research/flagless-kernel-obstruction/SOURCES.json @@ -0,0 +1,80 @@ +{ + "schema_version": 1, + "base_commit": "ec2780e8aeb1c88acaf5e9e470ef8c68e7fbbb6c", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395", + "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/auxiliary-span-six-cyclic-line/README.md", + "usage": "provenance", + "git_blob": "15cb91a38710642fd801b5cb42df705de1ae1790", + "sha256": "8be8cb05e213eaf50f29c75e8aa71894a6f836357765fb42a1070178e8543454" + }, + { + "path": "research/auxiliary-span-six-flag/README.md", + "usage": "provenance", + "git_blob": "fcb3305be469805d6f6a15eb2c8ca6676af16730", + "sha256": "babb6e44c8ac7640a0cde329b7f6582e72adc2c9307de0d4b5bd2b2510489e1d" + }, + { + "path": "research/bit-dirty-auxiliary-registers/README.md", + "usage": "provenance", + "git_blob": "273bb963ee40869145cf8309db4f8dddebcfe43d", + "sha256": "da984fddaa09bfa7b1a3e11505e737283cee36e7972b2081f9de28ec420607cd" + }, + { + "path": "research/bit-three-register-lower-bound/README.md", + "usage": "provenance", + "git_blob": "25e41c370c101a33a6deb978de08b03ed7539b79", + "sha256": "c12b33ef388deece0cbf891505a2ce2c0779a0c3a6cf1f0f7f7039bab59cbebd" + }, + { + "path": "research/bit-four-role-two-patterns/README.md", + "usage": "provenance", + "git_blob": "e79087d9cd8f4473e6e48fa4e521902b7809f3a4", + "sha256": "e4ee830e783b20bfb0886ae8c91133a6138157ed5dcaac90ce16ddc616c8d49f" + } + ], + "predecessor_references": [ + { + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/4119", + "head": "ea20dfd71c24072888755e2d03d61278bd25f2db", + "credit": "unpaidmoon", + "usage": "Exceptional-pool handoff, saturated cube relations and coordinate-call separation; cited premises, no scientific replay." + }, + { + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/5075", + "head": "c7b3403cf154ccb92286b911055db5d38dfd8bd6", + "credit": "JoyboyBrian", + "usage": "Explicit surviving flagless-branch handoff; cyclic-line theorem is separate." + }, + { + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1882", + "credit": "waynenilsen", + "usage": "Two-invertible-target six-call theorem with dirty auxiliaries; cited mathematical premise.", + "head": "a9c146e2919c82065e157b3e9bc050f38ac816db" + }, + { + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/468", + "head": "07a78bf335b0b5039a1fecd7cd74a0fe1d1605ea", + "credit": "Ali Romman", + "usage": "Formal abelian alphabet and low-span reasoning, with retained eumemic and huxint lineage." + }, + { + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1846", + "head": "ebd6bf651e1728a94d98c54208f74a529eddb43f", + "credit": "woklerx", + "usage": "Existing scalar catalogue and 24/48 orbit split. The new contribution excludes eight-call realization of the 48-pool orbit; it does not claim the classification." + } + ] +} diff --git a/research/flagless-kernel-obstruction/TASK.json b/research/flagless-kernel-obstruction/TASK.json new file mode 100644 index 0000000000..ae978f510c --- /dev/null +++ b/research/flagless-kernel-obstruction/TASK.json @@ -0,0 +1,88 @@ +{ + "schema_version": 1, + "task_id": "bit-new-register-model", + "priority_revision": 7, + "base_commit": "ec2780e8aeb1c88acaf5e9e470ef8c68e7fbbb6c", + "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_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read Model section 1 of the three-register bound and identify the exact excluded free operations.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "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": "refined", + "actual_scope": "Exclude the 48 noncoordinate-kernel flagless span-six pools for eight calls, three invertible rational 3-by-3 targets and one dirty auxiliary.", + "scope_change_reason": "The larger four-register model is an explicit allowed variation. This answers a surviving branch of unpaidmoon PR4119 and JoyboyBrian PR5075 with a new obstruction; no predecessor audit is the deliverable.", + "bottleneck_link": "This partial formal bit-register obstruction reduces the exceptional pool catalogue from 72 to 24. It supplies no native realization or paid supplier improvement.", + "budget_minutes": 60, + "stop_rule": "Ship the first proved partial obstruction; do not extend to the remaining coordinate-kernel pools or span five.", + "outcome": "completed", + "evidence": "PROOF.md gives the coordinate-kernel rank-budget proof using credited relation-support and two-target premises. verify.py checks exact coordinate orbits, kernel supports, literal matrix arithmetic, formal fixed-vector identities and every bounded coordinate-call allocation. The scalar 24/48 orbit classification belongs to woklerx PR1846; only its eight-call obstruction is new.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can the remaining 24 coordinate-kernel flagless pools realize the eight-call endpoint?", + "why_it_matters": "They are precisely the portion of the exceptional flagless catalogue not covered by this obstruction.", + "first_step": "Keep the literal pool (0x0003,0x0022,0x0550) and target projectors in the original basis, then retain its two cube relations through a source-bound three-role reduction.", + "blocked_by": "The common kernels have support on only one coordinate, so the new rank budget does not force a second zero contribution." + }, + { + "question": "Can a literal native caller implement a changed register mechanism with a favorable full bill?", + "why_it_matters": "Formal paid-call exclusions alone do not determine the selected supplier or exponent.", + "first_step": "Specify the actual caller, independent targets, dirty-state interface and every physical frame/access/restoration charge.", + "blocked_by": "No source-compatible native construction or complete invoice is supplied." + } + ], + "coordination": { + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19146123", + "upstream_checked_at": "2026-10-23T12:58:05Z", + "upstream_commit": "ec2780e8aeb1c88acaf5e9e470ef8c68e7fbbb6c", + "open_pr_coverage": 341, + "discussion_record_coverage": 4446, + "coverage_limit": "Remote text pagination complete as reported by the helper; sparse local scan searched 162 of 6996 notes. Separate main Git searches and live PR bodies supplemented it. Unpublished work and arbitrary diffs are not exhaustively covered." + }, + "local_validation": { + "environment": { + "python": "CPython 3.12.15", + "platform": "macOS 27.0.1 arm64" + }, + "direct_normal_seconds": 0.3434, + "direct_optimized_seconds": 0.3443, + "timing_scope": "Local verification durations, not performance-improvement measurements.", + "checks": "Both registered modes, direct warning-strict modes, metadata/provenance and AST function bounds passed. Source-history and committed export checks follow publication commit." + } +} diff --git a/research/flagless-kernel-obstruction/VERIFY.json b/research/flagless-kernel-obstruction/VERIFY.json new file mode 100644 index 0000000000..e301278073 --- /dev/null +++ b/research/flagless-kernel-obstruction/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": "New coordinate-kernel obstruction: exact pool orbits, literal arithmetic, formal kernel identities, diagonal criteria, rank budgets and named boundary controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "The same explicit acceptance checks with assertions disabled." + } + ] +} diff --git a/research/flagless-kernel-obstruction/verify.py b/research/flagless-kernel-obstruction/verify.py new file mode 100644 index 0000000000..bf433c79b0 --- /dev/null +++ b/research/flagless-kernel-obstruction/verify.py @@ -0,0 +1,264 @@ +#!/usr/bin/env python3 +"""Exact finite corroboration of the coordinate-kernel obstruction.""" + +import hashlib +import itertools +import json +from collections import Counter, defaultdict +from pathlib import Path + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def outer(x, y): + return sum(((x >> i & 1) * (y >> j & 1)) << (4 * i + j) + for i in range(4) for j in range(4)) + + +def action(matrix, vector): + return sum(((matrix >> (4 * i) & 15 & vector).bit_count() % 2) << i + for i in range(4)) + + +def transpose(matrix): + return sum((matrix >> (4 * j + i) & 1) << (4 * i + j) + for i in range(4) for j in range(4)) + + +def multiply(first, second): + return sum((action(first, action(second, 1 << j)) >> i & 1) + << (4 * i + j) for i in range(4) for j in range(4)) + + +def literal_multiply(first, second): + result = 0 + for i, j in itertools.product(range(4), repeat=2): + entry = sum((first >> (4 * i + k) & 1) * (second >> (4 * k + j) & 1) + for k in range(4)) % 2 + result |= entry << (4 * i + j) + return result + + +def off_diagonal(matrix): + return matrix & ~0x8421 + + +def kernel(matrices): + return tuple(v for v in range(1, 16) + if all(action(matrix, v) == 0 for matrix in matrices)) + + +def lacks_line_plane(matrices): + for line in range(1, 16): + if not all(action(matrix, line) in (0, line) for matrix in matrices): + continue + for vector in range(1, 16): + if vector == line: + continue + plane = (0, line, vector, line ^ vector) + if all(action(matrix, v) in plane + for matrix in matrices for v in plane): + return False + return True + + +def exceptional_pools(): + """Enumerate only the predecessor's partial-plane triple shape.""" + fibers = defaultdict(list) + for x, y in itertools.product(range(1, 16), repeat=2): + if (x & y).bit_count() % 2: + matrix = outer(x, y) + fibers[off_diagonal(matrix)].append(matrix) + pools = [] + for first in sorted(fibers): + if first == 0 or len(fibers[first]) != 2: + continue + for second in sorted(fibers): + if second == 0 or len(fibers[second]) != 1: + continue + if first ^ second in fibers: + continue + matrices = tuple(sorted(fibers[first] + fibers[second])) + if lacks_line_plane(matrices): + pools.append(matrices) + require(len(pools) == len(set(pools)), "duplicate exceptional pool") + return tuple(sorted(pools)) + + +def permute(matrix, permutation): + return sum((matrix >> (4 * i + j) & 1) + << (4 * permutation[i] + permutation[j]) + for i in range(4) for j in range(4)) + + +def coordinate_orbit(matrices): + return {tuple(sorted(permute(matrix, p) for matrix in matrices)) + for p in itertools.permutations(range(4))} + + +def classify(pools): + right = coordinate_orbit((0x0003, 0x0022, 0x0DD0)) + left = {tuple(sorted(transpose(matrix) for matrix in pool)) + for pool in right} + coordinate = coordinate_orbit((0x0003, 0x0022, 0x0550)) + require(len(right) == len(left) == len(coordinate) == 24, "orbit size") + require(not (right & left or right & coordinate or left & coordinate), + "coordinate orbits overlap") + require(set(pools) == right | left | coordinate, "unclassified pool") + histogram = Counter() + for pool in pools: + r = kernel(pool) + l = kernel(tuple(transpose(matrix) for matrix in pool)) + require(len(r) == len(l) == 1, "kernel dimension is not one") + require((r[0] & l[0]).bit_count() % 2 == 1, "kernel/image split") + histogram[r[0].bit_count(), l[0].bit_count(), + (r[0] | l[0]).bit_count()] += 1 + require(histogram == {(1, 1, 1): 24, (2, 1, 2): 24, (1, 2, 2): 24}, + "left/right support histogram") + return tuple(sorted(right | left)), coordinate, histogram + + +def formal_word(word): + """Multiply in the full group algebra on independent integer exponents.""" + result = {(0,) * len(word): 0x8421} + for index, projector in enumerate(word): + following = {} + for exponent, coefficient in result.items(): + other = list(exponent) + other[index] += 1 + shifted = tuple(other) + first = multiply(coefficient, 0x8421 ^ projector) + second = multiply(coefficient, projector) + following[exponent] = following.get(exponent, 0) ^ first + following[shifted] = following.get(shifted, 0) ^ second + result = {exponent: value for exponent, value in following.items() if value} + return result + + +def formal_kernel_checks(pools): + words = coefficients = 0 + for pool in pools: + right = kernel(pool)[0] + left = kernel(tuple(transpose(matrix) for matrix in pool))[0] + for length in range(4): + for word in itertools.product(pool, repeat=length): + for exponent, coefficient in formal_word(word).items(): + origin = not any(exponent) + require(action(coefficient, right) == (right if origin else 0), + "formal right-kernel identity") + require(action(transpose(coefficient), left) + == (left if origin else 0), "formal left-kernel identity") + coefficients += 1 + words += 1 + return words, coefficients + + +def diagonal_checks(pools): + checks = 0 + for pool in pools: + r = kernel(pool)[0] + l = kernel(tuple(transpose(matrix) for matrix in pool))[0] + for labels in itertools.product((-1, 0, 1), repeat=4): + for vector in (r, l): + predicted = all(labels[i] == 0 for i in range(4) if vector >> i & 1) + actual = {(i, labels[i]): 1 for i in range(4) if vector >> i & 1} + expected = {(i, 0): 1 for i in range(4) if vector >> i & 1} + require(predicted == (actual == expected), "fixed-diagonal criterion") + checks += 1 + return checks + + +def allocations(total): + require(0 <= total <= 9, "allocation domain") + return tuple(v for v in itertools.product(range(total + 1), repeat=4) + if sum(v) == total) + + +def surviving_budgets(pools, total): + survivors = [] + for pool in pools: + forced = kernel(pool)[0] | kernel(tuple(transpose(m) for m in pool))[0] + for auxiliary in range(4): + active = tuple(i for i in range(4) if i != auxiliary) + for size in range(3, total + 1): + for counts in allocations(total - size): + capacity = [counts[i] + (0 if forced >> i & 1 else size - 2) + for i in active] + if min(capacity) >= 3: + survivors.append((size, counts, active, forced)) + return survivors + + +def budget_checks(pools): + survivors = surviving_budgets(pools, 8) + require(len(survivors) == 96, "critical allocation count") + for size, counts, active, forced in survivors: + require(size == 5 and sum(counts) == 3, "noncritical allocation survived") + zeros = tuple(i for i in active if forced >> i & 1) + require(len(zeros) == 1 and counts[zeros[0]] == 3, "forced role bill") + require(all(counts[i] == 0 for i in active if i not in zeros), + "remaining targets have coordinate contributions") + # The cited two-invertible-target theorem requires six S calls. + require(size < 6, "two-target theorem no longer excludes the budget") + require(bool(surviving_budgets(pools[:1], 9)), "nine-call budget control") + return len(survivors) + + +def controls(pools, coordinate): + seed = (0x0003, 0x0022, 0x0DD0) + require(seed in pools, "literal initial fixture missing") + require(kernel(seed) == (12,), "initial right kernel changed") + require(kernel(tuple(transpose(m) for m in seed)) == (8,), "initial left kernel") + require(all((kernel(p)[0] | kernel(tuple(transpose(m) for m in p))[0]).bit_count() == 1 + for p in coordinate), "coordinate control was excluded") + for pool in pools: + require(all(multiply(m, m) == m for m in pool), "idempotence") + require(action(outer(4, 4), 12) != 0, "coordinate interleaving countercontrol") + require(allocations(0) == ((0, 0, 0, 0),), "zero allocation") + for invalid in (-1, 10): + try: + allocations(invalid) + except ValueError: + continue + raise ValueError("invalid allocation accepted") + return ("literal_fixture", "right_kernel", "left_kernel", "coordinate_exclusion_boundary", + "idempotence", "coordinate_interleaving", "zero_allocation", + "negative_allocation_rejected", "oversized_allocation_rejected") + + +def arithmetic_checks(pools): + matrices = sorted({m for pool in pools for m in pool} | {0, 0x8421}) + checks = 0 + for first, second in itertools.product(matrices, repeat=2): + require(multiply(first, second) == literal_multiply(first, second), + "literal binary matrix product disagrees") + checks += 1 + return checks + + +def main(): + excluded, coordinate, histogram = classify(exceptional_pools()) + arithmetic = arithmetic_checks(excluded) + words, coefficients = formal_kernel_checks(excluded) + diagonals = diagonal_checks(excluded) + critical = budget_checks(excluded) + control_names = controls(excluded, coordinate) + root = Path(__file__).resolve().parent + names = ("README.md", "PROOF.md", "verify.py", "TASK.json", "SOURCES.json", "VERIFY.json") + hashes = {name: hashlib.sha256((root / name).read_bytes()).hexdigest() for name in names} + receipt = {"status": "PASS_FLAGLESS_KERNEL_OBSTRUCTION", "excluded_pools": len(excluded), + "remaining_coordinate_pools": len(coordinate), "formal_words": words, + "formal_coefficient_matrices": coefficients, "diagonal_label_checks": diagonals, + "critical_rank_budgets": critical, "controls": list(control_names), + "literal_matrix_products": arithmetic, + "kernel_histogram": {str(k): v for k, v in sorted(histogram.items())}, + "pool_sha256": hashlib.sha256(json.dumps(excluded).encode()).hexdigest(), + "source_sha256": hashes} + print(json.dumps(receipt, indent=2, sort_keys=True)) + + +if __name__ == "__main__": + main()