[petalas]

Result

Unsigned F3 connector with n immutable sources, all 2^n − 1 binary-mask outputs and one dirty restored connector. Write the optimum as 3(n + 2^n − 1) + 3X(n), where X(n) is the excess over the floor.

• Deletion step (scoped proof): every legal word is a source path with readout lists, and deleting source j gives a legal (n − 1)-source word with excess at most X − load_j. If X ≥ 1, some source has load at least one, so X(n − 1) ≤ X(n) − 1. With Prove the seven-source F3 connector floor fails: optimum 405, floor attained exactly for n ≤ 6 (no new κ) #4250's seven-source exclusion, X(n) ≥ n − 6 for every n ≥ 7.
• Eight sources, exact (proof plus finite certificate): a 30-event path with two sources doubled serves all 255 masks with readout triples. The word has 795 calls, which meets the bound. opt(8) = 795, floor 789 + 6.
• Nine sources (finite certificate): a 39-event path with four doubled sources gives 1572 calls, so 1569 ≤ opt(9) ≤ 1572.
• Counting (proof): a cyclic triple count, combined with the deletion step, gives a lower-bound table to n = 64. It overtakes n − 6 from n = 17 (X(20) ≥ 42).

This answers #4250's open question 1 for n = 8: the optimum is not floor + 3 there. No new κ, no selected-frontier change, no multiplication theorem. Only research/f3-n-source-connector-excess/ is added.

Evidence

verify.py is standard-library only. It builds both certified words call by call and simulates them with generic noncommuting coefficients (z as a formal sum over z0 and B_j x_j; each A_m left-multiplies). It checks the lower-bound table, applies the deletion map to every source of both words and of #4232's 405-call word, simulates each result and compares its excess with the lemma. Four mutation controls must be rejected.

Reproduce from the repository root:

~/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/f3-n-source-connector-excess/verify.py
~/git/integer-mult-bounds/.venv/bin/python3.12 -O -W error -B research/f3-n-source-connector-excess/verify.py
~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/f3-n-source-connector-excess
~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/f3-n-source-connector-excess --check-source-history

Expected marker: PASS_F3_N_SOURCE_CONNECTOR_EXCESS opt8=795 excess_lb=n-6 exact_n=8, receipt 75687d9b04722afd0f687e9028b5af842b7d3330d4c1c42085f4c206ff18d870 bound to all six package files. Locally each registered command takes about 1.2 s; research_package.py and the committed-byte/source-history preflight pass on head 3db80aec82509d9fe1137b8b99426300e03cdfc3.

Limitations

• The lower bound depends on Prove the seven-source F3 connector floor fails: optimum 405, floor attained exactly for n ≤ 6 (no new κ) #4250's n = 7 computer census, which is cited, not replayed. The deletion step and the counting bound are written proofs. No proof-kernel check or independent human review is claimed.
• Exact optima are known only for n ≤ 8. Annealing with three doubled sources at n = 9 reached 499 of 511 masks; at n = 10 fourteen runs reached at most 993 of 1023. These are search failures, not exclusions, and the annealing code is not committed.
• Unsigned, immutable-source, complete-call F3 interface only. Admission, coefficient preparation, dispatch and physical costs are unknown; no consumer is instantiated.

Open next questions

1. Is opt(9) 1569 or 1572?
2. Exact optima for n = 10..16, where the deletion step beats the counting bound.
3. Can the deletion step remove more than one excess unit per source, for example by averaging loads?

Related open work

• Prove the seven-source F3 connector floor fails: optimum 405, floor attained exactly for n ≤ 6 (no new κ) #4250 (head aa61e1746f8c12807bed59cd169591bd82320bc6): seven-source optimum 405, X(7) = 1. Base case of the induction here; this PR answers its open question 1 at n = 8. Its 405 agrees: the verifier rebuilds Bound the unsigned F3 connector floor for every source count: attained for n ≤ 6, impossible for n ≥ 14 (no new κ) #4232's 405-call word and every one of its seven deletions is a 207-call six-source floor word.
• Bound the unsigned F3 connector floor for every source count: attained for n ≤ 6, impossible for n ≥ 14 (no new κ) #4232 (head 86ad339efc9f817846479431d8cc0f04edf95fb9): interface, floor deletion lemma (the X = 0 case of the lemma here) and counting threshold. Its C(3n+3, 3) count is sharpened to C(3n+2, 3) by counting boundaries cyclically; both leave n ≤ 13 open for the floor, which agrees.
• Lower the characteristic-four connector floor bound to N(4) ≤ 20; the known nine-source walk does not extend (no new κ) #4255: parity bounds for the binary-mask floor in even characteristic. Odd characteristic here; no shared number.
• Prove the optimal full-coefficient connector overhead exponent in every finite characteristic (no new κ) #4256: full coefficient demand over characteristic c. Different output set; no shared number.
• Reach the unsigned connector floor for k ≤ 2c in every characteristic; 9 ≤ N(4) ≤ 21 (no new κ) #4248, Classify the unsigned five-source connector in every characteristic (36c for c ≥ 3; no new κ) #4231, Prove the exact 108-call unsigned F3 five-source connector optimum #4225: floor results at other characteristics or at n = 5 (108 at c = 3 agrees with X(5) = 0).

CI notes

Hosted run 39506081119 on head 3db80aec82509d9fe1137b8b99426300e03cdfc3 is green: plan passed in 3m2s and the package replay in 1m11s. No check failed and no local obligation was left to CI.

Produced by Nick Petalas. The interface, floor deletion lemma and 405-call word are from #4232; the seven-source exclusion from #4250; the mod-three count argument from #4225; the F3 alphabet and one-source handoff from Riquelme Soares's #4189; the connector interface and prefix-readout criterion from Ross Richardson's #943. Apache-2.0.