[petalas]

Summary

This contribution was produced by Nick Petalas. Claim type: scoped written proof with exact finite corroboration; no κ change.

For lee-phys's PR6210 demand (e, h, e+h+z) over F2[e,h,z]/(e,h,z)^2, the restoring count vectors (P_0,P_1,P_2; K_0,K_1,K_2) (insertions and incoming ADDs per row) have exactly 13 componentwise-minimal elements: PR6210's ten price-envelope vertices D, T_i, R_ij;k, plus three unexposed vectors V_k = ((1,1,1) - e_k; 2,2,2).

The branch PR6210 left open, one unit insertion in each of two rows, none in the third, and K = (2,2,2), is attainable. An explicit eight-gate word works over every commutative unital local ring when lambda_i, lambda_j are in m and lambda_k is nonzero:

E_ki(g), P_i(1+l_i), E_ki(-g), E_ji(l_j-1), E_ij(1), P_j(1), E_ij(-1), E_ji(1-l_j),   g = -l_k (1+l_i)^-1

V_k is never the unique cheapest at a strictly positive price (PR6210's inequality (2)), so the ten-term tariff is unchanged. It remains the minimum of the same ten terms when prices are only nonnegative. This answers Open next question 1 of PR6210, including its suggested first step.

The package is research/r16-radical-pareto-frontier/.

Evidence

verify.py is standard-library Python and imports no predecessor code.

• Ring axioms checked exhaustively in R16, F3[e,h,z]/(e,h,z)^2 and Z/4[x,y]/(x,y)^2 (where m^2 != 0).
• The word, over all independent demand triples (168, 11,232, 10,752) and every ordered row choice, plus the relaxed hypothesis: 256,704 words, each equal to the target matrix with count vector V_k.
• Literal R16 check for the requested demand: six row orders on every scalar dirty/source input, forward and inverse, 393,216 cases.
• An exhaustive first-order search (exact because m^2 = 0) over all words of at most nine gates in R16: 20,362,086 nodes, no solvable word type with a count vector outside the up-set of the 13. It attains all 13, including the three V_k independently of the explicit word, and each attained type is rebuilt as a literal word that matches the target.
• Five mutated words and two search controls are rejected; the pinned PR6210 README bytes and the five case-analysis sentences used are checked.

Reproduce from the repository root (about 47 s and 520 MB locally):

/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/r16-radical-pareto-frontier/verify.py
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/r16-radical-pareto-frontier/verify.py
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/r16-radical-pareto-frontier
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/r16-radical-pareto-frontier --check-source-history

Expected marker: PASS_R16_RADICAL_PARETO_FRONTIER frontier=13 search_gates=9.

Local results, CPython 3.12.15: the direct normal and optimized warning-strict runs pass in 33.2 s and 32.8 s (518 MB peak). The registered launcher passes both commands (PASS_REGISTERED_RESEARCH_PACKAGE, 64 s in total). --check-only metadata and pin validation and the committed-byte and source-history check pass at 824117ea0f9efe4dd43bae6aae60cd1ac4d5e2f4. Each run prints a generated receipt bound to the hashes of verify.py and VERIFY.json.

Limitations

• Completeness for words longer than nine gates and for rings other than R16 rests on PR6210's written case analysis, which is cited and not replayed or machine checked here. The search is independent finite corroboration up to nine gates in R16.
• The first-order criterion is exact only for m^2 = 0; for Z/4[x,y]/(x,y)^2 only the word identity is checked.
• Counts are aggregated by receiving row, as in PR6210. This is not a per-edge frontier or a dependent-class frontier, and the model has no auxiliary rows.
• No physical supplier, κ change, proof-kernel verification or independent human review is claimed.

Open next questions

1. Dependent demands. What is the frontier for a rank-two demand such as (e,h,e+h)? PR6210 records a cheaper word there. First step: run the search with the two specific pure-source targets. Blocker: no written lower bound for dependent classes.
2. Directed edges. What are the minimal per-edge ADD count vectors, and the tariff with independently priced directed edges (PR6210's question 2)? First step: label each ADD by its directed edge in the search. Blocker: the return lemma does not strengthen per edge.
3. Rings with m^2 != 0. Does a second-order search corroborate the cited lower bound for Z/4[x,y]/(x,y)^2? First step: add quadratic terms for words of at most seven gates. Blocker: the conditions become nonlinear.

Related open work

• Prove exact Boolean directed-cycle tariff 108 (no κ) #6663 (open): the same gate model for a Boolean demand with directed-cycle prices. It prices directed edges; this PR classifies receiving-row count vectors for R16. The two share no quantity or number.
• Prove the realizable two-plane signatures of 4x4 bases are exactly 439 (no κ) #6691, Link ten stored open questions to the merged packages that answer them (no κ) #6692, Prove seven orthogonal binary full-guard events lie below the product of their marginals (no κ) #6694, Prove no toggle alphabet beats the five-source connector DUO point (no κ) #6695 and Prove the eight-query mutable-source tariff is exactly 460 (no κ) #6696 (open, same account, created after this work was claimed) study other objects: two-plane signatures of 4x4 bases, a ledger linking stored questions, seven-event guard correlation, a five-source toggle frontier and an eight-query mutable-source tariff. None computes a number this PR also computes.

CI notes

CI passed at head 824117ea0f9efe4dd43bae6aae60cd1ac4d5e2f4 in run 41719902146: plan (5m51s) and replay (research/r16-radical-pareto-frontier) (18m11s) both succeeded. In the replay job log the two registered commands took 78.9 s (normal) and 78.8 s (optimized), and the job printed PASS_REGISTERED_RESEARCH_PACKAGE research/r16-radical-pareto-frontier outcome=completed. The checkout and setup phase before them took about 15.5 minutes (21:19:55Z to 21:35:21Z); its cause was not investigated. Nothing was re-run.