diff --git a/research/braid-3214-shortest-words/PROOF.md b/research/braid-3214-shortest-words/PROOF.md new file mode 100644 index 0000000000..2a347b88ff --- /dev/null +++ b/research/braid-3214-shortest-words/PROOF.md @@ -0,0 +1,131 @@ +# Shortest words for the braid endpoint 3214 + +Produced by Nick Petalas. Apache-2.0. A written argument plus an exact finite +census re-executed by [verify.py](verify.py). It is not a proof-kernel +certificate or a physical caller invoice. + +## Setting + +The setting is the one of unpaidmoon's PR6642. K is a field, A=K^2, U is the +12-dimensional space of ordered pairs e_(i,j), i≠j in {1,2,3,4}, with +σ·e_(i,j)=e_(σ(i),σ(j)), and [σ] acts on A⊗U as I⊗σ. Composition is +(ab)(i)=a(b(i)), and products of operators act rightmost first, so +[a][b]=[ab]. With s=(1 2), t=(2 3), u=(3 4), the target is T=[w] with +w=sts=tst, one-line notation 3214. For a transposition r and an idempotent N +on A, + + D_r(N) = I + ([r] - I) N. + +A paid factor is D_r(N) with r ∈ {s,t,u} and N of rank one. Write X'=I-X. +PR6642 proves that every word equal to T has at least six factors. Over F_q +there are n=q(q+1) rank-one projectors. + +## Three identities, valid over every field + +**(C) Conjugation.** [σ] D_r(N) [σ]^{-1} = D_{σrσ^{-1}}(N) for every +permutation σ, since I⊗σ commutes with N⊗I. + +**(L) Line lemma.** Let Z be a rank-one projector and let every factor of a +product be D_{r_k}(N_k) with N_k ∈ {Z, Z'} and r_k an arbitrary transposition. +Each factor preserves (im Z)⊗U and (ker Z)⊗U. On (im N_k)⊗U it acts as [r_k] +and on the other summand as the identity. Hence the product equals +Z⊗π_L + Z'⊗π_M, where π_L is the ordered product of the labels of the factors +with projector Z and π_M that of the factors with projector Z'. If π_L=π_M=π +the product is the pure permutation [π]. + +The complement identity D_r(Z)D_r(Z')=[r] of PR6642 is the case of two +factors. + +## Theorem + +**(a) Every field.** Each of the following sixteen words equals [w] for all +rank-one projectors P, X, Y. + +| pattern | word | free projectors | +|---|---|---| +| ssttss | s(P) s(P') t(X) t(X') s(Y) s(Y') | 3 | +| ttsstt | t(P) t(P') s(X) s(X') t(Y) t(Y') | 3 | +| sttsst | s(P) t(X) t(X') s(Y) s(Y') t(P') | 3 | +| tsstts | t(P) s(X) s(X') t(Y) t(Y') s(P') | 3 | +| sststs | s(P) s(P') t(X) s(X) t(X') s(X') | 2 | +| ttstst | t(P) t(P') s(X) t(X) s(X') t(X') | 2 | +| stssts | s(P) t(P) s(X) s(X') t(P') s(P') | 2 | +| tsttst | t(P) s(P) t(X) t(X') s(P') t(P') | 2 | +| ststss | s(P) t(P) s(P') t(P') s(X) s(X') | 2 | +| tststt | t(P) s(P) t(P') s(P') t(X) t(X') | 2 | +| ststst | s(P) t(X) s(X) t(X') s(X') t(P') | 2 | +| tststs | t(P) s(X) t(X) s(X') t(X') s(P') | 2 | +| ststts | s(P) t(P') s(P') t(X) t(X') s(P) | 2 | +| tstsst | t(P) s(P') t(P') s(X) s(X') t(P) | 2 | +| sttsts | s(P) t(X) t(X') s(P') t(P') s(P) | 2 | +| tsstst | t(P) s(X) s(X') t(P') s(P') t(P) | 2 | + +Here r(Z) abbreviates D_r(Z). Each free projector occurs literally at a fixed +position, so each parametrization is injective, and distinct label patterns +give disjoint families. Over F_q the families contain exactly +4n^3+12n^2 distinct words, n=q(q+1). + +**(b) Finite fields F2 and F3.** Every six-factor word equal to +[w] lies in one of the sixteen families. So the number of shortest words is +1296 over F2 and 8640 over F3, in both cases 4n^3+12n^2. The verifier +accepts other primes as an opt-in run; no such run is claimed here. + +**Corollary (every field).** Every tight two-factor suffix allowed by the +PR6642 peel table extends to a shortest word. The suffix r(P') r(P) occurs in +the family ssttss or ttsstt, and r'(N) r(P) with r≠r' in {s,t} occurs in +tsstts or sttsst, whose last two projectors Y' and P' are independent. + +Part (b) is an exhaustive computation, not an all-field theorem. Whether the +families are complete over every field is the first open question in the +README. + +## Proof of (a) + +Each word is rewritten to [w] by two moves. A contiguous block whose +projectors all lie in one pair {Z,Z'} and whose two line products agree is +replaced by the pure permutation [π] given by (L). The pure permutation is then +moved to the right end through the remaining factors by (C), which changes +their labels to other transpositions but keeps their projectors. Repeat until +no factor remains and compare the accumulated permutation with w. +`reduce_certificate` in verify.py performs exactly these moves on the symbolic +words and checks the final permutation. Every move is a field-independent +identity, so the check proves (a) for every field. + +Two hand evaluations show the pattern. + +* s(P) t(X) s(X) t(X') s(X') t(P'). The middle block lies in {X,X'} with + π_L=π_M=ts, so it is [ts]. By (C), [ts] D_t(P') = D_{(ts)t(ts)^{-1}}(P')[ts] + and (ts)t(ts)^{-1}=tstst=s by the braid relation. The word becomes + D_s(P)D_s(P')[ts]=[s][ts]=[sts]=[w]. +* s(P) t(X) t(X') s(Y) s(Y') t(P'). The two inner pairs give [t][s]=[ts]; the + same conjugation turns the last factor into D_s(P'), and the word is again + [s][ts]=[w]. + +## Proof of (b) + +Two independent engines enumerate words over F_p. Operators are stored as +elements Σ_σ M_σ⊗σ of M_2(F_p)[S_4], and every equality test uses the exact +24×24 operator on A⊗U, the equality notion of PR6642. + +1. **Tight-peel search.** With φ(M)=dim H-dim(H∩M^{-1}H), H=A⊗U+, PR6642 + shows φ is subadditive and φ(D_r(N))=1. The verifier recomputes φ(T)=6 and + φ=1 for every factor of the field. If a word f1⋯f6 equals T, then for each + k the right prefix W_k=f_{7-k}⋯f6 satisfies φ(T W_k^{-1}) = 6-k, since + otherwise the remaining factors could not supply the missing defect. The + search therefore keeps only tight peels, and a word is accepted only when + the final remainder is the identity operator. +2. **Unpruned join (F2, F3).** All three-factor products are tabulated. Every + factor is an involution, so f1⋯f6=T exactly when f1f2f3 = T f6 f5 f4. This + join uses no defect argument. + +Both engines return the same word set, and it equals the union of the +families. Its size is checked against 4n^3+12n^2. + +## Limits + +Completeness is proved only over F2 and F3. Spectator +elimination (JoyboyBrian PR4765), the length bound and the defect (PR6642, +PR6449) are inherited and not replayed. Scalar conjugation is algebraic, not a +physical basis change. No caller, tape, precision, stock or compiler cost is +priced. The selected conditional value 781451/250000000 is unchanged and all +five framework assumptions remain. diff --git a/research/braid-3214-shortest-words/README.md b/research/braid-3214-shortest-words/README.md new file mode 100644 index 0000000000..f53a8edd8d --- /dev/null +++ b/research/braid-3214-shortest-words/README.md @@ -0,0 +1,81 @@ +# Shortest paid words for the braid endpoint 3214 + +This package answers the first open question of unpaidmoon's +[PR6642](https://github.com/CrocSwap/integer-mult-bounds/pull/6642): which +shortest normalized words realize the plane endpoint [w], w=sts=tst=3214, in +the paid alphabet D_r(N)=I+([r]-I)N with r ∈ {s,t,u} and N a rank-one +projector on K^2. PR6642 proves the length is six and fixes the last two +peels. This package finds the words. + +## Result + +**Every field (scoped proof).** Sixteen explicit families of six-factor words +equal [w]: four with three free projectors (for example +`s(P) s(P') t(X) t(X') s(Y) s(Y')` and `s(P) t(X) t(X') s(Y) s(Y') t(P')`) and +twelve with two (for example `s(P) t(X) s(X) t(X') s(X') t(P')`), where +X'=I-X. The full table is in [PROOF.md](PROOF.md). The proof uses only two +field-independent identities: a line lemma for factors that share one +splitting, and conjugation of a factor by a pure permutation. Over F_q the +families contain 4n^3+12n^2 distinct words, n=q(q+1). + +**F2 and F3 (finite certificate, exhaustive).** These families are every +six-factor word equal to [w]: 1296 words over F2 and 8640 over F3. Two +independent searches agree, a tight-peel depth-first search and an unpruned +meet-in-the-middle join, with exact operator equality on A⊗U. The u label +never occurs, and only two projector splittings occur in the two-parameter +families. + +Over F2 and F3, every tight two-factor suffix allowed by the PR6642 peel +table extends to a shortest word: r(P') r(P) through the repeated-label +families, and r'(N) r(P) for every rank-one N through the families +`tsstts`/`sttsst`. The concern in PR6642 that a free second peel might not +extend does not occur over these fields. Over every field the same two +families already show that every free suffix extends, since P and Y are +independent there. + +This is not an all-field completeness theorem. Completeness over infinite +fields and over fields not enumerated is open. + +## Reproduce + +From the repository root, with CPython 3.12 and the standard library only: + +```sh +python3.12 -B scripts/research_package.py --package research/braid-3214-shortest-words +python3.12 -B research/braid-3214-shortest-words/verify.py # F2 and F3, about 11 s +python3.12 -B research/braid-3214-shortest-words/verify.py 5 # optional, not claimed +``` + +The registered check prints `PASS_BRAID_3214_SHORTEST_WORDS`. Larger primes +are an opt-in run with a much longer search; no completed run beyond F3 is +claimed. + +## Scope and remaining obligations + +The catalogue card is `formal-interface-lemma`; the scope change is recorded +in [TASK.json](TASK.json), following PR6642. Source pins are in +[SOURCES.json](SOURCES.json). Inherited and not replayed: spectator elimination +(Brian/JoyboyBrian PR4765), the six-factor lower bound and peel table +(unpaidmoon PR6642), the ordered-pair defect (Nick Petalas PR6449) and the st +classification (ToikY PR6550). No caller, tape, precision, stock or compiler +cost is priced. The selected conditional value stays 781451/250000000 and all +five framework assumptions remain. There is no new κ. + +## Open next questions + +The structured list is in [TASK.json](TASK.json). + +* Are the sixteen families complete over every field? First step: derive the + tight third-peel table symbolically after each second-peel branch of PR6642. +* Do other length-three rank-two endpoints have the same three building blocks + (complement pairs, single-splitting blocks, conjugation)? First step: change + the target constant in verify.py and rerun over F2 and F3. +* What does one two-splitting realization cost physically, compared with a + three-splitting one? Blocked on a caller tariff. + +## Credit + +Produced by Nick Petalas. The question, the six-factor bound and the peel +table are unpaidmoon's PR6642. Predecessor geometry: ToikY PR6550, +Nick Petalas PR6449, Brian/JoyboyBrian PR4765, Ross Richardson PR1989 and Adam +Gall's cut lineage. New work is Apache-2.0. diff --git a/research/braid-3214-shortest-words/SOURCES.json b/research/braid-3214-shortest-words/SOURCES.json new file mode 100644 index 0000000000..594089b9c7 --- /dev/null +++ b/research/braid-3214-shortest-words/SOURCES.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "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" + } + ] +} diff --git a/research/braid-3214-shortest-words/TASK.json b/research/braid-3214-shortest-words/TASK.json new file mode 100644 index 0000000000..4028d468f5 --- /dev/null +++ b/research/braid-3214-shortest-words/TASK.json @@ -0,0 +1,108 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 8, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "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": "Classify the six-factor paid words equal to the rank-two braid endpoint w=3214 (alphabet D_r(N), r in {s,t,u}, N rank-one), the first open question of PR6642: an all-field sufficiency proof for 16 explicit families and an exhaustive census over F2 and F3 showing these families are every shortest word.", + "scope_change_reason": "The catalogue card asks for one caller-bound formal interface lemma. This package answers the braid-endpoint shortest-word question left open by PR6642 (unpaidmoon), which itself changed scope from the same card. It does not discharge a selected-assumption interface or a Lean binding.", + "bottleneck_link": "Side result for optimal formal words at one braid endpoint. No supplier is priced and the selected conditional value 781451/250000000 is unchanged.", + "budget_minutes": 60, + "stop_rule": "Stop at the family list, its all-field sufficiency certificate and the finite-field completeness census. Do not attempt the all-field completeness proof or a caller invoice in this package.", + "outcome": "completed", + "evidence": "verify.py reduces each of the 16 symbolic families to [w] using only the complement/line identity and conjugation, both field-independent; then, over each requested prime field, it enumerates every six-factor word equal to [w] by tight-peel depth-first search with an operator-level final test, and over F2 and F3 also by an unpruned meet-in-the-middle join, and checks that both equal the union of the families, of size 4n^3+12n^2 with n=p(p+1). PROOF.md gives the written argument.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Are the 16 families every six-factor word for [3214] over every field, including infinite fields and F4?", + "why_it_matters": "The census proves completeness only over the fields it enumerates; an all-field classification would make the count 4n^3+12n^2 a theorem for every finite field.", + "first_step": "Extend the PR6642 peel table one level: classify tight third peels after each second-peel branch, using the same pair-support method, and show the remainder is forced into a family.", + "blocked_by": "After a free second peel the remainder involves two unrelated splittings; the third-peel table has not been derived symbolically." + }, + { + "question": "Do other rank-two endpoints of length three, such as 1432 or the longest element of S3 on other adjacent pairs, have the same family structure, and what is the general count for a reduced word set of size k?", + "why_it_matters": "It would show whether shortest paid words are always generated by complement pairs, line-diagonal blocks and conjugation.", + "first_step": "Run the same census with the target permutation changed, over F2 and F3.", + "blocked_by": "None for the finite census; the verifier is target-specific only in the constant W." + }, + { + "question": "What is the complete physical cost of one realization from the two-splitting families (for example s(P) t(X) s(X) t(X') s(X') t(P'))?", + "why_it_matters": "These words use only two projector splittings, which may be cheaper to deliver than three.", + "first_step": "Fix one caller and its basis-delivery tariff, then compare a two-splitting and a three-splitting family.", + "blocked_by": "No tape, precision, stock, compiler or caller tariff is supplied here." + } + ], + "coordination_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19376725" +} diff --git a/research/braid-3214-shortest-words/VERIFY.json b/research/braid-3214-shortest-words/VERIFY.json new file mode 100644 index 0000000000..8631e908f0 --- /dev/null +++ b/research/braid-3214-shortest-words/VERIFY.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 180, + "checks": "All-field sufficiency certificate for the 16 families; exhaustive tight-peel census over F2 and F3 with operator-level final test; unpruned meet-in-the-middle join over F2 and F3; census equals the family union of size 4n^3+12n^2." + } + ] +} diff --git a/research/braid-3214-shortest-words/verify.py b/research/braid-3214-shortest-words/verify.py new file mode 100644 index 0000000000..31941058ed --- /dev/null +++ b/research/braid-3214-shortest-words/verify.py @@ -0,0 +1,301 @@ +#!/usr/bin/env python3 +"""Shortest six-factor words for the braid endpoint w = 3214. + +Standard library only. Checks: + 1. an all-field sufficiency certificate for 16 explicit word families, + built only from three field-independent operator identities; + 2. an exhaustive census over F_p of every six-factor word equal to [w], + by tight-peel depth-first search (operator-level final test); + 3. an independent unpruned meet-in-the-middle join at operator level; + 4. that census = union of the families, with 4 n^3 + 12 n^2 words, + n = p(p+1) the number of rank-one projectors; + 5. that every two-factor suffix allowed by the PR6642 peel table occurs. +Usage: verify.py [p ...] (default: 2 3; p must be prime) +""" +import itertools +import sys + +ID = (0, 1, 2, 3) +LABELS = {"s": (1, 0, 2, 3), "t": (0, 2, 1, 3), "u": (0, 1, 3, 2)} +W = (2, 1, 0, 3) # one-line 3214, zero-based +PAIRS = [(i, j) for i in range(4) for j in range(4) if i != j] +PIDX = {pr: k for k, pr in enumerate(PAIRS)} +POS = [k for k, (i, j) in enumerate(PAIRS) if i < j] +NEG = [k for k, (i, j) in enumerate(PAIRS) if i > j] +NEGIDX = {k: r for r, k in enumerate(NEG)} + +# Families: letter = label, name = projector; X' denotes I - X. +FAMILIES = [ + "s(P) s(P') t(X) t(X') s(Y) s(Y')", + "t(P) t(P') s(X) s(X') t(Y) t(Y')", + "s(P) t(X) t(X') s(Y) s(Y') t(P')", + "t(P) s(X) s(X') t(Y) t(Y') s(P')", + "s(P) s(P') t(X) s(X) t(X') s(X')", + "t(P) t(P') s(X) t(X) s(X') t(X')", + "s(P) t(P) s(X) s(X') t(P') s(P')", + "t(P) s(P) t(X) t(X') s(P') t(P')", + "s(P) t(P) s(P') t(P') s(X) s(X')", + "t(P) s(P) t(P') s(P') t(X) t(X')", + "s(P) t(X) s(X) t(X') s(X') t(P')", + "t(P) s(X) t(X) s(X') t(X') s(P')", + "s(P) t(P') s(P') t(X) t(X') s(P)", + "t(P) s(P') t(P') s(X) s(X') t(P)", + "s(P) t(X) t(X') s(P') t(P') s(P)", + "t(P) s(X) s(X') t(P') s(P') t(P)", +] + + +def compose(a, b): + """(ab)(i) = a(b(i)); rightmost acts first.""" + return tuple(a[b[i]] for i in range(4)) + + +def inverse(a): + out = [0] * 4 + for i, v in enumerate(a): + out[v] = i + return tuple(out) + + +def parse(fam): + out = [] + for tok in fam.split(): + lab, name = tok[0], tok[2:-1] + out.append((lab, name.rstrip("'"), name.endswith("'"))) + return out + + +# ---------------------------------------------------------------- part 1 +def reduce_certificate(fam): + """Rewrite a symbolic word to a pure permutation using only: + (A) line lemma: a contiguous block whose projectors lie in {Z, I-Z} + acts by pi_L on im Z and pi_M on ker Z; if pi_L == pi_M it is [pi]; + (B) conjugation: [sigma] D_r(N) = D_{sigma r sigma^-1}(N) [sigma]. + Labels become arbitrary transpositions; both identities hold for every + transposition, every rank-one projector and every field. + Returns the resulting permutation and the list of steps.""" + word = [(LABELS[l], z, c) for (l, z, c) in parse(fam)] + pure = ID # pure permutation accumulated on the right end + steps = [] + while word: + found = None + for i in range(len(word)): + for j in range(len(word), i, -1): + block = word[i:j] + if len({z for (_, z, _) in block}) != 1: + continue + pl, pm = ID, ID + for (r, _, c) in block: + if c: + pm = compose(pm, r) + else: + pl = compose(pl, r) + if pl == pm and (j - i) >= 2: + found = (i, j, pl) + break + if found: + break + if found is None: + return None, steps + i, j, pi = found + steps.append((i, j, pi)) + # push [pi] to the right end through word[j:] by conjugation + tail = [(compose(compose(pi, r), inverse(pi)), z, c) for (r, z, c) in word[j:]] + word = word[:i] + tail + pure = compose(pi, pure) + # pure permutations already on the right commute past nothing left + return pure, steps + + +def check_families_all_fields(): + for fam in FAMILIES: + res, steps = reduce_certificate(fam) + assert res == W, (fam, res, steps) + pats = [''.join(t[0] for t in parse(f)) for f in FAMILIES] + assert len(set(pats)) == 16 + return pats + + +# ---------------------------------------------------------------- engines +def mm(a, b, p): + return ((a[0]*b[0]+a[1]*b[2]) % p, (a[0]*b[1]+a[1]*b[3]) % p, + (a[2]*b[0]+a[3]*b[2]) % p, (a[2]*b[1]+a[3]*b[3]) % p) + + +def gmul(x, y, p): + """Product of elements sum_sigma M_sigma (x) [sigma] of M_2(F_p)[S_4].""" + out = {} + for s1, m1 in x.items(): + for s2, m2 in y.items(): + s = compose(s1, s2) + m = mm(m1, m2, p) + o = out.get(s) + out[s] = m if o is None else tuple((u + v) % p for u, v in zip(o, m)) + return {s: m for s, m in out.items() if any(m)} + + +def opkey(x, p): + """Exact 24x24 operator on A (x) U, flattened (the equality notion of PR6642).""" + mat = [[0] * 24 for _ in range(24)] + for sig, m in x.items(): + for k, (i, j) in enumerate(PAIRS): + k2 = PIDX[(sig[i], sig[j])] + for a in range(2): + for b in range(2): + mat[2*k2+a][2*k+b] = (mat[2*k2+a][2*k+b] + m[2*a+b]) % p + return tuple(v for row in mat for v in row) + + +def rank(rows, p): + rows = [r[:] for r in rows] + r = 0 + for c in range(len(rows[0])): + piv = next((i for i in range(r, len(rows)) if rows[i][c]), None) + if piv is None: + continue + rows[r], rows[piv] = rows[piv], rows[r] + inv = pow(rows[r][c], p - 2, p) + rows[r] = [v * inv % p for v in rows[r]] + for i in range(len(rows)): + if i != r and rows[i][c]: + f = rows[i][c] + rows[i] = [(v - f * w) % p for v, w in zip(rows[i], rows[r])] + r += 1 + return r + + +def phi(x, p): + """dim H - dim(H cap M^-1 H) = rank of the negative-row/positive-column block.""" + blk = [[0] * 12 for _ in range(12)] + for sig, m in x.items(): + for c, k in enumerate(POS): + i, j = PAIRS[k] + r = NEGIDX.get(PIDX[(sig[i], sig[j])]) + if r is None: + continue + for a in range(2): + for b in range(2): + blk[2*r+a][2*c+b] = (blk[2*r+a][2*c+b] + m[2*a+b]) % p + return rank(blk, p) + + +def projectors(p): + out = [] + for n in itertools.product(range(p), repeat=4): + if mm(n, n, p) == n and (n[0] + n[3]) % p == 1: + out.append(n) + assert len(out) == p * (p + 1) + return out + + +def comp(n, p): + return ((1 - n[0]) % p, (-n[1]) % p, (-n[2]) % p, (1 - n[3]) % p) + + +def factor(lab, n, p): + return {ID: comp(n, p), LABELS[lab]: n} + + +def alphabet(p): + return [((lab, n), factor(lab, n, p)) for lab in "stu" for n in projectors(p)] + + +def word_op(word, p): + x = {ID: (1, 0, 0, 1)} + for lab, n in word: + x = gmul(x, factor(lab, n, p), p) + return opkey(x, p) + + +# ---------------------------------------------------------------- part 2 +def census_dfs(p): + fs = alphabet(p) + target = {W: (1, 0, 0, 1)} + assert phi(target, p) == 6 + for _, f in fs: + assert phi(f, p) == 1 + ident = opkey({ID: (1, 0, 0, 1)}, p) + words = set() + + def rec(rem, depth, suffix): + if depth == 6: + if opkey(rem, p) == ident: + words.add(tuple(reversed(suffix))) + return + for name, f in fs: + nxt = gmul(rem, f, p) + if phi(nxt, p) == 5 - depth: + rec(nxt, depth + 1, suffix + [name]) + + rec(target, 0, []) + return words + + +# ---------------------------------------------------------------- part 3 +def census_mitm(p): + """No defect pruning. word = L R with |L| = |R| = 3; factors are + involutions, so L = T R^{-1} = T * reversed(R).""" + fs = alphabet(p) + left = {} + for trip in itertools.product(fs, repeat=3): + x = gmul(gmul(trip[0][1], trip[1][1], p), trip[2][1], p) + left.setdefault(opkey(x, p), []).append(tuple(t[0] for t in trip)) + words = set() + target = {W: (1, 0, 0, 1)} + for trip in itertools.product(fs, repeat=3): + x = gmul(gmul(gmul(target, trip[2][1], p), trip[1][1], p), trip[0][1], p) + for lw in left.get(opkey(x, p), ()): + words.add(lw + tuple(t[0] for t in trip)) + return words + + +# ---------------------------------------------------------------- part 4 +def family_words(p): + projs = projectors(p) + out = set() + count = 0 + for fam in FAMILIES: + toks = parse(fam) + names = sorted({z for (_, z, _) in toks}) + for vals in itertools.product(projs, repeat=len(names)): + env = dict(zip(names, vals)) + w = tuple((l, comp(env[z], p) if c else env[z]) for (l, z, c) in toks) + out.add(w) + count += 1 + assert count == len(out), "family parametrizations overlap" + return out + + +def main(primes): + pats = check_families_all_fields() + print("PASS all-field sufficiency certificate for 16 families:", " ".join(pats)) + for p in primes: + n = p * (p + 1) + fam = family_words(p) + target = opkey({W: (1, 0, 0, 1)}, p) + bad = [w for w in fam if word_op(w, p) != target] + assert not bad, bad[:1] + dfs = census_dfs(p) + assert dfs == fam, (len(dfs), len(fam)) + assert len(dfs) == 4 * n**3 + 12 * n**2 + projs = projectors(p) + suffixes = {w[4:] for w in dfs} + allowed = set() + for r, r2 in (("s", "t"), ("t", "s")): + for P in projs: + allowed.add(((r, comp(P, p)), (r, P))) + for N in projs: + allowed.add(((r2, N), (r, P))) + assert suffixes == allowed and len(allowed) == 2 * (n + n * n) + msg = f"PASS F{p}: n={n} census={len(dfs)} = 4n^3+12n^2, equal to the 16 families; every tight two-peel suffix extends" + if p <= 3: + mitm = census_mitm(p) + assert mitm == dfs + msg += "; unpruned meet-in-the-middle agrees" + print(msg) + print("PASS_BRAID_3214_SHORTEST_WORDS") + + +if __name__ == "__main__": + args = [int(a) for a in sys.argv[1:]] or [2, 3] + main(args)