From 7fb68fae85e68da0e28d87659b15c2f456620ea2 Mon Sep 17 00:00:00 2001 From: ToikY <27568617+ToikY@users.noreply.github.com> Date: Wed, 14 Oct 2026 06:56:40 -0700 Subject: [PATCH 1/3] Research: characterize clean selector encoding widths and volume cost Exact single-host clean-subspace width and phase specialization of credited spectral methods. No new kappa or frontier change. Prepared with substantial OpenAI Codex assistance. --- .../clean-selector-embedding/CERTIFICATE.json | 370 ++++++++++++++++++ .../PREDECESSORS.json | 38 ++ research/clean-selector-embedding/PROOF.md | 184 +++++++++ research/clean-selector-embedding/README.md | 131 +++++++ .../clean-selector-embedding/SOURCES.json | 24 ++ research/clean-selector-embedding/TASK.json | 107 +++++ .../clean-selector-embedding/VALIDATION.json | 83 ++++ research/clean-selector-embedding/VERIFY.json | 34 ++ .../clean-selector-embedding/test_verify.py | 79 ++++ research/clean-selector-embedding/verify.py | 237 +++++++++++ 10 files changed, 1287 insertions(+) create mode 100644 research/clean-selector-embedding/CERTIFICATE.json create mode 100644 research/clean-selector-embedding/PREDECESSORS.json create mode 100644 research/clean-selector-embedding/PROOF.md create mode 100644 research/clean-selector-embedding/README.md create mode 100644 research/clean-selector-embedding/SOURCES.json create mode 100644 research/clean-selector-embedding/TASK.json create mode 100644 research/clean-selector-embedding/VALIDATION.json create mode 100644 research/clean-selector-embedding/VERIFY.json create mode 100644 research/clean-selector-embedding/test_verify.py create mode 100644 research/clean-selector-embedding/verify.py diff --git a/research/clean-selector-embedding/CERTIFICATE.json b/research/clean-selector-embedding/CERTIFICATE.json new file mode 100644 index 0000000000..d1e0afd187 --- /dev/null +++ b/research/clean-selector-embedding/CERTIFICATE.json @@ -0,0 +1,370 @@ +{ + "status": "PASS_CLEAN_SELECTOR_EMBEDDING", + "no_new_kappa": true, + "scope": "Exact invariant clean-subspace algebra; inherited full-volume tariff screen only", + "multiplicity_oracle_widths": 131, + "width_cases": 4096, + "width_table_sha256": "12873f0c677ad03b12084ccd8272ce8c006caa334c08c262c2512f633ee04637", + "fixed_width_counts": { + "1": 4032, + "2": 64 + }, + "optional_phase_width_counts": { + "1": 4096, + "2": 0 + }, + "fixtures": [ + { + "n": 1, + "s": 1, + "d": 4, + "phase": 0, + "ambient_coordinates": 16, + "payload_coordinates": 4, + "volume_ratio": "4", + "mapping": [ + 0, + 1, + 15, + 2 + ], + "intertwiner_entries": 64, + "gram_entries": 16 + }, + { + "n": 1, + "s": 1, + "d": 3, + "phase": 3, + "ambient_coordinates": 8, + "payload_coordinates": 4, + "volume_ratio": "2", + "mapping": [ + 1, + 3, + 2, + 5 + ], + "intertwiner_entries": 32, + "gram_entries": 16 + }, + { + "n": 1, + "s": 2, + "d": 5, + "phase": 0, + "ambient_coordinates": 32, + "payload_coordinates": 8, + "volume_ratio": "4", + "mapping": [ + 0, + 1, + 15, + 2, + 23, + 4, + 27, + 8 + ], + "intertwiner_entries": 256, + "gram_entries": 64 + }, + { + "n": 1, + "s": 2, + "d": 4, + "phase": 2, + "ambient_coordinates": 16, + "payload_coordinates": 8, + "volume_ratio": "2", + "mapping": [ + 3, + 7, + 5, + 11, + 6, + 13, + 9, + 14 + ], + "intertwiner_entries": 128, + "gram_entries": 64 + }, + { + "n": 2, + "s": 1, + "d": 4, + "phase": 0, + "ambient_coordinates": 16, + "payload_coordinates": 8, + "volume_ratio": "2", + "mapping": [ + 0, + 1, + 2, + 3, + 15, + 4, + 8, + 5 + ], + "intertwiner_entries": 128, + "gram_entries": 64 + }, + { + "n": 2, + "s": 1, + "d": 4, + "phase": 0, + "ambient_coordinates": 16, + "payload_coordinates": 8, + "volume_ratio": "2", + "mapping": [ + 0, + 1, + 2, + 3, + 15, + 4, + 8, + 5 + ], + "intertwiner_entries": 128, + "gram_entries": 64 + }, + { + "n": 2, + "s": 2, + "d": 6, + "phase": 0, + "ambient_coordinates": 64, + "payload_coordinates": 16, + "volume_ratio": "4", + "mapping": [ + 0, + 1, + 2, + 3, + 15, + 4, + 8, + 5, + 23, + 16, + 31, + 6, + 27, + 32, + 47, + 9 + ], + "intertwiner_entries": 1024, + "gram_entries": 256 + }, + { + "n": 2, + "s": 2, + "d": 5, + "phase": 2, + "ambient_coordinates": 32, + "payload_coordinates": 16, + "volume_ratio": "2", + "mapping": [ + 3, + 7, + 11, + 0, + 5, + 13, + 14, + 15, + 6, + 19, + 21, + 23, + 9, + 22, + 25, + 27 + ], + "intertwiner_entries": 512, + "gram_entries": 256 + }, + { + "n": 3, + "s": 1, + "d": 5, + "phase": 0, + "ambient_coordinates": 32, + "payload_coordinates": 16, + "volume_ratio": "2", + "mapping": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 15, + 8, + 16, + 9, + 31, + 10, + 12, + 11 + ], + "intertwiner_entries": 512, + "gram_entries": 256 + }, + { + "n": 3, + "s": 1, + "d": 5, + "phase": 0, + "ambient_coordinates": 32, + "payload_coordinates": 16, + "volume_ratio": "2", + "mapping": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 15, + 8, + 16, + 9, + 31, + 10, + 12, + 11 + ], + "intertwiner_entries": 512, + "gram_entries": 256 + }, + { + "n": 1, + "s": 4, + "d": 7, + "phase": 0, + "ambient_coordinates": 128, + "payload_coordinates": 32, + "volume_ratio": "4", + "mapping": [ + 0, + 1, + 15, + 2, + 23, + 4, + 27, + 8, + 29, + 16, + 30, + 31, + 39, + 32, + 43, + 47, + 45, + 55, + 46, + 59, + 51, + 61, + 53, + 62, + 54, + 64, + 57, + 79, + 58, + 87, + 60, + 91 + ], + "intertwiner_entries": 4096, + "gram_entries": 1024 + }, + { + "n": 1, + "s": 4, + "d": 6, + "phase": 2, + "ambient_coordinates": 64, + "payload_coordinates": 32, + "volume_ratio": "2", + "mapping": [ + 3, + 7, + 5, + 11, + 6, + 13, + 9, + 14, + 10, + 19, + 12, + 21, + 17, + 22, + 18, + 25, + 20, + 26, + 24, + 28, + 33, + 35, + 34, + 37, + 36, + 38, + 40, + 41, + 48, + 42, + 63, + 44 + ], + "intertwiner_entries": 2048, + "gram_entries": 1024 + } + ], + "controls": [ + "insufficient i eigenspace", + "duplicate eigenvector", + "unbilled phase", + "zero payload width", + "no batching", + "dirty complement not restored", + "constant-only smoke test insufficient" + ], + "motivating_target_counts": [ + 16, + 16, + 0, + 0 + ], + "native_d6_counts": [ + 16, + 12, + 16, + 20 + ], + "native_d7_counts": [ + 36, + 28, + 28, + 36 + ], + "tariff": "ambient/payload >= 2; B_native/B_lanes = 2^(d-n-s)*(d/n)^sigma > 2 for 02^{N/2}. +\] + +Thus \(d=N\) is impossible for every phase. This full-space obstruction is +credited to Arham's active [Discussion #1901](https://github.com/CrocSwap/integer-mult-bounds/discussions/1901); +it is an inherited lower endpoint here, not a new claim of priority. + +To prove existence at \(N+2\), each residue class of weights is contained in +one parity class, giving \(m_n(j)\leq2^{n-1}\). The roots-of-unity filter, for +\(d>0\), gives + +\[ +m_d(j)=2^{d-2}+2^{d/2-1} +\cos(d\pi/4-j\pi/2). +\] + +Consequently, since \(N\geq2\), + +\[ +\min_j m_{N+2}(j)\geq2^N-2^{N/2}\geq2^{N-1} +\geq q\max_jm_n(j). +\] + +This proves (1) simultaneously for all four phases. These real expressions are +only the written bound; exact finite certificates can use the integer binomial +sums or the recurrence \(m_{d+1}(j)=m_d(j)+m_d(j-1)\). + +If an arbitrary scalar phase \(\lambda\) is proposed, the target has a nonzero +eigenspace of eigenvalue 1. Intertwining into \(\lambda C_d\) therefore forces +\(\lambda i^k=1\) for some integer \(k\). Thus the four phases above exhaust +all scalar phases that can satisfy the exact encoding equation. + +## Explicit injective Walsh encoding and restoration + +Let \(W_d[x,y]=(-1)^{x\cdot y}\) be the unnormalized Walsh matrix. Then +\(W_d^2=2^dI\) and \(C_dW_d=W_d\operatorname{diag}(i^{|y|})\). +Write \(W=I_q\otimes W_n\). Under (1), choose distinct labels +\(f(\ell,y)\in\{0,1\}^d\), one for each lane and data eigenlabel, such that + +\[ +|f(\ell,y)|\equiv |y|-u\pmod4. +\] + +Choosing unused labels in increasing integer order makes this deterministic. +Let \(J_f\) inject the target standard basis into those ambient labels. The +exact dyadic-rational matrices + +\[ +E=2^{-n}W_dJ_fW,\qquad L=2^{-d}WJ_f^TW_d +\] + +satisfy \(LE=I\) and \(i^uC_dE=EB\). No square-root coefficients are needed. +An isometric version also exists by using normalized Walsh matrices; its +implementation costs are not assumed free. + +Extend the selected labels to a permutation of all ambient labels. This extends +\(E\) to an invertible encoder \(P\) whose inverse is an exact decoder, and + +\[ +P^{-1}(i^uC_d)P=B\oplus D_{\mathrm{comp}}, +\] + +where the complement block is diagonal with the remaining fourth-root phases. +Hence encoding \((x,0)\), applying the child, and decoding returns \((Bx,0)\) +for every complex input \(x\), including correlated lane values. The complement +is algebraically restored to zero. For arbitrary dirty complement \(z\), the +endpoint is instead \((Bx,D_{\mathrm{comp}}z)\); it generally does not restore +\(z\). This clean contract does not establish the predecessor's arbitrary-dirty +padding contract. An additional dirty restoration must be proved and charged if +that stronger contract is required. + +## Sixteen-lane example and explicit volume charge + +For \(n=1,s=4\), target multiplicities are \((16,16,0,0)\). The exact ambient +vectors at \(d=5,6,7\) are respectively + +\[ +(6,6,10,10),\quad(16,12,16,20),\quad(36,28,28,36). +\] + +The fixed-phase least dimension is 7: dimensions 5 and 6 fail and dimension 7 +passes. Its 128 ambient states are four times the 32 active states. If the +phase \(u=2\) is permitted, dimension 6 passes using ambient classes 2 and 3, +whose multiplicities are 16 and 20. This uses 64 ambient states, twice the active +dimension, and the global sign must be included in the complete implementation. + +Let \(V\) be one original lane's volume, including spectator fibers. The +original \(q\) children have the inherited numerical budget +\(A V q n^\sigma\), where \(0<\sigma<1\). A child on the encoded ambient +array has volume \(2^{d-n}V\), so its budget alone is + +\[ +A V\,2^{d-n}d^\sigma, +\qquad +\frac{\text{ambient-child budget}}{\text{original budget}} +=2^{d-N}(d/n)^\sigma>2. +\] + +This inequality holds for every allowable phase because \(d\geq N+1\). +It grants the encoder, decoder, clean-space preparation, routing, phase work, +coefficient storage, precision and restoration for free. Charging those +nonnegative costs cannot improve this particular comparison. The comparison is +between inherited upper-bound expressions, not a lower bound on actual runtime +or a prohibition of other recursion algorithms. + +The dimensions here are literal tensor dimensions. If data width is scaled to +\(nf\) while the number of lanes remains \(2^s\), recompute the criterion with +\(nf\) in place of \(n\): the ambient dimension is \(nf+s+1\) or \(nf+s+2\). +The finite example \(C_7\) must not be relabeled \(C_{7f}\) while retaining its +constant fourfold volume. Scaling selector width as well changes the lane +count and must charge that volume explicitly. + +The retained [selector-batching note](../selector-batching/README.md) supplies +the kernel convention, monomial support obstruction, arbitrary-dirty-padding +restoration and volume accounting. This result changes its hypothesis to a +clean invariant subspace and characterizes that algebraic contract exactly. +It supplies no new owner assignment, restored-work or precision theorem, +supplier admission, or improved \(\kappa\). diff --git a/research/clean-selector-embedding/README.md b/research/clean-selector-embedding/README.md new file mode 100644 index 0000000000..934b7431ad --- /dev/null +++ b/research/clean-selector-embedding/README.md @@ -0,0 +1,131 @@ +# Sharp clean encoding width for independent tensor lanes + +**Scoped algebraic interface and unfavorable inherited-budget result; no new κ.** + +For `q=2^s` independent same-direction `C_n` lanes, an exact injective encoding +into one `i^u C_d` child exists precisely when its four eigenspace multiplicities +dominate the lane multiplicities. For every `n,s>=1` and each allowed phase, the +least native width is **`n+s+1` or `n+s+2`**, decided by four integer inequalities. +[PROOF.md](PROOF.md) gives the all-size argument and an explicit dyadic Walsh +encoding; the finite checker is separate evidence. + +The motivating 16-lane, width-one target has multiplicities `(16,16,0,0)`: + +| Native width | Multiplicities of C_d | Exact phase | Optional phase | +| --- | --- | --- | --- | +| 5 | `(6,6,10,10)` | fails | every phase fails | +| 6 | `(16,12,16,20)` | fails | `-C_6` passes | +| 7 | `(36,28,28,36)` | passes | passes | + +Thus the exact-phase encoding uses 128 ambient coordinates for 32 active +coordinates; allowing a global minus sign reduces it to 64. A phase is an +explicit interface choice, not an ignored equality up to phase. + +The input may be arbitrary and correlated within the encoded subspace. Its +complement must be zero. An invertible extension of the encoder returns that +zero complement to zero, but generally rotates **dirty** complement coordinates +by fourth-root phases. This does not provide an arbitrary-dirty workspace +replacement for a selected child. + +Under the predecessor's full-array cost expression `A V d^sigma`, `0 2. +``` + +This waives encoding, decoding, initialization, routing, phase application, +restoration and precision costs. Nonnegative extra charges cannot rescue this +particular comparison. These are available upper-bound expressions; this is +not a lower bound on optimal runtime or a universal obstruction to other +algorithms. Scaling a data width to `n*f` requires recomputing the literal +dimension; the finite `C_7` example is not automatically a `C_(7f)` interface. + +## Reproduction and evidence + +```sh +python3.12 -I -B research/clean-selector-embedding/verify.py +python3.12 -B scripts/research_package.py --package research/clean-selector-embedding +``` + +Expected `PASS_CLEAN_SELECTOR_EMBEDDING`, followed by the registered-package +marker. Standard library only. The verifier reads its committed certificate; +`--output /new/path.json` creates an exclusively new receipt. + +- Independent integer binomial and roots-of-unity character counts agree at + all 131 widths `0..130`. +- All 4,096 `(n,s)` pairs in `1..64` check fixed and optional phase boundaries, + exclusion at equal volume, and the uniform two-extra-bit upper endpoint. +- Twelve complete fixtures, including both 16-lane phase conventions, compare + every entry of `i^u C_d E` and `E (I_q tensor C_n)` by literal Gaussian-dyadic + butterflies. Exact Gram identities give a left inverse of each encoding. +- Seven controls reject insufficient eigenspace capacity, duplicate labels, + an unbilled phase, zero payload width, absence of batching, unrestored dirty + complement, and admission from a constant-vector smoke test. + +These linear identities cover arbitrary complex coefficients on the declared +subspace. No existing supplier word, physical route or production precision +schedule is executed by these fixtures. Local replay details and external +source-byte pins are recorded in `VALIDATION.json` and `PREDECESSORS.json`. + +## Task and overlap + +Base `0b1cccf86e2f5132ed286a26ef0a681a495740ea`; fresh OS nonce +`9a396c07a6d107acdb9a76567c1010d0`; revision 3 complex-mechanisms / +complex-rank-shape-decoder. Selected-record SHA256 +`10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32`. +Baseline bindings, assigned ceiling positive control and lever table were +replayed before the detour. + +The initial full-space reciprocal-basis idea overlapped Arham Tahir's fresh +[Discussion1901](https://github.com/CrocSwap/integer-mult-bounds/discussions/1901). +Before implementation, one pivot changed the premise to a clean invariant +subspace. The exact claim and completed handoff are in that Discussion. The +card's physical construction and 5% gain acceptance gate is **not met**. + +PR665 already states the generic multiplicity criterion and builds a spectral +encoder for a different two-host split. This contribution specializes that +credited method to one `C_d` host for repeated equal-width lanes and supplies +the sharp native width, explicit phase distinction and full-volume screen. +It does not claim priority for spectral encoding or for Arham's full-space +trace obstruction. PR679 and Ross Richardson's subsequent audit concern the +monomial arbitrary-dirty contract; their conclusions remain credited. + +Initial overlap covered 554 open PR titles/bodies, local notes and relevant +live Discussions. Numbered REST pages are non-atomic; no complete Discussion +census or novelty certificate is claimed. The pre-submission refresh at +13:54–13:55 UTC covered 573 open PR bodies and 873 local notes. Arham's newly +published [PR1920](https://github.com/CrocSwap/integer-mult-bounds/pull/1920), +head `057b214aea45c65926b93ad8b95693c80f0f79c9`, explicitly excludes the +parallel clean-injective premise. Frozen sources and the selected frontier +remain unchanged. + +## Open next questions + +- Can a different recursion algorithm price an encoded host by its reachable + subspace? First give a uniform implementation and complete volume/workspace + invoice; the current full-array bound does not permit that discount. +- Can a selected caller supply the clean invariant space and a legal encoder? + First identify one exact source-bound call and prove its entry state belongs + to the subspace; no selected occurrence or compiler is provided here. +- Can nonreciprocal adapters or a different child alphabet change the budget? + First name the changed endpoint and charge both adapters and dirty restoration. + The current statement covers an injective invariant encoding only. + +## Credit and limits + +Douglas R. Colkitt's PR665 supplies the spectral-capacity/Walsh method. Greer +Guthrie's PR679 supplies the kernel, monomial support obstruction, dirty padding +and volume warning. Arham Tahir's Discussion1901 supplies the parallel +full-space trace obstruction; his PR1605 supplies the rank-shape budget context. +Ross Richardson's `8a3900c84213fd7603b99beaceaff48f501b4232` audit identifies +the direct-sum/tensor gap and clean-encoding next question. Credit Jose Manuel +(jmbarrancoml), publishing account Cinna Davis (1337isnot1337)/PR1779, Josie +Elliston/PR1817, icekylinx's exact kernel and the Rohan Arun, Jeremy Kothe, +Hao Yan and retained selected construction lineage. + +New specialization/checker by ToikY with substantial OpenAI Codex assistance +and bounded proof/review agents. Apache-2.0. No full selected cold replay, +physical/native admission, all-size tape compiler, production precision, +analytic transfer, Lean multiplication theorem, hosted CI pass or independent +human approval is claimed. diff --git a/research/clean-selector-embedding/SOURCES.json b/research/clean-selector-embedding/SOURCES.json new file mode 100644 index 0000000000..fca80172b8 --- /dev/null +++ b/research/clean-selector-embedding/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea", + "files": [ + { + "path": "docs/research/agent-task-catalog.json", + "usage": "input", + "git_blob": "06c96f5579bb67ed1b86d334e78fbed7da6945f1", + "sha256": "6686ad58f1fbdbc87134a78901b60fd53a20d3984355e91defbbebc9e9fa8075" + }, + { + "path": "certificates/selected-result.json", + "usage": "input", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "research/selector-batching/README.md", + "usage": "input", + "git_blob": "167f5ca029190e92c4a84423c22bbe15a8534031", + "sha256": "e50bae87f9bfa2dee515468aeb56d47676410ca3adfdf0e83d11bf0e31fadf2d" + } + ] +} diff --git a/research/clean-selector-embedding/TASK.json b/research/clean-selector-embedding/TASK.json new file mode 100644 index 0000000000..3b9e356aa7 --- /dev/null +++ b/research/clean-selector-embedding/TASK.json @@ -0,0 +1,107 @@ +{ + "schema_version": 1, + "task_id": "complex-rank-shape-decoder", + "priority_revision": 3, + "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea", + "original_card": { + "id": "complex-rank-shape-decoder", + "question": "Can a decoder deliver the local paid mass in fewer, larger-rank children (block frame climbs instead of rank-1 to rank-3 steps)?", + "starting_points": [ + "research/complex-local-word-ceiling/README.md", + "research/complex-decoder-field-extension-seed44/README.md", + "research/complex-frame-pair-decoders/README.md" + ], + "methods": [ + "Find one exact small decoding identity whose frame path climbs in blocks, and price its complete per-call profile.", + "Bound the best effective child rank achievable for one fixed support alphabet, including copies, frames and restoration." + ], + "acceptance_gate": "A per-call local profile, with all copied information, frames and restoration counted, whose ceiling exceeds the selected word's by at least 5%; masked or overcomplete supports must change an assumption of the eight-term all-pairs bound.", + "first_step": { + "command": [ + "python3", + "-B", + "research/complex-local-word-ceiling/verify.py" + ], + "expected": "PASS_COMPLEX_LOCAL_WORD_CEILING", + "inspect": "Read the selected word's per-call local profile, its packing ceiling and the lever table; run levers.py for the ideal budget of the lever you target.", + "scope": "Positive control and planning budget only; this is not a new construction or full cold replay." + }, + "first_experiment": "Before any synthesis, write the candidate per-call local profile (and centre charge / unpaid coordinates if changed) and screen it with ceiling.ceiling(); reject it if even the ideal ceiling does not beat the selected word's by your stated margin. Ideal budget: rank-16 delivery is 2.31x (levers.py).", + "bottleneck_link": "Rank-1 children are about half of recursive cost; the selected word's effective child rank is about 3.9. Larger-rank delivery lowers recursive cost per unit of paid mass.", + "allowed_variations": [ + "One masked, overcomplete or block decoder family with exact labels and supports.", + "A scoped lower bound on effective rank for one alphabet.", + "If the coverage law, template or guard changes, derive an applicable fully charged replacement bound instead of applying the incumbent ceiling outside its scope." + ], + "scope_change_triggers": [ + "Repacking idle remainders of an unchanged word (covered by the packing ceiling).", + "Repeating the eight-term all-pairs search inside its proved scope." + ], + "overlap_terms": [ + "rank shape", + "block climb", + "masked decoder", + "overcomplete", + "effective rank" + ] + }, + "selection": { + "seed": "9a396c07a6d107acdb9a76567c1010d0", + "scope_key": "02b31ebd160542c86299", + "track": "complex-mechanisms", + "source": "SELECTION.json saved in the external session handoff archive" + }, + "scope_status": "changed", + "actual_scope": "Characterize clean invariant encodings E satisfying i^u C_d E = E (I_(2^s) tensor C_n), for integers n,s >= 1 and u in {0,1,2,3}: exact eigenspace domination, explicit dyadic Walsh intertwiners and decoders, least ambient width n+s+1 or n+s+2, and the full ambient-volume charge under the inherited tariff. Corroborate n,s=1..64 and small literal operator fixtures. This is an algebraic clean-complement contract and a negative tariff screen, without physical supplier admission.", + "scope_change_reason": "Fresh overlap found Arham's active Discussion #1901 claiming the full-space conjugation obstruction and opposite-direction exception. The selected physical block-climb construction card is therefore changed before implementation to the distinct clean invariant-subspace contract; the full-space endpoint is credited prior art, and this package does not satisfy the card's 5% constructive acceptance gate.", + "bottleneck_link": "Combining independently paid lanes into a larger-rank child requires the native tensor operator to preserve an encoded lane subspace. This gives an exact algebraic admission criterion and charges its compulsory extra ambient volume; even with encoder and restoration costs waived, the inherited child-budget expression exceeds the separate-lane expression by more than a factor of two.", + "budget_minutes": 60, + "session_start_utc": "2026-10-14T13:33:32Z", + "construction_cutoff_utc": "2026-10-14T14:18:32Z", + "session_end_utc": "2026-10-14T14:33:32Z", + "stop_rule": "Stop construction at 14:18:32 UTC and use the final quarter for exact receipt replay, independent review, source and metadata checks, and handoff. Restrict synthesis to explicit small Walsh fixtures and the stated n,s=1..64 corroboration; do not build Lean, run cold suppliers, or change the selected frontier.", + "outcome": "negative-result", + "evidence": "PROOF.md gives the sharp all-size single-host clean-encoding width and inherited volume tariff comparison. CERTIFICATE.json records 4096 width cases, 131 independent multiplicity counts, 12 complete literal butterfly/Gram fixtures and seven semantic/domain controls. Registered Python3.12.14 replay passes; five no-Git optimized/source/receipt/output tests pass. These are scoped algebraic and budget results, not physical supplier admission or the card construction gate.", + "author": "ToikY", + "ai_assistance": "Substantial: OpenAI Codex selected the changed bounded scope after live overlap review, derived the proof and exact checks, and wrote the implementation, documentation and package metadata; independent Codex agents reviewed mathematics and provenance.", + "predecessor_credit": [ + { + "reference": "https://github.com/CrocSwap/integer-mult-bounds/pull/679", + "author": "Greer Guthrie (g-guthrie)", + "head": "dce137e540acd2b689281afe222cd32c0ec1f1ae", + "contribution": "Monomial two-sided routing obstruction, explicit selector correction, arbitrary-dirty-padding restoration and full joined-volume accounting in research/selector-batching/README.md." + }, + { + "reference": "https://github.com/CrocSwap/integer-mult-bounds/pull/665", + "author": "Douglas R. Colkitt (Mister-Meeseeks)", + "head": "d0e4f1eb295e5cce508dc76c6937290a9175e42b", + "contribution": "Prior spectral-capacity encoder for the C_(9f) to C_(4f) direct-sum C_(5f) interface, with explicit dirty-complement restoration and a losing complete boundary bill. The general eigenspace-capacity method is prior art; the new delta is the single-host selector-lane criterion and least width." + }, + { + "reference": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1901", + "author": "Arham", + "head": null, + "contribution": "Active all-size full-space conjugation obstruction and opposite-direction exception; the trace lower endpoint is inherited, not claimed as new." + } + ], + "open_questions": [ + { + "question": "Can an explicit encoder and decoder be implemented with a complete physical, arithmetic and precision bill that is useful under a changed cost contract?", + "why_it_matters": "The exact linear injection alone is not an admitted native supplier or a runtime improvement.", + "first_step": "Choose one small Walsh injection and specify every paid encoder, decoder, phase, routing and clean-space preparation operation.", + "blocked_by": "A target-specific physical implementation and a justified cost contract beyond the inherited full-volume screen." + }, + { + "question": "What is the least additional cost to restore an arbitrary dirty complement for this selected injection?", + "why_it_matters": "The proved endpoint restores a zero complement; native interfaces may require restoration for every incoming workspace value.", + "first_step": "List the unused Walsh phases and construct the explicit inverse complement action with all work and precision charged.", + "blocked_by": "An allowed paid restoration alphabet and its complete hosting and precision obligations." + }, + { + "question": "Can a nonreciprocal input/output map avoid the invariant-subspace tariff screen while preserving the exact required lane endpoint?", + "why_it_matters": "The criterion applies to one injection and its left-inverse decoder, so it does not exclude distinct input and output maps or other recursion algorithms.", + "first_step": "State a concrete pair of input/output linear maps, the clean or dirty workspace domain, and their full per-call profile before searching.", + "blocked_by": "A distinct exact interface with source, restoration, phase and physical ownership costs specified." + } + ] +} diff --git a/research/clean-selector-embedding/VALIDATION.json b/research/clean-selector-embedding/VALIDATION.json new file mode 100644 index 0000000000..2c5a07e5ca --- /dev/null +++ b/research/clean-selector-embedding/VALIDATION.json @@ -0,0 +1,83 @@ +{ + "schema_version": 1, + "status": "PASS_SCOPED_CLEAN_ENCODING_VALIDATION", + "python": "3.12.14 (main, Aug 25 2026, 13:50:33) [Clang 22.1.3 ]", + "platform": "macOS-26.5.2-arm64-arm-64bit", + "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea", + "selected_record_sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32", + "certificate_sha256": "83a2adcb783bc3d6590d6a854e13a4698628843fe22a4fae03a61fa290e775df", + "commands": [ + { + "argv": [ + "python3.12", + "-I", + "-B", + "research/clean-selector-embedding/verify.py" + ], + "result": "PASS_CLEAN_SELECTOR_EMBEDDING width_cases4096 fixtures12 controls7" + }, + { + "argv": [ + "python3.12", + "-I", + "-O", + "-B", + "research/clean-selector-embedding/verify.py" + ], + "result": "PASS, same committed receipt; read-only" + }, + { + "argv": [ + "python3.12", + "-B", + "scripts/research_package.py", + "--package", + "research/clean-selector-embedding" + ], + "result": "PASS_REGISTERED_RESEARCH_PACKAGE outcome=negative-result; includes5 subprocess tests" + }, + { + "argv": [ + "python3.12", + "-B", + "scripts/research_package.py", + "--package", + "research/clean-selector-embedding", + "--check-only" + ], + "result": "PASS, all3 Git/SHA input pins and originalcard match" + }, + { + "argv": [ + "python3.12", + "-B", + "-m", + "unittest", + "discover", + "-s", + "tests", + "-p", + "test_research_onboarding.py", + "-v" + ], + "result": "18 tests pass" + } + ], + "independent_review": { + "kind": "bounded separate Codex agents; no human review", + "findings_addressed": [ + "PR665 spectral-capacity method credited", + "integer-to-boolean JSON aliases reject", + "literal fixtures cover declared selected phases; algebraic width signs cover all4" + ], + "separate_recurrence": "Independent agent used its own four-state recurrence for all576 n,s=1..12 and four-phase cases; lower/upper and exact phase mapping agree. Final static proof/code/metadata review found no actionable error after stated corrections." + }, + "unrun": [ + "make frontier1094-verify", + "Lean/kernel proof", + "physical encoder/decoder and selected call source admission", + "production precision/tape/compiler", + "hosted CI and independent human review" + ], + "scope": "Newpackage only; no selected supplier or frontier mutation; inherited full-volume upper-expression screen, not runtime lower bound." +} diff --git a/research/clean-selector-embedding/VERIFY.json b/research/clean-selector-embedding/VERIFY.json new file mode 100644 index 0000000000..5b41470fbe --- /dev/null +++ b/research/clean-selector-embedding/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "docs/research/agent-task-catalog.json", + "certificates/selected-result.json", + "research/selector-batching/README.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Pinned source SHA256 checks; two independent exact multiplicity oracles; n,s=1..64 fixed and optional-phase minimum-width screening; literal butterfly intertwiner and Gram left-inverse fixtures; seven domain, phase, injection and dirty-complement controls; exact CERTIFICATE.json comparison." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/test_verify.py" + ], + "timeout_seconds": 120, + "checks": "Five subprocess tests: no-Git normal/optimized export, actual pinned-source corruption, numeric receipt corruption, integer-to-boolean alias corruption, new/occupied output preservation." + } + ] +} diff --git a/research/clean-selector-embedding/test_verify.py b/research/clean-selector-embedding/test_verify.py new file mode 100644 index 0000000000..4a8de27782 --- /dev/null +++ b/research/clean-selector-embedding/test_verify.py @@ -0,0 +1,79 @@ +#!/usr/bin/env python3 +"""Actual no-Git, optimized, source/receipt corruption and output controls.""" +import hashlib +import json +from pathlib import Path +import shutil +import subprocess +import sys +import tempfile +import unittest + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parents[1] + + +class ExportChecks(unittest.TestCase): + def setUp(self): + self.temp = tempfile.TemporaryDirectory() + self.addCleanup(self.temp.cleanup) + self.root = Path(self.temp.name) + self.package = self.root / "research" / PACKAGE.name + shutil.copytree(PACKAGE, self.package) + sources = json.loads((PACKAGE / "SOURCES.json").read_text()) + for row in sources["files"]: + dest = self.root / row["path"] + dest.parent.mkdir(parents=True, exist_ok=True) + shutil.copyfile(ROOT / row["path"], dest) + + def run_check(self, *args, optimized=False): + command = [sys.executable, "-I", "-B"] + if optimized: + command.append("-O") + command += [str(self.package / "verify.py"), *args] + return subprocess.run(command, cwd=self.root, text=True, capture_output=True, timeout=30) + + def rejected(self, result, text): + self.assertNotEqual(result.returncode, 0, result.stdout) + self.assertIn(text, result.stderr) + + def test_no_git_normal_and_optimized(self): + self.assertFalse((self.root / ".git").exists()) + for mode in (False, True): + result = self.run_check(optimized=mode) + self.assertEqual(result.returncode, 0, result.stderr) + self.assertIn("PASS_CLEAN_SELECTOR_EMBEDDING", result.stdout) + + def test_source_corruption(self): + path = self.root / "research/selector-batching/README.md" + path.write_bytes(path.read_bytes() + b"\nchanged source\n") + self.rejected(self.run_check(optimized=True), "changed pinned source") + + def test_receipt_number_corruption(self): + path = self.package / "CERTIFICATE.json" + receipt = json.loads(path.read_text()) + receipt["native_d6_counts"][1] += 1 + path.write_text(json.dumps(receipt)) + self.rejected(self.run_check(optimized=True), "certificate mismatch") + + def test_receipt_boolean_alias(self): + path = self.package / "CERTIFICATE.json" + receipt = json.loads(path.read_text()) + self.assertEqual(receipt["fixtures"][0]["n"], 1) + receipt["fixtures"][0]["n"] = True + path.write_text(json.dumps(receipt)) + self.rejected(self.run_check(optimized=True), "certificate mismatch") + + def test_new_output_and_occupied_output(self): + path = self.root / "new.json" + result = self.run_check("--output", str(path), optimized=True) + self.assertEqual(result.returncode, 0, result.stderr) + self.assertEqual(json.loads(path.read_text()), + json.loads((self.package / "CERTIFICATE.json").read_text())) + before = hashlib.sha256(path.read_bytes()).hexdigest() + self.rejected(self.run_check("--output", str(path)), "FileExistsError") + self.assertEqual(hashlib.sha256(path.read_bytes()).hexdigest(), before) + + +if __name__ == "__main__": + unittest.main() diff --git a/research/clean-selector-embedding/verify.py b/research/clean-selector-embedding/verify.py new file mode 100644 index 0000000000..1f46019324 --- /dev/null +++ b/research/clean-selector-embedding/verify.py @@ -0,0 +1,237 @@ +#!/usr/bin/env python3 +"""Exact clean invariant-subspace certificates. ToikY with OpenAI Codex; Apache-2.0.""" +import argparse +from fractions import Fraction as F +from hashlib import sha256 +from math import comb +import json +from pathlib import Path + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parents[1] + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def multiplicities(n): + need(type(n) is int and n >= 0, "invalid address width") + counts = [0] * 4 + for k in range(n + 1): + counts[k % 4] += comb(n, k) + return counts + + +def character_counts(n): + # Independent roots-of-unity filter: (1+i)^n, evaluated as integer pairs. + real, imag = 1, 0 + for _ in range(n): + real, imag = real - imag, real + imag + alternating = int(n == 0) # (1-1)^n, including n=0. + nums = [2**n + alternating + 2*real, + 2**n - alternating + 2*imag, + 2**n + alternating - 2*real, + 2**n - alternating - 2*imag] + need(all(x % 4 == 0 for x in nums), "nonintegral character filter") + return [x // 4 for x in nums] + + +def feasible(n, s, d, phase=0): + need(type(n) is int and n >= 1 and type(s) is int and s >= 1, + "positive payload and selector widths required") + need(type(d) is int and d >= 0 and type(phase) is int and 0 <= phase < 4, + "invalid native width or phase") + native, target = multiplicities(d), [2**s*x for x in multiplicities(n)] + return all(native[(j-phase) % 4] >= target[j] for j in range(4)) + + +def least_width(n, s, phases=(0,)): + for d in range(n+s, n+s+3): + for phase in phases: + if feasible(n, s, d, phase): + return d, phase + raise ValueError("proved upper width failed") + + +def injection(n, s, d, phase=0): + need(feasible(n, s, d, phase), "insufficient native eigenspace") + pools = [[v for v in range(2**d) if v.bit_count() % 4 == (j-phase) % 4] + for j in range(4)] + cursor = [0] * 4 + mapping = [] + for _lane in range(2**s): + for u in range(2**n): + j = u.bit_count() % 4 + mapping.append(pools[j][cursor[j]]) + cursor[j] += 1 + return mapping + + +def validate_mapping(n, s, d, phase, mapping): + need(len(mapping) == 2**(n+s) and len(set(mapping)) == len(mapping), + "encoding is not injective") + need(all(type(v) is int and 0 <= v < 2**d for v in mapping), "encoding range") + need(all((v.bit_count()+phase) % 4 == (x % 2**n).bit_count() % 4 + for x, v in enumerate(mapping)), "encoding eigenphase mismatch") + + +def sign(x): + return -1 if x.bit_count() % 2 else 1 + + +def encoding_columns(n, s, d, mapping): + # E = H_d P (I_q tensor H_n) / 2^n; columns are exact rational vectors. + return [[F(sum(sign(u & x)*sign(mapping[lane*2**n+u] & y) + for u in range(2**n)), 2**n) + for y in range(2**d)] + for lane in range(2**s) for x in range(2**n)] + + +def add(a, b): + return a[0]+b[0], a[1]+b[1] + + +def mul(a, b): + return a[0]*b[0]-a[1]*b[1], a[0]*b[1]+a[1]*b[0] + + +def times_i(a, phase): + return (a, (-a[1], a[0]), (-a[0], -a[1]), (a[1], -a[0]))[phase] + + +def tensor_action(vector, width, phase=0): + # Literal C butterflies, without multiplicity/eigenvector formulas. + need(len(vector) == 2**width, "operator dimension") + out = list(vector) + alpha, beta = (F(1, 2), F(1, 2)), (F(1, 2), F(-1, 2)) + for bit in range(width): + step = 1 << bit + for x in range(2**width): + if not x & step: + a, b = out[x], out[x | step] + out[x] = add(mul(alpha, a), mul(beta, b)) + out[x | step] = add(mul(beta, a), mul(alpha, b)) + return [times_i(x, phase) for x in out] + + +def fixture(n, s, d, phase): + mapping = injection(n, s, d, phase) + validate_mapping(n, s, d, phase, mapping) + columns = encoding_columns(n, s, d, mapping) + ambient, payload = 2**d, len(columns) + scalar_checks = 0 + for x, column in enumerate(columns): + left = tensor_action([(a, F(0)) for a in column], d, phase) + basis = [(F(int(k == x % 2**n)), F(0)) for k in range(2**n)] + local = tensor_action(basis, n) + start = (x // 2**n)*2**n + right = [(sum(columns[start+k][y]*local[k][0] for k in range(2**n)), + sum(columns[start+k][y]*local[k][1] for k in range(2**n))) + for y in range(ambient)] + need(left == right, "literal intertwiner failed") + scalar_checks += ambient + # Independent exact Gram check gives F E=I for F=2^(n-d) E^T. + for x in range(payload): + for y in range(payload): + dot = sum(a*b for a, b in zip(columns[x], columns[y])) + need(dot == F(2**d, 2**n)*int(x == y), "left inverse failed") + return {"n": n, "s": s, "d": d, "phase": phase, + "ambient_coordinates": ambient, "payload_coordinates": payload, + "volume_ratio": str(F(ambient, payload)), + "mapping": mapping, "intertwiner_entries": scalar_checks, + "gram_entries": payload**2} + + +def rejection(action): + try: + action() + except ValueError: + return + raise ValueError("negative control was accepted") + + +def compute(): + for n in range(131): + need(multiplicities(n) == character_counts(n), "multiplicity oracles differ") + table = [] + for n in range(1, 65): + for s in range(1, 65): + N = n+s + fixed = least_width(n, s) + phased = least_width(n, s, (0, 2, 1, 3)) # Prefer real signs at equal width. + # Full-space exclusion for every allowed global fourth-root phase. + for phase in range(4): + need(not feasible(n, s, N, phase), "equal-volume encoding admitted") + need(feasible(n, s, N+2, phase), "two-bit upper bound failed") + need(fixed[0] in (N+1, N+2) and phased[0] in (N+1, N+2), "width range") + table.append([n, s, *fixed, *phased]) + fixtures = [] + for n, s in [(1,1), (1,2), (2,1), (2,2), (3,1), (1,4)]: + for phases in [(0,), (0, 2, 1, 3)]: + d, phase = least_width(n, s, phases) + fixtures.append(fixture(n, s, d, phase)) + need(least_width(1, 4) == (7, 0), "fixed-phase motivating width") + need(least_width(1, 4, (0, 2, 1, 3)) == (6, 2), "rephased motivating width") + controls = [] + rejection(lambda: injection(1, 4, 6, 0)); controls.append("insufficient i eigenspace") + m = injection(1, 4, 7) + wrong = list(m); wrong[1] = wrong[0] + rejection(lambda: validate_mapping(1, 4, 7, 0, wrong)); controls.append("duplicate eigenvector") + rejection(lambda: validate_mapping(1, 4, 7, 1, m)); controls.append("unbilled phase") + rejection(lambda: feasible(0, 1, 2)); controls.append("zero payload width") + rejection(lambda: feasible(1, 0, 2)); controls.append("no batching") + # Dirty complement is NOT restored: choose an unused non-fixed Walsh vector. + dirty = next(v for v in range(128) if v not in m and v.bit_count() % 4 != 0) + vector = [(F(sign(dirty & x)), F(0)) for x in range(128)] + after = tensor_action(vector, 7) + need(after != vector and after == [times_i(z, dirty.bit_count() % 4) for z in vector], + "dirty-complement control") + controls.append("dirty complement not restored") + # Full constant vector alone does not validate a purported full-space encoding. + ones = [(F(1), F(0))]*32 + need(tensor_action(ones, 5) == ones, "constant vector positive control") + need(not feasible(1, 4, 5), "constant-only admission") + controls.append("constant-only smoke test insufficient") + table_bytes = json.dumps(table, separators=(",", ":")).encode() + return {"status": "PASS_CLEAN_SELECTOR_EMBEDDING", "no_new_kappa": True, + "scope": "Exact invariant clean-subspace algebra; inherited full-volume tariff screen only", + "multiplicity_oracle_widths": 131, "width_cases": len(table), + "width_table_sha256": sha256(table_bytes).hexdigest(), + "fixed_width_counts": {str(k): sum(row[2]-row[0]-row[1] == k for row in table) for k in (1,2)}, + "optional_phase_width_counts": {str(k): sum(row[4]-row[0]-row[1] == k for row in table) for k in (1,2)}, + "fixtures": fixtures, "controls": controls, + "motivating_target_counts": [16,16,0,0], + "native_d6_counts": multiplicities(6), "native_d7_counts": multiplicities(7), + "tariff": "ambient/payload >= 2; B_native/B_lanes = 2^(d-n-s)*(d/n)^sigma > 2 for 0 Date: Wed, 14 Oct 2026 07:04:20 -0700 Subject: [PATCH 2/3] Clarify literal host width and unchanged spectator scope The minimum is for C_d with unchanged external spectator factors; it does not minimize active recursive rank under arbitrary spectator reassignment. Keep the exact theorem, and state explicit changed-contract examples. --- research/clean-selector-embedding/PROOF.md | 19 ++++++++++++++++++- research/clean-selector-embedding/README.md | 8 ++++++++ research/clean-selector-embedding/TASK.json | 2 +- .../clean-selector-embedding/VALIDATION.json | 3 ++- 4 files changed, 29 insertions(+), 3 deletions(-) diff --git a/research/clean-selector-embedding/PROOF.md b/research/clean-selector-embedding/PROOF.md index 71e12b0796..0ff68f9db9 100644 --- a/research/clean-selector-embedding/PROOF.md +++ b/research/clean-selector-embedding/PROOF.md @@ -14,7 +14,12 @@ C=((1+i)I+(1-i)X)/2,\qquad C_d=C^{\otimes d},\qquad C_0=I. Fix integers \(n,s\geq1\), put \(q=2^s\), \(N=n+s\), and let \(B=I_q\otimes C_n\). The active dimension is \(D=2^N\). The optional phase convention is \(i^uC_d\), with \(u\in\{0,1,2,3\}\); -the fixed convention means \(u=0\). +the fixed convention means \(u=0\). Here \(d\) counts all axes of this literal +\(C_d\) host: there is no additional variable spectator factor in the existence +problem. If each lane has a separate common spectator fiber, this result +extends only by \(E\otimes I\), keeping that same fiber unchanged and outside +the encoding. Neither the minimum width nor the budget formula below covers +arbitrary changes to the native/spectator split. ## Exact existence and least ambient dimension @@ -176,6 +181,18 @@ The finite example \(C_7\) must not be relabeled \(C_{7f}\) while retaining its constant fourfold volume. Scaling selector width as well changes the lane count and must charge that volume explicitly. +Allowing a different spectator factor changes the minimum active width. For +example, \(I_{16}\otimes C_1\otimes I_{256}\) is permutation-equivalent to +\(C_1\otimes I_{4096}\). This keeps all 8192 coordinates and native width one, +with the same volume-linear budget as sixteen original lanes. Also, the +different host \(C_2\otimes I_{4096}\) has multiplicities +\((4096,8192,4096,0)\), dominating the payload's \((4096,4096,0,0)\), and +admits a clean encoding on 16384 ambient coordinates. Its separate budget +ratio is \(2\cdot2^\sigma>2\). Neither example contradicts the literal +width-seven result: both change the spectator factor. The displayed general +\(2^{d-N}(d/n)^\sigma\) formula must not be applied to that changed model; +its full dimension and cost invoice must be derived separately. + The retained [selector-batching note](../selector-batching/README.md) supplies the kernel convention, monomial support obstruction, arbitrary-dirty-padding restoration and volume accounting. This result changes its hypothesis to a diff --git a/research/clean-selector-embedding/README.md b/research/clean-selector-embedding/README.md index 934b7431ad..f910910b2a 100644 --- a/research/clean-selector-embedding/README.md +++ b/research/clean-selector-embedding/README.md @@ -9,6 +9,14 @@ least native width is **`n+s+1` or `n+s+2`**, decided by four integer inequaliti [PROOF.md](PROOF.md) gives the all-size argument and an explicit dyadic Walsh encoding; the finite checker is separate evidence. +This minimum is for the literal host `C_d` with no extra variable spectator +factor. Common spectator fibers extend the result only by `E tensor I`, with +the same fibers separate from the encoding. Reassigning them changes the +contract; neither the minimum width nor the budget formula below covers that +model. PROOF.md gives an unchanged-volume width-one example and a distinct +twofold-volume width-two example. This is not a minimum supplier recursive-rank +theorem. + The motivating 16-lane, width-one target has multiplicities `(16,16,0,0)`: | Native width | Multiplicities of C_d | Exact phase | Optional phase | diff --git a/research/clean-selector-embedding/TASK.json b/research/clean-selector-embedding/TASK.json index 3b9e356aa7..3da71d40f1 100644 --- a/research/clean-selector-embedding/TASK.json +++ b/research/clean-selector-embedding/TASK.json @@ -52,7 +52,7 @@ "source": "SELECTION.json saved in the external session handoff archive" }, "scope_status": "changed", - "actual_scope": "Characterize clean invariant encodings E satisfying i^u C_d E = E (I_(2^s) tensor C_n), for integers n,s >= 1 and u in {0,1,2,3}: exact eigenspace domination, explicit dyadic Walsh intertwiners and decoders, least ambient width n+s+1 or n+s+2, and the full ambient-volume charge under the inherited tariff. Corroborate n,s=1..64 and small literal operator fixtures. This is an algebraic clean-complement contract and a negative tariff screen, without physical supplier admission.", + "actual_scope": "Characterize clean invariant encodings E satisfying i^u C_d E = E (I_(2^s) tensor C_n), for integers n,s >= 1 and u in {0,1,2,3}: exact eigenspace domination, explicit dyadic Walsh intertwiners and decoders, least ambient width n+s+1 or n+s+2, and the full ambient-volume charge under the inherited tariff. Corroborate n,s=1..64 and small literal operator fixtures. This is an algebraic clean-complement contract and a negative tariff screen, without physical supplier admission. The least d is for literal C_d without a separately variable spectator factor; common spectator extension is E tensor I with the same factor. Arbitrary spectator reassignment is outside that minimum-width and cost formula.", "scope_change_reason": "Fresh overlap found Arham's active Discussion #1901 claiming the full-space conjugation obstruction and opposite-direction exception. The selected physical block-climb construction card is therefore changed before implementation to the distinct clean invariant-subspace contract; the full-space endpoint is credited prior art, and this package does not satisfy the card's 5% constructive acceptance gate.", "bottleneck_link": "Combining independently paid lanes into a larger-rank child requires the native tensor operator to preserve an encoded lane subspace. This gives an exact algebraic admission criterion and charges its compulsory extra ambient volume; even with encoder and restoration costs waived, the inherited child-budget expression exceeds the separate-lane expression by more than a factor of two.", "budget_minutes": 60, diff --git a/research/clean-selector-embedding/VALIDATION.json b/research/clean-selector-embedding/VALIDATION.json index 2c5a07e5ca..2e83add290 100644 --- a/research/clean-selector-embedding/VALIDATION.json +++ b/research/clean-selector-embedding/VALIDATION.json @@ -68,7 +68,8 @@ "findings_addressed": [ "PR665 spectral-capacity method credited", "integer-to-boolean JSON aliases reject", - "literal fixtures cover declared selected phases; algebraic width signs cover all4" + "literal fixtures cover declared selected phases; algebraic width signs cover all4", + "Literal width and budget theorem explicitly limits spectator extension to E tensor I with the same factor. Independent recurrence checks changed-host example counts; permutation C1 tensor I4096 also keeps8192 coordinates at width1 and budget tie. Arbitrary spectator reassignment is outside the theorem." ], "separate_recurrence": "Independent agent used its own four-state recurrence for all576 n,s=1..12 and four-phase cases; lower/upper and exact phase mapping agree. Final static proof/code/metadata review found no actionable error after stated corrections." }, From 0a7c54dd94bce3784b61c4203adfdda98d13d53d Mon Sep 17 00:00:00 2001 From: ToikY <27568617+ToikY@users.noreply.github.com> Date: Wed, 14 Oct 2026 07:11:23 -0700 Subject: [PATCH 3/3] Give the sharp closed residue formula for clean tensor encoding widths Pascal averaging resolves all positive widths: optional phase always needs one extra axis, and fixed-phase exceptions are exactly the two small-width residue classes. Corroborate the written proof with independent exact count oracles. --- .../clean-selector-embedding/CERTIFICATE.json | 17 +++++ research/clean-selector-embedding/PROOF.md | 70 ++++++++++++++++++- research/clean-selector-embedding/README.md | 13 ++++ research/clean-selector-embedding/TASK.json | 4 +- .../clean-selector-embedding/VALIDATION.json | 5 +- research/clean-selector-embedding/VERIFY.json | 2 +- research/clean-selector-embedding/verify.py | 18 +++++ 7 files changed, 123 insertions(+), 6 deletions(-) diff --git a/research/clean-selector-embedding/CERTIFICATE.json b/research/clean-selector-embedding/CERTIFICATE.json index d1e0afd187..b35afaa890 100644 --- a/research/clean-selector-embedding/CERTIFICATE.json +++ b/research/clean-selector-embedding/CERTIFICATE.json @@ -5,6 +5,23 @@ "multiplicity_oracle_widths": 131, "width_cases": 4096, "width_table_sha256": "12873f0c677ad03b12084ccd8272ce8c006caa334c08c262c2512f633ee04637", + "closed_width_formula": { + "fixed_n1_extra1_s_mod8": [ + 0, + 6, + 7 + ], + "fixed_n2_extra1_s_mod8": [ + 0, + 1, + 5, + 6, + 7 + ], + "fixed_n_at_least3_extra": 1, + "fixed_other_small_cases_extra": 2, + "optional_fourth_root_phase_extra": 1 + }, "fixed_width_counts": { "1": 4032, "2": 64 diff --git a/research/clean-selector-embedding/PROOF.md b/research/clean-selector-embedding/PROOF.md index 0ff68f9db9..62b7b09627 100644 --- a/research/clean-selector-embedding/PROOF.md +++ b/research/clean-selector-embedding/PROOF.md @@ -62,7 +62,7 @@ there is no additional Jordan-block condition. For each fixed \(u\), the least legal \(d\) is exactly one of \(N+1,N+2\): test (1) at \(d=N+1\), taking that value if it passes and \(N+2\) otherwise. If any of the four phases is permitted, test all four at \(N+1\); the least -dimension is \(N+1\) if one passes, otherwise \(N+2\). +dimension is always \(N+1\), as the closed classification below proves. Here is the uniform proof. Dimension forces \(d\geq N\). At \(d=N\), an injective \(E\) would be invertible and give a full-space similarity. But @@ -96,6 +96,74 @@ This proves (1) simultaneously for all four phases. These real expressions are only the written bound; exact finite certificates can use the integer binomial sums or the recurrence \(m_{d+1}(j)=m_d(j)+m_d(j-1)\). +### Closed classification + +Within the literal-host contract above, the fixed-phase minimum is + +| Payload width | Condition for minimum \(d=N+1\) | Otherwise | +| --- | --- | --- | +| \(n=1\) | \(s\bmod8\in\{0,6,7\}\) | \(d=N+2\) | +| \(n=2\) | \(s\bmod8\in\{0,1,5,6,7\}\) | \(d=N+2\) | +| \(n\geq3\) | Every \(s\geq1\) | No other case | + +If any fourth-root phase is permitted, the minimum is \(N+1\) for every +\(n,s\geq1\). This is a specialization of the credited PR665 spectral-capacity +method, using Pascal's recurrence to bound the normalized multiplicities; no +claim of priority for the recurrence or averaging argument is made. + +To prove the classification, put \(p_k(j)=m_k(j)/2^k\). Pascal's recurrence +becomes + +\[ +p_{k+1}(j)=\tfrac12(p_k(j)+p_k(j-1)). +\] + +Thus \(\min_jp_k(j)\) is nondecreasing and \(\max_jp_k(j)\) is nonincreasing. +At \(d=N+1\), criterion (1) is exactly +\(2p_d(j-u)\geq p_n(j)\) for all four classes. + +For \(n\geq3\), \(\max_jp_n(j)\leq\max_jp_3(j)=3/8\). Also +\(d\geq5\), so \(\min_jp_d(j)\geq\min_jp_5(j)=3/16\). +Therefore \(2\min_jp_d(j)\geq\max_jp_n(j)\), proving feasibility for every +phase, not just phase zero. + +For \(n=2\), \(p_2=(1/4,1/2,1/4,0)\) and \(d=s+3\geq4\). +The bound \(\min_jp_d(j)\geq\min_jp_4(j)=1/8\) handles all nonpeak target +classes for every phase. The remaining peak condition is +\(m_d(1-u)\geq2^{d-2}\). By the character formula, it is equivalent to + +\[ +\sin(d\pi/4+u\pi/2)\geq0, +\quad\text{or}\quad(d+2u)\bmod8\in\{0,1,2,3,4\}. +\] + +For \(u=0\), substituting \(d=s+3\) gives the table's five residue classes. +With a phase choice, some native class has density at least the average +\(1/4\); rotate the target peak to that class. The nonpeak bound still applies, +so an allowed phase always works at \(N+1\). + +For \(n=1\), \(p_1=(1/2,1/2,0,0)\) and \(d=s+2\geq3\). The two required +native classes must both have density at least \(1/4\). The character formula +therefore gives exactly + +\[ +\cos(d\pi/4+u\pi/2)\geq0,\qquad +\sin(d\pi/4+u\pi/2)\geq0, +\] + +or \((d+2u)\bmod8\in\{0,1,2\}\). Phase zero gives +\(s\bmod8\in\{0,6,7\}\). For any \(d\), the four deviations from the average +are a positive common factor times \((c,t,-c,-t)\), where +\(c=\cos(d\pi/4)\) and \(t=\sin(d\pi/4)\). At least one adjacent cyclic pair +is nonnegative: choose the pair in the quadrant of \((c,t)\), allowing a zero +on its boundary. A phase rotation maps the two target classes to that pair, +proving optional-phase feasibility at \(N+1\). + +Failures at \(N+1\) in the fixed-phase table have minimum \(N+2\) by the +uniform upper endpoint and the exclusion at \(N\) already proved. The cases +\(n=0\) and \(s=0\) are excluded from this statement; they do not inherit this +positive-payload, genuine-batching classification. + If an arbitrary scalar phase \(\lambda\) is proposed, the target has a nonzero eigenspace of eigenvalue 1. Intertwining into \(\lambda C_d\) therefore forces \(\lambda i^k=1\) for some integer \(k\). Thus the four phases above exhaust diff --git a/research/clean-selector-embedding/README.md b/research/clean-selector-embedding/README.md index f910910b2a..6bfc2132ba 100644 --- a/research/clean-selector-embedding/README.md +++ b/research/clean-selector-embedding/README.md @@ -17,6 +17,19 @@ model. PROOF.md gives an unchanged-volume width-one example and a distinct twofold-volume width-two example. This is not a minimum supplier recursive-rank theorem. +The sharp closed formula, with `N=n+s`, is: + +| Convention | Least d | +| --- | --- | +| Exact phase, `n>=3` | `N+1` | +| Exact phase, `n=2` and `s mod 8` in `{0,1,5,6,7}` | `N+1` | +| Exact phase, `n=1` and `s mod 8` in `{0,6,7}` | `N+1` | +| Other exact-phase cases | `N+2` | +| Any fourth-root global phase allowed | `N+1` | + +Pascal averaging and the eight-residue character signs prove this for every +positive `n,s`; finite enumeration corroborates the formula separately. + The motivating 16-lane, width-one target has multiplicities `(16,16,0,0)`: | Native width | Multiplicities of C_d | Exact phase | Optional phase | diff --git a/research/clean-selector-embedding/TASK.json b/research/clean-selector-embedding/TASK.json index 3da71d40f1..03c0bdccc4 100644 --- a/research/clean-selector-embedding/TASK.json +++ b/research/clean-selector-embedding/TASK.json @@ -52,7 +52,7 @@ "source": "SELECTION.json saved in the external session handoff archive" }, "scope_status": "changed", - "actual_scope": "Characterize clean invariant encodings E satisfying i^u C_d E = E (I_(2^s) tensor C_n), for integers n,s >= 1 and u in {0,1,2,3}: exact eigenspace domination, explicit dyadic Walsh intertwiners and decoders, least ambient width n+s+1 or n+s+2, and the full ambient-volume charge under the inherited tariff. Corroborate n,s=1..64 and small literal operator fixtures. This is an algebraic clean-complement contract and a negative tariff screen, without physical supplier admission. The least d is for literal C_d without a separately variable spectator factor; common spectator extension is E tensor I with the same factor. Arbitrary spectator reassignment is outside that minimum-width and cost formula.", + "actual_scope": "Characterize clean invariant encodings E satisfying i^u C_d E = E (I_(2^s) tensor C_n), for integers n,s >= 1 and u in {0,1,2,3}: exact eigenspace domination, explicit dyadic Walsh intertwiners and decoders, least ambient width n+s+1 or n+s+2, and the full ambient-volume charge under the inherited tariff. Corroborate n,s=1..64 and small literal operator fixtures. This is an algebraic clean-complement contract and a negative tariff screen, without physical supplier admission. The least d is for literal C_d without a separately variable spectator factor; common spectator extension is E tensor I with the same factor. Arbitrary spectator reassignment is outside that minimum-width and cost formula. Give the sharp closed residue classification: fixed phase n>=3 always uses one extra axis; at n=1 selector residues0,6,7 pass with one extra, at n=2 residues0,1,5,6,7 do; other fixed small cases require two. Optional fourth-root phase always needs exactly one extra axis.", "scope_change_reason": "Fresh overlap found Arham's active Discussion #1901 claiming the full-space conjugation obstruction and opposite-direction exception. The selected physical block-climb construction card is therefore changed before implementation to the distinct clean invariant-subspace contract; the full-space endpoint is credited prior art, and this package does not satisfy the card's 5% constructive acceptance gate.", "bottleneck_link": "Combining independently paid lanes into a larger-rank child requires the native tensor operator to preserve an encoded lane subspace. This gives an exact algebraic admission criterion and charges its compulsory extra ambient volume; even with encoder and restoration costs waived, the inherited child-budget expression exceeds the separate-lane expression by more than a factor of two.", "budget_minutes": 60, @@ -61,7 +61,7 @@ "session_end_utc": "2026-10-14T14:33:32Z", "stop_rule": "Stop construction at 14:18:32 UTC and use the final quarter for exact receipt replay, independent review, source and metadata checks, and handoff. Restrict synthesis to explicit small Walsh fixtures and the stated n,s=1..64 corroboration; do not build Lean, run cold suppliers, or change the selected frontier.", "outcome": "negative-result", - "evidence": "PROOF.md gives the sharp all-size single-host clean-encoding width and inherited volume tariff comparison. CERTIFICATE.json records 4096 width cases, 131 independent multiplicity counts, 12 complete literal butterfly/Gram fixtures and seven semantic/domain controls. Registered Python3.12.14 replay passes; five no-Git optimized/source/receipt/output tests pass. These are scoped algebraic and budget results, not physical supplier admission or the card construction gate.", + "evidence": "PROOF.md gives the sharp all-size single-host clean-encoding width and inherited volume tariff comparison. CERTIFICATE.json records 4096 width cases, 131 independent multiplicity counts, 12 complete literal butterfly/Gram fixtures and seven semantic/domain controls. Registered Python3.12.14 replay passes; five no-Git optimized/source/receipt/output tests pass. These are scoped algebraic and budget results, not physical supplier admission or the card construction gate. The closed all-size residue formula is separately corroborated in all4096 finite width cases.", "author": "ToikY", "ai_assistance": "Substantial: OpenAI Codex selected the changed bounded scope after live overlap review, derived the proof and exact checks, and wrote the implementation, documentation and package metadata; independent Codex agents reviewed mathematics and provenance.", "predecessor_credit": [ diff --git a/research/clean-selector-embedding/VALIDATION.json b/research/clean-selector-embedding/VALIDATION.json index 2e83add290..86180cda7c 100644 --- a/research/clean-selector-embedding/VALIDATION.json +++ b/research/clean-selector-embedding/VALIDATION.json @@ -5,7 +5,7 @@ "platform": "macOS-26.5.2-arm64-arm-64bit", "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea", "selected_record_sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32", - "certificate_sha256": "83a2adcb783bc3d6590d6a854e13a4698628843fe22a4fae03a61fa290e775df", + "certificate_sha256": "9b48ea90df1d17655f92604ad4e1e1d065989a7c0190cf3b3db7349adc21251a", "commands": [ { "argv": [ @@ -71,7 +71,8 @@ "literal fixtures cover declared selected phases; algebraic width signs cover all4", "Literal width and budget theorem explicitly limits spectator extension to E tensor I with the same factor. Independent recurrence checks changed-host example counts; permutation C1 tensor I4096 also keeps8192 coordinates at width1 and budget tie. Arbitrary spectator reassignment is outside the theorem." ], - "separate_recurrence": "Independent agent used its own four-state recurrence for all576 n,s=1..12 and four-phase cases; lower/upper and exact phase mapping agree. Final static proof/code/metadata review found no actionable error after stated corrections." + "separate_recurrence": "Independent agent used its own four-state recurrence for all576 n,s=1..12 and four-phase cases; lower/upper and exact phase mapping agree. Final static proof/code/metadata review found no actionable error after stated corrections.", + "closed_formula": "A separate agent four-state Pascal recurrence (no package imports) agrees on all4096 pairs:4032 fixed-phase +1,64 fixed-phase +2, all optional-phase +1. Independent written-proof review validates monotone normalized counts, small-width residue signs, and phase rotations." }, "unrun": [ "make frontier1094-verify", diff --git a/research/clean-selector-embedding/VERIFY.json b/research/clean-selector-embedding/VERIFY.json index 5b41470fbe..f79a99f0e6 100644 --- a/research/clean-selector-embedding/VERIFY.json +++ b/research/clean-selector-embedding/VERIFY.json @@ -17,7 +17,7 @@ "{package}/verify.py" ], "timeout_seconds": 120, - "checks": "Pinned source SHA256 checks; two independent exact multiplicity oracles; n,s=1..64 fixed and optional-phase minimum-width screening; literal butterfly intertwiner and Gram left-inverse fixtures; seven domain, phase, injection and dirty-complement controls; exact CERTIFICATE.json comparison." + "checks": "Pinned source SHA256 checks; two independent exact multiplicity oracles; n,s=1..64 fixed and optional-phase minimum-width screening; literal butterfly intertwiner and Gram left-inverse fixtures; seven domain, phase, injection and dirty-complement controls; exact CERTIFICATE.json comparison. Exact closed width classification independently compared with count-based minima at every finite pair." }, { "argv": [ diff --git a/research/clean-selector-embedding/verify.py b/research/clean-selector-embedding/verify.py index 1f46019324..6fe0577034 100644 --- a/research/clean-selector-embedding/verify.py +++ b/research/clean-selector-embedding/verify.py @@ -55,6 +55,16 @@ def least_width(n, s, phases=(0,)): raise ValueError("proved upper width failed") +def fixed_width_formula(n, s): + # Closed all-size classification; checked below by independent count oracles. + extra = 1 + if n == 1 and s % 8 not in (0, 6, 7): + extra = 2 + elif n == 2 and s % 8 not in (0, 1, 5, 6, 7): + extra = 2 + return n+s+extra + + def injection(n, s, d, phase=0): need(feasible(n, s, d, phase), "insufficient native eigenspace") pools = [[v for v in range(2**d) if v.bit_count() % 4 == (j-phase) % 4] @@ -166,6 +176,8 @@ def compute(): need(not feasible(n, s, N, phase), "equal-volume encoding admitted") need(feasible(n, s, N+2, phase), "two-bit upper bound failed") need(fixed[0] in (N+1, N+2) and phased[0] in (N+1, N+2), "width range") + need(fixed[0] == fixed_width_formula(n, s), "closed fixed-width classification") + need(phased[0] == N+1, "closed optional-phase classification") table.append([n, s, *fixed, *phased]) fixtures = [] for n, s in [(1,1), (1,2), (2,1), (2,2), (3,1), (1,4)]: @@ -199,6 +211,12 @@ def compute(): "scope": "Exact invariant clean-subspace algebra; inherited full-volume tariff screen only", "multiplicity_oracle_widths": 131, "width_cases": len(table), "width_table_sha256": sha256(table_bytes).hexdigest(), + "closed_width_formula": { + "fixed_n1_extra1_s_mod8": [0,6,7], + "fixed_n2_extra1_s_mod8": [0,1,5,6,7], + "fixed_n_at_least3_extra": 1, + "fixed_other_small_cases_extra": 2, + "optional_fourth_root_phase_extra": 1}, "fixed_width_counts": {str(k): sum(row[2]-row[0]-row[1] == k for row in table) for k in (1,2)}, "optional_phase_width_counts": {str(k): sum(row[4]-row[0]-row[1] == k for row in table) for k in (1,2)}, "fixtures": fixtures, "controls": controls,