Prove sharp five-factor cost for binary three-role products (no new κ)

research/right-vector-three-role-products/PROOF.md

@@ -0,0 +1,165 @@
+# A sharp five-factor bound for binary three-role products
+
+## Model and claim type
+
+Put K=F2 and R=K^k for a positive integer k. A paid factor on three roles is
+
+```text
+P(u,b) = I + u b^T,     u in R^3, b in K^3.
+```
+
+The embedding K into R is diagonal. Thus b is common to all k components,
+whereas u may have a different binary three-vector in each component. Free
+maps are common matrices in GL3(K), allowed anywhere. No extra roles are
+allowed. This is the formal alphabet of Wentao Li #4099 following #2513,
+with the free-map normal form retained in Nick Petalas #4243. ToikY #4334
+proved the sharp two-role field-product result and its common-direction
+upper construction.
+
+This package supplies a complete finite certificate and a scoped algebraic
+consequence of that certificate:
+
+1. Every invertible three-role target over F2^k costs at most five paid factors.
+2. The target U over F2^168 whose components list GL3(F2) costs exactly five.
+   Therefore the uniform bound is sharp, also for every k>=168 by padding.
+3. For that U the column lower bound delta(U) is exactly three. Its gap from
+   the exact cost is two.
+
+No minimum component count for cost five is asserted. No all-field,
+extra-role, local-ring or native-supplier statement is asserted.
+
+## 1. Reduction to common direction words
+
+Conjugation by a free matrix S preserves the alphabet:
+
+```text
+S P(u,b) S^-1 = P(Su, S^-T b).
+```
+
+Move all free maps to the right. A word of length L is a product of L paid
+factors followed by one common free S. For chronological direction sequence
+b1,...,bL, define the paid product as P_L ... P_1, with P_1 applied first.
+A zero direction gives the identity. It can be replaced by b=e1,u=0.
+Words shorter than four can likewise be padded to four.
+
+If a component of the target is invertible, every square factor in that
+component must be invertible, by rank submultiplicativity. In K, write a
+component paid factor as I+a b^T. It is invertible exactly when b.a=0.
+Indeed when b.a=0 its square is I. When b.a=1, a is nonzero and the factor
+kills a. For each nonzero b there are exactly four eligible a, including
+zero. These are all possibilities, not a restriction to coordinate vectors
+or to some chosen gate library.
+
+There are seven nonzero directions. For a fixed ordered word of length
+four there are exactly 4^4 eligible parameter tuples. Its reachable set is
+computed from {I} by left multiplication by each of the four eligible
+factors at each step. There are exactly 7^4=2401 ordered direction words.
+
+## 2. The complete finite certificate
+
+`verify.py` encodes a binary matrix by its three rows, each a three-bit
+integer, least significant row first. Thus I has encoding 273. It builds
+GL3(F2) by rank-three elimination on all 512 matrices. Independently, it
+builds every binary linear bijection on the eight vectors by enumerating
+all ordered triples of nonzero basis images and retaining the bijections.
+Both groups contain the same 168 matrices.
+
+The matrix calculation propagates reachable sets through all four steps.
+The independent calculation composes permutations of the eight vectors:
+first all 16 parameter choices for each two-direction word, then every
+pair of two-step results. It explicitly enumerates all
+7^4 * 4^4 = 614656 direction/parameter tuples. The two implementations agree
+on the complete 168-bit endpoint mask for every one of the 2401 direction
+words, rather than merely on cardinalities.
+
+The resulting complete histogram is:
+
+| Reachable group elements | 4 | 16 | 24 | 64 | 96 | 144 |
+|---|---:|---:|---:|---:|---:|---:|
+| Ordered four-direction words | 7 | 126 | 420 | 504 | 672 | 672 |
+
+In particular no four-direction word reaches all 168 matrices.
+
+For the fixed chronological sequence
+
+```text
+b1,b2,b3,b4,b5 = e1,e2,e3,e1,e2,
+```
+
+the matrix calculation constructs one literal five-factor witness for each
+of the 168 matrices. The action calculation independently enumerates all
+4^5=1024 parameter tuples and reaches all 168 endpoints. Every constructed
+witness is also evaluated on all eight binary inputs, giving 1344 complete
+component/input checks. This proves the upper-bound certificate. The
+verifier hashes the complete four-word endpoint table and the complete
+five-factor witness table. It also emits a generated receipt bound to the
+six package files and two pinned predecessor inputs.
+
+The computations are exact and use no randomness, numerical tolerance,
+symmetry reduction or pruning. All validations remain active under -O.
+They are executable finite evidence, not formal proof-kernel checking.
+
+## 3. Sharpness with arbitrary free maps
+
+For any common S in GL3(F2), the components of U S^-1 again list every
+element of GL3(F2), since right translation permutes the group. If U had a
+word with at most four paid factors and any free maps, Section 1 would give
+a common four-direction word for U S^-1 after identity padding. Its
+components would then have to lie in a reachable set of at most 144
+elements. They contain all 168, a contradiction.
+
+For any invertible M over F2^k, each component M_i has the Section 2 witness
+with the same five directions. At step j assemble its k left coefficients
+into u_j in R^3. Componentwise multiplication now gives M in five paid
+factors. Arbitrary componentwise left coefficients are permitted by the
+stated model; componentwise free maps or right directions are never used.
+This proves the quantified upper bound and cost(U)=5. Appending arbitrary
+invertible components to U preserves its lower bound by projection and its
+five-factor upper bound by the same construction.
+
+## 4. The column-bound gap
+
+The predecessor's general column bound is
+
+```text
+delta(M) = min over T in GL3(F2) of dim_F2 ((M T - I) F2^3) <= cost(M).
+```
+
+For U and any T, its translated components range over every group element.
+If a nonzero v were in the common kernel, every A in GL3(F2) would satisfy
+A v=v. But GL3(F2) sends a given nonzero v to every nonzero vector. This is
+impossible. Hence that map from F2^3 is injective and delta(U)=3. The
+verifier separately stacks all component rows and checks rank three for
+every one of the 168 free choices. It also checks all 4704 labelled
+factor/free-map conjugations, including the seven identity labels.
+
+Thus the column bound does not give an exact cost, or a uniform
+three-factor bound, even for invertible targets over a product of copies
+of the base field on only three roles. This is compatible with the exact
+local-algebra result in #4787: F2^168 is not local.
+
+## Attribution and relation to classical work
+
+This contribution was produced by Nick Petalas. The new contribution is
+the complete common-direction certificate and its sharp cost consequence
+in the repository's alphabet. ToikY #4334 supplied the field-product
+question, the shared-direction viewpoint and the two-role predecessor.
+Nick Petalas #4243/#4265/#4276 and #4749 supplied the retained normal form,
+column bound applications, general-target question and semilocal context.
+The alphabet and original column expansion are Wentao Li #4099 following
+#2513. Their packages are preserved unchanged.
+
+Short linear register-update programs have a classical literature. See
+Gadouleau and Riis, [Memoryless computation: new results, constructions,
+and extensions, Section 3.3](https://arxiv.org/html/1111.6026#S3.SS3), and
+Cameron, Fairbairn and Gadouleau,
+[Computing in matrix groups without memory](https://arxiv.org/abs/1310.6009).
+The general idea of short update programs and the generic 2n-1 upper-bound
+phenomenon are not claimed as original here. Our finite lower certificate
+ranges over every common binary covector sequence, with a common free
+GL3 map absorbed at the end. It concerns simultaneous product components.
+
+Native preparation, access, reversible restoration, precision, stock,
+physical implementation and a complete recursive invoice remain unknown.
+No complete multiplication theorem, supplier admission or new kappa follows.
+Independent human and formal proof-kernel review are unclaimed. Apache-2.0.

research/right-vector-three-role-products/README.md

@@ -0,0 +1,91 @@
+# Exact five-factor cost for binary three-role products
+
+A complete finite certificate gives a sharp formal-alphabet result. Every
+invertible three-role target over F2^k costs at most five paid factors
+I+u b^T, where b is a common binary vector and u may vary by component.
+The target over F2^168 listing all elements of GL3(F2) costs exactly five,
+even with arbitrary free GL3(F2) maps anywhere. Its column lower bound is
+only three. No new kappa or native supplier is claimed.
+
+The chronological upper directions are e1,e2,e3,e1,e2. All 2401 ordered
+four-direction words reach at most 144 of the 168 group elements. The
+[proof and scope](PROOF.md) explain why this finite census gives the
+all-k upper bound and survives arbitrary interleaved free maps. This
+extends ToikY's #4334 two-role product-field result. The contribution is
+the exact common-direction obstruction and certificate in this model;
+classical short register-update programs retain the credit listed there.
+
+## Evidence and reproduction
+
+From the repository root, using CPython 3.12 and only its standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B -W error research/right-vector-three-role-products/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -O -B -W error research/right-vector-three-role-products/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/right-vector-three-role-products
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/right-vector-three-role-products --check-source-history
+```
+
+Any CPython 3.12 installation can replace the local interpreter path.
+Expected scientific marker:
+
+```text
+PASS_RIGHT_VECTOR_THREE_ROLE_PRODUCTS group=168 words4=2401 max4=144 upper=5 delta=3 controls=7
+```
+
+Two algorithms compare every complete four-word endpoint set. The second
+enumerates 614656 parameter tuples as permutations of the eight binary
+vectors. The fixed upper word has 1024 parameter tuples and reaches all
+168 endpoints; its chosen witnesses pass all 1344 component/input cases.
+All 168 free right translations and delta cases, 4704 labelled
+conjugations and seven rejection controls pass. A generated JSON receipt
+binds results and file hashes; nothing is written into the checkout.
+
+The four-word histogram, indexed by reachable-set size, is
+`{4:7,16:126,24:420,64:504,96:672,144:672}`. The verifier derives it afresh
+and checks the complete masks with a second implementation. This is a
+finite certificate with a scoped algebraic consequence. It is not a search
+failure offered as a universal obstruction.
+
+## Limits and implementation discipline
+
+The field is F2, there are exactly three roles, and only invertible product
+components are covered. The sharp witness uses 168 components; minimal
+component count is open. Native preparation, routing, storage, dirty-state
+restoration, precision, stock and the full supplier invoice remain unknown.
+The selected construction is unchanged. Lean, Docker and a selected cold
+replay are outside scope and unrun. Independent human and formal
+proof-kernel review are unclaimed.
+
+The verifier uses bounded loops, explicit exceptions and no recursion.
+Its largest direction census has 2401 states, each with at most 168
+endpoints; the action multiplication table has 168^2 entries. CPython
+requires dynamic allocation, so fixed allocation is a documented managed
+runtime deviation, with collection sizes bounded by those finite domains.
+Functions stay under 60 lines. Warning-strict ordinary and optimized
+commands are registered. The negative-control dispatcher has seven fixed
+call targets; it is the only callback-based test dispatch. File errors
+propagate, and all file handles are owned by pathlib's bounded read calls.
+No package-wide configuration change is needed for this isolated script.
+
+## Open next questions
+
+1. What is the minimum k for which an invertible target over F2^k costs
+   five? This would replace the deliberately large universal witness.
+   Start with the complement sets of the already computed four-word masks
+   and their common right translates. This is a new covering problem;
+   the present certificate does not settle it.
+2. Which changed physical contract realizes one of these shared-direction
+   factors? Start with a named producer and consumer and account for
+   coefficient preparation, overwrites and restoration. All such physical
+   costs are unknown; this formal result does not authorize a supplier
+   construction campaign.
+
+## Credit
+
+This contribution was produced by Nick Petalas. Credit ToikY #4334 for the
+product-field question and two-role common-direction construction;
+Nick Petalas #4243/#4265/#4276/#4749 for the retained cost framework; and
+Wentao Li #4099 following #2513 for the alphabet and column bound. Classical
+memoryless-computation work by Gadouleau, Riis, Cameron and Fairbairn is
+linked in PROOF.md. Predecessor files and credit are unchanged. Apache-2.0.

research/right-vector-three-role-products/SOURCES.json

@@ -0,0 +1,30 @@
+{
+  "schema_version": 1,
+  "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395",
+      "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602",
+      "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72"
+    },
+    {
+      "path": "research/right-vector-commutative-products/PROOF.md",
+      "usage": "input",
+      "git_blob": "f149515c1684ac16bcb1ef0fd014b98d6f92f5db",
+      "sha256": "b401a15bc3a11e2040cdde9d99d4a5b8ec7b4f92643eac547f21b7c667fbf408"
+    },
+    {
+      "path": "research/right-vector-diagonal-free-basis/PROOF.md",
+      "usage": "input",
+      "git_blob": "0964deb3438280a08774d3de3f55de58ce6d9389",
+      "sha256": "e8bd7ab05fab6a929d0bb5303a823ba3d0105271d67af75e5d68b86601093a12"
+    }
+  ]
+}

research/right-vector-three-role-products/TASK.json

@@ -0,0 +1,74 @@
+{
+  "schema_version": 1,
+  "task_id": "connector-alphabet-change",
+  "priority_revision": 7,
+  "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43",
+  "original_card": {
+    "id": "connector-alphabet-change",
+    "question": "Does one explicit extension of the connector alphabet offer a favorable completed budget?",
+    "starting_points": [
+      "docs/research/research-family-status.md",
+      "research/universal-connector-boundary/README.md",
+      "certificates/selected-result.json"
+    ],
+    "methods": [
+      "Construct and charge a legal extra operation on a minimal instance.",
+      "Prove a target-specific bound after adding one specified operation family."
+    ],
+    "acceptance_gate": "State which fixed-alphabet premise changes and charge its implementation; do not declare it free. 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",
+        "research/universal-connector-boundary/verify.py"
+      ],
+      "expected": "PASS_UNIVERSAL_CONNECTOR_BOUNDARY",
+      "inspect": "Reproduce the 945-pairing control, then read Exact interface to list the allowed calls.",
+      "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay."
+    },
+    "first_experiment": "Add exactly one legally priced operation and test a tiny dirty-input instance before enumerating larger cases.",
+    "bottleneck_link": "A new legal connector operation could change recursive interface cost; a larger census in the same alphabet is a separate side result.",
+    "allowed_variations": [
+      "Choose one additional operation and a small source count for its first counterexample."
+    ],
+    "scope_change_triggers": [
+      "Keeping the alphabet and only increasing the source count; record this as a changed assignment.",
+      "Extending a source-count census without naming a supplier/interface decision it could change; audit #2973 pruning concerns before relying on the affected predecessor exclusions."
+    ],
+    "overlap_terms": [
+      "universal connector",
+      "source-toggle",
+      "connector alphabet"
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "The exact universal paid right-vector cost for invertible three-role targets over F2^k, including arbitrary common free GL3(F2) maps.",
+  "scope_change_reason": "This is an algebraic side question extending ToikY #4334 from two to three roles. It does not add a physically priced connector operation or claim a favorable complete supplier budget.",
+  "bottleneck_link": "Side result: the sharp common-direction obstruction rules out extending the two-role three-factor bound to three roles without extra cost. Native realization and complete recursive cost are unknown.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop at the first verified sharp finite result; do not minimize the component count or extend to other fields.",
+  "outcome": "completed",
+  "evidence": "All 2401 four-direction words reach at most 144 endpoints. The fixed five-direction word reaches all 168 GL3(F2) elements. Independent permutation enumeration agrees on every full mask. PROOF.md gives the all-k reduction and arbitrary-free-map lower bound.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "What is the least k for which an invertible target over F2^k costs five?",
+      "why_it_matters": "It would make the universal 168-component obstruction smaller.",
+      "first_step": "Use complements of the computed four-word masks and their common right translates as a covering instance.",
+      "blocked_by": "The exact covering problem is unrun; the current witness is not claimed minimal."
+    },
+    {
+      "question": "Can a literal physical producer and consumer implement one shared-direction factor at a favorable complete cost?",
+      "why_it_matters": "Formal factors alone do not imply native supplier savings.",
+      "first_step": "Specify coefficient acquisition, overwrite, access and reversible restoration before pricing the complete invoice.",
+      "blocked_by": "All physical preparation, routing, precision, stock and restoration costs remain unknown."
+    }
+  ],
+  "upstream_checkpoint": {
+    "commit": "624de9dc66858af0945e5f8a0942488d62280d43",
+    "checked_at": "2026-10-22T20:23:34.456826+00:00",
+    "priority_revision": 7
+  },
+  "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19132081"
+}

research/right-vector-three-role-products/VERIFY.json

@@ -0,0 +1,35 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/right-vector-commutative-products/PROOF.md",
+    "research/right-vector-diagonal-free-basis/PROOF.md"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "-W",
+        "error",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Exact matrix and independent eight-vector-action endpoint masks; 614656 parameter tuples; fixed five-factor witnesses; all common free maps; delta; seven rejection controls; generated file-bound receipt."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-O",
+        "-B",
+        "-W",
+        "error",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Exact matrix and independent eight-vector-action endpoint masks; 614656 parameter tuples; fixed five-factor witnesses; all common free maps; delta; seven rejection controls; generated file-bound receipt."
+    }
+  ]
+}