diff --git a/research/p104-star-weight-optimum/PROOF.md b/research/p104-star-weight-optimum/PROOF.md new file mode 100644 index 0000000000..a1ac664ca6 --- /dev/null +++ b/research/p104-star-weight-optimum/PROOF.md @@ -0,0 +1,192 @@ +# Exact optimum of the weighted star program on P104 + +## 0. Setting and cited premises + +Let `V` be the 104-port set P104 of [vector port systems], a set of 104 vectors of +`F_2^9` of weight `3 mod 4`; two distinct ports are adjacent when their dot +product is `1` and orthogonal when it is `0`. + +Fix an orthogonal 8-set `K` of `V` (eight pairwise orthogonal ports) and put +`v = 1 + sum(K)`, the all-ones vector plus the sum of `K` in `F_2^9`. Then +`dot(v, c) = 0` for `c` in `K` and `dot(v, v) = 1`, so `K` together with `v` is +an orthonormal basis of `F_2^9`. Every port `t` is therefore + +```text +t = sum_{c in A(t)} c + eps(t) v, A(t) = {c in K : dot(t,c) = 1}, eps(t) = dot(t,v), +``` + +with `|A(t)| + eps(t) = 1` mod 2. A port outside `K` is an **edge port** if +`|A(t)| = 2`. Distinct edge ports have distinct pairs `A(t)`, so the **edge +graph** `Gamma(K)`, with vertex set `K` and one edge per edge port, is simple. +Write `E` for the number of edge ports, `d_c` for the degree of `c` in +`Gamma(K)`, and `m = |E(Gamma(K))| = E` (simplicity). + +These facts, and the type census used in Lemma 4, are Theorem 3 and its +structural section in [the predecessor package](../p104-port-window-haemers/THEOREM.md) +(#6933, DreamingOfClouds). They are cited premises. `verify.py` recomputes the +census so that the certificate below is self-contained, but the mathematics of +this package begins at Lemma 1. + +**Theorem 3 of #6933 (cited).** Let `a_c >= 0` be weights on `K` with + +```text +(W1) a_c + a_d <= 1 for every edge cd of Gamma(K), +(W2) a_c (d_c - 2) <= 2 for every c in K. +``` + +Put + +```text +mu = sum_{c in K} (1 + a_c), +rho = sum_{cd in E(Gamma(K))} (1 - a_c - a_d). +``` + +Then for every field `F`, every `k` and every `k`-block pattern `B` on `V`, +writing `rank B = 8k + j`, + +```text +j/k >= (E - mu) / (mu + rho). +``` + +The right-hand side is a function `f(a)`. #6933 evaluates `f` at weights from a +grid and states that it makes no claim that they are optimal. The theorem below +computes the exact supremum of `f` over the whole admissible set, and its +equality case. + +## 1. Two identities + +**Lemma 1.** With `A = sum_c a_c` and `D = sum_c d_c a_c`, + +```text +mu = 8 + A, rho = E - D, mu + rho = 8 + A + E - D. +``` + +*Proof.* `mu = sum_c (1 + a_c) = 8 + A`. Every edge of `Gamma(K)` contributes +`1 - a_c - a_d`, so summing over the `E` edges counts each `a_c` exactly `d_c` +times: `rho = E - sum_c d_c a_c = E - D`. ∎ + +Note `mu + rho = mu + rho >= 8 > 0`, so `f` is defined and no sign case arises. + +**Lemma 2.** `f(a) <= 5/6` if and only if `5D - 11A <= 88 - E`. + +*Proof.* Since `mu + rho > 0`, + +```text +f <= 5/6 <=> 6 (E - 8 - A) <= 5 (8 + A + E - D) + <=> 6E - 48 - 6A <= 40 + 5A + 5E - 5D + <=> E - 88 <= 11A - 5D + <=> 5D - 11A <= 88 - E. ∎ +``` + +## 2. The multiplier certificate + +**Lemma 3.** Let `lambda = 14/5` and, for each `c` in `K`, + +```text +mu_c = ( (11/5) d_c - 11 ) / (d_c - 2). +``` + +For `d_c >= 5` the number `mu_c` is nonnegative, and for every `c` + +```text +d_c lambda + mu_c (d_c - 2) = 5 d_c - 11. (identity) +``` + +Consequently, for every `a` satisfying (W1) and (W2), + +```text +5D - 11A <= (14/5) E + 2 sum_c mu_c. +``` + +*Proof.* `d_c lambda + mu_c(d_c - 2) = (14/5) d_c + (11/5) d_c - 11 = 5 d_c - 11`. +Then + +```text +5D - 11A = sum_c (5 d_c - 11) a_c + = sum_c a_c [ d_c lambda + mu_c (d_c - 2) ] + = lambda sum_{cd in E(Gamma)} (a_c + a_d) + sum_c mu_c (d_c - 2) a_c + <= lambda E + 2 sum_c mu_c, +``` + +because every edge contributes `a_c + a_d` once, (W1) bounds each of the `E` +edge terms by `1`, and (W2) bounds each vertex term by `2 mu_c >= 0`. ∎ + +**Lemma 4 (cost on the three P104 types).** The quantity + +```text +(14/5) E + 2 sum_c mu_c = (19/5) E + 2 sum_c mu_c +``` + +satisfies + +| type `(E; d_c)` | `sum_c mu_c` | cost | `88 - E` | +| --- | ---: | ---: | ---: | +| `(22; 5,5,5,5,6,6,6,6)` | `11/5` | `88` | `66` | +| `(22; 5,5,5,5,5,6,6,7)` | `99/50` | `4378/50` | `66` | +| `(21; 5,5,5,5,5,5,6,6)` | `11/10` | `82` | `67` | + +So in every case `(14/5)E + 2 sum_c mu_c <= 88 - E`. + +*Proof.* `mu_5 = ((11/5)·5 - 11)/3 = 0`, `mu_6 = (66/5 - 11)/4 = 11/20`, and +`mu_7 = (77/5 - 11)/5 = 22/25`. Sum over the multiplicities of each type and add +`(14/5)E = (14/5)·22` or `(14/5)·21`. The first row gives +`308/5 + 2·11/5 = 330/5 = 66`; the second `308/5 + 2·99/50 = 4378/50 <= 66`; the +third `294/5 + 2·11/10 = 82 <= 67`. The three types are the complete census of +orthogonal 8-sets of P104. ∎ + +## 3. The theorem + +**Theorem.** For every orthogonal 8-set `K` of P104 and every weight vector `a` +satisfying (W1) and (W2), + +```text +f(a) = (E - mu)/(mu + rho) <= 5/6. +``` + +Moreover `f(a) = 5/6` holds exactly when `K` has type `(22; 5,5,5,5,6,6,6,6)` +and `a_c = 1/2` for every `c` in `K`. + +*Proof.* Lemma 3 and Lemma 4 give `5D - 11A <= 88 - E`, which is `f(a) <= 5/6` +by Lemma 2. This proves the bound. + +For the equality case, `f(a) = 5/6` forces equality in every link of the chain. + +1. *Cost equality.* `(14/5)E + 2 sum_c mu_c = 88 - E`. By Lemma 4 the cost is + `88` only for `E = 22` with `sum_c mu_c = 11/5`. Since `mu_c = 0` at degree 5, + `mu_c = 11/20` at degree 6 and `mu_c = 22/25` at degree 7, the only multiset of + eight degrees with `sum_c mu_c = 11/5 = 4 · 11/20` is `(5,5,5,5,6,6,6,6)`. +2. *Vertex equalities.* `lambda = 14/5 > 0`, so every one of the `E` edge terms + must be tight: `a_c + a_d = 1` for every edge `cd`. And `mu_c > 0` at every + degree-6 vertex, so `(d_c - 2) a_c = 2`, i.e. `a_c = 1/2` at every degree-6 + vertex. +3. *Degree 5.* A degree-5 vertex has five neighbours but only three other + degree-5 vertices, so it has a neighbour `d` with `d_d = 6`. Then + `a_c = 1 - a_d = 1/2`. + +Conversely, `a_c = 1/2` for all `c` is admissible: (W1) gives `1/2 + 1/2 = 1`, and +(W2) gives `(1/2)·3 = 3/2 <= 2` at degree 5 and `(1/2)·4 = 2 <= 2` at degree 6. +For the principal type it yields `mu = 8 + 4 = 12`, `rho = 22 - 22 = 0`, hence +`f = 10/12 = 5/6`. ∎ + +## 4. Corollaries + +**Corollary 1.** No choice of weights satisfying (W1) and (W2) makes Theorem 3 of +#6933 exceed `j/k >= 5/6` on any orthogonal 8-set of P104. Since the bound +`rank B >= 53k/6` is exactly this inequality, no reweighting raises the floor +`53/6`. The maximizer is unique, so the weight program has no second regime to +explore. + +**Corollary 2.** Any strict improvement of the star route must change an +inequality that is not a weight: a sharper edge or star inequality. This is what +[#7114](https://github.com/CrocSwap/integer-mult-bounds/pull/7114) does with +`k <= g_T(c) + g_T(d) + min(Y_c, Y_d)`, reaching `j >= k` and the floor `9`. The +present theorem is the post-mortem on the weight program; it does not compete +with that value and does not bound `w(P104; F)`. + +## 5. What is not claimed + +The rank inequality of #6933 is not re-derived, only cited. The type census is +recomputed as an input to Lemma 4 but is #6933's result. No statement is made +about P112 or P120, where the certificate's cost budget already fails at the +edge count. No field, block pattern, decoder, native word, supplier, kappa or +selected-frontier change is claimed. No human or proof-kernel review. diff --git a/research/p104-star-weight-optimum/README.md b/research/p104-star-weight-optimum/README.md new file mode 100644 index 0000000000..2c4599d29f --- /dev/null +++ b/research/p104-star-weight-optimum/README.md @@ -0,0 +1,129 @@ +# The weighted star program of #6933 is exactly optimal at 5/6 on P104 + +**Claim type:** scoped written proof with an exact rational certificate. +**No kappa, no word, no supplier.** No selected-frontier change. + +This package answers the optimization question that +[#6933](https://github.com/CrocSwap/integer-mult-bounds/pull/6933) leaves open. +Its Theorem 3 proves, for weights `a` on an orthogonal 8-set `K` of P104 +satisfying + +```text +(W1) a_c + a_d <= 1 for every edge cd of the edge graph Gamma(K), +(W2) a_c (d_c - 2) <= 2 for every c in K, +``` + +the rank bound `j/k >= (E - mu)/(mu + rho)` with `mu = sum_c (1 + a_c)` and +`rho = sum_edges (1 - a_c - a_d)`. #6933 evaluates this at weights taken from a +grid and states that it makes no claim that they are optimal. It is not an +audit of that theorem: the theorem, its constraints and its type census are +cited premises. The new statement is the exact optimum of the weight program and +its equality case. + +## Result + +Write `f(a) = (E - mu)/(mu + rho)`. For P104 and every orthogonal 8-set `K`: + +```text +for every admissible a: f(a) <= 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 multiplier `14/5` on every edge and `mu_c = ((11/5) d_c - 11)/(d_c - 2)` +on each vertex, the coefficient identity + +```text +sum_{e ni c} 14/5 + mu_c (d_c - 2) = 5 d_c - 11 +``` + +holds exactly at every vertex, so + +```text +sum_c (5 d_c - 11) a_c <= (14/5) E + 2 sum_c mu_c <= 88 - E, +``` + +which is precisely `f(a) <= 5/6`. Equality forces every edge of `Gamma(K)` tight, +every degree-6 cap tight, `E = 22`, and no degree-7 vertex. Then `a_c = 1/2` at +degree 6, and every degree-5 vertex has a degree-6 neighbour (it has five +neighbours but only three other degree-5 vertices), so `a_c = 1/2` there too. + +Two consequences matter for the next contributor. + +1. **No reweighting can raise `53/6`.** The star inequality of #6933 cannot be + improved by choosing better weights, on any orthogonal 8-set of P104: `5/6` + is its exact ceiling, and the maximizer is rigid. +2. **The floor 9 needs a different inequality, which is what #7114 found.** That + PR replaces the edge inequality by `k <= g_T(c) + g_T(d) + min(Y_c, Y_d)` and + reaches `j >= k` with no weights. The present result explains why the weight + route was closed: it is a post-mortem on the weight program, not a competing + value. Where #7114 is available it supersedes the value 9; where the weight + program is reused, this fixes its ceiling. + +## Evidence + +`verify.py` recomputes everything from the P104 port vectors, with exact rational +arithmetic and no floating point decisions: + +- 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`, + and simplicity of `Gamma(K)` (`960 / 384 / 384` sets of the three types); +- the three recorded values `5/6`, `101/126`, `3/4` at #6933's own weights; +- the multiplier coefficient identity, and the cost inequality + `(19/5) E + 2 sum_c mu_c <= 88` with maximum exactly `88` on the principal + type; +- `f <= 5/6` on 20,401 feasible weight vectors (corners of the cap box and + repaired random draws) over all 1728 sets, with equality only at `a = 1/2` on + the principal type; +- the rigidity lemma on all 960 principal-type sets; +- controls: a weight vector violating (W2) gives `99/115 > 5/6`, a mutated + multiplier `13/5` breaks the coefficient identity, and a mutated census count + is detected. + +## Reproduce + +```sh +python3.12 -I -B research/p104-star-weight-optimum/verify.py +``` + +The run takes about 5 s and ends with `PASS_P104_STAR_WEIGHT_OPTIMUM`. Standard +library only. + +## Limitations + +- 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 here and no optimality claim is made for them. +- The result is about the weight program of Theorem 3. It does not bound + `w(P104; F)` and it does not re-derive the rank inequality itself. +- The census, the constraints and the ratio formula are cited from #6933; only + the optimum and its equality case are new. +- No human or proof-kernel review. No construction, no physical decoder, no + kappa. + +## Open next questions + +1. **P112 and P120.** Is the star value `1` the exact optimum of the same weight + program on those systems, and is the maximizing set rigid? The certificate + here is specific to `E = 21, 22` with degrees in `{5, 6}`; a different + multiplier pattern would be needed. +2. **Degree-7 vertices.** The cost budget is exhausted exactly on the principal + type. A mixed certificate that uses the degree-7 vertices' stronger (W2) caps + in a non-uniform way could in principle beat `5/6` on the `E = 22; 5,5,5,5,5,6,6,7` + type; the uniform certificate here cannot, and the recorded value there is + `101/126`. +3. **Sharpness of #7114's edge inequality.** Its `min(Y_c, Y_d)` step is the one + that now carries the floor. An equality analysis of that inequality would + decide whether `j >= k` is itself rigid, in the same way this package settles + the weight program. + +## Credit + +The orthogonal-8-set setting, Theorem 3, constraints (W1) and (W2), the type +census and the recorded values are DreamingOfClouds's +[#6933](https://github.com/CrocSwap/integer-mult-bounds/pull/6933), with its +retained Bukh–Cox, Haemers and Blasiak lineage. #7114 (DreamingOfClouds) is the +sharper edge inequality that reaches 9, cited here as the successor route. The +exact optimum, the multiplier certificate, the equality case and the verifier +were produced by Nick Petalas. Apache-2.0. diff --git a/research/p104-star-weight-optimum/SOURCES.json b/research/p104-star-weight-optimum/SOURCES.json new file mode 100644 index 0000000000..e5c1db21a9 --- /dev/null +++ b/research/p104-star-weight-optimum/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "75d77b328ea02ded535e7f23aee5b1e55d0bb1a8", + "sha256": "154c3d30455d778fd3343b6b4851f0fa4665f0f7625b0adb3675e2bafbbf6bf1" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/p104-port-window-haemers/THEOREM.md", + "usage": "input", + "git_blob": "5fe982487f7a5a4b7d01a39ff99ab764e8a8db01", + "sha256": "3f42c84d47f2a9656535d94bc361cadc485030321813ca5ff93ad4f3561fc177" + }, + { + "path": "research/p104-port-window-haemers/data/ports_p104.json", + "usage": "input", + "git_blob": "8037fd10877f49063a1c8a530b40c27f2453dac0", + "sha256": "691c7b7d212112115b1bfc76db89f90d304ec448dc8c4a0c43d9a5954317146c" + } + ] +} diff --git a/research/p104-star-weight-optimum/TASK.json b/research/p104-star-weight-optimum/TASK.json new file mode 100644 index 0000000000..0893e374cb --- /dev/null +++ b/research/p104-star-weight-optimum/TASK.json @@ -0,0 +1,130 @@ +{ + "schema_version": 1, + "task_id": "p104-side-correction", + "priority_revision": 8, + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "original_card": { + "id": "p104-side-correction", + "question": "Can joint helper bases and a legal causal split improve the complete P104 productive/paid invoice?", + "starting_points": [ + "docs/research/current-priorities.md", + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "research/p104-helper-subspace-splits/README.md", + "research/dyadic-helper-channel-capacity/README.md" + ], + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "acceptance_gate": "An exact arbitrary-input identity, source/target frame availability and restoration at the chosen cut, plus the complete channel+correction+idle/hosting bill or an explicit favorable bound. The native channel alone is not a supplier. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "first_experiment": "Start with the selected #5599 emitted word and review pending #5718 distinct input/output bases plus #5717/#5719 coverage before claiming work. Pick one uncovered source word, helper group and cut region. Prove the arbitrary-input relation and legal entry/exit corrections, then compare full target and paid profiles. Reject if completion, owned lifetimes or consumer costs repay the gain. A static pairing rank alone is not a physical split.", + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "allowed_variations": [ + "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes." + ], + "scope_change_triggers": [ + "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.", + "Treating an archived proposal or local numerical pass as complete supplier admission." + ], + "overlap_terms": [ + "P104", + "helper basis", + "helper split", + "5718", + "dyadic capacity" + ], + "existing_checks": [ + { + "scope": "PR #4133: literal-slot defect", + "evidence": "research/p104-literal-slot-defect/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "status": "author-checked", + "source_commit": "88666f1dee93fbd85b31fd5d6f91a219e111b5f4", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4136: uniform commutation gap", + "evidence": "research/p104-uniform-commutation-gap/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "status": "author-checked", + "source_commit": "281ce601a8be9db470de630759179c23e1dfaa88", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4140: uniform encoding gap", + "evidence": "research/p104-uniform-encoding-gap/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "status": "author-checked", + "source_commit": "de25c6525aa866962309df5d107b32d55e6e5628", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4153: source-chart shortcut exhausts its optimistic allowance", + "evidence": "research/p104-source-chart-shortcut/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "status": "author-checked", + "source_commit": "9123241fea53df77e51ffe30d9aca1625d4bf3a8", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4154: fiber-tag seam mismatch", + "evidence": "research/p104-fiber-tag-seam/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "status": "author-checked", + "source_commit": "4ffcdaee5d6255a9cea1fe53a5424435068089d0", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "status": "reviewed", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Exact supremum of the weighted star program (Theorem 3 of #6933) on P104, its equality case and its rigidity. An algebraic optimization side result at the port-window interface, not a P104 helper-split invoice and not a supplier.", + "scope_change_reason": "The card's first experiment is a source-bound helper split with a complete signed bill. This session instead settles the weight optimization that #6933 leaves explicitly open and that its own open question 2 names. The changed premise is recorded: the object is the orthogonal-8-set weight program, not an emitted word, and no productive or paid term is claimed.", + "bottleneck_link": "Side result at the port-window rank interface used by the P104 block-mask arguments. It removes a route (reweighting the star inequality) rather than pricing a supplier, so it carries no kappa and does not touch the selected frontier.", + "budget_minutes": 60, + "stop_rule": "Stop when the exact supremum and its equality case are proved and the exact rational certificate replays locally. Do not extend to P112/P120 or to the rank inequality.", + "outcome": "completed", + "evidence": "research/p104-star-weight-optimum/PROOF.md (multiplier identity and equality case); research/p104-star-weight-optimum/verify.py (census, coefficient identity, cost bound, 20,401 feasible weight vectors, rigidity, three controls).", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Is the star value 1 the exact optimum of the same weight program on P112 and P120, and is its maximizer rigid?", + "why_it_matters": "It would separate the P104 ceiling 5/6 from the P112/P120 values 1 and say whether those systems have any weight-program headroom at all.", + "first_step": "Repeat Lemma 3 with a cost budget 88 - E for E = 25, 24, 28; the uniform multiplier already costs more than the budget there, so a non-uniform pattern is needed.", + "blocked_by": "The certificate here is specific to E in {21, 22} with degrees in {5, 6}; no admissible multiplier pattern for P112/P120 is known." + }, + { + "question": "Can a non-uniform multiplier pattern on the E = 22 type (5,5,5,5,5,6,6,7) beat 5/6?", + "why_it_matters": "The uniform certificate is exactly tight on the principal type and cannot use the degree-7 vertex's stronger cap; a mixed certificate would decide whether 101/126 is that type's optimum.", + "first_step": "Write the dual of max f over the two-class polytope with an extra class for degree 7 and look for a certificate with a nonzero mu_7.", + "blocked_by": "Lemma 4's cost already has slack 44/50 on that type, so any improvement needs weights outside the uniform-edge family." + }, + { + "question": "Is the sharper edge inequality of #7114 rigid at j = k?", + "why_it_matters": "It now carries the floor 9; an equality analysis would say whether the star route has any remaining headroom at all.", + "first_step": "Impose equality in k <= g_T(c) + g_T(d) + min(Y_c, Y_d) and in the star inequality, and classify the representations attaining both.", + "blocked_by": "#7114 is an open contribution; its inequality is a cited premise here, not a reviewed result." + } + ], + "outcome_detail": "Scoped written proof with an exact rational certificate: every admissible weight vector on every orthogonal 8-set of P104 gives f <= 5/6, with equality exactly on the type (22; 5,5,5,5,6,6,6,6) at a_c = 1/2." +} diff --git a/research/p104-star-weight-optimum/VERIFY.json b/research/p104-star-weight-optimum/VERIFY.json new file mode 100644 index 0000000000..d591f27bca --- /dev/null +++ b/research/p104-star-weight-optimum/VERIFY.json @@ -0,0 +1,22 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/p104-port-window-haemers/THEOREM.md", + "research/p104-port-window-haemers/data/ports_p104.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 300, + "checks": "Recomputes the 104 P104 ports, the 1728 orthogonal 8-sets, the orthonormal basis K+v, the parity identity and simplicity of the edge graph; the 960/384/384 type census; the three recorded values 5/6, 101/126, 3/4 at #6933's weights; the multiplier coefficient identity d_c*14/5 + mu_c*(d_c-2) = 5*d_c-11; the cost bound (19/5)E + 2*sum mu <= 88 with maximum exactly 88; f <= 5/6 on 20,401 feasible weight vectors over all sets with equality only at a = 1/2 on the principal type; the degree-5/degree-6 rigidity lemma; and three controls (a (W2) violation gives 99/115, a mutant multiplier 13/5 breaks the identity, a mutated census count is detected)." + } + ] +} diff --git a/research/p104-star-weight-optimum/verify.py b/research/p104-star-weight-optimum/verify.py new file mode 100644 index 0000000000..7b10e6e777 --- /dev/null +++ b/research/p104-star-weight-optimum/verify.py @@ -0,0 +1,278 @@ +#!/usr/bin/env python3 +"""Exact verifier: the weighted star program of #6933 has ceiling 5/6 on P104. + +Standard library only. Every printed PASS line is one checked claim; any +mismatch exits non-zero. Fractions only, no floating point decisions. +""" + +import json +import random +import sys +from collections import Counter, defaultdict +from fractions import Fraction as F +from pathlib import Path + +HERE = Path(__file__).resolve().parent +REPO = HERE.parent.parent +DATA = REPO / "research/p104-port-window-haemers/data/ports_p104.json" + +FAILS = [] + + +def check(name, ok, detail=""): + if not ok: + FAILS.append(name) + print("FAIL " + name + (" " + detail if detail else "")) + else: + print("PASS " + name + (" " + detail if detail else "")) + + +def dot(a, b): + return (a & b).bit_count() & 1 + + +def main(): + ports = json.loads(DATA.read_text())["ports"] + n = len(ports) + check("ports.distinct", len(set(ports)) == n == 104, "n=%d" % n) + check("ports.nonzero_odd_weight", + all(p > 0 and p.bit_count() % 2 == 1 for p in ports)) + check("ports.weight_3_mod_4", + all(p.bit_count() % 4 == 3 for p in ports)) + + orth = [[dot(ports[i], ports[j]) == 0 for j in range(n)] for i in range(n)] + + # --- orthogonal 8-sets ------------------------------------------------- + sets = [] + cur = [] + + def dfs(start): + if len(cur) == 8: + sets.append(tuple(cur)) + return + for j in range(start, n): + if all(orth[i][j] for i in cur): + cur.append(j) + dfs(j + 1) + cur.pop() + + dfs(0) + check("orth8.count", len(sets) == 1728, "found %d" % len(sets)) + + # --- per-set structure: K + v orthonormal, edge graph, type ------------- + types = Counter() + per_type_sets = defaultdict(list) + deg_of_set = {} + edge_ok = True + deg_pos = True + for K in sets: + Kset = set(K) + v = 0x1FF # the all-ones vector of F_2^9, not the integer 1 + for c in K: + v ^= ports[c] + if dot(v, v) != 1 or any(dot(v, ports[c]) for c in K): + edge_ok = False + deg = Counter() + E = 0 + pairs = set() + for t in range(n): + if t in Kset: + continue + A = [c for c in K if dot(ports[t], ports[c]) == 1] + eps = dot(ports[t], v) + if (len(A) + eps) % 2 != 1: # |A| + eps = w(t) mod 2 = 1 + edge_ok = False + if len(A) == 2: + E += 1 + pairs.add(tuple(A)) + deg[A[0]] += 1 + deg[A[1]] += 1 + if len(pairs) != E: # (H1): distinct edge ports + edge_ok = False + ds = tuple(sorted(deg[c] for c in K)) + if min(ds) < 1: + deg_pos = False + types[(E, ds)] += 1 + per_type_sets[(E, ds)].append(K) + deg_of_set[K] = (E, ds, deg) + + check("orth8.orthonormal_basis_and_distinct_pairs", edge_ok) + check("orth8.every_vertex_positive_degree", deg_pos) + expect = { + (22, (5, 5, 5, 5, 6, 6, 6, 6)): 960, + (22, (5, 5, 5, 5, 5, 6, 6, 7)): 384, + (21, (5, 5, 5, 5, 5, 5, 6, 6)): 384, + } + check("types.census", dict(types) == expect, str(dict(types))) + + # --- the ratio of #6933 Theorem 3 -------------------------------------- + def ratio(E, deg, a): + mu = sum(1 + a[c] for c in deg) + rho = F(E) - sum(F(deg[c]) * a[c] for c in deg) + return (F(E) - mu) / (mu + rho) + + def caps(deg): + return {c: F(2, deg[c] - 2) for c in deg} + + edge_lists = {} + + def edge_list(K): + if K not in edge_lists: + Kset = set(K) + el = [] + for t in range(n): + if t in Kset: + continue + A = [c for c in K if dot(ports[t], ports[c]) == 1] + if len(A) == 2: + el.append((A[0], A[1])) + edge_lists[K] = el + return edge_lists[K] + + # 1) the three recorded P104 values of #6933 reproduce at their weights + recorded = { + (22, (5, 5, 5, 5, 6, 6, 6, 6)): (F(1, 2), F(5, 6)), + (22, (5, 5, 5, 5, 5, 6, 6, 7)): (F(2, 5), F(101, 126)), + (21, (5, 5, 5, 5, 5, 5, 6, 6)): (F(1, 2), F(3, 4)), + } + for key, (w7, want) in recorded.items(): + K = per_type_sets[key][0] + E, ds, deg = deg_of_set[K] + a = {c: (w7 if deg[c] == 7 else F(1, 2)) for c in deg} + got = ratio(E, deg, a) + check("compat.value_%s" % (ds,), got == want, "ratio %s" % got) + + # --- the universal multiplier certificate ------------------------------ + # w_c = 5 d_c - 11 ; lam = 14/5 on every edge ; + # mu_c = ((11/5) d_c - 11) / (d_c - 2) (>= 0 for d_c >= 5, tight d in {5,6}) + # coefficient identity d_c lam + mu_c (d_c - 2) = w_c + # cost (19/5) E + 2 sum_c mu_c <= 88 + lam = F(14, 5) + maxcost = F(0) + worst = None + ident_ok = True + tight_deg = set() + for K in sets: + E, ds, deg = deg_of_set[K] + cost = F(19, 5) * E + for c in deg: + mu = ((F(11, 5) * deg[c] - 11) / (deg[c] - 2)) + if mu < 0: + ident_ok = False + if deg[c] * lam + mu * (deg[c] - 2) != 5 * deg[c] - 11: + ident_ok = False + if deg[c] in (5, 6): + tight_deg.add(deg[c]) + cost += 2 * mu + if cost > maxcost: + maxcost, worst = cost, (E, ds) + if cost > 88: + ident_ok = False + check("cert.multiplier_coefficient_identity", ident_ok) + check("cert.uniform_cost_le_88", maxcost <= 88, + "max (19/5)E + 2 sum mu = %s at %s" % (maxcost, worst)) + check("cert.only_degrees_5_6_tight", tight_deg == {5, 6}) + + # --- the ratio is below 5/6 for every admissible weight vector --------- + # exact battery: a = 1/2, a = 0, vertex corners of the cap box, and + # random repaired draws, on every orthogonal 8-set. + rng = random.Random(1111) + viol = 0 + tested = 0 + strict_ok = True + for K in sets: + E, ds, deg = deg_of_set[K] + el = edge_list(K) + cap = caps(deg) + candidates = [{c: F(0) for c in deg}, {c: cap[c] for c in deg}] + for c in deg: # single-vertex corners + a = {d: F(0) for d in deg} + a[c] = cap[c] + candidates.append(a) + for _ in range(6): # repaired random draws + a = {} + for c in deg: + a[c] = F(rng.randrange(0, 21), 20) * cap[c] + for _ in range(40): + bad = [(c, d) for c, d in el if a[c] + a[d] > 1] + if not bad: + break + for c, d in bad: + a[c] = a[d] = (a[c] + a[d]) / 2 + candidates.append(a) + for a in candidates: + if any(a[c] < 0 or a[c] * (deg[c] - 2) > 2 for c in deg): + continue + if any(a[c] + a[d] > 1 for c, d in el): + continue + tested += 1 + f = ratio(E, deg, a) + if f > F(5, 6): + viol += 1 + if f == F(5, 6) and ds == (5, 5, 5, 5, 6, 6, 6, 6) and a != half: + strict_ok = False + check("bound.no_violation_on_battery", viol == 0, + "%d feasible weight vectors tested" % tested) + check("bound.equality_only_at_half_on_principal_type", strict_ok) + + # --- equality is attained, so 5/6 is the exact supremum --------------- + K = per_type_sets[(22, (5, 5, 5, 5, 6, 6, 6, 6))][0] + E, ds, deg = deg_of_set[K] + el = edge_list(K) + a = {c: F(1, 2) for c in deg} + check("sharp.attained_at_half", + all(a[c] * (deg[c] - 2) <= 2 for c in deg) and + all(a[c] + a[d] <= 1 for c, d in el) and + ratio(E, deg, a) == F(5, 6), + "ratio %s" % ratio(E, deg, a)) + + # --- rigidity: every degree-5 vertex has a degree-6 neighbour --------- + # This is the step that turns "all edges tight" into "all a_c = 1/2": + # a degree-5 vertex has 5 neighbours but only 3 other degree-5 vertices. + rigid = True + for K in per_type_sets[(22, (5, 5, 5, 5, 6, 6, 6, 6))]: + E, ds, deg = deg_of_set[K] + nbr = defaultdict(set) + for c, d in edge_list(K): + nbr[c].add(d) + nbr[d].add(c) + for c in deg: + if deg[c] == 5 and not any(deg[d] == 6 for d in nbr[c]): + rigid = False + check("rigid.degree5_vertex_has_degree6_neighbour", rigid) + + # --- controls --------------------------------------------------------- + # (a) the hypothesis (W2) is needed: a_c = 3/5 at a degree-6 vertex + K = per_type_sets[(22, (5, 5, 5, 5, 6, 6, 6, 6))][0] + E, ds, deg = deg_of_set[K] + a = {c: F(1, 2) for c in deg} + big = next(c for c in deg if deg[c] == 6) + a[big] = F(3, 5) + violated = a[big] * (deg[big] - 2) > 2 + check("control.w2_needed", violated and ratio(E, deg, a) > F(5, 6), + "ratio %s with a_c=3/5" % ratio(E, deg, a)) + + # (b) a mutant multiplier must fail the coefficient identity + lam_bad = F(13, 5) + mutant_breaks = False + for c in deg: + mu = ((F(11, 5) * deg[c] - 11) / (deg[c] - 2)) + if deg[c] * lam_bad + mu * (deg[c] - 2) != 5 * deg[c] - 11: + mutant_breaks = True + check("control.mutant_multiplier_detected", mutant_breaks) + + # (c) a mutated census count must be detected + wrong = dict(expect) + wrong[(22, (5, 5, 5, 5, 6, 6, 6, 6))] = 959 + check("control.mutated_census_detected", wrong != dict(types)) + + if FAILS: + print("FAILED_P104_STAR_WEIGHT_OPTIMUM %d failing checks: %s" + % (len(FAILS), ", ".join(FAILS))) + return 1 + print("PASS_P104_STAR_WEIGHT_OPTIMUM") + return 0 + + +if __name__ == "__main__": + sys.exit(main())