Construct common three-factor words for all matrix-algebra component targets

research/matrix-product-common-three-factor/PROOF.md

@@ -0,0 +1,122 @@
+# One common ABA word for every finite product of full matrix algebras
+
+JoyboyBrian, with substantial OpenAI Codex assistance. Apache-2.0.
+This is a written formal-alphabet theorem, not a physical supplier theorem.
+
+Let K be a field and R=product_{i=1}^k M_{m_i}(K), with finite k>=1 and
+m_i>=1. Scalars embed diagonally in every component. On two roles a paid
+factor is I+u y^T, u in R^2 and y in K^2. Common GL2(K) maps may be free,
+but the construction below uses NONE. No auxiliary roles are introduced.
+Targets may be singular, zero, or invertible, independently in each component.
+
+**Theorem.** Every M in M2(R) is the product of three paid factors with the
+SAME ordered right vectors e1,e2,e1 in every component. Thus every finite
+tuple of singular targets over (M2(F2))^k satisfies the claimed three-call
+contract. There is no component-count obstruction to this bound.
+
+The input lemma is Nick Petalas PR4805, exact head
+fbf2bd033f2d3ae1605a3cad690e1fc2fbf477e7,
+research/matrix-algebra-three-factor/PROOF.md, sections 'A classical subspace
+lemma' and 'Lifting the complement to a graph'. That source chooses free
+block swaps before applying the lemma. We eliminate the component-dependent
+swaps by a row-space completion and absorb its generally singular map into
+one paid factor. We retain the lemma's credit; classical basis extension is
+not claimed as new. PR4780 already supplies a common ABA word for pure field
+products. PR4749 covers invertible semilocal targets; neither settles the
+singular noncommutative product endpoint stated here.
+
+## 1. Complete the top row without charging a free algebra-valued map
+
+First consider a single component M=[[A,B],[C,D]], each block m by m.
+The row space of [A B] has dimension r0<=m in K^(2m). Extend a basis of that
+space to m independent rows, forming T=[X Y] of rank m. Every original row
+has unique coordinates in these rows, so a matrix a in M_m(K) satisfies
+
+    [A B] = a [X Y].
+
+There is no need for a to be invertible. Define
+
+    N = [[X,Y],[C,D]],     M = diag(a,I_m) N.
+
+This equality is only an intermediate algebraic identity: diag(a,I) is NOT
+assumed free or independently charged. It will be absorbed below. If the
+original top row is zero, take any m independent rows for T and a=0. The
+same construction includes M=0 without using an inverse of a.
+
+## 2. The predecessor graph lemma applies in this fixed chart
+
+Write W=im N, V=im [Y;D], and let pi be projection to the first output
+K^m. Since T has rank m, pi(W)=K^m. Thus Z=W intersect ker pi has dimension
+rank(N)-m. The first block column of N has at most m independent columns,
+so rank(N)<=m+dim V. Consequently dim Z<=dim V.
+
+PR4805's classical subspace lemma gives a complement U of V inside W with
+U intersect Z=0. Since U is contained in W, this also means U intersect
+ker pi=0. The proof works over every field, including F2; its union-of-two-
+proper-subspaces step requires no generic/random field choice.
+
+As in the cited graph lemma, N^{-1}(U) surjects onto the quotient of the
+input space by its second coordinate block: subtracting a vector in that
+block changes N's image by V, and W=U+V. Choose a linear section. Its image
+is the graph of -F for some m by m matrix F. Therefore
+
+    [X-YF; C-DF]
+
+has image in U. Injectivity of pi on U gives
+ker(X-YF) subset ker(C-DF). Extend the resulting linear map from im(X-YF)
+to K^m to obtain b satisfying C-DF=b(X-YF). Set E=X-YF and d=D-bY. Then
+
+    N = [[I,0],[b,I]] [[I,Y],[0,d]] [[E,0],[F,I]].
+
+This is the predecessor multiplication in the original fixed chart; there
+are no residual row swaps, column swaps or endpoint GL2 maps. The dimension
+inequality was proved directly, rather than invoking the predecessor's
+chart-selection procedure.
+
+## 3. Absorption and simultaneous component assembly
+
+Multiply the preceding identity on the left by diag(a,I). The full target
+is exactly
+
+    M = [[a,0],[b,I]] [[I,Y],[0,d]] [[E,0],[F,I]].       (1)
+
+The first factor equals I+(a-I,b)^T e1^T, even if a is singular or zero.
+The second equals I+(Y,d-I)^T e2^T; the third equals
+I+(E-I,F)^T e1^T. All three are legal. Column-data execution applies the
+rightmost factor first; equation (1) is algebraic product order.
+
+Apply this construction separately to each component. Assemble a,b,Y,d,E,F
+as tuples in R. Since each component uses the same right-vector sequence,
+these tuples give exactly three R-valued paid factors. This uses neither
+component-specific free scalar maps nor free internal-coordinate changes.
+The full two-role endpoint, including every off-diagonal block, is equation
+(1). No independent-component work is silently declared free.
+
+## 4. Cost and scope
+
+This is an upper bound of three formal paid updates, uniform in k. It does
+not say that every endpoint needs three: zero and many singular endpoints
+need fewer. Exact lower costs are governed by PR4276's inherited one/two-
+factor criteria applied over the PRODUCT algebra with common scalar charts.
+For example PR4780's binary six-component scalar rank-one tuple has cost
+three, not more than three. Embed its scalar entries as scalar I2 matrices:
+the common two-factor rank criterion remains the identical scalar condition,
+so this gives a singular tuple in the primary (M2(F2))^k domain with exact
+cost three. The new upper construction supplies the matching word.
+
+Finite executions test an explicitly bounded domain and corroborate the
+proof. They do not establish the all-field or arbitrary-k statement by
+extrapolation. The constructive proof establishes that statement. Native
+preparation of arbitrary matrix coefficients, overwritten-data recovery,
+physical ownership/routing/cleanup, precision, stock and a recursive supplier
+invoice remain unknown. There is no new kappa or selected-frontier change,
+and no independent human or kernel proof acceptance is claimed.
+
+## Open next questions
+
+Can the same uniform skeleton be lifted through a singular radical extension
+of a product of matrix algebras? Residue factorization alone need not lift
+singular equations. Begin with a named square-zero extension and a complete
+endpoint, preserving PR4776's existing radical obstructions. A physical
+application separately needs a real producer/consumer and a fully charged
+coefficient/overwrite/restoration bill before further construction expansion.

research/matrix-product-common-three-factor/README.md

@@ -0,0 +1,38 @@
+# Common three-factor words for noncommutative component targets
+
+Every two-role target over a finite product of full matrix algebras has a
+three-factor word with the same right vectors e1,e2,e1 in every component.
+This includes arbitrary singular and zero components. No free endpoint maps
+or auxiliary roles are used. The binary six-component singular tuple from
+PR4780, embedded as scalar I2 blocks, proves the uniform bound is sharp.
+
+PR4805 supplies each individual component with a three-factor construction
+but chooses free charts separately. Here row-space completion makes its graph
+lemma apply at one fixed chart. Absorbing the completion into the first paid
+factor closes the simultaneous endpoint. See [PROOF.md](PROOF.md).
+
+This is a formal algebra theorem, not a physical BIT decoder or supplier.
+All coefficient preparation, overwritten-data recovery, physical routing,
+precision, stock and recursive costs remain unpriced. No kappa changes.
+
+Run `python3.12 -I -B research/matrix-product-common-three-factor/verify.py`.
+The verifier reuses credited PR4805 linear algebra helpers, while independent
+matrix multiplication, rank/chart checks and dirty-input execution verify the
+result. Finite controls corroborate the written all-field/all-component proof.
+No historical exhaustive suite, Lean or native supplier replay is run.
+
+## Sources and credit
+
+Nick Petalas PR4805 supplies the complement/graph lemma and retained helper
+code; PR4276 the one/two-factor criterion; PR4780 the pure-field-product word
+and sharp scalar tuple. Credit PR4749/#4243, ToikY/#4334, Wentao Li/#4099
+following #2513, and classical basis extension/complement arguments. Exact
+base, source SHA256 and Git blobs are retained in SOURCES.json.
+New contribution by JoyboyBrian with substantial OpenAI Codex assistance;
+Apache-2.0. Agent review does not assert human or kernel acceptance.
+
+## Open next questions
+
+Prove an appropriate singular radical-lifting result, or bind a real native
+caller and pay its full coefficient/overwrite/restoration invoice before
+claiming a physical benefit. These are distinct from semisimple assembly.

research/matrix-product-common-three-factor/RESULT.json

@@ -0,0 +1,23 @@
+{
+  "block_sizes": [
+    1,
+    2,
+    3,
+    4
+  ],
+  "complete_binary_rank_le_one_targets": 226,
+  "controls": 30,
+  "dirty_executions": 96,
+  "factor_digest": "c7533032403af510fb1128e2a06ad0a1867e217b803c6bb180d1d31e4f2b24f0",
+  "fields": [
+    2,
+    3,
+    5,
+    7
+  ],
+  "schema_version": 1,
+  "scope": "written all-field finite-product theorem; bounded finite corroboration",
+  "sharp_singular_components": 6,
+  "status": "PASS_COMMON_ABA",
+  "targets": 1286
+}

research/matrix-product-common-three-factor/REVIEW.json

@@ -0,0 +1,22 @@
+{
+  "status": "PASS_DRAFT_UPPER_CONSTRUCTION_REVIEW",
+  "proof_sha256": "74e7821fa524d7b485b3537a92b1174bd87463da63963c0c1472c12d47c35efc",
+  "reviewer": "root Astra independent derivation",
+  "scope": "Complete upper-bound proof sections1-3, primary all singular binary M2 finite products and stated general finite-product lemma",
+  "findings": [],
+  "reasoning": [
+    "Extend row span of[A B] to m independent rowsT; unique coordinates give possibly singular a, M=diag(a,I)N.",
+    "For full top rankm: dim(W intersectkerpi)=rankN-m<=rank secondblockcolumn. Actual predecessor complement lemma applies without either swap.",
+    "Graph lift implies C-DF=b(X-YF); direct multiplication identity for N is exact over any field.",
+    "Left absorption yields legal e1 factor [[a,0],[b,I]], includinga=0; second/third legale2/e1.",
+    "Componentwise assembly has common scalar rightvectors, no free component chart."
+  ],
+  "remaining": [
+    "Validate sharp all-singular tuple embedding against exact shared-scalar twofactor criterion, not assumed independent component optimization.",
+    "Review final constructor/verifier/sourcepins and final proofbytes before publication."
+  ],
+  "no_claims": [
+    "No physical coefficient-preparation or ownership/cleanup tariff.",
+    "Not proof-kernel or independent human review."
+  ]
+}

research/matrix-product-common-three-factor/SOURCES.json

@@ -0,0 +1,55 @@
+{
+  "schema_version": 1,
+  "base_commit": "a5df48c55ea806d7952b65acc9c76d878ff09b13",
+  "files": [
+    {
+      "path": "research/matrix-algebra-three-factor/PROOF.md",
+      "usage": "input",
+      "sha256": "90cdf1d73621c5d71e901f8952f28db1d1cd342ac3e20b4b324f6af071b260cf",
+      "git_blob": "b134eed43d32c6d953956d15bd3ae699dc718758"
+    },
+    {
+      "path": "research/matrix-algebra-three-factor/verify.py",
+      "usage": "input",
+      "sha256": "97483d6e2cf41064bd8a98766243c8c36db0bc92676ff4d43981b859eb49fb80",
+      "git_blob": "e9dfe58a3e1883cee188a934c68392b4fc30d678"
+    },
+    {
+      "path": "research/right-vector-two-factor-criterion/PROOF.md",
+      "usage": "input",
+      "sha256": "c1065c51c839d11b0d31bccb8d39ebc07a869eb0f29899038518e3090a58c895",
+      "git_blob": "71888afa0db63d6d332cbbdc408abf1aa879681c"
+    },
+    {
+      "path": "research/singular-product-threshold/PROOF.md",
+      "usage": "input",
+      "sha256": "8d1e445bddb4d075603f2c95d59b3b41c0b8400889b282ef65135318d416c875",
+      "git_blob": "a36f102ede6e5f7b5c710bbc9c4dbe2758eae2f9"
+    },
+    {
+      "path": "research/right-vector-semilocal/PROOF.md",
+      "usage": "input",
+      "sha256": "12d72032a3ff8174a8ba4e68c89fba6c1479b785ea0a7a5ca7482b2c0c6247e2",
+      "git_blob": "3cd62bfe9800856f14f3089b179ce724b09ee05a"
+    },
+    {
+      "path": "LICENSE",
+      "usage": "input",
+      "sha256": "c71d239df91726fc519c6eb72d318ec65820627232b2f796219e87dcf35d0ab4",
+      "git_blob": "261eeb9e9f8b2b4b0d119366dda99c6fd7d35c64"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72",
+      "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602"
+    },
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375",
+      "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395"
+    }
+  ],
+  "attribution": "Nick Petalas PR4805 complement/graph proof and linear algebra helpers; PR4276 exact criterion; PR4780 scalar-product control; original notices retained"
+}

research/matrix-product-common-three-factor/TASK.json

@@ -0,0 +1,70 @@
+{
+  "schema_version": 1,
+  "task_id": "bit-new-register-model",
+  "priority_revision": 7,
+  "base_commit": "a5df48c55ea806d7952b65acc9c76d878ff09b13",
+  "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_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Read Model section 1 of the three-register bound and identify the exact excluded free operations.",
+      "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay."
+    },
+    "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": "A common fixed ABA three-factor word for arbitrary finite products of full matrix algebras, closing the singular binary M2-product handoff",
+  "scope_change_reason": "Formal-alphabet side result from PR4805: remove component-dependent free charts; no native admission",
+  "bottleneck_link": "Resolves simultaneous complete-endpoint factorization, not physical supplier costs",
+  "budget_minutes": 60,
+  "stop_rule": "Stop at proved shared constructor or precise common-skeleton handoff; no word census",
+  "outcome": "completed",
+  "evidence": "PROOF.md, constructor.py, RESULT.json",
+  "author": "JoyboyBrian",
+  "ai_assistance": "Substantial OpenAI Codex assistance; separate agent/root review, not human/kernel acceptance",
+  "open_questions": [
+    {
+      "question": "Lift through a singular radical extension",
+      "why_it_matters": "Semisimple component assembly does not solve singular radical equations",
+      "first_step": "Specify a square-zero extension and full endpoint, respecting existing radical obstructions",
+      "blocked_by": "Lifting singular factor equations is not established"
+    },
+    {
+      "question": "Price a literal native producer/consumer",
+      "why_it_matters": "Formal updates overwrite data and arbitrary coefficients are unpriced",
+      "first_step": "Bind one source caller with complete ownership and restoration contract",
+      "blocked_by": "Physical preparation, routing, precision and stock costs are unknown"
+    }
+  ]
+}

research/matrix-product-common-three-factor/VALIDATION.md

@@ -0,0 +1,37 @@
+# Validation scope
+
+Python 3.12.2, macOS27.0 arm64, standard library. Registered ordinary and
+optimized commands pass in about three seconds together. The receipt is
+regenerated from 1286 constructor executions, not an all-target census:
+226 distinct binary rank-at-most-one 4x4 targets, zero/identity and 64 seeded
+samples per (field,block-size) pair, and four source-cut fixtures. Sample
+families may overlap. Fields are 2,3,5,7 and block sizes1..4. The written proof,
+not these bounded checks, establishes generality.
+
+The independent endpoint oracle does not use predecessor multiplication or
+rank helpers: it checks all fixed columns, full products, and common-chart
+rank equality with its own elimination. Six embedded scalar rank-one
+components have no common two-factor chart, despite each individually having
+one. All96 component dirty-vector executions pass. Thirty executed controls
+cover illegal fixed columns, chronology, omitted factors and invalid input.
+No independent human or proof-kernel acceptance is claimed.
+
+ROOT REVIEW.json records the exact hash and scope of separate root proof
+review; it reviews the upper theorem and lists later checks separately.
+Source-history/committed-byte and official export integrity are publication
+checks. Git-free cold replay and deliberate source/typed-receipt corruption
+checks are recorded in the external publication receipt, rather than claimed
+as mathematical or hosted-CI acceptance. No selected/native/Lean replay.
+
+Commands:
+
+```
+python3.12 -B scripts/research_package.py --package research/matrix-product-common-three-factor
+python3.12 -B scripts/check_research_commit.py --package research/matrix-product-common-three-factor --check-source-history
+python3.12 -B scripts/export_research_package.py export --package research/matrix-product-common-three-factor --ref HEAD --output /tmp/common-three-factor.tar
+python3.12 -B scripts/export_research_package.py check /tmp/common-three-factor.tar
+```
+
+After safe extraction, run the direct `verify.py` command with Python3.12 -I
+-B and -O as desired; no Git or undeclared predecessor imports are needed.
+The retained PR4805 helper file is explicitly included by VERIFY.json.