Classify shortest words for the braid endpoint 3214 (no κ)

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.

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.

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"
+    }
+  ]
+}

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"
+}

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."
+    }
+  ]
+}