From 6025743bc95e096845af0962ba0c4c37cce89c4e Mon Sep 17 00:00:00 2001 From: Cursor Agent Date: Tue, 10 Nov 2026 08:58:21 +0000 Subject: [PATCH] Prove degree-881 payload involutions split a sector-3 joint space X_3 has trace -48 on the trivial (+1,+1) space of the explicit c=3 pair and splits it into invariant subspaces of dimensions 84 and 132. Z_508 halves that space. The selected kappa is unchanged. Co-authored-by: unpaidmoon --- research/c3-payload-sector3-split/PROOF.md | 209 ++++++ research/c3-payload-sector3-split/README.md | 122 ++++ .../c3-payload-sector3-split/SOURCES.json | 36 + research/c3-payload-sector3-split/TASK.json | 118 ++++ research/c3-payload-sector3-split/VERIFY.json | 32 + research/c3-payload-sector3-split/verify.py | 656 ++++++++++++++++++ 6 files changed, 1173 insertions(+) create mode 100644 research/c3-payload-sector3-split/PROOF.md create mode 100644 research/c3-payload-sector3-split/README.md create mode 100644 research/c3-payload-sector3-split/SOURCES.json create mode 100644 research/c3-payload-sector3-split/TASK.json create mode 100644 research/c3-payload-sector3-split/VERIFY.json create mode 100644 research/c3-payload-sector3-split/verify.py diff --git a/research/c3-payload-sector3-split/PROOF.md b/research/c3-payload-sector3-split/PROOF.md new file mode 100644 index 0000000000..eede4d80d9 --- /dev/null +++ b/research/c3-payload-sector3-split/PROOF.md @@ -0,0 +1,209 @@ +# Payload involutions that fix sector 3 and split its joint spaces + +This note answers the second open question of the c=3 sign-character +certificate: whether a payload involution from the degree-881 one-slot +certificate fixes sector 3 and splits a joint space of the explicit pair. +The selected conditional kappa stays `781451/250000000`. Nothing here is a +characteristic polynomial, a basis, or a census of every operator outside +the signed-permutation group. + +The claim is a **proof**. The trace formula is an identity for commuting +involutions. The port operators, the 512 addresses, and the 64-element +group below are finite sets, and the verifier evaluates the identities on +every element of each set. That is not a heuristic search, and it is not an +exhaustive census of a larger matrix group. + +## Operators + +The input is the pinned 8-by-112 query, SHA256 +`5c6c51fbffc07a683e922f17532fd90262ae9e23cc3560a696002073dd234ef3`. +Its columns lie in `{-1,0,1}^8`, each has weight 4, and `R R^T = 56 I_8`. +The 112 port labels are distinct odd-weight vectors in `F_2^9`. + +Bell block `c=3` is the 4096-dimensional space `C^8 ⊗ C^{512}`. Write +`e=511` and + + B_3 = sum_q (r_q r_q^T) ⊗ P_q(3), + +where the sum runs over the 112 ports and, on an address `a`, + + P_q(3) e_a = e_{a+q} if q·3 = 1, + P_q(3) e_a = (-1)^{q·a} e_a if q·3 = 0. + +The degree-881 certificate attaches two payload involutions to this block: + + X_3 e_a = e_{a+3}, + Z_{508} e_a = (-1)^{(3+e)·a} e_a. + +Both act as the identity on the eight coordinates. Here `3+e = 508` and +`3·508 = 0`, so the two operators commute and their product is an +involution. In the certificate's sector notation, the eigenvalue of `X_3` +is `s` and the eigenvalue of `Z_{508}` is `(-1)^t`. + +The explicit pair from the c=3 certificate is + +| name | permutation | minus signs | +|---|---|---| +| `u` | `(0 2)(4 6)` | coordinates 0 and 2 | +| `v` | `(0 4)(2 6)` | coordinates 0 and 4 | +| `uv` | `(0 6)(2 4)` | coordinates 0 and 6 | + +`H` is the order-16 group of diagonal signs that are positive on the even +coordinates `{0,2,4,6}` and arbitrary on the odd coordinates `{1,3,5,7}`. +The 64 products of `{1,u,v,uv}` with `H` are the operators used below. Each +one is rebuilt from the query as a signed coordinate permutation whose +induced port map `T` is linear and orthogonal on `F_2^9`. + +## They lie outside the signed-permutation representation + +A symmetry coming from a signed coordinate permutation acts as `S ⊗ U_T`, +and `T` is linear, so `U_T` fixes the address `0`. Then + + (S ⊗ U_T)(e_0 ⊗ e_0) = ε[σ(0)] e_{σ(0)} ⊗ e_0. + +`X_3` sends that same vector to `e_0 ⊗ e_3`. The address moved, so `X_3` is +not equal to any such symmetry. `Z_{508}` fixes every address and multiplies +`e_0` by `+1` but `e_4` by `-1`, because bit 2 of 508 is set. A coordinate +sign does not depend on the address, so `Z_{508}` is not a signed +permutation either. The same address translation shows that the product is +not one. This is why the order-3072 stabilizer census does not decide these +operators. + +The certificate defines `X_c` and `Z_{c+e}` as operators on block `c`. For +`c ≠ 3` that block is a different summand of the Bell decomposition. Those +operators are not endomorphisms of sector 3. The Walsh transform sends label +3 to 508, so it does not fix the block either. The named payload involutions +from the certificate that fix sector 3 are exactly `X_3` and `Z_{508}`. +Their product is the remaining nontrivial word in those two operators. It +fixes the same block, and the trace table below shows that it splits every +joint space of this pair as well. + +## They commute with B_3 and with the joint projectors + +Every port has odd weight, so `q·e = 1` and `q·508 = q·3 + 1`. If `q·3 = 1`, +then `q·508 = 0`: translation by `q` commutes with the diagonal character +`Z_{508}`. If `q·3 = 0`, then `P_q(3)` is itself diagonal and commutes with +`Z_{508}`. Translations commute with `X_3`, and a diagonal `P_q(3)` has the +same sign at `a` and at `a+3` precisely because `q·3 = 0`. Thus both payload +involutions commute with every `P_q(3)`, and therefore with `B_3`. The +verifier also applies both sides to all 512 addresses for every port. + +Each of the 64 signed permutations was rebuilt from the query. For each one, +`T(3) = 3`, `T(508) = 508`, and `T(511) = 511`. The transpose of `T` inverts +`T` on every address. Consequently `T(a+3) = T(a)+3` and +`508·T(a) = 508·a`, so `S ⊗ U_T` commutes with both payload involutions. + +The same rebuild gives the conjugation identity on addresses, + + U_T P_q(3) U_T^{-1} = P_{Tq}(3), + +checked for every port and every address. On coordinates, the signed +permutation sends each column to `±` a column, so it permutes the rank-one +tensors `r_q r_q^T`. The sum `B_3` is therefore invariant. The spectral +projections of `u`, `v`, and the elements of `H` are polynomials in those +symmetries, so they commute with `B_3`. The payload involutions commute with +those symmetries, so they preserve every joint eigenspace, and `B_3` +preserves each intersection of a joint eigenspace with an eigenspace of +`X_3` or `Z_{508}`. + +`X_3` is diagonalizable because it is a fixed-point-free involution of the +addresses: each pair `{a, a+3}` contributes eigenvalues `±1`. `Z_{508}` is +already diagonal in the address basis. Their product is an involution on +each of those pairs because `3·508 = 0`, so it is diagonalizable as well. +The minimal polynomial of each restriction divides `x^2-1`, which has +distinct roots, so the restrictions to an invariant joint space remain +diagonalizable. For an involution of trace `τ` on a space of dimension `d`, +the eigenvalue dimensions are `(d+τ)/2` and `(d-τ)/2`. + +## Traces + +On a signed permutation `g = S ⊗ U_T`, the block trace of +`I ⊗ (τ_b χ_f) ∘ g` factors as the product of the coordinate trace and the +address trace. The coordinate trace is the signed count of fixed +coordinates. The address trace counts solutions of `(T+I)a = b`, weighted +by `(-1)^{f·T(a)}`. The verifier computes that count by enumerating all 512 +addresses and, separately, by solving the affine equation and summing the +character on its kernel. The two counts agree on every element and every +operator used here. + +Let `P_{χ,ε,δ}` be the projector onto the `χ`-isotypic component of `H` and +the `(ε,δ)` joint eigenspace of `(u,v)`. Since `H`, `u`, and `v` commute and +are involutions, + + tr(W P_{χ,ε,δ}) + = (1/64) sum_{h in H} χ(h) + [tr(Wh) + ε tr(Wuh) + δ tr(Wvh) + εδ tr(Wuvh)]. + +The same formula with `W = I` reproduces the published joint dimensions, +including `216^4` on the trivial character and `8^4` on the unique +32-dimensional character. The character dimensions themselves are the +published histogram + + {864: 1, 432: 4, 192: 6, 80: 4, 32: 1}. + +Summing the four `(s,t)` intersections over all 16 characters and all four +`(u,v)` eigenvalues rebuilds four blocks of dimension 1024, which are the +degree-881 sectors of this Bell block. The `+1` space of `X_3` on the whole +block has dimension 2048, matching its global trace 0. + +## The split + +`Z_{508}` and the product `X_3 Z_{508}` have trace 0 on every joint space of +this pair. Every joint dimension below is positive and even, so each of +those two involutions splits every joint space in half. + +`X_3` does not act by a scalar on any of them. Its traces depend only on the +character weight and on the `(u,v)` eigenvalues: + +| weight | dimensions `(++,+-, -+, --)` | traces of `X_3` | +|---:|---|---| +| 0 | 216, 216, 216, 216 | -48, 16, 16, 16 | +| 1 | 180, 84, 84, 84 | 36, -12, -12, -12 | +| 2 | 48, 48, 48, 48 | -24, 8, 8, 8 | +| 3 | 44, 12, 12, 12 | 12, -4, -4, -4 | +| 4 | 8, 8, 8, 8 | 0, 0, 0, 0 | + +On the trivial character, the `(+1,+1)` space has dimension 216 and `X_3` +has trace `-48`. The eigenvalue `+1` therefore has dimension **84** and the +eigenvalue `-1` has dimension **132**. Both summands are `B_3`-invariant. +`Z_{508}` splits the same space as **108 + 108**. The address trace of +`Z_{508}`, and of the product, is already 0 on each of the 64 group +elements, so the joint traces vanish before the character average. Because +those traces are 0, `Z_{508}` halves each `X_3` eigenspace. The +intersections with the four degree-881 sectors `(s,t)` are + +| `(s,t)` | dimension inside the 216-space | +|---|---:| +| `(+1, 0)` | 42 | +| `(+1, 1)` | 42 | +| `(-1, 0)` | 66 | +| `(-1, 1)` | 66 | + +All four are positive, so this joint space meets every sector of the +degree-881 splitting of block 3. The same four-way count is positive on +every other joint space of this pair. In particular each 8-dimensional +weight-4 joint space meets all four sectors in dimension 2. That is a +dimension count. It is not the characteristic polynomial of an +8-dimensional joint space, and it is not the characteristic polynomial of a +16-dimensional sum of two of them. + +The other three trivial joint spaces have `X_3` trace 16, hence split as +116 + 100, and their sector intersections are 58, 58, 50, and 50. + +## What is not claimed + +The argument uses this query, Bell block 3, the named operators `X_3` and +`Z_{508}`, the order-16 group `H`, and the explicit pair `(u,v)`. It does +not list a basis and does not compute a minimal or characteristic +polynomial. It does not say that an arbitrary operator outside the +signed-permutation group splits these spaces. It does not rerun the +degree-881 coefficient certificate. A 42-dimensional invariant subspace +does not replace that certificate. The selected conditional kappa is +unchanged. + +The rejection controls are part of the verifier, not part of the theorem. A +translation by 1 does not commute with `u`. The address character of the +vector 1 does not commute with every port operator. Dropping one element of +`H` does not reproduce dimension 864. The identity trace on the 216-space is +216, not `-48`. The coordinate transposition `(0 1)` is not a symmetry of +the query. diff --git a/research/c3-payload-sector3-split/README.md b/research/c3-payload-sector3-split/README.md new file mode 100644 index 0000000000..6009fe9fac --- /dev/null +++ b/research/c3-payload-sector3-split/README.md @@ -0,0 +1,122 @@ +# Payload involutions split a sector-3 joint space + +Prepared by unpaidmoon with substantial Cursor Grok assistance. Apache-2.0. + +For the historical 8-by-112 centre query, the degree-881 payload involutions +that fix Bell block `c=3` are `X_3` and `Z_{508}`. Both lie outside the +signed-permutation group classified for this block. On the explicit +commuting pair from that classification, `X_3` splits the trivial +`(+1,+1)` joint space of dimension 216 into `B_3`-invariant subspaces of +dimensions **84** (eigenvalue `+1`) and **132** (eigenvalue `-1`). +`Z_{508}` splits the same space into dimensions **108 and 108**. The +intersections of that 216-space with the four degree-881 sectors have +dimensions **42, 42, 66, and 66**. + +The selected conditional kappa stays `781451/250000000`. [PROOF.md](PROOF.md) +separates the trace-formula proof from the facts that are not claimed. + +## Result + +The live input is the query pinned in [SOURCES.json](SOURCES.json), SHA256 +`5c6c51fbffc07a683e922f17532fd90262ae9e23cc3560a696002073dd234ef3`. +`X_3` translates addresses by 3. `Z_{508}` is the diagonal character of +`3 xor 511`. They commute with each other, with `B_3`, and with the +order-64 group generated by the explicit pair + + u = (0 2)(4 6) with minus signs on coordinates 0 and 2, + v = (0 4)(2 6) with minus signs on coordinates 0 and 4, + +together with the order-16 sign group that is positive on the even +coordinates. The joint dimensions of that pair match the published c=3 +table, including `216^4` on the trivial character. + +`X_3` has trace `-48` on the trivial `(+1,+1)` space. Its `+1` eigenspace +there has dimension 84 and its `-1` eigenspace has dimension 132. The same +trace formula gives both eigenvalues on every other joint space of this +pair. The address trace of `Z_{508}`, and of the product, is 0 on each of +the 64 group elements, so every joint trace of those two operators is 0 +and each joint space is split in half. Inside the 216-space, the +intersections with the four degree-881 sectors are 42, 42, 66, and 66, for +`(s,t)` equal to `(+1,0)`, `(+1,1)`, `(-1,0)`, and `(-1,1)`. Summing those +intersections over every character and every joint eigenvalue rebuilds the +four 1024-dimensional sectors. + +This is a proof. The address counts are exhaustive on a set of 512 +elements, once by enumeration and once by an affine solve, and the two +counts agree. It is not a stopped search and not a claim that every +operator outside the signed-permutation group splits these spaces. + +## Scope + +Catalogue card `formal-interface-lemma` asks for a formal interface binding. +The live question is open question 2 of +[PR #6965](https://github.com/CrocSwap/integer-mult-bounds/pull/6965), +recorded in discussion comment +[19507308](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19507308). +The predecessor classifies signed permutations only. This package starts +from the payload involutions named in Krzysztof Wojt's degree-881 +certificate and tests the ones whose block is sector 3. + +It does not redo that signed-permutation census, and it does not compute a +characteristic polynomial. The 16-dimensional weight-4 calculation left +open by #6965 stays open; the trace table here only records that each +8-dimensional weight-4 joint space meets the four sectors in dimension 2. +The 216-dimensional `c=1` polynomial is a different block. + +Selected-baseline orientation returned `PASS_RESEARCH_BASELINE_BINDINGS_ONLY` +for kappa `781451/250000000`. + +## Reproduce + +From the repository root, with CPython 3.12 and the standard library: + +```sh +python3 -B -W error research/c3-payload-sector3-split/verify.py +python3 -B -O research/c3-payload-sector3-split/verify.py +python3 -B scripts/research_package.py --package research/c3-payload-sector3-split --check-only +``` + +The direct marker is `PASS_C3_PAYLOAD_SECTOR3_SPLIT`. Acceptance uses +explicit checks, so `-O` does not skip them. The run rebuilds the 64 +symmetries from the query, checks commutation on every port and every +address, and evaluates the joint trace formula. On the measured host that +takes about five seconds. Rejection controls are a translation by 1, an +address character other than 508, a truncated sign average, the identity +trace on the same 216-space, and a coordinate transposition. No Lean, +Docker, degree-881 coefficient replay, or selected cold replay was run. + +## Overlap + +`scripts/find_overlap.py` was refreshed on 2026-11-10 against upstream +`17469fff78c22941280f04d39dc5a1faee09c840`. Coverage: local notes 10178 of +10178 HEAD paths, complete; 317 open PRs, pagination complete, fetched +2026-11-10T08:48:35Z; 6971 discussion records, pagination complete, fetched +2026-11-10T08:49:37Z. Closed PRs were searched through local READMEs, task +metadata and the ledger only. + +The phrase `payload involution` matches the degree-881 certificate, the +#6965 finding that leaves this question open, and the two local notes that +point at it. No open PR body reports a trace of `X_3` or `Z_{508}` on a +sector-3 joint space. This search is not a novelty certificate. + +## Open next questions + +The structured list is in [TASK.json](TASK.json). + +- The characteristic polynomial of the 84-dimensional `X_3 = +1` subspace + of the trivial `(+1,+1)` joint space is still uncomputed. It would place + this split inside the known degree-881 polynomial. The trace formula + gives the dimension without a basis. +- One other cross-coset pair, with a different odd sign, might move the + trace `-48` onto another `(u,v)` eigenvalue. This package fixes the + explicit masks from #6965. + +## Credit + +JoyboyBrian's handoff recorded the sign-character dimensions. The explicit +pair, the joint dimensions, and the signed-permutation boundary are the +certificate in upstream PR #6965. Ali Romman's PR4958 and PR4720 retain the +query and the Bell action. Nick Petalas's PR5120 is the degree-410 lower +bound. Krzysztof Wojt's exact one-slot package defines `X_c` and `Z_{c+e}` +and is the degree-881 annihilator. The doubled representation comes from +PR1719. New work is Apache-2.0. diff --git a/research/c3-payload-sector3-split/SOURCES.json b/research/c3-payload-sector3-split/SOURCES.json new file mode 100644 index 0000000000..a16afb78ce --- /dev/null +++ b/research/c3-payload-sector3-split/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "17469fff78c22941280f04d39dc5a1faee09c840", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/c3-centre-sign-split/PROOF.md", + "usage": "provenance", + "git_blob": "8da44a79e0e3f7d3cfcd7ebb8c46cc46146a9869", + "sha256": "6d9446760eb90201b96a73c78a04fdc0320c0c3973dc9d96f05a7fd135a45558" + }, + { + "path": "research/centre-polynomial-cache-limits/frozen/work/centre-encoding-campaign-20261014/lanes/circuit-interface/INTERFACE.json", + "usage": "input", + "git_blob": "4201e9a04c12273b919e2cae60a6b6482c8150f3", + "sha256": "5c6c51fbffc07a683e922f17532fd90262ae9e23cc3560a696002073dd234ef3" + }, + { + "path": "research/exact-one-slot-gram/PROOF.md", + "usage": "provenance", + "git_blob": "91854803c13d19d7962aafedf37aca0004827514", + "sha256": "30ccfa6d6623313a3c73c7107b7d9c3872eeffc07d2062e7e9b797162585e9b4" + } + ] +} diff --git a/research/c3-payload-sector3-split/TASK.json b/research/c3-payload-sector3-split/TASK.json new file mode 100644 index 0000000000..fcee5d901c --- /dev/null +++ b/research/c3-payload-sector3-split/TASK.json @@ -0,0 +1,118 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 8, + "base_commit": "17469fff78c22941280f04d39dc5a1faee09c840", + "original_card": { + "id": "formal-interface-lemma", + "question": "Can one uncovered interface implication be formalized with exact caller and certificate bindings?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/gate-operand-parity-lean/README.md", + "research/staged544-certified-endpoint/README.md", + "research/unconditional-batched-crt/README.md" + ], + "methods": [ + "Formalize a missing boundary lemma identified by the selected review.", + "Audit a formal theorem-to-certificate binding independently." + ], + "acceptance_gate": "State the exact formalized proposition and remaining assumptions; avoid duplicate arithmetic formalizations already present.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.", + "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse." + }, + "first_experiment": "Write one missing statement with quantified hypotheses, actual caller and existing coverage. A compact-switch lemma is a candidate only after its mathematical contract is reviewed. Establish a bounded proof plan before a separately budgeted proof-assistant build; do not rerun large Lean jobs as orientation.", + "bottleneck_link": "A missing interface proof can reduce the conditional gap even if it does not change kappa.", + "allowed_variations": [ + "Narrow to one formal lemma or one theorem-to-certificate binding." + ], + "scope_change_triggers": [ + "Formalizing already-covered arithmetic and claiming the full multiplication theorem." + ], + "overlap_terms": [ + "hyperplane end", + "formal interface", + "Lean binding", + "3807", + "3857", + "4100", + "gate-operand-parity-lean", + "staged544-certified-endpoint", + "unconditional-batched-crt" + ], + "existing_checks": [ + { + "scope": "PR #3807: scoped gate-operand parity formalization.", + "evidence": "research/gate-operand-parity-lean/README.md", + "remaining": "Exact theorem-to-caller binding and genuinely uncovered interface lemmas.", + "status": "author-checked", + "source_commit": "4c3530f42a6abcc48e7a6bcffd6c901911dc8269", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #3857: certified real-power moment/endpoint arithmetic.", + "evidence": "research/staged544-certified-endpoint/README.md", + "remaining": "Uniform algorithmic implications, not another endpoint digit.", + "status": "author-checked", + "source_commit": "ef4315b8caa605e47a2515004845eb2d2ed71a86", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4100: compact-switch formalization proposed as future validation.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Audit the statement and assumptions before a formal proof campaign.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Prove that the degree-881 payload involutions X_3 and Z_508 fix Bell block c=3, lie outside the signed-permutation representation, and split every joint eigenspace of the explicit c=3 pair. The trivial (+1,+1) space of dimension 216 splits as 84+132 under X_3 and as 42+42+66+66 under the pair of involutions.", + "scope_change_reason": "The catalogue card asks for a formal caller or certificate binding. Open question 2 of upstream PR #6965 asks whether a payload involution from the degree-881 certificate fixes sector 3 and splits a joint space of the explicit pair. Those operators are outside the signed-permutation census. This package answers that finite trace question. It does not add a Lean binding and it does not compute a characteristic polynomial.", + "bottleneck_link": "Scoped side result on the historical centre Gram. The selected conditional kappa remains 781451/250000000. These finer invariant subspaces do not replace the degree-881 one-slot certificate and do not admit a supplier.", + "budget_minutes": 60, + "stop_rule": "Stop once X_3 and Z_508 are checked on all 64 joint spaces of the explicit pair, both eigenvalue dimensions are positive, and the rejection controls pass. Do not build a basis or rerun the degree-881 coefficient certificate.", + "outcome": "completed", + "evidence": "verify.py recomputes the traces from INTERFACE.json in normal and optimized modes. Marker PASS_C3_PAYLOAD_SECTOR3_SPLIT. X_3 has trace -48 on the trivial (+1,+1) space and splits it as 84+132. The four sector intersections are 42, 42, 66, and 66. Address traces agree by enumeration and by affine solution. Selected baseline returned PASS_RESEARCH_BASELINE_BINDINGS_ONLY.", + "author": "unpaidmoon", + "ai_assistance": "Prepared by unpaidmoon with substantial Cursor Grok assistance. The assistant derived the commutation argument and the joint trace formula and wrote the verifier. This is not an independent human or proof-kernel review.", + "open_questions": [ + { + "question": "What is the characteristic polynomial of the 84-dimensional X_3=+1 subspace of the trivial (+1,+1) joint space?", + "why_it_matters": "It would place this finer split inside the known degree-881 one-slot polynomial. The subspace is the +1 eigenspace of X_3 inside the trivial c=3 joint space, not a 216-dimensional c=1 summand and not the weight-4 c=3 summand.", + "first_step": "Build an exact basis of the joint equations for H, u, v, and X_3=+1, then compute the characteristic polynomial of B_3 on that basis in characteristic zero.", + "blocked_by": "The trace formula certifies dimension 84 without listing a vector. Constructing the matrix was not run." + }, + { + "question": "Does one other cross-coset pair, with a different odd sign, move the X_3 trace -48 onto a different (u,v) eigenvalue?", + "why_it_matters": "The predecessor records that other cross-coset pairs keep the same joint-dimension multiset and move which slot is large. The trace -48 might move with those signs, or it might be fixed by the even permutations alone.", + "first_step": "Repeat the joint trace of X_3 for the same permutations with one odd minus sign added to u, and compare the four traces with -48, 16, 16, 16.", + "blocked_by": "This package fixes the explicit masks U_MASK=5 and V_MASK=17 from PR #6965. The other 3071 cross-coset pairs were not evaluated." + } + ], + "environment": { + "python": "3.12.3", + "platform": "linux" + }, + "overlap": { + "checked_at": "2026-11-10T08:49:37Z", + "canonical_main": "17469fff78c22941280f04d39dc5a1faee09c840", + "open_pr_records": 317, + "discussion_records": 6971, + "remote_pagination_complete": true, + "local_records": 10178, + "head_records": 10178, + "local_coverage_complete": true, + "predecessor_pr": "https://github.com/CrocSwap/integer-mult-bounds/pull/6965", + "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19507308", + "limits": "Closed PRs were searched through local READMEs, TASK metadata and the ledger. No code diffs or unpublished work. The phrase payload involution matches the degree-881 certificate and the open question, not a computed trace." + } +} diff --git a/research/c3-payload-sector3-split/VERIFY.json b/research/c3-payload-sector3-split/VERIFY.json new file mode 100644 index 0000000000..fd5ec3e845 --- /dev/null +++ b/research/c3-payload-sector3-split/VERIFY.json @@ -0,0 +1,32 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/centre-polynomial-cache-limits/frozen/work/centre-encoding-campaign-20261014/lanes/circuit-interface/INTERFACE.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "-W", + "error", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Rebuild the explicit c=3 pair and H from the query, check that X_3 and Z_508 commute with every port operator and all 64 symmetries, and require the trivial 216-space to split as 84+132 and as sector dimensions 42, 42, 66, 66. Five rejection controls must fire." + }, + { + "argv": [ + "{python}", + "-B", + "-O", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Repeat the same certificate with assertions removed. Acceptance uses explicit checks, so optimization does not skip a trace or a rejection control." + } + ] +} diff --git a/research/c3-payload-sector3-split/verify.py b/research/c3-payload-sector3-split/verify.py new file mode 100644 index 0000000000..94a91a488b --- /dev/null +++ b/research/c3-payload-sector3-split/verify.py @@ -0,0 +1,656 @@ +#!/usr/bin/env python3 +"""Prove that the degree-881 payload involutions split a c=3 joint space. + +X_3 and Z_{3 xor 511} are the payload involutions attached to Bell block 3 in +research/exact-one-slot-gram/PROOF.md. They are not coordinate signed +permutations. On the explicit pair from research/c3-centre-sign-split, both +eigenvalues occur on every joint space. Acceptance uses explicit checks, so +python -O does not skip a step. +""" + +import hashlib +import json +import pathlib + +ROOT = pathlib.Path(__file__).resolve().parents[2] +INTERFACE = ( + ROOT + / "research/centre-polynomial-cache-limits/frozen/work" + / "centre-encoding-campaign-20261014/lanes/circuit-interface/INTERFACE.json" +) +SELECTED = ROOT / "certificates/selected-result.json" +INTERFACE_SHA256 = ( + "5c6c51fbffc07a683e922f17532fd90262ae9e23cc3560a696002073dd234ef3" +) +SELECTED_KAPPA = "781451/250000000" +SECTOR = 3 +ALL_ONE = 511 +SHIFT = SECTOR +CHARACTER = SECTOR ^ ALL_ONE # 508 +ODDS = (1, 3, 5, 7) +U_SIGMA = (2, 1, 0, 3, 6, 5, 4, 7) # (0 2)(4 6) +U_MASK = 5 # minus signs on (0 2) +V_SIGMA = (4, 1, 6, 3, 0, 5, 2, 7) # (0 4)(2 6) +V_MASK = 17 # minus signs on (0 4) +JOINT_ORDER = ((1, 1), (1, -1), (-1, 1), (-1, -1)) +# Published c=3 sign-character dimensions, indexed by the F_2^4 character. +CHARACTER_DIMENSIONS = ( + 864, 432, 432, 192, 432, 192, 192, 80, + 432, 192, 192, 80, 192, 80, 80, 32, +) +# Joint (u, v) dimensions and X_3 traces, in JOINT_ORDER, by character weight. +# Z_{508} and the product have trace 0 on every one of these spaces. +EXPECTED_BY_WEIGHT = { + 0: ((216, 216, 216, 216), (-48, 16, 16, 16)), + 1: ((180, 84, 84, 84), (36, -12, -12, -12)), + 2: ((48, 48, 48, 48), (-24, 8, 8, 8)), + 3: ((44, 12, 12, 12), (12, -4, -4, -4)), + 4: ((8, 8, 8, 8), (0, 0, 0, 0)), +} + + +def fail(message): + raise SystemExit("FAIL: " + message) + + +def expect(condition, message): + if not condition: + fail(message) + + +def dot(left, right): + return bin(left & right).count("1") & 1 + + +def apply_map(matrix, address): + image = 0 + for bit in range(9): + if (address >> bit) & 1: + image ^= matrix[bit] + return image + + +def compose_maps(left, right): + return tuple(apply_map(left, column) for column in right) + + +def inverse_map(matrix): + inverse = [0] * 9 + for bit in range(9): + image = matrix[bit] + for row in range(9): + if (image >> row) & 1: + inverse[row] |= 1 << bit + return tuple(inverse) + + +def sha256_file(path): + digest = hashlib.sha256() + digest.update(path.read_bytes()) + return digest.hexdigest() + + +def mask_to_eps(mask): + return tuple(-1 if (mask >> bit) & 1 else 1 for bit in range(8)) + + +def eps_to_mask(eps): + return sum(1 << bit for bit in range(8) if eps[bit] < 0) + + +def inv_of(sigma): + inverse = [0] * 8 + for source, image in enumerate(sigma): + inverse[image] = source + return tuple(inverse) + + +def compose_perm(left, right): + return tuple(left[right[index]] for index in range(8)) + + +def compose_signed(left_sigma, left_mask, right_sigma, right_mask): + """Compose operators, right applied first. + + (Sv)_k = eps[k] * v[sigma^{-1}(k)]. + """ + sigma = compose_perm(left_sigma, right_sigma) + left_inv = inv_of(left_sigma) + eps = [] + for index in range(8): + left_sign = -1 if (left_mask >> index) & 1 else 1 + source = left_inv[index] + right_sign = -1 if (right_mask >> source) & 1 else 1 + eps.append(left_sign * right_sign) + return sigma, eps_to_mask(eps) + + +def norm_code(values): + code = 0 + sign = 1 + seen = False + for index, value in enumerate(values): + if value == 0: + continue + if not seen: + seen = True + sign = 1 if value > 0 else -1 + signed = value * sign + code |= (1 if signed > 0 else 2) << (2 * index) + return code + + +def rank_solve(vectors, target=None): + width = len(vectors) + matrix = [[(vector >> row) & 1 for vector in vectors] for row in range(9)] + image = None if target is None else [(target >> row) & 1 for row in range(9)] + pivot_at = [-1] * 9 + rank = 0 + for col in range(width): + pivot = None + for row in range(rank, 9): + if matrix[row][col]: + pivot = row + break + if pivot is None: + continue + matrix[rank], matrix[pivot] = matrix[pivot], matrix[rank] + if image is not None: + image[rank], image[pivot] = image[pivot], image[rank] + for row in range(9): + if row != rank and matrix[row][col]: + for entry in range(width): + matrix[row][entry] ^= matrix[rank][entry] + if image is not None: + image[row] ^= image[rank] + pivot_at[rank] = col + rank += 1 + if rank == 9: + break + if target is None: + return rank + if any(image[row] for row in range(rank, 9)): + return None + coef = [0] * width + for row in range(rank): + coef[pivot_at[row]] = image[row] + return coef + + +def coordinate_trace(sigma, mask): + total = 0 + for index in range(8): + if sigma[index] == index: + total += -1 if (mask >> index) & 1 else 1 + return total + + +def chi_value(chi, mask): + sign = 0 + for index, coordinate in enumerate(ODDS): + if (chi >> index) & 1 and (mask >> coordinate) & 1: + sign ^= 1 + return -1 if sign else 1 + + +def payload_action(label, sector, address): + """P_label(sector) on one address: image and sign.""" + if dot(label, sector): + return address ^ label, 1 + sign = -1 if dot(label, address) else 1 + return address, sign + + +def address_trace_enumerate(matrix, translation, character): + total = 0 + for address in range(512): + image = apply_map(matrix, address) + if (image ^ translation) == address: + total += -1 if dot(character, image) else 1 + return total + + +def address_trace_linear(matrix, translation, character): + """Same trace by solving (T+I)a = translation over F_2.""" + rows = [] + for row in range(9): + coef = 0 + for col in range(9): + image = matrix[col] ^ (1 << col) + if (image >> row) & 1: + coef |= 1 << col + rhs = (translation >> row) & 1 + rows.append(coef | (rhs << 9)) + pivot_of = [-1] * 9 + rank = 0 + for col in range(9): + pivot = None + for row in range(rank, 9): + if (rows[row] >> col) & 1: + pivot = row + break + if pivot is None: + continue + rows[rank], rows[pivot] = rows[pivot], rows[rank] + for row in range(9): + if row != rank and (rows[row] >> col) & 1: + rows[row] ^= rows[rank] + pivot_of[rank] = col + rank += 1 + for row in range(rank, 9): + if (rows[row] >> 9) & 1: + return 0 + particular = 0 + for row in range(rank): + if (rows[row] >> 9) & 1: + particular |= 1 << pivot_of[row] + pivots = set(pivot_of[:rank]) + kernel = [] + for col in range(9): + if col in pivots: + continue + vector = 1 << col + for row in range(rank): + if (rows[row] >> col) & 1: + vector ^= 1 << pivot_of[row] + kernel.append(vector) + if any(dot(character, vector) for vector in kernel): + return 0 + # On solutions, T(a) = a xor translation. + sign_bit = dot(character, particular) ^ dot(character, translation) + sign = -1 if sign_bit else 1 + return sign * (1 << len(kernel)) + + +def address_trace(matrix, translation, character): + enumerated = address_trace_enumerate(matrix, translation, character) + solved = address_trace_linear(matrix, translation, character) + expect( + enumerated == solved, + "address-trace methods disagree for translation " + + str(translation) + + " character " + + str(character) + + ": " + + str(enumerated) + + " vs " + + str(solved), + ) + return enumerated + + +def load_query(): + expect(sha256_file(INTERFACE) == INTERFACE_SHA256, "INTERFACE.json hash changed") + selected = json.loads(SELECTED.read_text()) + expect(selected["kappa"] == SELECTED_KAPPA, "selected kappa is not 781451/250000000") + data = json.loads(INTERFACE.read_text()) + ports = [int(port) for port in data["ports"]] + rows = data["R"] + columns = [ + tuple(int(rows[row].get(str(column), "0")) for row in range(8)) + for column in range(112) + ] + expect(len(ports) == 112 and len(set(ports)) == 112, "ports are not 112 distinct labels") + expect( + all(value in (-1, 0, 1) for column in columns for value in column), + "a column entry is outside {-1,0,1}", + ) + gram = [[0] * 8 for _ in range(8)] + for column in columns: + weight = sum(1 for value in column if value) + expect(weight == 4, "a column does not have weight 4") + for index, value in enumerate(column): + for other in range(8): + gram[index][other] += value * column[other] + expect( + all(gram[i][k] == (56 if i == k else 0) for i in range(8) for k in range(8)), + "RR^T is not 56 I", + ) + expect(all(dot(port, ALL_ONE) == 1 for port in ports), "a port label has even weight") + expect(dot(SHIFT, CHARACTER) == 0, "X_3 and Z_508 do not commute") + expect(CHARACTER == 508, "the sector character is not 508") + for port in ports: + if dot(port, SECTOR) == 1: + expect(dot(port, CHARACTER) == 0, "an odd port meets Z_508 while translating by the sector") + return columns, ports + + +def prepare_labels(columns, ports): + lookup = [-1] * (1 << 16) + for column, port in zip(columns, ports): + lookup[norm_code(column)] = port + basis = [] + for port in ports: + if rank_solve(basis + [port]) == len(basis) + 1: + basis.append(port) + if len(basis) == 9: + break + expect(len(basis) == 9, "ports do not span F2^9") + coords = [rank_solve(basis, 1 << bit) for bit in range(9)] + contrib = [[index for index, bit in enumerate(row) if bit] for row in coords] + basis_columns = [columns[ports.index(port)] for port in basis] + return lookup, basis_columns, contrib + + +def realize(lookup, columns, ports, basis_columns, contrib, sigma, mask): + inverse = inv_of(sigma) + port_of = {} + for column, port in zip(columns, ports): + values = [] + for index in range(8): + value = column[inverse[index]] + if value and (mask >> index) & 1: + value = -value + values.append(value) + found = lookup[norm_code(values)] + if found < 0: + return None + port_of[port] = found + basis_images = [] + for column in basis_columns: + values = [] + for index in range(8): + value = column[inverse[index]] + if value and (mask >> index) & 1: + value = -value + values.append(value) + found = lookup[norm_code(values)] + if found < 0: + return None + basis_images.append(found) + matrix = [] + for bit in range(9): + acc = 0 + for index in contrib[bit]: + acc ^= basis_images[index] + matrix.append(acc) + matrix = tuple(matrix) + for port, image in port_of.items(): + if apply_map(matrix, port) != image: + return None + for left in range(9): + for right in range(left, 9): + if dot(matrix[left], matrix[right]) != (1 if left == right else 0): + return None + block = coordinate_trace(sigma, mask) * address_trace(matrix, 0, 0) + return { + "sigma": sigma, + "mask": mask, + "T": matrix, + "trace": block, + } + + +def conjugation_holds(matrix, ports): + """U P_q(3) U^{-1} = P_{Tq}(3) on every address.""" + for port in ports: + image_port = apply_map(matrix, port) + for address in range(512): + moved, sign = payload_action(port, SECTOR, address) + transported = apply_map(matrix, moved) + expected, expected_sign = payload_action( + image_port, SECTOR, apply_map(matrix, address) + ) + if transported != expected or sign != expected_sign: + return False + return True + + +def commutes_with_translation(port, shift): + for address in range(512): + moved, sign = payload_action(port, SECTOR, address) + other, other_sign = payload_action(port, SECTOR, address ^ shift) + if (moved ^ shift) != other or sign != other_sign: + return False + return True + + +def commutes_with_character(port, character): + for address in range(512): + moved, _sign = payload_action(port, SECTOR, address) + if dot(character, moved) != dot(character, address): + return False + return True + + +def sign_masks(): + masks = [] + for odds in range(16): + mask = 0 + for index, coordinate in enumerate(ODDS): + if (odds >> index) & 1: + mask |= 1 << coordinate + masks.append(mask) + return masks + + +def eigenvalue_split(dimension, trace): + expect((dimension + trace) % 2 == 0, "involution trace has the wrong parity") + positive = (dimension + trace) // 2 + negative = (dimension - trace) // 2 + expect(positive >= 0 and negative >= 0, "an eigenvalue dimension is negative") + expect(positive + negative == dimension, "eigenvalues do not cover the space") + return positive, negative + + +def four_way(dimension, trace_x, trace_z, trace_xz): + spaces = {} + for eigenvalue_x in (1, -1): + for eigenvalue_z in (1, -1): + sector_t = 0 if eigenvalue_z == 1 else 1 + numerator = ( + dimension + + eigenvalue_x * trace_x + + eigenvalue_z * trace_z + + eigenvalue_x * eigenvalue_z * trace_xz + ) + expect(numerator % 4 == 0 and numerator >= 0, "four-way dimension is not a nonnegative quarter") + spaces[(eigenvalue_x, sector_t)] = numerator // 4 + expect(sum(spaces.values()) == dimension, "four-way spaces miss the joint space") + return spaces + + +def main(): + columns, ports = load_query() + lookup, basis_columns, contrib = prepare_labels(columns, ports) + + def build(sigma, mask): + return realize(lookup, columns, ports, basis_columns, contrib, sigma, mask) + + for port in ports: + expect(commutes_with_translation(port, SHIFT), "X_3 fails to commute with a port operator") + expect(commutes_with_character(port, CHARACTER), "Z_508 fails to commute with a port operator") + + identity = build(tuple(range(8)), 0) + expect(identity is not None and identity["trace"] == 4096, "the identity trace is not 4096") + u = build(U_SIGMA, U_MASK) + v = build(V_SIGMA, V_MASK) + expect(u is not None and v is not None, "the explicit pair is not a symmetry of the query") + product_sigma, product_mask = compose_signed(U_SIGMA, U_MASK, V_SIGMA, V_MASK) + expect(product_sigma == (6, 1, 4, 3, 2, 5, 0, 7), "the explicit product is not (0 6)(2 4)") + expect(product_mask == 65, "the explicit product has an unexpected sign") + uv = build(product_sigma, product_mask) + expect(uv is not None, "the explicit product is not a symmetry") + back_sigma, back_mask = compose_signed(V_SIGMA, V_MASK, U_SIGMA, U_MASK) + expect((back_sigma, back_mask) == (product_sigma, product_mask), "u and v do not commute") + + sign_group = [] + for mask in sign_masks(): + element = build(tuple(range(8)), mask) + expect(element is not None, "a positive-even sign is not a symmetry") + sign_group.append(element) + expect(len(sign_group) == 16, "H does not have order 16") + + bases = {"I": identity, "u": u, "v": v, "uv": uv} + elements = {} + for name, base in bases.items(): + for member in sign_group: + if name == "I": + element = member + else: + sigma, mask = compose_signed( + base["sigma"], base["mask"], member["sigma"], member["mask"] + ) + element = build(sigma, mask) + expect(element is not None, "a product left the symmetry representation") + expect( + element["T"] == compose_maps(base["T"], member["T"]), + "label maps do not multiply", + ) + expect(inv_of(element["sigma"]) == element["sigma"], "a group element is not an involution") + expect( + compose_signed(element["sigma"], element["mask"], element["sigma"], element["mask"]) + == (tuple(range(8)), 0), + "a group element does not square to the identity", + ) + matrix = element["T"] + inverse = inverse_map(matrix) + expect(apply_map(matrix, SECTOR) == SECTOR, "an element moves sector 3") + expect(apply_map(matrix, ALL_ONE) == ALL_ONE, "an element moves the all-one label") + expect(apply_map(matrix, CHARACTER) == CHARACTER, "an element moves 508") + for address in range(512): + expect( + apply_map(inverse, apply_map(matrix, address)) == address, + "a label map is not inverted by its transpose", + ) + expect( + apply_map(matrix, address ^ SHIFT) == (apply_map(matrix, address) ^ SHIFT), + "X_3 does not commute with a group element", + ) + expect( + dot(CHARACTER, apply_map(matrix, address)) == dot(CHARACTER, address), + "Z_508 does not commute with a group element", + ) + expect(conjugation_holds(matrix, ports), "port conjugation fails on a group element") + elements[(name, member["mask"])] = element + expect(len(elements) == 64, "the Klein coset of H is not 64 elements") + + dimensions = [] + for chi in range(16): + total = sum(chi_value(chi, element["mask"]) * element["trace"] for element in sign_group) + expect(total % 16 == 0, "a character dimension is not integral") + dimensions.append(total // 16) + expect(tuple(dimensions) == CHARACTER_DIMENSIONS, "c=3 character dimensions changed") + + operators = { + "I": (0, 0), + "X": (SHIFT, 0), + "Z": (0, CHARACTER), + "XZ": (SHIFT, CHARACTER), + } + traces = {name: {} for name in operators} + for key, element in elements.items(): + for name, (translation, character) in operators.items(): + counted = address_trace(element["T"], translation, character) + if name in ("Z", "XZ"): + expect(counted == 0, "Z_508 or the product fixes a weighted address") + traces[name][key] = coordinate_trace(element["sigma"], element["mask"]) * counted + expect(traces["I"][key] == element["trace"], "the identity payload trace drifted") + + def joint_trace(op_name, chi, eps, delta): + total = 0 + for member in sign_group: + chi_h = chi_value(chi, member["mask"]) + terms = ( + (1, "I"), + (eps, "u"), + (delta, "v"), + (eps * delta, "uv"), + ) + for coef, name in terms: + total += chi_h * coef * traces[op_name][(name, member["mask"])] + expect(total % 64 == 0, "a joint trace is not a multiple of 64") + return total // 64 + + sector_total = {(1, 0): 0, (1, 1): 0, (-1, 0): 0, (-1, 1): 0} + x_positive = 0 + headline = None + for chi in range(16): + weight = bin(chi).count("1") + expected_dims, expected_x = EXPECTED_BY_WEIGHT[weight] + for index, (eps, delta) in enumerate(JOINT_ORDER): + dimension = joint_trace("I", chi, eps, delta) + trace_x = joint_trace("X", chi, eps, delta) + trace_z = joint_trace("Z", chi, eps, delta) + trace_xz = joint_trace("XZ", chi, eps, delta) + expect(dimension == expected_dims[index], "a joint dimension changed") + expect(trace_x == expected_x[index], "an X_3 joint trace changed") + expect(trace_z == 0 and trace_xz == 0, "Z_508 or the product has a nonzero joint trace") + positive, negative = eigenvalue_split(dimension, trace_x) + expect(positive > 0 and negative > 0, "X_3 misses an eigenvalue on a joint space") + z_positive, z_negative = eigenvalue_split(dimension, trace_z) + expect(z_positive > 0 and z_negative > 0, "Z_508 misses an eigenvalue on a joint space") + pieces = four_way(dimension, trace_x, trace_z, trace_xz) + expect(all(value > 0 for value in pieces.values()), "a sector intersection is empty") + expect( + pieces[(1, 0)] + pieces[(1, 1)] == positive, + "the +1 space of X_3 is not the sum of its Z sectors", + ) + for key, value in pieces.items(): + sector_total[key] += value + x_positive += positive + if chi == 0 and (eps, delta) == (1, 1): + headline = (dimension, trace_x, positive, negative, pieces) + expect(sum(dimensions) == 4096, "characters do not cover the block") + expect(sector_total == {(1, 0): 1024, (1, 1): 1024, (-1, 0): 1024, (-1, 1): 1024}, + "sector intersections do not rebuild the four 1024-dimensional sectors") + expect(x_positive == 2048, "the +1 space of X_3 is not half the block") + expect(headline is not None, "the trivial joint space was not reached") + dimension, trace_x, positive, negative, pieces = headline + expect(dimension == 216 and trace_x == -48, "the trivial ++ witness moved") + expect(positive == 84 and negative == 132, "X_3 does not split 216 as 84+132") + expect( + pieces == {(1, 0): 42, (1, 1): 42, (-1, 0): 66, (-1, 1): 66}, + "the four sector intersections of the 216-space changed", + ) + + # X_3 and Z_508 are not signed permutations S tensor U, because U fixes 0. + expect(apply_map(identity["T"], 0) == 0, "the identity label map moves 0") + expect(SHIFT != 0, "the translation has a fixed address at 0") + expect(dot(CHARACTER, 0) == 0 and dot(CHARACTER, 4) == 1, "Z_508 does not separate addresses 0 and 4") + + # Rejection controls. Each one must fire; a silent pass is a failure. + controls = 0 + moved = False + for address in range(512): + if apply_map(u["T"], address ^ 1) != (apply_map(u["T"], address) ^ 1): + moved = True + break + expect(moved, "translation by 1 commuted with u") + controls += 1 + expect( + any(not commutes_with_character(port, 1) for port in ports), + "character 1 commuted with every port operator", + ) + controls += 1 + partial = sign_group[:-1] + partial_trace = sum(element["trace"] for element in partial) + expect( + partial_trace % len(partial) != 0 or partial_trace // len(partial) != 864, + "dropping a sign still reproduced the trivial dimension", + ) + controls += 1 + zero_shift = joint_trace("I", 0, 1, 1) + expect(zero_shift == 216 and zero_shift != trace_x, "the identity trace collapsed onto the X_3 trace") + controls += 1 + expect(build((1, 0, 2, 3, 4, 5, 6, 7), 0) is None, "a coordinate transposition was accepted") + controls += 1 + expect(controls == 5, "a rejection control was not reached") + + print("PASS_C3_PAYLOAD_SECTOR3_SPLIT") + print("trivial ++ dimension", dimension) + print("X_3 trace", trace_x) + print("X_3 split", positive, negative) + print("Z_508 split", dimension // 2, dimension // 2) + print( + "sector intersections", + pieces[(1, 0)], + pieces[(1, 1)], + pieces[(-1, 0)], + pieces[(-1, 1)], + ) + print("controls", controls) + + +if __name__ == "__main__": + main()