diff --git a/research/encoded-bank-criterion-audit/AUDIT.md b/research/encoded-bank-criterion-audit/AUDIT.md new file mode 100644 index 0000000000..61559736f1 --- /dev/null +++ b/research/encoded-bank-criterion-audit/AUDIT.md @@ -0,0 +1,173 @@ +# Independent proof audit of PR2872 + +DLamdata with substantial OpenAI Codex assistance, including a separate +verifier agent. Apache-2.0. + +Audited commit: `cc5c2398505447a321fb9f9826163825e3b269fd`. +[Original proof](https://github.com/tekuuu/integer-mult-bounds/blob/cc5c2398505447a321fb9f9826163825e3b269fd/research/encoded-phase-bank/PROOF.md), +SHA256 `154cf967411b93da3a5c56c84c4f8a62f62192448c14c08e510e830054897bf9`. +The lead authenticated the frozen tree against Git; the verifier agent derived +these arguments from the model statement before opening the source proof, +then compared them. Both share the stated contract. This is a separate AI +review, not an independent human review or formal-kernel verification. + +**Verdict:** no substantive gap found in Theorem 1, Lemma 2, Theorem 3, +Lemma 4 or Corollary 5 under the stated contract. All mathematical claims +remain credited to Tekalign and the predecessors named in the source. +No new supplier, native cost result or exponent improvement is claimed. + +## Derivation before source inspection + +Write `epsilon_j=(-1)^(u_j dot v_j)` and `P_j=B_j(v_j)A_j(u_j)`. +Homomorphisms from a binary vector group give involutions, identity at zero, +and commuting generators within each A or B family. + +### 1. Exact paired-word criterion + +Setting every other label to zero leaves `P_j^2=epsilon_j I`. +Since A and B are involutions, this is equivalent to +`A_j(u)B_j(v)=epsilon_j B_j(v)A_j(u)`. Thus the within-column +Weyl relation is necessary for every u and v. + +If the occurrences of i and j alternate, isolate one A or B label +generator in each column and set all other labels to zero. The desired +phase is one, and the two surviving operators S,T are involutions. The +endpoint is `(ST)^2=I` or `(TS)^2=I`, according to multiplication convention. +Either equation is equivalent to ST=TS. The four choices A/A, A/B, B/A, +B/B therefore force all four crossing commutations. Generator commutation +extends to the full homomorphic families. This uses independence of labels; +a cancellation among correlated labels could not justify the same step. + +Conversely, among the pairs remaining in the word choose one with the +shortest distance between its two occurrences. Its interior contains no +complete pair, since such a pair would have smaller distance. Each interior +symbol has its other occurrence outside, so it alternates with the chosen +pair and its P commutes with the chosen P. Move the chosen P through this +interior, replace its square by epsilon, and delete the pair. The relative +order of every other pair is unchanged; hence every crossing in the reduced +word was already a crossing. Induction yields the product of all epsilon_j. +This does not impose commutation on nested or disjoint columns. + +This derivation establishes the exact criterion for arbitrary invertible +complex matrices, not just signed permutations, Paulis, or unitary matrices. +Reversing matrix multiplication to account for chronological action changes +none of the conclusions. + +### 2. Producer-prefix dimensions + +Define a partial order by `i < j` in the natural producer order and i +preceding j in the consumer permutation. Crossings are precisely comparable +pairs, and cliques are increasing subsequences. + +For a clique with total rank R, collect all its binary-coordinate A and B +generators as Z_a and X_a. All Z's commute; each satisfies `Z_a^2=I`. +Over C these generators are diagonalizable because their minimal polynomials +divide `(t-1)(t+1)`, which has distinct roots. Commuting diagonalizable +operators have a simultaneous eigenspace decomposition +`V = direct_sum_s V_s` for s in `F2^R`. No normality or inner-product +argument is needed. X_a is invertible and sends V_s bijectively to +V_(s+e_a), because it anticommutes with Z_a and commutes with the other +Z's. These translations act transitively on the indices. At least one +eigenspace is nonzero, so all 2^R eigenspaces have equal positive dimension. +Consequently `2^R | d`. A maximum-weight chain gives `2^W | d`. + +For the upper bound, process columns in consumer order. Set the start of +column j to the largest endpoint of an earlier smaller column, or zero; +give j the next r_j integer slots. Its endpoint is the maximum weight of +an increasing subsequence ending at j. Thus no slot exceeds W-1, and +comparable columns receive disjoint slots. On W binary coordinates, +use the standard Z/X pair at these slots for A_j/B_j. Each column has +the right dot-product relation and crossing columns commute, so the paired +word criterion applies. The dimension is `2^W`. Taking a direct sum of +any positive number of identical representations realizes every positive +multiple of `2^W`. + +Zero ranks cause no difficulty: their label groups and slot intervals are +empty, and they contribute zero to every clique weight. In the eigenspace +proof R=0 gives one eigenspace and the vacuous divisibility `1 | d`. +If every rank is zero, all operators are identities and every d>=1 works. +The nonempty-bank requirement is essential to the step that some eigenspace +is nonzero. + +### 3. The C5 minimum + +The occurrence positions of the word `0 1 4 0 3 4 2 3 1 2` are: + +| Column | Positions (zero based) | +| --- | --- | +| 0 | 0, 3 | +| 1 | 1, 8 | +| 2 | 6, 9 | +| 3 | 4, 7 | +| 4 | 2, 5 | + +The alternating pairs are exactly `01,12,23,34,40`. Each scalar column +generates an algebra isomorphic to M2(C). To see this without a unitary +assumption, diagonalize its A; B bijects its plus and minus eigenspaces. +Choose a basis in the plus eigenspace and use its B image in the minus +eigenspace. Then A is `diag(I,-I)` and B swaps the two blocks. The generated +algebra is `M2 tensor I_m` and its commutant is `I_2 tensor M_m`, with +`d=2m`. + +An edge already forces `4 | d`. At d=4, the algebra of column 0 and the +commuting algebra of its neighbor 1 are complementary copies of M2. Each +has a four-dimensional commutant. Column 2 commutes with column 1; its +four-dimensional algebra is contained in that commutant and must equal +column 0's algebra. Similarly column 4's algebra equals column 1's. +Column 3 commutes with both 2 and 4, so its algebra would be in the common +commutant of the two complementary M2's, namely the scalars. That contradicts +its anticommuting involution pair. Thus d=4 is impossible. Together with +`4 | d`, this leaves d>=8. Assigning the coordinate colors `(0,1,0,1,2)` +to columns gives an explicit d=8 representation. + +This proves the stated minimum. It does not assert that every possible +larger dimension is a multiple of eight, or that clique/coloring formulas +classify every paired schedule. + +## Comparison with the frozen proof and existing checks + +The frozen proof agrees with each derivation above. Its sparse-label +necessity is sufficient because the labels are independent. Its shortest +interval argument remains valid after deletions. Its simultaneous +diagonalization needs no omitted unitary assumption. Its d=4 commutant +inclusion becomes equality because both spaces have dimension four; the +displayed block form also proves the double-commutant identity it uses. +The proof's stronger odd-cycle statement follows by repeatedly alternating +an algebra with its commutant along a path. + +Existing `verify.py` already tests Pauli phase polynomials, weighted +permutations including ranks zero, and the two-qubit symplectic-plane +commutant graph. Existing `independent.py` already tests exact dense +nonunitary endpoint fixtures. Existing `test_package.py` already isolates +all four crossing relations. Repeating those checks would not create a +new independent mathematical implication, and this subtask did not rerun +the existing suite. + +The source package’s `verify.py` rejects an empty schedule. The proof's mathematical +extension to zero columns is trivial with W=0, but executable coverage should +not be described as including f=0. This is a scope observation, not a defect +in the claims reviewed here. + +## Additional exact witness + +`commutant.py` is a new, standalone Fraction/RREF computation. It +imports no candidate or predecessor implementation. Starting with two local +M2 factors on C4, it conjugates them by an explicit nonorthogonal rational +basis change and solves unrestricted matrix equations `MG-GM=0` in all +16 unknown entries. The check verifies a nonunitary generator, both +four-dimensional algebras, their four-dimensional complementary commutants, +the double commutant, a one-dimensional common commutant, and the full +16-dimensional joint algebra. This directly checks the exact linear-algebra +step behind the d=4 obstruction in a nonunitary fixture; the existing +symplectic-plane census does not perform this unrestricted centralizer solve. + +The result is `PASS_EXACT_NONUNITARY_D4_COMMUTANT` in +`COMMUTANT.json`. Boundary controls verify that dropping B leaves +an eight-dimensional centralizer, dropping the second neighboring algebra +leaves a four-dimensional one, and changing a single pair's multiplicity +to three in C6 gives a nine-dimensional centralizer. The last control +guards against generalizing the d=4 equal-dimension step to other d; it +does not claim a valid d=6 crossing-edge representation. + +This finite rational witness is corroboration, not an exhaustive check of +complex representations. Universal validity rests on the derivation above. diff --git a/research/encoded-bank-criterion-audit/COMMUTANT.json b/research/encoded-bank-criterion-audit/COMMUTANT.json new file mode 100644 index 0000000000..6cdf3c0050 --- /dev/null +++ b/research/encoded-bank-criterion-audit/COMMUTANT.json @@ -0,0 +1,24 @@ +{ + "algebra_dimensions": [ + 4, + 4 + ], + "arithmetic": "Fraction exact rational RREF on unrestricted matrix entries", + "candidate_imports": [], + "common_commutant_dimension": 1, + "commutant_dimensions": [ + 4, + 4 + ], + "dimension": 4, + "double_commutant_dimension": 4, + "failure_controls": { + "d6_single_pair_centralizer_dimension": 9, + "drop_B_centralizer_dimension": 8, + "drop_second_neighbor_centralizer_dimension": 4 + }, + "joint_algebra_dimension": 16, + "limitation": "Finite witness only; all-GL result rests on the written proof", + "nonunitary_generator": true, + "status": "PASS_EXACT_NONUNITARY_D4_COMMUTANT" +} diff --git a/research/encoded-bank-criterion-audit/INTERNAL-REVIEW.md b/research/encoded-bank-criterion-audit/INTERNAL-REVIEW.md new file mode 100644 index 0000000000..4ff26a3010 --- /dev/null +++ b/research/encoded-bank-criterion-audit/INTERNAL-REVIEW.md @@ -0,0 +1,53 @@ +# Internal review and resolution + +Two focused native Codex subagents supported this audit. This is separate AI +checking under shared model assumptions, not independent human review, maintainer +acceptance or formal-kernel verification. + +The verifier derived the criterion, weighted dimension argument and C5 exclusion +from the explicit model before inspecting PR2872's proof. Its derivation is in +AUDIT.md. It then implemented the rational centralizer witness without importing +predecessor code. The lead authenticated the input tree and replayed all three +predecessor command bodies; exact pins/output are in SOURCE-REPLAY.json. + +The skeptical reviewer read a frozen package and the exact source proof. It found +no substantive mathematical or executable defect. It independently enumerated +all labeled paired words through four columns, using swap-connected components +and recursive deletion rather than the new piling routine. Its portable +`review_words.py` retains that oracle, comparing 162,014 cases with the new checker +and its receipt. It is now a registered command. The reviewer also independently +authenticated all 13 source Git bindings and both provenance files and checked +the centralizer fixture via matrix-unit commutators, exact kernel membership and +ranks modulo 101/103. Those finite-field ranks were used only with exact rational +nullspace witnesses; none is a statement about all complex representations. + +Two low-severity wording issues were resolved: + +1. The main census uses canonical paired words up to global relabeling. README + and VERIFY.json now say this explicitly; the all-graph census and independent + fully labeled check support the symmetry reduction. +2. The empty-schedule rejection in AUDIT.md belongs to the source package's + `verify.py`; the new checker deliberately includes the empty word. The text + now names the source package explicitly. + +Neither finding required changing the two mathematical checker implementations. +The portable reviewer script changes only location/output plumbing from the +reviewer's scratch version and omits its separate local-Git authentication stage. +The final narrow review confirmed AST identity of all six retained functions +and unchanged hashes for the first two checkers. The lead then completed the +final three-command replay and relocated/read-only check of the third script. +The tested environment is Linux; the reviewer script uses Unix resource metrics. +It imports this package's checker only for comparison; its rewrite oracle does +not use that checker's piling, crossings or word enumeration. + +Reproduction: + +```sh +python3.12 scripts/research_package.py --package research/encoded-bank-criterion-audit +``` + +The lead additionally ran both receipt corruptions (expected nonzero exits), +optimized relocated Git-free/read-only replay, source-byte preflight, and final +upstream/overlap checks. Validation scope and results are recorded in +VALIDATION.json. Native costs, physical caller implementation, the full selected +cold replay and the complete multiplication theorem remain unreviewed. diff --git a/research/encoded-bank-criterion-audit/README.md b/research/encoded-bank-criterion-audit/README.md new file mode 100644 index 0000000000..c74aeac0a6 --- /dev/null +++ b/research/encoded-bank-criterion-audit/README.md @@ -0,0 +1,106 @@ +# Independent audit of the encoded-bank crossing theorem + +**Independent audit; no substantive gap found and no new bound claimed.** This +package checks [PR2872](https://github.com/CrocSwap/integer-mult-bounds/pull/2872) +at `cc5c2398505447a321fb9f9826163825e3b269fd`. Under its separated-label, +homomorphic, identical-paired-word, arbitrary-bank-state contract, its crossing +criterion, weighted producer-prefix dimension theorem and dimension-four +odd-cycle exclusion are supported by a separate derivation and exact checks. + +## Scope and evidence + +The theorem and constructions belong to Tekalign/@tekuuu and the credited +predecessors. The added value is independently implemented evidence aimed at +two proof steps, rather than a new bank-dimension theorem: + +- [AUDIT.md](AUDIT.md) records a verifier agent's derivation from the model + before it read the source proof, followed by a clause-by-clause comparison. + It covers zero ranks, nonunitary diagonalization, deleting paired symbols, + and why the dimension-four commutant argument does not classify larger d. +- [verify.py](verify.py) implements dependency-stack cancellation of formal + involutive letters, without matrix encodings or predecessor code. For every + paired word up to global relabeling on **0 through 5 columns**, and every commutation graph, it + compares reduction with the geometric crossing criterion: **974,528 cases**. + All **128 cases through 3 columns** are also checked by exhaustive literal + adjacent-swap/deletion search. The five C5 edge-deletion controls fail as + required; nested noncommuting pairs pass. Six malformed-domain controls fail. +- [review_words.py](review_words.py), contributed by the skeptical reviewer, + independently enumerates all **162,014 labeled cases through 4 columns** and + decides literal rewriting by swap-connected components and recursive pair + deletion. It agrees with the piling implementation and canonical receipts. +- [commutant.py](commutant.py) independently solves all unrestricted rational + matrix equations `MG-GM=0` after a nonunitary similarity. It checks both + four-dimensional complementary algebras, their double commutant, scalar + common commutant and 16-dimensional joint algebra. Dropped-generator and + changed-multiplicity controls expose the hypotheses used by the proof. +- All three original registered command bodies passed at the pinned source + on CPython 3.12.14 under `-I -O -B`. [SOURCE-REPLAY.json](SOURCE-REPLAY.json) + retains exact commands, timings, output and the authenticated 13-file Git + inventory. The source tree was unchanged. This was direct execution of the + manifest's commands in a frozen export, not a claim that the upstream CI or + the original package's generic metadata launcher was run. + +The formal-letter checker audits the **combinatorial cancellation step**. Its +letters square to one; the actual bank operators square to label-dependent +central signs. A legal cancellation in the actual word contributes exactly +one self phase per column. The audit proves that step separately. The checker +does not implement the four A/B necessity arguments, classify complex matrix +representations, or derive dimension lower bounds. The rational commutant +fixture is likewise finite corroboration; universal statements rest on the +written proof. Standard piling, eigenspace and commutant methods are not +claimed as new mathematics. + +The original task draw selected `recursive-interfaces`. [TASK.json](TASK.json) +records the changed scope from `centre-path-sharing` to the explicit independent +audit handoff in [Discussion2842](https://github.com/CrocSwap/integer-mult-bounds/discussions/2842) +and its newest successor. The [coordination claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/2842#discussioncomment-18965571) was posted manually by the donor. [SOURCES.json](SOURCES.json) records base provenance; +the source replay pins are reference evidence, not imported mathematical code. +Ordinary replay of this new package does not access GitHub or rerun predecessors. + +## Reproduce + +Python 3.12 on Linux, standard library only; from the repository root: + +```sh +python3.12 scripts/research_package.py --package research/encoded-bank-criterion-audit +``` + +Expected markers: `PASS_ENCODED_BANK_CRITERION_AUDIT`, +`PASS_EXACT_NONUNITARY_D4_COMMUTANT`, `PASS_INDEPENDENT_LABELED_REWRITE_CLOSURE`, +and `PASS_REGISTERED_RESEARCH_PACKAGE`. +All three registered scripts use explicit checks that survive `-O`; ordinary replay +reads and compares the committed receipts without writing files. Direct +scripts also work from a Git-free export. For `verify.py` and `commutant.py`, `--emit` deliberately prints a new +receipt for comparison; `review_words.py` always reports its independent census. Each command is limited to 120 seconds; the full +census took under a minute on the audit host. + +No native C/Q invoice, two-level physical recursion, storage/precision/hosting +contract, selected supplier cold replay or full multiplication theorem was +audited. No selected record or predecessor file is changed. A separate AI +derivation is not independent human review or proof-assistant verification. + +## Open next questions + +The inherited useful next question is whether a paid actual caller can change +the separated-label, repeated-word or endpoint premise and still improve its +complete invoice. Start with an explicit two-column caller and check arbitrary +dirty inputs at two parent levels before expanding a search. The blocker is +the native implementation and complete cost, not another bank basis under the +audited contract. This audit gives no reason to expand the unchanged encoding +family. Classification of larger C5 dimensions remains outside scope and is +not proposed here as a supplier optimization. Structured details are in TASK.json. + +## Credit + +Tekalign/@tekuuu's PR2872 supplies the audited theorem. Gareth Davidson/@bitplane's +[PR2850](https://github.com/CrocSwap/integer-mult-bounds/pull/2850) supplies the +phase-boundary mechanism and failed-budget handoff; Dennis/@antunishdPursuit's +[PR2859](https://github.com/CrocSwap/integer-mult-bounds/pull/2859) supplies its +assigned-bit order/LIS predecessor. PR2872 credits Dugongue's concurrent +[PR2871](https://github.com/CrocSwap/integer-mult-bounds/pull/2871) P006/P056 +vector-control constructions. No priority claim over these results is made. + +Prepared for **DLamdata with substantial OpenAI Codex assistance**, including +an independent derivation/commutant subagent and a skeptical review subagent. +All share the source's model assumptions. New files are Apache-2.0; repository +LICENSE applies. No predecessor implementation is copied into this package. diff --git a/research/encoded-bank-criterion-audit/RESULT.json b/research/encoded-bank-criterion-audit/RESULT.json new file mode 100644 index 0000000000..bf14cf3586 --- /dev/null +++ b/research/encoded-bank-criterion-audit/RESULT.json @@ -0,0 +1,53 @@ +{ + "domain": [ + { + "accepted": 1, + "columns": 0, + "graphs": 1, + "rejected": 0, + "words": 1 + }, + { + "accepted": 1, + "columns": 1, + "graphs": 1, + "rejected": 0, + "words": 1 + }, + { + "accepted": 5, + "columns": 2, + "graphs": 2, + "rejected": 1, + "words": 3 + }, + { + "accepted": 71, + "columns": 3, + "graphs": 8, + "rejected": 49, + "words": 15 + }, + { + "accepted": 2449, + "columns": 4, + "graphs": 64, + "rejected": 4271, + "words": 105 + }, + { + "accepted": 191263, + "columns": 5, + "graphs": 1024, + "rejected": 776417, + "words": 945 + } + ], + "empty_word_checked": true, + "invalid_domain_controls": 6, + "literal_rewrite_cases": 128, + "omitted_C5_edge_controls": 5, + "scope": "Formal involutive letters only; no universal matrix or supplier certificate.", + "status": "PASS_ENCODED_BANK_CRITERION_AUDIT", + "word_graph_cases": 974528 +} diff --git a/research/encoded-bank-criterion-audit/SOURCE-REPLAY.json b/research/encoded-bank-criterion-audit/SOURCE-REPLAY.json new file mode 100644 index 0000000000..c7174d64a7 --- /dev/null +++ b/research/encoded-bank-criterion-audit/SOURCE-REPLAY.json @@ -0,0 +1,81 @@ +{ + "audited_commit": "cc5c2398505447a321fb9f9826163825e3b269fd", + "python": "3.12.14 (main, Aug 25 2026, 14:00:49) [Clang 22.1.3 ]", + "platform": "Linux-6.18.44-x86_64-with-glibc2.41", + "files": { + "MATRICES.json": "e3e15bb9a2e63cea719148a35d063a5dd4bc808687a78b4c30d4b401fe3f61e1", + "PROOF.md": "154cf967411b93da3a5c56c84c4f8a62f62192448c14c08e510e830054897bf9", + "README.md": "36651182958171759da5d212c62f90b5f162f6e9928b9bdb3ae46616c987b78d", + "REFERENCES.json": "4cb7815d6314ff139b65c94799a32e13b66b2dc607db9b783e9339a7b3a37515", + "RESULT.json": "d0d6793b3b0c1deb023770a5e24512461a3ce533d2cf1c31f17d4e0dd83a0e6c", + "SOURCES.json": "9fd35245f32aeabc5897c481207149276268854b65a36f657adef0c441768f39", + "TASK.json": "8e6c44de931c0c220aef7b411c8a9db92bd494b93e7767b22824ab98a2c100cf", + "VERIFY.json": "3b6c403ac565741689c65acd70ae1523c782d7fa23a9f78206c626908584ac7d", + "independent.py": "f49341f2c712ad9009a7a0a455697436415b43d68a61794c507a276c306c0906", + "references/PR2850-README.md": "65d18a905d30ef2d411ad85cd22ab1a689ca0687bf6c78dda6cd7e0ea529d7d6", + "references/PR2859-README.md": "5e60c3e6868b5c335df8f0d3a76526caf4be9d895d999d03ef72b29f0b26bcf9", + "test_package.py": "a6d765cf347f891e6c938fe51dc66f5273de3a1318ef324d6388c26a169501ac", + "verify.py": "a0a4fccb10f9f51704c9b0978f728ff778f122254d0742dfcbe8902952a48346" + }, + "commands": [ + { + "argv": [ + "/workspace/integer-mult-bounds/.venv/bin/python", + "-I", + "-O", + "-B", + "work/frozen-pr2872/research/encoded-phase-bank/verify.py" + ], + "returncode": 0, + "seconds": 10.068, + "stdout": "{\"C5\": {\"constructed_bits\": 3, \"orthogonality_edges\": 10, \"schedule\": [0, 1, 4, 0, 3, 4, 2, 3, 1, 2], \"two_bit_symplectic_planes\": 20}, \"max_constructed_bits\": 10, \"negative_controls\": {\"extra_consumer\": true, \"label_gap\": true, \"missing_consumer\": true, \"omit_term_(0, 1)\": true, \"omit_term_(0, 3)\": true, \"omit_term_(1, 2)\": true, \"same_order_shared_bit\": true, \"three_crossing_one_bit\": true, \"wrong_diagonal_pairing\": true}, \"no_new_kappa\": true, \"q1_canonical_words\": 124, \"q1_correct_encodings\": 19302, \"q1_exhaustive_encodings\": 139434, \"q2_one_encoding_per_word\": 11464, \"q2_seed\": 70, \"references\": 2, \"status\": \"PASS_ENCODED_PHASE_BANK\", \"weighted_permutation_cases\": 31287}\n", + "stderr": "" + }, + { + "argv": [ + "/workspace/integer-mult-bounds/.venv/bin/python", + "-I", + "-O", + "-B", + "work/frozen-pr2872/research/encoded-phase-bank/independent.py" + ], + "returncode": 0, + "seconds": 2.125, + "stdout": "{\"coefficients\": 84032, \"complete_columns\": 10784, \"joint_label_dimension_one_escape\": 1024, \"negative_controls\": [{\"name\": \"crossed noncommuting dense columns\", \"rejected\": true, \"witness\": {\"actual\": [\"1/2\", \"1/2\"], \"bank_column\": 0, \"expected\": [\"1\", \"0\"], \"labels\": [0, 1, 0, 1]}}, {\"name\": \"missing consumer\", \"rejected\": true, \"witness\": {\"actual\": [\"0\", \"1\"], \"bank_column\": 0, \"expected\": [\"1\", \"0\"], \"labels\": [0, 1, 0, 0]}}, {\"name\": \"wrong same-column square\", \"rejected\": true, \"witness\": {\"actual\": [\"1\", \"0\"], \"bank_column\": 0, \"expected\": [\"-1\", \"0\"], \"labels\": [1, 1]}}, {\"name\": \"permutation destroys sharing\", \"rejected\": true, \"witness\": {\"actual\": [\"-1\", \"0\", \"0\", \"0\"], \"bank_column\": 0, \"expected\": [\"1\", \"0\", \"0\", \"0\"], \"labels\": [0, 1, 0, 0, 1, 0]}}, {\"name\": \"same-family commutation is necessary\", \"rejected\": true, \"witness\": {\"actual\": [\"-1\", \"0\", \"0\", \"0\"], \"bank_column\": 0, \"expected\": [\"1\", \"0\", \"0\", \"0\"], \"labels\": [1, 0, 1, 0]}}], \"no_new_kappa\": true, \"positive_fixtures\": [{\"bank_dimension\": 2, \"coefficients\": 64, \"complete_columns\": 32, \"name\": \"non-Pauli nested columns\", \"widths\": [1, 1]}, {\"bank_dimension\": 4, \"coefficients\": 1024, \"complete_columns\": 256, \"name\": \"dense producer-prefix\", \"widths\": [1, 1, 1]}, {\"bank_dimension\": 4, \"coefficients\": 1024, \"complete_columns\": 256, \"name\": \"interleaved path\", \"widths\": [1, 1, 1]}, {\"bank_dimension\": 8, \"coefficients\": 16384, \"complete_columns\": 2048, \"name\": \"dense weighted blocks\", \"widths\": [1, 2, 1]}, {\"bank_dimension\": 8, \"coefficients\": 65536, \"complete_columns\": 8192, \"name\": \"C5 attained dimension eight\", \"widths\": [1, 1, 1, 1, 1]}], \"status\": \"PASS_INDEPENDENT_ENCODED_BANK_MATRICES\"}\n", + "stderr": "" + }, + { + "argv": [ + "/workspace/integer-mult-bounds/.venv/bin/python", + "-I", + "-O", + "-B", + "work/frozen-pr2872/research/encoded-phase-bank/test_package.py" + ], + "returncode": 0, + "seconds": 23.593, + "stdout": "PASS_ENCODED_BANK_PACKAGE_CONTROLS semantic=5 corruption=3 optimized_git_free_read_only=true\n", + "stderr": "" + } + ], + "source_tree_unchanged": true, + "git_blobs": { + "MATRICES.json": "fde0bd0e264ec631bd77450f9227b35a92976244", + "PROOF.md": "c38d5232680fe6a4f2889eeff156ef351bb30eed", + "README.md": "9f39cd579aa67a6e814d300fee67d41f3ed85d23", + "REFERENCES.json": "c54b622de930065560b21f12e5881f0198e8cbc4", + "RESULT.json": "29e162ecdc1f953c0918b05fff6052c209567fc6", + "SOURCES.json": "f5e65a7974f6b41390e1dbe8322606c298c66cba", + "TASK.json": "ec4cfa77880ce29e3d855fbbe70858ca7dbdcca1", + "VERIFY.json": "f914c6a431b6859c30c32eb093bb511d431dc4d9", + "independent.py": "4eb80898d808f2071a5a0778a6d51ae451531f8c", + "references/PR2850-README.md": "b9a6966efaa8901b7ccc3b88a133aec661258fca", + "references/PR2859-README.md": "43a4b14ef67d609fe5ea5209b03012c8ef33dd43", + "test_package.py": "ad458dcbd520da25bdcf0113b0d332518c249072", + "verify.py": "12ec8e2acc3c02a8826b9a4e99aad4847f6a8d39" + }, + "git_authenticated": true, + "source_package_tree": "fc6a233bca93f2502cb014febe5241fa81e692be", + "reproduction": "git archive cc5c2398505447a321fb9f9826163825e3b269fd research/encoded-phase-bank | tar -x -C EXPORT; run the listed -I -O -B command bodies from that export, each with the manifest timeout.", + "scope": "Observed source replay and byte authentication; reference evidence only. Not rerun or remotely authenticated by the new package verifier." +} diff --git a/research/encoded-bank-criterion-audit/SOURCES.json b/research/encoded-bank-criterion-audit/SOURCES.json new file mode 100644 index 0000000000..f3e0207f01 --- /dev/null +++ b/research/encoded-bank-criterion-audit/SOURCES.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "base_commit": "67b122d33d6c599a49f65d50afa2f3fe8d790d02", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "889b95d936746df124872133ae1e7cc339adcb92", + "sha256": "7d185cd8c2af35988d638d969748ad7b670f902606444dbfc748e4402c340df6" + } + ] +} diff --git a/research/encoded-bank-criterion-audit/TASK.json b/research/encoded-bank-criterion-audit/TASK.json new file mode 100644 index 0000000000..8ffcf2d777 --- /dev/null +++ b/research/encoded-bank-criterion-audit/TASK.json @@ -0,0 +1,162 @@ +{ + "schema_version": 1, + "task_id": "centre-path-sharing", + "priority_revision": 5, + "base_commit": "67b122d33d6c599a49f65d50afa2f3fe8d790d02", + "original_card": { + "id": "centre-path-sharing", + "question": "Can the 64-per-call centre path (eight rank-8 COPY/ERASE totals through the private temporary) be shared across calls or shrunk?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/complex-local-word-ceiling/README.md", + "research/split-centres-global/proofs/PR386-BIT-GEOMETRY.txt", + "certificates/selected-result.json" + ], + "methods": [ + "Derive a fully charged favorable relaxation for sharing one centre path across k calls, including restoration, hosting and precision.", + "Prove a lower bound on copied information per call for the selected decoder contract." + ], + "acceptance_gate": "Show the changed centre charge and copy profile per call with every added restoration or hosting cost charged, and its ceiling via ceiling.ceiling(centre=...). 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", + "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": "Write the per-call centre charge and copy children for sharing across k = 2 calls, charge the sharing overhead, and screen it; stop this route if even the ideal sharing gains under 10%. Ideal budgets: free 2.80x, shared by two 1.90x (levers.py).", + "bottleneck_link": "The centre path consumes 64 of about 99.6 unpaid coordinates per call, i.e. about 64% of the raw deficit.", + "allowed_variations": [ + "One sharing pattern across a fixed number of calls.", + "One reduced copied-total contract for the existing decoder.", + "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": [ + "Removing copies without a replacement contract for the decoder's copied totals.", + "Continuing a partial cost improvement while leaving the same unpriced consumer, restoration or central-readout obligation unresolved; refresh the family expansion decision first. Local product-retiming evidence has a narrow scope and is not a ban on changed graphs or contracts." + ], + "overlap_terms": [ + "centre path", + "copied totals", + "private temporary", + "shared centre", + "batching" + ] + }, + "scope_status": "changed", + "actual_scope": "Independent audit of PR2872 exact crossing criterion, weighted producer-prefix bank dimension, and d=4 odd-cycle obstruction.", + "scope_change_reason": "The fresh phase-boundary handoff in Discussion2842 asks for an independent audit. PR2859 and PR2872 already settle the construction extensions, so this checks the newest precise claims rather than repeating a centre-sharing search.", + "bottleneck_link": "An audit of a stateful recursive boundary. No centre-charge saving is claimed; its bank-dimension theorem closes an encoding loophole only under a specific caller contract.", + "budget_minutes": 45, + "stop_rule": "Stop after the scoped proof audit, all paired words f<=5 and all commutation graphs (one CPU, 300-second experiment cap), source replay, and skeptical review. No larger unchanged-alphabet search.", + "outcome": "completed", + "evidence": "AUDIT.md independent derivation; RESULT.json exact word census; COMMUTANT.json rational RREF; SOURCE-REPLAY.json pinned predecessor execution and byte authentication.", + "author": "DLamdata, with OpenAI Codex assistance", + "ai_assistance": "Substantial OpenAI Codex assistance in derivation, code, execution, inspection and writing. One lead; one independent verifier agent; one skeptical reviewer agent. No independent human or formal-kernel review.", + "open_questions": [ + { + "question": "Can one paid actual caller change label separation, paired-word semantics or endpoint while improving the complete recursive invoice?", + "why_it_matters": "The proved dimension restriction applies only within the stated contract; the native construction remains width-critical.", + "first_step": "Specify an f=2 caller with complete encoding/consumer costs and check arbitrary dirty inputs at two parent levels.", + "blocked_by": "A favorable native implementation and paid full cost; abstract encodings alone do not establish savings." + } + ], + "seed": "c5030fa074f07c604ec5ffa727d7a464", + "track": "recursive-interfaces", + "audited_commit": "cc5c2398505447a321fb9f9826163825e3b269fd", + "milestone": "independent audit; no new kappa", + "coordination": { + "thread": "https://github.com/CrocSwap/integer-mult-bounds/discussions/2842", + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/2842#discussioncomment-18965571", + "claim_status": "Posted manually by donor; use as canonical coordination reference. Integration posting remains blocked; do not retry." + }, + "entry_overlap": { + "searched_at": "2026-10-16T06:16:36.563532+00:00", + "terms": [ + "encoded-phase-bank", + "phase-order-bank", + "phase-accumulator", + "2872" + ], + "coverage": { + "open_prs": { + "fetched_at": "2026-10-16T06:13:37.521184+00:00", + "complete_pagination": true, + "records": 495 + }, + "discussions": { + "fetched_at": "2026-10-16T06:16:13.430553+00:00", + "complete_pagination": true, + "records": 1515 + }, + "closed_prs": { + "fetched_at": "2026-10-16T06:16:36.285732+00:00", + "complete_pagination": true, + "records": 2077 + } + }, + "local_records": 2541, + "warnings": [], + "limits": "Remote PR scope includes open and closed/merged titles and bodies, with separate coverage and timestamps. State changes are deduplicated by latest PR update; snapshots are not atomic. No code diffs or arbitrary package files are searched. Recheck relevant heads before submission.", + "matches_total": 18 + }, + "predecessors": [ + { + "pr": 2872, + "commit": "cc5c2398505447a321fb9f9826163825e3b269fd", + "author": "Tekalign / tekuuu" + }, + { + "pr": 2859, + "commit": "395b7fbde8f009263c8dceb46e0f2ee8a2a6e846", + "author": "Dennis / antunishdPursuit", + "note": "Scientific predecessor pin used by PR2872; later live head186a38eb has additional CI changes." + }, + { + "pr": 2850, + "commit": "a007c32f992195ad372806db38c9359dd49382ad", + "author": "Gareth Davidson / bitplane" + } + ], + "finding": "No substantive proof gap found; independent formal-word and exact rational commutant evidence.", + "final_overlap": { + "searched_at": "2026-10-16T06:23:54.295568+00:00", + "terms": [ + "encoded-phase-bank", + "phase-order-bank", + "phase-accumulator", + "commutant", + "2872" + ], + "coverage": { + "open_prs": { + "fetched_at": "2026-10-16T06:20:47.310586+00:00", + "complete_pagination": true, + "records": 495 + }, + "discussions": { + "fetched_at": "2026-10-16T06:23:32.328523+00:00", + "complete_pagination": true, + "records": 1517 + }, + "closed_prs": { + "fetched_at": "2026-10-16T06:23:53.940173+00:00", + "complete_pagination": true, + "records": 2077 + } + }, + "local_records": 2543, + "warnings": [], + "limits": "Remote PR scope includes open and closed/merged titles and bodies, with separate coverage and timestamps. State changes are deduplicated by latest PR update; snapshots are not atomic. No code diffs or arbitrary package files are searched. Recheck relevant heads before submission.", + "matches_total": 26 + }, + "upstream_checkpoint": { + "commit": "4b82082f901945f8d0314f143576c7ad31e021fc", + "priority_revision": 5, + "checked_at_utc": "2026-10-16T06:25:15.121506+00:00", + "decision": "Retain scientific base. Guidance, task catalogue, selected record and package runner unchanged. New upstream changes are disjoint integration/selected-residual-live-volume work; audited PR2872 head unchanged." + } +} diff --git a/research/encoded-bank-criterion-audit/VALIDATION.json b/research/encoded-bank-criterion-audit/VALIDATION.json new file mode 100644 index 0000000000..9e950c3e70 --- /dev/null +++ b/research/encoded-bank-criterion-audit/VALIDATION.json @@ -0,0 +1,44 @@ +{ + "python": "CPython 3.12.14", + "registered_replay": "PASS_REGISTERED_RESEARCH_PACKAGE: all three final commands completed successfully under -I -O -B", + "source_replay": "SOURCE-REPLAY.json", + "package_controls": { + "status": "PASS_PACKAGE_CONTROLS", + "readonly_tree_unchanged": true + }, + "controls": [ + { + "name": "Git-free read-only relocated verify.py", + "returncode": 0 + }, + { + "name": "Git-free read-only relocated commutant.py", + "returncode": 0 + }, + { + "name": "mutated RESULT.json word_graph_cases", + "returncode": 1, + "expected_failure": "receipt mismatch" + }, + { + "name": "mutated COMMUTANT.json joint_algebra_dimension", + "returncode": 1, + "expected_failure": "commutant receipt mismatch" + }, + { + "name": "Git-free read-only relocated review_words.py", + "returncode": 0 + } + ], + "scientific_files_sha256": { + "commutant.py": "b1eb4776b5c33f5e1e5b921cc27d273682585217729b3ff53be05209ec5b39ed", + "review_words.py": "059b1b7c447621051dbf1d75d7da6ed4bab8c0279e9f39157d657badf8123973", + "verify.py": "21acf6478c2b770db8359b89bb1b2257d29f8564645575de0f79bd4cc12ea5e9" + }, + "registered_log_sha256": "220e0d2cc6a0b44e195f303207c2e8473887772f07e6e0df627244fa1ce6d9be", + "verification_commands": [ + "python3.12 scripts/research_package.py --package research/encoded-bank-criterion-audit", + "python3 scripts/research_package.py --package research/encoded-bank-criterion-audit --check-only" + ], + "skipped": "Full selected supplier replay, native C/Q recursion, physical caller costs, hosting/precision and formal-kernel proof are outside the additive audit scope." +} diff --git a/research/encoded-bank-criterion-audit/VERIFY.json b/research/encoded-bank-criterion-audit/VERIFY.json new file mode 100644 index 0000000000..065e15fab5 --- /dev/null +++ b/research/encoded-bank-criterion-audit/VERIFY.json @@ -0,0 +1,42 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "All canonical paired words f<=5 (up to global relabeling) and all commutation graphs, literal rewrite cross-check f<=3, omitted-edge and domain controls, exact receipt comparison." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/commutant.py" + ], + "timeout_seconds": 120, + "checks": "Unrestricted exact rational centralizer solve in a nonunitary d4 fixture, generator/multiplicity boundary controls, exact receipt comparison." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/review_words.py" + ], + "timeout_seconds": 120, + "checks": "Independent exhaustive swap-component/deletion oracle on162014 labeled paired-word/graph cases f<=4; compare piling, crossing criterion and canonical receipts." + } + ] +} diff --git a/research/encoded-bank-criterion-audit/commutant.py b/research/encoded-bank-criterion-audit/commutant.py new file mode 100644 index 0000000000..f8462fc8c9 --- /dev/null +++ b/research/encoded-bank-criterion-audit/commutant.py @@ -0,0 +1,168 @@ +#!/usr/bin/env python3 +"""Exact d=4 commutant witness, written without importing candidate code. + +DLamdata with OpenAI Codex assistance, including a separate verifier agent. +Apache-2.0. + +This finite rational witness corroborates an algebraic step; it does not +establish the theorem for all complex representations. +""" +from fractions import Fraction as Q +import argparse +import json +from pathlib import Path + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def identity(n): + return [[Q(i == j) for j in range(n)] for i in range(n)] + + +def multiply(a, b): + return [[sum((x * y for x, y in zip(row, col)), Q(0)) + for col in zip(*b)] for row in a] + + +def rref(rows, columns): + a = [[Q(x) for x in row] for row in rows] + pivots = [] + for col in range(columns): + k = len(pivots) + pivot = next((i for i in range(k, len(a)) if a[i][col]), None) + if pivot is None: + continue + a[k], a[pivot] = a[pivot], a[k] + divisor = a[k][col] + a[k] = [x / divisor for x in a[k]] + for i in range(len(a)): + if i != k and a[i][col]: + factor = a[i][col] + a[i] = [x - factor * y for x, y in zip(a[i], a[k])] + pivots.append(col) + return a, pivots + + +def inverse(a): + n = len(a) + rr, pivots = rref([r + s for r, s in zip(a, identity(n))], n) + need(len(pivots) == n, 'singular basis') + return [r[n:] for r in rr] + + +def flatten(a): + return [x for row in a for x in row] + + +def span_rank(matrices): + return len(rref([flatten(m) for m in matrices], len(matrices[0]) ** 2)[1]) + + +def centralizer(generators): + """Solve all entries of M G - G M=0 over Q, with no ansatz on M.""" + n = len(generators[0]) + equations = [] + for g in generators: + for i in range(n): + for j in range(n): + row = [Q(0)] * (n * n) + for k in range(n): + row[i * n + k] += g[k][j] + row[k * n + j] -= g[i][k] + equations.append(row) + rr, pivots = rref(equations, n * n) + basis = [] + for free in sorted(set(range(n * n)) - set(pivots)): + vector = [Q(0)] * (n * n) + vector[free] = Q(1) + for k, pivot in enumerate(pivots): + vector[pivot] = -rr[k][free] + basis.append([vector[i * n:(i + 1) * n] for i in range(n)]) + return basis + + +def tensor(a, b): + return [[x * y for x in ra for y in rb] for ra in a for rb in b] + + +def same_span(a, b): + return span_rank(a) == span_rank(b) == span_rank(a + b) + + +def run(): + z = [[Q(1), Q(0)], [Q(0), Q(-1)]] + x = [[Q(0), Q(1)], [Q(1), Q(0)]] + s = [[Q(v) for v in row] for row in + [[1, 1, 1, 1], [0, 1, 2, 3], [0, 0, 1, 4], [0, 0, 0, 1]]] + sinv = inverse(s) + conjugate = lambda m: multiply(multiply(s, m), sinv) + a, b = [conjugate(tensor(m, identity(2))) for m in (z, x)] + c, d = [conjugate(tensor(identity(2), m)) for m in (z, x)] + unit = identity(4) + for first, second in ((a, b), (c, d)): + need(multiply(first, first) == multiply(second, second) == unit, + 'involution relation') + neg = [[-v for v in row] for row in multiply(second, first)] + need(multiply(first, second) == neg, 'Weyl relation') + need(multiply([list(row) for row in zip(*a)], a) != unit, + 'fixture accidentally unitary') + alg0 = [unit, a, b, multiply(a, b)] + alg1 = [unit, c, d, multiply(c, d)] + cent0 = centralizer([a, b]) + cent1 = centralizer([c, d]) + double0 = centralizer(cent0) + common = centralizer([a, b, c, d]) + need(same_span(cent0, alg1) and same_span(cent1, alg0), + 'complementary commutants') + need(same_span(double0, alg0), 'double commutant') + need(same_span(common, [unit]), 'intersection must be scalar') + need(span_rank([multiply(p, q) for p in alg0 for q in alg1]) == 16, + 'joint algebra is not all M4') + drop_one = len(centralizer([a])) + drop_neighbor = len(centralizer([a, b])) + need(drop_one == 8, 'dropping B must enlarge centralizer') + need(drop_neighbor == 4, 'dropping one neighbor must leave M2') + # Multiplicity three exposes the dimension-four premise: its commutant + # has dimension nine, so a neighboring four-dimensional algebra need + # not exhaust it. No claim about a valid d=6 crossing edge is made. + multiplicity_three = len(centralizer([tensor(z, identity(3)), + tensor(x, identity(3))])) + need(multiplicity_three == 9, 'multiplicity-three commutant') + result = { + 'status': 'PASS_EXACT_NONUNITARY_D4_COMMUTANT', + 'arithmetic': 'Fraction exact rational RREF on unrestricted matrix entries', + 'candidate_imports': [], + 'dimension': 4, + 'algebra_dimensions': [span_rank(alg0), span_rank(alg1)], + 'commutant_dimensions': [len(cent0), len(cent1)], + 'double_commutant_dimension': len(double0), + 'common_commutant_dimension': len(common), + 'joint_algebra_dimension': 16, + 'nonunitary_generator': True, + 'failure_controls': { + 'drop_B_centralizer_dimension': drop_one, + 'drop_second_neighbor_centralizer_dimension': drop_neighbor, + 'd6_single_pair_centralizer_dimension': multiplicity_three, + }, + 'limitation': 'Finite witness only; all-GL result rests on the written proof', + } + return result + + +def main(): + parser = argparse.ArgumentParser() + parser.add_argument('--emit', action='store_true') + args = parser.parse_args() + result = run() + if not args.emit: + expected = json.loads(Path(__file__).with_name('COMMUTANT.json').read_text()) + need(json.dumps(result, sort_keys=True) == json.dumps(expected, sort_keys=True), + 'commutant receipt mismatch') + print(json.dumps(result, indent=2, sort_keys=True)) + + +if __name__ == '__main__': + main() diff --git a/research/encoded-bank-criterion-audit/review_words.py b/research/encoded-bank-criterion-audit/review_words.py new file mode 100644 index 0000000000..69f525ff67 --- /dev/null +++ b/research/encoded-bank-criterion-audit/review_words.py @@ -0,0 +1,131 @@ +"""Independent labeled-word closure, f<=4. + +DLamdata with OpenAI Codex skeptical-review assistance. Apache-2.0. +The oracle uses swap components and pair deletions, not crossing or piling. +""" +import importlib.util +import itertools +import json +from pathlib import Path +import resource +import sys +import time + +PKG = Path(__file__).resolve().parent + +def need(ok, message): + if not ok: + raise RuntimeError(message) + +def load(name): + spec = importlib.util.spec_from_file_location(name, PKG / (name + '.py')) + module = importlib.util.module_from_spec(spec) + spec.loader.exec_module(module) + return module + +candidate = load('verify') + +def words(letters): + counts = {a: 2 for a in letters} + result = [] + def extend(prefix): + if len(prefix) == 2 * len(letters): + result.append(prefix) + return + for a in letters: + if counts[a]: + counts[a] -= 1 + extend(prefix + (a,)) + counts[a] += 1 + extend(()) + return result + +def canonical(word): + labels = {} + result = [] + for a in word: + if a not in labels: + labels[a] = len(labels) + result.append(labels[a]) + return tuple(result) + +def accepted_by_components(n, allowed, domain): + """Swap components at each subset; seed by deletion into smaller subsets. + + This is exhaustive search of the literal rewrite relation. It neither uses + interval crossings nor piling. All labeled words are generated independently. + """ + accepted = {(): True} + for size in range(1, n + 1): + for subset in itertools.combinations(range(n), size): + ws = domain[subset] + lookup = {w: i for i, w in enumerate(ws)} + parent = list(range(len(ws))) + def root(i): + while parent[i] != i: + parent[i] = parent[parent[i]] + i = parent[i] + return i + deletion_seeds = [] + for i, w in enumerate(ws): + for k in range(len(w) - 1): + a, b = w[k:k + 2] + if a == b: + if accepted[w[:k] + w[k + 2:]]: + deletion_seeds.append(i) + elif frozenset((a, b)) in allowed: + v = w[:k] + (b, a) + w[k + 2:] + ri, rj = root(i), root(lookup[v]) + if ri != rj: + parent[ri] = rj + good = {root(i) for i in deletion_seeds} + for i, w in enumerate(ws): + accepted[w] = root(i) in good + return accepted + +def census(): + rows = [] + for n in range(5): + domain = {subset: words(subset) for k in range(n + 1) + for subset in itertools.combinations(range(n), k)} + full = domain[tuple(range(n))] + canonical_words = {canonical(w) for w in full} + need(canonical_words == set(candidate.paired_words(n)), + ('canonical coverage mismatch', n)) + edges = list(itertools.combinations(range(n), 2)) + accepted_count = rejected_count = 0 + canonical_accepted = canonical_rejected = 0 + for mask in range(1 << len(edges)): + allowed = {frozenset(e) for k, e in enumerate(edges) if mask & (1 << k)} + accepted = accepted_by_components(n, allowed, domain) + deps = candidate.dependencies(n, mask) + for w in full: + actual = accepted[w] + need(actual == candidate.piling_identity(w, deps), + ('piling discrepancy', n, mask, w)) + needed = candidate.crossing_mask(w, n) + need(actual == (needed & mask == needed), + ('crossing discrepancy', n, mask, w)) + accepted_count += actual + rejected_count += not actual + if w in canonical_words: + canonical_accepted += actual + canonical_rejected += not actual + row = dict(columns=n, labeled_words=len(full), graphs=1 << len(edges), + accepted=accepted_count, rejected=rejected_count, + canonical_accepted=canonical_accepted, + canonical_rejected=canonical_rejected) + receipt = json.loads((PKG / 'RESULT.json').read_text())['domain'][n] + need(canonical_accepted == receipt['accepted'] and + canonical_rejected == receipt['rejected'], ('receipt mismatch', n)) + rows.append(row) + return rows + +started = time.monotonic() +result = {'python': sys.version, 'census': census()} +result['total_labeled_word_graph_cases'] = sum(r['accepted'] + r['rejected'] + for r in result['census']) +result['seconds'] = round(time.monotonic() - started, 3) +result['max_rss_kib'] = resource.getrusage(resource.RUSAGE_SELF).ru_maxrss +result['status'] = 'PASS_INDEPENDENT_LABELED_REWRITE_CLOSURE' +print(json.dumps(result, indent=2, sort_keys=True)) diff --git a/research/encoded-bank-criterion-audit/verify.py b/research/encoded-bank-criterion-audit/verify.py new file mode 100644 index 0000000000..a510dc53b6 --- /dev/null +++ b/research/encoded-bank-criterion-audit/verify.py @@ -0,0 +1,181 @@ +#!/usr/bin/env python3 +"""Independent finite audit of formal paired-word crossing support. + +DLamdata with OpenAI Codex assistance, Apache-2.0. +No predecessor implementation or matrix encoding is imported. +""" +import argparse +from collections import Counter, deque +from itertools import combinations +import json +from pathlib import Path + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def paired_words(n): + """Enumerate position matchings, labelled by first occurrence.""" + def match(positions, pairs): + if not positions: + word = [None] * (2 * n) + for label, (a, b) in enumerate(sorted(pairs)): + word[a] = word[b] = label + yield tuple(word) + return + a, *rest = positions + for b in rest: + yield from match([x for x in rest if x != b], pairs + [(a, b)]) + yield from match(list(range(2 * n)), []) + + +def validate(word, n, mask): + require(type(n) is int and n >= 0, "invalid alphabet") + require(all(type(x) is int for x in word), "non-integer letter") + require(Counter(word) == Counter({j: 2 for j in range(n)}), "not a paired word") + require(type(mask) is int and 0 <= mask < 1 << (n * (n - 1) // 2), + "invalid commutation mask") + + +def dependencies(n, mask): + """Noncommuting neighbors, computed without inspecting a word.""" + deps = [[] for _ in range(n)] + for bit, (a, b) in enumerate(combinations(range(n), 2)): + if not (mask >> bit) & 1: + deps[a].append(b) + deps[b].append(a) + return deps + + +def piling_identity(word, deps): + """Involution-group piling, with beads and noncommutation blockers. + + A 1 records a letter; its 0 blockers prevent cancellation across an + uncancelled dependent letter. A matching top bead removes its blockers. + This procedure does not compute crossings or choose shortest intervals. + """ + stacks = [[] for _ in deps] + cancelled = [0] * len(deps) + for a in word: + if stacks[a] and stacks[a][-1] == 1: + stacks[a].pop() + for b in deps[a]: + require(stacks[b] and stacks[b][-1] == 0, "piling blocker mismatch") + stacks[b].pop() + cancelled[a] += 1 + else: + stacks[a].append(1) + for b in deps[a]: + stacks[b].append(0) + empty = not any(stacks) + if empty: + require(cancelled == [1] * len(deps), "lost or duplicated self phase") + return empty + + +def literal_identity(word, n, mask): + """All adjacent swaps and adjacent-double deletions, no search cutoff.""" + commute = {pair for bit, pair in enumerate(combinations(range(n), 2)) + if (mask >> bit) & 1} + todo, seen = deque([word]), {word} + while todo: + current = todo.popleft() + if not current: + return True + for k in range(len(current) - 1): + a, b = current[k:k + 2] + if a == b: + nxt = current[:k] + current[k + 2:] + elif tuple(sorted((a, b))) in commute: + nxt = current[:k] + (b, a) + current[k + 2:] + else: + continue + if nxt not in seen: + seen.add(nxt) + todo.append(nxt) + return False + + +def crossing_mask(word, n): + """Independent prediction from occurrence positions alone.""" + ends = [[k for k, letter in enumerate(word) if letter == j] for j in range(n)] + result = 0 + for bit, (a, b) in enumerate(combinations(range(n), 2)): + x, y = ends[a] + z, t = ends[b] + if x < z < y < t or z < x < t < y: + result |= 1 << bit + return result + + +def run(): + rows, literal_cases = [], 0 + for n in range(6): + graphs = [(mask, dependencies(n, mask)) for mask in range(1 << (n * (n - 1) // 2))] + words = list(paired_words(n)) + require(len(words) == len(set(words)), "duplicate matching") + expected_words = 1 + for k in range(1, 2 * n, 2): + expected_words *= k + require(len(words) == expected_words, "incomplete matching enumeration") + accepted = rejected = 0 + for word in words: + required = crossing_mask(word, n) + for mask, deps in graphs: + validate(word, n, mask) + actual = piling_identity(word, deps) + require(actual == (required & mask == required), + f"crossing discrepancy: {word}, {mask}") + accepted += actual + rejected += not actual + if n <= 3: + require(literal_identity(word, n, mask) == actual, + f"literal rewrite discrepancy: {word}, {mask}") + literal_cases += 1 + rows.append({"columns": n, "words": len(words), "graphs": len(graphs), + "accepted": accepted, "rejected": rejected}) + cycle = (0, 1, 4, 0, 3, 4, 2, 3, 1, 2) + needed = crossing_mask(cycle, 5) + edges = list(combinations(range(5), 2)) + require([edges[k] for k in range(10) if needed >> k & 1] == + [(0, 1), (0, 4), (1, 2), (2, 3), (3, 4)], "wrong C5") + require(piling_identity(cycle, dependencies(5, needed)), "C5 positive fixture") + omitted = 0 + for k in range(10): + if needed >> k & 1: + require(not piling_identity(cycle, dependencies(5, needed ^ (1 << k))), + "omitted C5 relation accepted") + omitted += 1 + require(piling_identity((0, 1, 1, 0), dependencies(2, 0)), "nested positive fixture") + require(not piling_identity((0, 1, 0, 1), dependencies(2, 0)), "crossing negative fixture") + invalid = [((0, 1, 0), 2, 0), ((0, 0, 0, 0), 2, 0), ((-1, -1), 1, 0), + ((True, True), 1, 0), ((0, 0), 1, 1), ((0, 0), 1, -1)] + for args in invalid: + try: + validate(*args) + except ValueError: + continue + raise ValueError("malformed domain accepted") + return {"status": "PASS_ENCODED_BANK_CRITERION_AUDIT", "domain": rows, + "word_graph_cases": sum(r["accepted"] + r["rejected"] for r in rows), + "literal_rewrite_cases": literal_cases, "omitted_C5_edge_controls": omitted, + "invalid_domain_controls": len(invalid), "empty_word_checked": True, + "scope": "Formal involutive letters only; no universal matrix or supplier certificate."} + + +def main(): + parser = argparse.ArgumentParser() + parser.add_argument("--emit", action="store_true") + args = parser.parse_args() + result = run() + if not args.emit: + expected = json.loads(Path(__file__).with_name("RESULT.json").read_text()) + require(json.dumps(result, sort_keys=True) == json.dumps(expected, sort_keys=True), + "receipt mismatch") + print(json.dumps(result, indent=2, sort_keys=True)) + + +if __name__ == "__main__": + main()