From 2c2dad2058a4f01485214b7437b3e8b8d4d8f57c Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Wed, 11 Nov 2026 22:03:03 +0000 Subject: [PATCH] feat(research): exclude common image or kernel lines from the diagonal pair Prove that rank-one idempotents sharing an image line or a kernel line can never realise diag([a],[b]) with a != b, at any word length and over any field, and that at most two calls never suffice under the #6097 target hypotheses. Exact corroboration over F2, F3, F4 and F5. --- .../diagonal-pair-line-separation/PROOF.md | 167 +++++++++ .../diagonal-pair-line-separation/README.md | 127 +++++++ .../SOURCES.json | 36 ++ .../diagonal-pair-line-separation/TASK.json | 107 ++++++ .../diagonal-pair-line-separation/VERIFY.json | 19 ++ .../diagonal-pair-line-separation/verify.py | 321 ++++++++++++++++++ 6 files changed, 777 insertions(+) create mode 100644 research/diagonal-pair-line-separation/PROOF.md create mode 100644 research/diagonal-pair-line-separation/README.md create mode 100644 research/diagonal-pair-line-separation/SOURCES.json create mode 100644 research/diagonal-pair-line-separation/TASK.json create mode 100644 research/diagonal-pair-line-separation/VERIFY.json create mode 100644 research/diagonal-pair-line-separation/verify.py diff --git a/research/diagonal-pair-line-separation/PROOF.md b/research/diagonal-pair-line-separation/PROOF.md new file mode 100644 index 0000000000..bb25670abf --- /dev/null +++ b/research/diagonal-pair-line-separation/PROOF.md @@ -0,0 +1,167 @@ +# Proof of the line exclusion + +## Setting + +Let `F` be a field, `G` a group, `L` a label set, and `F[G]` the group algebra. +For a rank-one idempotent `N` in `M_2(F)` and `g in L`, a call is + + D_N(g) = (I - N) + [g] N. + +Fix `N_1, ..., N_k` and labels `g_1, ..., g_k`. Expanding the product over the +`2^k` subsets `U` of positions gives the identity in `M_2(F[G])` + + P := D_{N_1}(g_1) ... D_{N_k}(g_k) = sum_U [g_U] P_U, (1) + +where `g_U` is the product of the labels at the positions of `U` in increasing +order, `P_U = product_{i in U} N_i` in increasing order, and `P_empty = I`. +Every matrix entry of `P` is an element of the commutative ring `F[G]`. + +## Common image line + +Suppose all `N_i` have the same image line, so `N_i = u v_i^T` for one nonzero +`u` and vectors `v_i`. Idempotence gives `v_i^T u = 1`: + + N_i N_i = u (v_i^T u) v_i^T = u v_i^T = N_i. + +Hence for every `i, j` + + N_i N_j = u (v_i^T u) v_j^T = u v_j^T = N_j. (2) + +By (2) and induction on the size of `U`, every nonempty `P_U` is `N_{max U}`: + + N_{i_1} N_{i_2} ... N_{i_r} = N_{i_r} for i_1 < ... < i_r. + +Substituting in (1), with `c_j := sum_{V subseteq {1..j-1}} [g_V]` and +`[g_U] = [g_{U without j}] [g_j]` for `U` with maximum `j`, + + P = I + sum_{j=1}^k c_j [g_j] N_j = I + u w^T, + w^T := sum_j c_j [g_j] v_j^T. (3) + +Every entry of `u w^T` is `u_i` times an element of `F[G]`, and `u_i` lies in +the central subfield `F`. Therefore the determinant of `P - I` vanishes +identically in `F[G]`: + + det(P - I) = 0. (4) + +## Common kernel line + +Suppose all `N_i` share a kernel line, so `N_i = u_i v^T` for one nonzero `v`. +Idempotence gives `v^T u_i = 1`, hence `N_i N_j = u_i (v^T u_j) v^T = N_i`. +The same induction gives `P_U = N_{min U}`, and (1) becomes + + P = I + w v^T, w := sum_j c'_j [g_j] u_j, + +so (4) holds again. + +A family with a single repeated projector is a special case of both paragraphs: +all its members share an image line and a kernel line. + +## The determinant is not zero for a separated pair + +Let `a != b` be elements of `G`. We show + + ([a] - 1)([b] - 1) != 0 in F[G] for every field F. (5) + +The product is `[ab] - [a] - [b] + 1`. Its support is contained in +`{ab, a, b, e}` with integer coefficients `+1, -1, -1, +1` on the four basis +elements, where repeated elements are collected. Since `a != e`, `b != e` and +`a != b`, the only possible collisions are `ab = e`, `ab = a`, `ab = b`, and +`ab` distinct from all of them. + +- `ab = a` forces `b = e`, excluded. `ab = b` forces `a = e`, excluded. +- `ab = e`: the coefficient of `e` is `+1 + 1 = 2` and the coefficients of `a` + and `b` are `-1`. If `a != b` then `[e]`, `[a]`, `[b]` are distinct basis + elements, so the product is nonzero because `2 != 0` or `a`, `b` are distinct + from `e`. If `a = b` the case is excluded by hypothesis. +- Otherwise `ab`, `a`, `b`, `e` are four distinct basis elements and the + coefficient of `ab` is `1 != 0`. + +In every case some basis coefficient is nonzero in `F`, so (5) holds. + +Now assume `P = diag([a],[b])`. Then `P - I = diag([a]-1, [b]-1)` and + + det(P - I) = ([a] - 1)([b] - 1). + +By (5) this is nonzero whenever `a != b`, contradicting (4). This proves +Theorem 1: a common image line or a common kernel line can never produce a +diagonal pair with distinct targets, at any length, over any field and any +group. + +## Corollary: line separation is necessary + +Let `a != b` and suppose neither is a product of at most two labels. If a +product equals `diag([a],[b])`, Theorem 1 excludes every family with one image +line or one kernel line. Hence the projector list contains two projectors with +distinct image lines and two with distinct kernel lines. A repeated projector +family is excluded as well. + +## Two calls never suffice + +Let `P = D_{N_1}(g_1) ... D_{N_k}(g_k) = diag([a],[b])` with `k <= 2`. + +*Normalisation.* For `S in GL_2(F)`, conjugating the whole product gives + + S P S^{-1} = D_{S N_1 S^{-1}}(g_1) ... D_{S N_k S^{-1}}(g_k), + +and `S diag([a],[b]) S^{-1} = diag([a],[b])` because `[a]` and `[b]` are +central scalars. Rank-one idempotents are conjugate, so we may assume +`N_1 = E00`. + +*Case `k <= 1`.* Then `P - I` is either `0` or `(1 + [g_1]) N_1`, which has +determinant zero, while `diag([a]-1, [b]-1)` has determinant +`([a]-1)([b]-1) != 0` by (5). Contradiction. + +*Case `k = 2`.* Put `t_2 = 1 + [g_2]`, which is nonzero because the coefficient +of the identity basis element is `1`. With `N_1 = E00`, + + P = diag([g_1], 1) (I + t_2 N_2). + +A product of two diagonal matrices is diagonal, and `diag([g_1], 1)` is +invertible in the total ring of fractions, so `Q := I + t_2 N_2` is diagonal. +Writing `N_2 = (p, q; r, s)`, the off-diagonal entries of `Q` are `t_2 q` and +`t_2 r`. Since `F[G]` is a free `F`-module and `t_2 != 0`, `t_2 q = 0` forces +`q = 0`, and similarly `r = 0`. So `N_2` is diagonal, hence `N_2` is `E00` or +`E11`. + +Four possibilities remain, and each has a target that is the identity or a +single label: + + D_E00(g_1) D_E00(g_2) = diag([g_1 g_2], 1), + D_E00(g_1) D_E11(g_2) = diag([g_1], [g_2]), + D_E11(g_1) D_E00(g_2) = diag([g_2], [g_1]), + D_E11(g_1) D_E11(g_2) = diag(1, [g_1 g_2]). + +In each case `a` or `b` is `e` or a single label, so it is a product of at most +two labels, contradicting the hypothesis. This proves Theorem 2. + +## What the verifier checks + +`verify.py` reconstructs each field from its addition and multiplication, builds +the rank-one idempotent inventory directly from `N^2 = N` and `trace(N) = 1`, and +then checks by exact arithmetic: + +- the inventories `q(q+1) = 6, 12, 20, 30` for `F2, F3, F4, F5`; +- every ordered pair in every image-line and kernel-line class satisfies (2) or + its transpose (`24, 72, 160, 300` pairs); +- every nonempty subset product of every enumerated same-line tuple collapses to + the last or first projector (`7,812 / 71,736 / 43,400 / 123,960` checks); +- the determinant of `P - I` vanishes for each such tuple, computed by exact + expansion in the group algebra of the free abelian group on the positions + (`372 / 2,904 / 3,400 / 9,360` tuples at the lengths shown in the run line); +- the two-call diagonal-forcing step: for every projector `N_2`, the product + `D_E00(g_1) D_{N_2}(g_2)` is diagonal if and only if `N_2` is diagonal; +- the positive control `D_E00(x)^3 D_E11(y)^3 = diag([x^3],[y^3])`, whose + determinant is nonzero with the four predicted coefficients, and the + mixed-line control `D_E00(x) D_E11(y)` with a nonzero determinant. + +The free abelian group is a commutative instance, which is what the rank +argument uses; the verifier is finite corroboration, not a proof kernel. It does +not enumerate tuples outside the same-line families and is not a census. + +## Remaining proof obligations + +- The general `F4`, `F5`, odd-characteristic and larger-width six-call floors + remain open. Nothing here bounds tuples with two or more image lines. +- Theorem 2 is a written argument; only the diagonal-forcing step is machine + checked. +- No native, compiler, supplier or kappa claim is made or implied. diff --git a/research/diagonal-pair-line-separation/README.md b/research/diagonal-pair-line-separation/README.md new file mode 100644 index 0000000000..5a527d2e31 --- /dev/null +++ b/research/diagonal-pair-line-separation/README.md @@ -0,0 +1,127 @@ +# A common image or kernel line cannot build the diagonal pair + +This contribution was produced by Nick Petalas. Apache-2.0. +Independent human and formal proof-kernel review are unclaimed. + +Scoped written proof with exact finite corroboration. No new kappa, no native +supplier, no selected-frontier change. + +## Result + +Work in the rank-one-idempotent register model of Wentao Li's #4089, as used by +Nick Petalas's #6038, Josie Elliston's #6048 and JoyboyBrian's #6097. Fix a +field `F`, a group `G`, a label set `L`, and write `[g]` for the basis element of +`F[G]`. A call is + + D_N(g) = (I - N) + [g] N, g in L, + +where `N` is a rank-one idempotent `2 x 2` matrix over `F`. + +**Theorem 1 (line exclusion).** Let `N_1, ..., N_k` be rank-one idempotents that +share a common image line, or share a common kernel line. Then for every labels +`g_1, ..., g_k`, no product `D_{N_1}(g_1) ... D_{N_k}(g_k)` equals +`diag([a],[b])` with `a != e != b`. This holds for every `k >= 0`, every field, +and every group. + +**Corollary 1.1 (necessary line separation).** If a product of `k` calls equals +`diag([a],[b])` with `a != b` and neither `a` nor `b` a product of at most two +labels, then the projector list contains two projectors with distinct image +lines and two projectors with distinct kernel lines. In particular no family +with a single image line, a single kernel line, or one repeated projector +attains the pair at any length. + +**Theorem 2 (two calls never suffice).** Over every field and every group, no +product of at most two calls equals `diag([a],[b])` when `a != b` and neither +`a` nor `b` is a product of at most two labels. Without that length hypothesis +two calls do suffice: `D_{E00}(x) D_{E11}(y) = diag([x],[y])`. + +Theorem 1 is written out in [PROOF.md](PROOF.md). Theorem 2 is a short +normalisation argument in the same file; it is *not* machine-checked, and it is +labelled as a written step. + +## Why it matters for the open field question + +JoyboyBrian's #6097 proves the six-call floor over `F2` at width two and leaves +the field extension open: its stored second next question asks whether the floor +extends to odd characteristic or `F4`, with the blocker "even pairing is specific +to `F2`". That question is the one answered here only in part: Theorem 1 removes +a whole family of candidate counterexamples at every length and field, and +Theorem 2 removes lengths zero, one and two. The general `F4` and odd +characteristic floor stays open, and no claim about it is made. + +Theorem 1 composes with the existing symmetry reduction rather than replacing +it. Nick Petalas's #6609 counts `267,072` representatives of the `3,200,000` +five-call `F4` projector tuples and `1,520,110` of the `24,300,000` `F5` tuples +under simultaneous monomial conjugation and reversal with transpose. Every +remaining representative of a completing word must carry two image lines and +two kernel lines. + +## Evidence + +`verify.py`, standard library only, checks by exact integer and finite-field +arithmetic: + +1. the rank-one idempotent inventories `q(q+1)` for `q = 2,3,4,5`, namely + `6, 12, 20, 30`; +2. `N_i N_j = N_j` for every ordered pair with a common image line, and + `N_i N_j = N_i` for every ordered pair with a common kernel line; +3. the subset collapse `P_U = N_{max U}` and `P_U = N_{min U}` for every subset + of every enumerated same-line tuple; +4. the vanishing of the determinant of `P - I`, computed by exact expansion in + the group algebra of the free abelian group on the call positions, for every + enumerated same-line tuple over `F2`, `F3`, `F4` and `F5` at the lengths + recorded in the run line (`5` for `F2`, `F3`; `4` for `F4`, `F5`); +5. the positive control that the six-call `F2` word has a nonzero minor, and the + negative control that mixing image lines can produce a nonzero minor. + +The enumeration is finite corroboration of a written argument, not a +replacement for it. It is not a census of all projector tuples, and it says +nothing about tuples outside the same-line families. + +## Reproduce + +From the repository root, with the interpreter used for this package: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B research/diagonal-pair-line-separation/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -O -B research/diagonal-pair-line-separation/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/diagonal-pair-line-separation +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/diagonal-pair-line-separation --check-source-history +``` + +Any CPython 3.12 installation may replace the displayed path. The first two +commands print one line beginning `PASS_DIAGONAL_PAIR_LINE_SEPARATION`. Checks +raise explicit exceptions, so `-O` does not disable them. + +## Credit + +JoyboyBrian's #6097 supplies the width-two `F2` six-call floor, the six-projector +inventory, the collision relaxation and the six-call word; its stored next +question is the source of this target. Josie Elliston's #6048 and #6137 supply +the four-call floor and the width-two framing. Wentao Li's #4089 introduces the +register model. Nick Petalas's #6038 supplies the earlier four-call `xy`/`yx` +result, and #6609 supplies the related symmetry reduction, which is cited as +related work and is not used as a step here. No predecessor executable is +imported or run. + +## Limits + +- Theorems 1 and 2 only. The `F4`, `F5`, odd-characteristic and larger-width + six-call floors remain open. +- Theorem 1 excludes same-line families. It does not bound tuples with two or + more image lines, which is where a counterexample must live. +- The finite enumeration corroborates the collapse and the minor identity; it is + not a proof kernel and not a complete tuple census. +- No native tariff, supplier or multiplication bound is inferred. + +## Open next questions + +1. Does the six-call floor hold over `F4`? The remaining search is the `267,072` + representatives of #6609 restricted to tuples with at least two image and two + kernel lines. Smallest useful step: run that restricted search at length five + with the coefficient-class relaxation of #6097. +2. Same for `F5` and for odd characteristic generally, where `#6097`'s even + pairing has no direct analogue. +3. Widths above two: does the `2 x 2` line-exclusion argument extend to rank-one + idempotents in `M_d(F)`, where the collapse `N_i N_j = N_j` still holds for a + common image line but the target is a `d`-fold diagonal? diff --git a/research/diagonal-pair-line-separation/SOURCES.json b/research/diagonal-pair-line-separation/SOURCES.json new file mode 100644 index 0000000000..09ef394adc --- /dev/null +++ b/research/diagonal-pair-line-separation/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "75d77b328ea02ded535e7f23aee5b1e55d0bb1a8", + "sha256": "154c3d30455d778fd3343b6b4851f0fa4665f0f7625b0adb3675e2bafbbf6bf1" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/diagonal-pair-five-call-collisions/PROOF.md", + "usage": "provenance", + "git_blob": "75a4586f3ab6f3533ba4660a3178aaa226ca38c6", + "sha256": "3d607f594f34c5779508f70bd6afc76989107c5f74e0522021305e8cf9b538b0" + }, + { + "path": "research/diagonal-pair-five-call-collisions/README.md", + "usage": "provenance", + "git_blob": "cebd2e061c6cf8d502a1d55fb25687899c2465cd", + "sha256": "c40dad749ceaf46d78984f1a084d1b51310db538ffc113f8f30c7124f8a85832" + }, + { + "path": "research/diagonal-pair-five-call-collisions/TASK.json", + "usage": "provenance", + "git_blob": "da30f03b65a5ae3aaf94f1e4098be280a49a13a6", + "sha256": "14cbec29ffc99ab83d46bc3a1180f0167e68bd69a9f6a2d0e54c70097d8f8c8e" + } + ] +} \ No newline at end of file diff --git a/research/diagonal-pair-line-separation/TASK.json b/research/diagonal-pair-line-separation/TASK.json new file mode 100644 index 0000000000..6901267abf --- /dev/null +++ b/research/diagonal-pair-line-separation/TASK.json @@ -0,0 +1,107 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 8, + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "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 a common image line or a common kernel line can never realise the width-two diagonal-pair target at any word length over any field, and that at most two calls never suffice under the #6097 target hypotheses.", + "scope_change_reason": "The explicit field-extension question stored in JoyboyBrian's merged #6097 package replaces the generic interface-lemma task; formal group-algebra obstruction only, no native implementation.", + "bottleneck_link": "A scoped exclusion narrows the open F4/F5/odd-characteristic register search to tuples with at least two image lines and two kernel lines; no primitive saving or complete BIT supplier is claimed.", + "budget_minutes": 45, + "stop_rule": "One written line-exclusion lemma with exact finite corroboration; no claim about the general F4 or odd-characteristic six-call floor.", + "outcome": "completed", + "evidence": "PROOF.md and registered verify.py: projector inventories 6/12/20/30, ordered collapse pairs 24/72/160/300, subset collapses and vanishing determinants over F2, F3, F4, F5, two-call diagonal forcing, six-call positive control and mixed-line negative control.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Does the six-call diagonal-pair floor hold over F4?", + "why_it_matters": "It is the remaining field scope of the width-two question in #6097.", + "first_step": "Run the coefficient-class relaxation of #6097 on the #6609 representatives restricted to tuples with at least two image lines and two kernel lines.", + "blocked_by": "The 267,072 five-call F4 representatives have not been searched." + }, + { + "question": "Does the six-call floor hold over F5 and general odd characteristic?", + "why_it_matters": "The even-pairing argument in #6097 has no direct odd-characteristic analogue.", + "first_step": "Replace parity pairing by the coefficient-class constraints of the target field.", + "blocked_by": "No sound relaxation is known to reject the larger odd-characteristic domains." + }, + { + "question": "Does the line-exclusion argument extend to rank-one idempotents in M_d(F) for d above two?", + "why_it_matters": "It would remove the same-image and same-kernel families at larger widths.", + "first_step": "Repeat the collapse N_i N_j = N_j and the rank-one factorisation at d above two.", + "blocked_by": "The d-fold diagonal target and the paid-call model at larger widths are not specified here." + } + ] +} \ No newline at end of file diff --git a/research/diagonal-pair-line-separation/VERIFY.json b/research/diagonal-pair-line-separation/VERIFY.json new file mode 100644 index 0000000000..aab68e1fc2 --- /dev/null +++ b/research/diagonal-pair-line-separation/VERIFY.json @@ -0,0 +1,19 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": ["{python}", "-B", "-W", "error", "{package}/verify.py"], + "timeout_seconds": 60, + "checks": "Projector inventories 6/12/20/30, ordered same-image and same-kernel collapse pairs, subset collapse, vanishing determinant of P-I over F2/F3/F4/F5, two-call diagonal forcing, six-call positive control and mixed-line negative control." + }, + { + "argv": ["{python}", "-O", "-B", "-W", "error", "{package}/verify.py"], + "timeout_seconds": 60, + "checks": "Same exact checks with optimisations enabled; all assertions are explicit raises." + } + ] +} diff --git a/research/diagonal-pair-line-separation/verify.py b/research/diagonal-pair-line-separation/verify.py new file mode 100644 index 0000000000..c6c4cb532f --- /dev/null +++ b/research/diagonal-pair-line-separation/verify.py @@ -0,0 +1,321 @@ +#!/usr/bin/env python3 +"""Same-image-line and same-kernel-line exclusion for the diagonal-pair word. + +Standard library only. Exact finite-field arithmetic; the group algebra is the +free group on the call positions, with words as multisets of call positions (the free abelian group), so a +vanishing group-algebra element is a coefficient-wise vanishing identity. +""" +import itertools +import json + +# ---------------------------------------------------------------- fields + +class PrimeField: + def __init__(self, p): + self.q = p + self.elements = tuple(range(p)) + self.zero = 0 + self.one = 1 + + def add(self, a, b): + return (a + b) % self.q + + def mul(self, a, b): + return (a * b) % self.q + + def neg(self, a): + return (-a) % self.q + + def inv(self, a): + for b in self.elements: + if self.mul(a, b) == self.one: + return b + raise ValueError('not invertible') + + +class GF4: + q = 4 + elements = (0, 1, 2, 3) + zero = 0 + one = 1 + MUL = ((0, 0, 0, 0), (0, 1, 2, 3), (0, 2, 3, 1), (0, 3, 1, 2)) + + def add(self, a, b): + return a ^ b + + def mul(self, a, b): + return self.MUL[a][b] + + def neg(self, a): + return a + + def inv(self, a): + for b in self.elements: + if self.mul(a, b) == self.one: + return b + raise ValueError('not invertible') + + +FIELDS = (PrimeField(2), PrimeField(3), GF4(), PrimeField(5)) + +# ---------------------------------------------------------------- matrices + +def mmul(F, A, B): + return (F.add(F.mul(A[0], B[0]), F.mul(A[1], B[2])), + F.add(F.mul(A[0], B[1]), F.mul(A[1], B[3])), + F.add(F.mul(A[2], B[0]), F.mul(A[3], B[2])), + F.add(F.mul(A[2], B[1]), F.mul(A[3], B[3]))) + + +def madd(F, A, B): + return tuple(F.add(x, y) for x, y in zip(A, B)) + + +def mscale(F, c, A): + return tuple(F.mul(c, x) for x in A) + + +I2 = (1, 0, 0, 1) + + +def projectors(F): + out = [] + for a in F.elements: + for b in F.elements: + for c in F.elements: + for d in F.elements: + N = (a, b, c, d) + if mmul(F, N, N) != N: + continue + if F.add(a, d) != F.one: + continue + out.append(N) + return tuple(out) + + +def normalise(F, v): + for x in v: + if x != F.zero: + inv = F.inv(x) + return tuple(F.mul(inv, y) for y in v) + return None + + +def image_line(F, N): + a, b, c, d = N + for v in ((a, c), (b, d)): + w = normalise(F, v) + if w is not None: + return w + raise ValueError('zero image') + + +def kernel_line(F, N): + a, b, c, d = N + for v in ((b, F.neg(a)), (d, F.neg(c))): + w = normalise(F, v) + if w is not None: + # keep only vectors that really lie in the kernel + if (F.add(F.mul(a, w[0]), F.mul(b, w[1])) == F.zero and + F.add(F.mul(c, w[0]), F.mul(d, w[1])) == F.zero): + return w + raise ValueError('no kernel vector found') + +# ---------------------------------------------------------------- group algebra + +def gadd(A, B, F): + out = dict(A) + for w, c in B.items(): + v = F.add(out.get(w, F.zero), c) + if v == F.zero: + out.pop(w, None) + else: + out[w] = v + return out + + +def gmul(A, B, F): + # commutative group algebra: words are multisets of call positions + out = {} + for w1, c1 in A.items(): + for w2, c2 in B.items(): + w = tuple(sorted(w1 + w2)) + v = F.add(out.get(w, F.zero), F.mul(c1, c2)) + if v == F.zero: + out.pop(w, None) + else: + out[w] = v + return out + + +def gscale(A, c, F): + if c == F.zero: + return {} + return {w: F.mul(c, v) for w, v in A.items() if F.mul(c, v) != F.zero} + + +def gneg(A, F): + return {w: F.neg(v) for w, v in A.items() if F.neg(v) != F.zero} + + +def expand(F, Ns): + """Return the four entries of the product as group-algebra elements. + + Ward 0 of the dict is the empty word (the identity of the free group). + """ + terms = {(): I2} + for i, N in enumerate(Ns): + nxt = {} + for mask, C in terms.items(): + left = mmul(F, C, madd(F, I2, mscale(F, F.neg(F.one), N))) + right = mmul(F, C, N) + nxt[mask] = left + nxt[mask + (i,)] = right + terms = nxt + entries = [{}, {}, {}, {}] + for mask, C in terms.items(): + for e in range(4): + if C[e] != F.zero: + entries[e][mask] = C[e] + return entries + + +def minor(F, entries): + A = [dict(entries[e]) for e in range(4)] + A[0] = gadd(A[0], {(): F.neg(F.one)}, F) + A[3] = gadd(A[3], {(): F.neg(F.one)}, F) + return gadd(gmul(A[0], A[3], F), gneg(gmul(A[1], A[2], F), F), F) + +# ---------------------------------------------------------------- main + +def require(cond, msg): + if not cond: + raise SystemExit('FAIL ' + msg) + + +def same_class(projector_list, key): + classes = {} + for N in projector_list: + classes.setdefault(key(N), []).append(N) + return classes + + +def main(): + report = {} + for F in FIELDS: + q = F.q + inv = projectors(F) + require(len(inv) == q * (q + 1), + 'projector inventory %d for q=%d' % (len(inv), q)) + require(all(mmul(F, N, N) == N for N in inv), 'idempotence') + require(all(F.add(N[0], N[3]) == F.one for N in inv), 'trace one') + + by_image = same_class(inv, lambda N: image_line(F, N)) + by_kernel = same_class(inv, lambda N: kernel_line(F, N)) + require(len(by_image) == q + 1, 'image line count') + require(len(by_kernel) == q + 1, 'kernel line count') + require(all(len(v) == q for v in by_image.values()), 'image class size') + require(all(len(v) == q for v in by_kernel.values()), 'kernel class size') + + pairs = 0 + for cls in by_image.values(): + for X in cls: + for Y in cls: + require(mmul(F, X, Y) == Y, 'image collapse') + pairs += 1 + for cls in by_kernel.values(): + for X in cls: + for Y in cls: + require(mmul(F, X, Y) == X, 'kernel collapse') + pairs += 1 + + # subset collapse and vanishing minors, bounded by tuple length + max_len = 5 if q <= 3 else 4 + tuples = 0 + subs = 0 + minors = 0 + for cls in by_image.values(): + for k in range(1, max_len + 1): + for Ns in _product(cls, k): + tuples += 1 + for mask in range(1, 1 << k): + prod = I2 + last = None + for i in range(k): + if mask >> i & 1: + prod = mmul(F, prod, Ns[i]) + last = Ns[i] + require(prod == last, 'subset collapse to last') + subs += 1 + M = minor(F, expand(F, Ns)) + require(M == {}, 'same-image minor did not vanish') + minors += 1 + for cls in by_kernel.values(): + for k in range(1, max_len + 1): + for Ns in _product(cls, k): + tuples += 1 + for mask in range(1, 1 << k): + prod = I2 + first = None + for i in range(k): + if mask >> i & 1: + prod = mmul(F, prod, Ns[i]) + if first is None: + first = Ns[i] + require(prod == first, 'subset collapse to first') + subs += 1 + M = minor(F, expand(F, Ns)) + require(M == {}, 'same-kernel minor did not vanish') + minors += 1 + + # two-call normal form: with N1 = E00, diag(diag([g1],1) (I+t2 N2)) + # forces N2 diagonal, checked in the free group on two letters. + E00 = (1, 0, 0, 0) + t2 = {(): F.one, (1,): F.one} + two_call = 0 + for N2 in inv: + entries = expand(F, (E00, N2)) # free group on two letters + diag_q = (entries[1] == {} and entries[2] == {}) + diag_n = (N2[1] == F.zero and N2[2] == F.zero) + require(diag_q == diag_n, 'two-call diagonal forcing') + two_call += 1 + + report[q] = { + 'projectors': len(inv), + 'ordered_collapse_pairs': pairs, + 'same_line_tuples': tuples, + 'subset_collapses': subs, + 'vanishing_minors': minors, + 'two_call_projectors': two_call, + 'max_tuple_length': max_len, + } + + _controls() + print('PASS_DIAGONAL_PAIR_LINE_SEPARATION ' + + json.dumps(report, sort_keys=True)) + + +def _product(cls, k): + return itertools.product(cls, repeat=k) + + +def _controls(): + F = PrimeField(2) + E00 = (1, 0, 0, 0) + E11 = (0, 0, 0, 1) + # six-call F2 word: diag([g1 g2 g3], [g4 g5 g6]); the minor is nonzero + w = (E00, E00, E00, E11, E11, E11) + M = minor(F, expand(F, w)) + require(M != {}, 'six-call positive control minor vanished') + expected = {(0, 1, 2): 1, (3, 4, 5): 1, (0, 1, 2, 3, 4, 5): 1, (): 1} + require(M == expected, 'six-call minor coefficients') + # mixing image lines can give a nonzero minor: E00 then E11 is diagonal + # with two distinct targets, so (P-I) has rank two there. + require(image_line(F, E11) != image_line(F, E00), 'control lines coincide') + require(minor(F, expand(F, (E00, E11))) != {}, 'mixed-line control vanished') + # a same-image pair does vanish (already covered above, repeat explicitly) + require(minor(F, expand(F, (E00, E00))) == {}, 'same-image control') + + +if __name__ == '__main__': + main()