Prove the width-two F2 six-call floor with genuine group-word collisions

research/diagonal-pair-five-call-collisions/PROOF.md

@@ -0,0 +1,151 @@
+# A cancellation certificate for the five-call diagonal-pair obstruction
+
+## Statement and scope
+
+Let G be any group, L any set of group labels, and a,b distinct elements,
+neither expressible as a product of zero, one or two labels from L. Over
+F2[G], let D_N(g) = (I-N) + [g]N, where N is a rank-one idempotent 2 by 2
+matrix over F2 and g belongs to L. Then **no product of at most five calls is
+diag([a],[b])**.
+
+This is a computer-assisted theorem: the written argument below proves that
+an actual realization survives the finite collision relaxation; the registered
+exact verifier exhausts and rejects that relaxation. It is not a handwritten
+classification of all projector tuples, a proof-kernel result, a finite-group
+sample, or a theorem for other fields or widths.
+
+In particular, when a=xyx and b=yxy satisfy the stated shortest-word and
+distinctness hypotheses for L={x,y}, the minimum is exactly six. The upper
+bound is D_E00(x) D_E00(y) D_E00(x) D_E11(y) D_E11(x) D_E11(y).
+This is the formal register model of Wentao Li (#4089), as used by Nick
+Petalas (#6038) and Josie Elliston (#6048). No native tariff, supplier or
+multiplication bound is inferred.
+
+## Free scalar changes of basis
+
+The stated product form also covers arbitrary invertible scalar basis changes
+between paid calls. Write such a circuit as
+
+    S0 D_N1(g1) S1 ... D_Nk(gk) Sk,
+    Si in GL_2(F2).
+
+Let Ci=S0 ... S_(i-1). The identity S D_N(g) S^-1 = D_(S N S^-1)(g)
+moves each scalar factor to the right, giving
+
+    D_(C1 N1 C1^-1)(g1) ... D_(Ck Nk Ck^-1)(gk) S,
+    S=S0 ... Sk.
+
+Conjugation preserves rank-one idempotence, so every resulting projector is
+in the six-element inventory. The group-algebra augmentation [g] -> 1 sends
+every paid factor to I and sends diag([a],[b]) to I. Thus any successful
+circuit has S=I. Free scalar changes of basis therefore add no missing
+terminal factor or extra cases. This normalization does not admit free
+address-dependent maps, clean auxiliary registers, COPY or ERASE.
+
+## The missing group implication
+
+Write the chronological labels of a k-call candidate as g_1,...,g_k. They
+are positional symbols, not presumed distinct. For a subset U of positions,
+let w_U be its increasing sequence and g_U its group product. If two such
+sequences have a common prefix p, then
+
+    g_(pu) = g_(pv) if and only if g_u = g_v.
+
+The same equivalence holds for a common suffix. These are cancellation and
+multiplication in G; they hold in every group, including groups with torsion
+and arbitrary relations. In particular inserting one nonidentity letter
+between a fixed prefix and suffix cannot preserve the group element.
+The certificate uses both implications, only when all sequences involved
+are chronological subsets of the candidate. It does not presume that these
+rules decide the word problem.
+
+A concrete five-call tuple has projectors, in row-major bit encoding,
+
+    (1,5,5,3,10) = (E00, [[1,0],[1,0]], [[1,0],[1,0]],
+                   [[1,1],[0,0]], [[0,1],[0,1]]).
+
+Its matrix coefficients are
+
+    T00 = [g1 g2 g3 g4]
+    T01 = [g1 g2 g3 g4] + [g1 g2 g3 g5]
+    T10 = [g4] + [g2 g3 g4]
+    T11 = [g4] + [g2 g3 g5] + [g2 g3 g4].
+
+The required zero T10 forces g4=g2 g3 g4, hence g2 g3=e. Consequently
+T00=[g1 g4], so a has a two-label expression, contrary to the hypothesis.
+Separate choices of cancellation classes for different coefficients miss
+this shared implication. The finite certificate propagates it jointly.
+
+## Why the finite relaxation contains every realization
+
+Drop identity-labelled calls first. Therefore all remaining g_i are
+nonidentity and k is still at most five. Expand the product exactly as
+
+    product_i D_Ni(gi) = sum_U [g_U] P_U,
+    P_U = product_i (N_i if i in U else I-N_i),
+
+with every product in increasing position order. Each of the four matrix
+entries gives an equation over F2[G]. Move [a] into the 00 equation and [b]
+into the 11 equation. Every equation must now be zero.
+
+The solver has one node for each subset U and two extra nodes A,B for a,b.
+A partition stores only equalities forced or chosen so far. Initially all
+nodes are separate. A genuine realization supplies a coarser partition by
+actual group value. Every solver step preserves at least one branch
+compatible with that realization:
+
+1. **Cancellation closure.** For every common-prefix or common-suffix rule,
+   if its premise nodes have been equated, equate its conclusion nodes.
+   The group equivalences above justify this. The reverse rules are valid
+   multiplication by the common prefix or suffix.
+2. **Forbidden equalities.** Reject if the empty subset equals a singleton,
+   if A=B, or if A or B equals a subset of size at most two. These contradict
+   respectively g_i != e, a != b, or the shortest-label hypothesis.
+3. **Parity equations.** Replace each equation node by its current partition
+   class, retaining precisely classes with odd multiplicity. An actual
+   group-value class must occur evenly because the elements [g] form a
+   basis of F2[G]. If exactly two classes remain, their equality is forced.
+   If an odd number remain, no partition into even multiplicities exists.
+4. **Exhaustive partner branching.** Otherwise choose the first class in a
+   shortest nonempty residual equation. In any actual completion its
+   group-value class has even multiplicity, so at least one of the other
+   remaining classes has that same value. Branch over every such partner
+   and equate them. At least one branch retains the actual realization.
+
+Every branch strictly merges two classes; closure also only merges classes.
+Thus the search terminates. It may accept partitions unrealizable by groups,
+because it omits many group implications, but this only weakens a rejection.
+If every branch rejects, no actual realization of that projector tuple
+exists. The node cap fails the verifier rather than declaring a rejection.
+
+## Finite coverage
+
+A nonzero rank-one idempotent over F2 is u v^T with v^T u=1. The six 2 by 2
+possibilities have row-major bit encodings 1,3,5,8,10,12. The verifier obtains
+them by idempotence and trace one, then independently checks the outer-product
+inventory. It evaluates all 6^k tuples for each k=0,...,5, without identifying
+or omitting symmetry classes. There are 9,331 tuples in total.
+
+Every label sequence, in every group and every label set, is covered by the
+positional-symbol argument for its projector tuple. No assignment of x,y,
+no finite group, and no determinant/degree invariant is enumerated. The
+computed zero survivors, together with the sound relaxation argument,
+establish the scoped theorem.
+
+## Controls and remaining proof obligations
+
+The six-call direct construction is checked by exact free-word coefficients.
+Removing cancellation reopens the four-call tuple (1,5,1,10), demonstrating
+that support and coefficient parity alone do not prove the result. Relaxing
+the target length hypothesis reopens the two-call tuple (E00,E11). The
+explicit five-call example above is checked by the same refutation engine.
+The verifier independently authenticates every generated cancellation rule as a
+single common-context law, checks the displayed coefficient expansion, and
+accepts the actual four- and six-call constructions in the collision solver.
+It uses explicit checks, which remain active under Python -O.
+
+The proof still depends on the correctness and successful completion of the
+small Python certificate. Independent human or proof-assistant review has
+not been claimed. The six-projector inventory and characteristic-two parity
+are essential scope restrictions; extension to other fields or widths
+requires new reasoning.

research/diagonal-pair-five-call-collisions/README.md

@@ -0,0 +1,69 @@
+# Five-call diagonal-pair collision obstruction
+
+**All-group computer-assisted obstruction, restricted to width two over F2.
+No new kappa.** In the formal rank-one-idempotent call model, a diagonal pair
+of distinct targets, each requiring at least three labels, needs at least six
+calls. For (xyx,yxy) satisfying these hypotheses, the direct six-call word
+meets the bound.
+
+[PROOF.md](PROOF.md) gives the exact scope, a symbolic five-call cancellation
+example, and the soundness argument for the exhaustive finite refutation.
+[verify.py](verify.py) checks every one of the 9,331 projector tuples of
+length zero through five. It propagates common-prefix/suffix cancellation
+jointly through the four group-algebra coefficient equations. Free invertible scalar basis changes are normalized by conjugation and
+augmentation in the proof. The groups and label alphabets remain arbitrary; this is not evidence extrapolated
+from a finite group census.
+
+This resolves the width-two/F2 portion of Josie Elliston's #6048 open
+question 1. That package's support-only relaxation admitted 20 four-call
+and 938 five-call projector tuples. Its arbitrary subset-class assignment
+omitted joint group-word consistency. This successor adds cancellation and
+all coefficient equations, rather than repeating the free-group degree
+control. Nick Petalas's #6038 established the earlier four-call xy/yx result.
+
+## Reproduce
+
+Standard-library Python 3.12; approximately two seconds per direct run:
+
+```sh
+python3 -B research/diagonal-pair-five-call-collisions/verify.py
+python3 -O -B research/diagonal-pair-five-call-collisions/verify.py
+python3 -B scripts/research_package.py --package research/diagonal-pair-five-call-collisions
+```
+
+Expected marker: `PASS_DIAGONAL_PAIR_FIVE_CALL_COLLISIONS`, with zero survivors
+at every length. Registered controls include the six-call exact endpoint,
+a reopened four-call support-only instance when cancellation is removed,
+and a reopened two-call instance when short targets are allowed. Independent
+controls authenticate every generated context rule and require the collision
+solver itself to accept the known four- and six-call constructions.
+
+The package has no runtime source dependencies. Exact predecessor proof and
+README pins are provenance in SOURCES.json; their bytes are not imported or
+modified. The verifier also runs directly in a Git-free source export.
+
+## Open next questions
+
+1. Does the six-call floor hold at larger widths over F2? It would remove the
+   two-register restriction. First inspect whether the parity refutation can
+   be replaced by a rank/corner argument; the six-projector inventory does
+   not cover larger matrices.
+2. Does it hold in odd characteristic or F4? It would address the remaining
+   field scope of #6048's question. First derive coefficient-class constraints
+   with nonbinary weights; even pairing is specific to F2 and is not valid
+   unchanged over those fields.
+
+Neither question authorizes another construction round or certifies a native
+implementation. Conversion, restoration, tariffs, whole callers and the
+selected multiplication frontier are outside this result.
+
+## Credit
+
+Prepared by JoyboyBrian with substantial OpenAI Codex assistance, Apache-2.0.
+Josie Elliston (#6048, substantial Claude assistance) supplied the longer-pair
+question, support-only counterexamples and group-free proof approach; Nick
+Petalas (#6038) supplied the preceding all-group xy/yx theorem and corner
+method; Wentao Li (#4089/#4093) supplied the rank-one-idempotent group-algebra
+model, following Cinna Davis's A5 target (#2246). Their broader results are
+not re-audited here. Source heads are pinned, and no frozen predecessor is
+changed.

research/diagonal-pair-five-call-collisions/SOURCES.json

@@ -0,0 +1,46 @@
+{
+  "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/conjugate-pair-group-free-audit/README.md",
+      "usage": "provenance",
+      "pin": "head:518cd2a7880f94b80c9c93aad304a7f041def647:research/conjugate-pair-group-free-audit/README.md",
+      "git_blob": "c0ae47bf6c566c69466e150661641d61fd9ff636",
+      "sha256": "3adf65a79d27ea7a60ec8978fa6b45f75d65c07c3aed019080b64431078f28f3"
+    },
+    {
+      "path": "research/conjugate-pair-group-free-audit/PROOF.md",
+      "usage": "provenance",
+      "pin": "head:518cd2a7880f94b80c9c93aad304a7f041def647:research/conjugate-pair-group-free-audit/PROOF.md",
+      "git_blob": "a92cbe6f25408cd5ff1e4f820963d44cabc9f362",
+      "sha256": "a37a1bc0bd306a94c148c703c43e41ee4f8d90fcf009cfeb7cee8b2a31fa600a"
+    },
+    {
+      "path": "research/conjugate-pair-every-group/README.md",
+      "usage": "provenance",
+      "pin": "head:0cee0e104b68ce6f06bf84af03f46ac30680e64c:research/conjugate-pair-every-group/README.md",
+      "git_blob": "47bb74c1399e2bed48afd5be200e53223bb7e4c0",
+      "sha256": "9ddac65a112890de4d098a5387209927d753cbdb68fa3a5d064d6dfe717b9a1a"
+    },
+    {
+      "path": "research/conjugate-pair-every-group/PROOF.md",
+      "usage": "provenance",
+      "pin": "head:0cee0e104b68ce6f06bf84af03f46ac30680e64c:research/conjugate-pair-every-group/PROOF.md",
+      "git_blob": "46d33fc3b993a53435bf8c450421a5310e20a8a0",
+      "sha256": "414b5f88f7fd24d7066b03efa371bdf7a28fbed22a8c36fd78a1073b469aafd2"
+    }
+  ]
+}

research/diagonal-pair-five-call-collisions/TASK.json

@@ -0,0 +1,70 @@
+{
+  "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": "Prove or refute the five-call diagonal-pair obstruction using genuine group-word collisions, initially width two over F2.",
+  "scope_change_reason": "Explicit preclaimed handoff #6048 open question 1 replaces the generic register-model task; formal group-algebra obstruction only, no native implementation.",
+  "bottleneck_link": "A scoped lower bound on sharing longer noncommutative diagonal targets; no primitive saving or complete BIT supplier is claimed.",
+  "budget_minutes": 30,
+  "stop_rule": "One written collision lemma or exact counterexample; bounded exhaustive projector certificate only, no finite-group inference.",
+  "outcome": "completed",
+  "evidence": "PROOF.md and registered verify.py: all 9331 tuples at lengths 0 through 5 rejected; exact six-call endpoint and weakened-hypothesis controls.",
+  "author": "JoyboyBrian",
+  "ai_assistance": "Substantial OpenAI Codex assistance.",
+  "open_questions": [
+    {
+      "question": "Does the six-call floor extend to larger widths over F2?",
+      "why_it_matters": "Removes the two-register restriction.",
+      "first_step": "Replace the six-projector case split by a rank/corner argument.",
+      "blocked_by": "Finite projector inventory only covers width two."
+    },
+    {
+      "question": "Does the six-call floor extend to odd characteristic or F4?",
+      "why_it_matters": "Addresses remaining field scope of predecessor question.",
+      "first_step": "Derive weighted coefficient-class constraints.",
+      "blocked_by": "Even pairing is specific to F2."
+    }
+  ]
+}

research/diagonal-pair-five-call-collisions/VERIFY.json

@@ -0,0 +1,32 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "-W",
+        "error",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 30,
+      "checks": "All 9331 projector tuples, common-prefix/suffix collision closure, exact six-call endpoint, missing-cancellation and short-target controls."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-O",
+        "-B",
+        "-W",
+        "error",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 30,
+      "checks": "All 9331 projector tuples, common-prefix/suffix collision closure, exact six-call endpoint, missing-cancellation and short-target controls."
+    }
+  ]
+}