diff --git a/research/two-write-spectator-projection/README.md b/research/two-write-spectator-projection/README.md new file mode 100644 index 0000000000..7eaec71019 --- /dev/null +++ b/research/two-write-spectator-projection/README.md @@ -0,0 +1,154 @@ +# Exactly two writes: a support-sensitive projector constraint + +**Scoped written lemma and exact finite corroboration; no new kappa.** This +continues Nick Petalas's PR6012 at `3d9d5eb2ae784356497771661960ad0455b137db`, +`research/two-three-cycles-every-dimension/PROOF.md`, Sections 2–4 and Open next +question 3. It derives the two-write analogue with all middle-label terms +retained. It does not exclude the residual ten-call case. + +## Model and projection + +Use PR6012's formal model `M_2(F2[GL_n(F2)])`, with ordinary matrix product for +address labels and row `k` represented by `e_k^T`. A call is +`D(g,N)=(I+N)+[g]N`, where `g=E_ij=I+e_i e_j^T` writes `i`, reads `j`, and +`N` is a rank-one binary idempotent. Every endpoint coefficient is formal. +Free scalar maps are normalized into the call projectors as in the source; +move scalar maps to one end by conjugating the projectors. Augmentation of +the endpoint `[c]I` forces that terminal scalar map to be `I`. Thus every +normalized subword has augmentation `I`. + +Suppose exactly two calls write coordinate `k`. Write the complete word as + +`P=A D(g,N) B D(h,M) C`, with `g=E_kj`, `h=E_kl`, `j,l != k`. + +The factors in `A,B,C` do not write `k`; all their address support belongs to +`S_k={b:e_k^T b=e_k^T}`. Write `B=sum_b [b] B_b`, and let `pi_k` retain only +labels in `S_k`. Define the **selected and relabelled** middle polynomial + +`T_(j,l)(B)=sum_(b in S_k : e_j^T b=e_l^T) [g b h] B_b`. + +Then the exact identity is + +`pi_k(P)=A ((I+N) B (I+M) + N T_(j,l)(B) M) C`. (1) + +Proof: expand the two calls into their four terms. The term using neither +address label lies in `S_k`. The two terms using exactly one lie outside it: +`S_k g S_k` and `S_k h S_k` are disjoint from the subgroup. In the double +term, put `r=e_j^T b`. Since `b` fixes row `k`, + +`e_k^T g b h = e_k^T + r + (1+r_k)e_l^T`. + +This equals `e_k^T` precisely when `r=e_l^T`: if `r_k=1`, equality would force +`r=0`, impossible for an invertible `b`; if `r_k=0`, it forces `r=e_l^T`. +Multiplication on either side by support in `S_k` preserves membership in +`S_k`, proving (1). In general `g b h` is not `b`, so merely filtering `B` +without relabelling is incorrect. All scalar matrix orders in (1) matter. + +## Equal and complementary projector pairs + +Let the endpoint be `[c]I`, as for the two equal coordinate 3-cycles. Put +`S=sum_(e_j^T b=e_l^T) B_b`, the augmentation of the selected middle terms. +The augmentation of `A,B,C` is `I`. + +If `c` fixes row `k`, applying augmentation to (1) gives + +`I=(I+N)(I+M)+N S M`. (2) + +Multiply (2) on the left by `I+N` to get `(I+N)M=0`, and on the right by +`I+M` to get `N(I+M)=0`. Thus `M=NM=N`. Equation (2) then reduces to +`N S N=N`. This is a necessary projector condition for **any restored +coordinate written exactly twice**, without restricting the intermediate reads. +The equality conclusion uses idempotence; it holds beyond rank one as well, +but only the stated rank-one source model is used here. + +If `c` moves row `k`, then `pi_k([c]I)=0`, so instead + +`0=(I+N)(I+M)+N S M`. (3) + +Left multiplication by `I+N` gives `(I+N)(I+M)=0`. This alone does not +force complementary projectors. Each paid call is an involution, so the inverse is a legal reversed word. +Apply the same argument to that inverse: +its two writer projectors occur in order `M,N`; every other label still fixes +row `k`. Since a subgroup is closed under inversion, `c^{-1}` also moves row +`k`. Thus `(I+M)(I+N)=0` as well. In dimension two, the first equality gives +`im(N)=ker(M)` and the second gives `im(M)=ker(N)`. Consequently `MN=NM=0`, +and the first equality now yields **`M=I+N`**. The two projections of the word +and its inverse are both essential. The remaining necessary coefficient +condition from (3) is `N S (I+N)=0`. + +## Residual ten-call consequence and limits + +PR6012's cited reduction leaves `n=5`, two scalar roles and the ten-call +write profile `(target,spectator)=(6,4)`. Both spectators are therefore written +exactly twice. Their two writer projectors must be equal by (2). Applying the +transpose/reversed-word version gives the same necessary equality for the +two reads of each spectator. Total length ten and PR6012's two-read minimum +for each of the five coordinates force exactly two reads per coordinate. +Each of the three target coordinates is also written and read exactly twice; +its writer pair and reader pair must each be complementary. These equalities +are necessary, not sufficient for a full formal endpoint; +no length-ten or length-eleven exclusion is asserted. + +## A live two-write spectator and a necessary relabelling term + +Take distinct address coordinates `i,j,k`, put `g=E_kj`, `h=E_ik`, +`t=E_ij`, and fix any one rank-one projector `N`. In the address group, +`g h g h t=e`. Products with the same projector satisfy +`D(a,N)D(b,N)=(I+N)+[ab]N`. Consequently + +`D(g,N) D(h,N) D(g,N) D(h,N) D(t,N)=I`. + +Coordinate `k` is written twice and read twice, and all inputs are restored. +This refutes an unrestricted claim that every live restored spectator must +be written at least three times. It is not a ten-call two-cycle counterexample. +For the middle `B=D(h,N)`, both support labels pass the selection with `j=l`, +but `g h g != h`. Omitting the relabelling in (1) changes the result. The +identity can be inserted before the known twelve-call endpoint, giving a +seventeen-call positive endpoint with a live two-write spectator. + +## Evidence and reproduction + +```sh +python3.12 -I -W error -B research/two-write-spectator-projection/verify.py +python3.12 -I -W error -B research/two-write-spectator-projection/independent.py +python3.12 -B scripts/research_package.py --package research/two-write-spectator-projection +``` + +The standard-library checker compares all 3,600 two-write contexts with a +middle of zero or one calls in the declared three-coordinate domain, checks +all 576 augmented `(N,M,S)` cases and all six commutator fixtures. It finds +6 restored pairs, 12 forward-zero pairs, but only 6 pairs passing both forward +and inverse conditions: exactly the complements. Controls reject missing +middle support selection, missing relabelling and each deleted commutator +call; the extra forward-only pairs refute the insufficient one-sided argument. +`independent.py` uses complete permutations of all address vectors as group +**labels**, retaining a separate scalar coefficient for every permutation. +It does not accept equality merely in the permutation-module representation. +Its separate dense scalar arithmetic checks all 288 GL(3,2) return-filter +cases, 72 five-coordinate contexts with outer subwords and longer middles, +the twelve-call positive endpoint, and all six seventeen-call insertions. +Both engines were prepared in this session; this is implementation diversity, +not independent human review. A separate read-only agent review independently +checked the proof, augmented matrices and group fixtures; no proof-kernel +acceptance is claimed. Finite checks corroborate the written proof. No unrestricted length-ten or +length-eleven search is part of this task. + +## Open next questions + +Can the full off-subgroup equations combine the equal spectator pairs and +complementary target pairs to exclude the residual `(6,4)` case? First analyze +these constraints on the read/write incidence cycles, then bind a proposed +strengthening to the complete endpoint. +The missing implication is formal cancellation, not a larger sampled word set. + +## Credit and scope + +Canonical base `721c03822c421b7f7fcbb2598993b947c4d88419`, priority 8, selected +PR6030 kappa `0.003125804`, unchanged. [Advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/6075). +Credit Nick Petalas/PR6012 for the single-write projection and reduction, +Mihir Srivastava/PR4939 for the formal model, James Reed/jwr404 #5005/#5379 for +the cited exact small-dimension costs, and JoyboyBrian/#4974 for the prior +single-cycle reduction. The commutator identity is standard, not a new group +identity. This application and checks were prepared by JoyboyBrian with +substantial OpenAI Codex assistance. Apache-2.0. No native tariff, physical +supplier, complete multiplication theorem or new kappa is claimed. diff --git a/research/two-write-spectator-projection/SOURCES.json b/research/two-write-spectator-projection/SOURCES.json new file mode 100644 index 0000000000..c564367c00 --- /dev/null +++ b/research/two-write-spectator-projection/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419", + "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/three-cycle-address-floor/README.md", + "usage": "input", + "git_blob": "6a65c91f29e5b226cebd32d0c1d6963a60a98761", + "sha256": "a63c4ea4c874cac1fb064e1aff07f8ef791391eb795aec22a2154eb44a8fa81e" + }, + { + "path": "research/two-three-cycles-every-dimension/PROOF.md", + "usage": "input", + "git_blob": "ca692812836f82484d228d8b4eb0f250c007d7a8", + "sha256": "b7af7801ddd5ff1e8d07d50dcd6f537f052d515839b828f0c4fd040351b8bce3" + } + ] +} diff --git a/research/two-write-spectator-projection/TASK.json b/research/two-write-spectator-projection/TASK.json new file mode 100644 index 0000000000..f4085887db --- /dev/null +++ b/research/two-write-spectator-projection/TASK.json @@ -0,0 +1,64 @@ +{ + "schema_version": 1, + "task_id": "bit-new-register-model", + "priority_revision": 8, + "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419", + "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": "Derive the exact two-write row-stabilizer projection for PR6012; prove equal restored-row projector pairs and complementary moved-row pairs, retaining inverse-word and middle-label conditions.", + "scope_change_reason": "Take PR6012 Open next question 3 and the public Discussion 6075 claim: a support-sensitive two-write lemma rather than a new physical register construction.", + "bottleneck_link": "Provides necessary writer/read constraints on the residual ten-call (6,4) case; does not decide it or give a supplier.", + "budget_minutes": 60, + "stop_rule": "Stop with the scoped lemma, exact finite controls and explicit live-two-write counterexample. No unrestricted length10/11 census.", + "outcome": "partial", + "evidence": "python3.12 -B scripts/research_package.py --package research/two-write-spectator-projection", + "author": "JoyboyBrian", + "ai_assistance": "Substantial OpenAI Codex assistance in proof, checker and documentation; separate agent read-only review, no independent human or proof-kernel acceptance.", + "open_questions": [ + { + "question": "Do equal spectator pairs, complementary target pairs and the full off-subgroup equations exclude the residual ten-call (6,4) case?", + "why_it_matters": "This is the remaining five-coordinate case identified by PR6012, distinct from already excluded lengths below 10.", + "first_step": "Analyze the read/write incidence cycles with these projector constraints and retain exact middle support and labels.", + "blocked_by": "Projector constraints are only necessary; full noncommutative formal coefficient cancellation remains unresolved." + } + ] +} diff --git a/research/two-write-spectator-projection/VERIFY.json b/research/two-write-spectator-projection/VERIFY.json new file mode 100644 index 0000000000..836e02fa96 --- /dev/null +++ b/research/two-write-spectator-projection/VERIFY.json @@ -0,0 +1,62 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/three-cycle-address-floor/README.md", + "research/two-three-cycles-every-dimension/PROOF.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Exact 3600 two-write contexts, 576 augmented matrices, 6 commutator identities and rejecting controls" + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "All projection, classification and control checks remain active under optimization" + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/independent.py" + ], + "timeout_seconds": 60, + "checks": "Independent complete-permutation group labels: 288 return filters, 72 outer contexts, six 17-call positive endpoints" + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/independent.py" + ], + "timeout_seconds": 60, + "checks": "Independent formal-coefficient and positive endpoint checks under optimization" + } + ] +} diff --git a/research/two-write-spectator-projection/independent.py b/research/two-write-spectator-projection/independent.py new file mode 100644 index 0000000000..1c6a3b940d --- /dev/null +++ b/research/two-write-spectator-projection/independent.py @@ -0,0 +1,137 @@ +"""Independent full-permutation group labels and dense scalar arithmetic.""" +import importlib.util +import json +from itertools import product +from pathlib import Path + +HERE = Path(__file__).resolve().parent +spec = importlib.util.spec_from_file_location('two_write_primary', HERE / 'verify.py') +primary = importlib.util.module_from_spec(spec) +spec.loader.exec_module(primary) +ONE = (1, 0, 0, 1) +ZERO = (0, 0, 0, 0) + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def dense_product(a, b): + return tuple(sum(a[2*i+k] * b[2*k+j] for k in range(2)) % 2 + for i in range(2) for j in range(2)) + + +def bit_tuple(value): + return tuple((value >> bit) & 1 for bit in range(4)) + + +def permutation(n, d, s): + return tuple(x ^ (((x >> s) & 1) << d) for x in range(1 << n)) + + +def compose(a, b): + return tuple(a[x] for x in b) + + +def toggled(out, label, value): + prior = out.get(label, ZERO) + value = tuple(a ^ b for a, b in zip(prior, value)) + if value == ZERO: + out.pop(label, None) + else: + out[label] = value + + +def oracle(word, n): + current = {tuple(range(1 << n)): ONE} + for d, s, encoded in word: + N = bit_tuple(encoded) + complement = tuple(a ^ b for a, b in zip(ONE, N)) + g = permutation(n, d, s) + nxt = {} + for p, value in current.items(): + toggled(nxt, p, dense_product(value, complement)) + toggled(nxt, compose(p, g), dense_product(value, N)) + current = nxt + return current + + +def row_is(p, row, expected): + return all(((p[x] >> row) & 1) == ((x >> expected) & 1) for x in range(len(p))) + + +def convert(poly): + out = {} + for rows, value in poly.items(): + p = tuple(sum(((r & x).bit_count() % 2) << i for i, r in enumerate(rows)) + for x in range(1 << len(rows))) + out[p] = bit_tuple(value) + return out + + +def group_filter(): + cases = 0 + for rows in product(range(8), repeat=3): + b = tuple(sum(((r & x).bit_count() % 2) << i for i, r in enumerate(rows)) for x in range(8)) + if len(set(b)) != 8: + continue + for k in range(3): + if not row_is(b, k, k): + continue + for j, l in product([i for i in range(3) if i != k], repeat=2): + gbh = compose(compose(permutation(3, k, j), b), permutation(3, k, l)) + need(row_is(gbh, k, k) == row_is(b, j, l), 'independent return filter') + cases += 1 + need(cases == 288, 'complete GL3 filter inventory') + return cases + + +def outer_contexts(Ns): + n, k = 5, 4 + letters = [(d, s) for d in range(4) for s in range(5) if d != s] + for index in range(72): + N, M = Ns[(index // 6) % 6], Ns[index % 6] + j, l = index % 4, (index // 4) % 4 + A = (letters[index % 16] + (Ns[(index + 1) % 6],),) + C = (letters[(index + 7) % 16] + (Ns[(index + 3) % 6],),) + B = tuple(letters[(index + 3*t) % 16] + (Ns[(index + t) % 6],) for t in range(2 + index % 2)) + word = A + ((k, j, N),) + B + ((k, l, M),) + C + actual = oracle(word, n) + need(actual == convert(primary.word_poly(word, n)), 'independent full formal coefficients') + actual = {p: value for p, value in actual.items() if row_is(p, k, k)} + center = primary.two_write_formula(B, n, k, j, l, N, M) + expected = primary.multiply(primary.multiply(primary.word_poly(A, n), center), primary.word_poly(C, n)) + need(actual == convert(expected), 'projection with arbitrary outer contexts') + return 72 + + +def positive_endpoints(Ns): + n = 5 + swaps = ((0, 1), (1, 0), (0, 1), (1, 2), (2, 1), (1, 2)) + word12 = tuple((d, s, N) for N in (1, 8) for d, s in swaps) + c = tuple(range(1 << n)) + for d, s in swaps: + c = compose(c, permutation(n, d, s)) + expected = {c: ONE} + need(oracle(word12, n) == expected, 'twelve-call endpoint') + for N in Ns: + loop = ((3, 1, N), (0, 3, N), (3, 1, N), (0, 3, N), (0, 1, N)) + need(oracle(loop, n) == {tuple(range(1 << n)): ONE}, 'independent commutator') + word17 = loop + word12 + need(oracle(word17, n) == expected, 'seventeen-call endpoint') + need(sum(d == 3 for d, s, _ in word17) == sum(s == 3 for d, s, _ in word17) == 2, + 'seventeen-call live spectator') + return 6 + + +def main(): + primary.source_check() + Ns = primary.projectors() + counts = {'return_filter': group_filter(), 'outer_contexts': outer_contexts(Ns), + 'seventeen_call_endpoints': positive_endpoints(Ns)} + print('PASS_TWO_WRITE_INDEPENDENT ' + json.dumps(counts, sort_keys=True)) + + +if __name__ == '__main__': + main() diff --git a/research/two-write-spectator-projection/verify.py b/research/two-write-spectator-projection/verify.py new file mode 100644 index 0000000000..ed533ba757 --- /dev/null +++ b/research/two-write-spectator-projection/verify.py @@ -0,0 +1,170 @@ +#!/usr/bin/env python3 +"""Exact two-write projection and projector constraints; no long-word census.""" +from hashlib import sha256 +from itertools import product +import json +from pathlib import Path + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parents[1] +I = 9 # Row-major 2x2 binary identity. + + +def require(ok, message): + if not ok: + raise ValueError(message) + + +def smul(a, b): + out = 0 + for r in range(2): + for c in range(2): + bit = ((a >> (2*r) & 1) & (b >> c & 1)) ^ ((a >> (2*r+1) & 1) & (b >> (2+c) & 1)) + out |= bit << (2*r+c) + return out + + +def identity(n): + return tuple(1 << i for i in range(n)) + + +def label(n, d, s): + rows = list(identity(n)) + rows[d] ^= 1 << s + return tuple(rows) + + +def gmul(a, b): + return tuple(xor(b[j] for j in range(len(b)) if row >> j & 1) for row in a) + + +def xor(values): + out = 0 + for value in values: + out ^= value + return out + + +def put(poly, group, coefficient): + value = poly.get(group, 0) ^ coefficient + if value: + poly[group] = value + else: + poly.pop(group, None) + + +def multiply(a, b): + out = {} + for g, x in a.items(): + for h, y in b.items(): + put(out, gmul(g, h), smul(x, y)) + return out + + +def word_poly(word, n): + e = identity(n) + out = {e: I} + for d, s, projector in word: + out = multiply(out, {e: I ^ projector, label(n, d, s): projector}) + return out + + +def sandwich(poly, a, b): + out = {} + for group, coefficient in poly.items(): + put(out, group, smul(smul(a, coefficient), b)) + return out + + +def projected(poly, k): + return {g: value for g, value in poly.items() if g[k] == 1 << k} + + +def two_write_formula(middle, n, k, j, l, N, M, relabel=True, select=True): + B = word_poly(middle, n) + g, h = label(n, k, j), label(n, k, l) + out = sandwich(B, I ^ N, I ^ M) + for b, value in B.items(): + if not select or b[j] == 1 << l: + put(out, gmul(gmul(g, b), h) if relabel else b, smul(smul(N, value), M)) + return out + + +def augment(poly): + return xor(poly.values()) + + +def projectors(): + return [a for a in range(1, 16) if a != I and smul(a, a) == a and + ((a & 1) * (a >> 3 & 1) ^ (a >> 1 & 1) * (a >> 2 & 1)) == 0] + + +def source_check(): + pins = json.loads((PACKAGE / 'SOURCES.json').read_text()) + for pin in pins['files']: + if pin.get('usage') == 'input': + require(sha256((ROOT / pin['path']).read_bytes()).hexdigest() == pin['sha256'], 'source mismatch') + + +def classify(Ns): + restored, moved = set(), set() + for N, M, S in product(Ns, Ns, range(16)): + F = smul(I ^ N, I ^ M) ^ smul(smul(N, S), M) + if F == I: + restored.add((N, M)) + require(N == M and smul(smul(N, S), N) == N, 'restored classification') + if F == 0: + moved.add((N, M)) + require(smul(I ^ N, I ^ M) == 0, 'forward moved condition') + both = {(N, M) for N, M in moved if (M, N) in moved} + require(len(restored) == 6 and len(moved) == 12 and len(both) == 6, 'pair inventory') + require(all(M == I ^ N for N, M in both), 'inverse moved condition') + return moved + + +def check_formula(Ns): + n, k = 3, 2 + middles = [()] + [((d, s, N),) for d in (0, 1) for s in range(3) if d != s for N in Ns] + cases = 0 + for middle, j, l, N, M in product(middles, (0, 1), (0, 1), Ns, Ns): + word = ((k, j, N),) + middle + ((k, l, M),) + actual = projected(word_poly(word, n), k) + expected = two_write_formula(middle, n, k, j, l, N, M) + require(actual == expected, 'two-write projection') + cases += 1 + require(cases == 3600, 'formula coverage') + return cases + + +def commutator(N): + # i=0,j=1,k=2; products act on column vectors from right to left. + return ((2, 1, N), (0, 2, N), (2, 1, N), (0, 2, N), (0, 1, N)) + + +def controls(Ns, moved): + require(any(M != I ^ N for N, M in moved), 'forward-only strengthening control') + for N in Ns: + word = commutator(N) + require(word_poly(word, 3) == {identity(3): I}, 'commutator identity') + require(sum(d == 2 for d, s, _ in word) == sum(s == 2 for d, s, _ in word) == 2, 'live spectator') + middle = (word[1],) + good = two_write_formula(middle, 3, 2, 1, 1, N, N) + require(good != two_write_formula(middle, 3, 2, 1, 1, N, N, relabel=False), 'relabel mutation') + require(all(word_poly(word[:i]+word[i+1:], 3) != {identity(3): I} for i in range(5)), 'omission mutation') + require(any(two_write_formula((), 3, 2, 0, 1, N, M) != + two_write_formula((), 3, 2, 0, 1, N, M, select=False) + for N, M in product(Ns, repeat=2)), 'selection mutation') + + +def main(): + source_check() + Ns = projectors() + require(len(Ns) == 6, 'six projectors') + moved = classify(Ns) + count = check_formula(Ns) + controls(Ns, moved) + print('PASS_TWO_WRITE_PROJECTION cases=' + str(count) + ' restored_pairs=6 forward_pairs=12 inverse_pairs=6 commutators=6 no_length10_exclusion') + + +if __name__ == '__main__': + main()