Skip to content

Prove the clean square-zero coupling optimum with priced primitive lowering - #5007

Merged
Mister-Meeseeks merged 3 commits into
CrocSwap:mainfrom
JoyboyBrian:brian/r6-clean-square-zero
Oct 23, 2026
Merged

Mister-Meeseeks merged 3 commits into
CrocSwap:mainfrom
JoyboyBrian:brian/r6-clean-square-zero

Conversation

@JoyboyBrian

Copy link
Copy Markdown
Contributor

For a rank-q square-zero binary coupling, allowing returned clean workspace changes the exact reflection-call minimum to q+1. At rank two, one clean role permits three calls where Nick Petalas's PR #4912 proves four with dirty workspace. The uniform lower bound allows arbitrary finite clean and restored dirty helpers, with free constant binary scalar mixing. The even-rank construction and its clean return are explicit.

The package also lowers every call to literal coordinate reflections and scalar CNOTs, including inverse operations and common basis transport. Its canonical even-rank word costs (q+1)R + 2q(q+2)C + H; the explicitly lowered predecessor split compiler costs (q+2)R + (2q²-4)C. It wins exactly when R > 4(q+1)C + H. In particular the first fixture is 3R+16C+H versus 4R+4C. These are prices of specified words; scalar-network optimality and a native clean-resource price are unclaimed.

Canonical CLAIM. Three substantive commits separate the proof/compiler, independent primitive interpreter, and actual corruption/relocation controls. Only the new opt-in research/clean-square-zero-compiler/ package changes.

Evidence at head 7c9247ea3878906715c136421d5e5248535596fe:

  • The written proof normalizes free scalar maps on active input columns, uses rank saturation to exclude q calls, and constructs q+1 legal projectors. Even-rank helpers have full action [g], so only their initialized zero state returns; a dirty replacement is explicitly rejected.
  • Primary checks cover all 343 square-zero binary matrices through four data roles, eight nontrivially conjugated rank-one through rank-eight fixtures with dirty spectators, exact clean-column one/two-call obstructions, and literal scalar counts through even rank sixteen.
  • The independent faithful-action interpreter executes one scalar CNOT or one address swap at a time. It checks 351 fixtures, all 3,556 full input basis columns, 160 dense dirty states, separately computed clean-column shortest sums, 44 omitted reflections, four dirty-ancilla failures and four noninvolutory-label failures.
  • Six actual relocated CLI tests check normal/optimized read-only replay, source corruption, Boolean receipt corruption, an incorrect reflection role, an omitted clean projector and a missing scalar inverse. The wrong-reflection-role mutant passes the algebra/count checker and fails the independently implemented literal endpoint oracle.
  • All five registered commands pass under CPython 3.12.2 on macOS arm64, standard library only. The two scientific scripts also pass directly under CPython 3.14.6; the generic launcher correctly requires Python 3.12.
  • Metadata, final committed bytes/source-history, official 11-file export and export integrity pass. All five commands pass from the checked export with Git absent from PATH; all exported bytes remain unchanged. Cold times are 0.254/0.264 seconds for the primary normal/optimized checks, 0.180/0.179 seconds for the literal checks, and 1.890 seconds for the actual CLI controls.
python3.12 -B scripts/research_package.py --package research/clean-square-zero-compiler
python3.12 -B scripts/check_research_commit.py --package research/clean-square-zero-compiler --check-source-history

Scope and remaining obligations: the full formal group algebra is F2[C2] for one fixed nonidentity involution, and paid couplings remain binary rank-one idempotents. The theorem is a written uniform argument; finite checks corroborate it. A clean address function, its reservation charge H, complete stationary primitive prices, physical tapes/routing/frames and native reflection implementation are not supplied. No scalar-network optimum, recursive supplier admission, new κ, selected-frontier change or full multiplication theorem is claimed. Lean, Docker, the full selected cold replay and predecessor executables were not run. Open next questions identify a literal native price binding and a matched optimization of both primitive streams.

Source/overlap: canonical main bee95ce88f9f19802f0613f92838895cd0e14a1f, priority revision 7. Main retains PR #4912 head eaea286b055724895adb4ca949b5ac0495be5ff8; its live body, head and comments were read. The initial complete cache covers 310 open PRs at 2026-10-23 06:05:59 UTC, 4096 Discussion records at 06:06:48 UTC, and all 6690 main package notes. The square-zero/clean query has twelve related leads and no same minimum. Cached text, omitted arbitrary diffs/history and unpublished work remain coverage limits. Submission refresh is recorded separately before publication.

Credit Nick Petalas #4912 for the exact dirty optimum, odd-rank construction and even-rank split; ywz65 #2716 for the product identity and arbitrary-coupling implementation motivation; Adam Gall #1911, eumemic #288, Ali Romman #468, woklerx #1443, Gareth Davidson #1333, Arham Tahir #1589 and Cinna Davis #2290 for retained register-model lineage. JoyboyBrian with substantial OpenAI Codex assistance. Apache-2.0. Independent human and proof-kernel review are unclaimed.

Hosted CI is pending at publication; local replay success is not a claim that hosted checks passed.

Submission refresh (2026-10-23 06:22–06:24 UTC): canonical main f259dabc7d70e0db8d6d36bfda888f008bbfecc1 was fetched; governing guidance, selected record and every declared scientific input for this package are unchanged. The scientific base remains bee95ce88f9f19802f0613f92838895cd0e14a1f intentionally; all new package paths are disjoint from upstream changes. Refreshed overlap paginated 304 open PRs and 4,114 discussion records; local coverage is all 6,690 notes at the pinned scientific base. Cached coverage is not a novelty certificate.

@jwr404

jwr404 commented Oct 23, 2026

Copy link
Copy Markdown
Contributor

Independent check at head 7c9247ea. The registered replay passes on Linux with CPython 3.12.14 in 3.3 s.

Lower bound (§1). Since t² = 0, P = I + tΣx_jy_jᵀ, and the column identity Σx_jy_jᵀE = EN gives k ≥ q. If k = q, then X₀ is injective and V = YE is surjective. So X₀VX₀V = N² = 0 gives VX₀ = 0, while its diagonal is y_jᵀx_j = 1. ✓ Only the active input columns are constrained, so the clean columns impose no parity condition. This is exactly why the dirty parity bound of #4912 doesn't carry over.

Even construction (§2). I recomputed it with my own bitmask code for every even q = 2, 4, …, 12. All q+1 pairings have yᵀx = 1 through h, and Σx_jy_jᵀ = N + hhᵀ exactly, so the clean role acts as [g] and returns zero from a zero start. The literal lowering counts 2(wt x − 1) + 2(wt y − 1) summed to 16, 48, 96, 160, 240, 336 = 2q(q+2) CNOTs, as stated.

Comparison (§3). The dirty baseline is 2(q−1)² + 4(q−1) − 4 (odd block) + 2 (rank-one block) = 2q² − 4 CNOTs with q+2 reflections. So the clean word wins iff R > 4(q+1)C + H. At q = 2 that is 3R + 16C + H versus 4R + 4C. ✓

The scope is as stated: a changed workspace contract with no native price for the clean role. This is an author-independent check, not acceptance, and κ is unchanged.

Reviewed by James Reed with substantial Anthropic Claude (Claude Code) assistance.

@Mister-Meeseeks
Mister-Meeseeks merged commit 5948b87 into CrocSwap:main Oct 23, 2026
2 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants