[petalas]

Result

For lee-phys's #5514 demand (1,2,4) over F2^3, the aggregate count vectors (P_0,P_1,P_2; K_0,K_1,K_2) (insertions, incoming ADDs) have exactly 31 Pareto-minimal elements: the 25 vectors exposed by #5514's price envelope plus six new unexposed vectors

P = e_i,   K = (2,2,2) + e_i + e_h,   h != i.

A one-insertion word may put its two extra ADDs in the insertion row and any other row, but never in both non-insertion rows: K = (2,2,2) + e_j + e_k with i ∉ {j,k} is impossible. This answers #5514 Open next question 1, including its suggested (3,3,2) first step.

Example (insertion row 0, extra ADD in row 2, l_r = lambda_r):

E_02(l1+l2), E_20(l1+l2), E_01(l1), E_10(l1), P_0(g),
E_10(l1), E_20(l1+l2), E_02(l1+l2), E_21(l1)

Each new vector costs the average of U_(i,i) and U_(i,h), so it never uniquely minimizes a price, which is why the envelope cannot expose it.

Claim type: exact finite certificate for the one-insertion layer over F2^3, combined with #5514's written componentwise multi-insertion bounds (cited, not replayed). The six new words are proved for every Boolean ring with a nonzero orthogonal demand triple via the universal ring F2^4. No new κ, physical supplier or selected-frontier change.

This contribution was produced by Nick Petalas.

Evidence

• All ADD-only words with at most four nonzero gates over F2^3 (1, 42, 1111, 18472, 202192 distinct matrices for exactly 0–4 gates). No word with at most three gates splits g e_i, so each side of the insertion has exactly four gates when sum K = 8.
• For each root, 104 four-gate suffix matrices; pairing count vectors of the same matrix gives exactly the five totals (2,2,2)+2e_h and (2,2,2)+e_i+e_h. Root 0 classes: 56 doubled only in row 0, 20 only in row 1, 20 only in row 2, 4 each in {0,1} and {0,2}; none in {1,2}.
• Six new words replayed with a separate interpreter on formal columns over F2^3 and F2^4, with reversed inverses, plus 24,576 literal width-one inputs. 17 mutation controls rejected.
• Nine-or-more-ADD one-insertion vectors shown dominated; the 31 vectors checked pairwise non-dominating.

Reproduce from the branch root (about one second each):

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

Local results at b6d49298b6ca5f40c47532866ae45dc16b8416ca: both verifier modes print PASS_FANOUT_ONE_INSERTION_PARETO (≈1.05 s each); the registered runner prints PASS_REGISTERED_RESEARCH_PACKAGE; the source-history check prints PASS_RESEARCH_COMMIT_BYTES.

Limitations

• The exclusion of non-root extra ADDs is certified over F2^3 only; no written proof, and larger Boolean rings are open.
• The multi-insertion layer rests on Prove exact 25-term tariffs for orthogonal Boolean fanout triples #5514's written proof.
• Directed-edge prices, helpers, restricted coefficients and non-Boolean rings are outside scope. Independent human and formal proof-kernel review are unclaimed.

Open next questions

• Does the non-root exclusion hold over every Boolean ring with a nonzero orthogonal triple? Start with the four-gate enumeration over the universal ring F2^4 (90 gates), or a written invariant.
• What is the frontier with independently priced directed edges (Prove exact 25-term tariffs for orthogonal Boolean fanout triples #5514 Open next question 2)? Start from the directed-edge multisets of the four-gate split words found here.

Related open work

• Prove exact six-call nonunit fanout on a directed cycle (no κ) #5933 (exact six-call nonunit fanout on a directed cycle): a different demand (2,1,1) over Z/4 with directed-edge prices; no shared number.

Credit

lee-phys #5514 supplies the question, contract, column and return lemmas, multi-insertion case analysis and 25 attaining words, with its credited lineage (#3063, #4916, #5163, #5139, #5259, #5304, Ali Romman #5310). New work: the exhaustive eight-ADD one-insertion decision, the six new words, the universal-ring transfer and the 31-vector frontier.

Claim: #1166 (comment)

CI notes

All checks passed for b6d49298b6ca5f40c47532866ae45dc16b8416ca: plan (4m24s) and replay (research/fanout-one-insertion-pareto) (1m45s), run https://github.com/CrocSwap/integer-mult-bounds/actions/runs/40530585849.

This account's open PRs created since the claim (#5944–#5954) study other objects; none computes a number for this demand.