diff --git a/research/matrix-product-common-three-factor/PROOF.md b/research/matrix-product-common-three-factor/PROOF.md new file mode 100644 index 0000000000..04dc020c9a --- /dev/null +++ b/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. diff --git a/research/matrix-product-common-three-factor/README.md b/research/matrix-product-common-three-factor/README.md new file mode 100644 index 0000000000..df3b9d2a47 --- /dev/null +++ b/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. diff --git a/research/matrix-product-common-three-factor/RESULT.json b/research/matrix-product-common-three-factor/RESULT.json new file mode 100644 index 0000000000..1a456e6945 --- /dev/null +++ b/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 +} diff --git a/research/matrix-product-common-three-factor/REVIEW.json b/research/matrix-product-common-three-factor/REVIEW.json new file mode 100644 index 0000000000..aa4da9695e --- /dev/null +++ b/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." + ] +} diff --git a/research/matrix-product-common-three-factor/SOURCES.json b/research/matrix-product-common-three-factor/SOURCES.json new file mode 100644 index 0000000000..b5c899e480 --- /dev/null +++ b/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" +} diff --git a/research/matrix-product-common-three-factor/TASK.json b/research/matrix-product-common-three-factor/TASK.json new file mode 100644 index 0000000000..e318a8b8df --- /dev/null +++ b/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" + } + ] +} diff --git a/research/matrix-product-common-three-factor/VALIDATION.md b/research/matrix-product-common-three-factor/VALIDATION.md new file mode 100644 index 0000000000..b05ad4c2f2 --- /dev/null +++ b/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. diff --git a/research/matrix-product-common-three-factor/VERIFY.json b/research/matrix-product-common-three-factor/VERIFY.json new file mode 100644 index 0000000000..3173f97a32 --- /dev/null +++ b/research/matrix-product-common-three-factor/VERIFY.json @@ -0,0 +1,41 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/matrix-algebra-three-factor/PROOF.md", + "research/matrix-algebra-three-factor/verify.py", + "research/right-vector-two-factor-criterion/PROOF.md", + "research/singular-product-threshold/PROOF.md", + "research/right-vector-semilocal/PROOF.md", + "LICENSE", + "docs/research/agent-task-catalog.json", + "certificates/selected-result.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "-Werror", + "{package}/verify.py" + ], + "timeout_seconds": 30, + "checks": "Common fixed ABA factors, full endpoint oracle, sharp singular tuple and rejection controls" + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "-Werror", + "{package}/verify.py" + ], + "timeout_seconds": 30, + "checks": "Same explicit checks under optimization" + } + ] +} diff --git a/research/matrix-product-common-three-factor/constructor.py b/research/matrix-product-common-three-factor/constructor.py new file mode 100644 index 0000000000..37d09cb578 --- /dev/null +++ b/research/matrix-product-common-three-factor/constructor.py @@ -0,0 +1,55 @@ +"""Common ABA constructor, retaining Nick Petalas PR4805 linear algebra. +JoyboyBrian, substantial OpenAI Codex assistance; Apache-2.0. +""" +import importlib.util +from pathlib import Path + +def load_source(root): + path=Path(root)/'research/matrix-algebra-three-factor/verify.py' + spec=importlib.util.spec_from_file_location('retained_matrix_constructor',path) + module=importlib.util.module_from_spec(spec) + exec(compile(path.read_bytes(),str(path),'exec'),module.__dict__) + return module + +def construct(source,target,q): + """Return three factors with right vectors e1,e2,e1; no free endpoints. + + Finite executable domain is prime fields 2,3,5,7 and 1<=m<=4. + The written proof is independent of these corroboration limits. + """ + s=source;m=len(target)//2 + s.check(q in (2,3,5,7) and 1<=m<=4 and len(target)==2*m,'constructor domain') + s.check(all(len(row)==2*m and all(type(x) is int and 0<=x