diff --git a/research/bit-clean-workspace-compression/README.md b/research/bit-clean-workspace-compression/README.md new file mode 100644 index 0000000000..bd752384cc --- /dev/null +++ b/research/bit-clean-workspace-compression/README.md @@ -0,0 +1,233 @@ +# Arbitrarily many clean auxiliaries still need six calls + +In the formal abelian bit model below, two invertible rational 3-by-3 targets +need exactly six rank-one calls, even with any finite number of clean auxiliary +registers. Clean auxiliaries start at zero and must return to zero. The theorem +uses a new workspace reduction and an independently implemented exact census +of 69,728 reduced words. It is a computer-assisted scoped theorem, not a native +supplier, a new kappa or proof-assistant verification. + +waynenilsen's [PR2167](https://github.com/CrocSwap/integer-mult-bounds/pull/2167), +head `cea5d7be431b09877848354f04d5f2ba512339fd`, establishes the same minimum +with one or two clean auxiliaries and explicitly leaves arbitrary counts open. +Its [canonical discussion](https://github.com/CrocSwap/integer-mult-bounds/discussions/2073) +is the predecessor investigation. No code or recorded search output from that +PR is used here. This package closes the unbounded-workspace question through a +separate proof and census, rather than repeating its 24.9-billion-word run. + +## Model + +Let `H` be generated by nonzero rational rank-one address matrices `A_j` in +`M_3(Q)`. Work over `F2[H]`, with `[A][B]=[A+B]`. On any finite number `n` of +binary scalar roles, call `j` acts chronologically by + +`F_j = I + ([A_j]-1) x_j y_j^T`, with `y_j^T x_j = 1`. + +Thus its scalar coupling is rank one and idempotent. The endpoint need only +satisfy `P e_i = [C_i] e_i` for the two data basis vectors `i=0,1`, where +`P=F_k ... F_1` and both `C_i` are invertible. Every auxiliary output on these +data columns is zero. Auxiliary input columns are unrestricted, since the +auxiliaries start at zero. Equality is coefficientwise in the formal group +algebra, not equality at sampled address sizes. + +Free binary scalar changes of basis are allowed. Commute them to one final +scalar map `M`, conjugating the rank-one idempotents along the way. Augmentation +of the clean endpoint gives `M e_i=e_i`. Removing `M` therefore preserves the +same data-column endpoint, even though `M` need not be identity on auxiliary +columns. Free address maps, nilpotent couplings and discarded nonzero auxiliary +outputs are not included. + +## 1. Delete a coloop image in a shortest word + +This argument works for any address dimension and any number of data targets +of rational rank at least two. Call `j` a coloop when `x_j` is outside the binary +span of all other `x_t`. Choose a binary linear functional `lambda` killing +those other images and satisfying `lambda(x_j)=1`. + +Only call `j` can change the `lambda` coordinate. For each data input, +chronological telescoping gives + +`([A_j]-1) h_ji = ([C_i]-1) lambda(e_i)`, + +where `h_ji = y_j^T F_(j-1) ... F_1 e_i`. + +Since `rank A_j=1` but `rank C_i>=2`, there is a rational linear functional +`ell` on address matrices killing `A_j` but not `C_i`. The induced map +`[A] -> [ell(A)]` makes the left side zero. The right side is nonzero if +`lambda(e_i)=1`. Hence `lambda(e_i)=0` for every data input. Back in the +original ring, the displayed equation gives `h_ji=0`, since `A_j!=0` and the +group algebra of a finitely generated torsion-free abelian group is a domain. +Call `j` therefore acts as identity on every actual data column at its cut. +Deleting it preserves all subsequent data columns and the clean endpoint. + +Consequently a shortest successful word has no coloop image. If it has `k` +calls, its image span `U=sum im(x_j y_j^T)` has dimension at most `k-1`. +The rank-at-least-two hypothesis matters. A one-call rank-one target on one +data role is a nonremovable active coloop, checked by the replay. + +## 2. Compress the clean workspace + +Every coefficient image of `P-I` lies in `U`. The coefficient at each nonzero +data target contains its data axis, so `U` contains both data axes. It is also +invariant under every paid coupling. Restrict to `U`, using a binary basis +starting with the data axes. Each restricted coupling remains rank-one +idempotent: its image vector lies in `U` and it fixes that vector. The clean +data-column endpoint survives; the remaining basis coordinates still start +and end at zero. No condition on auxiliary input columns is needed. + +Thus a shortest successful `k`-call word uses at most `k-1` total roles. +If a word of at most five calls exists, first take a shortest one and split +nonzero frames as needed using + +`D_N(A) = D_N(A/2) D_N(A/2)`. + +Splitting preserves the rational frame span and the absence of image coloops. +It yields five calls on an image span of dimension `r` with `2 <= r <= 4`. + +This is a clean-input reduction. It is different from the mixed-target dirty +reduction in [PR2900](https://github.com/CrocSwap/integer-mult-bounds/pull/2900), +head `af4e996ac29cfced53ce8a6d1feed95918fd7f76`, which requires the entire +endpoint matrix and uses an augmentation bound involving target-frame span. +We do not assume its stronger dirty endpoint for clean auxiliaries. + +## 3. Reduce the rational addresses to 117 collision patterns + +The inherited low-span argument of +[Ali Romman's PR468, section 3](../bit-three-register-lower-bound/README.md) +works on clean data columns, as PR2167 observes. For completeness, choose a +basis of paid rank-one frames when their span has dimension at most three. +An invertible target forces dimension exactly three. Common invertible row +and column transformations make that span diagonal, so each paid rank-one +frame occupies exactly one diagonal line. Project onto one line. Both data +targets have nonzero projected labels, and the projected data block of `P-I` +has rank two over the projected Laurent fraction field. Each remaining call +contributes rank at most one by telescoping. Every line therefore needs at +least two calls, requiring six in total. + +At five calls the frame span is consequently four or five. Its integral +relation lattice is saturated and has rank at most one. With no relation, +subset sums do not collide. With a primitive generator `a` having an entry +of absolute value at least two, they do not collide either: no nonzero +integer multiple of `a` is a difference of binary subset indicators. +Otherwise `a` is a cube vector in `{-1,0,1}^5`, up to sign, with at least two +nonzero entries. There are 116 such vectors and one no-collision case. +These are exactly the same address reductions used by the predecessor, +not a search bound on rational frame numerators. + +Expand the full product as `sum_b M_b [sum_j b_j A_j]`, with `b` binary. +For each relation pattern, add coefficients whose subset indicators differ +by a multiple of `a`. A possible data input is any nonzero binary vector `v` +for which the grouped polynomial sends `v` to a single monomial times `v`. +Two distinct such vectors are automatically independent over `F2`. + +A monomial with subset representative `b` cannot have address rank three if +`b+t a` has support at most two for some rational `t`. Checking `t=-1,0,1` +suffices. A nonzero entry can vanish only at those values; all other `t` +have support at least that of `b`. The no-collision case uses only `support(b)`. +For a noncube relation this deliberately ignores additional sparse rational +representatives, making the screen more favorable, never less, to a proposed +construction. This is a necessary rank test, not an assertion that every +surviving address has rank three. Excluding even these favorable candidates +proves exclusion. + +## 4. Complete reduced scalar census + +Represent the ordered image vectors by the columns of an `r`-by-5 binary +matrix `X`. Row operations change the scalar basis only. Each row space has +one reduced row-echelon representative, so enumerate those representatives, +requiring every column nonzero and no coloop. For each column `x_j`, enumerate +all `2^(r-1)` covectors satisfying `y_j^T x_j=1`. No gate order, relation or +scalar coupling is omitted. After the basis change the two original data axes +can be any two independent binary vectors, which is why all nonzero vectors +are tested rather than only two coordinate columns. + +| Image dimension | Image row spaces | Ordered scalar words | High-rank candidate pairs | +|---:|---:|---:|---:| +| 2 | 35 | 1,120 | 0 | +| 3 | 35 | 35,840 | 0 | +| 4 | 1 | 32,768 | 0 | + +All 69,728 words are tested against all 117 address patterns, a total of +8,158,176 word/pattern cases. In dimension two, 12,208 cases have one possible +rank-three monomial eigenvector, so the one-target branch is nonvacuous. None +has two. Dimensions three and four have none. No five-call word exists. +Splitting excludes every shorter word as above. Six calls suffice by giving +each data role the three rank-one column summands of its invertible target. +This proves the stated exact minimum for any finite number of clean auxiliaries. + +## Reproduce and evidence + +Python 3.12 or newer and a C++20 compiler are required. No third-party Python +packages are needed. From the repository root: + +```sh +python3.12 -I -B scripts/research_package.py --package research/bit-clean-workspace-compression +python3.12 -I -O -B research/bit-clean-workspace-compression/verify.py +python3.12 -I -B research/bit-clean-workspace-compression/test_package.py +``` + +The registered replay compiles with conversion, sign-conversion, shadow and +pedantic warnings treated as errors. It runs the complete native census and +compares `RESULT.json`. The Python oracle independently enumerates actual +binary subspaces and checks all 1,120 dimension-two words plus deterministic +probes in dimensions three and four. Across 1,223 words and 143,091 relation +cases it compares every monomial eigenvector and exponent. It propagates +vectors with exact integer exponent tuples and eliminates the rational +relation, rather than using the C++ matrix expansion and subset-pair tables. +This is a full second implementation for the dimension-two census, not a +second full census in dimensions three and four. + +Positive controls include the exact six-call formal construction with distinct +integer and fractional targets, a removable clean-only coloop and the active +rank-one boundary where deletion is invalid. +Omitting a direct call fails. A synthetic two-eigenvector polynomial tests the +native candidate-acceptance branch but is not presented as a legal five-call +word. The CLI tests run normally and optimized after relocation without Git; +they reject a corrupted receipt/source and actual implementation mutations +that omit quotient grouping, skip the census or strengthen the rank threshold. +Normal replay writes nothing. `--write` regenerates only `RESULT.json`. + +The written reductions and full C++ census establish the scoped theorem. +Finite oracle probes alone do not prove it. Neither PR2167's engine nor its +historical receipt is trusted or imported. Source bindings, predecessor heads, +freshness, commands and limitations are recorded in `SOURCES.json` and +`TASK.json`. No selected cold replay, supplier-native compilation, hosting, +precision, all-size supplier or multiplication theorem is checked. + +## Open next questions + +Does the image-coloop reduction help the three-data-target, eight-call problem +with clean auxiliaries? It bounds a shortest word to at most seven total roles, +but that alone does not justify another large census. First specify one exact +frame multiset with favorable complete native and consumer costs, then test +its rational rank cuts and determinant before scalar enumeration. The missing +candidate and its full physical bill remain blockers. No family expansion is +claimed here. Structured next steps are in `TASK.json`. + +## Credit and implementation limits + +Nick Petalas. Apache-2.0. No independent human or proof-kernel review is claimed. +waynenilsen supplies PR2167's clean-auxiliary question, low-span observation +and one/two-auxiliary results, following the dirty-workspace work in PR1882. +Ali Romman/PR468 supplies the formal model, low-span and rational relation +methods, with eumemic/PR288 and huxint/PR203 retained. The new coloop deletion, +uniform clean compression and reduced census are the contribution here. +Build the Lever led to the replayable reduced census. Prove It Works and Test +Behavior, Not Implementation led to the independent vector oracle and real +CLI implementation mutants. + +Power of Ten review covers these three code files. All functions are below +60 lines, control flow is nonrecursive, and all loops have fixed finite +bounds. C++ uses fixed arrays, at most 32 polynomial coefficients, 117 relation +patterns and 4-by-4 binary matrices. Python and standard-library I/O allocation +are rule 3 deviations. Fixed subspace/probe domains and at most 32 terms per +vector polynomial bound the live collections. The engine's fixed record domain +bounds output below 15 MB; replay additionally rejects output above 2 MB. +Compiler and engine calls each have a 60-second timeout and temporary files +have scoped cleanup. This is a finite research command, not a steady service. +Replace the managed allocations +with fixed storage before service use. The fixed local sorting key and +Unittest dispatch are rule 9 deviations with one key function, six fixed test +methods and bounded subprocesses. No external code is imported or generated. +The generic registered runner supplies process +group cleanup; direct native compiler cancellation is not separately audited. diff --git a/research/bit-clean-workspace-compression/RESULT.json b/research/bit-clean-workspace-compression/RESULT.json new file mode 100644 index 0000000000..ed89ea6c64 --- /dev/null +++ b/research/bit-clean-workspace-compression/RESULT.json @@ -0,0 +1,91 @@ +{ + "schema_version": 1, + "census": { + "summaries": [ + { + "image_dimension": 2, + "image_spaces": 35, + "words": 1120, + "monomial_vectors": 47484, + "candidate_cases": 0, + "high_rank_vector_histogram": [ + 118832, + 12208, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ] + }, + { + "image_dimension": 3, + "image_spaces": 35, + "words": 35840, + "monomial_vectors": 1659156, + "candidate_cases": 0, + "high_rank_vector_histogram": [ + 4193280, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ] + }, + { + "image_dimension": 4, + "image_spaces": 1, + "words": 32768, + "monomial_vectors": 2402432, + "candidate_cases": 0, + "high_rank_vector_histogram": [ + 3833856, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ] + } + ], + "oracle_probes": 1223, + "oracle_relations": 143091, + "relation_patterns": 117 + }, + "controls": { + "six_call_positive": true, + "omission_rejected": true, + "removable_clean_coloop": true, + "rank_one_boundary": true + } +} diff --git a/research/bit-clean-workspace-compression/SOURCES.json b/research/bit-clean-workspace-compression/SOURCES.json new file mode 100644 index 0000000000..fb85c1c717 --- /dev/null +++ b/research/bit-clean-workspace-compression/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "0706e744cbda1e4d0da5a6c569ad9b47876c6960", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "889b95d936746df124872133ae1e7cc339adcb92", + "sha256": "7d185cd8c2af35988d638d969748ad7b670f902606444dbfc748e4402c340df6" + }, + { + "path": "research/bit-dirty-auxiliary-registers/README.md", + "usage": "input", + "git_blob": "273bb963ee40869145cf8309db4f8dddebcfe43d", + "sha256": "da984fddaa09bfa7b1a3e11505e737283cee36e7972b2081f9de28ec420607cd" + }, + { + "path": "research/bit-three-register-lower-bound/README.md", + "usage": "input", + "git_blob": "25e41c370c101a33a6deb978de08b03ed7539b79", + "sha256": "c12b33ef388deece0cbf891505a2ce2c0779a0c3a6cf1f0f7f7039bab59cbebd" + } + ] +} diff --git a/research/bit-clean-workspace-compression/TASK.json b/research/bit-clean-workspace-compression/TASK.json new file mode 100644 index 0000000000..2f3d0b4645 --- /dev/null +++ b/research/bit-clean-workspace-compression/TASK.json @@ -0,0 +1,125 @@ +{ + "schema_version": 1, + "task_id": "bit-new-register-model", + "priority_revision": 5, + "base_commit": "0706e744cbda1e4d0da5a6c569ad9b47876c6960", + "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": "Prove a uniform clean-workspace reduction and exclude five calls for two invertible rational 3-by-3 targets with any finite number of clean auxiliaries.", + "scope_change_reason": "The live PR2167 handoff leaves arbitrary clean counts open. Replace a new mechanism construction by this exact formal-interface gap; finite GL3 and dirty-workspace cases are already covered.", + "bottleneck_link": "This is a scoped bit-side obstruction, not a supplier improvement. It closes the unbounded clean-workspace loophole in the two-target model and prevents an unnecessary larger-register search. No native or exponent improvement follows.", + "budget_minutes": 60, + "stop_rule": "Stop after the coloop reduction and complete reduced five-call census, or at a failed implication. Do not expand to three targets or another construction campaign.", + "outcome": "negative-result", + "evidence": "README sections 1-4 prove the reductions; the independent C++ census checks 69728 scalar words and 117 relation patterns. Python checks every rank-two word and deterministic higher-rank probes. RESULT.json retains all counts.", + "author": "Nick Petalas", + "ai_assistance": "No independent human review is claimed. The written reductions, complete native census and separately implemented finite oracle are the evidence.", + "picker_nonce": "efdebea0d21919512493f05d88f74dcf", + "declared_milestone": "scoped formal-model theorem, not supplier admission", + "family_expansion_decision": "Stop. A changed three-target question needs an exact candidate and a complete physical budget before another dependent search.", + "predecessors": [ + { + "pr": 2167, + "author": "waynenilsen", + "head": "cea5d7be431b09877848354f04d5f2ba512339fd", + "scope": "One and two clean auxiliaries, with arbitrary counts explicitly open; no source or result data reused.", + "url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/2073" + }, + { + "pr": 2900, + "author": "Nick Petalas", + "head": "af4e996ac29cfced53ce8a6d1feed95918fd7f76", + "scope": "Mixed-target dirty compression requires a whole endpoint matrix. The new clean proof constrains only data columns. No implementation reused." + } + ], + "coordination": "Read Discussion1163, active discussions, Discussion1166 and canonical Discussion2073. No advance claim or Discussion mutation was posted under the engineering-mode communication restriction. This is not a retrospective reservation.", + "overlap": { + "open_prs": 490, + "open_checked_at": "2026-10-16T10:13:10.264529+00:00", + "closed_prs": 2115, + "closed_checked_at": "2026-10-16T10:14:54.760215+00:00", + "discussion_records": 1583, + "discussions_checked_at": "2026-10-16T10:13:35.776830+00:00", + "complete_pagination": true, + "limits": "Metadata, local READMEs/TASK files and ledger only. Arbitrary code diffs are not covered. PR2167 and its canonical thread were read directly." + }, + "freshness": { + "upstream_commit": "475fec190d5ad746bd4690574dca30d6901acdaf", + "checked_at_utc": "2026-10-16T10:33:59Z", + "priority_revision": 5, + "decision": "Continue from the original scientific base. Instructions, task catalogue, family status, selected record and both live source inputs are unchanged at refreshed main. PR2167's head is unchanged.", + "open_prs": 492, + "closed_prs": 2115, + "discussion_records": 1585, + "complete_pagination": true, + "warnings": [] + }, + "environment": { + "platform": "Linux 6.6.87.2-microsoft-standard-WSL2 x86_64", + "python": ["CPython 3.12.15", "CPython 3.13.5"], + "compilers": ["GCC 14.2.0", "Clang 19.1.7"], + "limits": "Local Linux only; hosted CI, macOS and Windows execution are not claimed. ASan/UBSan native output equals the Clang output byte-for-byte." + }, + "verification_commands": [ + "python3.12 -I -B scripts/research_package.py --package research/bit-clean-workspace-compression", + "CXX=clang++ python3.12 -I -O -B research/bit-clean-workspace-compression/verify.py", + "python3.13 -I -O -B research/bit-clean-workspace-compression/verify.py", + "python3.12 -B -m unittest discover -s tests -p 'test_research_*.py'", + "ruff check --select E4,E7,E9,F,B,I,UP research/bit-clean-workspace-compression", + "python3.12 -W error -m py_compile research/bit-clean-workspace-compression/verify.py research/bit-clean-workspace-compression/test_package.py", + "g++ -std=c++20 -O1 -g -fsanitize=address,undefined -fno-omit-frame-pointer -Wall -Wextra -Wpedantic -Wconversion -Wsign-conversion -Wshadow -Werror research/bit-clean-workspace-compression/engine.cpp -o /tmp/imb-clean-sanitized" + ], + "unrun_obligations": [ + "Second full implementation for image dimensions three and four", + "Proof-assistant verification", + "Predecessor's original 24.9-billion-word replay, which is not a dependency", + "Native supplier/compiler, hosting, precision, all-size, outer theorem and selected cold replay" + ], + "open_questions": [ + { + "question": "Can a specified three-target eight-call clean-workspace candidate pass complete necessary screens and a full native budget?", + "why_it_matters": "The coloop reduction bounds a shortest word to seven total roles, but the two-target exclusion does not settle that different model.", + "first_step": "Choose and save one exact rank-one frame multiset and target contract; check rational rank cuts, determinant compatibility and an optimistic complete physical bill before scalar search.", + "blocked_by": "No such candidate or full native/consumer budget is provided. A larger census is not justified by the workspace bound alone." + } + ] +} diff --git a/research/bit-clean-workspace-compression/VERIFY.json b/research/bit-clean-workspace-compression/VERIFY.json new file mode 100644 index 0000000000..ebf3af291c --- /dev/null +++ b/research/bit-clean-workspace-compression/VERIFY.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/bit-dirty-auxiliary-registers/README.md", + "research/bit-three-register-lower-bound/README.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Complete C++20 reduced census, independent full dimension-two and sampled higher-dimensional vector oracle, exact six-call positive and omission/coloop boundary controls" + }, + { + "argv": [ + "{python}", + "-B", + "{package}/test_package.py" + ], + "timeout_seconds": 180, + "checks": "Normal/optimized Git-free relocation, read-only replay, receipt/source corruption and three actual engine implementation mutants" + } + ] +} diff --git a/research/bit-clean-workspace-compression/decisions.tsv b/research/bit-clean-workspace-compression/decisions.tsv new file mode 100644 index 0000000000..6f0f62e301 --- /dev/null +++ b/research/bit-clean-workspace-compression/decisions.tsv @@ -0,0 +1,15 @@ +timestamp phase decision reason evidence result +2026-10-16T10:16:34Z plan 1. State the exit predicate before the first iteration. Prove a clean-workspace compression lemma and independently exclude five calls for two rank-three targets, or stop with a precise failed implication. PR2167 and Discussion2073 leave arbitrary clean workspace open. Active. +2026-10-16T10:16:34Z plan 2. Choose a local wake method. Prefer an event-aware watcher for process completion or file changes. Otherwise use a bounded polling interval appropriate to the task. Use the host's recurring wake capability only when the user explicitly asks for future or repeated execution. Synchronous bounded commands suffice. No background workers or repeated loop. No watcher needed. +2026-10-16T10:16:34Z plan 3. Start a decision trail with show-me-your-work when installed. Otherwise create an append-only decisions.tsv with timestamp, phase, decision, reason, evidence, and result columns. Skill unavailable. This file. Started. +2026-10-16T10:16:34Z plan 4. Each iteration makes the smallest evidence-supported change, checks the predicate, logs the result, and discards changes that did not help. First prove coloop deletion; then enumerate reduced image spaces; then independently check the census. Exact group-algebra model. Pending. +2026-10-16T10:16:34Z plan 5. Handle reversible local blockers within scope. Under an explicit full-autonomy grant, apply a default for a reversible user preference, explain it, and give one reply word that reverses it. Pause for missing authority, an irreversible decision, or a user-named gate. Worktree and focused PR authorized; no frontier changes. User assignment. No unresolved preference. +2026-10-16T10:16:34Z plan 6. Continue through a plateau by changing the hypothesis or measurement. Stop at the predicate or a documented dead end. Never weaken the predicate. One scoped result within about 60 minutes, reserving the last quarter for verification. Repository donation guidance. No larger construction campaign. +2026-10-16T10:16:34Z orientation Refine bit-new-register-model to arbitrary clean auxiliaries. Existing finite GL3 and dirty-workspace domains are covered; PR2167 states this clean gap explicitly. Canonical main 0706e744; priority 5; picker efdebea0d21919512493f05d88f74dcf; full live overlap 490 open, 2115 closed, 1583 Discussion records. Distinct formal-interface question. +2026-10-16T10:16:34Z coordination Read existing canonical Discussion2073 without posting an advance claim. Engineering-mode skill forbids human-directed comments; authorized PR publication remains the deliverable. Discussion2073 latest reply points to PR2167 at cea5d7be431b09877848354f04d5f2ba512339fd. No retrospective reservation will be claimed. +2026-10-16T10:19:01Z proof Use image-coloop deletion before workspace restriction. A rational address projection kills the sole image update but not any rank-at-least-two target; the group-algebra domain then makes the call inactive on every data column. README sections 1-2; exact clean-only and rank-one boundary fixtures. A shortest k-call word needs at most k-1 total roles. +2026-10-16T10:21:21Z census Enumerate canonical binary image row spaces and all scalar covectors. This preserves ordered calls while quotienting only scalar basis changes; all possible data eigenvectors remain tested. 35/35/1 row spaces; 1120/35840/32768 words; 117 address patterns. Zero two-target candidates. +2026-10-16T10:25:48Z freshness Continue with pinned scientific inputs after canonical-main refresh. Relevant instructions, priorities, selected result and both live mathematical inputs are unchanged. Main 475fec190d5ad746bd4690574dca30d6901acdaf; 491 open PRs, 2115 closed PRs, 1585 Discussion records; complete pagination, no warnings; PR2167 head unchanged. No conflicting clean-workspace completion identified; metadata coverage is not a novelty proof. +2026-10-16T10:30:36Z verification Retain the independently implemented reduced census. Normal/optimized replay and six real CLI test groups pass; actual grouping, skipped-census and strengthened-threshold mutants fail. 1223 Python vector-oracle words and 143091 relation cases; complete dimension-two cross-check; GCC14/Clang19 and ASan/UBSan output equality; 144 workflow tests pass. Exit predicate met within scope; no native supplier or selected-frontier change. +2026-10-16T10:31:42Z review Check proof coverage and implementation separately. Proof review checked clean-only endpoint normalization, coloop deletion, padding, noncube relations and arbitrary data eigenvectors; implementation review checked RREF coverage, rank-one updates, subset grouping and nonvacuous controls. README and all three code files inspected; Ruff correctness/bugbear/import/modernization checks pass after binding the sorting key's loop dimension. No unresolved local defect found. Higher-dimensional second full implementation, formal kernel and physical admission remain unrun. +2026-10-16T10:33:59Z submission Refresh current main and live overlap before publication. No relevant main/source change and no competing arbitrary-clean completion identified. Main remains 475fec190; 492 open PRs, 2115 closed PRs and 1585 Discussion records, complete pagination without warnings. Keep the original exact scientific pins; publish one additive package. diff --git a/research/bit-clean-workspace-compression/engine.cpp b/research/bit-clean-workspace-compression/engine.cpp new file mode 100644 index 0000000000..b9c0a46414 --- /dev/null +++ b/research/bit-clean-workspace-compression/engine.cpp @@ -0,0 +1,256 @@ +// Exact reduced clean-workspace census. Apache-2.0. Nick Petalas. +#include +#include +#include +#include +#include + +using Matrix = std::uint32_t; // Four rows, four bits each. +using Word = std::array; +struct Relation { + std::array representative{}; + std::array high_rank_possible{}; +}; +using Relations = std::array; +using Polynomial = std::array; + +void need(bool condition, const char* message) { + if (!condition) throw std::runtime_error(message); +} + +unsigned rank(Word columns) { + std::array basis{}; + unsigned result = 0; + for (unsigned value : columns) { + for (int bit = 3; bit >= 0; --bit) { + const auto index = static_cast(bit); + if (((value >> index) & 1U) == 0) continue; + if (basis[index] != 0) value ^= basis[index]; + else { basis[index] = value; ++result; break; } + } + } + return result; +} + +bool canonical_rows(unsigned encoded, unsigned dimension, Word& columns) { + std::array rows{}; + unsigned pivots = 0; + unsigned previous = 0; + for (unsigned i = 0; i < dimension; ++i) { + rows[i] = (encoded >> (5U * i)) & 31U; + if (rows[i] == 0) return false; + const unsigned pivot = static_cast(std::countr_zero(rows[i])); + if (i != 0 && pivot <= previous) return false; + previous = pivot; + pivots |= 1U << pivot; + } + for (unsigned i = 0; i < dimension; ++i) { + if (std::popcount(rows[i] & pivots) != 1) return false; + } + columns.fill(0); + for (unsigned j = 0; j < 5; ++j) { + for (unsigned i = 0; i < dimension; ++i) + columns[j] |= ((rows[i] >> j) & 1U) << i; + if (columns[j] == 0) return false; + } + for (unsigned j = 0; j < 5; ++j) { + Word removed = columns; + removed[j] = 0; + if (rank(removed) != dimension) return false; + } + return true; +} + +Relation make_relation(const std::array& direction) { + Relation result; + for (unsigned mask = 0; mask < 32; ++mask) { + result.representative[mask] = mask; + unsigned minimum_support = 5; + for (int lambda = -1; lambda <= 1; ++lambda) { + unsigned support = 0; + int other = 0; + bool binary = true; + for (unsigned j = 0; j < 5; ++j) { + const int entry = static_cast((mask >> j) & 1U) + + lambda * direction[j]; + support += static_cast(entry != 0); + if (entry < 0 || entry > 1) binary = false; + if (entry == 1) other |= 1 << j; + } + if (support < minimum_support) minimum_support = support; + if (binary && static_cast(other) < result.representative[mask]) + result.representative[mask] = static_cast(other); + } + result.high_rank_possible[mask] = minimum_support >= 3; + } + return result; +} + +Relations make_relations() { + Relations result; + result[0] = make_relation({0, 0, 0, 0, 0}); + unsigned count = 1; + for (unsigned code = 0; code < 243; ++code) { + unsigned rest = code; + std::array direction{}; + unsigned support = 0; + int first = 0; + for (unsigned j = 0; j < 5; ++j) { + direction[j] = static_cast(rest % 3U) - 1; + rest /= 3; + if (direction[j] == 0) continue; + ++support; + if (first == 0) first = direction[j]; + } + if (support < 2 || first != 1) continue; + need(count < result.size(), "too many relations"); + result[count++] = make_relation(direction); + } + need(count == result.size(), "missing relation"); + return result; +} + +Matrix left_rank_one(Matrix matrix, unsigned x, unsigned y) { + unsigned row = 0; + for (unsigned i = 0; i < 4; ++i) + if (((y >> i) & 1U) != 0) row ^= (matrix >> (4U * i)) & 15U; + Matrix result = 0; + for (unsigned i = 0; i < 4; ++i) + if (((x >> i) & 1U) != 0) result |= row << (4U * i); + return result; +} + +Polynomial expand(const Word& x, const Word& y, unsigned dimension) { + Polynomial result{}; + for (unsigned i = 0; i < dimension; ++i) result[0] |= 1U << (5U * i); + for (unsigned j = 0; j < 5; ++j) { + need((std::popcount(x[j] & y[j]) & 1) == 1, "nonidempotent call"); + for (unsigned mask = 0; mask < (1U << j); ++mask) { + const Matrix update = left_rank_one(result[mask], x[j], y[j]); + result[mask] ^= update; + result[mask | (1U << j)] = update; + } + } + return result; +} + +unsigned apply(Matrix matrix, unsigned vector) { + unsigned result = 0; + for (unsigned i = 0; i < 4; ++i) + result |= static_cast(std::popcount(((matrix >> (4U*i)) & 15U) + & vector) & 1) << i; + return result; +} + +// Return the unique monomial exponent, or 32 if this is not an eigenvector. +unsigned eigen_exponent(const Polynomial& grouped, unsigned vector) { + unsigned exponent = 32; + for (unsigned mask = 0; mask < 32; ++mask) { + const unsigned output = apply(grouped[mask], vector); + if (output == 0) continue; + if (output != vector || exponent != 32) return 32; + exponent = mask; + } + return exponent; +} + +struct Counts { + std::array histogram{}; + std::uint64_t monomial_vectors = 0; + std::uint64_t candidates = 0; +}; + +void inspect(const Polynomial& polynomial, unsigned dimension, + const Relations& relations, Counts& counts, bool probe) { + for (unsigned index = 0; index < relations.size(); ++index) { + const Relation& relation = relations[index]; + Polynomial grouped{}; + for (unsigned mask = 0; mask < 32; ++mask) + grouped[relation.representative[mask]] ^= polynomial[mask]; + unsigned high = 0; + if (probe) std::cout << "E " << index; + for (unsigned vector = 1; vector < (1U << dimension); ++vector) { + const unsigned exponent = eigen_exponent(grouped, vector); + if (exponent == 32) continue; + ++counts.monomial_vectors; + high += static_cast(relation.high_rank_possible[exponent]); + if (probe) std::cout << ' ' << vector << ':' << exponent; + } + if (probe) std::cout << '\n'; + ++counts.histogram[high]; + if (high >= 2) ++counts.candidates; + } +} + +void self_test(const Relations& relations) { + Polynomial positive{}; + positive[7] = 1U; // e0 is an eigenvector at a three-frame sum. + positive[25] = 1U << 5; // e1 is an independent such eigenvector. + need(eigen_exponent(positive, 1) == 7, "positive e0 rejected"); + need(eigen_exponent(positive, 2) == 25, "positive e1 rejected"); + need(eigen_exponent(positive, 3) == 32, "non-eigenvector accepted"); + need(relations[0].high_rank_possible[7], "rank-three support rejected"); + need(!relations[0].high_rank_possible[3], "rank-two support accepted"); + Counts counts; + inspect(positive, 2, relations, counts, false); + need(counts.candidates != 0, "acceptance branch not exercised"); + positive[25] ^= 1U; + need(eigen_exponent(positive, 1) == 32, "leaking vector accepted"); +} + +void census(unsigned dimension, const Relations& relations) { + std::uint64_t spaces = 0; + std::uint64_t words = 0; + Counts counts; + const unsigned choices = 1U << (dimension - 1U); + unsigned combinations = 1; + for (unsigned j = 0; j < 5; ++j) combinations *= choices; + for (unsigned encoded = 0; encoded < (1U << (5U * dimension)); ++encoded) { + Word x{}; + if (!canonical_rows(encoded, dimension, x)) continue; + ++spaces; + std::array, 5> allowed{}; + for (unsigned j = 0; j < 5; ++j) { + unsigned count = 0; + for (unsigned y = 1; y < (1U << dimension); ++y) + if ((std::popcount(x[j] & y) & 1) != 0) allowed[j][count++] = y; + need(count == choices, "wrong covector alphabet"); + } + for (unsigned code = 0; code < combinations; ++code) { + unsigned rest = code; + Word y{}; + for (unsigned j = 0; j < 5; ++j) { + y[j] = allowed[j][rest % choices]; + rest /= choices; + } + const bool probe = dimension == 2 || code == 0 || words % 997U == 0; + if (probe) { + std::cout << "P " << dimension; + for (unsigned value : x) std::cout << ' ' << value; + for (unsigned value : y) std::cout << ' ' << value; + std::cout << '\n'; + } + inspect(expand(x, y, dimension), dimension, relations, counts, probe); + ++words; + } + } + std::cout << "R " << dimension << ' ' << spaces << ' ' << words << ' ' + << counts.monomial_vectors << ' ' << counts.candidates; + for (auto value : counts.histogram) std::cout << ' ' << value; + std::cout << '\n'; + need(counts.candidates == 0, "candidate needs investigation"); +} + +int main() { + try { + const Relations relations = make_relations(); + self_test(relations); + for (unsigned dimension = 2; dimension <= 4; ++dimension) + census(dimension, relations); + std::cout << "PASS_CLEAN_REDUCED_CENSUS\n"; + return 0; + } catch (const std::exception& error) { + std::cerr << error.what() << '\n'; + return 1; + } +} diff --git a/research/bit-clean-workspace-compression/test_package.py b/research/bit-clean-workspace-compression/test_package.py new file mode 100644 index 0000000000..5027cf13c0 --- /dev/null +++ b/research/bit-clean-workspace-compression/test_package.py @@ -0,0 +1,91 @@ +#!/usr/bin/env python3 +"""Behavioral and implementation-mutation controls for the actual replay CLI.""" +from __future__ import annotations + +import hashlib +import json +import shutil +import subprocess +import sys +import tempfile +import unittest +from pathlib import Path + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parents[1] +EXPECTED = "PASS_CLEAN_WORKSPACE_COMPRESSION words=69728 candidates=0 no_new_kappa\n" + + +class ReplayTests(unittest.TestCase): + def setUp(self) -> None: + self.temporary = tempfile.TemporaryDirectory(prefix="clean replay controls ") + self.addCleanup(self.temporary.cleanup) + self.root = Path(self.temporary.name) + self.package = self.root / "research" / PACKAGE.name + shutil.copytree(PACKAGE, self.package, ignore=shutil.ignore_patterns("__pycache__")) + sources = json.loads((PACKAGE / "SOURCES.json").read_text()) + for source in sources["files"]: + if source["usage"] == "input": + destination = self.root / source["path"] + destination.parent.mkdir(parents=True, exist_ok=True) + shutil.copyfile(ROOT / source["path"], destination) + + def run_replay(self, optimized: bool = True, extra: tuple[str, ...] = ()) -> subprocess.CompletedProcess: + options = ["-I", "-B", "-W", "error"] + if optimized: + options.append("-O") + return subprocess.run([sys.executable, *options, str(self.package / "verify.py"), *extra], + cwd=self.root, capture_output=True, text=True, timeout=60, check=False) + + def rewrite_engine(self, old: str, new: str) -> None: + path = self.package / "engine.cpp" + contents = path.read_text() + self.assertEqual(contents.count(old), 1) + path.write_text(contents.replace(old, new)) + + def assert_rejected(self, run: subprocess.CompletedProcess, reason: str) -> None: + self.assertNotEqual(run.returncode, 0) + self.assertNotIn("PASS_CLEAN_WORKSPACE_COMPRESSION", run.stdout) + self.assertIn(reason, run.stderr) + + def test_normal_and_optimized_relocated_read_only(self) -> None: + before = {p.name: hashlib.sha256(p.read_bytes()).hexdigest() + for p in self.package.iterdir() if p.is_file()} + for optimized in (False, True): + with self.subTest(optimized=optimized): + run = self.run_replay(optimized) + self.assertEqual((run.returncode, run.stdout, run.stderr), (0, EXPECTED, "")) + after = {p.name: hashlib.sha256(p.read_bytes()).hexdigest() + for p in self.package.iterdir() if p.is_file()} + self.assertEqual(after, before) + + def test_receipt_corruption(self) -> None: + path = self.package / "RESULT.json" + path.write_text(path.read_text().replace('"oracle_probes": 1223', '"oracle_probes": 1224')) + self.assert_rejected(self.run_replay(), "receipt mismatch") + + def test_no_quotient_implementation_mutant(self) -> None: + self.rewrite_engine("grouped[relation.representative[mask]] ^= polynomial[mask];", + "grouped[mask] ^= polynomial[mask];") + self.assert_rejected(self.run_replay(), "independent eigenvector oracle mismatch") + + def test_vacuous_enumeration_implementation_mutant(self) -> None: + self.rewrite_engine("if (!canonical_rows(encoded, dimension, x)) continue;", + "if (!canonical_rows(encoded, dimension, x) || dimension >= 2) continue;") + self.assert_rejected(self.run_replay(), "missing oracle probe") + + def test_rank_threshold_implementation_mutant(self) -> None: + self.rewrite_engine("minimum_support >= 3", "minimum_support >= 4") + self.assert_rejected(self.run_replay(), "rank-three support rejected") + + def test_source_corruption_and_invalid_cli(self) -> None: + path = self.root / "research/bit-three-register-lower-bound/README.md" + path.write_bytes(path.read_bytes() + b"\nchanged\n") + self.assert_rejected(self.run_replay(), "source input changed") + run = self.run_replay(extra=("--not-an-option",)) + self.assertEqual(run.returncode, 2) + self.assertIn("unrecognized arguments", run.stderr) + + +if __name__ == "__main__": + unittest.main() diff --git a/research/bit-clean-workspace-compression/verify.py b/research/bit-clean-workspace-compression/verify.py new file mode 100644 index 0000000000..c520b817e8 --- /dev/null +++ b/research/bit-clean-workspace-compression/verify.py @@ -0,0 +1,283 @@ +#!/usr/bin/env python3 +"""Independent exact oracle and bounded native census. Apache-2.0.""" +from __future__ import annotations + +import argparse +import hashlib +import itertools +import json +import os +import shutil +import subprocess +import tempfile +from fractions import Fraction +from pathlib import Path + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parents[1] +FLAGS = ("-std=c++20", "-O3", "-Wall", "-Wextra", "-Wpedantic", + "-Wconversion", "-Wsign-conversion", "-Wshadow", "-Werror") + + +def need(condition: bool, message: str) -> None: + if not condition: + raise ValueError(message) + + +def xor_rank(vectors: list[int] | tuple[int, ...]) -> int: + basis: dict[int, int] = {} + for value in vectors: + for pivot in sorted(basis, reverse=True): + if value >> pivot & 1: + value ^= basis[pivot] + if value: + basis[value.bit_length() - 1] = value + return len(basis) + + +def row_basis(space: tuple[int, ...]) -> tuple[int, ...]: + rows = list(space[1:]) + used = 0 + for pivot in range(5): + selected = next((i for i in range(used, len(rows)) if rows[i] >> pivot & 1), None) + if selected is None: + continue + rows[used], rows[selected] = rows[selected], rows[used] + for i in range(len(rows)): + if i != used and rows[i] >> pivot & 1: + rows[i] ^= rows[used] + used += 1 + return tuple(rows[:used]) + + +def image_spaces() -> dict[int, list[tuple[int, ...]]]: + """Enumerate actual binary subspaces, not the engine's RREF bit strings.""" + current = {(0,)} + result: dict[int, list[tuple[int, ...]]] = {} + for dimension in range(1, 5): + following = set() + for space in current: + for vector in range(1, 32): + if vector not in space: + following.add(tuple(sorted(space + tuple(x ^ vector for x in space)))) + current = following + if dimension < 2: + continue + retained = [] + for space in sorted(current): + rows = row_basis(space) + columns = tuple(sum(((row >> j) & 1) << i for i, row in enumerate(rows)) + for j in range(5)) + if 0 in columns: + continue + if all(xor_rank(columns[:j] + columns[j + 1:]) == dimension for j in range(5)): + retained.append(columns) + def encoded(columns: tuple[int, ...], r: int = dimension) -> int: + return sum(sum(((columns[j] >> i) & 1) << j for j in range(5)) << (5*i) + for i in range(r)) + result[dimension] = sorted(retained, key=encoded) + need([len(result[r]) for r in (2, 3, 4)] == [35, 35, 1], "image-space count") + return result + + +def relation_directions() -> list[tuple[int, ...]]: + result = [(0,)*5] + for reverse in itertools.product((-1, 0, 1), repeat=5): + direction = reverse[::-1] + support = [value for value in direction if value] + if len(support) >= 2 and support[0] == 1: + result.append(direction) + need(len(result) == 117, "relation count") + return result + + +def quotient(exponent: tuple[int, ...], direction: tuple[int, ...]) -> tuple[int, ...]: + pivot = next((i for i in range(5) if direction[i]), None) + if pivot is None: + return exponent + # Rational elimination along a primitive relation, not subset-pair tables. + return tuple(exponent[i] - exponent[pivot] * direction[i] * direction[pivot] + for i in range(5)) + + +def propagate(x: tuple[int, ...], y: tuple[int, ...], vector: int) -> dict[tuple[int, ...], int]: + state = {(0,)*5: vector} + for j in range(5): + following = dict(state) + for exponent, value in state.items(): + if (value & y[j]).bit_count() % 2 == 0: + continue + shifted = tuple(exponent[i] + int(i == j) for i in range(5)) + following[exponent] = following.get(exponent, 0) ^ x[j] + following[shifted] = following.get(shifted, 0) ^ x[j] + state = {key: value for key, value in following.items() if value} + need(len(state) <= 32, "polynomial capacity") + return state + + +def oracle(dimension: int, x: tuple[int, ...], y: tuple[int, ...], + directions: list[tuple[int, ...]]) -> list[list[tuple[int, int]]]: + vectors = [propagate(x, y, v) for v in range(1, 1 << dimension)] + result = [] + for direction in directions: + representatives = {} + for mask in range(32): + exponent = tuple(mask >> j & 1 for j in range(5)) + representatives.setdefault(quotient(exponent, direction), mask) + eigenvectors = [] + for vector, state in enumerate(vectors, 1): + grouped: dict[tuple[int, ...], int] = {} + for exponent, value in state.items(): + key = quotient(exponent, direction) + grouped[key] = grouped.get(key, 0) ^ value + surviving = [(key, value) for key, value in grouped.items() if value] + if len(surviving) == 1 and surviving[0][1] == vector: + eigenvectors.append((vector, representatives[surviving[0][0]])) + result.append(eigenvectors) + return result + + +def expected_probes(spaces: dict[int, list[tuple[int, ...]]]) -> set[tuple[int, ...]]: + result = set() + for dimension, columns_list in spaces.items(): + index = 0 + for x in columns_list: + choices = [tuple(y for y in range(1, 1 << dimension) if (y & v).bit_count() % 2) + for v in x] + for reverse in itertools.product(*choices[::-1]): + y = reverse[::-1] + if dimension == 2 or index % 997 == 0 or y == tuple(c[0] for c in choices): + result.add((dimension,) + x + y) + index += 1 + return result + + +def high_possible(mask: int, direction: tuple[int, ...]) -> bool: + return min(sum((mask >> j & 1) + multiple*direction[j] != 0 for j in range(5)) + for multiple in range(-2, 3)) >= 3 + + +def verify_engine_output(output: str) -> dict: + spaces = image_spaces() + directions = relation_directions() + expected = expected_probes(spaces) + seen = set() + summaries = [] + lines = iter(output.splitlines()) + rank_two_histogram = [0]*16 + rank_two_monomials = 0 + footer = False + for line in lines: + fields = line.split() + if fields[0] == "P": + key = tuple(map(int, fields[1:])) + need(key in expected and key not in seen, "unexpected/repeated probe") + seen.add(key) + dimension, x, y = key[0], key[1:6], key[6:11] + for index, eigenvectors in enumerate(oracle(dimension, x, y, directions)): + record = next(lines).split() + actual = [tuple(map(int, pair.split(":"))) for pair in record[2:]] + need(record[:2] == ["E", str(index)] and actual == eigenvectors, + "independent eigenvector oracle mismatch") + if dimension == 2: + high = sum(high_possible(mask, directions[index]) for _, mask in eigenvectors) + rank_two_histogram[high] += 1 + rank_two_monomials += len(eigenvectors) + elif fields[0] == "R": + summaries.append(list(map(int, fields[1:]))) + else: + need(line == "PASS_CLEAN_REDUCED_CENSUS" and not footer, "unexpected engine record") + footer = True + need(seen == expected, "missing oracle probe") + need(footer, "missing engine footer") + need(len(summaries) == 3, "missing census summary") + for dimension, summary in zip((2, 3, 4), summaries, strict=True): + need(len(summary) == 21 and summary[0] == dimension, "summary shape") + expected_words = len(spaces[dimension]) * (1 << (dimension-1))**5 + need(summary[1:3] == [len(spaces[dimension]), expected_words], "census coverage") + need(summary[4] == 0 and sum(summary[5:]) == expected_words*117, "candidate/coverage") + need(summaries[0][3] == rank_two_monomials, "independent full rank-two count") + need(summaries[0][5:] == rank_two_histogram, "independent full rank-two histogram") + records = [{"image_dimension": row[0], "image_spaces": row[1], + "words": row[2], "monomial_vectors": row[3], + "candidate_cases": row[4], "high_rank_vector_histogram": row[5:]} + for row in summaries] + return {"summaries": records, "oracle_probes": len(seen), + "oracle_relations": len(seen)*117, "relation_patterns": 117} + + +def physical_apply(calls: list[tuple[int, int, tuple[int | Fraction, ...]]], vector: int) -> dict: + state = {(0,)*9: vector} + need(len(calls) <= 7, "fixture call capacity") + for x, y, frame in calls: + following = dict(state) + for exponent, value in state.items(): + if (value & y).bit_count() % 2: + shifted = tuple(a+b for a, b in zip(exponent, frame, strict=True)) + following[exponent] = following.get(exponent, 0) ^ x + following[shifted] = following.get(shifted, 0) ^ x + state = {key: value for key, value in following.items() if value} + return state + + +def fixture_controls() -> dict: + frames = [tuple(int(j == 3*i+i) for j in range(9)) for i in range(3)] + identity = (1, 0, 0, 0, 1, 0, 0, 0, 1) + other = (Fraction(1, 2), 0, 0, Fraction(1, 3), -1, 0, + 2, Fraction(1, 4), Fraction(3, 2)) + columns = [tuple(value if j % 3 == column else 0 for j, value in enumerate(other)) + for column in range(3)] + direct = [(1, 1, frame) for frame in frames] + [(2, 2, frame) for frame in columns] + target = [{identity: 1}, {other: 2}] + need([physical_apply(direct, v) for v in (1, 2)] == target, "six-call fixture") + need([physical_apply(direct[:-1], v) for v in (1, 2)] != target, "omission control") + borrowed = direct[:2] + [(16, 16, frames[0])] + direct[2:] + need([physical_apply(borrowed, v) for v in (1, 2)] == target, "coloop deletion") + need(physical_apply(borrowed, 16) != physical_apply(direct, 16), "clean-only distinction") + # A rank-one target permits an active coloop: the lemma must exclude it. + clean_only = [(1, 3, frames[0])] + need(physical_apply(clean_only, 1) == {frames[0]: 1}, "rank-one clean endpoint") + need(physical_apply(clean_only, 2) != {(0,)*9: 2}, "unconstrained clean column") + need(physical_apply([], 1) != physical_apply(clean_only, 1), "active coloop boundary") + return {"six_call_positive": True, "omission_rejected": True, + "removable_clean_coloop": True, "rank_one_boundary": True} + + +def check_sources() -> None: + sources = json.loads((PACKAGE / "SOURCES.json").read_text()) + for source in sources["files"]: + if source["usage"] == "input": + digest = hashlib.sha256((ROOT / source["path"]).read_bytes()).hexdigest() + need(digest == source["sha256"], "source input changed: " + source["path"]) + + +def run_census() -> dict: + compiler = shutil.which(os.environ.get("CXX", "c++")) + need(compiler is not None, "a C++20 compiler is required") + with tempfile.TemporaryDirectory(prefix="clean-workspace-") as work: + executable = Path(work) / "census" + build = subprocess.run([compiler, *FLAGS, str(PACKAGE / "engine.cpp"), "-o", str(executable)], + text=True, capture_output=True, timeout=60, check=False) + need(build.returncode == 0 and not build.stderr, "compiler failed: " + build.stderr) + run = subprocess.run([str(executable)], text=True, capture_output=True, timeout=60, check=False) + need(run.returncode == 0 and not run.stderr, "engine failed: " + run.stderr) + need(len(run.stdout) <= 2_000_000, "engine output capacity") + return verify_engine_output(run.stdout) + + +def main() -> None: + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--write", action="store_true", help="regenerate only RESULT.json") + arguments = parser.parse_args() + check_sources() + result = {"schema_version": 1, "census": run_census(), "controls": fixture_controls()} + receipt = PACKAGE / "RESULT.json" + if arguments.write: + receipt.write_text(json.dumps(result, indent=2) + "\n") + else: + need(receipt.read_text() == json.dumps(result, indent=2) + "\n", "receipt mismatch") + print("PASS_CLEAN_WORKSPACE_COMPRESSION words=69728 candidates=0 no_new_kappa") + + +if __name__ == "__main__": + main()