diff --git a/research/cube-zero-lift-obstruction/README.md b/research/cube-zero-lift-obstruction/README.md new file mode 100644 index 0000000000..10044ad7c5 --- /dev/null +++ b/research/cube-zero-lift-obstruction/README.md @@ -0,0 +1,71 @@ +# Exact reachability of quadratic lifts of a split radical pencil + +This scoped proof classifies every quadratic lift of one split two-role radical pencil over R=F_2[x,y]/(x,y)^3. It follows the cube-zero reachability question in Nick Petalas's [PR #4764](https://github.com/CrocSwap/integer-mult-bounds/pull/4764), while keeping its pure-quadratic cost-three target separate. No new kappa is claimed. + +Let J=(x,y), l=x+y, and let Q=(q_ij) be any matrix with entries in J^2. Use the paid factors I+u v^T, with u in R^2 and v in F_2^2, and arbitrary free GL_2(F_2) maps. A word acts on all R^2 inputs. There are no additional roles. Put + +```text +M_Q = [[x,y],[y,x]] + Q, +omega(Q) = q_11+q_12+q_21+q_22, +L = l J = span_F2{x^2+xy, xy+y^2}. +``` + +**The exact answer is cost(M_Q)=2 if omega(Q) is in L, and cost(M_Q)=infinity otherwise.** This is an all-word theorem in the stated alphabet, not a bounded search failure. Of the 4,096 lifts, exactly 2,048 have cost two and 2,048 are unreachable. Every lift has the same reachable image modulo J^2, so reachability in that quotient is not sufficient for reachability in R. + +Only 512 lifts have an exact common nonzero base-field row/column pair phi M_Q v=0. A further 1,536 lifts are reachable with two factors despite having no such pair. Thus simply copying the square-zero common-zero criterion to this larger algebra also fails. For explicit examples, put all q_ij=0 except q_22. The choice q_22=x^2 is unreachable. The choice q_22=x^2+xy has cost two but no exact common base-field zero. + +**Two-factor construction.** Let G=H=[[1,1],[0,1]], both in GL_2(F_2). They are their own inverses. Then N=G M_Q H has entries + +```text +a=N_11=l+q_11+q_21, N_12=omega(Q), +c=N_21=y+q_21, d0=N_22=l+q_21+q_22. +``` + +If omega is in L, choose b in {0,x,y,x+y} with l b=omega. Since J^3=0, a b=l b. Therefore + +```text +[[a,0],[c,1]] [[1,b],[0,d0-cb]] = N. +``` + +The two factors are I+(a-1,c)^T e_1^T and I+(b,d0-cb-1)^T e_2^T. The free maps G and H recover M_Q. Its scalar residue is zero, while one paid factor has residue rank at least one, even after free maps. Thus the cost is exactly two. + +**All-word lower bound.** Every target in this family has determinant l^2=x^2+y^2, which is a nonzero element of J^2. Quadratic corrections cannot change it because J^3=0. Call a paid factor singular when its determinant is in J. An invertible paid factor has an invertible scalar residue. A singular paid factor has scalar rank exactly one: it fixes the nonzero kernel of its base-field right row and cannot have rank zero. The zero scalar residue of M_Q therefore requires at least two singular factors. Three singular factors would put the determinant in J^3=0. Thus any realizing word contains exactly two singular factors. + +Each singular paid factor is equivalent, by invertible matrices over R, to diag(a,1), where a is its determinant in J. To see this, change its nonzero base-field right row to e_1^T by a constant conjugation. The factor then has form [[a,0],[c,1]]. Right multiplication by [[1,0],[-c,1]] gives diag(a,1). Collect all intervening invertible matrices. Every hypothetical realization must have + +```text +M_Q = U diag(a,1) V diag(b,1) W, +U,V,W in GL_2(R), a,b in J. +``` + +This is a relaxation for the lower bound; the construction above uses only the stated free GL_2(F_2) maps. Every unit in R is 1+j with j in J. Since ab is in J^2, multiplication by any such unit leaves ab unchanged. Taking determinants gives ab=l^2. Hence the upper-left entry of U^(-1) M_Q W^(-1) is ab V_11, which belongs to L. + +Let r be the first row of U^(-1) and c the first column of W^(-1). Their scalar residues r_0,c_0 are nonzero. Because r M_Q c has no linear part, r_0 [[x,y],[y,x]] c_0=0. Over F_2 the only such nonzero pair is r_0=c_0=(1,1): the two coefficient matrices are I and the coordinate swap, whose unique common projective eigenline is span(1,1). This can also be checked directly on the three nonzero rows and columns. + +Write r=(1,1)+r_1 and c=(1,1)^T+c_1, with r_1,c_1 in J in each component. Terms involving Q and one of these radical corrections, or involving two corrections and the linear pencil, vanish in J^3. Since the pencil sends (1,1)^T to (l,l)^T and (1,1) sends it to (l,l), + +```text +r M_Q c = omega(Q) + l*(r_1,1+r_1,2+c_1,1+c_1,2). +``` + +Consequently its class in J^2/L is the class of omega(Q). But the normal-form corner above belongs to L. Thus omega(Q) must belong to L for every realizing word. Together with the two-factor construction, this proves the exact classification. + +**Counts and the two lifting boundaries.** The four entries of Q have 12 independent binary coefficients. Membership of omega in L is one nonzero linear parity condition, because a quadratic A x^2+B xy+C y^2 belongs to L exactly when A+B+C=0. Hence exactly 2^11 lifts are reachable. An exact common base-field zero must use the unique first-order pair (1,1),(1,1), and its response is omega. The condition omega=0 imposes three independent linear equations, leaving 2^9=512 lifts. This proves both reported counts without extrapolation. + +**Evidence.** The standard-library checker constructs the 64-element ring from its monomial table. For all 4,096 lifts it checks the fixed determinant, computes the exact two-factor criterion across all 18 projective row/basis choices using literal principal-ideal sets, and replays each of the 2,048 stated constructions as a matrix identity. It checks the obstruction class for all 256 linear row/column corrections on every lift: 1,048,576 covariance checks. Quadratic row/column corrections vanish from this calculation by J^3=0. It separately checks all 1,024 pairs of nonunit determinants, including the 64 pairs with the required product, and verifies the normal-form corner class for every ring scalar. Controls distinguish the two explicit lifts, exact common-zero counts, square-zero versus cube-zero multiplication, and the nonzero determinant premise. Normal and optimized warning-strict CPython 3.12.14 runs pass. These finite computations corroborate the written all-word proof. + +Credit Nick Petalas's [PR #4764](https://github.com/CrocSwap/integer-mult-bounds/pull/4764) and [pinned cube-zero proof](https://github.com/CrocSwap/integer-mult-bounds/blob/ff3cc58e370d0f678e529246f8c73e8094e18fcf/research/cube-zero-three-factor/README.md) for the higher-nilpotency question and separate cost-three example. His [PR #4276](https://github.com/CrocSwap/integer-mult-bounds/pull/4276) and [pinned exact two-factor criterion](https://github.com/CrocSwap/integer-mult-bounds/blob/ff3cc58e370d0f678e529246f8c73e8094e18fcf/research/right-vector-two-factor-criterion/README.md) supply the finite criterion used for corroboration. His [PR #4776](https://github.com/CrocSwap/integer-mult-bounds/pull/4776) and [pinned pencil proof](https://github.com/CrocSwap/integer-mult-bounds/blob/ff3cc58e370d0f678e529246f8c73e8094e18fcf/research/split-radical-pencil/README.md) supply the square-zero split-pencil result and determinant lineage. The [square-zero theorem, PR #4745](https://github.com/CrocSwap/integer-mult-bounds/pull/4745), applies only under its original algebra hypothesis. Wentao Li's [PR #4099](https://github.com/CrocSwap/integer-mult-bounds/pull/4099) supplies the right-vector alphabet, and ToikY's [PR #4334](https://github.com/CrocSwap/integer-mult-bounds/pull/4334) supplies the common-chart context. Classical determinant and local-ring arguments retain their credit. + +**Limits.** This classifies one binary first-order pencil with all its quadratic lifts. It does not classify arbitrary cube-zero targets, additional roles or other coefficient fields. In particular the predecessor's pure-quadratic target has determinant zero and can use three singular factors; the nonzero-determinant argument here does not apply to it. No predecessor executable or scientific census is imported or replayed. Native coefficient preparation, routing, restoration, precision, stock and the complete supplier/outer bill remain unknown. No selected cold replay, native build, Lean or Docker run was used. No independent human or proof-kernel acceptance is claimed. Base: canonical main ff3cc58e370d0f678e529246f8c73e8094e18fcf, priority revision 7. Prepared by Ali Romman with substantial OpenAI Codex assistance; Apache-2.0. + +## Reproduce + +```sh +python3 -B scripts/research_package.py --package research/cube-zero-lift-obstruction +``` + +Use Python 3.12 with the standard library. The normal and optimized commands must print `PASS_CUBE_ZERO_LIFT_OBSTRUCTION`. The launcher must print `PASS_REGISTERED_RESEARCH_PACKAGE`. The checker has no external runtime inputs. + +## Open next questions + +Classify another first-order pencil or the determinant-zero cube-zero stratum before proposing a general reachability theorem. The source binding and physical cost model are not supplied by this package. See `TASK.json` for the structured scope. diff --git a/research/cube-zero-lift-obstruction/SOURCES.json b/research/cube-zero-lift-obstruction/SOURCES.json new file mode 100644 index 0000000000..277ad46954 --- /dev/null +++ b/research/cube-zero-lift-obstruction/SOURCES.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "base_commit": "ff3cc58e370d0f678e529246f8c73e8094e18fcf", + "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" + } + ] +} diff --git a/research/cube-zero-lift-obstruction/TASK.json b/research/cube-zero-lift-obstruction/TASK.json new file mode 100644 index 0000000000..93d40c0340 --- /dev/null +++ b/research/cube-zero-lift-obstruction/TASK.json @@ -0,0 +1,101 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 7, + "base_commit": "ff3cc58e370d0f678e529246f8c73e8094e18fcf", + "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": "This scoped proof classifies all 4,096 quadratic lifts of [[x,y],[y,x]] over F2[x,y]/(x,y)^3 in the two-role right-vector alphabet. A second-order residue class gives exact cost two for 2,048 lifts and excludes the other 2,048 at every word length. It gives both a failure of quotient lifting and reachable targets without an exact common base-field zero.", + "scope_change_reason": "This is a scoped interface theorem. It does not complete the original supplier or uniform-transfer task.", + "bottleneck_link": "Classify another first-order pencil or the determinant-zero cube-zero stratum before proposing a general reachability theorem.", + "budget_minutes": 60, + "stop_rule": "Stop after the scoped proof, exact controls and bounded registered replay; do not expand to physical lowering.", + "outcome": "completed", + "evidence": "all 4,096 lifts, 2,048 literal constructions, 1,048,576 covariance checks and all 1,024 nonunit determinant pairs", + "author": "Ali Romman", + "ai_assistance": "Substantial OpenAI Codex assistance; no independent human or proof-kernel acceptance is claimed.", + "open_questions": [ + { + "question": "Classify another first-order pencil or the determinant-zero cube-zero stratum before proposing a general reachability theorem.", + "why_it_matters": "The abstract result needs an actual caller and a complete cost model.", + "first_step": "Classify another first-order pencil or the determinant-zero cube-zero stratum before proposing a general reachability theorem.", + "blocked_by": "No production caller or physical cost model is supplied." + } + ], + "upstream_checkpoint": { + "commit": "ff3cc58e370d0f678e529246f8c73e8094e18fcf", + "priority_revision": 7, + "checked_at": "2026-10-23T17:14:15.965471+00:00" + }, + "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19150613" +} diff --git a/research/cube-zero-lift-obstruction/VERIFY.json b/research/cube-zero-lift-obstruction/VERIFY.json new file mode 100644 index 0000000000..6daf9dca37 --- /dev/null +++ b/research/cube-zero-lift-obstruction/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "all 4,096 lifts, 2,048 literal constructions, 1,048,576 covariance checks and all 1,024 nonunit determinant pairs" + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "all 4,096 lifts, 2,048 literal constructions, 1,048,576 covariance checks and all 1,024 nonunit determinant pairs" + } + ] +} diff --git a/research/cube-zero-lift-obstruction/verify.py b/research/cube-zero-lift-obstruction/verify.py new file mode 100644 index 0000000000..3935334642 --- /dev/null +++ b/research/cube-zero-lift-obstruction/verify.py @@ -0,0 +1,94 @@ +"""Cube-zero pencil lifts. Ali Romman with OpenAI Codex assistance. Apache-2.0.""" +from itertools import product +import json + +MONOMIALS = ((0, 0), (1, 0), (0, 1), (2, 0), (1, 1), (0, 2)) +X, Y, L = 2, 4, 6 + + +def require(ok, message): + if not ok: + raise ValueError(message) + + +def ring_table(): + lookup = {a: i for i, a in enumerate(MONOMIALS)} + table = [[0]*64 for _ in range(64)] + for a, b in product(range(64), repeat=2): + for i, (ix, iy) in enumerate(MONOMIALS): + for j, (jx, jy) in enumerate(MONOMIALS): + if (a >> i) & (b >> j) & 1 and ix+iy+jx+jy <= 2: + table[a][b] ^= 1 << lookup[(ix+jx, iy+jy)] + return table + + +def mm(a, b, t): + return (t[a[0]][b[0]] ^ t[a[1]][b[2]], + t[a[0]][b[1]] ^ t[a[1]][b[3]], + t[a[2]][b[0]] ^ t[a[3]][b[2]], + t[a[2]][b[1]] ^ t[a[3]][b[3]]) + + +def response(row, matrix, col, t): + a = t[row[0]][matrix[0]] ^ t[row[1]][matrix[2]] + b = t[row[0]][matrix[1]] ^ t[row[1]][matrix[3]] + return t[a][col[0]] ^ t[b][col[1]] + + +def parity(q): + return ((q >> 3).bit_count() & 1) + + +def main(): + t = ring_table() + radical = range(0, 64, 2) + quadratics = range(0, 64, 8) + ideal = {t[L][a] for a in radical} + require(ideal == {0, 24, 40, 48}, 'quadratic ideal') + rows = ((1, 0), (0, 1), (1, 1)) + bases = [(a, b) for a, b in product(rows, repeat=2) if a != b] + ideals = [{t[a][b] for b in range(64)} for a in range(64)] + g = (1, 1, 0, 1) + counts = [0, 0]; zero_charts = constructions = covariance = 0 + for q in product(quadratics, repeat=4): + m = (X ^ q[0], Y ^ q[1], Y ^ q[2], X ^ q[3]) + omega = q[0] ^ q[1] ^ q[2] ^ q[3] + good = omega in ideal + require(t[m[0]][m[3]] ^ t[m[1]][m[2]] == 40, 'fixed nonzero determinant') + criterion = any(response(row, m, v, t) in ideals[response(row, m, w, t)] + for row in rows for w, v in bases) + require(criterion == good, 'literal two-factor chart criterion') + require(good == (parity(omega) == 0), 'parity expression') + counts[not good] += 1 + exact_zero = sum(response(row, m, col, t) == 0 for row, col in product(rows, repeat=2)) + zero_charts += exact_zero + require(exact_zero == int(omega == 0), 'unique common base-field zero') + if good: + n = mm(mm(g, m, t), g, t) + b = next(b for b in (0, X, Y, L) if t[L][b] == omega) + c1 = (n[0], 0, n[2], 1) + c2 = (1, b, 0, n[3] ^ t[n[2]][b]) + require(mm(mm(mm(g, c1, t), c2, t), g, t) == m, 'literal two-factor word') + constructions += 1 + for a, b, c, d in product((0, X, Y, L), repeat=4): + lifted = response((1 ^ a, 1 ^ b), m, (1 ^ c, 1 ^ d), t) + require((lifted ^ omega) in ideal, 'second-order class under lifted rows and columns') + covariance += 1 + determinant_pairs = [(a, b) for a, b in product(radical, repeat=2) if t[a][b] == 40] + require(len(determinant_pairs) == 64, 'all nonunit determinant pairs') + for a, b in determinant_pairs: + require(a & 6 == b & 6 == L, 'forced linear determinants') + require(all(t[t[a][b]][c] in ideal for c in range(64)), 'normal-form corner class') + require(counts == [2048, 2048] and zero_charts == 512, 'lift census') + require(8 not in ideal and 24 in ideal, 'opposite lifting controls') + require(t[t[X][X]][X] == 0 and t[X][X] != 0, 'cube-zero versus square-zero') + require(t[L][L] == 40 != 0, 'nonzero determinant premise') + print(json.dumps(dict(status='PASS_CUBE_ZERO_LIFT_OBSTRUCTION', lifts=sum(counts), + cost_two=counts[0], unreachable=counts[1], exact_zero_chart_targets=zero_charts, + literal_constructions=constructions, covariance_checks=covariance, + nonunit_determinant_pairs_checked=1024, feasible_determinant_pairs=len(determinant_pairs), + no_new_kappa=True), sort_keys=True)) + + +if __name__ == '__main__': + main()