From a8ae38561deb40edbd41b9f8790fab6ac949c0a3 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Tue, 10 Nov 2026 21:45:04 +0000 Subject: [PATCH] feat(research): certify the star-pattern floor n+1 on W4 and K33 Exact rational duals of the Shannon-type rank program prove that every k-block pattern on G_Gamma has rank at least (n+1)k over every field for the wheel W4 and for K33, two graphs of minimum degree 3 without K4. The Gram labels give the matching upper bound, so the fractional Haemers bound is 6 and 7. The prism stays uncertified and is listed as open. --- .../star-pattern-degree-three-floor/README.md | 212 ++++++++++++++++++ .../SOURCES.json | 37 +++ .../star-pattern-degree-three-floor/TASK.json | 139 ++++++++++++ .../VERIFY.json | 38 ++++ .../certificates.json | 1 + .../derive_certificates.py | 112 +++++++++ .../star_graphs.py | 172 ++++++++++++++ .../star-pattern-degree-three-floor/verify.py | 177 +++++++++++++++ 8 files changed, 888 insertions(+) create mode 100644 research/star-pattern-degree-three-floor/README.md create mode 100644 research/star-pattern-degree-three-floor/SOURCES.json create mode 100644 research/star-pattern-degree-three-floor/TASK.json create mode 100644 research/star-pattern-degree-three-floor/VERIFY.json create mode 100644 research/star-pattern-degree-three-floor/certificates.json create mode 100644 research/star-pattern-degree-three-floor/derive_certificates.py create mode 100644 research/star-pattern-degree-three-floor/star_graphs.py create mode 100644 research/star-pattern-degree-three-floor/verify.py diff --git a/research/star-pattern-degree-three-floor/README.md b/research/star-pattern-degree-three-floor/README.md new file mode 100644 index 0000000000..08f2c1e94e --- /dev/null +++ b/research/star-pattern-degree-three-floor/README.md @@ -0,0 +1,212 @@ +# Star patterns at minimum degree three: the floor n+1 on the wheel W4 and on K33 (no κ) + +No κ claim, no word and no supplier change. This package extends the star-pattern +floor of DreamingOfClouds's open PR #7114 from minimum degree four to two graphs +of minimum degree three that contain no `K_4`. + +## 1. Result + +Notation is that of #7114 (section 8) and #6933. For a simple graph Γ on `n` +points, `G_Γ` has the points and the edges of Γ ("pairs") as vertices. A point is +adjacent to the pairs containing it, two pairs are adjacent iff they are +disjoint, and two points are never adjacent. A *k-block pattern* on a graph is a +matrix with `k x k` blocks, invertible diagonal blocks and zero blocks on +non-adjacent pairs. `H_f(G;F)` is the infimum of `rank/k` over all `k` and all +k-block patterns over the field `F` (the fractional Haemers bound of Bukh and Cox). + +**Theorem 1 (finite certificate plus the scoped proof of section 2).** Let Γ be +the wheel `W_4` (a hub joined to a 4-cycle, `n = 5`) or `K_{3,3}` (`n = 6`). +For every field `F` and every `k`, every k-block pattern on `G_Γ` has rank at +least `(n+1)k`. Hence + +| Γ | minimum degree | contains `K_4` | `H_f(G_Γ;F)`, every field | +|---|---|---|---| +| `W_4` | 3 | no | 6 | +| `K_{3,3}` | 3 | no | 7 | + +The upper bound `n+1` is the Gram representation of #7114 Corollary 12, which +the verifier rebuilds as an integer matrix and checks entry by entry. + +**Corollary 2 (star configurations, scoped proof).** Let `(K, Γ, (T_e))` be a +star configuration in a graph `G` in the sense of #7114 section 1, with +`|K| = m`. If Γ has a subgraph isomorphic to `W_4` or `K_{3,3}`, then every +k-block pattern on `G` over every field has rank at least `(m+1)k`. In the +notation of #7114 Theorem 3', `j >= k`. + +**Corollary 3 (five points, exhaustive count).** All 26 labelled graphs on five +points with minimum degree at least 3 contain `W_4`, so Corollary 2 applies to +each of them. The one such graph on four points is `K_4`, where `G_Γ` is the +Petersen graph; its value 5 is the published result cited under Credit and related work and is +not re-proved here. + +**Remark 4 (degree two is not enough, scoped proof).** For every cycle `C_n`, +`n >= 3`, `H_f(G_{C_n};F) = n` over every field. So the floor `n+1` can fail at +minimum degree 2. + +What was known: #7114 Theorem 3' gives `j >= k` when every non-isolated vertex +of Γ has degree at least 4. At degree 3 its inequality (a) gives only +`j/k >= 1/2` for cubic Γ. The Petersen case `Γ = K_4` has value 5 by Blasiak, +Kleinberg and Lubetzky, with an all-field dual in Tuafo's merged #1744. + +## 2. Why a dual certificate bounds every block pattern + +This is the rank argument of Tuafo's #1744 +(`research/p112-characteristic-two-minrank/README.md`, "Exact Petersen +certificate and the all-field lower bound"), restated for a general graph `G` +with vertex set `V`. + +Let `B` be a k-block pattern on `G` over a field `F`. Let `W` be the row space +of `B` inside `F^(|V| k)`, let `E_v` be the span of the `k` coordinate vectors of +block `v`, and put + +```text +f(S) = dim(W + sum of E_v over v in S) / k for S a subset of V. +``` + +Then `f(empty) = rank(B)/k` and: + +- **(N)** `f(V) = |V|`. +- **(M)** `f(S+v) - f(S) <= 1`: block `v` adds at most `k` dimensions. +- **(S)** `f(S+i) + f(S+j) >= f(S+i+j) + f(S)`: write `A_S = W + E_S`. Then + `A_{S+i} + A_{S+j} = A_{S+i+j}` and `A_{S+i} ∩ A_{S+j}` contains `A_S`, and + `dim X + dim Y = dim(X+Y) + dim(X ∩ Y)`. +- **(D)** `f(S+v) = f(S)` if every neighbour of `v` lies in `S`: the `k` rows of + block row `v` lie in `W`, and they vanish outside block `v` and the blocks of + the neighbours of `v`. Subtracting their neighbour parts, which lie in `E_S`, + leaves `k` vectors supported in block `v` whose entries are the rows of the + invertible block `B_vv`. They span `E_v`, so `E_v` lies in `W + E_S`. + +By (D), `f(S) = f(cl S)`, where `cl S` is obtained by adding, repeatedly, every +vertex whose neighbours all lie in the set. A *certificate* is a list of +instances of (M) and (S) with positive rational multipliers whose weighted sum, +after replacing every set by its closure, is + +```text +f(cl empty) - c f(V) >= r. +``` + +With (N) it proves `rank(B)/k = f(empty) >= r + c |V|` for every `k` and every +field. No field property is used. + +`certificates.json` lists, for each graph, entries `["M", S, v]` and +`["S", S, i, j]` (sets as bit masks, points first, then pairs in the listed edge +order) with a multiplier. The verifier applies every automorphism of Γ to every +entry and gives each image the multiplier divided by the group order. Each image +is again an instance of (M) or (S), so the averaged list is a certificate in the +sense above, whatever the group is. The sizes: + +| Γ | vertices of `G_Γ` | automorphisms | listed entries | `r + c |V|` | +|---|---|---|---|---| +| `W_4` | 13 | 8 | 86 | 6 | +| `K_{3,3}` | 15 | 72 | 197 | 7 | + +## 3. Proofs of the corollaries and the remark + +**Corollary 2.** Let Γ' be a subgraph of Γ isomorphic to `W_4` or `K_{3,3}`, +with point set `Q` inside `K`. Keep all of `K` and only the edge ports `T_e` +with `e` an edge of Γ'. By (C1) of #7114 such a port is adjacent to its two +ends, which lie in `Q`, and to no other vertex of `K`. So the induced subgraph +of `G` on these vertices is the disjoint union of the `m - |Q|` isolated +vertices `K \ Q` and a graph `H` on `Q` and the chosen ports. By (C1) and (C2), +`H` has every point-pair edge of `G_{Γ'}` and no edge between pairs that share +a point; pairs that are disjoint may or may not be adjacent. So `H` is a +spanning subgraph of `G_{Γ'}`, and a pattern on `H` is a pattern on `G_{Γ'}` +(it has the required zero blocks and more). The principal submatrix of a +k-block pattern on these vertices is block diagonal: `m - |Q|` invertible +`k x k` blocks and a pattern on `H`. Its rank is at least +`(m - |Q|)k + (|Q| + 1)k = (m+1)k` by Theorem 1, and the rank of the whole +pattern is at least that. ∎ + +**Corollary 3.** The verifier enumerates all `2^10` labelled graphs on five +points and all `2^6` on four, keeps those of minimum degree at least 3, and +searches each for `K_4` and `W_4`. Counts: 26 graphs on five points (11 contain +`K_4`, all 26 contain `W_4`) and one on four points (`K_4`). ∎ + +**Remark 4.** The `n` points are pairwise non-adjacent, so the principal +submatrix on them is block diagonal with invertible blocks and the rank is at +least `nk`. For the upper bound take the `n` cliques `{c, pair (c, c+1)}`; the +sum of the outer squares of their indicator vectors has unit diagonal, is zero +outside the cliques, and has rank at most `n` over every field. The verifier +builds this matrix for `n = 3, 4, 5, 6`; the argument is the same for every `n`. ∎ + +## 4. Evidence and reproduction + +From the repository root, with CPython 3.12: + +```sh +python3.12 -B scripts/research_package.py --package research/star-pattern-degree-three-floor +python3.12 -I -B -W error -X dev research/star-pattern-degree-three-floor/verify.py +``` + +`verify.py` uses the standard library only and exact `Fraction` arithmetic. It +ends with + +```text +PASS_STAR_PATTERN_DEGREE_THREE_FLOOR graphs=2 controls=14 cycles=4 census=27 no_new_kappa +``` + +and runs in under one second. For each graph it checks minimum degree 3, the +absence of `K_4`, the certificate (bound exactly `n+1`), and the integer Gram +pattern. The 14 rejecting controls are, per graph: the certificate without its +first entry, without its last entry, with the first multiplier doubled, with the +first multiplier negated, on Γ with one edge deleted, on Γ with one edge moved, +and the Gram matrix against `G_Γ` with one pair-pair adjacency removed. + +`derive_certificates.py` is how the certificates were found. It needs numpy and +scipy, solves the symmetry-reduced linear program in floating point, rounds the +dual, and keeps it only if the exact check accepts it. It is not registered and +the verifier never imports it: + +```sh +python3.12 -B research/star-pattern-degree-three-floor/derive_certificates.py /tmp/certificates.json +``` + +A different solver version may return a different optimal dual; any dual the +exact check accepts proves the same bound. + +## 5. Limitations + +- Finite certificates for two graphs. No statement is proved for all graphs of + minimum degree 3. +- The prism (the other cubic graph on six points) is **not** certified. The + floating-point optimum of its linear program is 7.0, but the rounded dual was + rejected by the exact check, so no bound is claimed for it. +- The linear program only bounds below. On these two graphs it meets the Gram + upper bound; on other graphs it may not. +- The block-mask model is that of #6933 and #7114: whole `k x k` blocks, one + `k` for all ports, linear labels. Nothing is said about sub-block masks or + port-dependent block sizes. +- The orthogonal 8-sets of P104, P112 and P120 have minimum degree 5, 6 and 7 + (#7114), so their floor 9 does not need this result. Corollary 2 matters for + a port system or sub-configuration whose star graph has degree-3 vertices. +- #7114 is open and unreviewed. Only its definitions and its Gram labels are + used; the labels are re-checked here as an integer matrix. +- No human or proof-kernel review of this package is claimed. + +## Open next questions + +The structured list is in [TASK.json](TASK.json). + +1. Is `j >= k` forced for **every** star configuration whose Γ has minimum + degree at least 3? The cube `Q_3` contains none of `K_4`, `W_4`, `K_{3,3}` + and has 8 + 12 = 20 vertices in `G_Γ`. +2. Certify or refute the prism value 7 with an exact dual. +3. What are the exact values at minimum degree 2 beyond cycles? A local, + unshipped run of the same exact pipeline gave lower bounds 9/2 for `K_4` + minus an edge and 11/2 for `K_{2,3}`; no matching upper bound was sought. + +## Credit and related work + +- DreamingOfClouds, #6933 (`research/p104-port-window-haemers`) and open PR + #7114 (head `fc90dc68b54d613a0600e5bddd8e4f557a4b4eda`): block patterns and + the port window, star configurations, the graphs `G_Γ`, Theorem 3', the Gram + upper bound, and the open question this package addresses. +- Tuafo, #1744 (`research/p112-characteristic-two-minrank`): the all-field rank + argument of section 2 and the exact Petersen dual. +- A. Blasiak, R. Kleinberg, E. Lubetzky, *Index coding via linear programming* + (arXiv:1004.1379): the linear program and the Petersen rate 5. +- B. Bukh, C. Cox, *On a fractional version of Haemers' bound* + (arXiv:1802.00476): `H_f`. + +The two certificates, the corollaries, the cycle remark and the verifier were +produced by Nick Petalas. New work is Apache-2.0. diff --git a/research/star-pattern-degree-three-floor/SOURCES.json b/research/star-pattern-degree-three-floor/SOURCES.json new file mode 100644 index 0000000000..9c935cb706 --- /dev/null +++ b/research/star-pattern-degree-three-floor/SOURCES.json @@ -0,0 +1,37 @@ +{ + "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/README.md", + "usage": "provenance", + "git_blob": "f35b07beb6c22820680f05364a5bc4ffeb29e6b5", + "sha256": "d375ba7c139c4e9cace1e07abebe306fadb6657c4eed00dae08d28be56f49b80" + }, + { + "path": "research/p112-characteristic-two-minrank/README.md", + "usage": "provenance", + "git_blob": "387df8b87d0ec68bba74b3d5f2f8854a36db2f06", + "sha256": "dcc2081314205d42ac29c022bf7f83be06449eb756feab1ccdc96dfbcf395510" + } + ], + "related_work": [ + { + "pr": "https://github.com/CrocSwap/integer-mult-bounds/pull/7114", + "head": "fc90dc68b54d613a0600e5bddd8e4f557a4b4eda", + "role": "Source of the open question, the star-configuration definitions and the Gram labels; no source import, replay or unmerged Git-history dependency." + } + ] +} diff --git a/research/star-pattern-degree-three-floor/TASK.json b/research/star-pattern-degree-three-floor/TASK.json new file mode 100644 index 0000000000..7d5a958445 --- /dev/null +++ b/research/star-pattern-degree-three-floor/TASK.json @@ -0,0 +1,139 @@ +{ + "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": "Determine the fractional Haemers bound H_f(G_Gamma;F) of the star-configuration graphs of PR #7114 for two graphs Gamma of minimum degree 3 without K_4, the wheel W_4 and K_{3,3}, over every field, by exact rational dual certificates of the Shannon-type rank program; derive the consequence j >= k for star configurations containing either graph.", + "scope_change_reason": "The card asks for a helper split with a complete invoice. This package instead answers a graph question left open by PR #7114's port-window theory: whether its star-pattern floor, proved at minimum degree 4, survives at minimum degree 3. No helper basis, split, word or invoice is changed.", + "bottleneck_link": "Side result. PR #6933 and PR #7114 show that a fractional block window cannot beat the tensor lift on P104 because every orthogonal 8-set has a star graph of minimum degree at least 5. This package widens the class of star graphs with that floor to every graph containing W_4 or K_{3,3}, so the same exclusion applies to port systems or sub-configurations with degree-3 vertices. It supplies no paid saving and changes no supplier.", + "budget_minutes": 60, + "stop_rule": "Stop at the first exact certificate that meets the Gram upper bound on a minimum-degree-3 graph without K_4. Leave the prism, the cube and the general degree-3 statement open.", + "outcome": "completed", + "evidence": "certificates.json holds 86 and 197 rational dual entries for W_4 and K_{3,3}. verify.py (standard library, exact Fraction arithmetic) averages each entry over the automorphisms of Gamma, checks that the combination reduces to f(empty) >= n+1, rebuilds the integer Gram pattern of rank at most n+1, enumerates all graphs on four and five points of minimum degree at least 3 (27 labelled graphs), builds rank-n patterns for cycles of length 3 to 6, and runs 14 rejecting controls. README sections 2 and 3 give the written proofs.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Is j >= k forced for every star configuration whose graph Gamma has minimum degree at least 3?", + "why_it_matters": "It would replace the degree-4 hypothesis of PR #7114 Theorem 3' by degree 3 and make the floor a property of the degree alone; K_4, W_4 and K_{3,3} are three confirming cases.", + "first_step": "Run the symmetry-reduced program on the cube Q_3 (20 vertices in G_Gamma, 48 automorphisms), which contains none of K_4, W_4, K_{3,3}; then read the W_4 certificate for a per-vertex inequality that generalizes.", + "blocked_by": "No hand proof at degree 3; the full program on 20 vertices needs a closed-set or symmetry reduction to stay small." + }, + { + "question": "Does the prism, the other cubic graph on six points, have H_f(G_Gamma;F) = 7?", + "why_it_matters": "With K_{3,3} it would settle every cubic graph on six points and remove the last small exception to the degree-3 conjecture.", + "first_step": "Solve the reduced dual exactly on the float support (2,133 orbit variables) with rational or modular linear algebra, or search the optimal dual face for a vertex with small denominators.", + "blocked_by": "The floating-point optimum is 7.0 but the rounded dual was rejected by the exact check, so no bound is claimed." + }, + { + "question": "What is H_f(G_Gamma;F) at minimum degree 2 beyond cycles, for example for K_4 minus an edge and K_{2,3}?", + "why_it_matters": "Cycles have value n. A value strictly between n and n+1 would be a star graph where a fractional window beats every integer one.", + "first_step": "Certify the local lower bounds 9/2 and 11/2 with the shipped pipeline and compare them with the fractional clique-cover number and with k = 2 block patterns over F_2.", + "blocked_by": "The two lower bounds come from a local unshipped run; no upper bound below n+1 was sought." + } + ], + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19529109", + "overlap": { + "canonical_main": "e54523517d0f03e58352e647c403a5af3e525a57", + "priority_revision": 8, + "coverage": "Live open PR list, this account's PR list, the last 30 handoff comments, git grep for Petersen across main-branch research READMEs, and all-state PR searches for Petersen and fractional Haemers. Sparse checkout; no search result proves global novelty.", + "related_open_prs": [ + 7114 + ], + "novelty_correction": "The Petersen value asked for in PR #7114 is already on main (Blasiak-Kleinberg-Lubetzky, cited by merged packages; exact all-field dual in PR #1744). The delivered result is the degree-3 floor on W_4 and K_{3,3}." + } +} diff --git a/research/star-pattern-degree-three-floor/VERIFY.json b/research/star-pattern-degree-three-floor/VERIFY.json new file mode 100644 index 0000000000..7a7edac6ae --- /dev/null +++ b/research/star-pattern-degree-three-floor/VERIFY.json @@ -0,0 +1,38 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "-W", + "error", + "-X", + "dev", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact dual certificates for W_4 and K_{3,3} (bound n+1), integer Gram patterns, the five-point census, cycle patterns and 14 rejecting controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "-W", + "error", + "-X", + "dev", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "The same checks with optimization; every check raises an explicit exception." + } + ] +} diff --git a/research/star-pattern-degree-three-floor/certificates.json b/research/star-pattern-degree-three-floor/certificates.json new file mode 100644 index 0000000000..3c1444af67 --- /dev/null +++ b/research/star-pattern-degree-three-floor/certificates.json @@ -0,0 +1 @@ +{"schema_version":1,"graphs":[{"name":"wheel-W4","points":5,"edges":[[0,1],[0,2],[0,3],[0,4],[1,2],[2,3],[3,4],[4,1]],"lower_bound":"6","certificate":[[["M",0,1],"1"],[["M",2,6],"1"],[["M",36,12],"1"],[["M",520,10],"3/16"],[["S",520,11,12],"3/16"],[["M",560,3],"5/8"],[["M",560,10],"1/2"],[["S",560,7,11],"1/8"],[["M",568,6],"5/8"],[["M",648,4],"1/16"],[["S",648,8,11],"1/16"],[["M",664,6],"1/16"],[["S",688,10,11],"1/8"],[["M",720,10],"1/16"],[["S",720,3,5],"1/16"],[["S",752,10,11],"1/16"],[["S",904,11,12],"1/16"],[["M",1538,0],"3/16"],[["M",1539,4],"3/16"],[["S",1552,5,7],"1/16"],[["S",1552,5,11],"1/16"],[["S",1552,5,12],"1/16"],[["M",1584,0],"1/4"],[["M",1636,12],"1/16"],[["S",1636,4,11],"1/16"],[["S",1712,1,11],"1/16"],[["S",1714,3,12],"1/16"],[["S",1722,6,8],"1/16"],[["S",1780,1,3],"1/16"],[["M",1811,11],"3/16"],[["S",1840,0,3],"1/16"],[["M",1841,12],"3/16"],[["S",1848,0,1],"1/16"],[["S",1850,0,12],"1/16"],[["S",1978,11,12],"1/16"],[["S",2562,2,5],"3/16"],[["S",2566,5,8],"3/16"],[["S",2594,0,12],"1/4"],[["S",2595,2,8],"1/8"],[["S",2595,2,12],"1/8"],[["S",2599,8,12],"1/4"],[["M",2600,12],"1/4"],[["S",2600,6,7],"1/4"],[["S",2608,1,6],"1/16"],[["S",2608,3,12],"1/16"],[["S",2610,6,10],"1/16"],[["S",2616,6,8],"3/16"],[["S",2616,6,10],"1/16"],[["M",2664,8],"1/16"],[["S",2664,4,7],"3/8"],[["S",2722,3,8],"1/4"],[["S",2730,6,10],"1/4"],[["S",2757,3,5],"1/8"],[["S",2759,5,8],"1/8"],[["S",2765,5,12],"1/8"],[["S",2789,3,8],"1/8"],[["S",2791,3,8],"1/8"],[["M",2792,8],"1/4"],[["S",2792,0,4],"1/8"],[["S",2792,1,4],"1/2"],[["S",2793,2,8],"1/8"],[["S",2794,0,4],"1/4"],[["S",2794,4,10],"1/4"],[["S",2795,4,10],"1/4"],[["S",2797,8,12],"1/4"],[["S",2799,8,12],"1/8"],[["M",3586,7],"1/8"],[["S",3586,2,8],"1/16"],[["S",3590,4,7],"1/16"],[["S",3606,6,7],"1/16"],[["S",3634,0,2],"1/16"],[["S",3638,6,8],"1/16"],[["S",3652,0,4],"1/8"],[["S",3652,1,4],"1/8"],[["S",3654,0,4],"1/16"],[["S",3660,5,7],"1/16"],[["M",3668,0],"1/8"],[["S",3684,1,4],"1/16"],[["S",3692,4,7],"1/16"],[["S",3754,0,4],"1/4"],[["S",3770,0,12],"1/8"],[["S",3894,0,3],"1/16"],[["S",3902,0,12],"1/16"],[["S",3958,7,12],"1/16"],[["S",7854,0,4],"1/8"],[["S",7870,6,8],"1/8"]]},{"name":"K33","points":6,"edges":[[0,3],[0,4],[0,5],[1,3],[1,4],[1,5],[2,3],[2,4],[2,5]],"lower_bound":"7","certificate":[[["M",0,0],"218/229"],[["M",0,6],"120/229"],[["S",0,0,3],"109/229"],[["M",9,10],"109/229"],[["M",64,7],"120/229"],[["M",65,9],"14/229"],[["S",65,4,11],"14/229"],[["M",66,13],"53/229"],[["S",66,4,11],"53/229"],[["M",74,4],"12/229"],[["S",74,0,12],"4/229"],[["S",74,7,13],"12/229"],[["S",74,13,14],"10/229"],[["S",75,7,10],"2/229"],[["S",75,12,13],"2/229"],[["M",82,14],"58/229"],[["S",82,0,10],"2/229"],[["M",83,12],"10/229"],[["M",192,11],"124/229"],[["S",192,0,5],"4/229"],[["S",193,1,5],"2/229"],[["S",193,9,13],"2/229"],[["S",195,8,9],"2/229"],[["M",200,8],"113/229"],[["S",200,0,10],"45/229"],[["S",200,8,11],"39/229"],[["S",200,9,11],"15/229"],[["S",201,8,9],"45/229"],[["S",202,4,12],"2/229"],[["S",202,5,9],"2/229"],[["S",202,5,10],"8/229"],[["S",203,5,13],"2/229"],[["S",218,8,9],"2/229"],[["M",224,9],"68/229"],[["S",224,9,11],"72/229"],[["S",225,1,3],"2/229"],[["S",451,3,4],"2/229"],[["M",457,1],"4/229"],[["M",457,10],"25/229"],[["M",640,6],"43/229"],[["S",640,2,5],"43/229"],[["M",641,2],"45/229"],[["S",641,1,8],"5/229"],[["S",641,5,6],"47/229"],[["S",641,6,11],"4/229"],[["S",641,11,13],"4/229"],[["S",641,12,13],"52/229"],[["S",643,12,13],"5/229"],[["S",644,3,10],"33/229"],[["M",645,10],"45/229"],[["S",650,6,14],"2/229"],[["S",652,5,6],"45/229"],[["S",654,5,6],"2/229"],[["M",676,6],"101/229"],[["S",677,6,10],"45/229"],[["S",686,6,10],"2/229"],[["M",704,2],"43/229"],[["S",705,4,8],"65/229"],[["S",705,8,11],"5/229"],[["S",706,2,5],"45/229"],[["S",707,3,5],"2/229"],[["M",708,11],"8/229"],[["S",708,3,8],"2/229"],[["S",713,1,12],"45/229"],[["S",714,12,13],"24/229"],[["S",715,12,13],"47/229"],[["S",716,0,12],"2/229"],[["S",717,4,8],"2/229"],[["S",722,2,11],"8/229"],[["M",740,10],"101/229"],[["M",896,6],"68/229"],[["M",896,12],"68/229"],[["S",896,10,14],"12/229"],[["S",897,1,13],"5/229"],[["S",898,4,14],"8/229"],[["S",904,2,10],"18/229"],[["S",904,12,13],"106/229"],[["S",908,0,13],"8/229"],[["S",909,10,13],"8/229"],[["S",912,6,11],"101/229"],[["S",912,10,11],"5/229"],[["S",912,12,13],"4/229"],[["S",914,3,10],"4/229"],[["S",914,6,12],"4/229"],[["S",920,12,14],"10/229"],[["S",922,0,13],"4/229"],[["S",923,12,13],"4/229"],[["S",961,1,4],"2/229"],[["S",965,1,3],"2/229"],[["S",967,4,14],"2/229"],[["S",973,1,4],"2/229"],[["S",979,3,13],"2/229"],[["S",983,3,10],"2/229"],[["S",1856,0,3],"4/229"],[["S",1856,2,3],"8/229"],[["S",1857,7,13],"5/229"],[["M",1868,7],"8/229"],[["S",1873,7,12],"8/229"],[["S",1874,3,13],"1/229"],[["S",1874,13,14],"23/229"],[["M",1876,11],"23/229"],[["S",1876,5,7],"5/229"],[["S",1882,11,14],"44/229"],[["M",1904,2],"5/229"],[["S",1993,2,5],"3/229"],[["S",1999,4,12],"2/229"],[["M",2017,2],"131/229"],[["S",2017,12,14],"6/229"],[["M",4992,6],"68/229"],[["S",4993,1,4],"4/229"],[["S",4993,1,13],"9/229"],[["S",4993,4,6],"68/229"],[["S",4993,10,14],"25/229"],[["S",4995,6,10],"23/229"],[["S",5002,2,10],"27/229"],[["S",5002,6,10],"45/229"],[["S",5006,10,14],"27/229"],[["S",5010,0,13],"4/229"],[["S",5019,6,14],"4/229"],[["S",5388,6,13],"2/229"],[["M",5440,11],"4/229"],[["S",5440,0,1],"16/229"],[["S",5441,2,4],"25/229"],[["S",5442,0,13],"21/229"],[["S",5442,11,14],"109/229"],[["S",5445,3,13],"3/229"],[["S",5445,4,9],"22/229"],[["S",5446,11,14],"10/229"],[["S",5450,4,9],"25/229"],[["S",5452,0,13],"2/229"],[["S",5453,9,11],"5/229"],[["S",5459,7,14],"25/229"],[["S",5459,9,14],"2/229"],[["S",5459,11,14],"2/229"],[["M",5461,9],"3/229"],[["S",5575,5,9],"2/229"],[["S",5577,5,9],"6/229"],[["S",5577,9,11],"19/229"],[["S",5579,11,14],"10/229"],[["S",5609,1,13],"33/229"],[["M",6016,6],"20/229"],[["S",6016,1,5],"4/229"],[["S",6017,1,13],"33/229"],[["S",6017,2,5],"34/229"],[["S",6019,5,6],"59/229"],[["S",6020,11,14],"25/229"],[["S",6021,4,11],"4/229"],[["S",6026,0,11],"25/229"],[["S",6026,2,6],"26/229"],[["S",6026,4,11],"6/229"],[["S",6026,11,14],"39/229"],[["S",6027,2,5],"4/229"],[["S",6027,2,6],"10/229"],[["S",6027,11,14],"11/229"],[["S",6028,1,5],"57/229"],[["S",6030,5,6],"34/229"],[["S",6030,11,13],"125/229"],[["S",6031,5,6],"14/229"],[["S",6044,6,11],"61/229"],[["S",6053,3,4],"18/229"],[["S",6053,4,11],"5/229"],[["S",6061,1,14],"8/229"],[["S",6061,11,13],"14/229"],[["S",6091,11,14],"19/229"],[["S",6109,1,5],"2/229"],[["S",7556,0,3],"101/229"],[["S",7556,4,6],"8/229"],[["S",7557,3,4],"31/229"],[["S",7557,3,13],"78/229"],[["S",7557,4,6],"2/229"],[["S",7561,1,2],"8/229"],[["S",7563,2,4],"4/229"],[["S",7563,2,6],"4/229"],[["S",7573,3,5],"33/229"],[["S",7579,2,5],"37/229"],[["S",7607,3,13],"37/229"],[["S",7621,3,13],"35/229"],[["S",7623,3,4],"4/229"],[["S",7625,2,9],"19/229"],[["S",7639,3,13],"5/229"],[["S",7641,1,2],"29/229"],[["S",7643,5,13],"29/229"],[["S",7667,2,9],"83/458"],[["S",7667,13,14],"167/458"],[["S",7671,3,13],"73/458"],[["S",7675,2,9],"1/458"],[["S",7675,13,14],"131/458"],[["S",8139,2,4],"19/229"],[["S",8155,5,13],"19/229"],[["S",8187,13,14],"61/229"],[["S",15242,2,5],"11/229"],[["S",15242,2,6],"5/229"],[["S",15243,4,6],"8/229"],[["S",15243,5,6],"3/229"],[["S",15259,2,5],"8/229"],[["S",15263,5,6],"8/229"],[["S",15327,5,10],"121/458"]]}]} diff --git a/research/star-pattern-degree-three-floor/derive_certificates.py b/research/star-pattern-degree-three-floor/derive_certificates.py new file mode 100644 index 0000000000..99615d6deb --- /dev/null +++ b/research/star-pattern-degree-three-floor/derive_certificates.py @@ -0,0 +1,112 @@ +"""Derive the rational dual certificates (needs numpy and scipy; not registered). + +Solves the symmetry-reduced Shannon-type linear program for each graph, rounds +the dual to rationals and keeps it only if the exact check in star_graphs +accepts it. The registered verifier never imports this file. +""" +import json +import sys +from fractions import Fraction +from pathlib import Path + +import numpy as np +from scipy.optimize import linprog +from scipy.sparse import coo_matrix + +sys.path.insert(0, str(Path(__file__).resolve().parent)) +import star_graphs as sg # noqa: E402 + +GRAPHS = { + "wheel-W4": (5, [(0, 1), (0, 2), (0, 3), (0, 4), (1, 2), (2, 3), (3, 4), (4, 1)]), + "K33": (6, [(a, b) for a in range(3) for b in range(3, 6)]), +} +# Not certified: the float optimum is 7.0 but the rounded dual is rejected by the +# exact check, so the prism is solved only when named on the command line. +UNCERTIFIED = { + "prism": (6, [(0, 1), (1, 2), (2, 0), (3, 4), (4, 5), (5, 3), (0, 3), (1, 4), (2, 5)]), +} +MAX_DENOMINATOR = 10 ** 6 + + +def orbit_representatives(nbrs, group): + """Map every closed set to the least member of its orbit.""" + total = len(nbrs) + closure = [sg.close(mask, nbrs) for mask in range(1 << total)] + rep = {} + for mask in sorted(set(closure)): + if mask not in rep: + orbit = {sg.image(perm, mask) for perm in group} + least = min(orbit) + for member in orbit: + rep[member] = least + return closure, rep + + +def reduced_rows(nbrs, closure, rep): + """Distinct orbit-space rows of the M and S inequalities.""" + total = len(nbrs) + identity = list(range(total)) + rows = {} + for base in sorted(set(rep.values())): + free = [v for v in range(total) if not (base >> v) & 1] + entries = [["M", base, v] for v in free] + entries += [["S", base, i, j] for i in free for j in free if i < j] + for entry in entries: + terms, constant = sg.certificate_terms(entry, identity) + row = {} + for mask, sign in terms: + key = rep[closure[mask]] + row[key] = row.get(key, 0) + sign + row = {key: value for key, value in row.items() if value} + if row: + rows.setdefault((tuple(sorted(row.items())), constant), entry) + return rows + + +def solve(n, edges): + """Return (float optimum, rational certificate) for one graph.""" + nbrs = sg.neighbour_masks(n, edges) + total = len(nbrs) + group = sg.vertex_permutations(n, edges) + closure, rep = orbit_representatives(nbrs, group) + rows = reduced_rows(nbrs, closure, rep) + column = {mask: i for i, mask in enumerate(sorted(set(rep.values())))} + keys = list(rows) + r_idx, c_idx, data = [], [], [] + for r, (items, _) in enumerate(keys): + for mask, value in items: + r_idx.append(r) + c_idx.append(column[mask]) + data.append(-value) + a_ub = coo_matrix((data, (r_idx, c_idx)), shape=(len(keys), len(column))).tocsr() + b_ub = np.array([-constant for _, constant in keys], float) + cost = np.zeros(len(column)) + cost[column[rep[closure[0]]]] = 1 + a_eq = coo_matrix(([1.0], ([0], [column[(1 << total) - 1]])), shape=(1, len(column))).tocsr() + result = linprog(cost, A_ub=a_ub, b_ub=b_ub, A_eq=a_eq, b_eq=[total], + bounds=(None, None), method="highs-ds") + sg.require(result.status == 0, result.message) + duals = -result.ineqlin.marginals + certificate = [] + for r, key in enumerate(keys): + if duals[r] > 1e-10: + weight = Fraction(float(duals[r])).limit_denominator(MAX_DENOMINATOR) + certificate.append([rows[key], str(weight)]) + return float(result.fun), certificate + + +def main(out_path, names): + records = [] + for name in names: + n, edges = {**GRAPHS, **UNCERTIFIED}[name] + value, certificate = solve(n, edges) + bound = sg.certified_bound(n, edges, certificate) + print(name, "float optimum", value, "exact bound", bound, "entries", len(certificate)) + records.append({"name": name, "points": n, "edges": [list(e) for e in edges], + "lower_bound": str(bound), "certificate": certificate}) + Path(out_path).write_text(json.dumps({"schema_version": 1, "graphs": records}, + separators=(",", ":")) + "\n") + + +if __name__ == "__main__": + main(sys.argv[1], sys.argv[2:] or list(GRAPHS)) diff --git a/research/star-pattern-degree-three-floor/star_graphs.py b/research/star-pattern-degree-three-floor/star_graphs.py new file mode 100644 index 0000000000..0d50b1eda0 --- /dev/null +++ b/research/star-pattern-degree-three-floor/star_graphs.py @@ -0,0 +1,172 @@ +"""Star-configuration graphs G_Gamma and the exact dual-certificate arithmetic. + +Standard library only. Vertices of G_Gamma are numbered: points 0..n-1 (the +vertices of Gamma), then pair n+e for the e-th listed edge of Gamma. A point is +adjacent to the pairs containing it, two pairs are adjacent iff they are +disjoint, and two points are never adjacent (the definition of PR #7114, +section 8). Vertex sets are bit masks. +""" +from fractions import Fraction +from itertools import permutations + +MAX_POINTS = 6 +MAX_VERTICES = 15 + + +class CheckError(ValueError): + """A certificate or graph failed an exact check.""" + + +def require(condition, message): + """Raise CheckError unless condition holds (active under -O as well).""" + if not condition: + raise CheckError(str(message)) + + +def check_gamma(n, edges): + """Reject anything but a simple graph on points 0..n-1 within the size caps.""" + require(1 <= n <= MAX_POINTS, n) + require(n + len(edges) <= MAX_VERTICES, (n, len(edges))) + seen = set() + for a, b in edges: + require(0 <= a < n and 0 <= b < n and a != b, (a, b)) + key = frozenset((a, b)) + require(key not in seen, (a, b)) + seen.add(key) + return seen + + +def neighbour_masks(n, edges): + """Return the neighbour mask of every vertex of G_Gamma.""" + check_gamma(n, edges) + total = n + len(edges) + masks = [0] * total + for e, (a, b) in enumerate(edges): + for point in (a, b): + masks[point] |= 1 << (n + e) + masks[n + e] |= 1 << point + for f, (c, d) in enumerate(edges): + if f != e and len({a, b, c, d}) == 4: + masks[n + e] |= 1 << (n + f) + return masks + + +def close(mask, nbrs): + """Decoding closure: add every vertex whose neighbours all lie in the set.""" + total = len(nbrs) + current = mask + for _ in range(total + 1): + grown = current + for v in range(total): + if not (current >> v) & 1 and (nbrs[v] & ~current) == 0: + grown |= 1 << v + if grown == current: + return current + current = grown + raise CheckError("closure did not stabilise") + + +def vertex_permutations(n, edges): + """Permutations of G_Gamma induced by the automorphisms of Gamma.""" + edge_index = {frozenset(e): i for i, e in enumerate(edges)} + require(len(edge_index) == len(edges), "check failed") + found = [] + for p in permutations(range(n)): + images = [edge_index.get(frozenset((p[a], p[b]))) for a, b in edges] + if None not in images: + found.append(list(p) + [n + i for i in images]) + require(found and found[0] == list(range(n + len(edges))), "check failed") + return found + + +def image(perm, mask): + """Image of a vertex set under a vertex permutation.""" + out = 0 + for v, w in enumerate(perm): + if (mask >> v) & 1: + out |= 1 << w + return out + + +def certificate_terms(entry, perm): + """One certificate entry, moved by perm, as (coefficients, right-hand side). + + ["M", S, v] : f(S) - f(S+v) >= -1 (a vertex adds at most one) + ["S", S, i, j] : f(S+i) + f(S+j) - f(S+i+j) - f(S) >= 0 (submodularity) + Both hold for every vertex set S and vertices outside S, so the moved entry + is a valid inequality whether or not perm is an automorphism. + """ + kind, base = entry[0], image(perm, entry[1]) + moved = [perm[v] for v in entry[2:]] + require(len(set(moved)) == len(moved), "check failed") + for v in moved: + require(not (base >> v) & 1, entry) + if kind == "M": + require(len(moved) == 1, entry) + return [(base, 1), (base | 1 << moved[0], -1)], -1 + require(kind == "S" and len(moved) == 2, entry) + i, j = moved + return [(base | 1 << i, 1), (base | 1 << j, 1), + (base | 1 << i | 1 << j, -1), (base, -1)], 0 + + +def certified_bound(n, edges, certificate): + """Exact lower bound on f(empty set) proved by a group-averaged certificate. + + Returns the bound, or raises CheckError if the nonnegative combination + does not reduce to f(closure of empty) - c f(V) >= rhs. + """ + nbrs = neighbour_masks(n, edges) + total = len(nbrs) + full = (1 << total) - 1 + group = vertex_permutations(n, edges) + cache = {} + coefficient = {} + rhs = Fraction(0) + for entry, text in certificate: + require(0 <= entry[1] <= full, entry) + require(all(0 <= v < total for v in entry[2:]), entry) + weight = Fraction(text) + require(weight > 0, (entry, text)) + share = weight / len(group) + for perm in group: + terms, constant = certificate_terms(entry, perm) + rhs += share * constant + for mask, sign in terms: + if mask not in cache: + cache[mask] = close(mask, nbrs) + key = cache[mask] + coefficient[key] = coefficient.get(key, Fraction(0)) + share * sign + empty = close(0, nbrs) + left = {key: value for key, value in coefficient.items() if value != 0} + require(left.get(empty) == 1, "coefficient of f(empty) is not 1") + require(set(left) <= {empty, full}, "certificate leaves other sets") + return rhs - left.get(full, Fraction(0)) * total + + +def gram_pattern(n, edges): + """Integer 1-block pattern of rank at most n+1 (PR #7114, Corollary 12). + + Labels in Z^(n+1) with the form diag(1,...,1,-1): x_c = e_c for a point and + x_T = e_c + e_d + e_last for a pair T = cd. Returns the Gram matrix. + """ + labels = [] + for c in range(n): + labels.append([1 if i == c else 0 for i in range(n + 1)]) + for a, b in edges: + labels.append([1 if i in (a, b, n) else 0 for i in range(n + 1)]) + form = [1] * n + [-1] + return [[sum(x[i] * form[i] * y[i] for i in range(n + 1)) for y in labels] + for x in labels] + + +def is_pattern(matrix, nbrs): + """Unit diagonal and zeros on non-adjacent pairs, as integers.""" + total = len(nbrs) + for a in range(total): + if matrix[a][a] != 1: + return False + for b in range(total): + if a != b and not (nbrs[a] >> b) & 1 and matrix[a][b] != 0: + return False + return True diff --git a/research/star-pattern-degree-three-floor/verify.py b/research/star-pattern-degree-three-floor/verify.py new file mode 100644 index 0000000000..12a74f0153 --- /dev/null +++ b/research/star-pattern-degree-three-floor/verify.py @@ -0,0 +1,177 @@ +"""Exact check of the degree-three star-pattern floors. Standard library only. + +For each listed graph Gamma on n points the script proves, in exact rational +arithmetic, that every function f on vertex sets of G_Gamma satisfying the +block-pattern rank laws (README, section 2) has f(empty) >= n + 1, and that an +integer pattern of rank at most n + 1 exists. It then runs rejecting controls. +""" +import json +import sys +from fractions import Fraction +from itertools import combinations, permutations +from pathlib import Path + +HERE = Path(__file__).resolve().parent +sys.path.insert(0, str(HERE)) +import star_graphs as sg # noqa: E402 + +GRAPHS = { + "wheel-W4": (5, [[0, 1], [0, 2], [0, 3], [0, 4], [1, 2], [2, 3], [3, 4], [4, 1]]), + "K33": (6, [[a, b] for a in range(3) for b in range(3, 6)]), +} +CYCLE_LENGTHS = (3, 4, 5, 6) + + +def degrees(n, edges): + """Degree of every point of Gamma.""" + count = [0] * n + for a, b in edges: + count[a] += 1 + count[b] += 1 + return count + + +def has_k4(n, edges): + """True if four points of Gamma are pairwise joined.""" + joined = {frozenset(e) for e in edges} + for quad in combinations(range(n), 4): + if all(frozenset(p) in joined for p in combinations(quad, 2)): + return True + return False + + +def rejected(action): + """True if action raises CheckError.""" + try: + action() + except sg.CheckError: + return True + return False + + +def check_graph(name, record): + """Lower bound, upper bound and hypotheses for one graph; return counts.""" + n, edges = GRAPHS[name] + sg.require(record["points"] == n and record["edges"] == edges, name) + certificate = record["certificate"] + sg.require(min(degrees(n, edges)) == 3, (name, "minimum degree")) + sg.require(not has_k4(n, edges), (name, "contains K4")) + bound = sg.certified_bound(n, edges, certificate) + sg.require(bound == n + 1, (name, bound)) + sg.require(Fraction(record["lower_bound"]) == bound, (name, "stored bound")) + nbrs = sg.neighbour_masks(n, edges) + sg.require(sg.is_pattern(sg.gram_pattern(n, edges), nbrs), (name, "Gram pattern")) + return n, len(nbrs), len(sg.vertex_permutations(n, edges)), len(certificate) + + +def certificate_controls(name, record): + """Each damaged certificate or graph must be rejected; return the count.""" + n, edges = GRAPHS[name] + certificate = record["certificate"] + first_entry, first_weight = certificate[0] + doubled = [[first_entry, str(2 * Fraction(first_weight))]] + certificate[1:] + negated = [[first_entry, str(-Fraction(first_weight))]] + certificate[1:] + joined = {frozenset(e) for e in edges} + spare = next(list(p) for p in combinations(range(n), 2) if frozenset(p) not in joined) + damaged = [ + lambda: sg.certified_bound(n, edges, certificate[1:]), + lambda: sg.certified_bound(n, edges, certificate[:-1]), + lambda: sg.certified_bound(n, edges, doubled), + lambda: sg.certified_bound(n, edges, negated), + lambda: sg.certified_bound(n, edges[:-1], certificate), + lambda: sg.certified_bound(n, edges[:-1] + [spare], certificate), + ] + for index, action in enumerate(damaged): + sg.require(rejected(action), (name, "control accepted", index)) + return len(damaged) + + +def pattern_control(name): + """Dropping one adjacency between disjoint pairs must break the Gram pattern.""" + n, edges = GRAPHS[name] + nbrs = sg.neighbour_masks(n, edges) + matrix = sg.gram_pattern(n, edges) + for a in range(n, len(nbrs)): + for b in range(a + 1, len(nbrs)): + if (nbrs[a] >> b) & 1: + cut = list(nbrs) + cut[a] &= ~(1 << b) + cut[b] &= ~(1 << a) + sg.require(not sg.is_pattern(matrix, cut), (name, "pattern control")) + return 1 + raise sg.CheckError((name, "no adjacent pairs")) + + +def cycle_pattern_rank(length): + """Rank-n integer pattern on G_{C_n}: one point-pair clique per point.""" + edges = [[i, (i + 1) % length] for i in range(length)] + nbrs = sg.neighbour_masks(length, edges) + sg.require(min(degrees(length, edges)) == 2, length) + total = len(nbrs) + matrix = [[0] * total for _ in range(total)] + for c in range(length): + clique = (c, length + c) + sg.require((nbrs[c] >> (length + c)) & 1, (length, c)) + for a in clique: + for b in clique: + matrix[a][b] += 1 + sg.require(sg.is_pattern(matrix, nbrs), (length, "cycle pattern")) + points = range(length) + sg.require(all(not (nbrs[a] >> b) & 1 for a in points for b in points), length) + return length + + +def contains(n, joined, pattern_points, pattern_edges): + """True if the pattern graph embeds in the graph with edge set joined.""" + for chosen in permutations(range(n), pattern_points): + if all(frozenset((chosen[a], chosen[b])) in joined for a, b in pattern_edges): + return True + return False + + +def small_graph_census(n): + """Labelled graphs on n points of minimum degree >= 3: all contain K4 or W4. + + Returns (number of such graphs, number containing K4, number containing W4). + """ + slots = list(combinations(range(n), 2)) + wheel_points, wheel_edges = GRAPHS["wheel-W4"] + k4_edges = list(combinations(range(4), 2)) + found = with_k4 = with_wheel = 0 + for code in range(1 << len(slots)): + edges = [slots[i] for i in range(len(slots)) if (code >> i) & 1] + if min(degrees(n, edges)) < 3: + continue + joined = {frozenset(e) for e in edges} + k4 = contains(n, joined, 4, k4_edges) + wheel = n >= wheel_points and contains(n, joined, wheel_points, wheel_edges) + sg.require(k4 or wheel, (n, edges)) + found += 1 + with_k4 += k4 + with_wheel += wheel + return found, with_k4, with_wheel + + +def main(): + data = json.loads((HERE / "certificates.json").read_text()) + sg.require(data["schema_version"] == 1, "schema") + records = {record["name"]: record for record in data["graphs"]} + sg.require(set(records) == set(GRAPHS), sorted(records)) + controls = 0 + for name in GRAPHS: + n, total, group, entries = check_graph(name, records[name]) + controls += certificate_controls(name, records[name]) + pattern_control(name) + print(f"PASS {name}: n={n} vertices={total} automorphisms={group} " + f"entries={entries} lower={n + 1} upper={n + 1}") + cycles = [cycle_pattern_rank(length) for length in CYCLE_LENGTHS] + print(f"PASS cycles {cycles}: rank-n patterns at minimum degree 2") + census = {n: small_graph_census(n) for n in (4, 5)} + sg.require(census == {4: (1, 1, 0), 5: (26, 11, 26)}, census) + print(f"PASS census (graphs, with K4, with W4) of minimum degree >= 3: {census}") + print(f"PASS_STAR_PATTERN_DEGREE_THREE_FLOOR graphs={len(GRAPHS)} " + f"controls={controls} cycles={len(cycles)} census={census[4][0] + census[5][0]} " + f"no_new_kappa") + + +if __name__ == "__main__": + main()