diff --git a/research/a4-dirty-workspace-minimum/PROOF.md b/research/a4-dirty-workspace-minimum/PROOF.md new file mode 100644 index 0000000000..18fa8d7543 --- /dev/null +++ b/research/a4-dirty-workspace-minimum/PROOF.md @@ -0,0 +1,113 @@ +# Tight radical rank removes all dirty workspace + +## Statement and cited premises + +Let `a=(123)`, `b=(124)`, `c=aba^-1b^-1`, and `d=ab` in A4. +For every finite `r>=4`, the exact minimum number of paid factors for +`T_r=diag([a],[b],[c],[d],1,...,1)` is eight in the following model. +Work over `F2[A4]`. A paid factor is `D_N(g)=I+([g]+1)N`, where g is +a or b and `N=xy^T` is a binary rank-one idempotent, so `y^T x=1`. +Scalar `GL_r(F2)` maps are free. All r inputs are arbitrary, and the +complete formal operator must equal `T_r`. There are no clean roles, +COPY, ERASE, other address letters or free inverses. Restoration is paid. + +The new assertion is that a hypothetical six-call word on any r roles +restricts to a legal six-call word on four roles. The eight-call conclusion +uses two cited premises, neither audited or replayed here. + +* Cinna Davis #2116 excludes words of length at most six on four roles by + a finite exact group-algebra certificate. Sagar Thakrar #4032 retains + that exclusion with two further exact joins. +* Sagar Thakrar #4032 proves `n_a,n_b>=3` and `n_a=n_b mod 3` at every + finite role count. Its twisted-functional decompositions below have + rank three for each letter. These are written all-role statements. + +SOURCES.json pins both packages at the base commit. The six-call exclusion +remains a finite-certificate dependency. No wholly written replacement for +that exclusion is claimed. + +## 1. Normalize scalar maps + +Binary scalar conjugation preserves rank-one idempotents. Collect all free +scalar maps at one end of the word. Augmentation to F2 sends every paid +factor and `T_r` to `I_r`, so the collected scalar map is `I_r`. We may +therefore use a pure paid word in the original target coordinates. +Let H be the binary span of the first four coordinate vectors. + +## 2. Rank saturation + +Over any extension K of F2, suppose `D=sum_(j=1)^q x_j v_j`, with binary +columns `x_j`, K-rows `v_j`, and `rank_K D=q`. The column span of D is +contained in the K-span of the q columns `x_j`. Both spaces have dimension +q and hence are equal. Every `x_j` belongs to `col_K D`. If that space is +a coordinate space, all entries outside it vanish in every `x_j`. + +## 3. Apply equality to both letters + +Assume a six-call word equals `T_r`. The inherited floors force +`n_a=n_b=3`. In #4032's base-a splitting, each paid factor is `B_k E_k`. +The semisimple factor is `B_k=D_(N_k)(a)` for an a-call and +`B_k=D_(N_k)(a^2)` for a b-call. The latter has radical part +`E_k=I+([d]+1)N_k` because `b=a^2 d`. Set `C_k=B_(k+1)...B_L`. + +The inherited twisted functional Phi to F4 gives + +```text +diag(0,mu(d),mu(c),mu(d),0,...,0) + = sum_(b calls k) aug(C_k)^-1 mu(d) x_k y_k^T psi(C_k). +``` + +The three nonzero diagonal entries are nonzero because mu is injective +on the Klein four subgroup. Every `B_k` has augmentation `I_r`, since +`aug([a]+1)=aug([a^2]+1)=0`. Thus `aug(C_k)=I_r`, not an unspecified +invertible map. There are exactly three summands. Section 2 places every +b-call column in `H_b=span_F2(e_2,e_3,e_4)`. + +Using base b instead and putting `e=ba`, the inherited defect is +`diag(mu(e),0,mu(c),mu(d),0,...,0)`. Its suffixes again have augmentation +identity. Section 2 places every a-call column in +`H_a=span_F2(e_1,e_3,e_4)`. + +Consequently every paid output column `x_k` belongs to H. The rows +`y_k^T` may still read arbitrary extra dirty inputs. + +## 4. Restrict each factor + +In the split into H and its coordinate complement, write `x_k=(x'_k,0)` +and `y_k=(y'_k,y''_k)`. The column `x'_k` is nonzero and +`(y'_k)^T x'_k=y_k^T x_k=1`. Hence `N'_k=x'_k(y'_k)^T` is a nonzero +binary rank-one idempotent on four roles. Each factor has block form + +```text +[ D_(N'_k)(g_k) * ] +[ 0 I ]. +``` + +Taking the upper-left block commutes with multiplication of these block +matrices. The six restricted factors therefore have product `T_4`, in +contradiction to the cited four-role finite exclusion. Dependence on dirty +inputs in the upper-right blocks cannot change this product identity. + +## 5. Exact minimum and limits + +The inherited floors exclude lengths at most five. At seven calls they +allow only `(3,4)` and `(4,3)`, which violate `n_a=n_b mod 3`. +Section 4 excludes six. Separate-coordinate words `a`, `b`, `abba`, `ab` +use eight calls and extend by identity on every extra role. Eight is thus +exact for every finite r, using the cited certificate and written identities. + +This is an abstract register obstruction, not a physical supplier. Other +fields, nilpotent couplings, changed alphabets and different targets are +outside the statement. No new kappa, selected-frontier change, full +multiplication theorem or proof-kernel acceptance is claimed. + +## Credit + +The compression argument is produced by Nick Petalas. Sagar Thakrar #4032 +supplies the radical-rank decompositions, all-role floors and determinant +congruence. Cinna Davis #2116 supplies the model, target, direct word and +finite four-role exclusion. Retain Cinna Davis #2047/#2248/#2085, +juper997 #1478, woklerx #1443, Gareth Davidson #1333, commdata2338 #1414, +eumemic #288, Ali Romman #468 and the register-model lineage credited by +those predecessors. Rank saturation and invariant-subspace restriction +are classical linear algebra. Apache-2.0. diff --git a/research/a4-dirty-workspace-minimum/README.md b/research/a4-dirty-workspace-minimum/README.md new file mode 100644 index 0000000000..95997c7628 --- /dev/null +++ b/research/a4-dirty-workspace-minimum/README.md @@ -0,0 +1,150 @@ +# The A4 eight-call floor survives arbitrary dirty workspace + +For every finite `r>=4`, the formal endpoint +`diag([a],[b],[aba^-1b^-1],[ab],1,...,1)` over `F2[A4]` has exact paid-call +minimum **eight**, with arbitrary restored dirty roles, rank-one idempotent +couplings, positive a/b calls and free binary scalar mixing. + +The new result is a **scoped written workspace-compression proof** with +finite exact corroboration. Any hypothetical six-call word compresses to +the original four target roles. The minimum-eight corollary uses Cinna +Davis's [#2116](https://github.com/CrocSwap/integer-mult-bounds/pull/2116) +finite four-role exclusion and Sagar Thakrar's +[#4032](https://github.com/CrocSwap/integer-mult-bounds/pull/4032) all-role +radical-rank and determinant bounds as cited premises. Their searches and +proof checks are not replayed or audited here. This does not replace the +finite six-call exclusion with a wholly written proof. + +No new kappa, selected-frontier change or physical supplier is claimed. + +## The new step + +[PROOF.md](PROOF.md) gives the model and full argument. At six calls, both +letters must attain their inherited rank-three floors. The augmentation +of every semisimple suffix is identity, so equality forces each b-call's +original binary output column into coordinates 2,3,4, and each a-call's +column into coordinates 1,3,4. Every factor consequently has the form + +```text +[ four-role paid factor arbitrary dirty-input reads ] +[ 0 I ]. +``` + +Restricting to the first four roles preserves the nonzero rank-one +idempotent contract and commutes with multiplication. The restricted +six-call word would realize the four-role target excluded by #2116/#4032. +Their all-role lower bounds already exclude every other length below eight. +The inherited direct eight-call word extends by identity on extra roles. + +This answers the restored-workspace gap in #4032's scope. A coefficient +search on more roles cannot rescue a six-call word for this endpoint. +The rank-saturation step is essential: the checker includes four nonzero +rank-one summands of a rank-three target whose dirty output columns cancel. +Thus a version of the argument with slack in the call count would fail. + +## Evidence and reproduction + +From the repository root, use standard-library CPython 3.12: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/a4-dirty-workspace-minimum/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -O -B research/a4-dirty-workspace-minimum/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/a4-dirty-workspace-minimum +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/a4-dirty-workspace-minimum --check-source-history +``` + +Any installed CPython 3.12 may replace that interpreter path. The standalone +verifier also works in a Git-free export. Expected markers are +`PASS_A4_DIRTY_WORKSPACE_MINIMUM` and `PASS_REGISTERED_RESEARCH_PACKAGE`. +Normal and optimized replay run the same explicit checks. + +The checker enumerates all 29,791 ordered triples of nonzero binary columns +in five dimensions. Of these, 26,040 are independent. For each independent +triple and both diagonal support patterns, F4 augmented-matrix elimination +agrees with a separate oracle enumerating the binary column span. Exactly +336 triple/support pairs are compatible, and every compatible triple lies +in the required coordinate support. These are new rank-saturation fixtures, +not a census of predecessor words. + +The literal A4 regular action checks all 3,600 admitted single factors whose +output columns lie in the first four coordinates, across role counts 4..7. +An additional 256 deterministic words have lengths 2..8. The resulting +3,856 word fixtures check 287,616 complete role/address basis columns, +including every extra-role input column. Their lower blocks are identity +and their upper-left blocks equal the products of the restricted factors. +Dirty inputs may feed target outputs; no clean-input assumption is made. +The direct eight-call upper bound checks a further 264 basis columns at +role counts 4..7. Seven malformed field/coupling inputs reject, and the +rank-slack counterexample passes as a boundary control. A separate positive +fixture requires an extra dirty input to contribute to a target output. +Field arithmetic +also checks the defining polynomial, associativity and distributivity. + +Each run generates a receipt binding all six package files by SHA256 and +prints it to stdout. `--emit` prints only that generated receipt. There is +no handwritten or frozen receipt and no default filesystem output. The +finite tests corroborate the new linear-algebra implication; universal +coverage comes from the written proof. Hosted replay and scientific +acceptance are separate from these checks. + +## Scope, sources and costs + +The scientific base is canonical main +`ec2780e8aeb1c88acaf5e9e470ef8c68e7fbbb6c`, priority revision 7. +[SOURCES.json](SOURCES.json) pins the predecessor READMEs and #2116's +RESULT.json as historical mathematical premises. They are not runtime +inputs. No predecessor executable, generated search output or numerical +count is imported by this verifier. Frozen predecessor files stay intact. + +[TASK.json](TASK.json) records a changed `bit-new-register-model` scope. +This is a formal-model side result rather than a new native alphabet. +The card's current first-step substitute, `research_selected_baseline.py`, +passed its source-binding orientation check. That is not evidence for this +theorem. The advance [CLAIM](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19145499) +precedes the proof and finite corroboration. Entry overlap coverage includes +live PRs, recent handoffs, active Discussions, merged A4/workspace searches +and all-main README terms. Sparse cached local coverage and unpublished +work remain limitations; search absence is not a novelty certificate. + +Every role in this formal contract has arbitrary data and must satisfy the +full endpoint. There are no extra preparation or restoration calls in the +coordinate upper bound. Native implementation, frames, ownership, routing, +hosting, precision/tape, stock, recursive child ranks, compiler and outer +admission remain unpriced and unproved. Unknown costs are not zero. +No physical expansion round is proposed. Nilpotent couplings, other fields, +other targets or alphabets are outside the theorem. Lean, Docker, selected +cold replay and independent human or proof-kernel review are unrun. + +## Engineering constraints + +Build the Lever supplies a rerunnable exact checker. Prove It Works requires +full literal operator columns for restriction, including dirty inputs. +Power of Ten bounds all code loops by fixed domains, at most seven roles, +eight factors, 84 regular coordinates and matrices of shape at most 8 by 8. +Every function is below 60 physical lines. Acceptance uses explicit +exceptions that remain active under optimization. There is no recursion, +subprocess, dynamic import, shared mutable state or runtime code generation. +Managed Python allocation is a bounded rule-3 deviation; allocator internals +are not inspected. Each local file read is capped at 128 KiB. Warning-strict +normal and optimized registered checks provide recurring diagnostics. + +## Open next questions + +Can the original four-role six-call exclusion be replaced by a wholly written +contradiction? This would remove the finite-certificate dependency from the +all-workspace theorem. Start with compatibility of the two tight rank-three +decompositions on the four target coordinates, or their second radical-layer +coefficients. The missing compatibility argument is the blocker. This package +does not reserve that question. Its structured form is in TASK.json. + +## Credit + +This contribution is produced by Nick Petalas. Sagar Thakrar #4032 supplies +the radical-rank identities, all-role floors and determinant congruence. +Cinna Davis #2116 supplies the alphabet, endpoint, coordinate word and +finite four-role exclusion. Retain Cinna Davis #2047/#2248/#2085, +juper997 #1478, woklerx #1443, Gareth Davidson #1333, commdata2338 #1414, +eumemic #288, Ali Romman #468 and the retained register-model lineage. +The new step is tight-rank workspace compression, not the predecessor +four-role optimum. The underlying rank and restriction facts are classical. +Independent human and formal proof-kernel review are unclaimed. Apache-2.0. diff --git a/research/a4-dirty-workspace-minimum/SOURCES.json b/research/a4-dirty-workspace-minimum/SOURCES.json new file mode 100644 index 0000000000..972fc8a87f --- /dev/null +++ b/research/a4-dirty-workspace-minimum/SOURCES.json @@ -0,0 +1,36 @@ +{ + "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/a4-seven-call-radical-rank/README.md", + "usage": "provenance", + "git_blob": "ab5ea83019119dcada4b654b137d418503014cf5", + "sha256": "26c9a90b1e73ce90b6711417db3f023e79192acdde8b94f1e7cfa0a93fafd42b" + }, + { + "path": "research/a4-commutator-four-role-seed-dcbf/README.md", + "usage": "provenance", + "git_blob": "4611a7e147edc288c0355207dde2174f7867e523", + "sha256": "07d90cc975b359e30ff4b978130c4d1893d610ff244aa29e71f3a891abdb33ba" + }, + { + "path": "research/a4-commutator-four-role-seed-dcbf/RESULT.json", + "usage": "provenance", + "git_blob": "fa78cc9381f27efea106aac5947a465daa89b795", + "sha256": "2ff56618b041bbfe7d8c3c4e521cdf1b33b70d0f7299c1f56c780e76ec40a5c6" + } + ] +} diff --git a/research/a4-dirty-workspace-minimum/TASK.json b/research/a4-dirty-workspace-minimum/TASK.json new file mode 100644 index 0000000000..da9ff0cc87 --- /dev/null +++ b/research/a4-dirty-workspace-minimum/TASK.json @@ -0,0 +1,86 @@ +{ + "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": "changed", + "actual_scope": "Tight-rank compression of every hypothetical six-call A4 target word with restored dirty workspace to four roles; exact eight-call corollary using the cited four-role finite exclusion.", + "scope_change_reason": "A scoped formal-model side result takes the restored-workspace gap in Sagar Thakrar #4032, rather than introducing a physically priced new alphabet.", + "bottleneck_link": "This closes one workspace escape in a nonabelian register screening model. It does not improve the selected supplier or establish native conversion costs.", + "budget_minutes": 60, + "stop_rule": "Stop at the first proved workspace-compression result; do not replace or replay the predecessor finite census.", + "outcome": "completed", + "evidence": "PROOF.md proves all finite role counts. verify.py exhausts 29,791 binary column triples in five dimensions and corroborates factor restriction on all regular basis columns in its bounded domain.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can the four-role six-call exclusion be replaced by a wholly written contradiction?", + "why_it_matters": "The all-workspace optimum would then no longer depend on a finite exhaustive certificate.", + "first_step": "Use both tight rank-three decompositions on the original four target roles, or retain second radical-layer coefficients.", + "blocked_by": "Compatibility of the two decompositions beyond their column supports." + } + ], + "claim_type": "Scoped written proof with finite exact corroboration; eight-call corollary depends on the cited predecessor finite certificate.", + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19145499", + "overlap": { + "entry_utc": "2026-10-23T12:22:00Z", + "base_commit": "ec2780e8aeb1c88acaf5e9e470ef8c68e7fbbb6c", + "coverage": "Live first 100 open PRs; latest 200 account PRs; latest 60 handoff comments and 15 active Discussion threads; all-main README keyword searches; all-state A4 and merged A4 workspace searches. Cached card scan has incomplete sparse local coverage. Unpublished work and arbitrary code diffs are not covered.", + "scope": "Not a follow-up to this account's last-24-hour work. Builds on Sagar Thakrar #4032 and Cinna Davis #2116.", + "submission_utc": "2026-10-23T12:29:18.886638+00:00", + "submission_base": "ec2780e8aeb1c88acaf5e9e470ef8c68e7fbbb6c" + }, + "environment": { + "python": "3.12.15", + "platform": "macOS-27.0.1-arm64-arm-64bit", + "dependencies": "Python standard library; optional Ruff 0.17.1 diagnostics" + }, + "local_validation": { + "normal_seconds": 1.18, + "optimized_seconds": 1.17, + "registered_package": "passed; both explicit commands", + "static_analysis": "Ruff 0.17.1 E,F,I,B,UP,SIM,RUF,C4,PIE,PERF,PTH,RET and format passed", + "timing_scope": "Single wall-clock timings of each exact registered command, not performance benchmarks." + } +} diff --git a/research/a4-dirty-workspace-minimum/VERIFY.json b/research/a4-dirty-workspace-minimum/VERIFY.json new file mode 100644 index 0000000000..d8c1de8c99 --- /dev/null +++ b/research/a4-dirty-workspace-minimum/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Rank-saturation exhaust, independent binary span oracle, literal full regular-action restriction, complete eight-call workspace boundary and boundary controls." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Same exact checks with optimization; all acceptance checks remain enabled." + } + ] +} diff --git a/research/a4-dirty-workspace-minimum/verify.py b/research/a4-dirty-workspace-minimum/verify.py new file mode 100644 index 0000000000..11f4912d20 --- /dev/null +++ b/research/a4-dirty-workspace-minimum/verify.py @@ -0,0 +1,266 @@ +#!/usr/bin/env python3 +"""Corroborate tight-rank compression without replaying predecessor censuses.""" + +from __future__ import annotations + +import hashlib +import itertools +import json +import sys +from pathlib import Path + + +def require(ok: bool, message: str) -> None: + if not ok: + raise ValueError(message) + + +def mul4(a: int, b: int) -> int: + value = (a & 1) * b + if a & 2: + value ^= (b << 1) ^ (7 if b & 2 else 0) + return value + + +def rank4(rows: list[list[int]]) -> int: + require(1 <= len(rows) <= 8, "row bound") + width = len(rows[0]) + require(1 <= width <= 8, "column bound") + require(all(len(row) == width for row in rows), "ragged matrix") + require( + all(type(v) is int and 0 <= v < 4 for row in rows for v in row), + "invalid field entry", + ) + work = [row[:] for row in rows] + pivots = 0 + for col in range(width): + candidates = [i for i in range(pivots, len(work)) if work[i][col]] + if not candidates: + continue + p = candidates[0] + work[pivots], work[p] = work[p], work[pivots] + inverse = (0, 1, 3, 2)[work[pivots][col]] + require(mul4(work[pivots][col], inverse) == 1, "invalid pivot inverse") + work[pivots] = [mul4(inverse, v) for v in work[pivots]] + for i in range(len(work)): + if i != pivots and work[i][col]: + scale = work[i][col] + work[i] = [ + v ^ mul4(scale, w) + for v, w in zip(work[i], work[pivots], strict=True) + ] + pivots += 1 + return pivots + + +def saturation_checks() -> dict[str, int]: + counts = {"triples": 0, "full_rank": 0, "compatible": 0} + targets = ((0, 2, 3, 2, 0), (3, 0, 1, 2, 0)) + for columns in itertools.product(range(1, 32), repeat=3): + counts["triples"] += 1 + rows = [[(x >> i) & 1 for x in columns] for i in range(5)] + if rank4(rows) != 3: + continue + counts["full_rank"] += 1 + # A separate binary oracle enumerates the entire column span. + span = {0} + for x in columns: + span |= {v ^ x for v in tuple(span)} + for target in targets: + augmented = [ + row + [target[i] if i == j else 0 for j in range(5)] + for i, row in enumerate(rows) + ] + compatible = rank4(augmented) == 3 + oracle = all((1 << i) in span for i, v in enumerate(target) if v) + require(compatible == oracle, "field/binary span disagreement") + if compatible: + support = sum(1 << i for i, v in enumerate(target) if v) + require(all(x & ~support == 0 for x in columns), "support escape") + counts["compatible"] += 1 + require(counts["triples"] == 31**3, "incomplete domain") + require(counts["full_rank"] == 31 * 30 * 28, "basis count") + require(counts["compatible"] == 2 * 7 * 6 * 4, "target basis count") + return counts + + +def group() -> tuple[list[list[int]], int, int]: + perms = [ + p + for p in itertools.permutations(range(4)) + if sum(p[i] > p[j] for i in range(4) for j in range(i + 1, 4)) % 2 == 0 + ] + table = [ + [perms.index(tuple(p[q[i]] for i in range(4))) for q in perms] for p in perms + ] + require(len(perms) == 12, "A4 size") + return table, perms.index((1, 2, 0, 3)), perms.index((1, 3, 2, 0)) + + +def apply_word( + word: list[tuple[int, int, int]], roles: int, basis: int, table: list[list[int]] +) -> tuple[int, ...]: + require(4 <= roles <= 7 and 0 <= basis < 12 * roles, "action bounds") + require(len(word) <= 8, "word bound") + state = [0] * roles + state[basis // 12] = 1 << (basis % 12) + for x, y, label in word: + require(0 < x < 16 and 0 < y < 1 << roles, "coupling bounds") + require( + (x & y).bit_count() % 2 == 1 and 0 <= label < 12, + "rank-one idempotent contract", + ) + source = 0 + for j in range(roles): + if y >> j & 1: + source ^= state[j] + moved = sum(1 << table[label][j] for j in range(12) if source >> j & 1) + for i in range(4): + if x >> i & 1: + state[i] ^= source ^ moved + return tuple(state) + + +def restriction_checks() -> dict[str, int]: + table, a, b = group() + result = {"factors": 0, "words": 0, "basis_columns": 0, "dirty_reads": 0} + for roles in range(4, 8): + factors = [ + (x, y, g) + for x in range(1, 16) + for y in range(1, 1 << roles) + if (x & y).bit_count() % 2 + for g in (a, b) + ] + result["factors"] += len(factors) + words = [[f] for f in factors] + words += [ + [ + factors[(37 * seed + 19 * j + j * j) % len(factors)] + for j in range(2 + seed % 7) + ] + for seed in range(64) + ] + for word in words: + restricted = [(x, y & 15, g) for x, y, g in word] + result["words"] += 1 + result["dirty_reads"] += sum(y >> 4 != 0 for _, y, _ in word) + for basis in range(12 * roles): + full = apply_word(word, roles, basis, table) + tail = tuple( + (1 << (basis % 12)) if basis // 12 == i else 0 + for i in range(4, roles) + ) + require(full[4:] == tail, "dirty output changed") + if basis < 48: + small = apply_word(restricted, 4, basis, table) + require(full[:4] == small, "restriction not multiplicative") + result["basis_columns"] += 1 + require(result["dirty_reads"] > 0, "dirty reads missing") + return result + + +def direct_checks() -> int: + table, a, b = group() + identity = next(i for i in range(12) if table[i] == list(range(12))) + # Chronological left action reverses displayed group products. + word = [ + (1, 1, a), + (2, 2, b), + (4, 4, a), + (4, 4, b), + (4, 4, b), + (4, 4, a), + (8, 8, b), + (8, 8, a), + ] + c = table[table[table[a][b]][table[a][a]]][table[b][b]] + d = table[a][b] + columns = 0 + for roles in range(4, 8): + labels = [a, b, c, d] + [identity] * (roles - 4) + for basis in range(12 * roles): + expected = [0] * roles + expected[basis // 12] = 1 << table[labels[basis // 12]][basis % 12] + require( + apply_word(word, roles, basis, table) == tuple(expected), + "eight-call boundary", + ) + columns += 1 + return columns + + +def controls() -> int: + # One slack term permits dirty-column cancellation; each summand is nonzero. + xs = (1 | 16, 2, 4, 16) + vs = ((1, 0, 0), (0, 2, 0), (0, 0, 3), (1, 0, 0)) + total = [[0] * 3 for _ in range(5)] + for x, row in zip(xs, vs, strict=True): + for i in range(5): + for j in range(3): + if x >> i & 1: + total[i][j] ^= row[j] + require(rank4(total) == 3 and total[4] == [0, 0, 0], "slack control") + require(any(x & 16 for x in xs), "slack dirty column") + rejected = 0 + for rows in ([], [[1, 0], [1]], [[4]], [[True]]): + try: + rank4(rows) + except ValueError: + rejected += 1 + table, a, _ = group() + identity = next(i for i in range(12) if table[i] == list(range(12))) + expected = ((1 << a) ^ (1 << identity), 0, 0, 0, 1 << identity) + require( + apply_word([(1, 17, a)], 5, 48 + identity, table) == expected, + "dirty input must contribute to target", + ) + for word in ([(1, 2, a)], [(16, 16, a)], [(1, 1, 12)]): + try: + apply_word(word, 5, 0, table) + except ValueError: + rejected += 1 + require(rejected == 7, "boundary rejection missing") + return rejected + 2 + + +def main() -> None: + require(sys.argv[1:] in ([], ["--emit"]), "usage: verify.py [--emit]") + require(mul4(2, 2) == 3 and mul4(2, 3) == 1, "field polynomial") + for a, b, c in itertools.product(range(4), repeat=3): + require(mul4(a, mul4(b, c)) == mul4(mul4(a, b), c), "field associativity") + require(mul4(a, b ^ c) == mul4(a, b) ^ mul4(a, c), "field distributivity") + result = { + "saturation": saturation_checks(), + "restriction": restriction_checks(), + "direct_basis_columns": direct_checks(), + "controls": controls(), + } + package = Path(__file__).resolve().parent + names = ( + "PROOF.md", + "README.md", + "SOURCES.json", + "TASK.json", + "VERIFY.json", + "verify.py", + ) + require( + all((package / name).stat().st_size <= 131072 for name in names), + "package file size bound", + ) + hashes = { + name: hashlib.sha256((package / name).read_bytes()).hexdigest() + for name in names + } + receipt = {"result": result, "sha256": hashes} + canonical = json.dumps(receipt, sort_keys=True, indent=2) + "\n" + if sys.argv[1:] == ["--emit"]: + print(canonical, end="") + return + print(canonical, end="") + print("PASS_A4_DIRTY_WORKSPACE_MINIMUM") + + +if __name__ == "__main__": + main()