[petalas]

Result and claim type

Scoped written proof with an exact rational certificate. No κ, no word, no supplier, no selected-frontier change.

Theorem 3 of #6933 bounds the rank of a k-block pattern on the P104 ports by a weight program on an orthogonal 8-set K, and leaves the optimality of its weights open ("the weights here are from a grid; no claim is made that they are optimal"). This PR fixes the exact supremum of that program:

for every orthogonal 8-set K of P104 and every admissible weight vector a:
    f(a) = (E - mu)/(mu + rho) <= 5/6,
and 5/6 is attained, exactly when K has type (E; d) = (22; 5,5,5,5,6,6,6,6)
and a_c = 1/2 for every c in K.

The proof is a multiplier identity, not a search. With w_c = 5 d_c - 11, the uniform edge multiplier 14/5 and the vertex multipliers mu_c = ((11/5) d_c - 11)/(d_c - 2) satisfy

d_c (14/5) + mu_c (d_c - 2) = 5 d_c - 11        at every vertex,

so summing (W1) and (W2) over the E edges and the 8 vertices gives 5D - 11A <= 88 - E, which is algebraically the same as f <= 5/6. The cost (19/5)E + 2 sum_c mu_c is exactly 88 on the principal type and strictly below it on the other two recorded types, so equality forces E = 22 with four degree-6 vertices, every edge tight, and a_c = 1/2 at degree 6; each degree-5 vertex then has a degree-6 neighbour (five neighbours, only three other degree-5 vertices), so a_c = 1/2 there too.

Consequence for the next contributor: no reweighting of the star inequality raises the floor 53/6 on any orthogonal 8-set of P104, and the maximizer is unique. A strict improvement needs a sharper non-weight inequality, which is what #7114 supplies with k <= g_T(c) + g_T(d) + min(Y_c, Y_d) and the floor 9. This PR is the post-mortem on the weight route, not a competing value, and it does not bound w(P104; F).

Predecessor credit: the orthogonal-8-set setting, Theorem 3, constraints (W1)/(W2), the type census and the recorded values 5/6, 101/126, 3/4 are DreamingOfClouds's #6933, with its retained Bukh–Cox, Haemers and Blasiak lineage. #7114 (DreamingOfClouds) is the sharper edge inequality, cited as the successor route. Those are cited premises, not audit targets. The exact optimum, the multiplier certificate, the equality case and the verifier were produced by Nick Petalas.

Evidence and reproduction

New package research/p104-star-weight-optimum/ only:

• PROOF.md: the two identities, the multiplier certificate, the per-type cost table, the theorem, the equality case, and the corollaries.
• verify.py: exact rational arithmetic, no floating-point decisions.

~/git/integer-mult-bounds/.venv/bin/python3.12 -I -B research/p104-star-weight-optimum/verify.py

About 5 s, standard library only. It recomputes from the P104 port vectors the 104 ports, the 1728 orthogonal 8-sets, the orthonormal basis K + v with v the all-ones vector plus sum(K), the parity identity |A(t)| + eps = 1, simplicity of the edge graph, and the 960 / 384 / 384 type census; the three recorded values at #6933's own weights (5/6, 101/126, 3/4); the coefficient identity; the cost bound with maximum exactly 88 on the principal type; f <= 5/6 on 20,401 feasible weight vectors (cap-box corners and repaired random draws) over all 1728 sets, with equality only at a = 1/2 on the principal type; and the rigidity lemma on all 960 principal-type sets.

Controls, all printing PASS: a weight violating (W2) gives 99/115 > 5/6; a mutant multiplier 13/5 breaks the coefficient identity; a mutated census count is detected. Final marker PASS_P104_STAR_WEIGHT_OPTIMUM.

Package checks run locally on commit d7ede50f9:

~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/p104-star-weight-optimum
~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/p104-star-weight-optimum --check-source-history

Both pass (PASS_REGISTERED_RESEARCH_PACKAGE outcome=completed, PASS_RESEARCH_COMMIT_BYTES). The registered VERIFY command is the verify.py run above; it takes about 5 s, well under the 10-minute CI limit.

Limitations and unrun obligations

• P104 only. The same certificate fails on P112 and P120 because their edge counts already exceed the budget 88 - E. Their star values 1 are not re-derived and no optimality claim is made for them.
• The rank inequality is cited, not re-derived. This package proves only the optimum of the weight program and its equality case. It does not bound w(P104; F) and does not re-check Theorem 3.
• The type census is Port windows are a fractional Haemers bound: w >= 53/6 on P104 (no new κ) #6933's result, recomputed here only because the certificate's cost depends on it.
• No human or proof-kernel review. No construction, decoder, native word, supplier or κ.

Open next questions

1. P112 and P120. Is the star value 1 the exact optimum of the same weight program there, and is its maximizer rigid? A non-uniform multiplier pattern is needed, since the uniform one already costs more than 88 - E.
2. Degree-7 vertices. The cost budget is exhausted exactly on the principal type, so the uniform certificate cannot exploit a degree-7 vertex's stronger (W2) cap on the (22; 5,5,5,5,5,6,6,7) type. A mixed certificate would decide whether 101/126 is that type's optimum.
3. Rigidity of P104 port window is exactly 9 in characteristic 2 (no κ) #7114's edge inequality. min(Y_c, Y_d) now carries the floor 9. An equality analysis would say whether the star route has any remaining headroom at all, in the same way this PR settles the weight program.

Related open work

• P104 port window is exactly 9 in characteristic 2 (no κ) #7114 (P104 port window is exactly 9 in characteristic 2) studies the same port window. It reaches w(P104; F) >= 9 by sharpening the edge inequality rather than the weights, so it does not compute the quantity bounded here; this PR's 5/6 is the exact ceiling of the weight program alone, and no agreement or disagreement with that value is claimed.
• No other open PR studies the weighted star program of Port windows are a fractional Haemers bound: w >= 53/6 on P104 (no new κ) #6933; Exclude rank 15 in the fixed P120 quadratic space (no κ) #7266 and Witness a characteristic-3 rank-32 pattern on P120. #7087 study P120 rank patterns for a different quantity.

CI notes

Local package checks and the registered verifier pass on d7ede50f9c3045dfc7293f53ff9303f19e1a89b7. CI did not certify the package.

• Run: https://github.com/CrocSwap/integer-mult-bounds/actions/runs/43105875821 (job 130808921912), head d7ede50f9.
• The plan job failed at the "Onboarding helper tests" step on exactly one test out of 760 (24 skipped): test_research_current_status.CurrentCiNavigationTests.test_current_ci_section_matches_selected_record, with AssertionError: 'make frontier7000-verify' not found in '# CI verification ...'.
• Cause, checked in the log and in the files: on main (e54523517) certificates/selected-result.json names make frontier7000-verify, while docs/ci-verification.md still describes Conditional κ .003125804 (+5.22e-7 over #5907): remove helper 470's frame-593 rung, the twin of #5907's removal #6030 and make frontier6030-verify. The test therefore fails on main's own files.
• This PR touches only research/p104-star-weight-optimum/ (6 added files, 781 lines; no existing file is modified).
• The same single test fails, one failure each out of 760, in runs 42905094314, 42903313790 and 43105433200.
• The replay job was skipped because plan failed, so no CI job certified the package contents or the registered verifier. The certification for this package is local only: PASS_REGISTERED_RESEARCH_PACKAGE outcome=completed and PASS_RESEARCH_COMMIT_BYTES on d7ede50f9, plus the verify.py run above.