Classify exact cube-zero outer-product cost by quadratic relations

research/cube-zero-product-map-cost/README.md

@@ -0,0 +1,140 @@
+# Exact cost from the cube-zero product map
+
+This package answers the product-map question in Nick Petalas's PR4764. For the
+same two-role outer-product target, it classifies exactly when quadratic
+relations lower the paid right-vector cost from three to two. It also gives the
+minimum dimension of the product image needed for a cost-three witness. The
+complete kappa calculation is unchanged.
+
+## Theorem
+
+Let A=K plus J be a split commutative local algebra over a field K, with J cubed
+zero. Choose x,y whose images span a two-dimensional subspace U of J/J squared.
+Let mu: Sym squared(U) -> J squared be multiplication and let L=ker(mu).
+Identify Sym squared(U) with the three-dimensional binary quadratic forms
+on formal variables X,Y. Use paid factors I+u v^T, u in A squared and v in
+K squared, and arbitrary free GL2(K) maps. Singular paid factors are allowed.
+Put M=[[x squared,xy],[xy,y squared]]. Then
+
+```
+cost(M) = 3  if L contains no nonzero product of two K-linear forms;
+cost(M) = 2  otherwise.
+```
+
+Equivalently, cost is three exactly when L is zero or is a line generated by
+an irreducible binary quadratic. This covers every field, including
+characteristic two and inseparable irreducible quadratics. It classifies this
+outer-product family, not all matrices over a cube-zero algebra.
+
+## Proof
+
+The predecessor's three paid factors work unchanged:
+
+```
+C1 = [[x,0],[y,1]], C2 = [[1,y],[0,0]], C3 = [[x,0],[0,1]],
+C1 C2 C3 = M.
+```
+
+Each factor changes one base-field column direction. The identity uses only
+commutativity. All entries of M lie in J squared. The exact two-factor criterion
+of PR4276 says that cost is at most two exactly when some N=G M H, with G,H
+in GL2(K), satisfies N12 in N11 A. Since J cubed is zero, N11 A=K N11.
+Thus this condition is equivalent to a nonzero row phi and column v over K
+with phi M v=0. The forward direction subtracts the relevant scalar multiple
+of the first column of H from its second. The reverse direction chooses phi
+as the first row of G and v as the second column of H.
+
+For phi=(a,b) and v=(c,d), phi M v=(ax+by)(cx+dy). This is zero exactly when
+the nonzero split form (aX+bY)(cX+dY) lies in L. If such a pair exists, choose
+G,H as above; then N12=0 and the explicit two-factor construction is
+
+```
+N = [[N11,0],[N21,1]] [[1,0],[0,N22]],
+M = G^-1 N H^-1.
+```
+
+No zero- or one-factor word can equal M. Its scalar residue is the zero
+2-by-2 matrix. A free map has rank two, and the scalar residue of I+u v^T
+has rank at least one. Invertible free maps do not change that lower bound.
+This includes M=0: the zero matrix has cost two in this alphabet.
+
+It remains to classify L. If dim(L)>=2, the linear functional that takes the
+X squared coefficient has a nonzero kernel on L. A nonzero form there is
+Y(bX+cY), hence split. A one-dimensional L avoids all split forms exactly
+when its generator is irreducible. The zero space also avoids them. This
+proves the classification without a census or a field-size restriction.
+
+## Minimum product image and finite-field count
+
+The rank of mu is three minus dim(L). A cost-three witness therefore needs
+at least two product directions. Rank two suffices exactly when K has an
+irreducible quadratic. For such a form Q, the five-dimensional algebra
+K[X,Y]/((X,Y) cubed,Q) attains rank two and cost three. If K has no irreducible
+quadratic, rank three is necessary and K[X,Y]/(X,Y) cubed attains it.
+The minimum concerns this two-plane witness. It is not a minimum dimension
+for every possible right-vector obstruction or every local algebra.
+
+Over F_q, there are 1+q(q-1)/2 relation subspaces with cost three: the zero
+space and the irreducible quadratic lines. A nonzero irreducible binary
+quadratic has nonzero leading coefficient and gives one monic irreducible
+quadratic. Of the q squared monic quadratics, q(q+1)/2 are products with an
+unordered pair of roots in F_q. This gives the stated count. All other
+subspaces give cost two. The total number of subspaces of F_q cubed is
+2q squared+2q+4. Extra unused directions in J squared do not change the cost.
+
+For F2 the minimal example imposes X squared+XY+Y squared=0. Its product
+image has dimension two, and every pair of nonzero forms on U has nonzero
+product. Thus the predecessor's six-dimensional coefficient algebra is not
+minimal for this witness.
+
+## Evidence and reproduction
+
+```sh
+python3.12 -B scripts/research_package.py --package research/cube-zero-product-map-cost
+```
+
+Use Python 3.12 and the standard library. The verifier enumerates every
+quadratic relation subspace over F2,F3,F5,F7. It compares literal products of
+all projective pairs with a separate polynomial-root test, checks the full
+three-factor word, and constructs a two-factor free chart in every low-cost
+case. It applies each word to all independent quotient-basis input columns.
+Controls reject reversed order, deleted factors and a split relation mistaken
+for an irreducible one. Normal and optimized replay use explicit exceptions.
+The written proof supplies the all-field claim. No extension-field census,
+predecessor scientific replay, Lean or selected cold replay is claimed.
+
+## Sources, scope and overlap
+
+Nick Petalas's [PR #4764](https://github.com/CrocSwap/integer-mult-bounds/pull/4764)
+and its [retained proof and open question](https://github.com/CrocSwap/integer-mult-bounds/blob/32890bc5de034ab8fc93ac88ead7279a6a416d04/research/cube-zero-three-factor/README.md)
+supply the word and product-map question. His
+[PR #4276](https://github.com/CrocSwap/integer-mult-bounds/pull/4276) supplies the
+[pinned two-factor criterion](https://github.com/CrocSwap/integer-mult-bounds/blob/32890bc5de034ab8fc93ac88ead7279a6a416d04/research/right-vector-two-factor-criterion/PROOF.md).
+The higher-nilpotency and common-chart lineage retains its source credit.
+[PR #5320](https://github.com/CrocSwap/integer-mult-bounds/pull/5320) instead
+classifies quadratic lifts of a nonzero first-order pencil; this package has
+zero first-order target. Exact source objects are in SOURCES.json.
+
+The live all-state cube-zero search and current note/Discussion search found
+no same product-map classification. Unposted work and arbitrary historical
+diffs remain outside coverage. Source coefficient preparation, physical maps,
+routing, restoration, precision, stock and the whole supplier bill are unpriced.
+This result does not admit a supplier, change the selected frontier or prove
+a complete multiplication theorem.
+
+## Open next questions
+
+Find a physical realization of the five-dimensional irreducible-quotient
+algebra and price each coefficient operation in the three-factor word. Start
+with the explicit F2 relation above. Coefficient preparation and the complete
+producer/consumer cost are the blockers; fewer coefficient dimensions alone
+do not give a recursive saving. A different two-plane in a specified larger
+cube-zero algebra can be tested directly by the proved kernel criterion.
+
+## Credit
+
+Nick Petalas (@petalas) supplies the exact criterion, original witness and open
+question. Wentao Li's right-vector alphabet and ToikY's shared-chart context
+retain the attribution in those sources. Binary quadratic factorization and
+finite-field counts are classical. Ali Romman with substantial OpenAI Codex
+assistance; Apache-2.0. No independent human or proof-kernel acceptance is claimed.

research/cube-zero-product-map-cost/SOURCES.json

@@ -0,0 +1,36 @@
+{
+  "schema_version": 1,
+  "base_commit": "32890bc5de034ab8fc93ac88ead7279a6a416d04",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "fc3d4ba105e1f097d0d7d051a308281e86ab1446",
+      "sha256": "66974efdced4083c00025f97d95d83909a226cdf801edb9301c195c6641f6903"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602",
+      "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72"
+    },
+    {
+      "path": "research/cube-zero-three-factor/README.md",
+      "usage": "provenance",
+      "git_blob": "3a697077366e762de8b1b7304768e7ae8c4a1f62",
+      "sha256": "05c1e3d04630243bf2078059c6f13cce3361d0c9ed518190f5dba585d2e9d383"
+    },
+    {
+      "path": "research/right-vector-two-factor-criterion/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "71888afa0db63d6d332cbbdc408abf1aa879681c",
+      "sha256": "c1065c51c839d11b0d31bccb8d39ebc07a869eb0f29899038518e3090a58c895"
+    },
+    {
+      "path": "research/cube-zero-lift-obstruction/README.md",
+      "usage": "provenance",
+      "git_blob": "10044ad7c5bdce30e67d756805b790f8fab1f07e",
+      "sha256": "36fc090489e43f8d73355aeeb7eac717d3d3a359b3abdf22530fc51a4068da20"
+    }
+  ]
+}

research/cube-zero-product-map-cost/TASK.json

@@ -0,0 +1,95 @@
+{
+  "schema_version": 1,
+  "task_id": "formal-interface-lemma",
+  "priority_revision": 7,
+  "base_commit": "32890bc5de034ab8fc93ac88ead7279a6a416d04",
+  "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": "Classify the exact two- or three-factor cost of every cube-zero two-plane outer-product witness by its quadratic relation space.",
+  "scope_change_reason": "Take PR4764 open question 2 as an algebraic interface theorem and exact census rather than a Lean formalization.",
+  "bottleneck_link": "Determine which coefficient multiplication maps retain the right-vector separation before pricing a physical realization.",
+  "budget_minutes": 60,
+  "stop_rule": "Finish the kernel theorem, minimal image dimension and complete small-field checks; do not infer a physical cost.",
+  "outcome": "completed",
+  "evidence": "README.md proof and verify.py complete relation-space census with attaining words.",
+  "author": "Ali Romman",
+  "ai_assistance": "Substantial OpenAI Codex assistance.",
+  "open_questions": [
+    {
+      "question": "Can the five-dimensional irreducible-quotient algebra be realized and priced physically?",
+      "why_it_matters": "The formal cost separation helps only if coefficient production and use fit the complete bill.",
+      "first_step": "Realize the explicit binary quotient and price the three-factor word.",
+      "blocked_by": "No physical coefficient, routing or restoration model is supplied."
+    }
+  ]
+}

research/cube-zero-product-map-cost/VERIFY.json

@@ -0,0 +1,30 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Complete relation spaces, projective products, explicit words and all quotient-basis inputs."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-B",
+        "-O",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Complete relation spaces, projective products, explicit words and all quotient-basis inputs."
+    }
+  ]
+}