From 362cead4c481b2d9856baa07b711687425cfe002 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Tue, 27 Oct 2026 21:18:12 +0000 Subject: [PATCH] feat(research): prove shear target and inverse need eight calls Answer the open question of PR #3905: diag([B],[B^-1]) with B = X^2Y^2 in the integer-shear alphabet costs exactly eight paid calls. A complete ordered-subproduct census shows no word of length at most seven covers both labels, so the cover theorem of research/group-subproduct-cover (PR #5394) gives the lower bound; the coordinate-projector word attains it. --- research/sl2z-inverse-pair-cover/README.md | 166 ++++++++++ research/sl2z-inverse-pair-cover/SOURCES.json | 30 ++ research/sl2z-inverse-pair-cover/TASK.json | 70 ++++ research/sl2z-inverse-pair-cover/VERIFY.json | 32 ++ research/sl2z-inverse-pair-cover/verify.py | 307 ++++++++++++++++++ 5 files changed, 605 insertions(+) create mode 100644 research/sl2z-inverse-pair-cover/README.md create mode 100644 research/sl2z-inverse-pair-cover/SOURCES.json create mode 100644 research/sl2z-inverse-pair-cover/TASK.json create mode 100644 research/sl2z-inverse-pair-cover/VERIFY.json create mode 100644 research/sl2z-inverse-pair-cover/verify.py diff --git a/research/sl2z-inverse-pair-cover/README.md b/research/sl2z-inverse-pair-cover/README.md new file mode 100644 index 0000000000..821f3ac939 --- /dev/null +++ b/research/sl2z-inverse-pair-cover/README.md @@ -0,0 +1,166 @@ +# An integer-shear target and its inverse share no paid call + +**Scoped exact minimum in a formal register model. No new κ, supplier or +selected-frontier change.** + +This contribution was produced by Nick Petalas. Apache-2.0. + +## Question + +PR [#3905](https://github.com/CrocSwap/integer-mult-bounds/pull/3905) +(1337isnot1337, `research/sl2z-four-call-native-target`, head +`b27bf4c72a822b21f483e08cb3241ad9d165b66f`) fixes the shear group + +$$ +G=\langle X,Y\rangle\leq\mathrm{SL}_2(\mathbb Z),\qquad +X=\begin{pmatrix}1&1\\0&1\end{pmatrix},\quad +Y=\begin{pmatrix}1&0\\1&1\end{pmatrix}, +$$ + +the paid labels $\mathcal A=\{X,X^{-1},Y,Y^{-1}\}$, scalar ring +$\mathbb F_2[G]$, and the one-call factor +$D_N([g])=I_2+([g]+[e])N$ with $N$ a rank-one idempotent in +$M_2(\mathbb F_2)$. It proves that $\mathrm{diag}([B],[e])$, with +$B=X^2Y^2=\begin{pmatrix}5&2\\2&1\end{pmatrix}$, costs exactly four calls. + +Its Open next question asks whether the two-role endpoint + +$$ +T=\mathrm{diag}([B],[B^{-1}]) +$$ + +can share paid factors across roles and cost fewer than the eight calls of +the coordinate-projector word. + +## Result + +**The exact minimum is eight calls.** Cross-role sharing saves nothing. + +The lower bound holds in a larger class than #3905's: any $\mathbb F_2$ +frames $N$ (any rank, unit cost), arbitrary interleaved scalar maps, finite +clean or dirty workspace, and any change to workspace. The upper bound uses +only #3905's rank-one idempotents, two roles, no workspace and no cleanup. + +### Lower bound + +Over $\mathbb F_2$, $I+([g]+[e])N=(I-N)[e]+N[g]$. So every #3905 factor +is a gate of Ali Romman's merged +[`research/group-subproduct-cover`](../group-subproduct-cover/README.md) +(PR [#5394](https://github.com/CrocSwap/integer-mult-bounds/pull/5394)). +Its cover theorem ([PROOF.md](../group-subproduct-cover/PROOF.md), section 2) +states that, with the label set fixed, the paid count of a diagonal target +equals the least $k$ for which one word $w=(g_1,\dots,g_k)$ over the labels +has every target label in its ordered subproduct set + +$$ +S(w)=\{g_1^{b_1}\cdots g_k^{b_k}: b_j\in\{0,1\}\}. +$$ + +We cite that theorem and do not re-prove or audit it. The new step is the +cover number of $\{B,B^{-1}\}$ over $\mathcal A$. The verifier builds +$S(w)$ for **every** word of length $0$ to $8$ (87,381 words in total). +No word of length at most seven has both $B$ and $B^{-1}$ in $S(w)$. +Therefore every circuit for $T$ needs at least eight paid calls. + +The census also records: + +- $B$ and $B^{-1}$ each have exactly one four-letter word, `XXYY` and + `yyxx` (lower case is the inverse label), and no shorter one. +- Exactly 124 words of length eight cover both targets. +- In 54 of them, some subproduct mask for $B$ and some mask for $B^{-1}$ + share a position. Positions can be shared at length eight, but never at + a lower length. + +### Upper bound + +With $P=E_{11}$ and $Q=E_{22}$, both rank-one idempotents, + +$$ +D_P([X])^2D_P([Y])^2\,D_Q([Y^{-1}])^2D_Q([X^{-1}])^2 +=\mathrm{diag}([X^2Y^2],[Y^{-2}X^{-2}]) +=\mathrm{diag}([B],[B^{-1}]). +$$ + +The verifier checks this as an equality in $M_2(\mathbb F_2[G])$ and on 16 +explicit dirty columns. + +### Complete bill in the stated model + +| Item | Count | +| --- | ---: | +| Paid factors (labels `X X Y Y y y x x`) | 8 | +| Scalar roles | 2, both arbitrary dirty inputs | +| Scratch roles | 0 | +| Copy, reset, restore or cleanup calls | 0 | +| Uncharged address updates | 0 | + +## Evidence + +`verify.py` uses the standard library only. It checks: + +1. #3905's factor equals the #5394 gate for all six rank-one idempotents of + $M_2(\mathbb F_2)$ and all four labels (the 24 legal factors); +2. the complete ordered-subproduct census above; +3. the eight-call identity and dirty columns; +4. eleven controls: each of the eight single-factor deletions fails, the + reordered word `XYXY` fails, the pair $\{B,X^2\}$ is found to share one + four-letter cover (so the census detects sharing when it exists), and + 40 random five-factor circuits with arbitrary $\mathbb F_2$ frames and + interleaved scalar matrices keep all support inside $S(w)$. + +A second cover-number routine in the same script (breadth-first over the +sets $S(w)$, separate from the census loop) agrees: no cover at length seven, a cover at length eight. + +## Reproduce + +From the repository root, with CPython 3.12: + +```sh +python3.12 -W error -B research/sl2z-inverse-pair-cover/verify.py +python3.12 -W error -O -B research/sl2z-inverse-pair-cover/verify.py +python3.12 -B scripts/research_package.py --package research/sl2z-inverse-pair-cover +``` + +Expected marker (about one second per run): + +```text +PASS_SL2Z_INVERSE_PAIR_COVER legal_factors=24 census_words=87381 max_both_cover_below_8=0 length8_both_covers=124 overlapping_mask_covers=54 geodesics=1+1 minimum_calls=8 controls=11 no_new_kappa +``` + +## Claim type and limits + +This is a **scoped exact minimum**: a finite certificate (the census) +combined with a cited written theorem (#5394's cover theorem). The census +is complete for its stated alphabet and lengths; the lower bound for +arbitrary frames and workspace rests on the #5394 proof, which is not +re-checked here. + +It is not a supplier, native implementation or complete multiplication +theorem. Group labels are formal basis elements. Native conversion of the +shear action, its physical cost and any recursive moment are unpriced; see +the commutative-carrier obstruction (#3937), binary carrier (#3947) and +moment results (#4126, #4146) for those questions. The result holds only +for the four-label alphabet: a larger alphabet can change the cover number. + +## Open next questions + +1. **Higher powers.** Is the paid count of $\mathrm{diag}([B^k],[B^{-k}])$ + exactly $8k$ for every $k\ge 2$? A cross-role saving for a higher power + would be the first sharing gain for an inverse pair here. First step: a + pruned census for $k=2$ up to length 15, or a general no-sharing lemma + from the shortest words for $B^k$ and $B^{-k}$. Blocker: the naive census + grows as $4^L$. +2. **One added label.** Does the eight-call minimum survive if the order-four + element $S=XY^{-1}X$, or any single extra label, joins the paid alphabet? + First step: repeat the census over five labels through length seven. + Blocker: each added label needs its own native price; a formal count is + not a supplier. + +## Credit + +- 1337isnot1337: model, single-target four-call theorem and this open + question (PR #3905, cited, not audited). +- Ali Romman / aliromman: the ordered-subproduct cover theorem in + `research/group-subproduct-cover` (PR #5394), used for the lower bound. +- The register-model lineage credited by #3905 (PRs #288 and #203) is + retained. diff --git a/research/sl2z-inverse-pair-cover/SOURCES.json b/research/sl2z-inverse-pair-cover/SOURCES.json new file mode 100644 index 0000000000..a07e81a141 --- /dev/null +++ b/research/sl2z-inverse-pair-cover/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8", + "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/group-subproduct-cover/PROOF.md", + "usage": "provenance", + "git_blob": "308e63dcc668b0089b4a0c5152dda0733b01fed5", + "sha256": "7392dca9e7258dcdb4802a3c9f60cd8e5ccced271950a4ce2e4823f449586c00" + }, + { + "path": "research/group-subproduct-cover/README.md", + "usage": "provenance", + "git_blob": "36faba920c546d36f3a51a026e8e84d925acf723", + "sha256": "b9241c29301d2d20af35fe9f09ff2b0e7e7aca0566394b8e4c7708924e59d161" + } + ] +} diff --git a/research/sl2z-inverse-pair-cover/TASK.json b/research/sl2z-inverse-pair-cover/TASK.json new file mode 100644 index 0000000000..f99cff6b2d --- /dev/null +++ b/research/sl2z-inverse-pair-cover/TASK.json @@ -0,0 +1,70 @@ +{ + "schema_version": 1, + "task_id": "bit-new-register-model", + "priority_revision": 8, + "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "original_card": { + "id": "bit-new-register-model", + "question": "Can an explicitly larger or nonabelian register model escape the scoped three-register obstruction?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/bit-three-register-lower-bound/README.md", + "certificates/selected-result.json", + "research/bit-gl3-mixed-targets-length10/README.md", + "docs/research/community-efficient1000-review.md" + ], + "methods": [ + "Construct the smallest exact identity in a newly specified legal operation alphabet.", + "Derive a target-specific relaxation bound for that same explicit alphabet." + ], + "acceptance_gate": "Name the changed hypothesis, all counted roles and a uniform identity; finite column tests alone do not certify it. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "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": "First compare the alphabet, role count and length with the fully replayed #1974 census and #2027 mixed-root tariff. Identify a changed premise and a legal native implementation; then price one smallest completed instance before searching larger words.", + "bottleneck_link": "A small-width completed saving changes the bit primitive; a finite-address identity alone is insufficient.", + "allowed_variations": [ + "Choose a fixed larger register count or a specified nonabelian operation family." + ], + "scope_change_triggers": [ + "Remaining inside the already-excluded three-register abelian model.", + "Repeating the two-register GL3 census or a covered three-register length without changing a hypothesis; a formal group-algebra word without native conversion is a partial result." + ], + "overlap_terms": [ + "three-register", + "nonabelian", + "group algebra" + ] + }, + "scope_status": "changed", + "actual_scope": "Determine the exact paid-call minimum of the two-role endpoint diag([B],[B^-1]), B=X^2Y^2, in the PR #3905 integer-shear alphabet, over all F2 frames, interleaved scalar maps, finite workspace and dirty inputs.", + "scope_change_reason": "This answers the Open next question of PR #3905, a specified nonabelian operation family allowed by this card. It refines the card to one two-role cross-sharing question rather than a new register identity.", + "bottleneck_link": "Side result in the formal register model. It shows that cross-role sharing gives no saving for this inverse pair, so a cheaper inverse-pair word must change the alphabet or gate model. No native conversion, supplier or kappa effect.", + "budget_minutes": 60, + "stop_rule": "Ship the first exact minimum. Do not extend to powers B^k, other alphabets or native implementations.", + "outcome": "completed", + "evidence": "verify.py checks the #3905/#5394 gate identity for all 24 legal factors, a complete ordered-subproduct census of all 87,381 words of length at most 8, the exact eight-call identity in M2(F2[G]) with dirty columns, and 11 controls. The lower bound applies the cited #5394 cover theorem to this census.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "What is the exact paid count of diag([B^k],[B^-k]) for k>=2, and does it always equal 8k?", + "why_it_matters": "A cross-role saving for a higher power would be the first sharing gain for an inverse pair in this alphabet.", + "first_step": "Run the same ordered-subproduct census at lengths up to 15 for k=2 with pruning by the single-target bound, or prove a general no-sharing lemma from the shortest words for B^k and B^-k.", + "blocked_by": "The naive census grows as 4^L; a proof needs a structural argument about subproducts that evaluate to B^k." + }, + { + "question": "Does the eight-call minimum survive if one adds the order-four element S = X Y^-1 X, or any single extra label, to the paid alphabet?", + "why_it_matters": "Identifies which alphabet change, if any, makes inverse-pair sharing profitable.", + "first_step": "Repeat the census over the five-label alphabet through length seven.", + "blocked_by": "Each added label needs its own native implementation and price; the formal count alone is not a supplier." + } + ] +} diff --git a/research/sl2z-inverse-pair-cover/VERIFY.json b/research/sl2z-inverse-pair-cover/VERIFY.json new file mode 100644 index 0000000000..3b81dc6d47 --- /dev/null +++ b/research/sl2z-inverse-pair-cover/VERIFY.json @@ -0,0 +1,32 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Gate-form identity for all 24 legal factors; complete ordered-subproduct census of all 87,381 shear words of length 0..8 (no length<=7 word covers B and B^-1; 124 length-8 covers, 54 with overlapping masks); exact eight-call identity in M2(F2[G]) with dirty columns; deletion, reorder, sharing and support-lemma controls." + }, + { + "argv": [ + "{python}", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "The same checks under optimized Python; the verifier uses explicit checks, not assert." + } + ] +} diff --git a/research/sl2z-inverse-pair-cover/verify.py b/research/sl2z-inverse-pair-cover/verify.py new file mode 100644 index 0000000000..bcede48135 --- /dev/null +++ b/research/sl2z-inverse-pair-cover/verify.py @@ -0,0 +1,307 @@ +#!/usr/bin/env python3 +"""Exact paid-call minimum for diag([B],[B^-1]) in the integer-shear alphabet. + +Model: PR #3905. G = in SL2(Z), labels X^{+-1}, Y^{+-1}, scalar +ring F2[G], paid factor I + ([g] + [e]) N with N a rank-one idempotent in +M2(F2). Over F2 this is the gate (I - N)[e] + N[g] of the merged +research/group-subproduct-cover package (PR #5394), whose cover theorem +gives the lower bound once the ordered-subproduct cover number is known. + +This script checks: + 1. the two gate forms agree for every rank-one idempotent and label; + 2. a complete census of label sequences of length 0..8: none of length + at most seven has both B and B^-1 among its ordered subproducts; + 3. the eight-call coordinate-projector word equals diag([B],[B^-1]) in + the formal algebra M2(F2[G]); + 4. deletion, reordering, sharing and support-lemma controls. + +Standard library only. Read-only; no network, Git or file writes. +""" + +import itertools +import random +import sys + +# 2x2 integer matrices as tuples (a, b, c, d) = [[a, b], [c, d]]. +IDENTITY = (1, 0, 0, 1) +LABELS = { + "X": (1, 1, 0, 1), + "x": (1, -1, 0, 1), # X^-1 + "Y": (1, 0, 1, 1), + "y": (1, 0, -1, 1), # Y^-1 +} +LETTERS = "XxYy" +MAX_LENGTH = 8 + + +def mul(p, q): + a, b, c, d = p + e, f, g, h = q + return (a * e + b * g, a * f + b * h, c * e + d * g, c * f + d * h) + + +def evaluate(word): + m = IDENTITY + for letter in word: + m = mul(m, LABELS[letter]) + return m + + +B = evaluate("XXYY") +B_INV = evaluate("yyxx") + + +def fail(message): + print("FAIL_SL2Z_INVERSE_PAIR_COVER " + message) + sys.exit(1) + + +def require(condition, message): + if not condition: + fail(message) + + +# --------------------------------------------------------------------------- +# Formal algebra M_n(F2[G]). An entry is a frozenset of group elements: the +# support of an F2 combination, with addition as symmetric difference. + +def entry_mul(u, v): + out = set() + for g in u: + for h in v: + out ^= {mul(g, h)} + return frozenset(out) + + +def mat_mul(p, q): + n, inner, m = len(p), len(q), len(q[0]) + out = [] + for i in range(n): + row = [] + for j in range(m): + acc = set() + for k in range(inner): + acc ^= entry_mul(p[i][k], q[k][j]) + row.append(frozenset(acc)) + out.append(tuple(row)) + return tuple(out) + + +def scalar(matrix): + """Embed an F2 matrix as a formal matrix with coefficient [e].""" + return tuple( + tuple(frozenset({IDENTITY}) if x % 2 else frozenset() for x in row) + for row in matrix + ) + + +def gate_3905(n_matrix, letter): + """I + ([g] + [e]) N, the PR #3905 factor.""" + g = LABELS[letter] + size = len(n_matrix) + rows = [] + for i in range(size): + row = [] + for j in range(size): + acc = {IDENTITY} if i == j else set() + if n_matrix[i][j] % 2: + acc ^= {g} + acc ^= {IDENTITY} + row.append(frozenset(acc)) + rows.append(tuple(row)) + return tuple(rows) + + +def gate_5394(n_matrix, letter): + """(I - N)[e] + N[g], the PR #5394 gate, reduced over F2.""" + g = LABELS[letter] + size = len(n_matrix) + rows = [] + for i in range(size): + row = [] + for j in range(size): + acc = set() + if ((1 if i == j else 0) - n_matrix[i][j]) % 2: + acc ^= {IDENTITY} + if n_matrix[i][j] % 2: + acc ^= {g} + row.append(frozenset(acc)) + rows.append(tuple(row)) + return tuple(rows) + + +def product(factors): + out = factors[0] + for f in factors[1:]: + out = mat_mul(out, f) + return out + + +def rank_one_idempotents(): + found = [] + for bits in itertools.product((0, 1), repeat=4): + n_matrix = ((bits[0], bits[1]), (bits[2], bits[3])) + square = tuple( + tuple(sum(n_matrix[i][k] * n_matrix[k][j] for k in range(2)) % 2 for j in range(2)) + for i in range(2) + ) + det = (bits[0] * bits[3] - bits[1] * bits[2]) % 2 + if square == n_matrix and any(bits) and det == 0: + found.append(n_matrix) + return found + + +# --------------------------------------------------------------------------- +# Census of ordered-subproduct sets S(w) for every word w of length <= 8. + +def census(): + """Return per-length counts and the length-8 words covering both targets.""" + covers_b = [0] * (MAX_LENGTH + 1) + covers_inv = [0] * (MAX_LENGTH + 1) + covers_both = [0] * (MAX_LENGTH + 1) + words = [0] * (MAX_LENGTH + 1) + both_words = [] + stack = [("", frozenset({IDENTITY}))] + while stack: + word, subproducts = stack.pop() + k = len(word) + words[k] += 1 + has_b = B in subproducts + has_inv = B_INV in subproducts + covers_b[k] += has_b + covers_inv[k] += has_inv + if has_b and has_inv: + covers_both[k] += 1 + if k == MAX_LENGTH: + both_words.append(word) + if k == MAX_LENGTH: + continue + for letter in LETTERS: + g = LABELS[letter] + extended = subproducts | {mul(s, g) for s in subproducts} + stack.append((word + letter, frozenset(extended))) + return words, covers_b, covers_inv, covers_both, sorted(both_words) + + +def masks_for(word, target): + k = len(word) + out = [] + for mask in range(1 << k): + if evaluate(word[i] for i in range(k) if mask >> i & 1) == target: + out.append(mask) + return out + + +def cover_number(targets, limit): + """Least k <= limit with every target in one S(w); None if absent.""" + level = {frozenset({IDENTITY})} + for k in range(limit + 1): + if any(all(t in s for t in targets) for s in level): + return k + level = { + frozenset(s | {mul(x, LABELS[letter]) for x in s}) + for s in level + for letter in LETTERS + } + return None + + +def main(): + require(B == (5, 2, 2, 1), "B is not [[5,2],[2,1]]") + require(mul(B, B_INV) == IDENTITY, "B_INV is not the inverse of B") + + # 1. Gate identity and the 24 legal factors of PR #3905. + idempotents = rank_one_idempotents() + require(len(idempotents) == 6, "expected six rank-one idempotents in M2(F2)") + for n_matrix in idempotents: + for letter in LETTERS: + require( + gate_3905(n_matrix, letter) == gate_5394(n_matrix, letter), + "gate forms differ", + ) + legal_factors = len(idempotents) * len(LETTERS) + + # 2. Complete census. + words, covers_b, covers_inv, covers_both, both_words = census() + require(words == [4 ** k for k in range(MAX_LENGTH + 1)], "census word counts") + require(all(c == 0 for c in covers_both[: MAX_LENGTH]), "a word of length <= 7 covers both targets") + require(covers_both[MAX_LENGTH] == 124, "expected 124 covering words of length 8") + require(covers_b[3] == 0 and covers_inv[3] == 0, "a single target is covered below length 4") + require(covers_b[4] == 1 and covers_inv[4] == 1, "single-target covers at length 4") + geodesics_b = ["".join(w) for w in itertools.product(LETTERS, repeat=4) if evaluate(w) == B] + geodesics_inv = ["".join(w) for w in itertools.product(LETTERS, repeat=4) if evaluate(w) == B_INV] + require(geodesics_b == ["XXYY"] and geodesics_inv == ["yyxx"], "geodesic words") + overlapping = 0 + for word in both_words: + mb = masks_for(word, B) + mi = masks_for(word, B_INV) + require(mb and mi, "census cover lacks a mask") + if any(p & q for p in mb for q in mi): + overlapping += 1 + require(overlapping == 54, "expected 54 length-8 covers with an overlapping mask pair") + require("XXYYyyxx" in both_words, "coordinate-projector word missing from census") + + # 3. Eight-call construction in M2(F2[G]). + e11 = ((1, 0), (0, 0)) + e22 = ((0, 0), (0, 1)) + schedule = [(e11, "X"), (e11, "X"), (e11, "Y"), (e11, "Y"), + (e22, "y"), (e22, "y"), (e22, "x"), (e22, "x")] + target = ( + (frozenset({B}), frozenset()), + (frozenset(), frozenset({B_INV})), + ) + require(product([gate_3905(n, g) for n, g in schedule]) == target, "eight-call word") + # Dirty inputs: the endpoint is an operator identity, so (u, v) -> (Bu, B^-1 v) + # for every u, v in F2[G]. Check a few explicit dirty columns. + rng = random.Random(3905) + pool = [evaluate(w) for k in range(4) for w in itertools.product(LETTERS, repeat=k)] + for _ in range(16): + u = frozenset(rng.sample(pool, 3)) + v = frozenset(rng.sample(pool, 3)) + column = ((u,), (v,)) + out = mat_mul(product([gate_3905(n, g) for n, g in schedule]), column) + require(out == ((entry_mul(frozenset({B}), u),), (entry_mul(frozenset({B_INV}), v),)), + "dirty column") + + # 4. Controls. + controls = 0 + for drop in range(len(schedule)): + shorter = schedule[:drop] + schedule[drop + 1:] + require(product([gate_3905(n, g) for n, g in shorter]) != target, "deletion control") + controls += 1 + swapped = [(e11, "X"), (e11, "Y"), (e11, "X"), (e11, "Y")] + schedule[4:] + require(product([gate_3905(n, g) for n, g in swapped]) != target, "reorder control") + controls += 1 + # Sharing is detectable: B and X^2 share one four-letter cover. + require(cover_number([B, evaluate("XX")], 6) == 4, "sharing control") + require(cover_number([B, B_INV], 7) is None, "cover-number cross-check") + require(cover_number([B, B_INV], 8) == 8, "cover-number cross-check at 8") + controls += 1 + # Support lemma sanity: arbitrary F2 frames and interleaved scalar matrices + # never produce a group element outside S(w). + for _ in range(40): + word = "".join(rng.choice(LETTERS) for _ in range(5)) + factors = [] + for letter in word: + frame = tuple(tuple(rng.randrange(2) for _ in range(2)) for _ in range(2)) + mixer = tuple(tuple(rng.randrange(2) for _ in range(2)) for _ in range(2)) + factors.append(scalar(mixer)) + factors.append(gate_3905(frame, letter)) + result = product(factors) + allowed = {evaluate(word[i] for i in range(5) if m >> i & 1) for m in range(32)} + for row in result: + for entry in row: + require(entry <= allowed, "support lemma violated") + controls += 1 + + print( + "PASS_SL2Z_INVERSE_PAIR_COVER " + f"legal_factors={legal_factors} census_words={sum(words)} " + f"max_both_cover_below_8={max(covers_both[:MAX_LENGTH])} " + f"length8_both_covers={covers_both[MAX_LENGTH]} overlapping_mask_covers={overlapping} " + f"geodesics=1+1 minimum_calls=8 controls={controls} no_new_kappa" + ) + + +if __name__ == "__main__": + main()