[petalas]

Prove that a common image line or a common kernel line can never realise the width-two diagonal-pair target, at any word length and over any field, and that at most two calls never suffice under the target hypotheses of #6097.

Result and claim type

Scoped written proof with exact finite corroboration. No new κ, no supplier, no selected-frontier change.

Setting: the rank-one-idempotent register model of Wentao Li's #4089, as used by Nick Petalas's #6038, Josie Elliston's #6048/#6137 and JoyboyBrian's #6097. For a field F, a group G, labels L and a rank-one idempotent N ∈ M₂(F), a call is D_N(g) = (I−N) + [g]N.

Theorem 1. Let N₁,…,N_k be rank-one idempotents that share a common image line, or share a common kernel line. Then for every labels and every k ≥ 0, the product ∏ D_{N_i}(g_i) is never diag([a],[b]) with a ≠ e ≠ b. This holds over every field and every group.

Proof sketch: with a common image line, N_i = u v_iᵀ and v_iᵀu = 1, so N_iN_j = N_j. Every subset product collapses to its last projector, and the whole product is I + u wᵀ with u a field vector and w over F[G]. Hence det(P−I) = 0. For a ≠ b the element ([a]−1)([b]−1) is nonzero in F[G] over every field, so a diagonal pair with distinct targets is impossible. The common-kernel case is the transpose argument.

Corollary. Any word attaining diag([a],[b]) with a ≠ b, neither target a product of at most two labels, must contain two projectors with distinct image lines and two with distinct kernel lines. In particular no family with a single image line, a single kernel line or one repeated projector can attain the pair at any length.

Theorem 2. Over every field and group, no product of at most two calls equals diag([a],[b]) when a ≠ b and neither target is a product of at most two labels. Without the length hypothesis two calls do suffice: D_{E00}(x) D_{E11}(y) = diag([x],[y]).

This is the field/width scope left open by Open next question 2 of JoyboyBrian's #6097 ("does the six-call floor extend to odd characteristic or F4?", blocked by "even pairing is specific to F2"). It answers that question only in part: a whole family of candidate counterexamples is removed at every length and field, and lengths 0–2 are removed. The general F4, F5, odd-characteristic and larger-width six-call floors remain open.

Evidence and reproduction

Package: research/diagonal-pair-line-separation/ (README.md, PROOF.md, TASK.json, SOURCES.json, VERIFY.json, verify.py).

/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

verify.py is standard-library only, about 0.7 s per run, and prints one line beginning PASS_DIAGONAL_PAIR_LINE_SEPARATION. It builds each field from its arithmetic, derives the rank-one idempotent inventory from N² = N and tr(N) = 1, and checks by exact arithmetic:

• inventories q(q+1) = 6, 12, 20, 30 over F2, F3, F4, F5;
• all 24 / 72 / 160 / 300 ordered same-image and same-kernel pairs satisfy the collapse N_iN_j = N_j or its transpose;
• 7,812 / 71,736 / 43,400 / 123,960 nonempty subset products collapse to the last or first projector;
• the determinant of P−I vanishes for all 372 / 2,904 / 3,400 / 9,360 enumerated same-line tuples at lengths up to 5 over F2, F3 and up to 4 over F4, F5, computed by exact expansion in the group algebra of the free abelian group on the call positions;
• the two-call diagonal-forcing step for every projector over each field;
• the positive control D_{E00}(x)³ D_{E11}(y)³ = diag([x³],[y³]) with its four predicted coefficients, and the mixed-line negative 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. Checks raise explicit exceptions, so -O does not disable them.

Local status: both registered VERIFY commands, scripts/research_package.py and scripts/check_research_commit.py --check-source-history pass at head 2c2dad2058a4f01485214b7437b3e8b8d4d8f57c.

Limitations and unrun obligations

• Theorems 1 and 2 only. Nothing here bounds tuples with two or more image lines, which is where any counterexample must live.
• Theorem 2 is a written argument; only its diagonal-forcing step is machine checked.
• The finite enumeration corroborates the collapse and the determinant identity. It is not a proof kernel and not a complete tuple census.
• The general F4, F5, odd-characteristic and larger-width six-call floors are not decided.
• No native tariff, compiler, supplier or multiplication bound is inferred.

Related open work

No open PR was found that studies the same diagonal-pair line separation. The own-open-PR check at head 2c2dad2058a4f01485214b7437b3e8b8d4d8f57c also found none from this account on this object; the nearest open one, #7213, proves an exact diagonal-rank cost in a different group-gate model, and no number is compared with it. The source question is JoyboyBrian's merged #6097; Josie Elliston's merged #6048/#6137 supply the width-two framing and the four-call floor; Nick Petalas's merged #6609 supplies a related symmetry quotient of the same projector domain and is cited as related work, not used as a step. No number in this PR depends on another open PR.

Open next questions

1. Does the six-call floor hold over F4? The remaining search is the 267,072 five-call representatives of Count exact symmetry quotients for width-two projector words (no κ) #6609 restricted to tuples with at least two image lines and two kernel lines.
2. Same for F5 and general odd characteristic, where the even-pairing argument of Prove the width-two F2 six-call floor with genuine group-word collisions #6097 has no direct analogue.
3. Does the line-exclusion argument extend to rank-one idempotents in M_d(F) at widths above two, where the same collapse holds but the target is a d-fold diagonal?

CI notes

Head 2c2dad2058a4f01485214b7437b3e8b8d4d8f57c. Run 43108616300, job 130818414715: the plan job failed and the replay job was skipped, so CI certified nothing for this package. Both registered VERIFY commands, scripts/research_package.py and scripts/check_research_commit.py --check-source-history pass locally at this head.

The failure is repository-level and independent of this branch. plan ran the onboarding helper tests and failed exactly one of 760 tests (24 skipped): test_research_current_status.CurrentCiNavigationTests.test_current_ci_section_matches_selected_record, with

AssertionError: '`make frontier7000-verify`' not found in '# CI verification ... ## Current selected-family replay: #6030 ...'

At the merge base e54523517, certificates/selected-result.json names make frontier7000-verify and the pr7000 review, while docs/ci-verification.md still describes #6030 and make frontier6030-verify. The test requires SELECTED['reproduce'] to occur in the current section of that doc, so it fails on main's own files, before any package of this branch is read.

The same single test with failures=1, skipped=24 fails in the same job on runs 42905094314 (head d14f787dc0), 42903313790 (head 020d581d98) and 43107053327 (head a9b4838571, identical assertion text). No package check was run by CI and no CI pass is claimed.