Independently audit encoded-bank crossing and dimension proofs

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.

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"
+}

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.

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.