[petalas]

Summary

Scoped written proof: every quadratic lift of diag(x,y) over K[x,y]/(x,y)^3 has exact paid right-vector cost two or three, over every field K. This answers the distinct-factor pencil instance left open by Ali Romman's #5320. The endpoint uses exactly two roles, arbitrary inputs, common base-field right vectors and arbitrary free GL2(K) maps.

gamma = coefficient of y^2 in Q12
delta = coefficient of x^2 in Q21
cost(diag(x,y)+Q) = 2 if gamma*delta=0, otherwise 3

The new step is the complete coefficient classification and attaining words for this pencil. A radical shear followed by two column replacements proves the upper bound. Nick Petalas's #4276 exact two-factor criterion supplies the cited lower-bound interface. Over F_q the counts are (2q-1)q^10 cost-two lifts and (q-1)^2 q^10 cost-three lifts. No new kappa, supplier admission or selected-frontier change.

This contribution was produced by Nick Petalas. Credit Ali Romman #5320 for the next-pencil question and distinct repeated-factor result; Nick Petalas #4276/#4764 for the criterion and earlier separate cube-zero example; Wentao Li #4099 following #2513 for the alphabet; and ToikY #4334 for the common-chart context. Predecessor sources and credit remain unchanged. No predecessor scientific verifier was imported, replayed or audited.

Evidence

Before, #5320 classified a different binary repeated-factor pencil and left another pencil open. After, PROOF.md gives the all-field classification for diag(x,y), and the standalone checker enumerates every one of its 4,096 binary quadratic lifts. The results are exactly 3,072 cost-two and 1,024 cost-three lifts.

Local warning-strict normal and optimized replays pass on CPython 3.12.15, standard library only. Each command took 0.33 seconds when timed separately. The checker applies the cited principal-ideal criterion to each new target, searching common free endpoint pairs until a witness or exhaustive rejection, replays every attaining word, and checks 49,152 basis-input actions. It also checks 34/74/122 distinct construction samples over F3/F5/F7 and eight rejecting controls. All checks remain active under optimization. Its stdout receipt is generated and bound to all six package files by SHA256.

Exact reproduction from the worktree root:

/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -B -W error research/distinct-pencil-quadratic-lifts/verify.py
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -B -W error research/distinct-pencil-quadratic-lifts/verify.py
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/distinct-pencil-quadratic-lifts
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/distinct-pencil-quadratic-lifts --check-source-history --check-modes

Another CPython 3.12 path may replace the local interpreter. Expected markers are PASS_DISTINCT_PENCIL_QUADRATIC_LIFTS, PASS_REGISTERED_RESEARCH_PACKAGE and PASS_RESEARCH_COMMIT_BYTES. Local metadata, source pins, committed bytes, modes and source-history checks pass at e35e8bb95491e6bb64b8a7dc7f227360f760f74f. The current source-binding positive control also passed with PASS_RESEARCH_BASELINE_BINDINGS_ONLY; that is metadata orientation, not a selected scientific replay.

Limitations and unrun obligations

The universal statement is the written scoped proof. Enumeration is exhaustive only over the binary lifts; odd-field examples are samples, and no extension-field census was run. The exact two-factor criterion is a credited premise. Other first-order pencils, additional roles and general cube-zero reachability remain outside scope.

Native coefficient preparation, movement, restoration, precision, stock, a physical caller and a complete recursive invoice are unknown and unrun. No native/compiler application replay, Lean, Docker or selected scientific cold replay was run. Independent human and formal proof-kernel review are unclaimed. The formal-interface-lemma card is explicitly changed to this algebraic side question, without claiming its original formalization acceptance gate.

Open next questions

• Classify lifts of the rank-one first-order pencil diag(x,0), beginning with a three-factor normal form and its second-order terms. The present lower bound uses two independent diagonal linear forms.
• Bind an attaining three-factor word to an actual native producer and consumer, pricing the radical shear, overwritten inputs and restoration. Coefficient availability and a complete physical invoice remain the blockers.

Related open work

No open PR studying this diagonal quadratic-lift pencil was identified in the checked open titles and bodies. The predecessor #5320 and the separate pure-quadratic product-map package #5454 are merged; they concern different first-order endpoints. Their reported counts are cited context, not recomputed or compared as new evidence here.

The overlap refresh checked canonical main, targeted merged PR searches, the cached fully paginated open title/body corpus, refreshed recent open metadata, recent handoff claims and local reservations. Sparse local-note coverage, arbitrary historical diffs and unpublished work remain limitations. Advance CLAIM. The delivered scope matches it.

The completion refresh listed this account's nine other open PRs created since the CLAIM: #7178, #7179, #7180, #7181, #7183, #7184, #7185, #7186 and #7187. Their titles and relevant body text concern multiplicative shells, A2 tariffs, Gaussian inverse norms, Clifford response sectors, directed radical delivery, rational headers, block signatures and residue samplers. None studies this diagonal cube-zero lift classification or computes a competing target-cost count. No extra scientific computations were run to check those contributions.

• #7183 is the nearest algebraic context: a preserved-source demand on three dirty rows over a square-zero coefficient algebra with directed ADD/insertion prices. This package instead classifies two-role endpoints over a cube-zero algebra in the unrestricted-left-vector alphabet. The endpoint, nilpotency and charged operations differ; no numerical result is shared.

CI notes

At exact head e35e8bb95491e6bb64b8a7dc7f227360f760f74f, run 42992720936, plan job 130429239891, failed in Onboarding helper tests on exactly one of 760 tests, with 24 skipped:

test_research_current_status.CurrentCiNavigationTests.test_current_ci_section_matches_selected_record
AssertionError: '`make frontier7000-verify`' not found
FAILED (failures=1, skipped=24)

I confirmed the cause from the job log and the immutable main files at e54523517d0f03e58352e647c403a5af3e525a57: certificates/selected-result.json names make frontier7000-verify, while the current section of docs/ci-verification.md still describes #6030 and make frontier6030-verify. This PR changes neither file.

The same sole failing test, missing command, 760-test total, one failure and 24 skips were confirmed from the failed-step logs of all five comparison runs:

• Other contributors: 42905094314 and 42903313790.
• Prove sharp multiplicative-shell growth for every rank alphabet (no κ) #7178: 42992088329.
• Prove five A2 targets need five rank-three calls (no κ) #7179: 42992340683.
• Prove the sharp half-shift Gaussian inverse lower envelope (no κ) #7180: 42992579989.

CI did not certify this package. Its replay job was skipped because plan failed. Local registered normal/optimized, metadata and publication checks remain the available automated package evidence. The completed checks were read once. No repair, new commit, push, retrigger or job rerun was made; maintainers will address the repository-level mismatch.

Merge danger

Two-way door. Blast radius: isolated. Only six files in research/distinct-pencil-quadratic-lifts/ are added; shared code and the selected frontier are unchanged.