From f9af520c844d23ffb9936ff4402533983aebbb30 Mon Sep 17 00:00:00 2001 From: Cursor Agent Date: Tue, 10 Nov 2026 10:34:53 +0000 Subject: [PATCH] Record the characteristic polynomial of the c=3 X_3=+1 subspace The trivial (+1,+1) joint space of the explicit pair has an explicit 84-dimensional X_3=+1 basis. The monic characteristic polynomial of A_1 on that subspace has degree 84, and its minimal polynomial has degree 25. The selected kappa is unchanged. Prepared by unpaidmoon with substantial Cursor Grok assistance. Co-authored-by: unpaidmoon --- research/c3-x3-plus-charpoly/PROOF.md | 212 ++++ research/c3-x3-plus-charpoly/README.md | 139 +++ research/c3-x3-plus-charpoly/SOURCES.json | 30 + research/c3-x3-plus-charpoly/TASK.json | 117 ++ research/c3-x3-plus-charpoly/VERIFY.json | 33 + .../c3-x3-plus-charpoly/evidence/basis.json | 1 + .../c3-x3-plus-charpoly/evidence/matrix.json | 1 + research/c3-x3-plus-charpoly/verify.py | 1038 +++++++++++++++++ 8 files changed, 1571 insertions(+) create mode 100644 research/c3-x3-plus-charpoly/PROOF.md create mode 100644 research/c3-x3-plus-charpoly/README.md create mode 100644 research/c3-x3-plus-charpoly/SOURCES.json create mode 100644 research/c3-x3-plus-charpoly/TASK.json create mode 100644 research/c3-x3-plus-charpoly/VERIFY.json create mode 100644 research/c3-x3-plus-charpoly/evidence/basis.json create mode 100644 research/c3-x3-plus-charpoly/evidence/matrix.json create mode 100644 research/c3-x3-plus-charpoly/verify.py diff --git a/research/c3-x3-plus-charpoly/PROOF.md b/research/c3-x3-plus-charpoly/PROOF.md new file mode 100644 index 0000000000..272a4a158c --- /dev/null +++ b/research/c3-x3-plus-charpoly/PROOF.md @@ -0,0 +1,212 @@ +# Characteristic polynomial of the 84-dimensional X_3=+1 subspace + +This is a finite exact computation for one invariant subspace of Bell block +`c=3` of the historical one-slot doubled centre operator. It is not a new +minimal polynomial of the full operator, not a change of the selected +conditional kappa, and not a census of payload involutions outside the named +pair. + +The claim is a **proof**. The coordinate set has 4096 elements. The basis +below classifies every coordinate. The characteristic polynomial is an exact +determinant, the factorisation is checked by multiplication and an exhaustive +integer search, and the minimal polynomial is identified by an exact +annihilator. None of these steps is a stopped search. + +## Operator + +The input is the 8-by-112 query in `INTERFACE.json`, SHA256 +`5c6c51fbffc07a683e922f17532fd90262ae9e23cc3560a696002073dd234ef3`. +Its columns lie in `{-1,0,1}^8`, each has weight 4, the 112 port labels are +distinct odd-weight vectors in `F_2^9`, and `R R^T = 56 I_8`. + +On `Q^8 ⊗ Q[F_2^9]`, of dimension 4096, the `c=3` block and its integer form are + +```text +A_1 = (1/4) sum_q r_q r_q^T ⊗ P_q(3), +B = 4 A_1 = sum_q r_q r_q^T ⊗ P_q(3). +``` + +`P_q(3)` sends `e_a` to `e_{a+q}` when the `F_2` dot product `q·3` equals 1, +and to `(-1)^{q·a} e_a` otherwise. Basis index `i*512+a` means query +coordinate `i` and address `a`. + +Krzysztof Wojt's `research/exact-one-slot-gram/` gives the minimal polynomial +of the full one-slot operator, of degree 881. This note does not replay that +certificate. It uses the two published `c=3`, `s=+1` sector coefficient lists +only for the divisibility comparison below. Those lists are the degree-126 +polynomials for `(t,s) = (0,+1)` and `(1,+1)`. + +## The subspace + +`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 explicit pair from the c=3 sign-character certificate is + +| name | permutation | minus signs | +|---|---|---| +| `u` | `(0 2)(4 6)` | coordinates 0 and 2 | +| `v` | `(0 4)(2 6)` | coordinates 0 and 4 | + +Each element is rebuilt from the query as a signed coordinate permutation. +All 64 products are symmetries, they fix sector 3, and `u` and `v` are +commuting involutions. The payload involution `X_3` translates every address +by 3 and fixes the eight coordinates. It commutes with all 64 products and is +not equal to any of them. `Z_508` is the diagonal character of `3 xor 511`. + +Let `V` be the set of vectors fixed by every element of `H`, by `u`, and by +`v`, and fixed by `X_3`. This is the `X_3 = +1` subspace of the trivial +`(+1,+1)` joint space. The same equations without `X_3` have an explicit +basis of dimension 216. The trace of `X_3` on that 216-space, computed as the +average of the address-and-coordinate traces of `X_3 g` over the 64 group +elements, is `-48`. The projector onto `V`, averaged over the order-128 group +generated by `H`, `u`, `v`, and `X_3`, has trace 84. The explicit basis of the +same equations also has dimension 84, and the `X_3 = -1` equations have +dimension 132. Imposing `v = -1` instead of `v = +1`, with `X_3 = +1`, +produces dimension 116, so the basis is the `(+1,+1)` joint eigenvalue rather +than one of the other three. + +The basis is canonical. The equations `v_{ρ(j)} = σ_j v_j`, as `ρ` runs +through the 64 group elements and through `X_3`, partition the coordinates +that are not forced to zero. In each component the representative is the +least index, its coefficient is `+1`, and every other coefficient is the +unique sign forced by the equations. Components are ordered by increasing +representative. The basis is stored in `evidence/basis.json`. Support sizes +are exactly 8, 32, and 64. + +`Z_508` preserves `V` and splits it into dimensions 42 and 42, for eigenvalues +`+1` (`t=0`) and `-1` (`t=1`). + +## The matrix + +`B` preserves `V`. Two independent expansions, one by the 4096 columns and +one by the 112 ports, agree on every basis vector of `V` and of both +`Z_508` eigenspaces. In the ordered basis, the matrix `M` of `B` has integer +entries in `-28..28`. It is stored in `evidence/matrix.json`. If `size_r` is +the support of the `r`-th basis vector, then `size_r M_{r s} = size_s M_{s r}`. + +The trace of `M` is 0. The same trace is the average of `tr(B g)` over the +order-128 group, so the matrix trace agrees with the trace formula. The two +`Z_508` blocks have traces 168 and -168. + +The matrix of `A_1` on `V` is `M/4`. + +## Characteristic polynomial + +Let `chi_B(x) = det(x I - M)` and `chi_{A_1}(x) = det(x I - M/4)`. Then +`chi_{A_1}(x) = 4^{-84} chi_B(4x)`, and both polynomials are monic of degree +84 in `Z[x]`. The SHA256 hex digests of the JSON arrays of ascending +coefficients are + +```text +chi_A c4bcbd4e52f92d13f3ad451d92c9d22256e7725e4be24ee203bea1c96c129648 +chi_B 185b51cfd084f95c1dbd814b0b211ce4ab35b2d59604d7795715d65a0a4e5e65 +``` + +The irreducible factorisation over `Z` is + +```text +chi_{A_1}(x) = + x^16 + * (x - 14) + * (x - 12) + * (x - 4)^6 + * (x - 2)^14 + * (x + 2)^14 + * (x + 4)^6 + * (x + 12) + * (x + 14) + * (x^4 - 16x^2 - 8x + 16)^2 + * (x^4 - 16x^2 + 8x + 16)^2 + * (x^4 - 12x^3 + 20x^2 + 32x - 32) + * (x^4 + 12x^3 + 20x^2 - 32x - 32). +``` + +The two `Z_508` blocks have + +```text +t = 0: + x^8 (x - 14) (x + 12) (x - 4)^6 (x + 2)^6 (x - 2)^8 + * (x^4 - 12x^3 + 20x^2 + 32x - 32) + * (x^4 - 16x^2 + 8x + 16)^2 + +t = 1: + x^8 (x - 12) (x + 14) (x - 2)^6 (x + 4)^6 (x + 2)^8 + * (x^4 + 12x^3 + 20x^2 - 32x - 32) + * (x^4 - 16x^2 - 8x + 16)^2. +``` + +Their product is `chi_{A_1}`. Every irreducible factor of `chi_B` divides at +least one of the two published degree-126 minimal polynomials of the `c=3`, +`s=+1` sectors in `research/exact-one-slot-gram/CERTIFICATE.json`. The hits +are recorded by `SECTOR_HITS` in `verify.py`. Those two polynomials are among +the sector polynomials whose monic LCM is the degree-881 minimal polynomial +of `B` in that certificate. This comparison reads coefficients. It does not +recompute the LCM and it does not replay the degree-881 certificate. + +The degree-4 factors are irreducible over `Z`: the rational-root theorem +gives no root, and an exhaustive search of integer pairs `(b,d)` with +`bd` equal to the constant term finds no quadratic factorisation. The search +does reject `(x^2+1)^2`, so the negative test is not vacuous. Linear factors +are irreducible because they have degree 1. + +## Minimal polynomial and rational eigenvalues + +Every irreducible factor of a characteristic polynomial divides the minimal +polynomial. The square-free product of the factors above has degree 25. The +corresponding monic integer polynomial in `B`, obtained by sending each +factor `f(x)` of degree `d` to `4^d f(y/4)`, evaluates to the zero matrix on +`M`. Therefore that degree-25 polynomial annihilates `A_1` on `V`, and it is +the minimal polynomial of `A_1` on `V`. The same argument on each 42-by-42 +block shows that the square-free part of that block's characteristic +polynomial, of degree 14, is the minimal polynomial of the block. + +On this matrix, each rational eigenvalue of `A_1` has geometric multiplicity +equal to its algebraic multiplicity. For eigenvalue `λ`, the verifier +exhibits `m` integer vectors in the kernel of `M - 4λ I`, checks that each +image is zero, and checks that their free coordinates form a diagonal +submatrix, so they are independent. The algebraic multiplicity is an upper +bound, so the geometric multiplicity is exactly `m`: + +| eigenvalue of `A_1` | multiplicity | +|---:|---:| +| 0 | 16 | +| 2 and -2 | 14 each | +| 4 and -4 | 6 each | +| 12 and -12 | 1 each | +| 14 and -14 | 1 each | + +These nine eigenvalues account for 60 of the 84 dimensions. The remaining 24 +dimensions belong to the four quartic factors. Because each repeated quartic +occurs to the first power in the minimal polynomial and to the second power +in the characteristic polynomial, its primary part is two companion blocks of +degree 4. Each simple quartic is one companion block of degree 4. Each +rational eigenvalue is a diagonal of 1-by-1 blocks. This is the rational +canonical form of `A_1` on `V`. The package does not list cyclic generators. + +## Verification + +`verify.py` uses CPython 3.12 and the standard library. It rebuilds the +matrix from the query, computes each characteristic polynomial by the +Hessenberg recurrence modulo primes whose product exceeds twice the +Gershgorin binomial coefficient bound, and lifts by the Chinese remainder +theorem. Determinants of `tI-M` at `t=0,1,2,3,5` agree with that polynomial +modulo the first prime. + +Rejection controls refuse the coordinate transposition `(0 1)`, the `c=1` +block operator on this subspace, translation by 1 in place of `X_3`, a +flipped group sign that still claims dimension 84, a one-entry change of `M` +that preserves the polynomial modulo `1000003`, a missing factor, and a +one-coordinate sign error in a linked basis vector. + +Not run: Lean, Docker, the degree-881 coefficient replay, and the selected +cold replay. Selected-baseline orientation returned +`PASS_RESEARCH_BASELINE_BINDINGS_ONLY` for kappa `781451/250000000`. + +## What this does not say + +An 84-dimensional invariant subspace does not replace the degree-881 minimal +polynomial. The selected conditional kappa stays `781451/250000000`. The +polynomial is for this query, this sign group, this explicit pair, and the +eigenvalue `X_3 = +1`. It does not compute the 132-dimensional complement, and +it does not move the odd signs on the pair. A factor that divides a published +sector polynomial is not a new factor of the degree-881 polynomial. diff --git a/research/c3-x3-plus-charpoly/README.md b/research/c3-x3-plus-charpoly/README.md new file mode 100644 index 0000000000..cd12a07279 --- /dev/null +++ b/research/c3-x3-plus-charpoly/README.md @@ -0,0 +1,139 @@ +# Characteristic polynomial of the 84-dimensional X_3=+1 subspace + +Prepared by unpaidmoon with substantial Cursor Grok assistance. Apache-2.0. + +For the historical 8-by-112 centre query, the trivial `(+1,+1)` joint space of +the explicit c=3 pair has dimension 216. The payload involution `X_3` cuts it +into dimensions 84 and 132. On the 84-dimensional eigenvalue-`+1` subspace, +the monic characteristic polynomial of `A_1` in characteristic zero is the +explicit degree-84 polynomial in [PROOF.md](PROOF.md). Its minimal polynomial +has degree 25 and is the product of the distinct irreducible factors. + +No new kappa. The selected conditional kappa stays `781451/250000000`. + +## Result + +Write `B = 4 A_1` on the `c=3` block. On this subspace, +`chi_{A_1}(x) = 4^{-84} chi_B(4x)`, and both polynomials lie in `Z[x]`. +The irreducible factorisation is + +```text +x^16 (x-14) (x-12) (x-4)^6 (x-2)^14 (x+2)^14 (x+4)^6 (x+12) (x+14) + * (x^4 - 16x^2 - 8x + 16)^2 + * (x^4 - 16x^2 + 8x + 16)^2 + * (x^4 - 12x^3 + 20x^2 + 32x - 32) + * (x^4 + 12x^3 + 20x^2 - 32x - 32) +``` + +Ascending coefficient SHA256 values are + +```text +chi_A c4bcbd4e52f92d13f3ad451d92c9d22256e7725e4be24ee203bea1c96c129648 +chi_B 185b51cfd084f95c1dbd814b0b211ce4ab35b2d59604d7795715d65a0a4e5e65 +``` + +The basis is the least-index signed orbit basis of the joint equations for +`H`, `u`, `v`, and `X_3 = +1`, pinned in +[evidence/basis.json](evidence/basis.json). The integer matrix of `B` in that +basis is pinned in [evidence/matrix.json](evidence/matrix.json). Its entries +lie in `-28..28`, and its trace is 0. + +`Z_508` splits the same 84-space into dimensions 42 and 42. The +characteristic polynomial of the `t=0` block is + +```text +x^8 (x-14) (x+12) (x-4)^6 (x+2)^6 (x-2)^8 + * (x^4 - 12x^3 + 20x^2 + 32x - 32) + * (x^4 - 16x^2 + 8x + 16)^2 +``` + +and the `t=1` block is + +```text +x^8 (x-12) (x+14) (x-2)^6 (x+4)^6 (x+2)^8 + * (x^4 + 12x^3 + 20x^2 - 32x - 32) + * (x^4 - 16x^2 - 8x + 16)^2. +``` + +Every irreducible factor of `chi_B` divides a published `c=3`, `s=+1` sector +minimal polynomial from `research/exact-one-slot-gram/CERTIFICATE.json`. +Those two degree-126 polynomials are part of the certificate whose monic LCM +is the degree-881 minimal polynomial of `B`. The comparison reads +coefficients. It does not replay the degree-881 certificate. + +Each rational eigenvalue of `A_1` on this matrix has geometric multiplicity +equal to its algebraic multiplicity: 16 for 0, 14 for each of `±2`, 6 for +each of `±4`, and 1 for each of `±12` and `±14`. + +## Scope + +Catalogue card `formal-interface-lemma` asks for a formal interface binding. +The live question is open question 1 of +[PR #7020](https://github.com/CrocSwap/integer-mult-bounds/pull/7020), +recorded in discussion comment +[19514155](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19514155). +That pull request proves the trace split and states that the trace formula +does not list a vector. This package builds the basis and computes the +polynomial. + +It does not redo the payload-involution split, the signed-permutation +classification, the 16-dimensional or 12-dimensional c=3 polynomials, or the +216-dimensional c=1 polynomial. It does not change the odd signs on the pair. + +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-x3-plus-charpoly/verify.py +python3 -B -O research/c3-x3-plus-charpoly/verify.py +python3 -B scripts/research_package.py --package research/c3-x3-plus-charpoly --check-only +``` + +The marker is `PASS_C3_X3_PLUS_CHARPOLY`. Acceptance uses explicit checks, so +`-O` does not skip a theorem or a rejection control. On the measured host one +run takes about five seconds. No Lean, Docker, degree-881 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; 339 open PRs, pagination complete, fetched +2026-11-10T10:24:45Z; 7013 discussion records, pagination complete, fetched +2026-11-10T10:25:50Z. Closed PRs were searched through local READMEs, task +metadata and the ledger only. + +The phrase `84-dimensional` matches open PR #7020, which records the +dimension and says the characteristic polynomial is uncomputed, and open PR +#7009, whose `84` is a c=1 character dimension. No open PR body gives this +polynomial. This search is not a novelty certificate. + +## Open next questions + +The structured list is in [TASK.json](TASK.json). + +- The characteristic polynomial of the 132-dimensional `X_3 = -1` complement, + inside the same trivial `(+1,+1)` joint space, is still uncomputed. The + same basis routine applies with the opposite eigenvalue. The published + comparison for that half is the pair of degree-88 sector polynomials. +- One 66-dimensional intersection of that complement with a single eigenvalue + of `Z_508` is the smaller block. Its polynomial is not determined by the + degree-84 factorisation above. + +## Credit + +JoyboyBrian's handoff recorded the sign-character dimensions. The explicit +pair and the signed-permutation boundary are upstream PR #6965. The trace +`-48`, the dimensions 84 and 132, and the open polynomial question are +upstream PR #7020. 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_3` and `Z_508` and is the degree-881 +annihilator and the sector coefficient list used for the divisibility +comparison. The doubled representation comes from PR1719. The 216-dimensional +c=1 polynomial in `research/a1-joint-216-charpoly/` is a different block; its +Hessenberg recurrence is the model for the determinant. New work is +Apache-2.0. diff --git a/research/c3-x3-plus-charpoly/SOURCES.json b/research/c3-x3-plus-charpoly/SOURCES.json new file mode 100644 index 0000000000..da775281b1 --- /dev/null +++ b/research/c3-x3-plus-charpoly/SOURCES.json @@ -0,0 +1,30 @@ +{ + "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/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/CERTIFICATE.json", + "usage": "input", + "git_blob": "96c3dc7a8bca73fb35b8a9ec49a17856308a029d", + "sha256": "29e0b0d86c7fd8929ad36d9de48c2b8b55500491576dc5ac1d0b1ff076d27483" + } + ] +} diff --git a/research/c3-x3-plus-charpoly/TASK.json b/research/c3-x3-plus-charpoly/TASK.json new file mode 100644 index 0000000000..7296ca1813 --- /dev/null +++ b/research/c3-x3-plus-charpoly/TASK.json @@ -0,0 +1,117 @@ +{ + "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": "Characteristic polynomial, over Q, of A_1 on the 84-dimensional X_3=+1 subspace of the trivial (+1,+1) joint space of the explicit c=3 pair.", + "scope_change_reason": "The catalogue card asks for a formal caller or certificate binding. Open question 1 of PR #7020 asks for the characteristic polynomial of the 84-dimensional X_3=+1 subspace and names a basis of the joint equations as the first step. This package answers that polynomial. It does not add a Lean binding.", + "bottleneck_link": "Scoped side result on the historical centre Gram. The selected conditional kappa remains 781451/250000000. The one-slot minimal polynomial remains degree 881 in research/exact-one-slot-gram/; this polynomial locates one invariant subspace inside that certificate and does not replace it.", + "budget_minutes": 60, + "stop_rule": "Stop once one explicit 84-dimensional basis and the characteristic polynomial of A_1 on it are recomputed from the pinned query, with the matrix pinned and the factorisation checked. Do not rerun the degree-881 certificate or change the odd signs on the pair.", + "outcome": "completed", + "evidence": "verify.py rebuilds the basis and the 84-by-84 integer matrix of B=4 A_1. Marker PASS_C3_X3_PLUS_CHARPOLY. chi_A SHA256 c4bcbd4e52f92d13f3ad451d92c9d22256e7725e4be24ee203bea1c96c129648. The degree-25 square-free product annihilates the matrix. Selected baseline returned PASS_RESEARCH_BASELINE_BINDINGS_ONLY.", + "author": "unpaidmoon", + "ai_assistance": "Prepared by unpaidmoon with substantial Cursor Grok assistance. The assistant derived the basis and checked the polynomial. This is not an independent human or proof-kernel review.", + "open_questions": [ + { + "question": "What is the characteristic polynomial of the 132-dimensional X_3=-1 complement of this same trivial (+1,+1) joint space?", + "why_it_matters": "PR #7020 splits the 216-space into dimensions 84 and 132. The polynomial computed here is only the eigenvalue-+1 half. The complement would meet the two published degree-88 sector polynomials.", + "first_step": "Impose X_3 eigenvalue -1 on the same joint equations for H, u and v, and repeat the signed orbit-sum matrix of B.", + "blocked_by": "The trace formula gives dimension 132 without listing a vector. This package stops at eigenvalue +1." + }, + { + "question": "What is the characteristic polynomial of one 66-dimensional intersection of that X_3=-1 complement with a single eigenvalue of Z_508?", + "why_it_matters": "The 132-space is the sum of two 66-dimensional sector intersections. One 66-dimensional polynomial would sit inside a single degree-88 sector polynomial.", + "first_step": "Add the diagonal character Z_508 at one eigenvalue to the X_3=-1 equations and compute the 66-by-66 matrix of B.", + "blocked_by": "This package does not build the X_3=-1 basis, so it has no coordinates on which to impose Z_508." + } + ], + "environment": { + "python": "3.12.3", + "platform": "linux" + }, + "overlap": { + "checked_at": "2026-11-10T10:25:50Z", + "canonical_main": "17469fff78c22941280f04d39dc5a1faee09c840", + "open_pr_records": 339, + "discussion_records": 7013, + "remote_pagination_complete": true, + "local_records": 10178, + "head_records": 10178, + "local_coverage_complete": true, + "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19514155", + "limits": "Closed PRs were searched through local READMEs, TASK metadata and the ledger. No code diffs or unpublished work. The phrase 84-dimensional matches PR #7020, which leaves this polynomial uncomputed, and does not match another open computation of it." + } +} diff --git a/research/c3-x3-plus-charpoly/VERIFY.json b/research/c3-x3-plus-charpoly/VERIFY.json new file mode 100644 index 0000000000..7a4e5c0504 --- /dev/null +++ b/research/c3-x3-plus-charpoly/VERIFY.json @@ -0,0 +1,33 @@ +{ + "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", + "research/exact-one-slot-gram/CERTIFICATE.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "-W", + "error", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Rebuild the pinned query, the 84-dimensional X_3=+1 basis and matrix, and the characteristic polynomial; check the Z_508 split, the factorisation, irreducibility, sector divisibility, the degree-25 annihilator, the rational geometric multiplicities, and the rejection controls." + }, + { + "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 theorem or a rejection control." + } + ] +} diff --git a/research/c3-x3-plus-charpoly/evidence/basis.json b/research/c3-x3-plus-charpoly/evidence/basis.json new file mode 100644 index 0000000000..bed0fbb43f --- /dev/null +++ b/research/c3-x3-plus-charpoly/evidence/basis.json @@ -0,0 +1 @@ +{"index":"coordinate*512+address","eigenvalues":{"H":1,"u":1,"v":1,"X_3":1},"roots":[0,1,4,5,8,9,12,13,16,17,20,21,24,25,28,29,32,36,40,41,44,45,48,49,52,53,57,61,64,68,72,76,81,85,89,93,97,101,120,124,128,129,132,133,136,137,140,141,144,145,148,149,152,153,156,157,160,164,168,172,177,181,185,189,192,196,217,221,384,388,409,413,425,429,432,436,456,460,465,469,481,485,504,508],"vectors":[[[0,1],[3,1],[1024,-1],[1027,-1],[2048,-1],[2051,-1],[3072,-1],[3075,-1]],[[1,1],[2,1],[121,1],[122,1],[433,1],[434,1],[457,1],[458,1],[1025,-1],[1026,-1],[1145,-1],[1146,-1],[1457,-1],[1458,-1],[1481,-1],[1482,-1],[2049,-1],[2050,-1],[2169,-1],[2170,-1],[2481,-1],[2482,-1],[2505,-1],[2506,-1],[3073,-1],[3074,-1],[3193,-1],[3194,-1],[3505,-1],[3506,-1],[3529,-1],[3530,-1]],[[4,1],[7,1],[1028,-1],[1031,-1],[2052,-1],[2055,-1],[3076,-1],[3079,-1]],[[5,1],[6,1],[125,1],[126,1],[437,1],[438,1],[461,1],[462,1],[1029,-1],[1030,-1],[1149,-1],[1150,-1],[1461,-1],[1462,-1],[1485,-1],[1486,-1],[2053,-1],[2054,-1],[2173,-1],[2174,-1],[2485,-1],[2486,-1],[2509,-1],[2510,-1],[3077,-1],[3078,-1],[3197,-1],[3198,-1],[3509,-1],[3510,-1],[3533,-1],[3534,-1]],[[8,1],[11,1],[56,1],[59,1],[448,1],[451,1],[496,1],[499,1],[1032,-1],[1035,-1],[1080,-1],[1083,-1],[1472,-1],[1475,-1],[1520,-1],[1523,-1],[2112,-1],[2115,-1],[2160,-1],[2163,-1],[2440,-1],[2443,-1],[2488,-1],[2491,-1],[3136,-1],[3139,-1],[3184,-1],[3187,-1],[3464,-1],[3467,-1],[3512,-1],[3515,-1]],[[9,1],[10,1],[65,1],[66,1],[441,1],[442,1],[497,1],[498,1],[1033,-1],[1034,-1],[1089,-1],[1090,-1],[1465,-1],[1466,-1],[1521,-1],[1522,-1],[2057,-1],[2058,-1],[2113,-1],[2114,-1],[2489,-1],[2490,-1],[2545,-1],[2546,-1],[3081,-1],[3082,-1],[3137,-1],[3138,-1],[3513,-1],[3514,-1],[3569,-1],[3570,-1]],[[12,1],[15,1],[60,1],[63,1],[452,1],[455,1],[500,1],[503,1],[1036,-1],[1039,-1],[1084,-1],[1087,-1],[1476,-1],[1479,-1],[1524,-1],[1527,-1],[2116,-1],[2119,-1],[2164,-1],[2167,-1],[2444,-1],[2447,-1],[2492,-1],[2495,-1],[3140,-1],[3143,-1],[3188,-1],[3191,-1],[3468,-1],[3471,-1],[3516,-1],[3519,-1]],[[13,1],[14,1],[69,1],[70,1],[445,1],[446,1],[501,1],[502,1],[1037,-1],[1038,-1],[1093,-1],[1094,-1],[1469,-1],[1470,-1],[1525,-1],[1526,-1],[2061,-1],[2062,-1],[2117,-1],[2118,-1],[2493,-1],[2494,-1],[2549,-1],[2550,-1],[3085,-1],[3086,-1],[3141,-1],[3142,-1],[3517,-1],[3518,-1],[3573,-1],[3574,-1]],[[16,1],[19,1],[88,1],[91,1],[416,1],[419,1],[488,1],[491,1],[1056,-1],[1059,-1],[1128,-1],[1131,-1],[1424,-1],[1427,-1],[1496,-1],[1499,-1],[2080,-1],[2083,-1],[2152,-1],[2155,-1],[2448,-1],[2451,-1],[2520,-1],[2523,-1],[3088,-1],[3091,-1],[3160,-1],[3163,-1],[3488,-1],[3491,-1],[3560,-1],[3563,-1]],[[17,1],[18,1],[33,1],[34,1],[473,1],[474,1],[489,1],[490,1],[1041,-1],[1042,-1],[1057,-1],[1058,-1],[1497,-1],[1498,-1],[1513,-1],[1514,-1],[2065,-1],[2066,-1],[2081,-1],[2082,-1],[2521,-1],[2522,-1],[2537,-1],[2538,-1],[3089,-1],[3090,-1],[3105,-1],[3106,-1],[3545,-1],[3546,-1],[3561,-1],[3562,-1]],[[20,1],[23,1],[92,1],[95,1],[420,1],[423,1],[492,1],[495,1],[1060,-1],[1063,-1],[1132,-1],[1135,-1],[1428,-1],[1431,-1],[1500,-1],[1503,-1],[2084,-1],[2087,-1],[2156,-1],[2159,-1],[2452,-1],[2455,-1],[2524,-1],[2527,-1],[3092,-1],[3095,-1],[3164,-1],[3167,-1],[3492,-1],[3495,-1],[3564,-1],[3567,-1]],[[21,1],[22,1],[37,1],[38,1],[477,1],[478,1],[493,1],[494,1],[1045,-1],[1046,-1],[1061,-1],[1062,-1],[1501,-1],[1502,-1],[1517,-1],[1518,-1],[2069,-1],[2070,-1],[2085,-1],[2086,-1],[2525,-1],[2526,-1],[2541,-1],[2542,-1],[3093,-1],[3094,-1],[3109,-1],[3110,-1],[3549,-1],[3550,-1],[3565,-1],[3566,-1]],[[24,1],[27,1],[96,1],[99,1],[424,1],[427,1],[464,1],[467,1],[1064,-1],[1067,-1],[1104,-1],[1107,-1],[1432,-1],[1435,-1],[1504,-1],[1507,-1],[2072,-1],[2075,-1],[2144,-1],[2147,-1],[2472,-1],[2475,-1],[2512,-1],[2515,-1],[3112,-1],[3115,-1],[3152,-1],[3155,-1],[3480,-1],[3483,-1],[3552,-1],[3555,-1]],[[25,1],[26,1],[1065,-1],[1066,-1],[2145,-1],[2146,-1],[3153,-1],[3154,-1]],[[28,1],[31,1],[100,1],[103,1],[428,1],[431,1],[468,1],[471,1],[1068,-1],[1071,-1],[1108,-1],[1111,-1],[1436,-1],[1439,-1],[1508,-1],[1511,-1],[2076,-1],[2079,-1],[2148,-1],[2151,-1],[2476,-1],[2479,-1],[2516,-1],[2519,-1],[3116,-1],[3119,-1],[3156,-1],[3159,-1],[3484,-1],[3487,-1],[3556,-1],[3559,-1]],[[29,1],[30,1],[1069,-1],[1070,-1],[2149,-1],[2150,-1],[3157,-1],[3158,-1]],[[32,1],[35,1],[104,1],[107,1],[400,1],[403,1],[472,1],[475,1],[1040,-1],[1043,-1],[1112,-1],[1115,-1],[1440,-1],[1443,-1],[1512,-1],[1515,-1],[2064,-1],[2067,-1],[2136,-1],[2139,-1],[2464,-1],[2467,-1],[2536,-1],[2539,-1],[3104,-1],[3107,-1],[3176,-1],[3179,-1],[3472,-1],[3475,-1],[3544,-1],[3547,-1]],[[36,1],[39,1],[108,1],[111,1],[404,1],[407,1],[476,1],[479,1],[1044,-1],[1047,-1],[1116,-1],[1119,-1],[1444,-1],[1447,-1],[1516,-1],[1519,-1],[2068,-1],[2071,-1],[2140,-1],[2143,-1],[2468,-1],[2471,-1],[2540,-1],[2543,-1],[3108,-1],[3111,-1],[3180,-1],[3183,-1],[3476,-1],[3479,-1],[3548,-1],[3551,-1]],[[40,1],[43,1],[80,1],[83,1],[408,1],[411,1],[480,1],[483,1],[1048,-1],[1051,-1],[1120,-1],[1123,-1],[1448,-1],[1451,-1],[1488,-1],[1491,-1],[2088,-1],[2091,-1],[2128,-1],[2131,-1],[2456,-1],[2459,-1],[2528,-1],[2531,-1],[3096,-1],[3099,-1],[3168,-1],[3171,-1],[3496,-1],[3499,-1],[3536,-1],[3539,-1]],[[41,1],[42,1],[1049,-1],[1050,-1],[2129,-1],[2130,-1],[3169,-1],[3170,-1]],[[44,1],[47,1],[84,1],[87,1],[412,1],[415,1],[484,1],[487,1],[1052,-1],[1055,-1],[1124,-1],[1127,-1],[1452,-1],[1455,-1],[1492,-1],[1495,-1],[2092,-1],[2095,-1],[2132,-1],[2135,-1],[2460,-1],[2463,-1],[2532,-1],[2535,-1],[3100,-1],[3103,-1],[3172,-1],[3175,-1],[3500,-1],[3503,-1],[3540,-1],[3543,-1]],[[45,1],[46,1],[1053,-1],[1054,-1],[2133,-1],[2134,-1],[3173,-1],[3174,-1]],[[48,1],[51,1],[1072,-1],[1075,-1],[2096,-1],[2099,-1],[3120,-1],[3123,-1]],[[49,1],[50,1],[73,1],[74,1],[385,1],[386,1],[505,1],[506,1],[1073,-1],[1074,-1],[1097,-1],[1098,-1],[1409,-1],[1410,-1],[1529,-1],[1530,-1],[2097,-1],[2098,-1],[2121,-1],[2122,-1],[2433,-1],[2434,-1],[2553,-1],[2554,-1],[3121,-1],[3122,-1],[3145,-1],[3146,-1],[3457,-1],[3458,-1],[3577,-1],[3578,-1]],[[52,1],[55,1],[1076,-1],[1079,-1],[2100,-1],[2103,-1],[3124,-1],[3127,-1]],[[53,1],[54,1],[77,1],[78,1],[389,1],[390,1],[509,1],[510,1],[1077,-1],[1078,-1],[1101,-1],[1102,-1],[1413,-1],[1414,-1],[1533,-1],[1534,-1],[2101,-1],[2102,-1],[2125,-1],[2126,-1],[2437,-1],[2438,-1],[2557,-1],[2558,-1],[3125,-1],[3126,-1],[3149,-1],[3150,-1],[3461,-1],[3462,-1],[3581,-1],[3582,-1]],[[57,1],[58,1],[113,1],[114,1],[393,1],[394,1],[449,1],[450,1],[1081,-1],[1082,-1],[1137,-1],[1138,-1],[1417,-1],[1418,-1],[1473,-1],[1474,-1],[2105,-1],[2106,-1],[2161,-1],[2162,-1],[2441,-1],[2442,-1],[2497,-1],[2498,-1],[3129,-1],[3130,-1],[3185,-1],[3186,-1],[3465,-1],[3466,-1],[3521,-1],[3522,-1]],[[61,1],[62,1],[117,1],[118,1],[397,1],[398,1],[453,1],[454,1],[1085,-1],[1086,-1],[1141,-1],[1142,-1],[1421,-1],[1422,-1],[1477,-1],[1478,-1],[2109,-1],[2110,-1],[2165,-1],[2166,-1],[2445,-1],[2446,-1],[2501,-1],[2502,-1],[3133,-1],[3134,-1],[3189,-1],[3190,-1],[3469,-1],[3470,-1],[3525,-1],[3526,-1]],[[64,1],[67,1],[112,1],[115,1],[392,1],[395,1],[440,1],[443,1],[1088,-1],[1091,-1],[1136,-1],[1139,-1],[1416,-1],[1419,-1],[1464,-1],[1467,-1],[2056,-1],[2059,-1],[2104,-1],[2107,-1],[2496,-1],[2499,-1],[2544,-1],[2547,-1],[3080,-1],[3083,-1],[3128,-1],[3131,-1],[3520,-1],[3523,-1],[3568,-1],[3571,-1]],[[68,1],[71,1],[116,1],[119,1],[396,1],[399,1],[444,1],[447,1],[1092,-1],[1095,-1],[1140,-1],[1143,-1],[1420,-1],[1423,-1],[1468,-1],[1471,-1],[2060,-1],[2063,-1],[2108,-1],[2111,-1],[2500,-1],[2503,-1],[2548,-1],[2551,-1],[3084,-1],[3087,-1],[3132,-1],[3135,-1],[3524,-1],[3527,-1],[3572,-1],[3575,-1]],[[72,1],[75,1],[1096,-1],[1099,-1],[2120,-1],[2123,-1],[3144,-1],[3147,-1]],[[76,1],[79,1],[1100,-1],[1103,-1],[2124,-1],[2127,-1],[3148,-1],[3151,-1]],[[81,1],[82,1],[1121,-1],[1122,-1],[2089,-1],[2090,-1],[3097,-1],[3098,-1]],[[85,1],[86,1],[1125,-1],[1126,-1],[2093,-1],[2094,-1],[3101,-1],[3102,-1]],[[89,1],[90,1],[105,1],[106,1],[401,1],[402,1],[417,1],[418,1],[1113,-1],[1114,-1],[1129,-1],[1130,-1],[1425,-1],[1426,-1],[1441,-1],[1442,-1],[2137,-1],[2138,-1],[2153,-1],[2154,-1],[2449,-1],[2450,-1],[2465,-1],[2466,-1],[3161,-1],[3162,-1],[3177,-1],[3178,-1],[3473,-1],[3474,-1],[3489,-1],[3490,-1]],[[93,1],[94,1],[109,1],[110,1],[405,1],[406,1],[421,1],[422,1],[1117,-1],[1118,-1],[1133,-1],[1134,-1],[1429,-1],[1430,-1],[1445,-1],[1446,-1],[2141,-1],[2142,-1],[2157,-1],[2158,-1],[2453,-1],[2454,-1],[2469,-1],[2470,-1],[3165,-1],[3166,-1],[3181,-1],[3182,-1],[3477,-1],[3478,-1],[3493,-1],[3494,-1]],[[97,1],[98,1],[1105,-1],[1106,-1],[2073,-1],[2074,-1],[3113,-1],[3114,-1]],[[101,1],[102,1],[1109,-1],[1110,-1],[2077,-1],[2078,-1],[3117,-1],[3118,-1]],[[120,1],[123,1],[1144,-1],[1147,-1],[2168,-1],[2171,-1],[3192,-1],[3195,-1]],[[124,1],[127,1],[1148,-1],[1151,-1],[2172,-1],[2175,-1],[3196,-1],[3199,-1]],[[128,1],[131,1],[176,1],[179,1],[200,1],[203,1],[248,1],[251,1],[256,1],[259,1],[304,1],[307,1],[328,1],[331,1],[376,1],[379,1],[1152,-1],[1155,-1],[1200,-1],[1203,-1],[1224,-1],[1227,-1],[1272,-1],[1275,-1],[1280,-1],[1283,-1],[1328,-1],[1331,-1],[1352,-1],[1355,-1],[1400,-1],[1403,-1],[2176,-1],[2179,-1],[2224,-1],[2227,-1],[2248,-1],[2251,-1],[2296,-1],[2299,-1],[2304,-1],[2307,-1],[2352,-1],[2355,-1],[2376,-1],[2379,-1],[2424,-1],[2427,-1],[3200,-1],[3203,-1],[3248,-1],[3251,-1],[3272,-1],[3275,-1],[3320,-1],[3323,-1],[3328,-1],[3331,-1],[3376,-1],[3379,-1],[3400,-1],[3403,-1],[3448,-1],[3451,-1]],[[129,1],[130,1],[249,1],[250,1],[257,1],[258,1],[377,1],[378,1],[1153,-1],[1154,-1],[1273,-1],[1274,-1],[1281,-1],[1282,-1],[1401,-1],[1402,-1],[2177,-1],[2178,-1],[2297,-1],[2298,-1],[2305,-1],[2306,-1],[2425,-1],[2426,-1],[3201,-1],[3202,-1],[3321,-1],[3322,-1],[3329,-1],[3330,-1],[3449,-1],[3450,-1]],[[132,1],[135,1],[180,1],[183,1],[204,1],[207,1],[252,1],[255,1],[260,1],[263,1],[308,1],[311,1],[332,1],[335,1],[380,1],[383,1],[1156,-1],[1159,-1],[1204,-1],[1207,-1],[1228,-1],[1231,-1],[1276,-1],[1279,-1],[1284,-1],[1287,-1],[1332,-1],[1335,-1],[1356,-1],[1359,-1],[1404,-1],[1407,-1],[2180,-1],[2183,-1],[2228,-1],[2231,-1],[2252,-1],[2255,-1],[2300,-1],[2303,-1],[2308,-1],[2311,-1],[2356,-1],[2359,-1],[2380,-1],[2383,-1],[2428,-1],[2431,-1],[3204,-1],[3207,-1],[3252,-1],[3255,-1],[3276,-1],[3279,-1],[3324,-1],[3327,-1],[3332,-1],[3335,-1],[3380,-1],[3383,-1],[3404,-1],[3407,-1],[3452,-1],[3455,-1]],[[133,1],[134,1],[253,1],[254,1],[261,1],[262,1],[381,1],[382,1],[1157,-1],[1158,-1],[1277,-1],[1278,-1],[1285,-1],[1286,-1],[1405,-1],[1406,-1],[2181,-1],[2182,-1],[2301,-1],[2302,-1],[2309,-1],[2310,-1],[2429,-1],[2430,-1],[3205,-1],[3206,-1],[3325,-1],[3326,-1],[3333,-1],[3334,-1],[3453,-1],[3454,-1]],[[136,1],[139,1],[184,1],[187,1],[264,1],[267,1],[312,1],[315,1],[1160,-1],[1163,-1],[1208,-1],[1211,-1],[1288,-1],[1291,-1],[1336,-1],[1339,-1],[2240,-1],[2243,-1],[2288,-1],[2291,-1],[2368,-1],[2371,-1],[2416,-1],[2419,-1],[3264,-1],[3267,-1],[3312,-1],[3315,-1],[3392,-1],[3395,-1],[3440,-1],[3443,-1]],[[137,1],[138,1],[193,1],[194,1],[265,1],[266,1],[321,1],[322,1],[1161,-1],[1162,-1],[1217,-1],[1218,-1],[1289,-1],[1290,-1],[1345,-1],[1346,-1],[2185,-1],[2186,-1],[2241,-1],[2242,-1],[2313,-1],[2314,-1],[2369,-1],[2370,-1],[3209,-1],[3210,-1],[3265,-1],[3266,-1],[3337,-1],[3338,-1],[3393,-1],[3394,-1]],[[140,1],[143,1],[188,1],[191,1],[268,1],[271,1],[316,1],[319,1],[1164,-1],[1167,-1],[1212,-1],[1215,-1],[1292,-1],[1295,-1],[1340,-1],[1343,-1],[2244,-1],[2247,-1],[2292,-1],[2295,-1],[2372,-1],[2375,-1],[2420,-1],[2423,-1],[3268,-1],[3271,-1],[3316,-1],[3319,-1],[3396,-1],[3399,-1],[3444,-1],[3447,-1]],[[141,1],[142,1],[197,1],[198,1],[269,1],[270,1],[325,1],[326,1],[1165,-1],[1166,-1],[1221,-1],[1222,-1],[1293,-1],[1294,-1],[1349,-1],[1350,-1],[2189,-1],[2190,-1],[2245,-1],[2246,-1],[2317,-1],[2318,-1],[2373,-1],[2374,-1],[3213,-1],[3214,-1],[3269,-1],[3270,-1],[3341,-1],[3342,-1],[3397,-1],[3398,-1]],[[144,1],[147,1],[216,1],[219,1],[272,1],[275,1],[344,1],[347,1],[1184,-1],[1187,-1],[1256,-1],[1259,-1],[1312,-1],[1315,-1],[1384,-1],[1387,-1],[2208,-1],[2211,-1],[2280,-1],[2283,-1],[2336,-1],[2339,-1],[2408,-1],[2411,-1],[3216,-1],[3219,-1],[3288,-1],[3291,-1],[3344,-1],[3347,-1],[3416,-1],[3419,-1]],[[145,1],[146,1],[161,1],[162,1],[273,1],[274,1],[289,1],[290,1],[1169,-1],[1170,-1],[1185,-1],[1186,-1],[1297,-1],[1298,-1],[1313,-1],[1314,-1],[2193,-1],[2194,-1],[2209,-1],[2210,-1],[2321,-1],[2322,-1],[2337,-1],[2338,-1],[3217,-1],[3218,-1],[3233,-1],[3234,-1],[3345,-1],[3346,-1],[3361,-1],[3362,-1]],[[148,1],[151,1],[220,1],[223,1],[276,1],[279,1],[348,1],[351,1],[1188,-1],[1191,-1],[1260,-1],[1263,-1],[1316,-1],[1319,-1],[1388,-1],[1391,-1],[2212,-1],[2215,-1],[2284,-1],[2287,-1],[2340,-1],[2343,-1],[2412,-1],[2415,-1],[3220,-1],[3223,-1],[3292,-1],[3295,-1],[3348,-1],[3351,-1],[3420,-1],[3423,-1]],[[149,1],[150,1],[165,1],[166,1],[277,1],[278,1],[293,1],[294,1],[1173,-1],[1174,-1],[1189,-1],[1190,-1],[1301,-1],[1302,-1],[1317,-1],[1318,-1],[2197,-1],[2198,-1],[2213,-1],[2214,-1],[2325,-1],[2326,-1],[2341,-1],[2342,-1],[3221,-1],[3222,-1],[3237,-1],[3238,-1],[3349,-1],[3350,-1],[3365,-1],[3366,-1]],[[152,1],[155,1],[224,1],[227,1],[280,1],[283,1],[352,1],[355,1],[1192,-1],[1195,-1],[1232,-1],[1235,-1],[1320,-1],[1323,-1],[1360,-1],[1363,-1],[2200,-1],[2203,-1],[2272,-1],[2275,-1],[2328,-1],[2331,-1],[2400,-1],[2403,-1],[3240,-1],[3243,-1],[3280,-1],[3283,-1],[3368,-1],[3371,-1],[3408,-1],[3411,-1]],[[153,1],[154,1],[169,1],[170,1],[209,1],[210,1],[225,1],[226,1],[281,1],[282,1],[297,1],[298,1],[337,1],[338,1],[353,1],[354,1],[1177,-1],[1178,-1],[1193,-1],[1194,-1],[1233,-1],[1234,-1],[1249,-1],[1250,-1],[1305,-1],[1306,-1],[1321,-1],[1322,-1],[1361,-1],[1362,-1],[1377,-1],[1378,-1],[2201,-1],[2202,-1],[2217,-1],[2218,-1],[2257,-1],[2258,-1],[2273,-1],[2274,-1],[2329,-1],[2330,-1],[2345,-1],[2346,-1],[2385,-1],[2386,-1],[2401,-1],[2402,-1],[3225,-1],[3226,-1],[3241,-1],[3242,-1],[3281,-1],[3282,-1],[3297,-1],[3298,-1],[3353,-1],[3354,-1],[3369,-1],[3370,-1],[3409,-1],[3410,-1],[3425,-1],[3426,-1]],[[156,1],[159,1],[228,1],[231,1],[284,1],[287,1],[356,1],[359,1],[1196,-1],[1199,-1],[1236,-1],[1239,-1],[1324,-1],[1327,-1],[1364,-1],[1367,-1],[2204,-1],[2207,-1],[2276,-1],[2279,-1],[2332,-1],[2335,-1],[2404,-1],[2407,-1],[3244,-1],[3247,-1],[3284,-1],[3287,-1],[3372,-1],[3375,-1],[3412,-1],[3415,-1]],[[157,1],[158,1],[173,1],[174,1],[213,1],[214,1],[229,1],[230,1],[285,1],[286,1],[301,1],[302,1],[341,1],[342,1],[357,1],[358,1],[1181,-1],[1182,-1],[1197,-1],[1198,-1],[1237,-1],[1238,-1],[1253,-1],[1254,-1],[1309,-1],[1310,-1],[1325,-1],[1326,-1],[1365,-1],[1366,-1],[1381,-1],[1382,-1],[2205,-1],[2206,-1],[2221,-1],[2222,-1],[2261,-1],[2262,-1],[2277,-1],[2278,-1],[2333,-1],[2334,-1],[2349,-1],[2350,-1],[2389,-1],[2390,-1],[2405,-1],[2406,-1],[3229,-1],[3230,-1],[3245,-1],[3246,-1],[3285,-1],[3286,-1],[3301,-1],[3302,-1],[3357,-1],[3358,-1],[3373,-1],[3374,-1],[3413,-1],[3414,-1],[3429,-1],[3430,-1]],[[160,1],[163,1],[232,1],[235,1],[288,1],[291,1],[360,1],[363,1],[1168,-1],[1171,-1],[1240,-1],[1243,-1],[1296,-1],[1299,-1],[1368,-1],[1371,-1],[2192,-1],[2195,-1],[2264,-1],[2267,-1],[2320,-1],[2323,-1],[2392,-1],[2395,-1],[3232,-1],[3235,-1],[3304,-1],[3307,-1],[3360,-1],[3363,-1],[3432,-1],[3435,-1]],[[164,1],[167,1],[236,1],[239,1],[292,1],[295,1],[364,1],[367,1],[1172,-1],[1175,-1],[1244,-1],[1247,-1],[1300,-1],[1303,-1],[1372,-1],[1375,-1],[2196,-1],[2199,-1],[2268,-1],[2271,-1],[2324,-1],[2327,-1],[2396,-1],[2399,-1],[3236,-1],[3239,-1],[3308,-1],[3311,-1],[3364,-1],[3367,-1],[3436,-1],[3439,-1]],[[168,1],[171,1],[208,1],[211,1],[296,1],[299,1],[336,1],[339,1],[1176,-1],[1179,-1],[1248,-1],[1251,-1],[1304,-1],[1307,-1],[1376,-1],[1379,-1],[2216,-1],[2219,-1],[2256,-1],[2259,-1],[2344,-1],[2347,-1],[2384,-1],[2387,-1],[3224,-1],[3227,-1],[3296,-1],[3299,-1],[3352,-1],[3355,-1],[3424,-1],[3427,-1]],[[172,1],[175,1],[212,1],[215,1],[300,1],[303,1],[340,1],[343,1],[1180,-1],[1183,-1],[1252,-1],[1255,-1],[1308,-1],[1311,-1],[1380,-1],[1383,-1],[2220,-1],[2223,-1],[2260,-1],[2263,-1],[2348,-1],[2351,-1],[2388,-1],[2391,-1],[3228,-1],[3231,-1],[3300,-1],[3303,-1],[3356,-1],[3359,-1],[3428,-1],[3431,-1]],[[177,1],[178,1],[201,1],[202,1],[305,1],[306,1],[329,1],[330,1],[1201,-1],[1202,-1],[1225,-1],[1226,-1],[1329,-1],[1330,-1],[1353,-1],[1354,-1],[2225,-1],[2226,-1],[2249,-1],[2250,-1],[2353,-1],[2354,-1],[2377,-1],[2378,-1],[3249,-1],[3250,-1],[3273,-1],[3274,-1],[3377,-1],[3378,-1],[3401,-1],[3402,-1]],[[181,1],[182,1],[205,1],[206,1],[309,1],[310,1],[333,1],[334,1],[1205,-1],[1206,-1],[1229,-1],[1230,-1],[1333,-1],[1334,-1],[1357,-1],[1358,-1],[2229,-1],[2230,-1],[2253,-1],[2254,-1],[2357,-1],[2358,-1],[2381,-1],[2382,-1],[3253,-1],[3254,-1],[3277,-1],[3278,-1],[3381,-1],[3382,-1],[3405,-1],[3406,-1]],[[185,1],[186,1],[241,1],[242,1],[313,1],[314,1],[369,1],[370,1],[1209,-1],[1210,-1],[1265,-1],[1266,-1],[1337,-1],[1338,-1],[1393,-1],[1394,-1],[2233,-1],[2234,-1],[2289,-1],[2290,-1],[2361,-1],[2362,-1],[2417,-1],[2418,-1],[3257,-1],[3258,-1],[3313,-1],[3314,-1],[3385,-1],[3386,-1],[3441,-1],[3442,-1]],[[189,1],[190,1],[245,1],[246,1],[317,1],[318,1],[373,1],[374,1],[1213,-1],[1214,-1],[1269,-1],[1270,-1],[1341,-1],[1342,-1],[1397,-1],[1398,-1],[2237,-1],[2238,-1],[2293,-1],[2294,-1],[2365,-1],[2366,-1],[2421,-1],[2422,-1],[3261,-1],[3262,-1],[3317,-1],[3318,-1],[3389,-1],[3390,-1],[3445,-1],[3446,-1]],[[192,1],[195,1],[240,1],[243,1],[320,1],[323,1],[368,1],[371,1],[1216,-1],[1219,-1],[1264,-1],[1267,-1],[1344,-1],[1347,-1],[1392,-1],[1395,-1],[2184,-1],[2187,-1],[2232,-1],[2235,-1],[2312,-1],[2315,-1],[2360,-1],[2363,-1],[3208,-1],[3211,-1],[3256,-1],[3259,-1],[3336,-1],[3339,-1],[3384,-1],[3387,-1]],[[196,1],[199,1],[244,1],[247,1],[324,1],[327,1],[372,1],[375,1],[1220,-1],[1223,-1],[1268,-1],[1271,-1],[1348,-1],[1351,-1],[1396,-1],[1399,-1],[2188,-1],[2191,-1],[2236,-1],[2239,-1],[2316,-1],[2319,-1],[2364,-1],[2367,-1],[3212,-1],[3215,-1],[3260,-1],[3263,-1],[3340,-1],[3343,-1],[3388,-1],[3391,-1]],[[217,1],[218,1],[233,1],[234,1],[345,1],[346,1],[361,1],[362,1],[1241,-1],[1242,-1],[1257,-1],[1258,-1],[1369,-1],[1370,-1],[1385,-1],[1386,-1],[2265,-1],[2266,-1],[2281,-1],[2282,-1],[2393,-1],[2394,-1],[2409,-1],[2410,-1],[3289,-1],[3290,-1],[3305,-1],[3306,-1],[3417,-1],[3418,-1],[3433,-1],[3434,-1]],[[221,1],[222,1],[237,1],[238,1],[349,1],[350,1],[365,1],[366,1],[1245,-1],[1246,-1],[1261,-1],[1262,-1],[1373,-1],[1374,-1],[1389,-1],[1390,-1],[2269,-1],[2270,-1],[2285,-1],[2286,-1],[2397,-1],[2398,-1],[2413,-1],[2414,-1],[3293,-1],[3294,-1],[3309,-1],[3310,-1],[3421,-1],[3422,-1],[3437,-1],[3438,-1]],[[384,1],[387,1],[1408,-1],[1411,-1],[2432,-1],[2435,-1],[3456,-1],[3459,-1]],[[388,1],[391,1],[1412,-1],[1415,-1],[2436,-1],[2439,-1],[3460,-1],[3463,-1]],[[409,1],[410,1],[1449,-1],[1450,-1],[2529,-1],[2530,-1],[3537,-1],[3538,-1]],[[413,1],[414,1],[1453,-1],[1454,-1],[2533,-1],[2534,-1],[3541,-1],[3542,-1]],[[425,1],[426,1],[1433,-1],[1434,-1],[2513,-1],[2514,-1],[3553,-1],[3554,-1]],[[429,1],[430,1],[1437,-1],[1438,-1],[2517,-1],[2518,-1],[3557,-1],[3558,-1]],[[432,1],[435,1],[1456,-1],[1459,-1],[2480,-1],[2483,-1],[3504,-1],[3507,-1]],[[436,1],[439,1],[1460,-1],[1463,-1],[2484,-1],[2487,-1],[3508,-1],[3511,-1]],[[456,1],[459,1],[1480,-1],[1483,-1],[2504,-1],[2507,-1],[3528,-1],[3531,-1]],[[460,1],[463,1],[1484,-1],[1487,-1],[2508,-1],[2511,-1],[3532,-1],[3535,-1]],[[465,1],[466,1],[1505,-1],[1506,-1],[2473,-1],[2474,-1],[3481,-1],[3482,-1]],[[469,1],[470,1],[1509,-1],[1510,-1],[2477,-1],[2478,-1],[3485,-1],[3486,-1]],[[481,1],[482,1],[1489,-1],[1490,-1],[2457,-1],[2458,-1],[3497,-1],[3498,-1]],[[485,1],[486,1],[1493,-1],[1494,-1],[2461,-1],[2462,-1],[3501,-1],[3502,-1]],[[504,1],[507,1],[1528,-1],[1531,-1],[2552,-1],[2555,-1],[3576,-1],[3579,-1]],[[508,1],[511,1],[1532,-1],[1535,-1],[2556,-1],[2559,-1],[3580,-1],[3583,-1]]]} diff --git a/research/c3-x3-plus-charpoly/evidence/matrix.json b/research/c3-x3-plus-charpoly/evidence/matrix.json new file mode 100644 index 0000000000..bd62899e16 --- /dev/null +++ b/research/c3-x3-plus-charpoly/evidence/matrix.json @@ -0,0 +1 @@ +{"rows":[[4,0,0,0,0,0,0,8,0,0,0,8,0,2,0,0,0,0,0,-2,0,0,0,8,0,0,0,0,0,0,0,0,2,0,0,0,2,0,0,0,0,0,0,8,0,8,0,0,0,8,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0],[0,4,0,0,0,0,4,0,0,0,4,0,4,0,0,0,0,4,0,0,0,0,2,0,0,0,0,0,0,4,2,0,0,0,0,0,0,0,0,0,0,0,8,0,4,0,0,0,4,0,0,0,0,0,0,0,4,0,0,0,0,0,0,0,4,0,0,0,2,0,0,0,0,0,0,0,0,0,0,0,0,0,2,0],[0,0,-4,0,0,8,0,0,0,8,0,0,0,0,0,2,0,0,0,0,0,-2,0,0,0,8,0,0,0,0,0,0,0,2,0,0,0,2,0,0,0,8,0,0,0,0,0,8,0,0,0,8,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0],[0,0,0,-4,4,0,0,0,4,0,0,0,0,0,4,0,4,0,0,0,0,0,0,0,2,0,0,0,4,0,0,2,0,0,0,0,0,0,0,0,8,0,0,0,0,0,4,0,0,0,4,0,0,0,0,0,0,4,0,0,0,0,0,0,0,4,0,0,0,2,0,0,0,0,0,0,0,0,0,0,0,0,0,2],[0,0,0,4,-4,4,0,0,0,0,0,0,0,0,0,2,0,0,0,0,0,2,0,0,0,4,4,0,0,0,0,0,0,0,4,0,0,0,0,0,0,4,0,0,0,0,0,4,0,0,0,0,0,8,0,0,0,0,0,0,4,0,0,4,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,2,0,2,0,0],[0,0,2,0,4,-4,0,0,4,0,0,0,0,0,4,0,0,0,0,0,4,0,0,0,0,0,0,0,4,0,0,2,0,0,0,0,0,0,0,0,8,0,0,0,0,0,4,0,0,0,0,0,4,0,0,0,0,0,4,0,0,0,0,0,0,4,0,0,0,0,0,0,0,0,0,2,0,0,0,0,0,0,0,2],[0,4,0,0,0,0,4,4,0,0,0,0,0,2,0,0,0,0,0,2,0,0,0,4,0,0,0,4,0,0,0,0,0,0,0,4,0,0,0,0,0,0,0,4,0,4,0,0,0,0,0,0,0,0,0,8,0,0,0,0,0,4,4,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,2,0,2,0,0,0],[2,0,0,0,0,0,4,4,0,0,4,0,4,0,0,0,0,0,4,0,0,0,0,0,0,0,0,0,0,4,2,0,0,0,0,0,0,0,0,0,0,0,8,0,4,0,0,0,0,0,0,0,0,0,4,0,0,0,0,4,0,0,0,0,4,0,0,0,0,0,0,0,0,0,2,0,0,0,0,0,0,0,2,0],[0,0,0,4,0,4,0,0,-4,4,0,0,0,0,0,2,0,0,0,0,0,0,0,0,0,4,0,0,0,0,0,0,0,2,4,0,0,0,0,0,0,4,0,0,0,0,0,0,0,0,0,4,0,8,0,0,0,0,0,0,4,0,0,0,0,0,0,4,0,0,0,0,0,2,0,0,0,0,0,0,0,2,0,0],[0,0,2,0,0,0,0,0,4,-4,0,0,0,0,4,0,4,0,0,0,4,0,0,0,2,0,0,0,4,0,0,0,0,0,0,0,0,0,0,0,8,0,0,0,0,0,0,0,0,0,4,0,4,0,0,0,0,4,4,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,2,0,0,0,0,0,2],[0,4,0,0,0,0,0,4,0,0,4,4,0,2,0,0,0,0,0,0,0,0,0,4,0,0,0,0,0,0,0,0,2,0,0,4,0,0,0,0,0,0,0,4,0,0,0,0,0,4,0,0,0,0,0,8,0,0,0,0,0,4,0,0,0,0,4,0,0,0,0,0,2,0,0,0,0,0,0,0,2,0,0,0],[2,0,0,0,0,0,0,0,0,0,4,4,4,0,0,0,0,4,4,0,0,0,2,0,0,0,0,0,0,4,0,0,0,0,0,0,0,0,0,0,0,0,8,0,0,0,0,0,4,0,0,0,0,0,4,0,4,0,0,4,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,2,0,0,0,0,0,2,0],[0,4,0,0,0,0,0,4,0,0,0,4,4,0,0,0,0,0,0,2,0,0,0,0,0,0,0,4,0,0,0,0,2,0,0,4,0,0,0,0,0,0,0,0,0,4,0,0,0,4,0,0,0,0,0,8,0,0,0,0,0,0,4,0,0,0,4,0,0,0,2,0,0,0,0,0,0,0,0,0,2,0,0,0],[2,0,0,0,0,0,8,0,0,0,8,0,0,-4,0,0,0,0,8,-8,0,0,-2,0,0,0,0,0,0,0,2,0,8,0,0,0,8,0,2,0,0,0,0,0,8,0,0,0,8,0,0,0,0,0,8,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0],[0,0,0,4,0,4,0,0,0,4,0,0,0,0,-4,0,0,0,0,0,0,2,0,0,0,0,4,0,0,0,0,0,0,2,4,0,0,0,0,0,0,0,0,0,0,0,0,4,0,0,0,4,0,8,0,0,0,0,0,0,0,0,0,4,0,0,0,4,0,0,0,2,0,0,0,0,0,0,0,0,0,2,0,0],[0,0,2,0,8,0,0,0,8,0,0,0,0,0,0,-4,0,0,0,0,8,0,0,0,-2,0,0,0,0,0,0,2,0,0,0,0,0,0,0,2,0,0,0,0,0,0,8,0,0,0,8,0,8,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0],[0,0,0,4,0,0,0,0,0,4,0,0,0,0,0,0,-4,0,0,0,0,2,0,0,0,4,4,0,0,0,0,0,0,0,4,0,0,2,0,0,0,4,0,0,0,0,0,0,0,0,0,4,0,8,0,0,0,0,0,0,4,0,0,0,0,0,0,4,0,0,0,2,0,0,0,0,0,0,0,2,0,0,0,0],[0,4,0,0,0,0,0,0,0,0,0,4,0,0,0,0,0,4,0,2,0,0,0,4,0,0,0,4,0,0,0,0,0,0,0,4,2,0,0,0,0,0,0,4,0,0,0,0,0,4,0,0,0,0,0,8,0,0,0,0,0,4,0,0,0,0,4,0,0,0,2,0,0,0,0,0,0,0,2,0,0,0,0,0],[0,0,0,0,0,0,0,4,0,0,0,4,0,2,0,0,0,0,4,0,0,0,0,4,0,0,0,4,0,0,0,0,0,0,0,4,2,0,0,0,0,0,0,0,0,4,0,0,0,4,0,0,0,0,0,8,0,0,0,0,0,0,4,0,0,0,4,0,0,0,0,0,2,0,0,0,0,0,2,0,0,0,0,0],[-2,0,0,0,0,0,8,0,0,0,0,0,8,-8,0,0,0,8,0,28,0,0,2,0,0,0,0,0,0,0,2,0,-8,0,0,0,-8,0,2,0,0,0,0,0,8,0,0,0,0,0,0,0,0,0,0,0,8,0,0,8,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0],[0,0,0,0,0,4,0,0,0,4,0,0,0,0,0,2,0,0,0,0,-4,0,0,0,0,4,4,0,0,0,0,0,0,0,4,0,0,2,0,0,0,0,0,0,0,0,0,4,0,0,0,4,0,8,0,0,0,0,0,0,0,0,0,4,0,0,0,4,0,0,0,0,0,2,0,0,0,0,0,2,0,0,0,0],[0,0,-2,0,8,0,0,0,0,0,0,0,0,0,8,0,8,0,0,0,0,-4,0,0,2,0,0,0,0,0,0,2,0,0,0,0,0,0,0,2,0,0,0,0,0,0,8,0,0,0,0,0,0,0,0,0,0,8,8,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0],[0,8,0,0,0,0,0,0,0,0,0,8,0,-2,0,0,0,0,0,2,0,0,4,0,0,0,0,8,0,0,0,0,2,0,0,0,2,0,0,0,0,0,0,0,0,0,0,0,0,8,0,0,0,0,0,0,0,0,0,0,0,8,8,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0],[2,0,0,0,0,0,4,0,0,0,4,0,0,0,0,0,0,4,4,0,0,0,0,4,0,0,0,0,0,4,0,0,0,0,0,0,0,0,2,0,0,0,8,0,4,0,0,0,4,0,0,0,0,0,0,0,4,0,0,0,0,0,0,0,4,0,0,0,0,0,0,0,0,0,2,0,2,0,0,0,0,0,0,0],[0,0,0,8,0,0,0,0,0,8,0,0,0,0,0,-2,0,0,0,0,0,2,0,0,-4,0,8,0,0,0,0,0,0,2,0,0,0,2,0,0,0,0,0,0,0,0,0,0,0,0,0,8,0,0,0,0,0,0,0,0,8,0,0,8,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0],[0,0,2,0,4,0,0,0,4,0,0,0,0,0,0,0,4,0,0,0,4,0,0,0,0,-4,0,0,4,0,0,0,0,0,0,0,0,0,0,2,8,0,0,0,0,0,4,0,0,0,4,0,0,0,0,0,0,4,0,0,0,0,0,0,0,4,0,0,0,0,0,0,0,0,0,2,0,2,0,0,0,0,0,0],[0,0,0,0,4,0,0,0,0,0,0,0,0,0,4,0,4,0,0,0,4,0,0,0,2,0,-4,0,4,0,0,0,0,0,0,0,0,0,0,2,8,0,0,0,0,0,4,0,0,0,0,0,4,0,0,0,0,0,4,0,0,0,0,0,0,4,0,0,0,2,0,0,0,0,0,0,0,2,0,0,0,0,0,0],[0,0,0,0,0,0,4,0,0,0,0,0,4,0,0,0,0,4,4,0,0,0,2,0,0,0,0,4,0,4,0,0,0,0,0,0,0,0,2,0,0,0,8,0,4,0,0,0,0,0,0,0,0,0,4,0,0,0,0,4,0,0,0,0,4,0,0,0,2,0,0,0,0,0,0,0,2,0,0,0,0,0,0,0],[0,0,0,4,0,4,0,0,0,4,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,4,4,0,-4,0,0,0,0,2,0,0,0,2,0,0,0,4,0,0,0,0,0,4,0,0,0,0,0,8,0,0,0,0,0,0,4,0,0,4,0,0,0,0,0,0,0,2,0,2,0,0,0,0,0,0,0,0,0,0],[0,4,0,0,0,0,0,4,0,0,0,4,0,0,0,0,0,0,0,0,0,0,0,4,0,0,0,4,0,4,0,0,2,0,0,0,2,0,0,0,0,0,0,4,0,4,0,0,0,0,0,0,0,0,0,8,0,0,0,0,0,4,4,0,0,0,0,0,0,0,2,0,2,0,0,0,0,0,0,0,0,0,0,0],[0,8,0,0,0,0,0,8,0,0,0,0,0,2,0,0,0,0,0,2,0,0,0,0,0,0,0,0,0,0,4,0,2,0,0,8,-2,0,0,0,0,0,0,0,0,8,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,8,0,0,0,0,8,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0],[0,0,0,8,0,8,0,0,0,0,0,0,0,0,0,2,0,0,0,0,0,2,0,0,0,0,0,0,0,0,0,-4,0,2,8,0,0,-2,0,0,0,0,0,0,0,0,0,8,0,0,0,0,0,0,0,0,0,0,0,0,8,0,0,0,0,0,0,8,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0],[2,0,0,0,0,0,0,0,0,0,8,0,8,8,0,0,0,0,0,-8,0,0,2,0,0,0,0,0,0,8,2,0,-4,0,0,0,8,0,-2,0,0,0,0,0,0,0,0,0,8,0,0,0,0,0,0,0,0,0,0,8,0,0,0,0,8,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0],[0,0,2,0,0,0,0,0,8,0,0,0,0,0,8,0,0,0,0,0,0,0,0,0,2,0,0,0,8,0,0,2,0,-4,0,0,0,0,0,-2,0,0,0,0,0,0,0,0,0,0,8,0,0,0,0,0,0,0,8,0,0,0,0,0,0,8,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0],[0,0,0,0,4,0,0,0,4,0,0,0,0,0,4,0,4,0,0,0,4,0,0,0,0,0,0,0,0,0,0,2,0,0,-4,0,0,0,0,2,8,0,0,0,0,0,0,0,0,0,4,0,4,0,0,0,0,4,4,0,0,0,0,0,0,0,0,0,0,2,0,0,0,0,0,2,0,0,0,0,0,0,0,0],[0,0,0,0,0,0,4,0,0,0,4,0,4,0,0,0,0,4,4,0,0,0,0,0,0,0,0,0,0,0,2,0,0,0,0,4,0,0,2,0,0,0,8,0,0,0,0,0,4,0,0,0,0,0,4,0,4,0,0,4,0,0,0,0,0,0,0,0,2,0,0,0,0,0,2,0,0,0,0,0,0,0,0,0],[2,0,0,0,0,0,0,0,0,0,0,0,0,8,0,0,0,8,8,-8,0,0,2,0,0,0,0,0,0,8,-2,0,8,0,0,0,-4,0,2,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,8,0,8,0,0,0,0,0,0,0,8,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0],[0,0,2,0,0,0,0,0,0,0,0,0,0,0,0,0,8,0,0,0,8,0,0,0,2,0,0,0,8,0,0,-2,0,0,0,0,0,-4,0,2,0,0,0,0,0,0,0,0,0,0,0,0,8,0,0,0,0,8,0,0,0,0,0,0,0,8,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0],[0,0,0,0,0,0,0,0,0,0,0,0,0,2,0,0,0,0,0,2,0,0,0,8,0,0,0,8,0,0,0,0,-2,0,0,8,2,0,4,0,0,0,0,8,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,8,0,0,0,8,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0],[0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,2,0,0,0,0,0,2,0,0,0,8,8,0,0,0,0,0,0,-2,8,0,0,2,0,-4,0,8,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,8,0,0,0,8,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0],[0,0,0,4,0,4,0,0,0,4,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,4,4,0,0,0,0,0,0,0,4,0,0,0,0,0,-4,4,0,0,0,0,0,4,0,0,0,4,0,4,0,0,0,0,0,0,4,0,0,4,0,0,0,4,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0],[0,0,2,0,4,0,0,0,4,0,0,0,0,0,0,0,4,0,0,0,0,0,0,0,0,0,0,0,4,0,0,0,0,0,0,0,0,0,0,2,8,-4,0,0,0,0,4,0,0,0,4,0,4,0,0,0,0,4,0,0,0,0,0,0,0,4,0,0,0,2,0,0,0,0,0,0,0,0,0,0,0,0,0,2],[0,4,0,0,0,0,0,4,0,0,0,4,0,0,0,0,0,0,0,0,0,0,0,4,0,0,0,4,0,0,0,0,0,0,0,4,0,0,0,0,0,0,4,4,0,4,0,0,0,4,0,0,0,0,0,4,0,0,0,0,0,4,4,0,0,0,4,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0],[2,0,0,0,0,0,4,0,0,0,4,0,0,0,0,0,0,4,0,0,0,0,0,0,0,0,0,0,0,4,0,0,0,0,0,0,0,0,2,0,0,0,8,4,4,0,0,0,4,0,0,0,0,0,4,0,4,0,0,0,0,0,0,0,4,0,0,0,2,0,0,0,0,0,0,0,0,0,0,0,0,0,2,0],[0,4,0,0,0,0,0,4,0,0,0,0,0,2,0,0,0,0,0,2,0,0,0,4,0,0,0,4,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,4,4,4,0,0,0,0,0,0,0,0,0,8,0,0,0,0,0,4,4,0,0,0,4,0,0,0,2,0,2,0,0,0,0,0,0,0,0,0,0,0],[2,0,0,0,0,0,4,0,0,0,0,0,4,0,0,0,0,0,4,0,0,0,0,0,0,0,0,0,0,4,2,0,0,0,0,0,0,0,0,0,0,0,8,0,4,4,0,0,4,0,0,0,0,0,4,0,0,0,0,4,0,0,0,0,4,0,0,0,2,0,0,0,0,0,0,0,2,0,0,0,0,0,0,0],[0,0,0,4,0,4,0,0,0,0,0,0,0,0,0,2,0,0,0,0,0,2,0,0,0,4,4,0,0,0,0,0,0,0,0,0,0,0,0,0,0,4,0,0,0,0,-4,4,0,0,0,0,0,8,0,0,0,0,0,0,4,0,0,4,0,0,0,4,0,0,0,2,0,2,0,0,0,0,0,0,0,0,0,0],[0,0,2,0,4,0,0,0,0,0,0,0,0,0,4,0,0,0,0,0,4,0,0,0,0,0,0,0,4,0,0,2,0,0,0,0,0,0,0,0,8,0,0,0,0,0,4,-4,0,0,4,0,4,0,0,0,0,0,4,0,0,0,0,0,0,4,0,0,0,2,0,0,0,0,0,0,0,2,0,0,0,0,0,0],[0,4,0,0,0,0,0,0,0,0,0,4,0,2,0,0,0,0,0,0,0,0,0,4,0,0,0,0,0,0,0,0,2,0,0,4,0,0,0,0,0,0,0,4,0,4,0,0,4,4,0,0,0,0,0,8,0,0,0,0,0,4,0,0,0,0,4,0,0,0,2,0,0,0,0,0,0,0,2,0,0,0,0,0],[2,0,0,0,0,0,0,0,0,0,4,0,4,0,0,0,0,4,4,0,0,0,2,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,8,0,0,0,0,0,4,4,0,0,0,0,4,0,4,0,0,4,0,0,0,0,4,0,0,0,2,0,0,0,0,0,2,0,0,0,0,0,0,0,0,0],[0,0,0,4,0,0,0,0,0,4,0,0,0,0,0,2,0,0,0,0,0,0,0,0,0,4,0,0,0,0,0,0,0,2,4,0,0,0,0,0,0,4,0,0,0,0,0,4,0,0,-4,4,0,8,0,0,0,0,0,0,4,0,0,0,0,0,0,4,0,0,0,2,0,0,0,0,0,0,0,2,0,0,0,0],[0,0,2,0,0,0,0,0,4,0,0,0,0,0,4,0,4,0,0,0,4,0,0,0,2,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,8,0,0,0,0,0,0,0,0,0,4,-4,4,0,0,0,0,4,4,0,0,0,0,0,0,4,0,0,0,2,0,0,0,0,0,2,0,0,0,0,0,0,0,0],[0,0,0,0,0,4,0,0,0,4,0,0,0,0,0,2,0,0,0,0,0,0,0,0,0,0,4,0,0,0,0,0,0,0,4,0,0,2,0,0,0,4,0,0,0,0,0,4,0,0,0,4,-4,8,0,0,0,0,0,0,0,0,0,4,0,0,0,4,0,0,0,2,0,0,0,0,0,0,0,0,0,2,0,0],[0,0,0,0,4,0,0,0,4,0,0,0,0,0,4,0,4,0,0,0,4,0,0,0,0,0,0,0,4,0,0,0,0,0,0,0,0,0,0,0,4,0,0,0,0,0,4,0,0,0,4,0,4,-4,0,0,0,4,4,0,0,0,0,0,0,4,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0],[0,0,0,0,0,0,0,4,0,0,0,4,0,2,0,0,0,0,0,0,0,0,0,0,0,0,0,4,0,0,0,0,0,0,0,4,2,0,0,0,0,0,0,4,0,4,0,0,0,4,0,0,0,0,4,8,0,0,0,0,0,0,4,0,0,0,4,0,0,0,2,0,0,0,0,0,0,0,0,0,2,0,0,0],[0,0,0,0,0,0,4,0,0,0,4,0,4,0,0,0,0,4,4,0,0,0,0,0,0,0,0,0,0,4,0,0,0,0,0,0,0,0,0,0,0,0,4,0,4,0,0,0,4,0,0,0,0,0,4,4,4,0,0,4,0,0,0,0,4,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0],[0,4,0,0,0,0,0,0,0,0,0,4,0,0,0,0,0,0,0,2,0,0,0,4,0,0,0,0,0,0,0,0,0,0,0,4,2,0,0,0,0,0,0,4,0,0,0,0,0,4,0,0,0,0,0,8,4,0,0,0,0,4,4,0,0,0,4,0,0,0,0,0,2,0,0,0,0,0,0,0,2,0,0,0],[0,0,0,4,0,0,0,0,0,4,0,0,0,0,0,0,0,0,0,0,0,2,0,0,0,4,0,0,0,0,0,0,0,0,4,0,0,2,0,0,0,4,0,0,0,0,0,0,0,0,0,4,0,8,0,0,0,-4,0,0,4,0,0,4,0,0,0,4,0,0,0,0,0,2,0,0,0,0,0,0,0,2,0,0],[0,0,0,0,0,4,0,0,0,4,0,0,0,0,0,0,0,0,0,0,0,2,0,0,0,0,4,0,0,0,0,0,0,2,4,0,0,0,0,0,0,0,0,0,0,0,0,4,0,0,0,4,0,8,0,0,0,0,-4,0,4,0,0,4,0,0,0,4,0,0,0,0,0,2,0,0,0,0,0,2,0,0,0,0],[0,0,0,0,0,0,0,4,0,0,0,4,0,0,0,0,0,0,0,2,0,0,0,0,0,0,0,4,0,0,0,0,2,0,0,4,0,0,0,0,0,0,0,0,0,4,0,0,0,4,0,0,0,0,0,8,0,0,0,4,0,4,4,0,0,0,4,0,0,0,0,0,2,0,0,0,0,0,2,0,0,0,0,0],[0,0,0,0,4,0,0,0,4,0,0,0,0,0,0,0,4,0,0,0,0,0,0,0,2,0,0,0,4,0,0,2,0,0,0,0,0,0,0,0,8,0,0,0,0,0,4,0,0,0,4,0,0,0,0,0,0,4,4,0,-4,0,0,0,0,4,0,0,0,0,0,0,0,0,0,2,0,2,0,0,0,0,0,0],[0,0,0,0,0,0,4,0,0,0,4,0,0,0,0,0,0,4,0,0,0,0,2,0,0,0,0,0,0,4,2,0,0,0,0,0,0,0,0,0,0,0,8,0,4,0,0,0,4,0,0,0,0,0,0,0,4,0,0,4,0,4,0,0,4,0,0,0,0,0,0,0,0,0,2,0,2,0,0,0,0,0,0,0],[0,0,0,0,0,0,4,0,0,0,0,0,4,0,0,0,0,0,4,0,0,0,2,0,0,0,0,0,0,4,0,0,0,0,0,0,0,0,2,0,0,0,8,0,4,0,0,0,0,0,0,0,0,0,4,0,4,0,0,4,0,0,4,0,4,0,0,0,0,0,0,0,0,0,2,0,0,0,0,0,0,0,2,0],[0,0,0,0,4,0,0,0,0,0,0,0,0,0,4,0,0,0,0,0,4,0,0,0,2,0,0,0,4,0,0,0,0,0,0,0,0,0,0,2,8,0,0,0,0,0,4,0,0,0,0,0,4,0,0,0,0,4,4,0,0,0,0,-4,0,4,0,0,0,0,0,0,0,0,0,2,0,0,0,0,0,0,0,2],[0,4,0,0,0,0,0,4,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,4,0,0,0,4,0,0,0,0,2,0,0,0,2,0,0,0,0,0,0,4,0,4,0,0,0,4,0,0,0,0,0,8,0,0,0,0,0,4,4,0,4,0,0,0,0,0,0,0,0,0,0,0,0,0,2,0,2,0,0,0],[0,0,0,4,0,4,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,4,4,0,0,0,0,0,0,2,0,0,0,2,0,0,0,4,0,0,0,0,0,4,0,0,0,4,0,8,0,0,0,0,0,0,4,0,0,4,0,-4,0,0,0,0,0,0,0,0,0,0,0,0,0,2,0,2,0,0],[0,0,0,0,0,0,0,0,0,0,4,0,4,0,0,0,0,4,4,0,0,0,0,0,0,0,0,0,0,0,2,0,0,0,0,0,0,0,2,0,0,0,8,0,4,0,0,0,4,0,0,0,0,0,4,0,4,0,0,4,0,0,0,0,0,0,4,0,0,0,0,0,0,0,0,0,2,0,0,0,0,0,2,0],[0,0,0,0,0,0,0,0,4,0,0,0,0,0,4,0,4,0,0,0,4,0,0,0,0,0,0,0,0,0,0,2,0,0,0,0,0,0,0,2,8,0,0,0,0,0,4,0,0,0,4,0,4,0,0,0,0,4,4,0,0,0,0,0,0,0,0,-4,0,0,0,0,0,0,0,0,0,2,0,0,0,0,0,2],[0,8,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,8,0,0,0,0,0,0,0,8,0,0,0,0,0,0,0,8,0,8,0,0,0,8,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,4,0,2,0,-2,0,0,0,0,0,2,0,2,0,0,0],[0,0,0,8,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,8,0,0,0,0,0,0,0,8,0,0,0,0,0,0,8,0,0,0,0,0,8,0,0,0,8,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,-4,0,2,0,-2,0,0,0,0,0,2,0,2,0,0],[0,0,0,0,0,0,0,0,0,0,0,0,8,0,0,0,0,8,0,0,0,0,0,0,0,0,0,0,0,8,0,0,0,0,0,0,0,0,0,0,0,0,0,0,8,0,0,0,8,0,0,0,0,0,8,0,0,0,0,0,0,0,0,0,0,0,0,0,2,0,4,0,0,0,-2,0,2,0,0,0,0,0,2,0],[0,0,0,0,0,0,0,0,0,0,0,0,0,0,8,0,8,0,0,0,0,0,0,0,0,0,0,0,8,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,8,0,0,0,8,0,8,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,2,0,4,0,-8,0,-2,0,2,0,8,0,-8,0,2],[0,0,0,0,0,0,0,0,0,0,8,0,0,0,0,0,0,0,8,0,0,0,0,0,0,0,0,0,0,8,0,0,0,0,0,0,0,0,0,0,0,0,0,0,8,0,0,0,0,0,0,0,0,0,0,0,8,0,0,8,0,0,0,0,0,0,0,0,-2,0,0,0,4,0,2,0,2,0,0,0,0,0,2,0],[0,0,0,0,0,0,0,0,8,0,0,0,0,0,0,0,0,0,0,0,8,0,0,0,0,0,0,0,8,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,8,0,0,0,0,0,0,0,0,0,0,8,8,0,0,0,0,0,0,0,0,0,0,-2,0,-8,0,4,0,2,0,2,0,8,0,-8,0,2],[0,0,0,0,0,0,0,8,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,8,0,0,0,0,0,0,0,0,0,0,0,8,0,0,0,0,0,0,0,0,0,0,0,0,0,8,0,0,0,0,0,0,0,0,0,0,0,8,8,0,0,0,0,0,0,0,-2,0,2,0,4,0,0,0,2,0,2,0,0,0],[0,0,0,0,0,8,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,8,0,0,0,0,0,0,0,0,8,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,8,0,0,0,0,0,0,0,0,8,0,0,8,0,0,0,0,0,0,0,-2,0,2,0,-4,0,0,0,2,0,2,0,0],[0,0,0,0,0,0,0,0,0,0,0,8,0,0,0,0,0,0,0,0,0,0,0,8,0,0,0,8,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,8,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,8,0,0,0,0,8,0,0,0,2,0,2,0,0,0,4,0,2,0,-2,0,0,0],[0,0,0,0,0,0,0,0,0,8,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,8,8,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,8,0,0,0,0,0,0,0,0,0,0,0,0,8,0,0,0,0,0,0,8,0,0,0,2,0,2,0,0,0,-4,0,2,0,-2,0,0],[0,0,0,0,0,0,8,0,0,0,0,0,0,0,0,0,0,8,8,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,8,0,0,0,0,0,0,0,0,0,0,8,0,0,0,0,8,0,0,0,2,0,0,0,0,0,2,0,2,0,4,0,0,0,-2,0],[0,0,0,0,8,0,0,0,0,0,0,0,0,0,0,0,8,0,0,0,8,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,8,0,0,0,0,0,0,0,8,0,0,0,0,0,0,8,0,0,0,2,0,8,0,8,0,2,0,2,0,-28,0,8,0,-2],[0,0,0,0,0,0,8,0,0,0,8,0,8,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,8,0,8,0,0,0,0,0,0,0,8,0,0,0,2,0,0,0,0,0,2,0,-2,0,0,0,4,0,2,0],[0,0,0,0,8,0,0,0,8,0,0,0,0,0,8,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,8,0,0,0,0,8,0,0,0,0,0,0,0,8,0,0,0,2,0,-8,0,-8,0,2,0,-2,0,8,0,4,0,2],[0,8,0,0,0,0,0,8,0,0,0,8,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,8,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,8,0,0,0,8,0,0,0,2,0,2,0,0,0,0,0,-2,0,2,0,4,0],[0,0,0,8,0,8,0,0,0,8,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,8,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,8,0,0,0,8,0,0,0,2,0,2,0,0,0,0,0,-2,0,2,0,-4]]} diff --git a/research/c3-x3-plus-charpoly/verify.py b/research/c3-x3-plus-charpoly/verify.py new file mode 100644 index 0000000000..d218f8aee9 --- /dev/null +++ b/research/c3-x3-plus-charpoly/verify.py @@ -0,0 +1,1038 @@ +#!/usr/bin/env python3 +"""Characteristic polynomial of the 84-dimensional X_3=+1 subspace. + +The space is the trivial character of the c=3 even-positive sign group H, +inside the joint (+1,+1) eigenspace of the explicit pair (u, v), cut by the +payload involution X_3 at eigenvalue +1. B = 4 A_1 is the integer operator +on Bell block c=3. Acceptance uses explicit checks, so python -O does not +skip a theorem or a rejection control. +""" + +import hashlib +import json +import pathlib +import sys +from fractions import Fraction + +ROOT = pathlib.Path(__file__).resolve().parents[2] +PACKAGE = pathlib.Path(__file__).resolve().parent +INTERFACE = ( + ROOT + / "research/centre-polynomial-cache-limits/frozen/work" + / "centre-encoding-campaign-20261014/lanes/circuit-interface/INTERFACE.json" +) +CERTIFICATE = ROOT / "research/exact-one-slot-gram/CERTIFICATE.json" +SELECTED = ROOT / "certificates/selected-result.json" +INTERFACE_SHA256 = "5c6c51fbffc07a683e922f17532fd90262ae9e23cc3560a696002073dd234ef3" +SELECTED_SHA256 = "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" +CERTIFICATE_SHA256 = "29e0b0d86c7fd8929ad36d9de48c2b8b55500491576dc5ac1d0b1ff076d27483" +SELECTED_KAPPA = "781451/250000000" +SECTOR = 3 +CHARACTER = 508 +ODDS = (1, 3, 5, 7) +U_INV = (2, 1, 0, 3, 6, 5, 4, 7) +U_EPS = (-1, 1, -1, 1, 1, 1, 1, 1) +V_INV = (4, 1, 6, 3, 0, 5, 2, 7) +V_EPS = (-1, 1, 1, 1, -1, 1, 1, 1) +CHI_A_SHA256 = "c4bcbd4e52f92d13f3ad451d92c9d22256e7725e4be24ee203bea1c96c129648" +CHI_B_SHA256 = "185b51cfd084f95c1dbd814b0b211ce4ab35b2d59604d7795715d65a0a4e5e65" +# Monic irreducible factors of chi_{A_1}, ascending coefficients, with multiplicity. +FACTORS = ( + (16, (0, 1)), + (1, (-14, 1)), + (1, (-12, 1)), + (6, (-4, 1)), + (14, (-2, 1)), + (14, (2, 1)), + (6, (4, 1)), + (1, (12, 1)), + (1, (14, 1)), + (2, (16, -8, -16, 0, 1)), + (2, (16, 8, -16, 0, 1)), + (1, (-32, 32, 20, -12, 1)), + (1, (-32, -32, 20, 12, 1)), +) +# Which published c=3, s=+1 sector polynomials, labelled by t, each factor divides. +SECTOR_HITS = ( + (0, 1), + (0,), + (1,), + (0,), + (0, 1), + (0, 1), + (1,), + (0,), + (1,), + (1,), + (0,), + (0,), + (1,), +) +# Square-free factors of the two Z_508 eigenspaces inside the 84-space. +FACTORS_T0 = ( + (1, (-14, 1)), + (1, (12, 1)), + (6, (-4, 1)), + (6, (2, 1)), + (8, (-2, 1)), + (8, (0, 1)), + (1, (-32, 32, 20, -12, 1)), + (2, (16, 8, -16, 0, 1)), +) +FACTORS_T1 = ( + (1, (-12, 1)), + (1, (14, 1)), + (6, (-2, 1)), + (6, (4, 1)), + (8, (0, 1)), + (8, (2, 1)), + (1, (-32, -32, 20, 12, 1)), + (2, (16, -8, -16, 0, 1)), +) +# Rational eigenvalues of A_1 and their common algebraic and geometric multiplicity. +RATIONAL_EIGENVALUES = ( + (0, 16), + (2, 14), + (-2, 14), + (4, 6), + (-4, 6), + (12, 1), + (-12, 1), + (14, 1), + (-14, 1), +) + + +def fail(message): + raise SystemExit("FAIL: " + message) + + +def expect(condition, message): + if not condition: + fail(message) + + +def sha256_bytes(data): + return hashlib.sha256(data).hexdigest() + + +def canonical(obj): + return json.dumps(obj, separators=(",", ":"), ensure_ascii=True) + + +def dot(left, right): + return bin(left & right).count("1") & 1 + + +def norm(vector): + for entry in vector: + if entry: + return tuple(entry * item for item in vector) + return vector + + +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 index in range(width): + matrix[row][index] ^= matrix[rank][index] + 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 load_query(): + raw = INTERFACE.read_bytes() + expect(sha256_bytes(raw) == INTERFACE_SHA256, "INTERFACE.json hash changed") + selected_bytes = SELECTED.read_bytes() + expect(sha256_bytes(selected_bytes) == SELECTED_SHA256, "selected-result.json bytes changed") + selected = json.loads(selected_bytes) + expect(selected["kappa"] == SELECTED_KAPPA, "selected kappa is not 781451/250000000") + certificate_bytes = CERTIFICATE.read_bytes() + expect(sha256_bytes(certificate_bytes) == CERTIFICATE_SHA256, "one-slot certificate bytes changed") + data = json.loads(raw) + 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: + expect(sum(value != 0 for value in column) == 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, 511) == 1 for port in ports), "a port label has even weight") + return columns, ports + + +def prepare(columns, ports): + port_of = {column: port for column, port in zip(columns, ports)} + lookup = {norm(column): port for column, port in port_of.items()} + 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, "the ports do not span F2^9") + coords = {address: tuple(rank_solve(basis, address)) for address in range(512)} + return port_of, lookup, basis, coords + + +def apply_linear(matrix, address): + image = 0 + for bit in range(9): + if (address >> bit) & 1: + image ^= matrix[bit] + return image + + +def operator(inv, eps, port_of, lookup, basis, coords): + mapping = {} + for column, port in port_of.items(): + image = tuple(eps[index] * column[inv[index]] for index in range(8)) + matched = lookup.get(norm(image)) + if matched is None: + return None + mapping[port] = matched + matrix = [] + for bit in range(9): + image = 0 + for index, flag in enumerate(coords[1 << bit]): + if flag: + image ^= mapping[basis[index]] + matrix.append(image) + for port, image in mapping.items(): + if apply_linear(matrix, port) != image: + return None + images = [mapping[vector] for vector in basis] + for left in range(9): + for right in range(left, 9): + if dot(basis[left], basis[right]) != dot(images[left], images[right]): + return None + return {"inv": tuple(inv), "eps": tuple(eps), "T": tuple(matrix)} + + +def compose(left, right): + inv = tuple(right["inv"][left["inv"][index]] for index in range(8)) + eps = tuple(left["eps"][index] * right["eps"][left["inv"][index]] for index in range(8)) + matrix = tuple(apply_linear(left["T"], column) for column in right["T"]) + return {"inv": inv, "eps": eps, "T": matrix} + + +def same_operator(left, right): + return left["inv"] == right["inv"] and left["eps"] == right["eps"] and left["T"] == right["T"] + + +def action_tables(element): + inv, eps, transform = element["inv"], element["eps"], element["T"] + sigma = [0] * 8 + for out_index, in_index in enumerate(inv): + sigma[in_index] = out_index + dest = [0] * 4096 + sign = [0] * 4096 + for coordinate in range(8): + image_coordinate = sigma[coordinate] + image_sign = eps[image_coordinate] + for address in range(512): + src = coordinate * 512 + address + dest[src] = image_coordinate * 512 + apply_linear(transform, address) + sign[src] = image_sign + return dest, sign + + +def translation_action(shift): + dest = [0] * 4096 + sign = [1] * 4096 + for coordinate in range(8): + for address in range(512): + dest[coordinate * 512 + address] = coordinate * 512 + (address ^ shift) + return dest, sign + + +def diagonal_action(character): + dest = list(range(4096)) + sign = [0] * 4096 + for coordinate in range(8): + for address in range(512): + sign[coordinate * 512 + address] = -1 if dot(character, address) else 1 + return dest, sign + + +def compose_actions(left, right): + left_dest, left_sign = left + right_dest, right_sign = right + dest = [0] * 4096 + sign = [0] * 4096 + for src in range(4096): + mid = right_dest[src] + dest[src] = left_dest[mid] + sign[src] = right_sign[src] * left_sign[mid] + return dest, sign + + +def action_trace(dest, sign): + return sum(sign[index] for index in range(4096) if dest[index] == index) + + +class Lattice: + """Solution space of v[dst] = sign * v[src] on Q^4096.""" + + def __init__(self): + self.parent = list(range(4096)) + self.rel = [1] * 4096 + self.dead = [False] * 4096 + + def find(self, index): + sign = 1 + seen = [] + while self.parent[index] != index: + seen.append(index) + sign *= self.rel[index] + index = self.parent[index] + accumulated = 1 + for step in reversed(seen): + accumulated = self.rel[step] * accumulated + self.rel[step] = accumulated + self.parent[step] = index + return index, sign + + def constrain(self, dst, src, sgn): + root_dst, sign_dst = self.find(dst) + root_src, sign_src = self.find(src) + if root_dst == root_src: + if sign_dst != sgn * sign_src: + self.dead[root_dst] = True + return + self.parent[root_dst] = root_src + self.rel[root_dst] = sgn * sign_src * sign_dst + if self.dead[root_dst] or self.dead[root_src]: + self.dead[root_src] = True + + def add_operator(self, dest, sign, eigenvalue): + for src in range(4096): + self.constrain(dest[src], src, sign[src] * eigenvalue) + + def basis(self): + groups = {} + for index in range(4096): + root, sign = self.find(index) + if self.dead[root]: + continue + groups.setdefault(root, []).append((index, sign)) + vectors = [] + for items in groups.values(): + items.sort() + pivot = items[0][1] + vectors.append((items[0][0], [(index, coeff * pivot) for index, coeff in items])) + vectors.sort() + return vectors + + +def column_table(columns, ports, sector): + raw = [{} for _ in range(4096)] + for port, root in zip(ports, columns): + support = [index for index in range(8) if root[index]] + translating = dot(port, sector) == 1 + for coordinate in support: + weight = root[coordinate] + for address in range(512): + src = coordinate * 512 + address + if translating: + target = address ^ port + parity = 1 + else: + target = address + parity = -1 if dot(port, address) else 1 + bucket = raw[src] + term = weight * parity + for out_coordinate in support: + index = out_coordinate * 512 + target + bucket[index] = bucket.get(index, 0) + root[out_coordinate] * term + return [{index: value for index, value in column.items() if value} for column in raw] + + +def literal_image(items, columns, ports, sector): + image = {} + for port, root in zip(ports, columns): + support = [index for index in range(8) if root[index]] + buckets = {} + for index, coeff in items: + coordinate, address = divmod(index, 512) + if root[coordinate]: + buckets[address] = buckets.get(address, 0) + root[coordinate] * coeff + translating = dot(port, sector) == 1 + for address, acc in buckets.items(): + if translating: + target = address ^ port + parity = 1 + else: + target = address + parity = -1 if dot(port, address) else 1 + acc *= parity + for coordinate in support: + index = coordinate * 512 + target + image[index] = image.get(index, 0) + root[coordinate] * acc + return {index: value for index, value in image.items() if value} + + +def column_image(columns_b, items): + image = {} + for index, coeff in items: + for target, value in columns_b[index].items(): + image[target] = image.get(target, 0) + coeff * value + return {index: value for index, value in image.items() if value} + + +def operator_trace(columns_b, dest, sign): + total = 0 + for src in range(4096): + value = columns_b[dest[src]].get(src, 0) + if value: + total += sign[src] * value + return total + + +def restriction_matrix(columns_b, columns, ports, vectors, sector): + members = [items for _root, items in vectors] + owners = {} + for component, items in enumerate(members): + for index, coeff in items: + owners[index] = (component, coeff) + matrix = [[0] * len(vectors) for _ in vectors] + sizes = [len(items) for items in members] + for column, items in enumerate(members): + by_columns = column_image(columns_b, items) + by_literal = literal_image(items, columns, ports, sector) + expect(by_columns == by_literal, "the two actions of B disagree on a basis vector") + alphas = {} + for index, value in by_columns.items(): + info = owners.get(index) + expect(info is not None, "B sends a basis vector outside the space") + component, coeff = info + alpha = value * coeff + previous = alphas.get(component) + expect(previous is None or previous == alpha, "B image is not constant on a component") + alphas[component] = alpha + for component, alpha in alphas.items(): + matrix[component][column] = alpha + for left in range(len(vectors)): + for right in range(left + 1, len(vectors)): + expect( + sizes[left] * matrix[left][right] == sizes[right] * matrix[right][left], + "the Gram identity size_r M_rs = size_s M_sr failed", + ) + return matrix, sizes + + +def subspace_preserved(columns_b, vectors): + owners = set() + for _root, items in vectors: + for index, _coeff in items: + owners.add(index) + for _root, items in vectors: + for index in column_image(columns_b, items): + if index not in owners: + return False + return True + + +def is_prime(number): + if number < 2: + return False + if number % 2 == 0: + return number == 2 + divisor = 3 + while divisor * divisor <= number: + if number % divisor == 0: + return False + divisor += 2 + return True + + +def primes_past(limit): + modulus = 1 + primes = [] + candidate = 1_000_003 + while modulus <= limit: + if is_prime(candidate): + primes.append(candidate) + modulus *= candidate + candidate += 2 + return primes, modulus + + +def charpoly_mod(matrix, prime): + size = len(matrix) + hess = [[entry % prime for entry in row] for row in matrix] + for column in range(size - 2): + pivot = None + for row in range(column + 1, size): + if hess[row][column]: + pivot = row + break + if pivot is None: + continue + if pivot != column + 1: + hess[column + 1], hess[pivot] = hess[pivot], hess[column + 1] + for row in hess: + row[column + 1], row[pivot] = row[pivot], row[column + 1] + inverse = pow(hess[column + 1][column], -1, prime) + for row in range(column + 2, size): + factor = hess[row][column] + if not factor: + continue + factor = factor * inverse % prime + for index in range(column, size): + hess[row][index] = (hess[row][index] - factor * hess[column + 1][index]) % prime + for host in hess: + host[column + 1] = (host[column + 1] + factor * host[row]) % prime + minors = [[1], [(prime - hess[0][0]) % prime, 1]] + for end in range(1, size): + previous = minors[end] + diagonal = hess[end][end] + output = [0] * (end + 2) + for index, coefficient in enumerate(previous): + output[index + 1] = coefficient + output[index] = (output[index] - diagonal * coefficient) % prime + product = 1 + for start in range(end - 1, -1, -1): + product = product * hess[start + 1][start] % prime + if product == 0: + break + scale = hess[start][end] * product % prime + if scale == 0: + continue + for index, coefficient in enumerate(minors[start]): + output[index] = (output[index] - scale * coefficient) % prime + expect(output[-1] % prime == 1, "Hessenberg characteristic polynomial is not monic") + minors.append([value % prime for value in output]) + return minors[size] + + +def det_mod(matrix, prime): + size = len(matrix) + work = [[entry % prime for entry in row] for row in matrix] + determinant = 1 + for column in range(size): + pivot = None + for row in range(column, size): + if work[row][column]: + pivot = row + break + if pivot is None: + return 0 + if pivot != column: + work[column], work[pivot] = work[pivot], work[column] + determinant = (-determinant) % prime + determinant = determinant * work[column][column] % prime + inverse = pow(work[column][column], -1, prime) + for row in range(column + 1, size): + factor = work[row][column] + if not factor: + continue + factor = factor * inverse % prime + for index in range(column, size): + work[row][index] = (work[row][index] - factor * work[column][index]) % prime + return determinant + + +def crt_signed(residues, primes): + value = 0 + modulus = 1 + for residue, prime in zip(residues, primes): + increment = ((residue - value) % prime) * pow(modulus % prime, -1, prime) % prime + value += increment * modulus + modulus *= prime + if value > modulus // 2: + value -= modulus + return value + + +def coeff_bound(size, row_sum): + best = 1 + binomial = 1 + power = 1 + for degree in range(size + 1): + term = binomial * power + if term > best: + best = term + if degree < size: + binomial = binomial * (size - degree) // (degree + 1) + power *= row_sum + return best + + +def charpoly(matrix): + size = len(matrix) + row_sum = max(sum(abs(entry) for entry in row) for row in matrix) + bound = coeff_bound(size, row_sum) + primes, modulus = primes_past(2 * bound) + expect(modulus > 2 * bound, "CRT modulus does not exceed the coefficient bound") + residues = [[] for _ in range(size + 1)] + for prime in primes: + polynomial = charpoly_mod(matrix, prime) + for index, coefficient in enumerate(polynomial): + residues[index].append(coefficient) + coefficients = [crt_signed(residues[index], primes) for index in range(size + 1)] + expect(coefficients[-1] == 1, "characteristic polynomial of B is not monic") + expect(sum(matrix[index][index] for index in range(size)) == -coefficients[-2], "trace disagrees with chi_B") + for point in (0, 1, 2, 3, 5): + work = [[(-entry) % primes[0] for entry in row] for row in matrix] + for index in range(size): + work[index][index] = (work[index][index] + point) % primes[0] + evaluated = 0 + power = 1 + for coefficient in coefficients: + evaluated = (evaluated + coefficient * power) % primes[0] + power = power * point % primes[0] + expect(det_mod(work, primes[0]) == evaluated, "chi_B disagrees with det(tI-M) at " + str(point)) + for index, coefficient in enumerate(coefficients): + expect(abs(coefficient) <= bound, "a coefficient exceeds the Gershgorin binomial bound") + expect(coefficient % (4 ** (size - index)) == 0, "chi_A is not an integer polynomial") + coefficients_a = [coefficient // (4 ** (size - index)) for index, coefficient in enumerate(coefficients)] + return coefficients, coefficients_a + + +def poly_mul(left, right): + output = [0] * (len(left) + len(right) - 1) + for i, left_coeff in enumerate(left): + for j, right_coeff in enumerate(right): + output[i + j] += left_coeff * right_coeff + return output + + +def poly_pow(base, exponent): + result = [1] + while exponent: + if exponent & 1: + result = poly_mul(result, base) + exponent >>= 1 + if exponent: + base = poly_mul(base, base) + return result + + +def product_factors(factors): + value = [1] + for multiplicity, coefficients in factors: + value = poly_mul(value, poly_pow(list(coefficients), multiplicity)) + return value + + +def scale_to_b(coefficients): + degree = len(coefficients) - 1 + return [coefficient * 4 ** (degree - index) for index, coefficient in enumerate(coefficients)] + + +def monic_divides(divisor, target): + work = list(target) + degree = len(divisor) - 1 + while len(work) > 1 and work[-1] == 0: + work.pop() + while len(work) - 1 >= degree and not (len(work) == 1 and work[0] == 0): + shift = len(work) - 1 - degree + lead = work[-1] + for index, coefficient in enumerate(divisor): + work[shift + index] -= lead * coefficient + while len(work) > 1 and work[-1] == 0: + work.pop() + return work == [0] or work == [] + + +def divisor_pairs(constant): + pairs = [] + seen = set() + value = abs(constant) + divisor = 1 + while divisor * divisor <= value: + if value % divisor == 0: + for left in (divisor, -divisor): + for pair in ((left, constant // left), (constant // left, left)): + if pair not in seen and pair[0] * pair[1] == constant: + seen.add(pair) + pairs.append(pair) + divisor += 1 + return pairs + + +def quadratic_factor(coefficients): + """Return an integer quadratic factorization, or None. Degree 4 only.""" + expect(len(coefficients) == 5 and coefficients[-1] == 1, "quadratic search expected a monic quartic") + constant, linear, quadratic, cubic, _lead = coefficients + if constant == 0: + return (0, 1), (0, 0, 1) + for root, _other in divisor_pairs(constant): + if constant + linear * root + quadratic * root ** 2 + cubic * root ** 3 + root ** 4 == 0: + return (root, 1), None + for left, right in divisor_pairs(constant): + if right != left: + numerator = linear - left * cubic + denominator = right - left + if numerator % denominator == 0: + first = numerator // denominator + second = cubic - first + if left + right + first * second == quadratic: + return (left, first, 1), (right, second, 1) + continue + if left * cubic != linear: + continue + discriminant = cubic * cubic - 4 * (quadratic - 2 * left) + if discriminant < 0: + continue + root = int(discriminant ** 0.5) + while (root + 1) * (root + 1) <= discriminant: + root += 1 + while root * root > discriminant: + root -= 1 + if root * root != discriminant: + continue + for sign in (1, -1): + if (cubic + sign * root) % 2 == 0: + return (left, (cubic + sign * root) // 2, 1), (left, cubic - (cubic + sign * root) // 2, 1) + return None + + +def prove_irreducible(coefficients): + degree = len(coefficients) - 1 + expect(coefficients[-1] == 1, "a factor is not monic") + if degree == 1: + return + expect(degree == 4, "a factor has degree other than 1 or 4") + expect(quadratic_factor(coefficients) is None, "a degree-4 factor is reducible over Z") + + +def matmul(left, right): + size = len(left) + return [ + [sum(left[row][index] * right[index][column] for index in range(size)) for column in range(size)] + for row in range(size) + ] + + +def apply_polynomial(matrix, coefficients): + size = len(matrix) + value = [[0] * size for _ in range(size)] + for coefficient in reversed(coefficients): + value = matmul(value, matrix) + for index in range(size): + value[index][index] += coefficient + return value + + +def is_zero(matrix): + return all(entry == 0 for row in matrix for entry in row) + + +def kernel_vectors(matrix): + """Integer kernel basis. Free coordinates form an identity submatrix.""" + size = len(matrix) + work = [[Fraction(entry) for entry in row] for row in matrix] + pivot_of_row = [] + rank = 0 + for column in range(size): + pivot = None + for row in range(rank, size): + if work[row][column] != 0: + pivot = row + break + if pivot is None: + continue + work[rank], work[pivot] = work[pivot], work[rank] + inverse = work[rank][column] + for row in range(size): + if row == rank or work[row][column] == 0: + continue + factor = work[row][column] / inverse + for index in range(column, size): + work[row][index] -= factor * work[rank][index] + pivot_of_row.append(column) + rank += 1 + pivots = set(pivot_of_row) + vectors = [] + free = [column for column in range(size) if column not in pivots] + for chosen in free: + raw = [Fraction(0)] * size + raw[chosen] = Fraction(1) + for row, column in enumerate(pivot_of_row): + raw[column] = -work[row][chosen] / work[row][column] + denominator = 1 + for value in raw: + denominator = denominator * value.denominator // math_gcd(denominator, value.denominator) + vectors.append([int(value * denominator) for value in raw]) + return free, vectors + + +def math_gcd(left, right): + while right: + left, right = right, left % right + return left + + +def fixed_by(dest, sign, items, eigenvalue): + values = {index: coeff for index, coeff in items} + for index, coeff in items: + image = dest[index] + if values.get(image, 0) != sign[index] * eigenvalue * coeff: + return False + return True + + +def build_space(actions, extras): + lattice = Lattice() + for dest, sign in actions: + lattice.add_operator(dest, sign, 1) + for dest, sign, eigenvalue in extras: + lattice.add_operator(dest, sign, eigenvalue) + return lattice.basis() + + +def descending(coefficients): + parts = [] + for power, coefficient in reversed(list(enumerate(coefficients))): + if coefficient == 0: + continue + if power == 0: + body = str(abs(coefficient)) + else: + letter = "x" if power == 1 else "x^" + str(power) + body = letter if abs(coefficient) == 1 else str(abs(coefficient)) + letter + if not parts: + parts.append(body if coefficient > 0 else "-" + body) + else: + parts.append(("+ " if coefficient > 0 else "- ") + body) + return " ".join(parts) if parts else "0" + + +def main(): + dump = "--dump-evidence" in sys.argv + columns, ports = load_query() + port_of, lookup, port_basis, coords = prepare(columns, ports) + identity = operator(tuple(range(8)), (1,) * 8, port_of, lookup, port_basis, coords) + expect(identity is not None and identity["T"] == tuple(1 << bit for bit in range(9)), "identity is not a symmetry") + group = [] + for odds in range(16): + eps = [1] * 8 + for index, coordinate in enumerate(ODDS): + if (odds >> index) & 1: + eps[coordinate] = -1 + built = operator(tuple(range(8)), tuple(eps), port_of, lookup, port_basis, coords) + expect(built is not None, "a positive-even sign is not a symmetry of the query") + expect(apply_linear(built["T"], SECTOR) == SECTOR, "H moves sector 3") + group.append(built) + expect(len(group) == 16, "H does not have order 16") + first = operator(U_INV, U_EPS, port_of, lookup, port_basis, coords) + second = operator(V_INV, V_EPS, port_of, lookup, port_basis, coords) + expect(first is not None and second is not None, "u or v is not a symmetry") + expect(same_operator(compose(first, first), identity), "u is not an involution") + expect(same_operator(compose(second, second), identity), "v is not an involution") + expect(same_operator(compose(first, second), compose(second, first)), "u and v do not commute") + expect(apply_linear(first["T"], SECTOR) == SECTOR and apply_linear(second["T"], SECTOR) == SECTOR, "the pair moves sector 3") + product = compose(first, second) + actors = [] + for element in group: + for extra in (identity, first, second, product): + actors.append(compose(extra, element)) + expect(len({(item["inv"], item["eps"], item["T"]) for item in actors}) == 64, "the joint group does not have order 64") + actions = [action_tables(element) for element in actors] + x_action = translation_action(SECTOR) + z_action = diagonal_action(CHARACTER) + expect(compose_actions(x_action, x_action) == (list(range(4096)), [1] * 4096), "X_3 is not an involution") + for dest, sign in actions: + expect(compose_actions(x_action, (dest, sign)) == compose_actions((dest, sign), x_action), "X_3 does not commute with the joint group") + expect(compose_actions(z_action, (dest, sign)) == compose_actions((dest, sign), z_action), "Z_508 does not commute with the joint group") + expect((dest, sign) != x_action, "X_3 is already a signed permutation in the joint group") + extended = actions + [compose_actions(x_action, action) for action in actions] + expect(len(extended) == 128, "the group generated by H, u, v and X_3 does not have order 128") + trace_sum = sum(action_trace(dest, sign) for dest, sign in extended) + expect(trace_sum % 128 == 0 and trace_sum // 128 == 84, "the projector trace is not 84") + x_trace = sum(action_trace(*compose_actions(x_action, action)) for action in actions) + expect(x_trace % 64 == 0 and x_trace // 64 == -48, "the trace of X_3 on the 216-space is not -48") + + joint_vectors = build_space(actions, []) + plus_vectors = build_space(actions, [(x_action[0], x_action[1], 1)]) + minus_vectors = build_space(actions, [(x_action[0], x_action[1], -1)]) + t0_vectors = build_space(actions, [(x_action[0], x_action[1], 1), (z_action[0], z_action[1], 1)]) + t1_vectors = build_space(actions, [(x_action[0], x_action[1], 1), (z_action[0], z_action[1], -1)]) + other_joint = build_space( + [action_tables(compose(extra, element)) for element in group for extra in (identity, first)], + [(action_tables(second)[0], action_tables(second)[1], -1), (x_action[0], x_action[1], 1)], + ) + expect(len(joint_vectors) == 216, "the trivial (+1,+1) basis is not 216-dimensional") + expect(len(plus_vectors) == 84 and len(minus_vectors) == 132, "X_3 does not split the 216-space as 84+132") + expect(len(t0_vectors) == 42 and len(t1_vectors) == 42, "Z_508 does not split the 84-space as 42+42") + expect(len(other_joint) == 116, "the (+1,-1) X_3=+1 space does not have dimension 116") + sizes = [len(items) for _root, items in plus_vectors] + expect(set(sizes) <= {8, 32, 64} and set(sizes) == {8, 32, 64}, "basis support sizes are not 8, 32 and 64") + + columns_b = column_table(columns, ports, SECTOR) + predicted = sum(operator_trace(columns_b, dest, sign) for dest, sign in extended) + expect(predicted % 128 == 0, "the trace of B is not integral on the projector") + matrix, _matrix_sizes = restriction_matrix(columns_b, columns, ports, plus_vectors, SECTOR) + matrix0, _sizes0 = restriction_matrix(columns_b, columns, ports, t0_vectors, SECTOR) + matrix1, _sizes1 = restriction_matrix(columns_b, columns, ports, t1_vectors, SECTOR) + expect(sum(matrix[index][index] for index in range(84)) == predicted // 128 == 0, "matrix trace is not the trace formula value 0") + expect(sum(matrix0[index][index] for index in range(42)) == 168, "t=0 trace is not 168") + expect(sum(matrix1[index][index] for index in range(42)) == -168, "t=1 trace is not -168") + entries = [entry for row in matrix for entry in row] + expect(min(entries) == -28 and max(entries) == 28, "matrix entries are not exactly the range -28..28") + + coefficients_b, coefficients_a = charpoly(matrix) + coefficients_b0, coefficients_a0 = charpoly(matrix0) + coefficients_b1, coefficients_a1 = charpoly(matrix1) + expect(poly_mul(coefficients_b0, coefficients_b1) == coefficients_b, "the sector polynomials do not multiply to chi_B") + expect(product_factors(FACTORS) == coefficients_a, "the pinned factors do not multiply to chi_A") + expect(product_factors(FACTORS_T0) == coefficients_a0, "the t=0 factors do not multiply to that characteristic polynomial") + expect(product_factors(FACTORS_T1) == coefficients_a1, "the t=1 factors do not multiply to that characteristic polynomial") + expect(sha256_bytes(canonical(coefficients_a).encode()) == CHI_A_SHA256, "chi_A SHA256 changed") + expect(sha256_bytes(canonical(coefficients_b).encode()) == CHI_B_SHA256, "chi_B SHA256 changed") + for multiplicity, coefficients in FACTORS: + prove_irreducible(list(coefficients)) + expect(multiplicity > 0, "a factor multiplicity is not positive") + expect(quadratic_factor((1, 0, 2, 0, 1)) is not None, "the irreducibility test accepted (x^2+1)^2") + + certificate = json.loads(CERTIFICATE.read_bytes()) + expect(certificate["source_sha256"] == INTERFACE_SHA256, "published one-slot certificate names a different query") + expect(certificate["operator"] == "B=4*A_1", "published certificate is not the integer operator B") + sectors = {} + for sector in certificate["sectors"]: + if sector["c"] == SECTOR and sector["s"] == 1: + sectors[sector["t"]] = [int(value) for value in sector["coefficients"]] + expect(set(sectors) == {0, 1}, "the c=3 s=+1 sector polynomials are not both present") + expect(len(sectors[0]) == 127 and len(sectors[1]) == 127, "a c=3 s=+1 sector polynomial does not have degree 126") + for (multiplicity, coefficients), hits in zip(FACTORS, SECTOR_HITS): + scaled = scale_to_b(coefficients) + found = tuple(key for key in (0, 1) if monic_divides(scaled, sectors[key])) + expect(found == hits, "sector divisibility of a factor changed") + expect(hits, "a factor divides neither published c=3 s=+1 sector polynomial") + expect(multiplicity >= 1, "multiplicity dropped out of the sector comparison") + + distinct = tuple((1, coefficients) for _multiplicity, coefficients in FACTORS) + annihilator = apply_polynomial(matrix, product_factors(tuple((1, scale_to_b(coefficients)) for _mult, coefficients in distinct))) + expect(is_zero(annihilator), "the degree-25 square-free polynomial does not annihilate B") + for sector_matrix, sector_factors in ((matrix0, FACTORS_T0), (matrix1, FACTORS_T1)): + distinct_sector = [] + seen = set() + for _multiplicity, coefficients in sector_factors: + if coefficients not in seen: + seen.add(coefficients) + distinct_sector.append((1, scale_to_b(coefficients))) + expect(is_zero(apply_polynomial(sector_matrix, product_factors(tuple(distinct_sector)))), "a sector square-free polynomial does not annihilate") + + accounted = 0 + for eigenvalue, multiplicity in RATIONAL_EIGENVALUES: + shifted = [row[:] for row in matrix] + for index in range(84): + shifted[index][index] -= 4 * eigenvalue + free, vectors = kernel_vectors(shifted) + expect(len(vectors) == multiplicity, "geometric multiplicity disagrees with the characteristic polynomial at " + str(eigenvalue)) + for vector in vectors: + image = [ + sum(shifted[row][column] * vector[column] for column in range(84)) + for row in range(84) + ] + expect(image == [0] * 84, "a claimed kernel vector is not in the kernel") + for position, vector in enumerate(vectors): + expect(vector[free[position]] != 0, "a kernel vector vanishes on its free coordinate") + for other, column in enumerate(free): + expect(vector[column] == (vector[free[position]] if other == position else 0), "kernel vectors are dependent on the free coordinates") + accounted += multiplicity + expect(accounted == 60, "the rational eigenvalues do not account for 60 dimensions") + + basis_payload = { + "index": "coordinate*512+address", + "eigenvalues": {"H": 1, "u": 1, "v": 1, "X_3": 1}, + "roots": [root for root, _items in plus_vectors], + "vectors": [[[index, coeff] for index, coeff in items] for _root, items in plus_vectors], + } + matrix_payload = {"rows": matrix} + basis_path = PACKAGE / "evidence" / "basis.json" + matrix_path = PACKAGE / "evidence" / "matrix.json" + if dump: + basis_path.parent.mkdir(parents=True, exist_ok=True) + basis_path.write_text(canonical(basis_payload) + "\n") + matrix_path.write_text(canonical(matrix_payload) + "\n") + else: + expect(json.loads(basis_path.read_text()) == basis_payload, "pinned basis does not match the recomputation") + expect(json.loads(matrix_path.read_text()) == matrix_payload, "pinned matrix does not match the recomputation") + + transposition = operator((1, 0, 2, 3, 4, 5, 6, 7), (1,) * 8, port_of, lookup, port_basis, coords) + expect(transposition is None, "the coordinate transposition (0 1) was accepted as a symmetry") + wrong_sector = column_table(columns, ports, 1) + expect(not subspace_preserved(wrong_sector, plus_vectors), "the c=1 block operator preserves this c=3 subspace") + shifted_once = translation_action(1) + wrong_translation = build_space(actions, [(shifted_once[0], shifted_once[1], 1)]) + expect(len(wrong_translation) != 84, "translation by 1 still produced an 84-dimensional space") + broken = Lattice() + for dest, sign in actions[1:]: + broken.add_operator(dest, sign, 1) + flipped = list(actions[0][1]) + flipped[0] *= -1 + broken.add_operator(actions[0][0], flipped, 1) + broken.add_operator(x_action[0], x_action[1], 1) + expect(len(broken.basis()) != 84, "flipping one group sign still produced dimension 84") + corrupted = [row[:] for row in matrix] + corrupted[0][0] += 1 + expect(charpoly_mod(corrupted, 1000003) != charpoly_mod(matrix, 1000003), "changing a matrix entry preserved the characteristic polynomial") + expect(product_factors(FACTORS[:-1]) != coefficients_a, "dropping a factor still multiplied to chi_A") + linked = None + for dest, sign in actions + [x_action]: + for _root, items in plus_vectors: + values = {index: coeff for index, coeff in items} + for index, _coeff in items: + if dest[index] != index and dest[index] in values: + linked = (dest, sign, items, index) + break + if linked: + break + if linked: + break + expect(linked is not None, "no operator links two basis coordinates; the sign control is vacuous") + dest, sign, items, index = linked + flipped_items = [(item, -coeff if item == index else coeff) for item, coeff in items] + expect(not fixed_by(dest, sign, flipped_items, 1), "a sign error in a basis vector was still fixed") + + print("PASS_C3_X3_PLUS_CHARPOLY") + print("selected kappa", SELECTED_KAPPA) + print("X_3 trace -48 on the 216-space; dimensions 84 and 132; Z_508 splits 42+42") + print("chi_A SHA256", CHI_A_SHA256) + print("chi_B SHA256", CHI_B_SHA256) + print("minimal polynomial degree 25") + for multiplicity, coefficients in FACTORS: + print("factor", multiplicity, descending(coefficients)) + + +if __name__ == "__main__": + main()