Prove a cube-zero radical target has exact cost three (no new κ)

research/cube-zero-three-factor/README.md

@@ -0,0 +1,150 @@
+# A radical target of exact right-vector cost three
+
+This contribution was produced by Nick Petalas. It answers the first
+higher-nilpotency question in
+[#4745](https://github.com/CrocSwap/integer-mult-bounds/pull/4745), pinned at
+`3edea13af13b755932852e9306a714b317630dda`, with a **scoped proof** and finite
+corroboration. A third paid factor enlarges the reachable radical set in the
+cube-zero algebra below. No new κ is claimed.
+
+For any field K, let R = K[x,y]/(x,y)³, with radical J = (x,y). Use two
+roles, paid factors I + u vᵀ with u ∈ R² and v ∈ K², and arbitrary free
+GL₂(K) maps anywhere in a word, as in Wentao Li's #4099 and Nick Petalas's
+#4243/#4276. Factors may be singular. Then
+
+```text
+M = [[x², xy], [xy, y²]] ∈ M₂(J²) has exact cost 3.
+```
+
+Every nonzero base-field row φ and column v satisfy φMv ≠ 0. Thus the
+common-zero obstruction from the square-zero ambient-algebra theorem does
+not extend to this cube-zero algebra, even for targets in its square-zero
+ideal J². The distinction is in the allowed coefficients of the factors:
+they can use J, whereas K ⊕ J² has no degree-one coefficients.
+
+## Proof and attaining word
+
+All displayed products use algebraic order; execution on column vectors is
+from right to left. The three paid factors are
+
+```text
+C₁ = [[x,0],[y,1]] = I + (x−1,y)ᵀ e₁ᵀ,
+C₂ = [[1,y],[0,0]] = I + (y,−1)ᵀ e₂ᵀ,
+C₃ = [[x,0],[0,1]] = I + (x−1,0)ᵀ e₁ᵀ.
+
+C₁ C₂ C₃ = [[x²,xy],[xy,y²]] = M.
+```
+
+There is no scratch or zero-input assumption. This matrix identity acts on
+arbitrary elements of R². It supplies the upper bound three.
+
+For the lower bound, use the exact two-factor criterion of Nick Petalas's
+[#4276](../right-vector-two-factor-criterion/PROOF.md), Theorem B. It states
+that cost(M) ≤ 2 holds exactly when some G,H ∈ GL₂(K) give N = GMH with
+N₁₂ ∈ N₁₁R. This theorem already includes arbitrary free maps and words
+with fewer paid factors. It is a cited dependency, not a result rechecked
+by this contribution.
+
+Every entry of N lies in J², and J²J = 0. Therefore N₁₁R = K N₁₁. If
+N₁₂ ∈ N₁₁R, there is a scalar c ∈ K with N₁₂ = cN₁₁. Let φ be the first
+row of G and let t,s be the first and second columns of H. Then
+
+```text
+0 = N₁₂ − cN₁₁ = φM(s−ct).
+```
+
+Both φ and s−ct are nonzero because G,H are invertible. However, for any
+nonzero row (a,b) and nonzero column (c,d) over K,
+
+```text
+(a,b) M (c,d)ᵀ = (ax+by)(cx+dy) ≠ 0 in R.
+```
+
+The two linear polynomials are nonzero. Their product is nonzero in the
+polynomial domain K[x,y], has degree two, and hence survives quotienting
+by (x,y)³. This contradiction excludes cost at most two and proves exact
+cost three over every field, including characteristic two.
+
+The subalgebra S = K ⊕ J² is split square-zero. The same target has no
+common zero there, so #4745's theorem makes it unreachable over S. That
+last comparison cites #4745; neither its proof nor its binary census is
+replayed here. The cost-three theorem above uses only the merged #4276
+criterion, and remains independently reviewable without the pending result.
+
+## Evidence and reproduction
+
+Run from the repository root with CPython 3.12 and the standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B -W error research/cube-zero-three-factor/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -O -B -W error research/cube-zero-three-factor/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/cube-zero-three-factor
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/cube-zero-three-factor --check-source-history
+```
+
+Another CPython 3.12 interpreter may replace the absolute local path. The
+verifier writes nothing. It emits a generated SHA-256 receipt binding all
+five package files and both declared source inputs, followed by
+`PASS_CUBE_ZERO_THREE_FACTOR`. The finite fields are F₂,F₃,F₄,F₅,F₇;
+F₄ uses the polynomial t²+t+1. Direct ring multiplication checks the word.
+An independent six-dimensional right-ideal rank test rejects every
+projective two-factor chart. The checker also evaluates every nonzero
+row/column pair, all 12 basis columns of the data action over each field,
+and every binary R² input. Positive ideal-membership controls, three
+dropped factors, reversed order, an odd-characteristic sign error, illegal
+right coefficients, a nonfield parameter and the degree-one quotient are
+checked. These checks corroborate the written proof, rather than proving
+its all-field quantifier in a proof kernel.
+
+The original card's positive control was run first and reported
+`PASS_UNIVERSAL_CONNECTOR_BOUNDARY pairings=945 max_coverage=31 queries=74 leaves=182`.
+It is orientation, with no new claim about that connector.
+
+## Limits and implementation decisions
+
+This is one target family in a formal alphabet, not a classification of
+all singular targets over R. Native coefficient preparation, conversion,
+routing, restoration, precision, stock and the complete supplier bill
+are unknown. There is no supplier admission or complete multiplication
+theorem. Independent human and formal proof-kernel review are unclaimed.
+No Lean, Docker or selected-construction replay was run.
+
+The checker fixes the five field orders, six monomials, two roles, at most
+448 charts per field and 4,096 binary inputs. Every loop has a fixed finite
+domain, no recursion or subprocess is used, and all functions are under
+60 physical lines. Meaningful checks remain active under optimized Python.
+Power-of-ten rule 3 has a bounded managed-runtime deviation: tuples,
+lists and field integers allocate during this offline calculation. The
+largest stored domain has 64 ring elements, each with six coefficients;
+the chart and input products are streamed. There is no service steady
+state or persistent resource. Source manifests and package files are
+small trusted local inputs. Warning-strict ordinary and optimized replay
+provide the available diagnostics; no separate static analyzer is part
+of the standard-library environment.
+
+## Open next questions
+
+1. Is every reachable radical target over K[x,y]/(x,y)³ attainable with
+   three factors? Start with a three-factor normal form. The present
+   example gives an exact lower bound, but no classification or global
+   upper bound.
+2. Which bilinear product maps J/J² × J/J² → J² admit such a cost-three
+   target in a general cube-zero local algebra? Start with two independent
+   degree-one elements and determine whether every product of their
+   nonzero scalar linear combinations survives. Relations may destroy
+   the lower-bound witness.
+
+These follow-ups are not investigated here. TASK.json records the questions,
+first steps and blockers.
+
+## Credit and source boundary
+
+Produced by Nick Petalas. Nick Petalas's #4745 supplies the explicit
+higher-nilpotency question and the square-zero comparison; #4276 supplies
+the exact two-factor ideal criterion; #4243 supplies the common free-map
+convention. ToikY's #4334 develops the shared-chart algebra interface.
+Wentao Li's #4099 supplies the right-vector alphabet, following #2513.
+The new contribution is this all-field cost-three radical target and its
+degree-two lower bound. SOURCES.json pins the unchanged merged dependencies
+at canonical main. Pending #4745 is an exact-head citation, with no runtime
+or Git-history dependency. Apache-2.0.

research/cube-zero-three-factor/SOURCES.json

@@ -0,0 +1,30 @@
+{
+  "schema_version": 1,
+  "base_commit": "b58ad9ef4d4e861b0eaa5dba41742bdc072dca51",
+  "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-diagonal-free-basis/README.md",
+      "usage": "input",
+      "git_blob": "50a1cbeea57e3cb16e0d8a569be365bba21890ff",
+      "sha256": "924334cf4e881775fafc6ec36630d03648dbda39f6bad4612a97b5b6d351fbcb"
+    },
+    {
+      "path": "research/right-vector-two-factor-criterion/PROOF.md",
+      "usage": "input",
+      "git_blob": "71888afa0db63d6d332cbbdc408abf1aa879681c",
+      "sha256": "c1065c51c839d11b0d31bccb8d39ebc07a869eb0f29899038518e3090a58c895"
+    }
+  ]
+}

research/cube-zero-three-factor/TASK.json

@@ -0,0 +1,96 @@
+{
+  "schema_version": 1,
+  "task_id": "connector-alphabet-change",
+  "priority_revision": 7,
+  "base_commit": "b58ad9ef4d4e861b0eaa5dba41742bdc072dca51",
+  "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": "Prove exact cost three for [[x^2,xy],[xy,y^2]] over K[x,y]/(x,y)^3 for every field K.",
+  "scope_change_reason": "Answer the explicit higher-nilpotency question of PR4745. This is a formal-alphabet side result rather than a new native connector operation.",
+  "bottleneck_link": "Shows that access to degree-one radical coefficients enlarges the reachable singular interface even for degree-two targets. All native and supplier costs remain unknown.",
+  "budget_minutes": 60,
+  "stop_rule": "Ship the first verified exact cost-three target; do not classify all singular targets or extend the algebra family.",
+  "outcome": "completed",
+  "evidence": "Written all-field proof using the cited two-factor ideal criterion, a literal three-factor word, and bounded finite-field ideal and data-action checks.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Is every reachable radical target over K[x,y]/(x,y)^3 attainable with three factors?",
+      "why_it_matters": "Would classify the possible extra word length after the square-zero case.",
+      "first_step": "Derive a three-factor normal form from the two-factor ideal criterion.",
+      "blocked_by": "The present attaining word is target-specific and gives no general upper bound."
+    },
+    {
+      "question": "Which cube-zero local-algebra multiplication maps admit the same cost-three separation?",
+      "why_it_matters": "Distinguishes a general radical-layer effect from this polynomial example.",
+      "first_step": "Test whether products of all nonzero linear combinations of two degree-one elements survive in J squared.",
+      "blocked_by": "Degree-two relations may destroy the no-common-zero lower bound."
+    }
+  ],
+  "predecessor_prs": [
+    {
+      "number": 4745,
+      "head": "3edea13af13b755932852e9306a714b317630dda",
+      "use": "Question and square-zero comparison only; exact-head citation with no runtime input."
+    },
+    {
+      "number": 4276,
+      "use": "Merged Theorem B, exact two-factor ideal criterion."
+    }
+  ],
+  "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19131122",
+  "upstream_refresh": {
+    "commit": "1f87c3578ae546c8f903f7f4d83dc2e2fb99650b",
+    "priority_revision": 7,
+    "status": "Guidance, selected record and both mathematical sources unchanged from base; retain the original research baseline without rewriting history."
+  },
+  "overlap": {
+    "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19131122",
+    "helper_open_prs": 521,
+    "helper_discussion_records": 3677,
+    "helper_complete_remote_pagination": true,
+    "local_notes_searched": 42,
+    "local_head_note_inventory": 5860,
+    "limitation": "Sparse local notes; main README term searches and targeted merged searches supplement the helper. Arbitrary diffs and unpublished work are not exhaustive.",
+    "scope_separation": "PR4745 supplies square-zero theorem; PR4749 and PR4601/4613 concern invertible targets. Concurrent square-zero all-field counting is separately claimed.",
+    "baseline_control": "PASS_UNIVERSAL_CONNECTOR_BOUNDARY pairings=945 max_coverage=31 queries=74 leaves=182"
+  }
+}

research/cube-zero-three-factor/VERIFY.json

@@ -0,0 +1,35 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/right-vector-diagonal-free-basis/README.md",
+    "research/right-vector-two-factor-criterion/PROOF.md"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "-W",
+        "error",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Literal three-factor word, independent right-ideal charts, no-common-zero pairs, arbitrary data action and rejecting controls."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-O",
+        "-B",
+        "-W",
+        "error",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Literal three-factor word, independent right-ideal charts, no-common-zero pairs, arbitrary data action and rejecting controls."
+    }
+  ]
+}