From b1b163cd5553c75c9bd5ca3ac31a2eab4e2f3511 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Thu, 22 Oct 2026 20:22:43 +0100 Subject: [PATCH] feat(research): prove a cube-zero radical target costs three --- research/cube-zero-three-factor/README.md | 150 ++++++++++++ research/cube-zero-three-factor/SOURCES.json | 30 +++ research/cube-zero-three-factor/TASK.json | 96 ++++++++ research/cube-zero-three-factor/VERIFY.json | 35 +++ research/cube-zero-three-factor/verify.py | 236 +++++++++++++++++++ 5 files changed, 547 insertions(+) create mode 100644 research/cube-zero-three-factor/README.md create mode 100644 research/cube-zero-three-factor/SOURCES.json create mode 100644 research/cube-zero-three-factor/TASK.json create mode 100644 research/cube-zero-three-factor/VERIFY.json create mode 100644 research/cube-zero-three-factor/verify.py diff --git a/research/cube-zero-three-factor/README.md b/research/cube-zero-three-factor/README.md new file mode 100644 index 0000000000..3a69707736 --- /dev/null +++ b/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. diff --git a/research/cube-zero-three-factor/SOURCES.json b/research/cube-zero-three-factor/SOURCES.json new file mode 100644 index 0000000000..9d6aeafa68 --- /dev/null +++ b/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" + } + ] +} diff --git a/research/cube-zero-three-factor/TASK.json b/research/cube-zero-three-factor/TASK.json new file mode 100644 index 0000000000..37271ba23b --- /dev/null +++ b/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" + } +} diff --git a/research/cube-zero-three-factor/VERIFY.json b/research/cube-zero-three-factor/VERIFY.json new file mode 100644 index 0000000000..019813924b --- /dev/null +++ b/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." + } + ] +} diff --git a/research/cube-zero-three-factor/verify.py b/research/cube-zero-three-factor/verify.py new file mode 100644 index 0000000000..5f4b7bc6ae --- /dev/null +++ b/research/cube-zero-three-factor/verify.py @@ -0,0 +1,236 @@ +#!/usr/bin/env python3 +"""Exact, bounded corroboration of the cube-zero cost-three target.""" + +from hashlib import sha256 +from itertools import product +import json +from pathlib import Path + + +FIELDS = (2, 3, 4, 5, 7) +MONOMIALS = ((0, 0), (1, 0), (0, 1), (2, 0), (1, 1), (0, 2)) +ZERO = (0,) * 6 + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def field_add(a, b, q): + return a ^ b if q == 4 else (a + b) % q + + +def field_mul(a, b, q): + if q != 4: + return (a * b) % q + result = 0 + for bit in range(2): + if b & (1 << bit): + result ^= a << bit + if result & 4: + result ^= 7 + return result + + +def field_neg(a, q): + return a if q == 4 else (-a) % q + + +def scale(a, scalar, q): + return tuple(field_mul(c, scalar, q) for c in a) + + +def add(a, b, q): + return tuple(field_add(c, d, q) for c, d in zip(a, b, strict=True)) + + +def multiply(a, b, q): + result = [0] * 6 + for i, (ix, iy) in enumerate(MONOMIALS): + for j, (jx, jy) in enumerate(MONOMIALS): + if ix + iy + jx + jy < 3: + k = MONOMIALS.index((ix + jx, iy + jy)) + result[k] = field_add(result[k], field_mul(a[i], b[j], q), q) + return tuple(result) + + +def basis(index): + return tuple(int(i == index) for i in range(6)) + + +def matrix_multiply(a, b, q): + return tuple(add(multiply(a[2*i], b[j], q), + multiply(a[2*i+1], b[2+j], q), q) + for i in range(2) for j in range(2)) + + +def matrix_vector(a, v, q): + return tuple(add(multiply(a[2*i], v[0], q), + multiply(a[2*i+1], v[1], q), q) for i in range(2)) + + +def paid(left, right, q): + require(q in FIELDS, "unsupported field") + require(len(left) == len(right) == 2, "two roles required") + require(all(type(c) is int and 0 <= c < q for c in right), + "right vector must lie in the base field") + return tuple(add(scale(left[i], right[j], q), + basis(0) if i == j else ZERO, q) + for i in range(2) for j in range(2)) + + +def word(q): + one, x, y = (basis(i) for i in range(3)) + minus_one = scale(one, field_neg(1, q), q) + x_minus_one = add(x, minus_one, q) + return (paid((x_minus_one, y), (1, 0), q), + paid((y, minus_one), (0, 1), q), + paid((x_minus_one, ZERO), (1, 0), q)) + + +def rank(rows, q): + work = [list(row) for row in rows] + height = 0 + for col in range(6): + pivot = next((i for i in range(height, len(work)) if work[i][col]), None) + if pivot is None: + continue + work[height], work[pivot] = work[pivot], work[height] + inverse = next(c for c in range(1, q) + if field_mul(work[height][col], c, q) == 1) + work[height] = [field_mul(c, inverse, q) for c in work[height]] + for i in range(height + 1, len(work)): + scalar = field_neg(work[i][col], q) + work[i] = [field_add(c, field_mul(scalar, d, q), q) + for c, d in zip(work[i], work[height], strict=True)] + height += 1 + return height + + +def in_right_ideal(a, b, q): + generators = tuple(multiply(a, basis(i), q) for i in range(6)) + return rank(generators, q) == rank(generators + (b,), q) + + +def bilinear(matrix, row, col, q): + result = ZERO + for i in range(2): + for j in range(2): + result = add(result, scale(matrix[2*i+j], + field_mul(row[i], col[j], q), q), q) + return result + + +def chart_check(matrix, q): + # Projective representatives remove only nonzero scalar rescalings. + lines = ((0, 1),) + tuple((1, c) for c in range(q)) + accepted = 0 + checked = 0 + for row in lines: + for first in lines: + for second in lines: + determinant = field_add(field_mul(first[0], second[1], q), + field_neg(field_mul(first[1], second[0], q), q), q) + if determinant: + a = bilinear(matrix, row, first, q) + b = bilinear(matrix, row, second, q) + accepted += in_right_ideal(a, b, q) + checked += 1 + require(checked == q * (q + 1)**2, "incomplete chart domain") + return accepted, checked + + +def check_field(q): + factors = word(q) + target = (basis(3), basis(4), basis(4), basis(5)) + actual = matrix_multiply(matrix_multiply(factors[0], factors[1], q), factors[2], q) + require(actual == target, "three-factor endpoint") + vectors = tuple(v for v in product(range(q), repeat=2) if v != (0, 0)) + for row in vectors: + for col in vectors: + require(bilinear(target, row, col, q) != ZERO, "common bilinear zero") + accepted, charts = chart_check(target, q) + require(accepted == 0, "two-factor chart accepted") + require(chart_check((basis(3), ZERO, ZERO, ZERO), q)[0] > 0, + "right-ideal test rejects the positive control") + for i in range(12): + initial = (basis(i % 6), ZERO) if i < 6 else (ZERO, basis(i % 6)) + final = initial + for factor in reversed(factors): + final = matrix_vector(factor, final, q) + require(final == matrix_vector(target, initial, q), "basis-column action") + return len(vectors)**2, charts + + +def exhaustive_binary_action(): + elements = tuple(product(range(2), repeat=6)) + target = (basis(3), basis(4), basis(4), basis(5)) + factors = word(2) + for initial in product(elements, repeat=2): + final = initial + for factor in reversed(factors): + final = matrix_vector(factor, final, 2) + require(final == matrix_vector(target, initial, 2), "arbitrary binary data") + return len(elements)**2 + + +def controls(): + factors = word(3) + target = (basis(3), basis(4), basis(4), basis(5)) + identity = (basis(0), ZERO, ZERO, basis(0)) + for omit in range(3): + result = identity + for i, factor in enumerate(factors): + if i != omit: + result = matrix_multiply(result, factor, 3) + require(result != target, "dropped factor not rejected") + result = identity + for factor in reversed(factors): + result = matrix_multiply(result, factor, 3) + require(result != target, "reversed word not rejected") + bad_middle = paid((basis(2), basis(0)), (0, 1), 3) + wrong_sign = matrix_multiply(matrix_multiply(factors[0], bad_middle, 3), factors[2], 3) + require(wrong_sign != target, "wrong-sign control") + for right, q in (((basis(1), basis(2)), 2), ((1, 0), 6)): + try: + paid((basis(1), basis(2)), right, q) + except ValueError: + continue + raise ValueError("invalid alphabet or field accepted") + # The quotient by J^2 kills the target and the bilinear obstruction. + require(all(entry[:3] == (0, 0, 0) for entry in target), "quotient control") + return 8 + + +def receipt(): + package = Path(__file__).resolve().parent + root = package.parent.parent + sources = json.loads((package / "SOURCES.json").read_text()) + hashes = {} + for entry in sources["files"]: + if entry["usage"] == "input": + digest = sha256((root / entry["path"]).read_bytes()).hexdigest() + require(digest == entry["sha256"], "source drift: " + entry["path"]) + hashes[entry["path"]] = digest + for name in ("README.md", "TASK.json", "SOURCES.json", "VERIFY.json", "verify.py"): + hashes[str(package.relative_to(root) / name)] = sha256((package / name).read_bytes()).hexdigest() + return {"schema": "cube-zero-three-factor/v1", "sha256": hashes} + + +def main(): + pairs = charts = 0 + for q in FIELDS: + pair_count, chart_count = check_field(q) + pairs += pair_count + charts += chart_count + data = exhaustive_binary_action() + rejected = controls() + print(json.dumps(receipt(), sort_keys=True)) + print(f"PASS_CUBE_ZERO_THREE_FACTOR fields={','.join(map(str, FIELDS))} " + f"bilinear_pairs={pairs} ideal_charts={charts} basis_columns=60 " + f"binary_inputs={data} controls={rejected} exact_cost=3 no_new_kappa") + + +if __name__ == "__main__": + main()