Prove the sharp singular rank-one product threshold (no new κ)

research/singular-product-threshold/PROOF.md

@@ -0,0 +1,155 @@
+# Singular rank-one product threshold
+
+Let K be a field and R=K^k for a positive finite k. Scalars embed diagonally
+in R. Use two roles. Paid factors are I+u y^T, where u belongs to R^2 and y
+belongs to K^2. Common GL_2(K) maps are free anywhere. A target is an ordered
+tuple M=(M_1,...,M_k) of 2-by-2 matrices over K. All M_i in the main theorem
+have rank exactly one. Cost means the least number of paid factors.
+
+## Cited criterion and the changed target contract
+
+Nick Petalas's #4276, Theorem B, states that cost(M)<=2 exactly when common
+G,H in GL_2(K) make N=GMH satisfy N12 in the right ideal N11 R. This criterion
+allows singular targets. We cite it as a predecessor theorem, rather than
+claiming or auditing it. Free maps can be collected at one endpoint by
+#4243's normal form, following Wentao Li's #4099/#2513 alphabet.
+
+For R=K^k, right-ideal membership is componentwise. Write t for the first
+column of H and phi for the first row of G. The other column of H completes
+t to a basis. In component i the ideal condition is equivalent to
+
+```text
+phi M_i t != 0, or phi M_i = 0.
+```
+
+Indeed a nonzero pivot generates the entire field. A zero pivot requires
+the other entry of the row to be zero, which means the entire row is zero.
+Conversely every nonzero t and phi extend to suitable H and G. Thus the
+displayed condition must hold for every i with the SAME t and phi.
+
+ToikY's #4334 studies invertible components, for which a zero row is
+impossible, and proves the sharp threshold q+1. The present theorem changes
+every component to a nonzero rank-one matrix. The zero-row alternative is
+essential, so applying the invertible common-unit-pivot test would be wrong.
+Nick Petalas's #4601 leaves singular local-product targets open.
+
+## Theorem 1: exact kernel/image criterion
+
+For each line T in K^2, let S_T be the span of the image lines im(M_i) for
+those i with ker(M_i)=T. The span of an empty collection is zero. Then
+
+```text
+cost(M)<=2  iff  some T has dim(S_T)<=1.
+```
+
+Proof. Fix a nonzero t spanning T. If t is not in ker(M_i), then M_i t is a
+nonzero vector spanning im(M_i). Every phi either evaluates nontrivially on
+this vector or kills the entire image. Both satisfy the cited criterion.
+If ker(M_i)=T, then M_i t=0. The criterion requires phi to kill im(M_i).
+Therefore a common nonzero phi exists exactly when it kills S_T, which is
+equivalent to dim(S_T)<=1 in a two-dimensional space. Taking all T proves
+both directions.
+
+## Lemma 2: three factors suffice
+
+In fact every target in M_2(K^k), without any rank assumption, has cost at
+most three. It is enough to factor each component with the common ordered
+right vectors e1,e2,e1. Left-vector entries can vary by component, so the
+following per-component choices assemble into three paid R-valued factors.
+
+For M_i=[[a,b],[c,d]] with b=0 use
+
+```text
+[[a,0],[c,1]] [[1,0],[0,d]] I = M_i.
+```
+
+For b!=0 put l=(d-1)/b, f=c-l*a, and e=a-b*f. Then use
+
+```text
+F1=[[1,0],[l,1]], F2=[[1,b],[0,1]], F3=[[e,0],[f,1]].
+F1 F2 F3 = [[e+b*f,b],[l*(e+b*f)+f,l*b+1]] = M_i.
+```
+
+Every displayed factor is I+u e_j^T for its stated right vector. The
+identity may use e1 and a zero left vector. These are algebraic product
+orders, so column-vector execution applies F3 first. No free endpoint is
+needed. The construction extends the invertible-only upper-word scope in
+#4334 to this pure-field product domain. It does not apply to general local
+algebras, where a nonzero b may fail to be invertible.
+
+## Theorem 3: sharp finite-field threshold
+
+Let K=F_q. Among tuples with all component matrices nonzero and rank one,
+
+```text
+k < 2(q+1): every target has cost <=2;
+k >= 2(q+1): some target has exact cost 3;
+every target has cost <=3.
+```
+
+Proof. There are q+1 possible kernel lines. If cost(M)>2, Theorem 1 says
+that every S_T has dimension two. Each such span needs at least two
+component matrices with kernel T and distinct image lines. A component has
+only one kernel, so k>=2(q+1).
+
+For sharpness, for each T choose a nonzero row r_T with kernel T. Include
+both e1*r_T and e2*r_T as component matrices. They have rank one, share
+kernel T and have different image lines. Now every S_T=K^2. Theorem 1
+excludes two factors, while Lemma 2 gives three. For larger k repeat any
+component. Repetition preserves the obstruction and the three-factor word.
+This proves all assertions.
+
+Over an infinite K, a finite tuple omits some possible kernel line T.
+Then S_T=0, and every such rank-one tuple costs at most two. This is a
+direct case of Theorem 1, not a finite-field enumeration claim.
+
+## Binary finite certificate
+
+Over F2 there are nine nonzero rank-one matrices. Literal zero-, one- and
+two-factor images are enumerated with all common free endpoints and all
+right-vector lines. Allowing arbitrary left vectors includes singular paid
+factors. Projective representatives suffice because a nonzero rescaling of
+y can be absorbed in u. A free map anywhere can be collected at the right
+endpoint by the cited normal form.
+
+For fixed common right-vector lines and endpoint, every component may
+choose its left vectors independently. Thus a tuple belongs to this chart
+exactly when every component belongs to its local image. Membership depends
+only on its support among the nine matrices. Comparing all 2^9 support
+sets with Theorem 1 is an exhaustive comparison for tuples of ANY length
+over this binary rank-one alphabet, without enumerating infinitely many
+tuples. There are 64 support sets outside the two-factor image, with minimum
+size six. A finite recurrence enumerates ordered-tuple multiplicities,
+starting with the empty support and adding one of nine entries at each
+step. It covers every tuple through length six exactly once.
+
+At length six the resulting exact cost histogram is
+
+```text
+cost 0: 0; cost 1: 567; cost 2: 511434; cost 3: 19440.
+total: 531441 = 9^6.
+```
+
+The 19,440 count also follows from the threshold criterion. Assign the six
+ordered positions in pairs to the three kernel lines, in 6!/(2!)^3=90 ways.
+For each kernel the ordered pair has 3*2=6 different image-line choices,
+and over F2 each kernel/image pair specifies one matrix. Thus the count is
+90*6^3=19440. The verifier checks the literal chart census independently of
+this arithmetic count.
+
+## Scope and credit
+
+The quantified result is a scoped algebraic proof, with a separate finite
+certificate over the stated binary domain and finite word checks over five
+fields. It is not a complete multiplication theorem. Native preparation,
+access, routing, restoration, precision, stock and complete supplier costs
+are unknown. Local radical lifts, matrix-algebra blocks, mixed-rank lower
+thresholds and more than two roles are outside scope. No supplier admission
+or new kappa is claimed. Independent human and formal proof-kernel review
+are unclaimed.
+
+This package was produced by Nick Petalas. The exact low-factor criterion
+and common-free normal form are credited above to Nick Petalas, the
+invertible-product predecessor and open gap to ToikY, and the alphabet and
+column bound to Wentao Li following #2513. Projective-line counting and
+elementary matrix multiplication are classical. Apache-2.0.

research/singular-product-threshold/README.md

@@ -0,0 +1,152 @@
+# Sharp threshold for singular right-vector products
+
+Scoped algebraic proof with a finite certificate. No new kappa.
+
+Let K=F_q and R=K^k. Use two roles, paid factors I+u y^T with u in R^2
+and y in K^2, and common GL_2(K) maps free anywhere. Suppose every component
+of a target M=(M_1,...,M_k) is a nonzero rank-one matrix. Then
+
+```text
+k < 2(q+1): every target costs at most two paid factors.
+k >= 2(q+1): some target costs exactly three.
+Every target costs at most three.
+```
+
+This answers a singular-target part of the open direction in ToikY's #4334
+and Nick Petalas's #4601. Their invertible-component threshold is q+1.
+The changed singular contract permits a zero pivot when the entire row
+vanishes, so the invertible common-unit-pivot test does not apply.
+
+The new exact criterion is particularly simple. For each input line T,
+collect the image lines of components having kernel T. Two paid factors
+suffice exactly when at least one T has at most one distinct collected
+image line. An obstruction therefore needs two different image lines for
+EVERY kernel line. An explicit family with two components per kernel
+attains the threshold. Over an infinite field every finite such tuple
+costs at most two. The [proof](PROOF.md) cites #4276's low-factor criterion
+and supplies a common-right-vector e1,e2,e1 word for the three-factor bound.
+No predecessor code or verifier is imported or replayed.
+
+## Exact finite evidence
+
+The standalone standard-library verifier constructs literal binary one- and
+two-factor images with every paid left vector, common right-vector line and
+common free endpoint. It includes singular paid factors. The complete
+rank-one alphabet has nine matrices, so all 512 support sets suffice to
+compare literal membership with the new criterion for tuples of any length.
+There are 64 obstructed supports, all with at least six distinct matrices.
+A finite support recurrence counts ordered tuples through six components.
+It is an exact multiplicity enumeration, not a raw scan of every tuple.
+
+```text
+components   tuples   cost 1    cost 2   cost 3
+1                 9        9         0        0
+2                81       27        54        0
+3               729       63       666        0
+4              6561      135      6426        0
+5             59049      279     58770        0
+6            531441      567    511434    19440
+```
+
+All these targets have cost greater than zero because every component is
+singular. The six-component count 19,440 is also derived directly in the
+proof. The code checks that count against the literal-chart enumeration.
+
+Over F2,F3,F4,F5,F7 the verifier checks the three-factor word on every
+2-by-2 matrix, including singular and zero matrices. This covers 3,379
+matrices and 138,163 arbitrary-input evaluations. F4 is implemented as
+F2[t]/(t^2+t+1). It also checks the sharp threshold witnesses at component
+counts 6,8,10,12,16 and all 52 single-component deletions. Field-table
+associativity, distributivity and inverses are checked before using them.
+
+Controls discriminate separate component charts, repeated equal image
+lines, reversing the word, omitting its final factor, odd-field sign errors
+and using the composite modulus six as a field. The deletion controls show
+that every component of the explicit threshold witness matters. Checks use
+explicit exceptions and remain active under Python optimization.
+
+Every run emits a generated JSON receipt binding all six package files by
+SHA256, followed only by stdout data. No receipt is hand-written or saved
+in the checkout.
+
+## Reproduction
+
+From the repository root, using the Python 3.12 standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B -W error research/singular-product-threshold/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -O -B -W error research/singular-product-threshold/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/singular-product-threshold
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/singular-product-threshold --check-source-history
+```
+
+Any CPython 3.12 installation can replace the local interpreter above.
+Expected verifier marker is
+`PASS_SINGULAR_PRODUCT_THRESHOLD binary_cost3=19440 threshold=6 no_new_kappa`.
+Both normal and optimized checks are registered with 120-second limits.
+SOURCES.json binds the predecessor statements and task catalogue as historical
+provenance at base 624de9dc66858af0945e5f8a0942488d62280d43. There are no live
+external inputs and no dependence on an unmerged Git object.
+
+The original formal-interface-lemma card is explicitly changed to this
+algebraic side question in TASK.json. Its historical first command,
+`scripts/research_baseline.py`, fails with `KeyError: 'bit_lower'` on the
+changed selected schema. After materializing the selected source closure,
+`scripts/research_selected_baseline.py` passes with selected 60403/20000000.
+That orientation check authenticates metadata only. No shared helper is changed.
+
+## Limits and verification design
+
+The universal claim is the written scoped proof. The exhaustive support
+certificate is binary; other fields have the finite word and sharp-witness
+checks stated above. Local radical lifts, non-field factors, mixed-rank
+thresholds and more than two roles remain outside the main theorem. The
+three-factor construction alone covers arbitrary matrices over K^k.
+
+Native coefficient preparation, access, routing, control, restoration,
+precision, stock and complete supplier costs are unknown. No supplier,
+selected frontier or complete multiplication theorem changes. Independent
+human and formal proof-kernel review are unclaimed. No Lean, Docker or
+selected operator replay is needed for or included in this isolated package.
+
+The code has no recursion, child process, network access, solver or CLI input.
+The field orders are restricted to five fixed cases with q<=7. Field-table
+loops use at most 7^3 triples; matrix loops use at most 7^4 targets; vector
+loops use at most 7^2 inputs. Binary image construction uses 3*6*3*4^2=864
+two-factor cases. Each support table and recurrence dictionary has at most
+512 entries; there are exactly six recurrence rounds. The sharp families
+have at most 16 components. Receipt reads are limited to six fixed files
+of at most 1 MiB each. The program writes only to stdout.
+
+Power of Ten rule 3 has a managed-runtime deviation. Python allocates
+integers, tuples and finite sets during enumeration. The explicit fixed
+domains bound live state to the 512-entry support/counter tables, tiny field
+and literal-image tables, and one matrix/word at a time. A fixed-buffer
+implementation would be the follow-up if the domains expand. Functions
+remain below the 60-line review ceiling. Warning-strict normal and optimized
+runs are registered in CI; no separate type checker or linter is required.
+
+## Open next questions
+
+1. What replaces the kernel/image criterion for rank-one residue targets
+   over products of local algebras? Start with two specified dual-number
+   components and enumerate their right-ideal constraints. Nilpotent
+   off-pivot entries can invalidate a zero residue pivot, so the field
+   threshold does not settle that question.
+2. Can one literal native producer/consumer realize the common-right-vector
+   alphabet at a favorable complete cost? First specify its coefficients,
+   access, restoration and precision contracts and full bill. Those physical
+   obligations are unknown; the formal word supplies none of them.
+
+TASK.json records why each question matters and its first bounded step.
+
+## Credit
+
+This package was produced by Nick Petalas. ToikY's #4334 supplies the
+invertible field-product predecessor and its singular-target gap. Nick
+Petalas's #4601 supplies the local-product follow-up, #4276 supplies the
+exact low-factor criterion, and #4243 supplies the common-free normal form.
+Wentao Li's #4099 supplies the alphabet and column bound, building on #2513.
+Projective-line counting and elementary matrix algebra are classical.
+The new contribution is the singular kernel/image criterion, its sharp
+threshold and the stated finite certificate. Apache-2.0.

research/singular-product-threshold/SOURCES.json

@@ -0,0 +1,36 @@
+{
+  "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-two-factor-criterion/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "71888afa0db63d6d332cbbdc408abf1aa879681c",
+      "sha256": "c1065c51c839d11b0d31bccb8d39ebc07a869eb0f29899038518e3090a58c895"
+    },
+    {
+      "path": "research/right-vector-commutative-products/README.md",
+      "usage": "provenance",
+      "git_blob": "fc9889d41621b596209c707b6057517744b4642f",
+      "sha256": "6222431360182204f502334d1c707eefc39a174d06578ef75c52f37b5873055f"
+    },
+    {
+      "path": "research/right-vector-local-products/README.md",
+      "usage": "provenance",
+      "git_blob": "e7886eba302aecd0f0111e76d9908ce8809f3262",
+      "sha256": "815089fc8c4ac15cffc20b3b529e232840bf675627e8a91cc01590e0f593b65f"
+    }
+  ]
+}