diff --git a/research/c3-odd-sign-trace-slot/PROOF.md b/research/c3-odd-sign-trace-slot/PROOF.md new file mode 100644 index 0000000000..d7130889d9 --- /dev/null +++ b/research/c3-odd-sign-trace-slot/PROOF.md @@ -0,0 +1,128 @@ +# An odd minus on u keeps the trace -48 on (+1, +1) + +This note answers the second open question of the sector-3 payload-involution +certificate: whether one other cross-coset pair, with a different odd sign, +moves the trace `-48` of `X_3` onto another `(u, v)` eigenvalue. The selected +conditional kappa stays `781451/250000000`. Nothing here is a characteristic +polynomial, a basis, or a census of all 3072 cross-coset pairs. + +The claim is a **proof**. The joint trace formula is an identity for commuting +involutions. The 512 addresses, the 16 odd signs, and the 16 characters below +are finite sets, and the verifier evaluates the identities on every element of +each set. That evaluation is exhaustive on those sets. It is not a heuristic +search, and it is not a proof that an arbitrary change of mask keeps the trace. + +## The pair + +The input is the pinned 8-by-112 query, SHA256 +`5c6c51fbffc07a683e922f17532fd90262ae9e23cc3560a696002073dd234ef3`. +Bell block `c=3` and the payload involution `X_3`, translation of the address +by 3, are the operators of the degree-881 certificate. The sign group `H` is +the order-16 group of diagonal signs supported on the odd coordinates +`{1, 3, 5, 7}` and positive on the even coordinates. Its characters are the +16 homomorphisms `F_2^4 → {±1}`, indexed by coordinates `(1, 3, 5, 7)`. + +The explicit pair from the c=3 sign-split certificate is + +| name | permutation | minus signs | +|---|---|---| +| `u` | `(0 2)(4 6)` | coordinates 0 and 2 | +| `v` | `(0 4)(2 6)` | coordinates 0 and 4 | +| `uv` | `(0 6)(2 4)` | coordinates 0 and 6 | + +The mask of `u` is 5 and the mask of `v` is 17. These even signs are one legal +opposite-cycle pattern: each 2-cycle is uniformly signed, and the two cycles +carry opposite signs. The odd signs of this pair are all positive. On the +trivial character, `X_3` has joint traces `-48, 16, 16, 16` in the eigenvalue +order `((+1,+1), (+1,-1), (-1,+1), (-1,-1))`. The verifier recomputes that row, +and the other published weight rows, before any sign is changed. + +## One odd minus + +Let `D` be the diagonal sign that is `-1` only on coordinate 1. Set +`u' = u ∘ D`, with `D` applied first. The permutation of `u'` is still +`(0 2)(4 6)`. Its minus signs are coordinates 0, 1, and 2, so the mask is 7. +The product `u' v` is still `(0 6)(2 4)`, now with mask 67. Both operators are +involutions, they commute, they commute with every element of `H`, they fix +sector 3, and `X_3` commutes with every element of the group they generate. +The group is the same set of 64 signed permutations as the group generated by +the unvaried pair and `H`. In particular `u'` lies in the original coset `uH`. + +The joint trace on the character `χ` and the eigenvalues `(ε, δ)` is + + tr(X_3 P) + = (1/64) sum_{h in H} χ(h) + [tr(X_3 h) + ε tr(X_3 u' h) + δ tr(X_3 v h) + εδ tr(X_3 u' v h)]. + +As `h` runs through `H`, so does `Dh`. For the trivial character every +coefficient `χ(h)` equals `+1`, and `{u' h : h in H}` equals `{u h : h in H}` +as sets of 16 operators. The same holds for the product coset, because `D` +commutes with `v`. The four unweighted sums are therefore the sums already +computed for `(u, v)`. The trivial-character traces stay + +| `(u', v)` eigenvalue | dimension | trace of `X_3` | +|---|---:|---:| +| `(+1, +1)` | 216 | -48 | +| `(+1, -1)` | 216 | 16 | +| `(-1, +1)` | 216 | 16 | +| `(-1, -1)` | 216 | 16 | + +The value `-48` remains the trace on the eigenvalue `(+1, +1)`. The +`+1` eigenspace of `X_3` on that 216-dimensional space still has dimension +`(216 + (-48))/2 = 84`, and the `-1` eigenspace still has dimension 132. +Those dimensions are the same arithmetic as in the unvaried pair. This package +does not list a basis of either space. + +The sign change is visible on another character. On the weight-1 character +that is `-1` on coordinate 1 and `+1` on coordinates 3, 5, and 7, the same +reindexing multiplies the `u`-eigenvalue by `χ(D) = -1`. The traces move from +`(36, -12, -12, -12)` to `(-12, -12, 36, -12)`, and the dimension 180 moves +from `(+1, +1)` to `(-1, +1)`. The value `-48` does not occur among those four +traces. The weight-1 character that is `-1` only on coordinate 3 is `+1` on +`D`, and its traces stay `(36, -12, -12, -12)`. + +The coordinate trace of `u'` is 2, while the coordinate trace of `u` is 4, so +`u'` is not the same operator as `u` on the whole block. The agreement on the +trivial character is the character average, not an unchanged matrix. + +## Every odd sign on this u + +The same identity applies to every diagonal sign supported on +`{1, 3, 5, 7}`. There are `2^4 = 16` such signs: one for each subset. The +empty subset is the unvaried pair. The other 15 are the odd-sign patterns on +this `u`, with `v` held at mask 17 and with the even minus signs held on +coordinates 0 and 2. Each pattern preserves the permutation `(0 2)(4 6)`, +keeps the product permutation `(0 6)(2 4)`, and uses the same 64 operators. +On the trivial character, all 16 patterns have `X_3` traces +`-48, 16, 16, 16` in the same eigenvalue order. For every character `χ`, the +traces and dimensions equal the unvaried traces and dimensions at eigenvalue +`(ε χ(D), δ)`. + +That is the complete list of odd signs that can be added to this `u` without +changing its even signs. The verifier checks the signed-permutation identity, +the fresh address trace of every element, and the joint formula, for every +pattern and every character. + +## What is not claimed + +The argument uses this query, Bell block 3, the operator `X_3`, the group +`H`, the permutations of the explicit pair, and odd signs added to `u` only. +It does not change the mask of `v`. It does not evaluate the other legal +even-cycle pattern on the same permutation, the pattern with minus signs on +coordinates 4 and 6. Flipping the sign on the single even coordinate 0 is a +different operation: that signed permutation still preserves the query, and +it sends sector 3 to 470, so it is not an endomorphism of this block. + +The degree-16 polynomial of a weight-4 summand, and the question of whether a +nontrivial odd-sign pattern splits that polynomial, are untouched. The +characteristic polynomial of the 84-dimensional `X_3 = +1` subspace is +untouched. No trace of `Z_508` was recomputed. A trace that stays equal to +`-48` on one joint space does not say that every cross-coset pair has this +trace, and it does not say that no other mask can move it. The selected +conditional kappa is unchanged. + +The rejection controls are part of the verifier, not part of the theorem. The +identity trace on the same 216-space is 216. Dropping one sign whose +contribution to the `(+1, +1)` numerator is nonzero does not reproduce `-48`. +Translation by 1 does not commute with the mask-7 representative. The +coordinate transposition `(0 1)` is not a symmetry of the query. diff --git a/research/c3-odd-sign-trace-slot/README.md b/research/c3-odd-sign-trace-slot/README.md new file mode 100644 index 0000000000..3205f6f3fb --- /dev/null +++ b/research/c3-odd-sign-trace-slot/README.md @@ -0,0 +1,126 @@ +# An odd minus on u keeps the X_3 trace -48 + +Prepared by unpaidmoon with substantial Cursor Grok assistance. Apache-2.0. + +On the explicit c=3 pair from the sign-split certificate, `X_3` has trace +`-48` on the trivial `(+1, +1)` joint space. Adding the minus sign on +coordinate 1 to `u`, and leaving `v` and the even signs unchanged, keeps that +trace on the eigenvalue `(+1, +1)`. The same holds for every odd sign added +to this `u`. The selected conditional kappa stays `781451/250000000`. +[PROOF.md](PROOF.md) separates the trace-formula proof from the facts that +are not claimed. + +## Result + +The live input is the query pinned in [SOURCES.json](SOURCES.json), SHA256 +`5c6c51fbffc07a683e922f17532fd90262ae9e23cc3560a696002073dd234ef3`. +The unvaried pair is + + u = (0 2)(4 6) with minus signs on coordinates 0 and 2, + v = (0 4)(2 6) with minus signs on coordinates 0 and 4. + +Its product is `(0 6)(2 4)` with mask 65. The assigned variation is the +composition of `u` with the diagonal sign on coordinate 1. The new mask is 7, +the product permutation is unchanged, and the product mask is 67. + +On the trivial character, the four joint traces of `X_3` remain +`-48, 16, 16, 16` for eigenvalues +`(+1,+1), (+1,-1), (-1,+1), (-1,-1)`. The value `-48` remains on +`(+1, +1)`. That space still has dimension 216, so the `X_3` eigenvalues +there are still dimensions 84 and 132. The same four traces occur for all 16 +diagonal signs supported on `{1, 3, 5, 7}`, with this `v` and these even +signs held fixed. The verifier enumerates those 16 signs, the 16 characters +of `H`, and all 512 addresses. + +The sign change moves a different trace. On the weight-1 character that is +`-1` on coordinate 1, the trace 36 and the dimension 180 move from +`(+1, +1)` to `(-1, +1)`. The value `-48` does not occur on that character. +The weight-1 character supported on coordinate 3 keeps the unvaried row +`(36, -12, -12, -12)`. + +This is a proof. The address counts are exhaustive on 512 elements, once by +enumeration and once by an affine solve, and the two counts agree. The odd +signs are all `2^4` subsets of the four odd coordinates. It is not a stopped +search, and it is not a claim about every cross-coset pair. + +## Scope + +Catalogue card `formal-interface-lemma` asks for a formal interface binding. +The live question is open question 2 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). +The first step named there is to repeat the trace with one odd minus sign +added to `u`. The masks and the unvaried pair come from +[PR #6965](https://github.com/CrocSwap/integer-mult-bounds/pull/6965). + +This package does not redo the payload-involution split. It does not compute +the characteristic polynomial of the 84-dimensional subspace, and it does not +factor the degree-16 weight-4 polynomial of +[PR #7021](https://github.com/CrocSwap/integer-mult-bounds/pull/7021). +The mask of `v` stays 17. The other legal even-cycle pattern, minus signs on +coordinates 4 and 6, is not evaluated. + +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-odd-sign-trace-slot/verify.py +python3 -B -O research/c3-odd-sign-trace-slot/verify.py +python3 -B scripts/research_package.py --package research/c3-odd-sign-trace-slot --check-only +``` + +The direct marker is `PASS_C3_ODD_SIGN_TRACE_SLOT`. Acceptance uses explicit +checks, so `-O` does not skip them. On the measured host the direct run takes +about two seconds. No Lean, Docker, degree-881 coefficient replay, or +selected cold replay was run. + +## Overlap + +`scripts/find_overlap.py` was refreshed on 2026-11-10 against upstream +`17469fff78c22941280f04d39dc5a1faee09c840`. Coverage: local notes 10178 of +10178 HEAD paths, complete; 339 open PRs, pagination complete, fetched +2026-11-10T10:28:46Z; 7013 discussion records, pagination complete, fetched +2026-11-10T10:29:46Z. Closed PRs were searched through local READMEs, task +metadata and the ledger only. The search terms were `trace -48`, +`odd minus`, and `cross-coset`. + +The matches are the predecessor statements and one unrelated use of the words +"cross-coset". PR #7020 records the trace `-48` and leaves other cross-coset +sign patterns unevaluated. PR #7021 asks whether a nontrivial odd-sign pattern +splits a degree-16 weight-4 polynomial; that polynomial is not this trace. +No open PR body reports the joint trace of `X_3` after an odd sign is added +to this pair. This search is not a novelty certificate. + +## Open next questions + +The structured list is in [TASK.json](TASK.json). + +- One odd minus added to `v`, with the mask of `u` held at 5, was not + evaluated. The reindexing above uses a sign added to `u`. The smallest + check is the same joint formula with the minus on coordinate 1 added to + `v` instead. +- The other legal even-cycle pattern on `(0 2)(4 6)`, with minus signs on + coordinates 4 and 6 and no odd minuses, was not evaluated. It is one of + the 32 stabilizer patterns of PR #6965, and it is not an element of `H`. + +## Credit + +The explicit pair, the free odd signs, and the joint-dimension table are the +certificate in upstream PR #6965. The trace `-48`, the 84+132 split, and the +question answered here are upstream PR #7020, head +`6025743bc95e096845af0962ba0c4c37cce89c4e`. Krzysztof Wojt's +`research/exact-one-slot-gram/` defines `X_3`. Ali Romman's #4958 and #4720 +retain the query and the Bell action. Nick Petalas's #5120 is the degree-410 +lower bound. JoyboyBrian's handoff recorded the sign-character dimensions. +The doubled representation comes from #1719. New work is Apache-2.0. + +## Workflow feedback + +The named open question fixed the masks and named the one sign to add, so +the trace stayed a sum over the existing group of 64 operators. +https://github.com/CrocSwap/integer-mult-bounds/discussions/1200 diff --git a/research/c3-odd-sign-trace-slot/SOURCES.json b/research/c3-odd-sign-trace-slot/SOURCES.json new file mode 100644 index 0000000000..a16afb78ce --- /dev/null +++ b/research/c3-odd-sign-trace-slot/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "17469fff78c22941280f04d39dc5a1faee09c840", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/c3-centre-sign-split/PROOF.md", + "usage": "provenance", + "git_blob": "8da44a79e0e3f7d3cfcd7ebb8c46cc46146a9869", + "sha256": "6d9446760eb90201b96a73c78a04fdc0320c0c3973dc9d96f05a7fd135a45558" + }, + { + "path": "research/centre-polynomial-cache-limits/frozen/work/centre-encoding-campaign-20261014/lanes/circuit-interface/INTERFACE.json", + "usage": "input", + "git_blob": "4201e9a04c12273b919e2cae60a6b6482c8150f3", + "sha256": "5c6c51fbffc07a683e922f17532fd90262ae9e23cc3560a696002073dd234ef3" + }, + { + "path": "research/exact-one-slot-gram/PROOF.md", + "usage": "provenance", + "git_blob": "91854803c13d19d7962aafedf37aca0004827514", + "sha256": "30ccfa6d6623313a3c73c7107b7d9c3872eeffc07d2062e7e9b797162585e9b4" + } + ] +} diff --git a/research/c3-odd-sign-trace-slot/TASK.json b/research/c3-odd-sign-trace-slot/TASK.json new file mode 100644 index 0000000000..cabc243aec --- /dev/null +++ b/research/c3-odd-sign-trace-slot/TASK.json @@ -0,0 +1,123 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 8, + "base_commit": "17469fff78c22941280f04d39dc5a1faee09c840", + "original_card": { + "id": "formal-interface-lemma", + "question": "Can one uncovered interface implication be formalized with exact caller and certificate bindings?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/gate-operand-parity-lean/README.md", + "research/staged544-certified-endpoint/README.md", + "research/unconditional-batched-crt/README.md" + ], + "methods": [ + "Formalize a missing boundary lemma identified by the selected review.", + "Audit a formal theorem-to-certificate binding independently." + ], + "acceptance_gate": "State the exact formalized proposition and remaining assumptions; avoid duplicate arithmetic formalizations already present.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.", + "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse." + }, + "first_experiment": "Write one missing statement with quantified hypotheses, actual caller and existing coverage. A compact-switch lemma is a candidate only after its mathematical contract is reviewed. Establish a bounded proof plan before a separately budgeted proof-assistant build; do not rerun large Lean jobs as orientation.", + "bottleneck_link": "A missing interface proof can reduce the conditional gap even if it does not change kappa.", + "allowed_variations": [ + "Narrow to one formal lemma or one theorem-to-certificate binding." + ], + "scope_change_triggers": [ + "Formalizing already-covered arithmetic and claiming the full multiplication theorem." + ], + "overlap_terms": [ + "hyperplane end", + "formal interface", + "Lean binding", + "3807", + "3857", + "4100", + "gate-operand-parity-lean", + "staged544-certified-endpoint", + "unconditional-batched-crt" + ], + "existing_checks": [ + { + "scope": "PR #3807: scoped gate-operand parity formalization.", + "evidence": "research/gate-operand-parity-lean/README.md", + "remaining": "Exact theorem-to-caller binding and genuinely uncovered interface lemmas.", + "status": "author-checked", + "source_commit": "4c3530f42a6abcc48e7a6bcffd6c901911dc8269", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #3857: certified real-power moment/endpoint arithmetic.", + "evidence": "research/staged544-certified-endpoint/README.md", + "remaining": "Uniform algorithmic implications, not another endpoint digit.", + "status": "author-checked", + "source_commit": "ef4315b8caa605e47a2515004845eb2d2ed71a86", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4100: compact-switch formalization proposed as future validation.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Audit the statement and assumptions before a formal proof campaign.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Prove that adding one odd minus sign to u, on coordinate 1, keeps the X_3 trace -48 on the trivial (+1,+1) eigenvalue of the explicit c=3 pair from PR #6965. The same identity covers all 16 odd signs on that u, with v's mask held at 17.", + "scope_change_reason": "The catalogue card asks for a formal caller or certificate binding. Open question 2 of upstream PR #7020 asks whether one other cross-coset pair, with a different odd sign, moves the X_3 trace -48 onto another (u, v) eigenvalue. The named first step is to repeat the trace with one odd minus sign added to u, keeping the masks inherited from PR #6965. This package answers that trace question. It does not add a Lean binding, and it does not compute a characteristic polynomial.", + "bottleneck_link": "Scoped side result on the historical centre Gram. The selected conditional kappa remains 781451/250000000. Keeping or moving this trace does not replace the degree-881 one-slot certificate and does not admit a supplier.", + "budget_minutes": 60, + "stop_rule": "Stop once the coordinate-1 variation has been traced and either -48 has moved to another (u, v) eigenvalue or the trace formula shows it remains on (+1,+1), and once the other odd signs on this u are recorded. Do not compute a characteristic polynomial and do not change the mask of v.", + "outcome": "completed", + "evidence": "verify.py recomputes the joint traces from INTERFACE.json in normal and optimized modes. Marker PASS_C3_ODD_SIGN_TRACE_SLOT. The mask-7 pair and all 16 odd signs on u keep trivial X_3 traces -48, 16, 16, 16, with -48 on (+1,+1) and split 84+132. Character 1 moves its trace 36 from (+1,+1) to (-1,+1). Address traces agree by enumeration and by affine solution. Selected baseline returned PASS_RESEARCH_BASELINE_BINDINGS_ONLY.", + "author": "unpaidmoon", + "ai_assistance": "Prepared by unpaidmoon with substantial Cursor Grok assistance. The assistant derived the reindexing argument and wrote the verifier. This is not an independent human or proof-kernel review.", + "open_questions": [ + { + "question": "Does one odd minus added to v, with u's mask held at 5, keep the X_3 trace -48 on the trivial (+1,+1) eigenvalue?", + "why_it_matters": "The census here adds odd signs only to u. An odd sign on v is the other factor of the same cross-coset pair, and the trace -48 could in principle sit on a different (u, v) eigenvalue there.", + "first_step": "Repeat the joint trace of X_3 with v's mask replaced by 19 (the minus on coordinate 1 added to mask 17) and with u's mask held at 5. Compare the four trivial traces with -48, 16, 16, 16.", + "blocked_by": "This package does not change v's mask. The commutation of odd signs through u was checked, but the v-side sum was not evaluated." + }, + { + "question": "What are the trivial X_3 traces for the other legal even-cycle pattern on (0 2)(4 6), with minus signs on coordinates 4 and 6 and no odd minuses?", + "why_it_matters": "PR #6965 lists two opposite-cycle sign patterns for each of the three permutations. This package holds the even signs of u fixed as minuses on coordinates 0 and 2. The other pattern is not an element of H, so the reindexing above does not apply to it.", + "first_step": "Realize the signed permutation (0 2)(4 6) with mask 80, keep v at mask 17, and evaluate the four trivial joint traces of X_3.", + "blocked_by": "Mask 80 changes even signs. The odd-sign identity does not determine that trace." + } + ], + "environment": { + "python": "3.12.3", + "platform": "linux" + }, + "overlap": { + "checked_at": "2026-11-10T10:29:46Z", + "canonical_main": "17469fff78c22941280f04d39dc5a1faee09c840", + "open_pr_records": 339, + "discussion_records": 7013, + "remote_pagination_complete": true, + "local_records": 10178, + "head_records": 10178, + "local_coverage_complete": true, + "predecessor_pr": "https://github.com/CrocSwap/integer-mult-bounds/pull/7020", + "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19514155", + "terms": [ + "trace -48", + "odd minus", + "cross-coset" + ], + "limits": "Closed PRs were searched through local READMEs, TASK metadata and the ledger. No code diffs or unpublished work. PR #7020 leaves the sign patterns unevaluated. PR #7021 asks about a degree-16 polynomial, which is not this trace." + } +} diff --git a/research/c3-odd-sign-trace-slot/VERIFY.json b/research/c3-odd-sign-trace-slot/VERIFY.json new file mode 100644 index 0000000000..545d42b67c --- /dev/null +++ b/research/c3-odd-sign-trace-slot/VERIFY.json @@ -0,0 +1,32 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/centre-polynomial-cache-limits/frozen/work/centre-encoding-campaign-20261014/lanes/circuit-interface/INTERFACE.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "-W", + "error", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Rebuild the explicit c=3 pair and the 16 odd signs from the query. Require the mask-7 variation, and all 16 odd signs on u, to keep the trivial X_3 traces at -48, 16, 16, 16, with -48 on (+1,+1). Require character 1 to move its trace 36. Five rejection controls must fire." + }, + { + "argv": [ + "{python}", + "-B", + "-O", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Repeat the same certificate with assertions removed. Acceptance uses explicit checks, so optimization does not skip a trace or a rejection control." + } + ] +} diff --git a/research/c3-odd-sign-trace-slot/verify.py b/research/c3-odd-sign-trace-slot/verify.py new file mode 100644 index 0000000000..f2f811fd9f --- /dev/null +++ b/research/c3-odd-sign-trace-slot/verify.py @@ -0,0 +1,686 @@ +#!/usr/bin/env python3 +"""Prove an odd minus on u keeps the X_3 trace -48 on (+1, +1). + +The explicit c=3 pair from research/c3-centre-sign-split has + + u = (0 2)(4 6) with minus signs on coordinates 0 and 2, + v = (0 4)(2 6) with minus signs on coordinates 0 and 4. + +Open question 2 of the payload-involution certificate asks for the trace of +X_3 after one odd minus sign is added to u. This verifier repeats that trace +for the minus on coordinate 1, then evaluates the same formula on every +diagonal sign supported on the odd coordinates. Acceptance uses explicit +checks, so python -O does not skip a step. +""" + +import hashlib +import json +import pathlib + +ROOT = pathlib.Path(__file__).resolve().parents[2] +INTERFACE = ( + ROOT + / "research/centre-polynomial-cache-limits/frozen/work" + / "centre-encoding-campaign-20261014/lanes/circuit-interface/INTERFACE.json" +) +SELECTED = ROOT / "certificates/selected-result.json" +INTERFACE_SHA256 = ( + "5c6c51fbffc07a683e922f17532fd90262ae9e23cc3560a696002073dd234ef3" +) +SELECTED_SHA256 = ( + "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" +) +SELECTED_KAPPA = "781451/250000000" +SECTOR = 3 +ALL_ONE = 511 +SHIFT = SECTOR +CHARACTER = SECTOR ^ ALL_ONE # 508 +ODDS = (1, 3, 5, 7) +EVENS = (0, 2, 4, 6) +U_SIGMA = (2, 1, 0, 3, 6, 5, 4, 7) # (0 2)(4 6) +U_MASK = 5 # minus signs on coordinates 0 and 2 +V_SIGMA = (4, 1, 6, 3, 0, 5, 2, 7) # (0 4)(2 6) +V_MASK = 17 # minus signs on coordinates 0 and 4 +PRODUCT_SIGMA = (6, 1, 4, 3, 2, 5, 0, 7) # (0 6)(2 4) +ADDED_COORDINATE = 1 +ADDED_MASK = 1 << ADDED_COORDINATE # 2 +JOINT_ORDER = ((1, 1), (1, -1), (-1, 1), (-1, -1)) +# Published comparison point: joint dimensions and X_3 traces of the unvaried pair. +EXPECTED_BY_WEIGHT = { + 0: ((216, 216, 216, 216), (-48, 16, 16, 16)), + 1: ((180, 84, 84, 84), (36, -12, -12, -12)), + 2: ((48, 48, 48, 48), (-24, 8, 8, 8)), + 3: ((44, 12, 12, 12), (12, -4, -4, -4)), + 4: ((8, 8, 8, 8), (0, 0, 0, 0)), +} +CHARACTER_DIMENSIONS = ( + 864, 432, 432, 192, 432, 192, 192, 80, + 432, 192, 192, 80, 192, 80, 80, 32, +) + + +def fail(message): + raise SystemExit("FAIL: " + message) + + +def expect(condition, message): + if not condition: + fail(message) + + +def sha256_file(path): + digest = hashlib.sha256() + digest.update(path.read_bytes()) + return digest.hexdigest() + + +def dot(left, right): + return bin(left & right).count("1") & 1 + + +def apply_map(matrix, address): + image = 0 + for bit in range(9): + if (address >> bit) & 1: + image ^= matrix[bit] + return image + + +def compose_maps(left, right): + return tuple(apply_map(left, column) for column in right) + + +def mask_to_eps(mask): + return tuple(-1 if (mask >> bit) & 1 else 1 for bit in range(8)) + + +def eps_to_mask(eps): + return sum(1 << bit for bit in range(8) if eps[bit] < 0) + + +def inv_of(sigma): + inverse = [0] * 8 + for source, image in enumerate(sigma): + inverse[image] = source + return tuple(inverse) + + +def compose_perm(left, right): + return tuple(left[right[index]] for index in range(8)) + + +def compose_signed(left_sigma, left_mask, right_sigma, right_mask): + """Compose operators, right applied first. + + (Sv)_k = eps[k] * v[sigma^{-1}(k)]. + """ + sigma = compose_perm(left_sigma, right_sigma) + left_inv = inv_of(left_sigma) + eps = [] + for index in range(8): + left_sign = -1 if (left_mask >> index) & 1 else 1 + source = left_inv[index] + right_sign = -1 if (right_mask >> source) & 1 else 1 + eps.append(left_sign * right_sign) + return sigma, eps_to_mask(eps) + + +def norm_code(values): + code = 0 + sign = 1 + seen = False + for index, value in enumerate(values): + if value == 0: + continue + if not seen: + seen = True + sign = 1 if value > 0 else -1 + signed = value * sign + code |= (1 if signed > 0 else 2) << (2 * index) + return code + + +def rank_solve(vectors, target=None): + width = len(vectors) + matrix = [[(vector >> row) & 1 for vector in vectors] for row in range(9)] + image = None if target is None else [(target >> row) & 1 for row in range(9)] + pivot_at = [-1] * 9 + rank = 0 + for col in range(width): + pivot = None + for row in range(rank, 9): + if matrix[row][col]: + pivot = row + break + if pivot is None: + continue + matrix[rank], matrix[pivot] = matrix[pivot], matrix[rank] + if image is not None: + image[rank], image[pivot] = image[pivot], image[rank] + for row in range(9): + if row != rank and matrix[row][col]: + for entry in range(width): + matrix[row][entry] ^= matrix[rank][entry] + if image is not None: + image[row] ^= image[rank] + pivot_at[rank] = col + rank += 1 + if rank == 9: + break + if target is None: + return rank + if any(image[row] for row in range(rank, 9)): + return None + coef = [0] * width + for row in range(rank): + coef[pivot_at[row]] = image[row] + return coef + + +def coordinate_trace(sigma, mask): + total = 0 + for index in range(8): + if sigma[index] == index: + total += -1 if (mask >> index) & 1 else 1 + return total + + +def chi_value(chi, mask): + sign = 0 + for index, coordinate in enumerate(ODDS): + if (chi >> index) & 1 and (mask >> coordinate) & 1: + sign ^= 1 + return -1 if sign else 1 + + +def odd_masks(): + """Every diagonal sign supported on the odd coordinates, once each.""" + masks = [] + for bits in range(16): + mask = 0 + for index, coordinate in enumerate(ODDS): + if (bits >> index) & 1: + mask |= 1 << coordinate + masks.append(mask) + return masks + + +def address_trace_enumerate(matrix, translation, character): + total = 0 + for address in range(512): + image = apply_map(matrix, address) + if (image ^ translation) == address: + total += -1 if dot(character, image) else 1 + return total + + +def address_trace_linear(matrix, translation, character): + """Same trace by solving (T+I)a = translation over F_2.""" + rows = [] + for row in range(9): + coef = 0 + for col in range(9): + image = matrix[col] ^ (1 << col) + if (image >> row) & 1: + coef |= 1 << col + rhs = (translation >> row) & 1 + rows.append(coef | (rhs << 9)) + pivot_of = [-1] * 9 + rank = 0 + for col in range(9): + pivot = None + for row in range(rank, 9): + if (rows[row] >> col) & 1: + pivot = row + break + if pivot is None: + continue + rows[rank], rows[pivot] = rows[pivot], rows[rank] + for row in range(9): + if row != rank and (rows[row] >> col) & 1: + rows[row] ^= rows[rank] + pivot_of[rank] = col + rank += 1 + for row in range(rank, 9): + if (rows[row] >> 9) & 1: + return 0 + particular = 0 + for row in range(rank): + if (rows[row] >> 9) & 1: + particular |= 1 << pivot_of[row] + pivots = set(pivot_of[:rank]) + kernel = [] + for col in range(9): + if col in pivots: + continue + vector = 1 << col + for row in range(rank): + if (rows[row] >> col) & 1: + vector ^= 1 << pivot_of[row] + kernel.append(vector) + if any(dot(character, vector) for vector in kernel): + return 0 + sign_bit = dot(character, particular) ^ dot(character, translation) + sign = -1 if sign_bit else 1 + return sign * (1 << len(kernel)) + + +def address_trace(matrix, translation, character): + enumerated = address_trace_enumerate(matrix, translation, character) + solved = address_trace_linear(matrix, translation, character) + expect( + enumerated == solved, + "address-trace methods disagree for translation " + + str(translation) + + " character " + + str(character) + + ": " + + str(enumerated) + + " vs " + + str(solved), + ) + return enumerated + + +def load_query(): + expect(sha256_file(INTERFACE) == INTERFACE_SHA256, "INTERFACE.json hash changed") + expect(sha256_file(SELECTED) == SELECTED_SHA256, "selected-result.json hash changed") + selected = json.loads(SELECTED.read_text()) + expect(selected["kappa"] == SELECTED_KAPPA, "selected kappa is not 781451/250000000") + data = json.loads(INTERFACE.read_text()) + ports = [int(port) for port in data["ports"]] + rows = data["R"] + columns = [ + tuple(int(rows[row].get(str(column), "0")) for row in range(8)) + for column in range(112) + ] + expect(len(ports) == 112 and len(set(ports)) == 112, "ports are not 112 distinct labels") + expect( + all(value in (-1, 0, 1) for column in columns for value in column), + "a column entry is outside {-1,0,1}", + ) + gram = [[0] * 8 for _ in range(8)] + for column in columns: + weight = sum(1 for value in column if value) + expect(weight == 4, "a column does not have weight 4") + for index, value in enumerate(column): + for other in range(8): + gram[index][other] += value * column[other] + expect( + all(gram[i][k] == (56 if i == k else 0) for i in range(8) for k in range(8)), + "RR^T is not 56 I", + ) + expect(all(dot(port, ALL_ONE) == 1 for port in ports), "a port label has even weight") + expect(dot(SHIFT, CHARACTER) == 0, "X_3 and Z_508 do not commute") + return columns, ports + + +def prepare_labels(columns, ports): + lookup = [-1] * (1 << 16) + for column, port in zip(columns, ports): + lookup[norm_code(column)] = port + basis = [] + for port in ports: + if rank_solve(basis + [port]) == len(basis) + 1: + basis.append(port) + if len(basis) == 9: + break + expect(len(basis) == 9, "ports do not span F2^9") + coords = [rank_solve(basis, 1 << bit) for bit in range(9)] + contrib = [[index for index, bit in enumerate(row) if bit] for row in coords] + basis_columns = [columns[ports.index(port)] for port in basis] + return lookup, basis_columns, contrib + + +def realize(lookup, columns, ports, basis_columns, contrib, sigma, mask): + inverse = inv_of(sigma) + port_of = {} + for column, port in zip(columns, ports): + values = [] + for index in range(8): + value = column[inverse[index]] + if value and (mask >> index) & 1: + value = -value + values.append(value) + found = lookup[norm_code(values)] + if found < 0: + return None + port_of[port] = found + basis_images = [] + for column in basis_columns: + values = [] + for index in range(8): + value = column[inverse[index]] + if value and (mask >> index) & 1: + value = -value + values.append(value) + found = lookup[norm_code(values)] + if found < 0: + return None + basis_images.append(found) + matrix = [] + for bit in range(9): + acc = 0 + for index in contrib[bit]: + acc ^= basis_images[index] + matrix.append(acc) + matrix = tuple(matrix) + for port, image in port_of.items(): + if apply_map(matrix, port) != image: + return None + for left in range(9): + for right in range(left, 9): + if dot(matrix[left], matrix[right]) != (1 if left == right else 0): + return None + return { + "sigma": sigma, + "mask": mask, + "T": matrix, + "coordinate_trace": coordinate_trace(sigma, mask), + } + + +def fixes_labels(matrix): + return ( + apply_map(matrix, SECTOR) == SECTOR + and apply_map(matrix, ALL_ONE) == ALL_ONE + and apply_map(matrix, CHARACTER) == CHARACTER + ) + + +def commutes_with_shift(matrix): + for address in range(512): + if apply_map(matrix, address ^ SHIFT) != (apply_map(matrix, address) ^ SHIFT): + return False + return True + + +def operator_trace(element, translation, character): + counted = address_trace(element["T"], translation, character) + return element["coordinate_trace"] * counted + + +def joint_traces(table, chi): + """Return (dimensions, X_3 traces) in JOINT_ORDER.""" + dimensions = [] + traces = [] + for eps, delta in JOINT_ORDER: + dimension_sum = 0 + trace_sum = 0 + for mask in table["masks"]: + weight = chi_value(chi, mask) + dimension_sum += weight * ( + table["I"][mask] + + eps * table["u"][mask] + + delta * table["v"][mask] + + eps * delta * table["uv"][mask] + ) + trace_sum += weight * ( + table["X"]["I"][mask] + + eps * table["X"]["u"][mask] + + delta * table["X"]["v"][mask] + + eps * delta * table["X"]["uv"][mask] + ) + expect(dimension_sum % 64 == 0, "a joint dimension is not a multiple of 64") + expect(trace_sum % 64 == 0, "a joint trace is not a multiple of 64") + dimensions.append(dimension_sum // 64) + traces.append(trace_sum // 64) + return tuple(dimensions), tuple(traces) + + +def build_table(build, identity, sign_group, u_element, v_element): + product_sigma, product_mask = compose_signed( + u_element["sigma"], u_element["mask"], v_element["sigma"], v_element["mask"] + ) + back_sigma, back_mask = compose_signed( + v_element["sigma"], v_element["mask"], u_element["sigma"], u_element["mask"] + ) + expect( + (product_sigma, product_mask) == (back_sigma, back_mask), + "the varied pair does not commute", + ) + product = build(product_sigma, product_mask) + expect(product is not None, "the varied product is not a symmetry") + bases = {"I": identity, "u": u_element, "v": v_element, "uv": product} + stored = {"I": {}, "u": {}, "v": {}, "uv": {}, "X": {"I": {}, "u": {}, "v": {}, "uv": {}}} + cosets = {} + masks = [] + for name, base in bases.items(): + keys = [] + for member in sign_group: + if name == "I": + element = member + else: + sigma, mask = compose_signed( + base["sigma"], base["mask"], member["sigma"], member["mask"] + ) + element = build(sigma, mask) + expect(element is not None, "a varied product left the symmetry representation") + expect( + element["T"] == compose_maps(base["T"], member["T"]), + "label maps do not multiply", + ) + expect( + compose_signed(element["sigma"], element["mask"], element["sigma"], element["mask"]) + == (tuple(range(8)), 0), + "a varied group element does not square to the identity", + ) + both = compose_signed( + element["sigma"], element["mask"], member["sigma"], member["mask"] + ) + reverse = compose_signed( + member["sigma"], member["mask"], element["sigma"], element["mask"] + ) + expect(both == reverse, "a varied group element does not commute with H") + expect(fixes_labels(element["T"]), "a varied group element moves sector 3, 511, or 508") + expect(commutes_with_shift(element["T"]), "X_3 does not commute with a varied group element") + stored[name][member["mask"]] = operator_trace(element, 0, 0) + stored["X"][name][member["mask"]] = operator_trace(element, SHIFT, 0) + keys.append((element["sigma"], element["mask"])) + cosets[name] = keys + if name == "I": + masks = [member["mask"] for member in sign_group] + stored["masks"] = masks + stored["product_sigma"] = product_sigma + stored["product_mask"] = product_mask + stored["u_mask"] = u_element["mask"] + stored["cosets"] = cosets + return stored + + +def eigenvalue_split(dimension, trace): + expect((dimension + trace) % 2 == 0, "an involution trace has the wrong parity") + positive = (dimension + trace) // 2 + negative = (dimension - trace) // 2 + expect(positive >= 0 and negative >= 0, "an eigenvalue dimension is negative") + return positive, negative + + +def main(): + columns, ports = load_query() + lookup, basis_columns, contrib = prepare_labels(columns, ports) + + def build(sigma, mask): + return realize(lookup, columns, ports, basis_columns, contrib, sigma, mask) + + masks = odd_masks() + expect(len(masks) == 16 and len(set(masks)) == 16, "the odd signs are not the 16 subsets") + expect( + all((mask & sum(1 << bit for bit in EVENS)) == 0 for mask in masks), + "an odd-sign mask meets an even coordinate", + ) + expect(ADDED_MASK in masks and ADDED_COORDINATE in ODDS, "coordinate 1 is not an odd sign") + expect(chi_value(0, ADDED_MASK) == 1, "the trivial character is not +1 on the added sign") + expect(chi_value(1, ADDED_MASK) == -1, "character 1 is not -1 on coordinate 1") + + identity = build(tuple(range(8)), 0) + expect(identity is not None, "the identity is not a symmetry") + expect(operator_trace(identity, 0, 0) == 4096, "the identity trace is not 4096") + sign_group = [] + for mask in masks: + element = build(tuple(range(8)), mask) + expect(element is not None, "a positive-even sign is not a symmetry") + sign_group.append(element) + for left in sign_group: + for right in sign_group: + expect( + compose_signed(left["sigma"], left["mask"], right["sigma"], right["mask"]) + == compose_signed(right["sigma"], right["mask"], left["sigma"], left["mask"]), + "two odd signs do not commute", + ) + u = build(U_SIGMA, U_MASK) + v = build(V_SIGMA, V_MASK) + expect(u is not None and v is not None, "the explicit pair is not a symmetry of the query") + original = build_table(build, identity, sign_group, u, v) + expect(original["product_sigma"] == PRODUCT_SIGMA, "the explicit product is not (0 6)(2 4)") + expect(original["product_mask"] == 65, "the explicit product mask is not 65") + original_sets = {name: set(original["cosets"][name]) for name in ("I", "u", "v", "uv")} + expect(len(original_sets["I"]) == 16, "H does not have 16 distinct signs") + expect( + all(len(original_sets[name]) == 16 for name in original_sets), + "a coset of the explicit pair is not 16 elements", + ) + expect(len(set().union(*original_sets.values())) == 64, "the Klein coset of H is not 64 elements") + + dimensions = [] + for chi in range(16): + total = sum(chi_value(chi, element["mask"]) * operator_trace(element, 0, 0) for element in sign_group) + expect(total % 16 == 0, "a character dimension is not integral") + dimensions.append(total // 16) + expect(tuple(dimensions) == CHARACTER_DIMENSIONS, "c=3 character dimensions changed") + + original_by_character = {} + for chi in range(16): + dims, traces = joint_traces(original, chi) + weight = bin(chi).count("1") + expected_dims, expected_traces = EXPECTED_BY_WEIGHT[weight] + expect(dims == expected_dims, "an unvaried joint dimension changed") + expect(traces == expected_traces, "an unvaried X_3 joint trace changed") + original_by_character[chi] = (dims, traces) + expect(original_by_character[0][1] == (-48, 16, 16, 16), "the comparison trace is not -48, 16, 16, 16") + + trace_by_perm = {} + for name in ("I", "u", "v", "uv"): + for mask, key in zip(original["masks"], original["cosets"][name]): + trace_by_perm[key] = (original[name][mask], original["X"][name][mask]) + + assigned = None + unchanged = 0 + for added in masks: + varied_sigma, varied_mask = compose_signed(U_SIGMA, U_MASK, tuple(range(8)), added) + expect(varied_sigma == U_SIGMA, "an odd sign changed the permutation of u") + expect(varied_mask == (U_MASK ^ added), "an odd sign did not add by disjoint XOR") + expect((varied_mask & sum(1 << bit for bit in EVENS)) == U_MASK, "an odd sign moved an even minus") + element = build(varied_sigma, varied_mask) + expect(element is not None, "an odd sign took u out of the symmetry representation") + table = build_table(build, identity, sign_group, element, v) + expect(table["product_sigma"] == PRODUCT_SIGMA, "an odd sign changed the product permutation") + for name in ("I", "u", "v", "uv"): + expect( + set(table["cosets"][name]) == original_sets[name], + "an odd sign moved a group element out of the explicit Klein coset", + ) + for mask, key in zip(table["masks"], table["cosets"][name]): + expect(key in trace_by_perm, "a varied element has no original trace") + expect( + (table[name][mask], table["X"][name][mask]) == trace_by_perm[key], + "a fresh address trace disagrees with the same signed permutation", + ) + for chi in range(16): + dims, traces = joint_traces(table, chi) + sign = chi_value(chi, added) + old_dims, old_traces = original_by_character[chi] + predicted_dims = [] + predicted_traces = [] + for eps, delta in JOINT_ORDER: + source = JOINT_ORDER.index((eps * sign, delta)) + predicted_dims.append(old_dims[source]) + predicted_traces.append(old_traces[source]) + expect(dims == tuple(predicted_dims), "a joint dimension missed the character reindexing") + expect(traces == tuple(predicted_traces), "an X_3 trace missed the character reindexing") + trivial_dims, trivial_traces = joint_traces(table, 0) + expect(trivial_dims == (216, 216, 216, 216), "a trivial joint dimension moved") + expect(trivial_traces == (-48, 16, 16, 16), "the trace -48 moved off (+1,+1) or changed") + expect(trivial_traces[0] == -48, "the (+1,+1) trace is not -48") + positive, negative = eigenvalue_split(trivial_dims[0], trivial_traces[0]) + expect(positive == 84 and negative == 132, "the (+1,+1) split is not 84+132") + unchanged += 1 + if added == ADDED_MASK: + assigned = (table, trivial_dims, trivial_traces, positive, negative) + + expect(unchanged == 16, "the odd-sign census did not cover 16 patterns") + expect(assigned is not None, "the coordinate-1 pair was not evaluated") + table, trivial_dims, trivial_traces, positive, negative = assigned + expect(table["u_mask"] == 7, "the assigned mask is not 7") + expect(table["product_mask"] == 67, "the assigned product mask is not 67") + moved_dims, moved_traces = joint_traces(table, 1) + expect(moved_dims == (84, 84, 180, 84), "character 1 did not move its large dimension") + expect(moved_traces == (-12, -12, 36, -12), "character 1 did not move its trace 36") + expect(-48 not in moved_traces, "the trace -48 appeared on the moved weight-1 character") + # Character 2 is the weight-1 character on coordinate 3. It is +1 on coordinate 1. + stayed_dims, stayed_traces = joint_traces(table, 2) + expect(chi_value(2, ADDED_MASK) == 1, "character 2 is not +1 on coordinate 1") + expect(stayed_dims == (180, 84, 84, 84), "a weight-1 character fixed by the added sign moved its dimensions") + expect(stayed_traces == (36, -12, -12, -12), "a weight-1 character fixed by the added sign moved its traces") + expect(coordinate_trace(U_SIGMA, 7) == 2, "the assigned representative did not change coordinate trace") + expect(coordinate_trace(U_SIGMA, U_MASK) == 4, "the unvaried coordinate trace is not 4") + + controls = 0 + even_flip = build(U_SIGMA, U_MASK ^ 1) + expect(even_flip is not None, "the even-coordinate control was not a symmetry") + expect(apply_map(even_flip["T"], SECTOR) == 470, "flipping coordinate 0 did not send sector 3 to 470") + expect(apply_map(even_flip["T"], SECTOR) != SECTOR, "an even sign flip still fixed sector 3") + controls += 1 + + identity_trace = joint_traces(table, 0)[0][0] + expect(identity_trace == 216 and identity_trace != trivial_traces[0], "the identity trace collapsed onto -48") + controls += 1 + + def plus_term(mask): + return ( + table["X"]["I"][mask] + + table["X"]["u"][mask] + + table["X"]["v"][mask] + + table["X"]["uv"][mask] + ) + + full_numerator = sum(plus_term(mask) for mask in table["masks"]) + expect(full_numerator == -48 * 64, "the assigned numerator is not -48 times 64") + changed = [ + full_numerator - plus_term(mask) + for mask in table["masks"] + if plus_term(mask) != 0 + ] + expect(changed, "every sign had a zero (+1,+1) contribution, so truncation was vacuous") + expect( + all(partial != -48 * 64 for partial in changed), + "dropping a nonzero sign still reproduced the trace -48", + ) + controls += 1 + + moved = False + assigned_u = build(U_SIGMA, 7) + for address in range(512): + if apply_map(assigned_u["T"], address ^ 1) != (apply_map(assigned_u["T"], address) ^ 1): + moved = True + break + expect(moved, "translation by 1 commuted with the assigned u") + controls += 1 + expect(build((1, 0, 2, 3, 4, 5, 6, 7), 0) is None, "a coordinate transposition was accepted") + controls += 1 + expect(controls == 5, "a rejection control was not reached") + + print("PASS_C3_ODD_SIGN_TRACE_SLOT") + print("assigned coordinate", ADDED_COORDINATE) + print("assigned u mask", table["u_mask"]) + print("assigned product mask", table["product_mask"]) + print("trivial X traces", *trivial_traces) + print("trace -48 slot +1 +1") + print("plus split", positive, negative) + print("weight-1 character 1 traces", *moved_traces) + print("odd patterns", unchanged) + print("controls", controls) + + +if __name__ == "__main__": + main()