Classify exact singular polynomial right-vector costs (no new κ)

research/singular-polynomial-cost/PROOF.md

@@ -0,0 +1,138 @@
+# Exact singular polynomial costs
+
+Let K be any field, R=K[t], and let the two data roles have paid factors
+`I+u y^T`, where u is in R² and y is in K². Every GL2(K) map is free anywhere
+in a word. Cost means the least number of paid factors. No scratch is used.
+
+## Theorem
+
+The zero matrix has cost two. Every nonzero matrix M with det M=0 has a
+factorization `M=a b`, where a is a primitive column in R² and b is a nonzero
+row in R². Primitive means that the entries generate R. Write
+
+```text
+V = span_K{b1,b2},       d = monic gcd(b1,b2).
+```
+
+Its exact cost is
+
+```text
+1  if a belongs to K² and V contains a nonzero constant;
+2  otherwise, if a belongs to K² or d belongs to V;
+3  otherwise.
+```
+
+Multiplying a by a nonzero scalar and b by its inverse does not change these
+conditions. Every singular target is reachable with at most three factors,
+although invertible polynomial targets can have unbounded cost as in #4763.
+
+## Primitive factorization
+
+Choose a nonzero column c of M and divide its entries by their monic gcd g,
+obtaining a primitive a. Write the other column as c'. The determinant
+condition says that c' is a fraction-field multiple h a. Choose r,s in R
+with r a1+s a2=1. Then h=r c'1+s c'2 is a polynomial, so both columns are
+polynomial multiples of a. This constructs b and proves existence. Two such
+primitive a differ by a unit of R, hence by a nonzero scalar. These are
+classical PID and Bezout facts.
+
+A primitive a has a nonzero K-linear annihilating row exactly when a is in
+K². Indeed, a nonzero relation makes its entries proportional over K, and
+primitivity then makes the common polynomial factor a unit. The converse is
+ordinary two-dimensional linear algebra.
+
+## Three-factor construction
+
+For every column a and row b over any associative unital ring, direct
+multiplication gives
+
+```text
+[[a1,0],[a2,1]] [[1,b2],[0,0]] [[b1,0],[0,1]] = a b.
+```
+
+The three displayed factors have right vectors e1,e2,e1 respectively, so
+all are legal paid factors over R. This uses no free maps. Applying the same
+word with a=0 and b=0 also gives zero, but zero already equals the product
+`diag(0,1) diag(1,0)` of two paid factors.
+
+## Exact two-factor boundary
+
+We use Theorem B of Nick Petalas's #4276, not a new proof of that predecessor:
+a two-role target costs at most two exactly when some G,H in GL2(K) make
+`N=G M H` satisfy `N12 in N11 R`. In this case `N11 C=N12` supplies the
+literal two-factor word
+
+```text
+N = [[N11,0],[N21,1]] [[1,C],[0,N22-N21 C]].
+```
+
+For M=a b let phi be the first row of G and let x,z be the columns of H.
+Then `N11=(phi a)(b x)` and `N12=(phi a)(b z)`.
+
+If a is constant, choose phi annihilating a. Both entries vanish and the
+criterion passes. If a is not constant, the primitive observation above
+makes phi a nonzero for every allowed phi. Since R is an integral domain,
+its factor cancels. The criterion becomes `b x divides b z`. The two
+polynomials b x,b z generate the same ideal as b1,b2 because H is invertible.
+Thus b x must be a nonzero scalar multiple of d. Conversely, if d is a
+K-linear combination b x, then x is nonzero, extends to such an H, and d
+divides b z. This proves
+
+```text
+cost(M)<=2  iff  a is constant or d belongs to V.
+```
+
+The cancellation and unit statements are specific to K[t]. They do not
+assert the same classification in rings with zero divisors.
+
+## Exact one-factor boundary
+
+For every two-role target, cost at most one is equivalent to the existence
+of nonzero x,w in K² with Mx=w. To see necessity, put a one-factor word in
+the predecessor free-map normal form `(I+u y^T) S`. A nonzero constant v in
+ker y is fixed by the paid factor; take x=S^-1 v and w=v. The free-only case
+has the same property. For sufficiency, choose T in GL2(K) with Tw=x.
+Then `(MT-I)w=0`, so the columns of MT-I span at most a one-dimensional
+K-space. It is `u y^T` for some allowed u,y, hence `M=(I+u y^T)T^-1`.
+This is the one-factor criterion already implicit in #4276, applied here.
+
+For nonzero rank-one M=a b, equality Mx=w says `a(bx)` is a nonzero constant
+column. A nonzero scalar polynomial times a nonzero polynomial has the sum
+of their degrees. Consequently a is constant and bx is a nonzero constant.
+The converse is immediate. Rank one prevents cost zero since free maps are
+invertible. Zero has no nonzero constant image and cannot cost one; its
+explicit two-factor word therefore has exact cost two. Combining these
+bounds proves every case of the theorem.
+
+## Sharp example over every field
+
+Take
+
+```text
+a = (1,t)^T,       b = (t,t²+1),
+M = [[t,t²+1],[t²,t³+t]].
+```
+
+The column is primitive and nonconstant. The row gcd is 1, but no K-linear
+combination of t and t²+1 is 1, by comparing degrees two and one. Therefore
+cost M=3 over every field, while the general column lower bound delta is at
+most two. The above three factors attain it. Multiplying b by a nonzero
+nonconstant polynomial leaves the exact cost three unchanged.
+
+## Scope and credit
+
+This contribution was produced by Nick Petalas. ToikY's #4334 explicitly
+leaves singular targets outside its field-product theorem. Nick Petalas's
+#4276 supplies the exact general two-factor criterion, and #4243 supplies
+the free-map normal form, following Wentao Li's #4099 and #2513. The
+invertible polynomial results #4763 and #4784 are complementary context.
+The fixed e1,e2,e1 field-product template of #4780 is related precedent for
+the outer-product construction; its basic matrix identity is elementary.
+The new result is the complete singular K[t] classification, including the
+attaining outer-product word and the all-field sharp example. The gcd and
+rank-one factorization facts retain their classical status. Apache-2.0.
+
+This is a scoped algebraic proof. Native coefficient preparation, routing,
+precision, reversible restoration, stock and complete supplier costs remain
+unknown. No new kappa, supplier admission or complete multiplication theorem
+follows. Independent human and formal proof-kernel review are unclaimed.

research/singular-polynomial-cost/README.md

@@ -0,0 +1,116 @@
+# Exact costs for singular polynomial targets
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+Scoped algebraic proof with finite corroboration. For every field K, every
+determinant-zero target in M2(K[t]) has paid right-vector cost at most three,
+with free GL2(K) maps anywhere and no scratch roles. The exact classification
+is in [PROOF.md](PROOF.md). No new kappa or supplier admission is claimed.
+
+For nonzero M, take its primitive polynomial column factorization M=a b.
+Let V be the K-span of the two entries of b, and let d be their monic gcd.
+
+```text
+cost 1: a is constant and V contains a nonzero constant;
+cost 2: otherwise, a is constant or d belongs to V;
+cost 3: otherwise.
+zero:  cost 2.
+```
+
+An attaining three-factor word has fixed right vectors e1,e2,e1. Over every
+field, `a=(1,t)^T`, `b=(t,t²+1)` gives exact cost three. This settles singular
+polynomial endpoints at every degree. Invertible polynomial endpoints can
+have unbounded cost, as proved in #4763 and counted in #4784; those results
+are complementary, cited context.
+
+ToikY's #4334 leaves singular targets outside its field-product theorem.
+Nick Petalas's #4276 supplies the exact two-factor criterion and #4243 the
+free-map normal form, following Wentao Li's #4099 and #2513. These are
+credited dependencies, not audit deliverables. The primitive PID and gcd
+facts are classical. The e1,e2,e1 field-product template in #4780 is related
+precedent for the outer-product word. SOURCES.json pins #4334 and #4276 as
+historical provenance. No predecessor code or live input is imported.
+
+## Evidence
+
+The verifier enumerates every determinant-zero matrix with the listed entry
+degree bounds, using literal polynomial determinants. For each nonzero
+matrix it constructs its primitive factorization, compares the new formula
+against a separate constant-chart divisibility test, checks the one-factor
+constant-image condition and multiplies all three literal paid factors.
+The direct two-factor test also returns and multiplies a complete witness,
+including its free endpoint maps. Zero is tested separately.
+
+| Field | Maximum entry degree | Targets | Cost 1 | Cost 2 | Cost 3 |
+|---|---:|---:|---:|---:|---:|
+| F2 | 4 | 8704 | 279 | 7489 | 936 |
+| F3 | 2 | 6561 | 800 | 5761 | 0 |
+| F4 | 1 | 2176 | 975 | 1201 | 0 |
+| F5 | 1 | 6625 | 3024 | 3601 | 0 |
+
+These are 24066 distinct targets across four separate domains. Each row
+includes zero once in cost two. All 35 enumerated control groups pass. They
+cover the sharp example in all four fields, factor order and omission,
+constant-image and constant-column exceptions, row-content normalization,
+gcd membership, invalid fields and a zero polynomial divisor. All checks
+remain active under optimized Python. The generated stdout receipt binds
+all six package files by SHA256; no receipt is handwritten.
+
+## Reproduce
+
+From the repository root, with the Python 3.12 standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B -W error research/singular-polynomial-cost/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -O -B -W error research/singular-polynomial-cost/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/singular-polynomial-cost
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/singular-polynomial-cost --check-source-history
+```
+
+Any Python 3.12 interpreter may replace the displayed local path. The direct
+marker is `PASS_SINGULAR_POLYNOMIAL_COST targets=24066 controls=35 no_new_kappa`.
+Both registered checks must finish within 120 seconds each.
+
+The original card is explicitly changed to this algebraic side question.
+Its historical baseline command stops at an omitted sparse input,
+`research/fresh-helper-thinned/PROOF.md`; no baseline or selected scientific
+replay pass is claimed. The selected record remains 60403/20000000.
+
+## Limits and code constraints
+
+The universal result is the written proof. The finite census corroborates
+only the displayed fields and degrees. The exact classification requires
+two roles, one polynomial variable and a field of constants. No statement
+about multivariate rings, general singular coefficient algebras or more roles
+is supplied. Native coefficient preparation, access, routing, precision,
+reversible dirty restoration, stock and complete supplier costs are unknown.
+No complete multiplication theorem, selected-frontier update, independent
+human review or formal proof-kernel acceptance is claimed. Lean, Docker and
+selected operator replay are outside scope and were not run.
+
+The verifier has no recursion, subprocess, dynamic code or indirect callback
+chain. Every function is below 60 physical lines. Explicit exceptions retain
+checks under -O, and registered commands make warnings errors. Polynomial
+capacity is 33 coefficients, bounded division and gcd take at most 34
+iterations, and census inputs are fixed. The largest matrix census considers
+32^4 matrices over F2. Product caches contain at most 1024 entries; only
+accepted targets are processed further, one at a time. Field operations are
+bounded to F2,F3,F4,F5, with F4 represented modulo x²+x+1. Python and the
+standard library allocate dynamically. This is a managed-runtime deviation
+from fixed allocation, bounded by those input and live-collection capacities.
+There is no real-time claim. A future larger census must revise and verify
+the resource bounds first. Optional external Python analyzers are not
+required and were unavailable; in-memory compilation is the syntax check.
+
+## Open next questions
+
+1. Which singular targets are reachable over the nonprincipal domain
+   K[s²,st,t²]? Start with `[[s²,st],[st,t²]]`, testing its outer-product
+   factorization and restricted-right-vector reachability. The one-variable
+   primitive-factorization argument does not supply that step.
+2. Can an actual native producer and consumer use one of these words at a
+   favorable complete cost? Specify coefficient preparation, ownership,
+   overwrites, restoration, precision and the full paid list before expanding
+   the construction. Unknown costs are not zero.
+
+TASK.json records the motivation, first steps and blockers for both questions.

research/singular-polynomial-cost/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/README.md",
+      "usage": "provenance",
+      "git_blob": "fc9889d41621b596209c707b6057517744b4642f",
+      "sha256": "6222431360182204f502334d1c707eefc39a174d06578ef75c52f37b5873055f"
+    },
+    {
+      "path": "research/right-vector-two-factor-criterion/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "71888afa0db63d6d332cbbdc408abf1aa879681c",
+      "sha256": "c1065c51c839d11b0d31bccb8d39ebc07a869eb0f29899038518e3090a58c895"
+    }
+  ]
+}

research/singular-polynomial-cost/TASK.json

@@ -0,0 +1,101 @@
+{
+  "schema_version": 1,
+  "task_id": "formal-interface-lemma",
+  "priority_revision": 7,
+  "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43",
+  "original_card": {
+    "id": "formal-interface-lemma",
+    "question": "Can one uncovered interface implication be formalized with exact caller and certificate bindings?",
+    "starting_points": [
+      "docs/research/research-family-status.md",
+      "certificates/selected-result.json",
+      "research/gate-operand-parity-lean/README.md",
+      "research/staged544-certified-endpoint/README.md",
+      "research/unconditional-batched-crt/README.md"
+    ],
+    "methods": [
+      "Formalize a missing boundary lemma identified by the selected review.",
+      "Audit a formal theorem-to-certificate binding independently."
+    ],
+    "acceptance_gate": "State the exact formalized proposition and remaining assumptions; avoid duplicate arithmetic formalizations already present.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Inventory the gate-operand parity lemma (#3807) and certified endpoint arithmetic (#3857). Neither is a full multiplication proof. For #4100, audit the compact-switch statement and its hypotheses before formalizing it.",
+      "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately."
+    },
+    "first_experiment": "Write one missing statement with quantified hypotheses, actual caller and existing coverage. A compact-switch lemma is a candidate only after its mathematical contract is reviewed. Establish a bounded proof plan before a separately budgeted proof-assistant build; do not rerun large Lean jobs as orientation.",
+    "bottleneck_link": "A missing interface proof can reduce the conditional gap even if it does not change kappa.",
+    "allowed_variations": [
+      "Narrow to one formal lemma or one theorem-to-certificate binding."
+    ],
+    "scope_change_triggers": [
+      "Formalizing already-covered arithmetic and claiming the full multiplication theorem."
+    ],
+    "overlap_terms": [
+      "hyperplane end",
+      "formal interface",
+      "Lean binding",
+      "3807",
+      "3857",
+      "4100",
+      "gate-operand-parity-lean",
+      "staged544-certified-endpoint",
+      "unconditional-batched-crt"
+    ],
+    "existing_checks": [
+      {
+        "scope": "PR #3807: scoped gate-operand parity formalization.",
+        "evidence": "research/gate-operand-parity-lean/README.md",
+        "remaining": "Exact theorem-to-caller binding and genuinely uncovered interface lemmas.",
+        "status": "author-checked",
+        "source_commit": "4c3530f42a6abcc48e7a6bcffd6c901911dc8269",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "PR #3857: certified real-power moment/endpoint arithmetic.",
+        "evidence": "research/staged544-certified-endpoint/README.md",
+        "remaining": "Uniform algorithmic implications, not another endpoint digit.",
+        "status": "author-checked",
+        "source_commit": "ef4315b8caa605e47a2515004845eb2d2ed71a86",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "PR #4100: compact-switch formalization proposed as future validation.",
+        "evidence": "research/unconditional-batched-crt/README.md",
+        "remaining": "Audit the statement and assumptions before a formal proof campaign.",
+        "status": "author-checked",
+        "source_commit": "337d04939571a637aeab54a0f58f54fde811663a",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      }
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "Exact paid right-vector costs for every determinant-zero two-role target over K[t], over any field K.",
+  "scope_change_reason": "This is an algebraic side result prompted by the singular-target gap in ToikY #4334, rather than a proof-assistant binding of the selected construction.",
+  "bottleneck_link": "Side result for the restricted right-vector coefficient alphabet. It separates reachable singular polynomial endpoints from the unbounded invertible family; native coefficient preparation, access, restoration and the complete supplier bill remain unknown.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop at the first verified original classification and package it; no further construction search.",
+  "outcome": "completed",
+  "evidence": "PROOF.md gives the all-field classification; verify.py independently enumerates 24066 determinant-zero polynomial matrices, checks the one/two-factor boundaries and constructs every three-factor word. Thirty-five enumerated control groups distinguish sharp and boundary cases.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Which singular targets are reachable over K[s\u00b2,st,t\u00b2]?",
+      "why_it_matters": "A nonprincipal coefficient domain tests the primitive outer-product assumption of the one-variable proof.",
+      "first_step": "Test outer-product factorization and restricted-right-vector reachability of [[s\u00b2,st],[st,t\u00b2]] in that subring.",
+      "blocked_by": "A replacement for the one-variable primitive-factorization argument."
+    },
+    {
+      "question": "Can one native producer and consumer realize a singular polynomial factor word at a favorable complete cost?",
+      "why_it_matters": "Formal factor counts alone do not admit a recursive supplier.",
+      "first_step": "Specify coefficient preparation, data ownership, overwrites, restoration, precision and every paid transition at one actual caller.",
+      "blocked_by": "All native cost and restoration contracts remain unknown."
+    }
+  ]
+}