From f3aa403e18577c66c4aedd4b0a2ef0e477eb3626 Mon Sep 17 00:00:00 2001 From: JoyboyBrian <122925040+JoyboyBrian@users.noreply.github.com> Date: Thu, 22 Oct 2026 23:16:10 -0700 Subject: [PATCH 1/3] Prove and compile the clean square-zero reflection optimum --- research/clean-square-zero-compiler/PROOF.md | 138 +++++++++ research/clean-square-zero-compiler/README.md | 89 ++++++ .../clean-square-zero-compiler/RESULT.json | 190 ++++++++++++ .../clean-square-zero-compiler/SOURCES.json | 30 ++ research/clean-square-zero-compiler/TASK.json | 70 +++++ .../clean-square-zero-compiler/VERIFY.json | 37 +++ research/clean-square-zero-compiler/verify.py | 287 ++++++++++++++++++ 7 files changed, 841 insertions(+) create mode 100644 research/clean-square-zero-compiler/PROOF.md create mode 100644 research/clean-square-zero-compiler/README.md create mode 100644 research/clean-square-zero-compiler/RESULT.json create mode 100644 research/clean-square-zero-compiler/SOURCES.json create mode 100644 research/clean-square-zero-compiler/TASK.json create mode 100644 research/clean-square-zero-compiler/VERIFY.json create mode 100644 research/clean-square-zero-compiler/verify.py diff --git a/research/clean-square-zero-compiler/PROOF.md b/research/clean-square-zero-compiler/PROOF.md new file mode 100644 index 0000000000..3eaec47c2c --- /dev/null +++ b/research/clean-square-zero-compiler/PROOF.md @@ -0,0 +1,138 @@ +# One returned clean role changes the exact projector-call minimum + +JoyboyBrian, with substantial OpenAI Codex assistance. Apache-2.0. + +## Exact scope + +Let N be any binary square-zero matrix of positive rank q on d arbitrary +data roles. Work coefficientwise over F2[C2], with one fixed nonidentity +involution g and t=1+[g], so t is nonzero and t²=0. Each paid call is +I+t xy^T with y^T x=1; every such coupling has binary rank one and is +idempotent. Constant binary invertible role maps are free and may be +interspersed. Any finite number of dirty helpers must be restored on every +input. Any finite number of clean helpers begin and end at zero. The data +endpoint is I+tN, with no output in any clean role on the active columns. + +**Theorem.** The minimum number of paid calls is q+1. At positive even q, +one clean role suffices and saves one reflection against Nick Petalas's +dirty-workspace optimum q+2 in PR4912. At odd q his q+1 construction already +attains the clean minimum. The zero coupling costs zero. + +This changes the workspace contract; it does not contradict the dirty +theorem. The clean role is an entire zero function of the address, not one +sample bit. A native source of this resource and its price are not provided. + +## 1. Lower bound with unrestricted finite workspace + +Include all dirty helpers among the d active roles, padding N by zero. +Let E embed these roles into the full active-plus-clean space. Commute all +free scalar maps to the input side, conjugating paid projectors. The word +has form P S, where P is a product of paid calls. Augmentation t->0 of +the required active columns gives S E=E. Consequently + + P E = E + t E N. + +The inherited product identity of ywz65 PR2716 gives P=I+t sum_j x_j y_j^T. +Comparing the [g] coefficient gives sum_j x_j y_j^T E=E N. This is only a +column equation: no identity on the initially clean input columns is assumed. +It implies k>=q by rank subadditivity. + +Suppose k=q. Put X=(x_1,...,x_q), Y with rows y_j^T, and V=Y E. +Then X V=E N has rank q, so X is injective and V is surjective. Its image is +exactly im(E N), which lies in the active subspace. Thus X=E X0 and +X0 V=N. Since N²=0, multiplication by a left inverse of X0 and right inverse +of V gives V X0=0. But diagonal entry j of this product equals +y_j^T E X0[:,j]=y_j^T x_j=1, a contradiction. Hence k>=q+1. + +This proof permits arbitrary many clean and dirty roles, arbitrary free +scalar mixing, and any call order. It uses no finite census or trace +constraint on unused clean input columns. Imposing such a trace constraint +would incorrectly reintroduce the predecessor's dirty parity obstruction. + +## 2. Explicit even-rank construction + +Choose binary chain coordinates e_i,f_i for 1<=i<=q so N=Σ e_i f_i^T; +any remaining data coordinates are killed by N. Existence follows from +im N contained in ker N: choose an image basis e_i and preimages f_i, +then complete by kernel vectors. Keep all original data arbitrary. + +Let h be one additional clean coordinate, and assume q>0 is even. Set + + x_i = e_i+h, y_i^T = Σ_(k≠i) f_k^T+h^T (1<=i<=q), + x_* = Σ_i e_i+h, y_*^T = Σ_i f_i^T+h^T. + +Every pairing y_j^T x_j=1 through the h coordinate; therefore these q+1 +couplings are legal rank-one idempotents. Summing their outer products gives + + Σ_j x_j y_j^T = N + h h^T. + +Indeed the image e_i has coefficient (Σ_(k≠i)f_k^T)+(Σ_k f_k^T)=f_i^T; +its h coefficient cancels. In the h row each f_k occurs q times, hence +cancels, while h^T occurs q+1 times and survives. All other rows are zero. +The full formal product is consequently + + I+t(N+h h^T) = (I+tN) direct-sum [g]. + +On every arbitrary data input the clean output is zero. Its full auxiliary +input action is [g], so a dirty helper does NOT meet the same contract. +The construction neither erases dirty data nor assumes a zero data register. +It remains exact in every order because t²=0. + +At q=2 the three pairs are + + (e1+h, f2^T+h^T), (e2+h, f1^T+h^T), + (e1+e2+h, f1^T+f2^T+h^T). + +For odd q use the predecessor's projectors e_i(Σ_k e_k^T+f_i^T) +and (Σ_i e_i)(Σ_i e_i^T). Their q+1 sum is N. That odd-rank identity, +the dirty optimum, normal-form background and involution-product identity +retain their original credit; the clean theorem and even construction are +the contribution here. + +## 3. Literal coordinate lowering and complete local comparison + +To implement an idempotent xy^T choose any pivot p with x_p=y_p=1. +Define the binary scalar involutions + + B=I+(x+e_p)e_p^T, A=I+e_p(y^T+e_p^T), S=B A. + +Then S e_p=x and e_p^T S^-1=y^T because y^T x=1. A coordinate reflection +D_p=I+t e_p e_p^T therefore obeys S D_p S^-1=I+t xy^T. The chronological +literal word is B, A, D_p, A, B. Each B is exactly wt(x)-1 CNOTs, and each +A is exactly wt(y)-1 CNOTs. All inverse scalar work is included. No dense +XOR or bulk basis change is billed as one CNOT. + +For the even clean word choose p=h. The first q projectors each need 2q +scalar CNOTs; the last needs 4q. Total: q+1 coordinate reflections and +2q(q+2) CNOTs. For an odd rank r the displayed predecessor word lowers to +r+1 reflections and 2r²+4r-4 CNOTs. Applying it on blocks q-1 and one gives +the positive-even dirty baseline q+2 reflections and 2q²-4 CNOTs. + +Thus, at stationary complete coordinate-reflection price R, scalar-CNOT +price C and additional clean-resource charge H>=0, the explicit clean word +beats this explicit dirty compiler exactly when + + R > 4(q+1) C + H. + +At rank two the comparison is 3R+16C+H against 4R+4C. Equality ties. +This is an exact comparison of two specified words, not a scalar-network +optimum or a claimed physical improvement. Adjacent inverse operations or +other lowerings could improve either baseline; they are not optimized here. + +For a general N=T N0 T^-1, conjugate either complete word by T on the data +and identity on h. The verifier emits T^-1 and T as literal row-elimination +CNOT networks, using three CNOTs per row swap. The same transport cost +2 tau(T) C is paid on both sides and cancels in the displayed comparison. +This does not assert that arbitrary T is physically local or free. Any +nonstationary frame, tape, scalar or clean-resource tariff needs a new invoice. + +## Proof versus corroboration + +The all-q statement is the written rank argument and construction. The finite +verifier independently sums projectors, checks arbitrary square-zero matrices +through four data roles, and checks conjugated ranks through eight. Its +clean-column two-call search allows arbitrary projectors on all five roles. +A separate literal interpreter applies one CNOT or one address swap at a +time to every faithful input basis column. These are reproducible finite +corroborations, not independent human or proof-kernel verification. No native +supplier, recursive price, multiplication theorem or new kappa follows. diff --git a/research/clean-square-zero-compiler/README.md b/research/clean-square-zero-compiler/README.md new file mode 100644 index 0000000000..67c8c1b4ab --- /dev/null +++ b/research/clean-square-zero-compiler/README.md @@ -0,0 +1,89 @@ +# Clean scratch lowers the square-zero compilation minimum + +For every nonzero square-zero binary coupling N of rank q, the exact paid +reflection-call minimum with returned clean workspace is **q+1**. One clean +role attains the new even-rank result; at rank two it uses three calls, +versus the exact dirty-workspace minimum four of Nick Petalas's PR4912. +Odd ranks retain his q+1 construction. The lower bound covers arbitrary +finite clean and restored dirty workspace and free binary scalar mixing. + +The complete endpoint is checked coefficientwise in F2[C2], with one fixed +nonidentity involution g. A paid call has a binary rank-one idempotent +coupling. The clean role is initialized and returned to the zero address +function; using a dirty role in its place fails. [PROOF.md](PROOF.md) states +the uniform theorem and every boundary assumption. + +This package also emits a literal coordinate-reflection/CNOT program, +including all inverse scalar work and common basis transport. At even q, +the new canonical word costs (q+1)R+2q(q+2)C+H, compared with +(q+2)R+(2q²-4)C for the explicitly lowered predecessor split compiler. +It wins precisely when R>4(q+1)C+H. In particular rank two is +3R+16C+H versus 4R+4C. R and C must be complete stationary primitive prices; +H is the additional clean-resource reservation/return charge. A saved formal +reflection does not establish a lower native total price. + +## Reproduce and exact scope + +Python 3.12 or newer, standard library only: + +```sh +python3 -I -W error -B research/clean-square-zero-compiler/verify.py +python3 -I -O -W error -B research/clean-square-zero-compiler/verify.py +python3 -B scripts/research_package.py --package research/clean-square-zero-compiler +``` + +`verify.py --write` regenerates only RESULT.json. Normal verification writes +nothing and compares the exact typed canonical scientific receipt. Every +proof-relevant live source is pinned in SOURCES.json and VERIFY.json. The +package does not import or execute predecessor code or re-run their census. + +The scientific checks cover all square-zero binary matrices through four +data roles, conjugated ranks one through eight with extra dirty spectators, +all clean-column one/two-call obstructions for the first rank-one/two +fixtures, literal scalar counts through even rank sixteen, and invalid +matrix/zero-coupling boundaries. The uniform theorem is not inferred from +these finite domains. Additional literal action and mutation checks are +described by their registered command and emitted report. + +Only this isolated opt-in package changes. Frozen predecessors, selected +sources and selected κ=0.00302015 remain unchanged. Native reflection +implementation, clean-resource availability, nonstationary routing/frames, +physical tapes, scalar network optimality, recursive supplier admission, +Lean, Docker and the full selected cold replay are unrun and unclaimed. + +## Overlap, sources and credit + +The changed premise is precisely the clean-workspace case excluded by +[PR4912](https://github.com/CrocSwap/integer-mult-bounds/pull/4912), retained +head eaea286b055724895adb4ca949b5ac0495be5ff8. Its dirty minimum, odd-rank +construction and q-1 plus one even-rank split retain Nick Petalas's credit. +ywz65 PR2716 supplies the product identity and arbitrary-coupling motivation. +Adam Gall PR1911, eumemic PR288, Ali Romman PR468, woklerx PR1443, Gareth +Davidson PR1333, Arham Tahir PR1589 and Cinna Davis PR2290 retain their +register-model lineage credit. Matrix rank, square-zero normal form and +elementary conjugation are standard background; no literature-priority +claim is made for them. + +At the initial fresh main bee95ce88f9f19802f0613f92838895cd0e14a1f checkpoint, +shared overlap searched 310 open PRs (06:05:59 UTC), 4096 Discussion records +(06:06:48 UTC) and all 6690 main package notes on 2026-10-23. The scoped +square-zero/clean query returned twelve related leads and no same minimum. +Live PR4912 head/body/comments and current handoffs were read. Cached text, +arbitrary diffs, omitted history and unpublished work remain limits; no +novelty guarantee follows. Later publication refresh is recorded in the PR. + +JoyboyBrian, with substantial OpenAI Codex assistance in proof, compiler, +independent checks and packaging. Apache-2.0. Independent human and formal +proof-kernel review are unclaimed. + +## Open next questions + +1. Can a literal native caller supply one returned clean role at a complete +price H and satisfy R>4(q+1)C+H? Start at rank two and bind all four data +roles, zero template reservation and coordinate reflection to actual source +operations. A native supplier and complete physical invoice are blockers. +2. Can sharing adjacent scalar conjugators improve the matched comparison? +Start with the two explicit rank-two primitive streams and optimize both, +preserving every arbitrary data column and the clean return. No claim of +scalar-network optimality justifies assuming either side already minimal. +Structured questions are in TASK.json; no construction expansion is claimed. diff --git a/research/clean-square-zero-compiler/RESULT.json b/research/clean-square-zero-compiler/RESULT.json new file mode 100644 index 0000000000..2265dfaf02 --- /dev/null +++ b/research/clean-square-zero-compiler/RESULT.json @@ -0,0 +1,190 @@ +{ + "boundary_controls": 6, + "larger": { + "conjugated_cases": 8, + "words": [ + { + "clean_roles": 1, + "common_transport_cnots": 12, + "data_roles": 4, + "rank": 1, + "reflections": 2, + "scalar_cnots": 14 + }, + { + "clean_roles": 1, + "common_transport_cnots": 46, + "data_roles": 6, + "rank": 2, + "reflections": 3, + "scalar_cnots": 62 + }, + { + "clean_roles": 1, + "common_transport_cnots": 60, + "data_roles": 8, + "rank": 3, + "reflections": 4, + "scalar_cnots": 86 + }, + { + "clean_roles": 1, + "common_transport_cnots": 88, + "data_roles": 10, + "rank": 4, + "reflections": 5, + "scalar_cnots": 136 + }, + { + "clean_roles": 1, + "common_transport_cnots": 178, + "data_roles": 12, + "rank": 5, + "reflections": 6, + "scalar_cnots": 244 + }, + { + "clean_roles": 1, + "common_transport_cnots": 198, + "data_roles": 14, + "rank": 6, + "reflections": 7, + "scalar_cnots": 294 + }, + { + "clean_roles": 1, + "common_transport_cnots": 238, + "data_roles": 16, + "rank": 7, + "reflections": 8, + "scalar_cnots": 360 + }, + { + "clean_roles": 1, + "common_transport_cnots": 248, + "data_roles": 18, + "rank": 8, + "reflections": 9, + "scalar_cnots": 408 + } + ] + }, + "shortest_clean_columns": [ + { + "all_projected_single_calls": 19, + "rank": 1, + "shorter_than": 2 + }, + { + "all_projected_single_calls": 361, + "rank": 2, + "shorter_than": 3 + } + ], + "small": { + "matrices": 343, + "ranks": { + "0": 4, + "1": 129, + "2": 210 + } + }, + "tariffs": [ + { + "clean": [ + 3, + 16 + ], + "dirty": [ + 4, + 4 + ], + "extra_cnots": 12, + "rank": 2 + }, + { + "clean": [ + 5, + 48 + ], + "dirty": [ + 6, + 28 + ], + "extra_cnots": 20, + "rank": 4 + }, + { + "clean": [ + 7, + 96 + ], + "dirty": [ + 8, + 68 + ], + "extra_cnots": 28, + "rank": 6 + }, + { + "clean": [ + 9, + 160 + ], + "dirty": [ + 10, + 124 + ], + "extra_cnots": 36, + "rank": 8 + }, + { + "clean": [ + 11, + 240 + ], + "dirty": [ + 12, + 196 + ], + "extra_cnots": 44, + "rank": 10 + }, + { + "clean": [ + 13, + 336 + ], + "dirty": [ + 14, + 284 + ], + "extra_cnots": 52, + "rank": 12 + }, + { + "clean": [ + 15, + 448 + ], + "dirty": [ + 16, + 388 + ], + "extra_cnots": 60, + "rank": 14 + }, + { + "clean": [ + 17, + 576 + ], + "dirty": [ + 18, + 508 + ], + "extra_cnots": 68, + "rank": 16 + } + ] +} diff --git a/research/clean-square-zero-compiler/SOURCES.json b/research/clean-square-zero-compiler/SOURCES.json new file mode 100644 index 0000000000..56f86bc850 --- /dev/null +++ b/research/clean-square-zero-compiler/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "bee95ce88f9f19802f0613f92838895cd0e14a1f", + "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/dihedral-arbitrary-couplings/README.md", + "usage": "input", + "git_blob": "66027d2a8856d931e7b1c8fa9811a65196d01637", + "sha256": "17bc49fd6215c155aacb0e4a8ce4a8e33e83226b8a1b937a638256a39b99f8ee" + }, + { + "path": "research/square-zero-idempotent-compiler/PROOF.md", + "usage": "input", + "git_blob": "7b14aa9c1f2f2a0f24e2f777fc2f4b054e07a652", + "sha256": "f5b162de16f22e5b47400424d70f55d9dc60211920fcfe1b2d78e3eb2bad6b8b" + } + ] +} diff --git a/research/clean-square-zero-compiler/TASK.json b/research/clean-square-zero-compiler/TASK.json new file mode 100644 index 0000000000..91b03f9f72 --- /dev/null +++ b/research/clean-square-zero-compiler/TASK.json @@ -0,0 +1,70 @@ +{ + "schema_version": 1, + "task_id": "bit-new-register-model", + "priority_revision": 7, + "base_commit": "bee95ce88f9f19802f0613f92838895cd0e14a1f", + "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": "Exact q+1 reflection minimum for every rank-q square-zero binary coupling with returned clean workspace, literal scalar lowering and matched complete-price comparison.", + "scope_change_reason": "Replace the card operation-family search by a changed workspace contract explicitly excluded by PR4912, retaining its original idempotent alphabet and predecessor credit.", + "bottleneck_link": "One saved reflection at even rank matters only if its complete price exceeds added scalar work and clean reservation; no native admission follows.", + "budget_minutes": 60, + "stop_rule": "Stop at the first uniform theorem, literal lowering, independent finite corroboration and corruption controls; do not expand into a native construction without its full resource contract.", + "outcome": "completed", + "evidence": "PROOF.md gives the uniform argument; verify.py checks new clean-column endpoints, first-fixture shortest sums and literal tariff counts.", + "author": "JoyboyBrian", + "ai_assistance": "Substantial OpenAI Codex assistance. Independent human and formal proof-kernel review unclaimed.", + "open_questions": [ + { + "question": "Can a literal native caller satisfy the complete clean-versus-dirty price inequality?", + "why_it_matters": "Saving a reflection alone may cost more scalar and clean-resource work.", + "first_step": "Bind rank-two R,C,H to one actual four-data-role caller and its returned zero template.", + "blocked_by": "Native reflection and clean-resource implementation/invoice unknown." + }, + { + "question": "Can adjacent scalar conjugators improve the two matched literal words?", + "why_it_matters": "The comparison is exact for specified streams, not globally scalar-optimal.", + "first_step": "Optimize both rank-two streams under their exact data/clean return contracts.", + "blocked_by": "An equally charged physical primitive model must be fixed." + } + ] +} diff --git a/research/clean-square-zero-compiler/VERIFY.json b/research/clean-square-zero-compiler/VERIFY.json new file mode 100644 index 0000000000..c28f4110c5 --- /dev/null +++ b/research/clean-square-zero-compiler/VERIFY.json @@ -0,0 +1,37 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/dihedral-arbitrary-couplings/README.md", + "research/square-zero-idempotent-compiler/PROOF.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Uniform construction corroboration, arbitrary square-zero data contracts, clean-column shortest sums, exact scalar tariff and invalid-input controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Same checks with assertions disabled." + } + ] +} diff --git a/research/clean-square-zero-compiler/verify.py b/research/clean-square-zero-compiler/verify.py new file mode 100644 index 0000000000..7eb3732b7a --- /dev/null +++ b/research/clean-square-zero-compiler/verify.py @@ -0,0 +1,287 @@ +"""Clean square-zero compiler. JoyboyBrian, with OpenAI Codex; Apache-2.0.""" +import argparse +import hashlib +import json +import random +from pathlib import Path + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def parity(value): + return value.bit_count() & 1 + + +def rank(vectors): + basis = {} + for value in vectors: + while value: + bit = value.bit_length() - 1 + if bit not in basis: + basis[bit] = value + break + value ^= basis[bit] + return len(basis) + + +def apply(matrix, vector): + return sum(parity(row & vector) << i for i, row in enumerate(matrix)) + + +def columns(matrix): + return tuple(apply(matrix, 1 << i) for i in range(len(matrix))) + + +def transpose(vectors): + return tuple(sum(((value >> i) & 1) << j for j, value in enumerate(vectors)) + for i in range(len(vectors))) + + +def matrix_product(left, right): + return transpose(tuple(apply(left, col) for col in columns(right))) + + +def matrix_input(matrix): + need(isinstance(matrix, (tuple, list)), 'matrix container') + n = len(matrix) + need(1 <= n <= 32, 'verifier matrix width must be 1..32') + need(all(type(row) is int and 0 <= row < (1 << n) for row in matrix), + 'binary row encoding') + need(all(apply(matrix, col) == 0 for col in columns(matrix)), + 'matrix is not square-zero') + + +def chain_basis(matrix): + image, preimages, kernel, elimination = [], [], [], {} + for j, col in enumerate(columns(matrix)): + value, pre = col, 1 << j + while value: + bit = value.bit_length() - 1 + if bit not in elimination: + elimination[bit] = (value, pre) + image.append(col) + preimages.append(1 << j) + break + other, label = elimination[bit] + value ^= other + pre ^= label + if not value: + kernel.append(pre) + q = len(image) + basis = image + preimages + need(rank(basis) == 2 * q, 'chain independence') + for vector in kernel: + if rank(basis + [vector]) > len(basis): + basis.append(vector) + need(len(basis) == len(matrix), 'complete chain basis') + return q, transpose(tuple(basis)) + + +def reduce_basis(matrix): + """Return literal scalar CNOTs whose product is matrix inverse.""" + rows, gates = list(matrix), [] + for j in range(len(rows)): + pivot = next((i for i in range(j, len(rows)) if rows[i] & (1 << j)), None) + need(pivot is not None, 'singular basis') + if pivot != j: + for dest, source in ((j, pivot), (pivot, j), (j, pivot)): + rows[dest] ^= rows[source] + gates.append(('xor', dest, source)) + for i in range(len(rows)): + if i != j and rows[i] & (1 << j): + rows[i] ^= rows[j] + gates.append(('xor', i, j)) + need(rows == [1 << i for i in range(len(rows))], 'basis reduction') + return gates + + +def odd_projectors(indices, q): + mask = sum(1 << i for i in indices) + result = [(1 << i, mask | (1 << (q + i)), i) for i in indices] + result.append((mask, mask, indices[0])) + return result + + +def canonical_projectors(q, n, clean=True): + if q == 0: + return [] + if q & 1: + return odd_projectors(list(range(q)), q) + if not clean: + return odd_projectors(list(range(q - 1)), q) + odd_projectors([q - 1], q) + h = 1 << n + sources = ((1 << q) - 1) << q + result = [((1 << i) | h, (sources ^ (1 << (q + i))) | h, n) + for i in range(q)] + result.append((((1 << q) - 1) | h, sources | h, n)) + return result + + +def projector_sum(projectors, width): + rows = [0] * width + for x, y, pivot in projectors: + need(x and y and parity(x & y) == 1, 'non-idempotent call') + need(((x & y) >> pivot) & 1, 'invalid reflection pivot') + for i in range(width): + if x & (1 << i): + rows[i] ^= y + return tuple(rows) + + +def lower_projectors(projectors, width): + gates = [] + for x, y, pivot in projectors: + need(parity(x & y) == 1 and ((x & y) >> pivot) & 1, 'lowering contract') + b = [('xor', i, pivot) for i in range(width) if i != pivot and x & (1 << i)] + a = [('xor', pivot, i) for i in range(width) if i != pivot and y & (1 << i)] + gates.extend(b + a + [('reflect', pivot)] + list(reversed(a)) + list(reversed(b))) + return gates + + +def compile_matrix(matrix): + matrix_input(matrix) + n = len(matrix) + q, basis = chain_basis(matrix) + changes = reduce_basis(basis) + projectors = canonical_projectors(q, n) + # shortcut: verifier emits finite-width words; the uniform proof is in PROOF.md. + gates = changes + lower_projectors(projectors, n + 1) + list(reversed(changes)) + return q, basis, projectors, gates, len(changes) + + +def check_matrix(matrix): + q, basis, projectors, gates, transport = compile_matrix(matrix) + n = len(matrix) + canonical = tuple((1 << (q + i)) if i < q else 0 for i in range(n)) + need(matrix_product(matrix, basis) == matrix_product(basis, canonical), + 'source-bound chain similarity') + expected = canonical + ((1 << n) if q and not q & 1 else 0,) + need(projector_sum(projectors, n + 1) == expected, 'full canonical formal endpoint') + need(len(projectors) == (q + 1 if q else 0), 'clean reflection count') + return q, gates, transport + + +def shortest_clean_checks(): + reports = [] + for q in (1, 2): + data, width = 2 * q, 2 * q + 1 + endpoints = set() + for x in range(1, 1 << width): + for y in range(1 << width): + if parity(x & y): + value = sum(((y & ((1 << data) - 1)) if x >> i & 1 else 0) + << (data * i) for i in range(width)) + endpoints.add(value) + target = sum((1 << (q + i)) << (data * i) for i in range(q)) + need(target not in endpoints, 'one-call clean obstruction') + if q == 2: + need(not any((target ^ p) in endpoints for p in endpoints), + 'two-call clean obstruction') + reports.append({'rank': q, 'all_projected_single_calls': len(endpoints), + 'shorter_than': q + 1}) + return reports + + +def all_small_matrices(): + count = 0 + by_rank = {} + for n in range(1, 5): + for bits in range(1 << (n * n)): + matrix = tuple((bits >> (n * i)) & ((1 << n) - 1) for i in range(n)) + if any(apply(matrix, col) for col in columns(matrix)): + continue + q, _, _ = check_matrix(matrix) + count += 1 + by_rank[str(q)] = by_rank.get(str(q), 0) + 1 + return {'matrices': count, 'ranks': by_rank} + + +def larger_matrices(): + cases, rows = 0, [] + for q in range(1, 9): + n = 2 * q + 2 + base = tuple((1 << (q + i)) if i < q else 0 for i in range(n)) + transform = [1 << i for i in range(n)] + rng = random.Random(900 + q) + for _ in range(n * 5): + dest, source = rng.sample(range(n), 2) + transform[dest] ^= transform[source] + reduction = reduce_basis(tuple(transform)) + inverse = [1 << i for i in range(n)] + for _, dest, source in reduction: + inverse[dest] ^= inverse[source] + matrix = matrix_product(matrix_product(tuple(transform), base), tuple(inverse)) + actual_q, word, transport = check_matrix(matrix) + need(actual_q == q, 'conjugated rank') + rows.append({'rank': q, 'data_roles': n, 'clean_roles': 1, + 'reflections': q + 1, 'scalar_cnots': len(word) - q - 1, + 'common_transport_cnots': 2 * transport}) + cases += 1 + return {'conjugated_cases': cases, 'words': rows} + + +def tariff_checks(): + result = [] + for q in range(2, 18, 2): + new = lower_projectors(canonical_projectors(q, 2 * q), 2 * q + 1) + old = lower_projectors(canonical_projectors(q, 2 * q, False), 2 * q + 1) + new_cnot = sum(g[0] == 'xor' for g in new) + old_cnot = sum(g[0] == 'xor' for g in old) + need(new_cnot == 2 * q * (q + 2), 'clean scalar tariff') + need(old_cnot == 2 * q * q - 4, 'dirty scalar tariff') + need(new_cnot - old_cnot == 4 * (q + 1), 'full comparison') + result.append({'rank': q, 'clean': [q + 1, new_cnot], + 'dirty': [q + 2, old_cnot], 'extra_cnots': 4 * (q + 1)}) + return result + + +def reject_controls(): + bad = [(True,), (2,), (1,), (), (0, -1)] + for matrix in bad: + try: + compile_matrix(matrix) + except ValueError: + pass + else: + raise ValueError('invalid input accepted') + need(compile_matrix((0,))[3] == [], 'zero needs no paid work') + return len(bad) + 1 + + +def authenticate(): + package = Path(__file__).resolve().parent + root = package.parent.parent + manifest = json.loads((package / 'SOURCES.json').read_text()) + sources = {} + for item in manifest['files']: + if item['usage'] == 'input': + data = (root / item['path']).read_bytes() + need(hashlib.sha256(data).hexdigest() == item['sha256'], 'source SHA256') + need(hashlib.sha1(b'blob ' + str(len(data)).encode() + b'\0' + data).hexdigest() + == item['git_blob'], 'source Git blob') + sources[item['path']] = item['sha256'] + return sources + + +def main(): + parser = argparse.ArgumentParser() + parser.add_argument('--write', action='store_true', help='regenerate only RESULT.json') + args = parser.parse_args() + sources = authenticate() + report = {'small': all_small_matrices(), 'larger': larger_matrices(), + 'shortest_clean_columns': shortest_clean_checks(), + 'tariffs': tariff_checks(), 'boundary_controls': reject_controls()} + payload = json.dumps(report, sort_keys=True, indent=2) + '\n' + receipt = Path(__file__).with_name('RESULT.json') + if args.write: + receipt.write_text(payload) + need(receipt.read_text() == payload, 'typed scientific receipt mismatch') + print(json.dumps({'result': report, 'live_source_sha256': sources}, sort_keys=True)) + print('PASS_CLEAN_SQUARE_ZERO_COMPILER rank2_calls=3 dirty_calls=4 no_new_kappa') + + +if __name__ == '__main__': + main() From e5741f1b073213c4ec6f22567cf1168f8f2df215 Mon Sep 17 00:00:00 2001 From: JoyboyBrian <122925040+JoyboyBrian@users.noreply.github.com> Date: Thu, 22 Oct 2026 23:18:31 -0700 Subject: [PATCH 2/3] Check literal reflection and scalar streams on faithful dirty inputs --- research/clean-square-zero-compiler/README.md | 8 +- .../clean-square-zero-compiler/VERIFY.json | 25 +++ .../clean-square-zero-compiler/literal.py | 190 ++++++++++++++++++ 3 files changed, 221 insertions(+), 2 deletions(-) create mode 100644 research/clean-square-zero-compiler/literal.py diff --git a/research/clean-square-zero-compiler/README.md b/research/clean-square-zero-compiler/README.md index 67c8c1b4ab..fdb5f2dd4b 100644 --- a/research/clean-square-zero-compiler/README.md +++ b/research/clean-square-zero-compiler/README.md @@ -29,6 +29,7 @@ Python 3.12 or newer, standard library only: ```sh python3 -I -W error -B research/clean-square-zero-compiler/verify.py python3 -I -O -W error -B research/clean-square-zero-compiler/verify.py +python3 -I -O -W error -B research/clean-square-zero-compiler/literal.py python3 -B scripts/research_package.py --package research/clean-square-zero-compiler ``` @@ -42,8 +43,11 @@ data roles, conjugated ranks one through eight with extra dirty spectators, all clean-column one/two-call obstructions for the first rank-one/two fixtures, literal scalar counts through even rank sixteen, and invalid matrix/zero-coupling boundaries. The uniform theorem is not inferred from -these finite domains. Additional literal action and mutation checks are -described by their registered command and emitted report. +these finite domains. The separate `literal.py` interpreter checks 351 fixtures, every full faithful +input basis column, 160 dense dirty states, the two independent shortest +clean-column obstructions, all 44 single-reflection omissions, four dirty +ancilla failures and four noninvolutory-label failures. It executes literal +scalar CNOTs and address swaps, without multiplying formal projectors. Only this isolated opt-in package changes. Frozen predecessors, selected sources and selected κ=0.00302015 remain unchanged. Native reflection diff --git a/research/clean-square-zero-compiler/VERIFY.json b/research/clean-square-zero-compiler/VERIFY.json index c28f4110c5..14c9627049 100644 --- a/research/clean-square-zero-compiler/VERIFY.json +++ b/research/clean-square-zero-compiler/VERIFY.json @@ -32,6 +32,31 @@ ], "timeout_seconds": 120, "checks": "Same checks with assertions disabled." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/literal.py" + ], + "timeout_seconds": 120, + "checks": "Independent faithful one-CNOT/one-address-swap interpreter on every full input basis column, independent clean-column minimum checks, omitted reflections, dirty ancilla and noninvolutory controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/literal.py" + ], + "timeout_seconds": 120, + "checks": "Independent faithful one-CNOT/one-address-swap interpreter on every full input basis column, independent clean-column minimum checks, omitted reflections, dirty ancilla and noninvolutory controls." } ] } diff --git a/research/clean-square-zero-compiler/literal.py b/research/clean-square-zero-compiler/literal.py new file mode 100644 index 0000000000..7b4fa38e22 --- /dev/null +++ b/research/clean-square-zero-compiler/literal.py @@ -0,0 +1,190 @@ +"""Faithful primitive-stream oracle; no formal projector products. + +JoyboyBrian, with OpenAI Codex assistance; Apache-2.0. +""" +import importlib.util +import json +from pathlib import Path +import random + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def load_compiler(): + path = Path(__file__).with_name('verify.py') + spec = importlib.util.spec_from_file_location('clean_compiler', path) + module = importlib.util.module_from_spec(spec) + spec.loader.exec_module(module) + module.authenticate() + return module + + +def shift(value, addresses=2): + mask = (1 << addresses) - 1 + return ((value << 1) & mask) | (value >> (addresses - 1)) + + +def execute(word, state, addresses=2): + tape = list(state) + for gate in word: + need(gate[0] in ('xor', 'reflect'), 'unknown primitive') + if gate[0] == 'xor': + _, dest, source = gate + need(0 <= source < len(tape) and 0 <= dest < len(tape) + and dest != source, 'invalid scalar CNOT') + tape[dest] ^= tape[source] + else: + _, role = gate + need(0 <= role < len(tape), 'invalid reflection role') + tape[role] = shift(tape[role], addresses) + return tuple(tape) + + +def expected(matrix, state, clean_shift=False, addresses=2): + output = list(state) + for i, row in enumerate(matrix): + for j in range(len(matrix)): + if row >> j & 1: + output[i] ^= state[j] ^ shift(state[j], addresses) + if clean_shift: + output[-1] = shift(state[-1], addresses) + return tuple(output) + + +def basis_states(width, active=None, addresses=2): + if active is None: + active = width + for role in range(active): + for bit in range(addresses): + state = [0] * width + state[role] = 1 << bit + yield tuple(state) + + +def check_literal(matrix, compiler): + q, _, _, word, _ = compiler.compile_matrix(matrix) + columns = 0 + for state in basis_states(len(matrix) + 1): + need(execute(word, state) == expected(matrix, state, q > 0 and not q & 1), + 'literal full-input endpoint') + columns += 1 + return columns + + +def small_and_conjugated(compiler): + fixtures, columns = 0, 0 + for n in range(1, 5): + for bits in range(1 << (n * n)): + matrix = tuple((bits >> (n * i)) & ((1 << n) - 1) for i in range(n)) + # Independent scalar square-zero decision, rather than compiler.apply. + if any(sum(((matrix[k] >> j) & 1) for k in range(n) if matrix[i] >> k & 1) & 1 + for i in range(n) for j in range(n)): + continue + columns += check_literal(matrix, compiler) + fixtures += 1 + random_columns = 0 + for q in range(1, 9): + n = 2 * q + 2 + matrix = [(1 << (q + i)) if i < q else 0 for i in range(n)] + rng = random.Random(2400 + q) + for _ in range(4 * n): + dest, source = rng.sample(range(n), 2) + matrix[dest] ^= matrix[source] + # Right multiplication by the same involutory elementary matrix. + for i, row in enumerate(matrix): + if row >> dest & 1: + matrix[i] ^= 1 << source + columns += check_literal(tuple(matrix), compiler) + _, _, _, word, _ = compiler.compile_matrix(tuple(matrix)) + for _ in range(20): + state = tuple(rng.randrange(4) for _ in range(n)) + (0,) + need(execute(word, state) == expected(tuple(matrix), state), + 'literal dense dirty data / clean return') + random_columns += 1 + fixtures += 1 + return {'fixtures': fixtures, 'faithful_input_basis_columns': columns, + 'dense_dirty_states': random_columns} + + +def independent_shortest(): + result = [] + for q in (1, 2): + data, width = 2 * q, 2 * q + 1 + basis = list(basis_states(width, data)) + changes = set() + for x in range(1, 1 << width): + for y in range(1 << width): + if (x & y).bit_count() % 2 != 1: + continue + encoded = 0 + for col, state in enumerate(basis): + source = 0 + for j in range(width): + if y >> j & 1: + source ^= state[j] + delta = source ^ shift(source) + for role in range(width): + if x >> role & 1: + encoded ^= delta << (2 * (role + width * col)) + changes.add(encoded) + matrix = tuple((1 << (q + i)) if i < q else 0 for i in range(data)) + target = 0 + for col, state in enumerate(basis): + output = expected(matrix, state) + for role in range(width): + target ^= (output[role] ^ state[role]) << (2 * (role + width * col)) + need(target not in changes, 'faithful single-call minimum') + if q == 2: + need(not any((target ^ delta) in changes for delta in changes), + 'faithful two-call minimum') + result.append({'rank': q, 'full_action_changes': len(changes), + 'shorter_than': q + 1}) + return result + + +def omission_and_boundary_controls(compiler): + omissions, all_dirty_failures, noninvolutory = 0, 0, 0 + for q in range(1, 9): + data = 2 * q + matrix = tuple((1 << (q + i)) if i < q else 0 for i in range(data)) + _, _, _, word, _ = compiler.compile_matrix(matrix) + states = list(basis_states(data + 1, data)) + for index, gate in enumerate(word): + if gate[0] != 'reflect': + continue + mutant = word[:index] + word[index + 1:] + need(any(execute(mutant, state) != expected(matrix, state) for state in states), + 'omitted paid reflection accepted') + omissions += 1 + if not q & 1: + helper = (0,) * data + (1,) + need(execute(word, helper) != expected(matrix, helper), + 'dirty helper falsely restored') + all_dirty_failures += 1 + three_states = list(basis_states(data + 1, data, 3)) + need(any(execute(word, state, 3) != expected(matrix, state, addresses=3) + for state in three_states), 'noninvolution falsely admitted') + noninvolutory += 1 + old = compiler.lower_projectors(compiler.canonical_projectors(q, data, False), + data + 1) + need(all(execute(old, state) == expected(matrix, state) + for state in basis_states(data + 1)), 'matched dirty baseline endpoint') + return {'omitted_reflections_rejected': omissions, + 'dirty_ancilla_rejected': all_dirty_failures, + 'noninvolutory_labels_rejected': noninvolutory} + + +def main(): + compiler = load_compiler() + report = small_and_conjugated(compiler) + report['independent_shortest'] = independent_shortest() + report['controls'] = omission_and_boundary_controls(compiler) + print(json.dumps(report, sort_keys=True)) + print('PASS_CLEAN_SQUARE_ZERO_LITERAL scalar_cnots_and_address_swaps no_new_kappa') + + +if __name__ == '__main__': + main() From 7c9247ea3878906715c136421d5e5248535596fe Mon Sep 17 00:00:00 2001 From: JoyboyBrian <122925040+JoyboyBrian@users.noreply.github.com> Date: Thu, 22 Oct 2026 23:20:16 -0700 Subject: [PATCH 3/3] Reject corrupted sources, receipts, and literal compiler mutants --- research/clean-square-zero-compiler/README.md | 14 ++- research/clean-square-zero-compiler/TASK.json | 10 ++- .../clean-square-zero-compiler/VERIFY.json | 13 +++ .../clean-square-zero-compiler/controls.py | 88 +++++++++++++++++++ 4 files changed, 119 insertions(+), 6 deletions(-) create mode 100644 research/clean-square-zero-compiler/controls.py diff --git a/research/clean-square-zero-compiler/README.md b/research/clean-square-zero-compiler/README.md index fdb5f2dd4b..7135e70c61 100644 --- a/research/clean-square-zero-compiler/README.md +++ b/research/clean-square-zero-compiler/README.md @@ -27,10 +27,10 @@ reflection does not establish a lower native total price. Python 3.12 or newer, standard library only: ```sh -python3 -I -W error -B research/clean-square-zero-compiler/verify.py -python3 -I -O -W error -B research/clean-square-zero-compiler/verify.py -python3 -I -O -W error -B research/clean-square-zero-compiler/literal.py -python3 -B scripts/research_package.py --package research/clean-square-zero-compiler +python3.12 -I -W error -B research/clean-square-zero-compiler/verify.py +python3.12 -I -O -W error -B research/clean-square-zero-compiler/verify.py +python3.12 -I -O -W error -B research/clean-square-zero-compiler/literal.py +python3.12 -B scripts/research_package.py --package research/clean-square-zero-compiler ``` `verify.py --write` regenerates only RESULT.json. Normal verification writes @@ -48,6 +48,12 @@ input basis column, 160 dense dirty states, the two independent shortest clean-column obstructions, all 44 single-reflection omissions, four dirty ancilla failures and four noninvolutory-label failures. It executes literal scalar CNOTs and address swaps, without multiplying formal projectors. +`controls.py` executes six actual CLI tests after relocation without Git: normal +and optimized read-only replay, live-source corruption, a Boolean scientific +receipt mutation, an incorrect reflection role, an omitted clean projector +and a missing scalar inverse. The wrong-role mutant intentionally passes the +primary algebra/count checker and is rejected by the literal oracle, showing +why the independently implemented endpoint check is necessary. Only this isolated opt-in package changes. Frozen predecessors, selected sources and selected κ=0.00302015 remain unchanged. Native reflection diff --git a/research/clean-square-zero-compiler/TASK.json b/research/clean-square-zero-compiler/TASK.json index 91b03f9f72..20a7d36182 100644 --- a/research/clean-square-zero-compiler/TASK.json +++ b/research/clean-square-zero-compiler/TASK.json @@ -50,7 +50,7 @@ "budget_minutes": 60, "stop_rule": "Stop at the first uniform theorem, literal lowering, independent finite corroboration and corruption controls; do not expand into a native construction without its full resource contract.", "outcome": "completed", - "evidence": "PROOF.md gives the uniform argument; verify.py checks new clean-column endpoints, first-fixture shortest sums and literal tariff counts.", + "evidence": "PROOF.md supplies the uniform rank-saturation lower bound and explicit clean construction. verify.py checks 343 small matrices, ranks through eight and matched tariffs; literal.py checks 351 fixtures / 3556 full basis columns / 160 dirty states, independent clean-column minima and 52 omission/boundary controls. controls.py adds six real relocated CLI/mutation tests.", "author": "JoyboyBrian", "ai_assistance": "Substantial OpenAI Codex assistance. Independent human and formal proof-kernel review unclaimed.", "open_questions": [ @@ -66,5 +66,11 @@ "first_step": "Optimize both rank-two streams under their exact data/clean return contracts.", "blocked_by": "An equally charged physical primitive model must be fixed." } - ] + ], + "environment": { + "python": "3.12.2 and 3.14.6", + "implementation": "CPython", + "platform": "macOS arm64", + "dependencies": "Python standard library only" + } } diff --git a/research/clean-square-zero-compiler/VERIFY.json b/research/clean-square-zero-compiler/VERIFY.json index 14c9627049..204f14a6ee 100644 --- a/research/clean-square-zero-compiler/VERIFY.json +++ b/research/clean-square-zero-compiler/VERIFY.json @@ -57,6 +57,19 @@ ], "timeout_seconds": 120, "checks": "Independent faithful one-CNOT/one-address-swap interpreter on every full input basis column, independent clean-column minimum checks, omitted reflections, dirty ancilla and noninvolutory controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/controls.py" + ], + "timeout_seconds": 120, + "checks": "Six actual relocated CLI tests: read-only Git-free normal/optimized replay, source and typed-receipt drift, wrong reflection target, omitted clean projector and lost scalar inverse." } ] } diff --git a/research/clean-square-zero-compiler/controls.py b/research/clean-square-zero-compiler/controls.py new file mode 100644 index 0000000000..51f26ef622 --- /dev/null +++ b/research/clean-square-zero-compiler/controls.py @@ -0,0 +1,88 @@ +"""Actual relocated CLI and mutation controls. JoyboyBrian; Apache-2.0.""" +import hashlib +import json +from pathlib import Path +import shutil +import subprocess +import sys +import tempfile +import unittest + + +class Controls(unittest.TestCase): + def setUp(self): + self.temp = tempfile.TemporaryDirectory(prefix='clean-square-zero-') + self.addCleanup(self.temp.cleanup) + self.root = Path(self.temp.name) + original = Path(__file__).resolve().parent + self.package = self.root / 'research' / original.name + shutil.copytree(original, self.package, ignore=shutil.ignore_patterns('__pycache__')) + repository = original.parent.parent + manifest = json.loads((original / 'VERIFY.json').read_text()) + for name in manifest['inputs']: + destination = self.root / name + destination.parent.mkdir(parents=True, exist_ok=True) + shutil.copyfile(repository / name, destination) + + def run_script(self, script, optimize=False): + command = [sys.executable, '-I'] + (['-O'] if optimize else []) + command += ['-W', 'error', '-B', str(self.package / script)] + return subprocess.run(command, cwd=self.root, capture_output=True, + text=True, timeout=20, check=False) + + def snapshot(self): + return {str(p.relative_to(self.root)): hashlib.sha256(p.read_bytes()).hexdigest() + for p in self.root.rglob('*') if p.is_file()} + + def replace(self, old, new): + path = self.package / 'verify.py' + source = path.read_text() + self.assertEqual(source.count(old), 1) + path.write_text(source.replace(old, new)) + + def assert_rejected(self, result, reason): + self.assertNotEqual(result.returncode, 0, result.stdout) + self.assertIn(reason, result.stderr) + + def test_git_free_readonly_normal_and_optimized(self): + before = self.snapshot() + for optimize in (False, True): + for script in ('verify.py', 'literal.py'): + result = self.run_script(script, optimize) + self.assertEqual(result.returncode, 0, result.stderr) + self.assertIn('PASS_CLEAN_SQUARE_ZERO_', result.stdout) + self.assertEqual(self.snapshot(), before) + + def test_declared_source_corruption_rejects(self): + path = self.root / 'research/square-zero-idempotent-compiler/PROOF.md' + path.write_bytes(path.read_bytes() + b'\ncorrupted source\n') + self.assert_rejected(self.run_script('verify.py', True), 'source SHA256') + + def test_boolean_receipt_rejects(self): + path = self.package / 'RESULT.json' + receipt = json.loads(path.read_text()) + receipt['boundary_controls'] = True + path.write_text(json.dumps(receipt, sort_keys=True, indent=2) + '\n') + self.assert_rejected(self.run_script('verify.py', True), 'typed scientific receipt mismatch') + + def test_wrong_reflection_role_needs_literal_oracle(self): + self.replace("gates.extend(b + a + [('reflect', pivot)]", + "gates.extend(b + a + [('reflect', (pivot + 1) % width)]") + primary = self.run_script('verify.py', True) + self.assertEqual(primary.returncode, 0, primary.stderr) + self.assert_rejected(self.run_script('literal.py', True), 'literal full-input endpoint') + + def test_omitted_even_clean_projector_rejects(self): + self.replace('result.append((((1 << q) - 1) | h, sources | h, n))', + 'pass # actual omitted clean projector control') + self.assert_rejected(self.run_script('verify.py', True), 'full canonical formal endpoint') + + def test_missing_scalar_inverse_rejects(self): + self.replace("+ list(reversed(a)) + list(reversed(b)))", + "+ list(reversed(b)))") + self.assert_rejected(self.run_script('verify.py', True), 'clean scalar tariff') + self.assert_rejected(self.run_script('literal.py', True), 'literal full-input endpoint') + + +if __name__ == '__main__': + unittest.main(verbosity=2)