From 5275d72e56afe7d22252f2a8bd7690e9a9344ded Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Tue, 27 Oct 2026 10:45:34 +0000 Subject: [PATCH] feat(research): prove affine floor with clean erasure --- research/clean-affine-erasure-floor/PROOF.md | 124 +++++++ research/clean-affine-erasure-floor/README.md | 55 +++ .../clean-affine-erasure-floor/SOURCES.json | 30 ++ research/clean-affine-erasure-floor/TASK.json | 110 ++++++ .../clean-affine-erasure-floor/VERIFY.json | 37 ++ research/clean-affine-erasure-floor/verify.py | 318 ++++++++++++++++++ 6 files changed, 674 insertions(+) create mode 100644 research/clean-affine-erasure-floor/PROOF.md create mode 100644 research/clean-affine-erasure-floor/README.md create mode 100644 research/clean-affine-erasure-floor/SOURCES.json create mode 100644 research/clean-affine-erasure-floor/TASK.json create mode 100644 research/clean-affine-erasure-floor/VERIFY.json create mode 100644 research/clean-affine-erasure-floor/verify.py diff --git a/research/clean-affine-erasure-floor/PROOF.md b/research/clean-affine-erasure-floor/PROOF.md new file mode 100644 index 0000000000..61ef1e3d1e --- /dev/null +++ b/research/clean-affine-erasure-floor/PROOF.md @@ -0,0 +1,124 @@ +# Clean workspace and erasure preserve the affine rank floor + +This is a scoped written proof, with finite corroboration in `verify.py`. +It is not a complete multiplication theorem or a proof-kernel certificate. + +## The changed boundary + +Fix `d >= 1`, `G = AGL_d(F2)` and the formal group algebra `R = F2[G]`. +Write `H(g) = [[A,b],[0,1]]` for `g(x)=Ax+b`, and +`r(g)=rank_F2([A-I | b])`. All compositions act rightmost first. + +There are `W >= 1` arbitrary input data registers. A finite circuit may +change its number of live registers. Every free instruction is an arbitrary +rectangular binary scalar matrix, acting identically on the address space. +This includes scalar mixing, singular maps, copying, zero allocation, reset +and discarding. Ancillas created in this way enter at zero. Arbitrarily many +initial dirty registers may also be present, provided the designated outputs +have the specified action for all their initial values. + +A paid instruction at any current width is exactly #1333's instruction + +`D_N(g)=I+([g]+1)N`, with `N=uv^T`, `v^T u=1`, `r(g)=1`. + +Each occurrence costs one. The `W` designated output registers must equal +`[g_j]` times input register `j`, with no other data or dirty-input dependence. +Other outputs may contain arbitrary garbage and may be discarded. This is +an identity of the retained output rows over the full formal algebra. +Initial clean allocation and final output selection are free rectangular maps. +No nonlinear, input-dependent, address-dependent or postselected free operation +is included. The schedule is a fixed finite linear circuit. + +**Theorem.** Even with this enlarged free-operation class, the exact minimum +paid-call count is `sum_j r(g_j)` for every finite tuple of affine targets. + +The predecessor, Gareth Davidson's #1333, proves this value when all free +maps are invertible and every auxiliary input is arbitrary and restored. +Its direct attaining factorization is used below as a cited premise. +The new assertion is the lower bound under the changed clean/erasing boundary. + +## A rectangular defect invariant + +Let `epsilon:R -> F2` be augmentation, sending every `[g]` to `1`. +Extend `H` linearly to `R`, and entrywise to rectangular matrices. +For `M` of size `a` by `b`, put + +`M_hat = H(M)`, `M_bar = epsilon(M) tensor I_(d+1)`, + +`delta(M) = rank_F2(M_hat - M_bar)`. + +These are ordinary rectangular binary matrices of size `a(d+1)` by +`b(d+1)`. Both hat and bar preserve every compatible product. +For an `a` by `b` matrix `U` and a `b` by `c` matrix `V`, + +``` +(UV)_hat - (UV)_bar + = (U_hat-U_bar) V_hat + U_bar (V_hat-V_bar). +delta(UV) <= delta(U) + delta(V). +``` + +This uses rank subadditivity and the fact that multiplication on either +side cannot increase rank. It needs neither inverses nor square matrices. +In particular, any scalar rectangular map `S` has `S_hat=S_bar` and +`delta(S)=0`, even if it is singular. For a paid instruction, + +``` +epsilon(D_N(g)) = I, +D_hat - D_bar = N tensor (H(g)-I), +delta(D_N(g)) = rank(N) rank(H(g)-I) = 1. +``` + +The tensor-rank equality here is ordinary matrix rank over a field. +Induction through the actual sequence of compatible dimensions therefore +gives `delta(F) <= q` for every circuit operator `F` using `q` paid calls. + +## Reading only the required outputs is enough + +First omit initial dirty registers. Include clean allocation and final +selection in the circuit. The complete retained operator on the `W` data +inputs is then the formal square matrix `T=diag([g_1],...,[g_W])`. +It has augmentation `I`, so + +``` +delta(T) = rank(diag(H(g_1)-I,...,H(g_W)-I)) + = sum_j r(g_j). +``` + +Consequently `q >= sum_j r(g_j)`. Garbage is irrelevant because output +selection was already included as a free rectangular instruction. Clean +helpers need not be restored, and no assertion about their endpoint columns +was used. + +If initial dirty registers are supplied, restrict their initial values to +zero by a scalar input embedding. A circuit correct for every dirty input +is correct under this restriction, with the same paid count. The preceding +argument applies. This is a lower-bound restriction, not a permission to +erase unknown data in a physical construction. + +For the matching upper bound, use #1333, PROOF.md Section 4: each affine +`g_j` is a product of exactly `r(g_j)` displacement-one affine labels. +Apply that factorization on its coordinate projector. It is a formal +group-algebra identity, uses no auxiliary register and belongs to the +enlarged model. Thus the enlarged model has the same exact optimum. +The predecessor's factorization and original tariff are not new claims here. + +## Scope of the inference + +The defect inequality itself also holds for other group representations +and for a sum of paid defect ranks. This proof uses it only for the stated +binary-affine model and does not identify its rank with a recursive child +tariff or a physical cost. In particular, a free address map has nonzero +defect in general and cannot be added to the free scalar class silently. + +The homogeneous representation is not faithful on `F2[G]`. Formal equality +implies the represented boundary used for the lower bound. Represented +equality alone cannot accept an attaining circuit. The upper theorem is +cited in the full formal algebra; every new clean/erasing finite fixture is +checked there and by a separate faithful regular-action interpretation. + +Credit Gareth Davidson #1333 for the model, homogeneous displacement method +and direct affine factorization, and its eumemic #288, Ali Romman #468, +David Govea #720 and classical rank-method lineage. Rank subadditivity is +classical. No general literature-priority claim is made. This extension was +produced by Nick Petalas. Independent human and formal proof-kernel review +are unclaimed. Apache-2.0. diff --git a/research/clean-affine-erasure-floor/README.md b/research/clean-affine-erasure-floor/README.md new file mode 100644 index 0000000000..8e5e2ba550 --- /dev/null +++ b/research/clean-affine-erasure-floor/README.md @@ -0,0 +1,55 @@ +# Clean copying and erasure cannot beat the binary-affine tariff + +This scoped algebraic proof extends Gareth Davidson's [#1333](https://github.com/CrocSwap/integer-mult-bounds/pull/1333). Its exact binary-affine paid-call floor survives arbitrary clean helpers, free scalar copying and reset, discarded garbage, and a changing number of live registers: + +``` +minimum paid calls = sum_j rank_F2([A_j-I | b_j]). +``` + +The paid alphabet is unchanged. Each call is `I+([g]+1)uv^T` over the full formal algebra `F2[AGL_d(F2)]`, with `v^T u=1` and `rank([A_g-I | b_g])=1`. Every free operation is an arbitrary rectangular binary scalar map. The retained outputs must implement the independent target maps `g_j(x)=A_j x+b_j` on arbitrary inputs. Helpers need not return to zero, garbage may be discarded, and any supplied dirty inputs must not affect the retained answer. The schedule is finite and fixed. + +The new [proof](PROOF.md) avoids inverse normalization. For a rectangular formal matrix `M`, define + +``` +delta(M) = rank(H(M) - epsilon(M) tensor I), +delta(UV) <= delta(U) + delta(V). +``` + +Here `H` is the homogeneous affine representation and `epsilon` is augmentation. Every free rectangular scalar map has defect zero; every paid call has defect one. The selected output rows have defect equal to the displayed target bill. This proves the enlarged-model lower bound. The matching upper construction is cited directly from #1333, PROOF.md Section 4; no predecessor census or verifier is replayed. + +This closes a clean/erasing-workspace loophole for this specified alphabet. It is a side result under `bit-new-register-model`, with changed free-operation and output hypotheses. It supplies no physical supplier, recursive moment, new kappa or complete multiplication theorem. The selected frontier is unchanged. + +## Reproduction and evidence + +From the repository root: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/clean-affine-erasure-floor/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/clean-affine-erasure-floor/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/clean-affine-erasure-floor +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/clean-affine-erasure-floor --check-source-history +``` + +Substitute another CPython 3.12 executable elsewhere. The standard library suffices. Verification writes only a generated JSON receipt to stdout, bound to the six package source hashes. The direct marker is `PASS_CLEAN_AFFINE_ERASURE_FLOOR`; the runner and publication preflight print `PASS_REGISTERED_RESEARCH_PACKAGE` and `PASS_RESEARCH_COMMIT_BYTES`. + +The finite corroboration checks 74,384 compatible rectangular products, 682 free scalar maps, 315 paid factors, 48 clean/erasing circuits, 2,304 faithful basis columns, 192 omitted-call controls and eight boundary controls. It exhausts every compatible pair of rectangular matrices with one or two rows/columns over `F2[C2]`. It separately checks all binary scalar maps of shapes one through three and every allowed paid factor through three roles in the dimension-two affine group. New clean copy/compute/reset/discard circuits use two arbitrary data inputs, two zero helpers, four paid calls and two retained outputs. Full formal multiplication and a separate set-based faithful regular-action interpreter check their endpoints, including every group/data basis column. Single-call omissions, dirty-helper leakage, illegal free addresses, rank undercharging, a nonfaithful representation kernel and invalid domains are controls. The proof covers unbounded finite parameters; this finite domain does not enumerate arbitrary circuit words. + +The card's first working command, `scripts/research_selected_baseline.py`, passed with `PASS_RESEARCH_BASELINE_BINDINGS_ONLY`. This was orientation only. No selected scientific replay, native/tape execution, Lean or Docker check was run. Hosted CI is separate from local evidence. + +## Implementation scope + +The checker has no external executable, dynamic imports, recursion or filesystem mutations. Its finite group bound is 24, scalar width is at most four, represented matrices have at most twelve rows/columns, and all enumeration products have fixed limits visible in the code. All mathematical acceptance checks remain enabled under `-O`. + +Power of Ten rule 3 deviation: CPython and its standard library allocate managed objects during verification. This six-file standalone checker bounds live mathematical data by the complete 292-entry small-matrix inventory and the fixed four-role/24-element domains; it streams composition checks and faithful basis inputs. Runtime/library allocation is not statically controlled. Follow-up is required if these limits are enlarged. Other checks include a separately enumerated row-span rank oracle, explicit domain rejection, functions below sixty lines and warning-strict normal/optimized execution. No standalone linter is installed in this environment; AST inspection and both interpreter modes are the available diagnostics. No repository-wide diagnostic configuration is changed. + +## Sources and overlap + +[SOURCES.json](SOURCES.json) pins the unchanged predecessor README and proof at canonical main `de5ec2e7a6074068452f45b1a191b5c72832df4a`. They are cited inputs, not scientific replay targets. [TASK.json](TASK.json) records the changed hypothesis, exact claim and bounded overlap coverage. Live PRs, recent handoffs, local question reservations, merged-PR searches and all-main README terms were checked before claiming and before publication. These searches do not exclude unpublished work or establish literature priority. + +Credit Gareth Davidson #1333 for the binary-affine model, homogeneous displacement method, exact original tariff and direct attaining factorization. Its eumemic #288, Ali Romman #468, David Govea #720 and classical rank/reflection lineage retain credit. The new contribution is the rectangular augmentation-defect lower bound and its clean/erasing boundary application. This contribution was produced by Nick Petalas. Independent human and formal proof-kernel review are unclaimed. Apache-2.0. + +## Open next questions + +Can a physically justified free operation escape this defect bound while its complete cost remains favorable? Start with one actual native address-dependent operation and compute its represented defect and complete input/output invoice. The current theorem excludes only scalar free maps; physical legality, movement, ownership, precision and recursive charges remain blockers. Adding a nonzero-defect address operation at zero price changes the model rather than supplying an improvement. + +Can the same rectangular invariant give a sharp tariff for another specified group representation with clean/erasing workspace? Start with a cited direct construction whose representation-rank bill is attained, then state the retained output contract. A matching upper construction is necessary; a generic lower bound alone is not an exact tariff. diff --git a/research/clean-affine-erasure-floor/SOURCES.json b/research/clean-affine-erasure-floor/SOURCES.json new file mode 100644 index 0000000000..c6e2a70512 --- /dev/null +++ b/research/clean-affine-erasure-floor/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a", + "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/binary-affine-register-bound/PROOF.md", + "usage": "input", + "git_blob": "b1152a39b559f7a058489ec74231488e4f8edd83", + "sha256": "36a33434222798434b0a17476ae5f9bc8a2a3891871c46e77cc50ce2e132206b" + }, + { + "path": "research/binary-affine-register-bound/README.md", + "usage": "input", + "git_blob": "7b68583becf8be6f3cf666b05b0943e7eb99270c", + "sha256": "7951868efdf35fdb2aacdd302ca825cbde0586a5fae6df23aee78e29f30c332a" + } + ] +} diff --git a/research/clean-affine-erasure-floor/TASK.json b/research/clean-affine-erasure-floor/TASK.json new file mode 100644 index 0000000000..59d525f59f --- /dev/null +++ b/research/clean-affine-erasure-floor/TASK.json @@ -0,0 +1,110 @@ +{ + "schema_version": 1, + "task_id": "bit-new-register-model", + "priority_revision": 8, + "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a", + "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 binary-affine paid-call floor with arbitrary rectangular scalar maps, clean workspace, reset, copying and discarded garbage.", + "scope_change_reason": "Replace invertible scalar changes and restored dirty boundaries in Gareth Davidson #1333 by a finite variable-width linear circuit and retained-output contract. This is a scoped side obstruction, not a native supplier search.", + "bottleneck_link": "Clean storage and scalar erasure do not escape this rank-priced binary-affine mechanism; a favorable new mechanism must change the paid/address contract.", + "budget_minutes": 60, + "stop_rule": "Stop at the first proved clean/erasing extension; do not expand a supplier search.", + "outcome": "completed", + "evidence": "PROOF.md and generated source-bound stdout receipt from verify.py; finite checks corroborate the written theorem.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can a physically justified free operation escape the defect bound at favorable complete cost?", + "why_it_matters": "Scalar clean/reset resources alone do not lower this alphabet bill.", + "first_step": "Compute the represented defect and full invoice of one actual address-dependent native operation.", + "blocked_by": "No such physical caller and complete invoice is supplied." + }, + { + "question": "Is this clean/erasing lower bound sharp for another specified group representation?", + "why_it_matters": "The invariant applies to compatible rectangular products beyond the affine group.", + "first_step": "Choose one cited direct construction attaining its representation-rank bill and specify retained outputs.", + "blocked_by": "An attaining full formal construction is needed for an exact tariff." + } + ], + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19214962", + "predecessor": { + "pr": 1333, + "author": "Gareth Davidson", + "source": "research/binary-affine-register-bound/PROOF.md", + "consumed": "Section 4 direct affine factorization; original model and rank method. No predecessor executable imported or replayed." + }, + "ownership": { + "initial_branch": "detached HEAD", + "initial_head": "de5ec2e7a6074068452f45b1a191b5c72832df4a", + "preserved": true + }, + "playbook": "Investigation; local research packaging explicitly authorized by the assignment.", + "claim_type": "Scoped written proof with exact finite corroboration", + "validation": { + "interpreter": "CPython 3.12.15", + "local_commands": "VERIFY.json commands and direct verifier; package metadata and committed-byte/source-history preflight.", + "unrun": "Independent human/formal proof-kernel review; selected cold replay; native physical supplier." + }, + "overlap": { + "upstream_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a", + "priority_revision": 8, + "checked_at_utc": "2026-10-27T10:44:00Z", + "cached_search": { + "task": "bit-new-register-model", + "open_prs": 426, + "discussions": 5331, + "remote_pagination_complete": true, + "local_notes_searched": 215, + "head_note_paths": 7845, + "local_coverage_complete": false + }, + "additional_checks": [ + "Canonical-main README searches for clean affine boundaries, rectangular augmentation, scalar reset and erasure", + "Merged PR searches for clean affine, affine ancilla, rectangular augmentation and affine erasure", + "Live open PR searches for affine and 1333; no same binary-affine clean/erasing target found", + "Recent handoff claims and all local reservation source files" + ], + "limitations": "No novelty guarantee; sparse working-tree note search is incomplete, and unpublished work is not covered. Main-tree distinctive searches supplement it." + } +} diff --git a/research/clean-affine-erasure-floor/VERIFY.json b/research/clean-affine-erasure-floor/VERIFY.json new file mode 100644 index 0000000000..7cd6e87f1b --- /dev/null +++ b/research/clean-affine-erasure-floor/VERIFY.json @@ -0,0 +1,37 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/binary-affine-register-bound/PROOF.md", + "research/binary-affine-register-bound/README.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Complete small rectangular products; free/paid ranks; new clean erasing formal and faithful endpoints; failure controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Identical mathematical checks with assertions disabled." + } + ] +} diff --git a/research/clean-affine-erasure-floor/verify.py b/research/clean-affine-erasure-floor/verify.py new file mode 100644 index 0000000000..ff058db57c --- /dev/null +++ b/research/clean-affine-erasure-floor/verify.py @@ -0,0 +1,318 @@ +#!/usr/bin/env python3 +"""Exact finite corroboration of the rectangular augmentation-rank proof.""" + +import hashlib +import itertools +import json +from pathlib import Path + + +MAX_ROLES = 4 + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def rank(rows, columns): + need(0 <= columns <= 12, "represented column bound") + need(len(rows) <= 12, "represented row bound") + need(all(0 <= row < 1 << columns for row in rows), "binary row") + work = list(rows) + pivot = 0 + for column in range(columns): + found = next((i for i in range(pivot, len(work)) if work[i] >> column & 1), None) + if found is None: + continue + work[pivot], work[found] = work[found], work[pivot] + for i in range(pivot + 1, len(work)): + if work[i] >> column & 1: + work[i] ^= work[pivot] + pivot += 1 + return pivot + + +def apply_linear(rows, value): + return sum(((row & value).bit_count() & 1) << i for i, row in enumerate(rows)) + + +def xor_rows(rows, mask): + result = 0 + for i, row in enumerate(rows): + if mask >> i & 1: + result ^= row + return result + + +def make_group(dimension): + need(dimension in (1, 2), "finite address dimension") + size = 1 << dimension + identity = tuple(1 << i for i in range(dimension)) + elements = [(identity, 0)] + for rows in itertools.product(range(size), repeat=dimension): + if rank(rows, dimension) == dimension: + elements.extend((rows, b) for b in range(size) if (rows, b) != (identity, 0)) + need(len(elements) <= 24, "finite group bound") + index = {g: i for i, g in enumerate(elements)} + table = [] + actions = [tuple(apply_linear(a, x) ^ b for x in range(size)) for a, b in elements] + action_index = {p: i for i, p in enumerate(actions)} + for i, (a, b) in enumerate(elements): + row = [] + for j, (c, e) in enumerate(elements): + linear = tuple(xor_rows(c, a[k]) for k in range(dimension)) + product = index[(linear, apply_linear(a, e) ^ b)] + literal = action_index[tuple(actions[i][actions[j][x]] for x in range(size))] + need(product == literal, "independent point-composition law") + row.append(product) + table.append(tuple(row)) + homogeneous = [tuple(a[i] | ((b >> i & 1) << dimension) for i in range(dimension)) + + (1 << dimension,) for a, b in elements] + return tuple(table), tuple(homogeneous) + + +def ring_product(a, b, table): + result = 0 + for i in range(len(table)): + if a >> i & 1: + for j in range(len(table)): + if b >> j & 1: + result ^= 1 << table[i][j] + return result + + +def shape(matrix): + need(isinstance(matrix, tuple) and 1 <= len(matrix) <= MAX_ROLES, "matrix rows") + width = len(matrix[0]) + need(1 <= width <= MAX_ROLES and all(len(row) == width for row in matrix), "matrix columns") + return len(matrix), width + + +def multiply(left, right, table): + height, inner = shape(left) + other_inner, width = shape(right) + need(inner == other_inner, "composition dimensions") + result = [] + for i in range(height): + row = [] + for j in range(width): + value = 0 + for k in range(inner): + value ^= ring_product(left[i][k], right[k][j], table) + row.append(value) + result.append(tuple(row)) + return tuple(result) + + +def scalar(rows, width): + need(1 <= width <= MAX_ROLES, "scalar width") + need(all(0 <= row < 1 << width for row in rows), "scalar entries") + result = tuple(tuple(row >> j & 1 for j in range(width)) for row in rows) + shape(result) + return result + + +def image(matrix, homogeneous, augmentation=False): + height, width = shape(matrix) + block = len(homogeneous[0]) + result = [0] * (height * block) + for i, row in enumerate(matrix): + for j, value in enumerate(row): + need(0 <= value < 1 << len(homogeneous), "formal coefficient bound") + for g in range(len(homogeneous)): + if value >> g & 1: + for a in range(block): + bits = 1 << a if augmentation else homogeneous[g][a] + result[i * block + a] ^= bits << (j * block) + return tuple(result) + + +def defect(matrix, homogeneous): + actual = image(matrix, homogeneous) + baseline = image(matrix, homogeneous, augmentation=True) + rows = tuple(a ^ b for a, b in zip(actual, baseline, strict=True)) + return rank(rows, len(matrix[0]) * len(homogeneous[0])) + + +def identity(roles): + return scalar(tuple(1 << i for i in range(roles)), roles) + + +def paid(roles, label, u, v): + need(1 <= roles <= MAX_ROLES, "paid roles") + need(0 < u < 1 << roles and 0 < v < 1 << roles, "paid vectors") + need((u & v).bit_count() & 1, "paid idempotence") + need(0 < label < 24, "paid label index") + return tuple(tuple((int(i == j) ^ ((1 ^ (1 << label)) + if (u >> i & 1) and (v >> j & 1) else 0)) + for j in range(roles)) for i in range(roles)) + + +def exhaustive_rectangles(table, homogeneous): + inventories = {} + for height, width in itertools.product((1, 2), repeat=2): + inventories[height, width] = tuple( + tuple(tuple(values[i * width:(i + 1) * width]) for i in range(height)) + for values in itertools.product(range(4), repeat=height * width)) + count = 0 + transcript = hashlib.sha256() + cached = {m: defect(m, homogeneous) for matrices in inventories.values() for m in matrices} + for matrix, value in cached.items(): + rows = tuple(a ^ b for a, b in zip(image(matrix, homogeneous), + image(matrix, homogeneous, augmentation=True), strict=True)) + span = {0} + for row in rows: + span |= {x ^ row for x in tuple(span)} + need(len(span) == 1 << value, "independent row-span rank oracle") + for height, inner, width in itertools.product((1, 2), repeat=3): + for a in inventories[height, inner]: + for b in inventories[inner, width]: + product = multiply(a, b, table) + value = cached[product] + need(value <= cached[a] + cached[b], "rectangular defect inequality") + transcript.update(bytes((height, inner, width, value))) + count += 1 + return count, transcript.hexdigest() + + +def free_and_paid(homogeneous): + free_count = 0 + paid_count = 0 + labels = [g for g in range(1, len(homogeneous)) + if defect(((1 << g,),), homogeneous) == 1] + for height, width in itertools.product(range(1, 4), repeat=2): + for bits in range(1 << (height * width)): + matrix = scalar(tuple(bits >> (i * width) & ((1 << width) - 1) + for i in range(height)), width) + need(defect(matrix, homogeneous) == 0, "free rectangular map") + free_count += 1 + for roles in range(1, 4): + for u, v in itertools.product(range(1, 1 << roles), repeat=2): + if (u & v).bit_count() & 1: + for g in labels: + need(defect(paid(roles, g, u, v), homogeneous) == 1, "paid rank") + paid_count += 1 + return free_count, paid_count, labels + + +def regular_apply(matrix, vector, table): + """Separate faithful action using sets, rather than packed convolution.""" + height, width = shape(matrix) + need(len(vector) == width, "regular input width") + output = [] + for i in range(height): + entries = set() + for j in range(width): + support = [g for g in range(len(table)) if matrix[i][j] >> g & 1] + for g in support: + for h in vector[j]: + value = table[g][h] + entries.symmetric_difference_update((value,)) + output.append(frozenset(entries)) + return tuple(output) + + +def replay(events, table): + operator = identity(len(events[0][0])) + for event in events: + operator = multiply(event, operator, table) + return operator + + +def clean_events(first, second): + enter = scalar((1, 2, 0, 0), 2) + copy = scalar((1, 2, 5, 10), 4) + erase = scalar((0, 0, 4, 8), 4) + select = scalar((4, 8), 4) + calls = [paid(4, first[0], 4, 4), paid(4, first[1], 4, 4), + paid(4, second[0], 8, 8), paid(4, second[1], 8, 8)] + return [enter, copy, *calls, erase, select] + + +def clean_fixtures(table, homogeneous, labels): + pairs = [(a, b) for a, b in itertools.product(labels, repeat=2) + if table[a][b] != table[b][a] + and defect(((1 << table[b][a],),), homogeneous) == 2] + need(len(pairs) > 0, "noncommuting fixture domain") + columns = 0 + omissions = 0 + for i, first in enumerate(pairs): + second = pairs[(i + 1) % len(pairs)] + events = clean_events(first, second) + target = ((1 << table[first[1]][first[0]], 0), + (0, 1 << table[second[1]][second[0]])) + need(replay(events, table) == target, "full formal clean endpoint") + need(defect(target, homogeneous) == 4, "sharp four-call boundary") + for call in range(2, 6): + need(replay(events[:call] + events[call + 1:], table) != target, "omitted call") + omissions += 1 + for role, g in itertools.product(range(2), range(len(table))): + vector = tuple(frozenset((g,)) if j == role else frozenset() for j in range(2)) + expected = regular_apply(target, vector, table) + actual = vector + for event in events: + actual = regular_apply(event, actual, table) + need(actual == expected, "faithful arbitrary-input clean circuit") + columns += 1 + return len(pairs), columns, omissions, pairs[0] + + +def controls(table, homogeneous, pair): + count = 0 + events = clean_events(pair, pair) + dirty = [identity(4), *events[1:]] + need(replay(dirty, table)[0][2] != 0, "dirty-helper leak control") + count += 1 + norm = (1 << len(table)) - 1 + need(norm != 0 and image(((norm,),), homogeneous) == (0, 0, 0), "nonfaithful kernel") + target = replay(events, table) + altered = ((target[0][0] ^ norm, target[0][1]), target[1]) + need(image(altered, homogeneous) == image(target, homogeneous) and altered != target, + "represented equality cannot certify formal equality") + count += 1 + need(defect(((1 << pair[0],),), homogeneous) == 1, "free address countercontrol") + count += 1 + double = ((1 << pair[0], 0), (0, 1 << pair[0])) + need(defect(double, homogeneous) == 2, "rank-two undercharge control") + count += 1 + for case in range(4): + try: + if case == 0: + make_group(3) + elif case == 1: + scalar((2,), 1) + elif case == 2: + paid(2, pair[0], 1, 2) + else: + multiply(identity(1), identity(2), table) + except ValueError: + count += 1 + else: + raise ValueError("invalid domain accepted") + return count + + +def main(): + small_table, small_homogeneous = make_group(1) + table, homogeneous = make_group(2) + rectangles, digest = exhaustive_rectangles(small_table, small_homogeneous) + free_count, paid_count, labels = free_and_paid(homogeneous) + fixtures, columns, omissions, pair = clean_fixtures(table, homogeneous, labels) + result = { + "status": "PASS_CLEAN_AFFINE_ERASURE_FLOOR", "claim_type": "scoped proof with finite corroboration", + "rectangular_products": rectangles, "rectangular_digest": digest, + "free_scalar_maps": free_count, "paid_factors": paid_count, + "clean_erasing_fixtures": fixtures, "faithful_basis_columns": columns, + "omission_controls": omissions, "boundary_controls": controls(table, homogeneous, pair), + "new_fixture_minimum": 4, "no_new_kappa": True, + } + package = Path(__file__).resolve().parent + names = ("README.md", "PROOF.md", "TASK.json", "SOURCES.json", "VERIFY.json", "verify.py") + result["source_sha256"] = {name: hashlib.sha256((package / name).read_bytes()).hexdigest() + for name in names} + print(json.dumps(result, sort_keys=True, indent=2)) + + +if __name__ == "__main__": + main()