From 339bfb5cc26185104984afd4647e5c1edeb11d8f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Krzysztof=20W=C3=B3jt?= <97155365+krzysztofwojt@users.noreply.github.com> Date: Fri, 23 Oct 2026 15:09:58 +0200 Subject: [PATCH] Classify the six-cycle branch of fifteen-owner equality --- research/centre-equality-six-cycles/PROOF.md | 197 +++++++++++++++ research/centre-equality-six-cycles/README.md | 104 ++++++++ .../centre-equality-six-cycles/SOURCES.json | 24 ++ research/centre-equality-six-cycles/TASK.json | 97 ++++++++ .../centre-equality-six-cycles/VERIFY.json | 43 ++++ .../centre-equality-six-cycles/WITNESS.json | 16 ++ .../centre-equality-six-cycles/independent.py | 222 +++++++++++++++++ .../literal_check.py | 200 +++++++++++++++ research/centre-equality-six-cycles/verify.py | 232 ++++++++++++++++++ 9 files changed, 1135 insertions(+) create mode 100644 research/centre-equality-six-cycles/PROOF.md create mode 100644 research/centre-equality-six-cycles/README.md create mode 100644 research/centre-equality-six-cycles/SOURCES.json create mode 100644 research/centre-equality-six-cycles/TASK.json create mode 100644 research/centre-equality-six-cycles/VERIFY.json create mode 100644 research/centre-equality-six-cycles/WITNESS.json create mode 100644 research/centre-equality-six-cycles/independent.py create mode 100644 research/centre-equality-six-cycles/literal_check.py create mode 100644 research/centre-equality-six-cycles/verify.py diff --git a/research/centre-equality-six-cycles/PROOF.md b/research/centre-equality-six-cycles/PROOF.md new file mode 100644 index 0000000000..3dc3d23cb6 --- /dev/null +++ b/research/centre-equality-six-cycles/PROOF.md @@ -0,0 +1,197 @@ +# The six-cycle case at fifteen owners + +This is a written reduction to a finite exact enumeration, together with an +explicit counterexample that can be verified without trusting the reduction. +It is not a proof-kernel formalization. All graphs below are finite and simple. + +## 1. Statement and inherited boundary + +**Theorem.** Let G be a cubic bipartite graph with parts B and D of size 15. +Suppose G has no four-cycle and each vertex belongs to at most one simple +six-cycle. If G contains a six-cycle, then G is isomorphic, by a map preserving +the two parts, to the graph in [WITNESS.json](WITNESS.json). That graph has +exactly four six-cycles, and they are vertex disjoint. In particular, the +possible numbers of six-cycles are exactly **0 and 4**. + +The existence assertion at zero uses the duad/perfect-matching graph already +given by Sagar Thakrar in PR3291. This package makes no new uniqueness claim +for the zero-six-cycle case. + +This answers Nick Petalas's PR5182 question at its original boundary. His +cubic reduction and vertex-disjointness argument show that the theorem applies +to equality in PR3291: minimum degree at least three, |B|=15, no C4, and +c6(d)<=1 at degree three, c6(d)<=floor(deg(d)^2/4) otherwise. To make the +dependency explicit, PR3291's local bound is |B|>=5 deg(d)-c6(d). For +4<=deg(d)<=15 its lower bound exceeds 15, so D is cubic. If a B vertex +had degree at least four, rooting at a neighboring D vertex would produce +at least fourteen third-level incidences; at most one collision can save a +vertex, requiring |B|>=3+14-1=16. Hence B is cubic and |D|=15. Two C6s +sharing a B vertex would share an incident edge, and therefore a D vertex, +contradicting its cap. These observations are credited predecessor results, +not claimed as new here. No connectedness assumption is needed. + +## 2. The forced neighborhood of a six-cycle + +Fix one C6. Label its B vertices b0,b1,b2 and its D vertices d0,d1,d2, +so that bi is adjacent to dj exactly when i differs from j. Indices in this +proof belong to {0,1,2}. A repeated index is not a summation convention. + +Write yi for the third D neighbor of bi, and xi for the third B neighbor +of di. These six vertices lie outside the C6: adding the missing bi-di +edge would create a C4. The three yi are distinct; if yi=yj, then bi and +bj would share that neighbor and the third cycle vertex dk, giving a C4. +The same reasoning makes the xi distinct. + +There is **no edge xi-yj**. If i differs from j, such an edge closes the +four-cycle xi-di-bj-yj-xi. If i=j, take the two other indices k,l. The +path xi-di-bk-dl-bi-yi-xi would be a second C6 through a vertex of the +fixed cycle. Both alternatives violate a hypothesis. + +Let Ui be the two remaining D neighbors of xi, and Vi the two remaining +B neighbors of yi. They are outside the cycle and its six external neighbors. +The Ui are pairwise disjoint. A vertex u in Ui intersect Uj, for i!=j, +would give the second cycle xi-u-xj-dj-bk-di-xi, where k is the third index. +Similarly, the Vi are pairwise disjoint. + +Thus each part is partitioned into three cycle vertices, three external +neighbors, six vertices in the three pairs, and three remaining vertices. +Call the remaining sets F_B and F_D, each of size three. + +## 3. The only remaining edges + +There are no edges from Vi to Uj for i!=j. Such an edge v-u would complete +the second cycle bi-yi-v-u-xj-dj-bi through the fixed cycle. + +The edges between Vi and Ui form a matching: two Vi vertices already share +yi, and two Ui vertices already share xi, so a vertex with two neighbors +in the opposite pair would create a C4. Let its size be s_i, at most two. +It is at least one. If s_i were zero, the two Vi vertices would need four +distinct neighbors in F_D: two each, with disjoint sets to avoid a C4 +through yi. But |F_D|=3. Therefore + + s_i in {1,2}. + +After independently labeling each pair, these matching edges are +v_i0-u_i0, and also v_i1-u_i1 when s_i=2. The remaining neighborhoods +of v_i0,v_i1 in F_D are disjoint and have sizes: + +| s_i | v_i0 | v_i1 | Number of assignments to labeled F_D | +|---|---|---|---| +| 1 | one vertex | the other two vertices | 3 | +| 2 | one vertex | a different vertex | 6 | + +Exactly the same alternatives hold for the neighbors of u_i0,u_i1 in F_B. +All other unfinished edges lie in F_B x F_D. There the only remaining +choices are the Boolean 3-by-3 matrices satisfying the residual degrees. +Every entry of the whole graph has now been specified or enumerated. + +Some such completions still have C4s or excessive C6s. They are retained +until the final literal graph predicates; the reduction does not assume that +all parameter choices are admissible. + +## 4. Complete finite domain and symmetry reduction + +The verifier uses the following labels on each side: + +| Role | B label | D label | +|---|---|---| +| cycle | bi=i | di=i | +| external | xi=3+i | yi=3+i | +| pair | v_ik=6+2i+k | u_ik=6+2i+k | +| remaining | 12,13,14 | 12,13,14 | + +Permuting the three indices simultaneously on both sides preserves the fixed +cycle and sorts (s0,s1,s2). The four possibilities, in the order used by the +primary checker, are (2,2,2), (1,2,2), (1,1,2), and (1,1,1). Independent +permutations of F_D and F_B put the first pair's attachments in the first +option displayed by `attachment_options`: for s0=1, vertex 0 versus vertices +1,2; for s0=2, vertex 0 versus vertex 1. These relabelings do not constrain +any other unenumerated edge. Pair labels were chosen to put their matching +on the diagonal. Consequently **every admissible graph with a chosen C6 has +at least one enumerated representative**. Uniqueness of representatives is +not assumed. + +`verify.py` enumerates all remaining attachments and all 512 Boolean free +blocks, retaining precisely those whose residual row and column sums fit. +It checks cubic degrees, all row-pair intersections for C4s, and every triple +of B vertices for C6s. In a C4-free graph each B pair has at most one common +D neighbor; a B triple forms a C6 exactly when its three common neighbors +exist and are distinct. Equal common neighbors form a claw, not a cycle. +Every six-cycle has exactly one B triple, so this procedure is exhaustive. + +The finite result is: + +| (s0,s1,s2) | Attachment pairs | Cubic completions | C4-free | Admissible | +|---|---:|---:|---:|---:| +| (2,2,2) | 1296 | 2176 | 496 | 0 | +| (1,2,2) | 1296 | 1728 | 816 | 16 | +| (1,1,2) | 324 | 324 | 112 | 0 | +| (1,1,1) | 81 | 81 | 4 | 0 | + +These 16 survivors all have four six-cycles. The ordered, sorted list of +their incidence-row bit masks, serialized by the exact compact JSON command +in the checker, has SHA256 +`436a29a84656b5b0e2d172e0c3c1a58077e877935d59d0e7a2a772ddecf57b3e`. +The digest records the result; it does not replace enumeration. + +## 5. One isomorphism class + +All 16 survivors are explicitly obtained from WITNESS.json using independent +choices of the following four involutions: + +1. Exchange B13 and B14. +2. Exchange D13 and D14. +3. Exchange B8 with B9 and D8 with D9 simultaneously. +4. Exchange B10 with B11 and D10 with D11 simultaneously. + +`witness_orbit` applies all 16 choices and compares the entire resulting +incidence-matrix set with the entire survivor set. These are explicit maps, +not an assumed graph-isomorphism heuristic. They establish the claimed single +isomorphism class containing a C6. Together with the exhaustive coverage +argument above, this proves the theorem by a finite computation. + +## 6. A counterexample independently of classification + +The witness's four C6s have B/D vertex sets + + {0,1,2}, {4,8,9}, {5,10,11}, {7,13,14} + +on each side. Its other vertices are {3,6,12} on each side. Direct checks +show a connected cubic graph with 45 edges, no C4, and precisely these four +C6s. The four sets are disjoint, so every vertex satisfies the cap. This +alone disproves girth-eight rigidity, even if a reader has not accepted the +normal-form coverage or the isomorphism classification. + +For comparison with PR5182, its integer defect E=C C^T C-4C-J has twelve +entries +1, twelve entries -1 and 201 zeros. The positive entries join +opposite vertices on a C6; the negative entries join different C6s. Both +supports are partial matchings on the 12 cycle vertices per side, and +E C^T is symmetric. These checks specialize the predecessor's necessary +identity to a realized nonzero defect; they do not constitute a new proof +of that identity. + +## 7. Separate checks and limits + +`independent.py` enumerates all eight labeled matching-size patterns and all +attachments, without sorting the patterns or fixing either free-side labeling. +It uses the adjacency fourth-moment identity for C4s and length-three path +counts for C6s. It finds 134,469 cubic completions, 42,948 C4-free cases and +432 admissible cases, all with four C6s. There are 144 survivors in each of +(1,2,2), (2,1,2), (2,2,1). Literal cycle walks corroborate every survivor. +This separately evaluates the supplied normal-form family; the universal +coverage still comes from Sections 2–4, not from two agreeing programs. + +`literal_check.py` independently checks the witness by all-root simple-path +DFS and integer matrix multiplication. It also checks the classical zero-C6 +duad/perfect-matching example and meaningful rejection controls. Separate AI +implementations are not independent human review. + +Neither the abstract witness nor its classification assigns the actual +selected routes or solves scalar coefficient equations. The fifteen-owner +floor is unchanged. The result prevents deleting the six-cycle branch from +a future actual-route search; it does not provide a physical repair saving, +a complete paid invoice, a supplier, a new kappa or an integer-multiplication +theorem. No claim of literature priority for this abstract graph is made. + +Prepared for Krzysztof Wójt with substantial OpenAI Codex assistance; Apache-2.0. +Exact predecessor references and attribution are in README.md and TASK.json. diff --git a/research/centre-equality-six-cycles/README.md b/research/centre-equality-six-cycles/README.md new file mode 100644 index 0000000000..5c83138baa --- /dev/null +++ b/research/centre-equality-six-cycles/README.md @@ -0,0 +1,104 @@ +# Fifteen-owner equality can have four six-cycles + +**A finite graph classification with a written coverage proof; no new kappa.** + +The fifteen-owner equality hypotheses do **not** force girth eight. +[WITNESS.json](WITNESS.json) gives a connected cubic bipartite graph on 15+15 +vertices with no four-cycles and exactly four vertex-disjoint six-cycles. +Moreover, every graph under these hypotheses containing a six-cycle is +isomorphic to this witness. Thus the possible six-cycle counts are exactly +**0 and 4**; counts 2, 3 and 5 do not occur. The known zero-cycle example +retains predecessor credit; its uniqueness is not a new claim here. + +This resolves the explicit remaining question in Nick Petalas's +[PR5182](https://github.com/CrocSwap/integer-mult-bounds/pull/5182), whose +structural result excluded one six-cycle but left counts 2–5 open. The +[released handoff](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19145292) +and our [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/3062#discussioncomment-19145989) +record the scope. Future actual-route searches cannot discard the six-cycle +case on the basis of these abstract hypotheses alone. + +## Proof and exact evidence + +[PROOF.md](PROOF.md) gives the complete reduction around a distinguished C6. +Three matching sizes in {1,2}, six small attachment choices and a free 3-by-3 +Boolean block specify every possible graph with a C6. Relabeling reduces +the domain to 2,997 attachment patterns and 4,309 cubic completions. Exactly +1,428 are C4-free and 16 meet the C6 cap. Sixteen explicitly listed vertex +permutations identify the entire survivor set with one witness. + +Two separately implemented checks corroborate the computation: + +- `independent.py` keeps all eight matching-size patterns and every free-side + labeling: 91,125 attachment patterns, 134,469 cubic completions, 42,948 + C4-free graphs and 432 admissible labeled graphs. Every survivor has four + C6s and receives a literal cycle-walk check. It uses adjacency-walk counts + rather than the primary triple-intersection predicate. +- `literal_check.py` checks the displayed witness by all-root simple-path + DFS, including exact cycles, disjointness, connectedness and the nonzero + signed defect from PR5182. It also checks the predecessor's classical + duad/perfect-matching positive control and malformed, omitted-cycle, + omitted-root and degree-preserving-switch controls. + +The universal coverage rests on the written reduction. Program agreement +alone is not a completeness argument. The explicit counterexample is +independently checkable even without accepting the classification proof. +Substantial AI assistance, including separate Luna supporting implementations, +is disclosed; no independent human or proof-kernel review is claimed. + +## Reproduce + +Python 3.12, standard library only, from the repository root: + +```sh +python3.12 -W error -B scripts/research_package.py --package research/centre-equality-six-cycles +``` + +The manifest runs all three standalone verifiers in ordinary and optimized +mode. Each prints deterministic JSON and writes no files. Expected markers +include `PASS_CENTRE_EQUALITY_SIX_CYCLES` and the runner's +`PASS_REGISTERED_RESEARCH_PACKAGE`. The same three scripts run directly in a +Git-free export. Publication-byte, source-history, export and mutation-check +evidence is recorded in the PR; CI execution is separate from scientific +acceptance. There are no network or third-party solver dependencies. + +## Scope, sources and credit + +This is a scoped override of the `centre-path-sharing` card to its abstract +equality obstruction. The original card, selected context and exact base +`ec2780e8aeb1c88acaf5e9e470ef8c68e7fbbb6c` are retained in +[TASK.json](TASK.json) and [SOURCES.json](SOURCES.json), priority revision 7. +The mathematical predecessor files are cited provenance, not imported +executables or replayed censuses. No frozen package is modified. + +| Predecessor | Exact head | Retained contribution | +|---|---|---| +| Sagar Thakrar, [#3291](https://github.com/CrocSwap/integer-mult-bounds/pull/3291) | `5d027c3c8724aec4501e0e2876388bebefa00ef7` | Sharp abstract fifteen-owner floor, local path inequality and duad example; `research/centre-block-moore-bound/PROOF.md` | +| Nick Petalas, [#5182](https://github.com/CrocSwap/integer-mult-bounds/pull/5182) | `a4a8956cb9c769cddd593d00b4c294d307b5fac5` | Cubic equality reduction, disjoint cycles, signed defect and exclusion of one C6; `research/centre-fifteen-owner-equality/PROOF.md` | + +PR5182's proof was inspected at SHA256 +`c73687ff86616e90db6828726745e6dcc22bfffeca6fcec0d728958f5b9dc9c4`. +It is an explicit citation; the cited Git commit is not a runtime dependency. +Also retain Matarener #3656, dcharb78 #3147, Ross Richardson #3071, +Gonzalo Mier #3097, Sudarsh Chaturvedi #3168, Aaron Wang/navinor, ywz65 and +their original selected-source lineage. The new work is the realized +six-cycle example and complete classification of the nonzero-cycle branch, +not a re-audit of their route censuses, lower bounds or physical models. + +Actual route labels and scalar coefficient equations remain unconstructed. +Acquisition, routing, arbitrary dirty restoration, frames, hosting, precision, +stock, recursive costs, all-size compilation and outer transfer remain +outside this result. There is no supplier-admission, new-kappa or +selected-frontier claim. No literature priority for the abstract graph is +asserted. Prepared for Krzysztof Wójt with substantial OpenAI Codex assistance; +Apache-2.0, with predecessor attribution retained. + +## Open next questions + +Can the displayed graph with four six-cycles carry the actual selected route labels +and scalar coefficient equations? It is now a necessary second branch beside +the zero-cycle incidence. A first step is to impose the exact six-edge route +relations on these four cycles and the remaining edges, then solve the +coefficient compatibility equations. The graph alone does not satisfy those +contracts, and a physical construction needs a complete favorable cost and +restoration budget before expansion. This task is unreserved. diff --git a/research/centre-equality-six-cycles/SOURCES.json b/research/centre-equality-six-cycles/SOURCES.json new file mode 100644 index 0000000000..12f6c2b842 --- /dev/null +++ b/research/centre-equality-six-cycles/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "base_commit": "ec2780e8aeb1c88acaf5e9e470ef8c68e7fbbb6c", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395", + "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/centre-block-moore-bound/PROOF.md", + "usage": "provenance", + "git_blob": "57e4adae5ab6247d7f82fefc2d91abccdb4bd39a", + "sha256": "4ff55b8d7c32f4ad2e32e267fd3e3340003b580dfa709577016eb605f157e137" + } + ] +} diff --git a/research/centre-equality-six-cycles/TASK.json b/research/centre-equality-six-cycles/TASK.json new file mode 100644 index 0000000000..ffea117abd --- /dev/null +++ b/research/centre-equality-six-cycles/TASK.json @@ -0,0 +1,97 @@ +{ + "schema_version": 1, + "task_id": "centre-path-sharing", + "priority_revision": 7, + "base_commit": "ec2780e8aeb1c88acaf5e9e470ef8c68e7fbbb6c", + "original_card": { + "id": "centre-path-sharing", + "question": "Can the 64-per-call centre path (eight rank-8 COPY/ERASE totals through the private temporary) be shared across calls or shrunk?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/complex-local-word-ceiling/README.md", + "research/split-centres-global/proofs/PR386-BIT-GEOMETRY.txt", + "certificates/selected-result.json" + ], + "methods": [ + "Derive a fully charged favorable relaxation for sharing one centre path across k calls, including restoration, hosting and precision.", + "Prove a lower bound on copied information per call for the selected decoder contract." + ], + "acceptance_gate": "Show the changed centre charge and copy profile per call with every added restoration or hosting cost charged, and its ceiling via ceiling.ceiling(centre=...). 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", + "research/complex-local-word-ceiling/verify.py" + ], + "expected": "PASS_COMPLEX_LOCAL_WORD_CEILING", + "inspect": "Read the selected word's per-call local profile, its packing ceiling and the lever table; run levers.py for the ideal budget of the lever you target.", + "scope": "Positive control and planning budget only; this is not a new construction or full cold replay." + }, + "first_experiment": "Write the per-call centre charge and copy children for sharing across k = 2 calls, charge the sharing overhead, and screen it; stop this route if even the ideal sharing gains under 10%. Ideal budgets: free 2.80x, shared by two 1.90x (levers.py).", + "bottleneck_link": "The centre path consumes 64 of about 99.6 unpaid coordinates per call, i.e. about 64% of the raw deficit.", + "allowed_variations": [ + "One sharing pattern across a fixed number of calls.", + "One reduced copied-total contract for the existing decoder.", + "If the coverage law, template or guard changes, derive an applicable fully charged replacement bound instead of applying the incumbent ceiling outside its scope." + ], + "scope_change_triggers": [ + "Removing copies without a replacement contract for the decoder's copied totals.", + "Continuing a partial cost improvement while leaving the same unpriced consumer, restoration or central-readout obligation unresolved; refresh the family expansion decision first. Local product-retiming evidence has a narrow scope and is not a ban on changed graphs or contracts." + ], + "overlap_terms": [ + "centre path", + "copied totals", + "private temporary", + "shared centre", + "batching" + ] + }, + "scope_status": "changed", + "actual_scope": "Classify the graphs containing a six-cycle under the cubic 15+15, C4-free and per-vertex C6-cap-one equality hypotheses; decide the two-through-five-cycle question released in PR5182.", + "scope_change_reason": "The handoff-first process identified PR5182's explicit unreserved equality question. This is an abstract incidence obstruction relevant to centre repair, not a proposed paid centre-path improvement.", + "bottleneck_link": "The witness with four six-cycles prevents restricting actual fifteen-owner route-label searches to girth eight. The complete nonzero-cycle classification supplies one concrete graph to test; no physical savings or supplier admission follow.", + "budget_minutes": 240, + "stop_rule": "Stop after resolving the abstract six-cycle branch. No wider physical construction or cost optimization is reserved. Failed heuristic searches are not exclusions.", + "outcome": "completed", + "evidence": "Written rooted-neighborhood coverage proof; 4309 reduced cubic completions, 16 explicit isomorphic survivors; separate unreduced 134469-completion walk-count check with 432 survivors; literal DFS witness, signed-defect checks and rejection controls. All survivors have four C6s. Validation status and exact publication head are recorded in the PR.", + "author": "Krzysztof W\u00f3jt", + "ai_assistance": "Substantial OpenAI Codex assistance for research, proof, implementation, verification and writing; Luna supporting agents separately implemented the unreduced enumeration and literal graph checker. This is not independent human or formal proof-kernel review.", + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/3062#discussioncomment-19145989", + "upstream_checkpoint": { + "commit": "ff3cc58e370d0f678e529246f8c73e8094e18fcf", + "checked_at": "2026-10-23T13:17:18Z", + "priority_revision": 7, + "decision": "Continue on the pinned scientific base. Guidance, task catalogue and selected record are unchanged; the exact cited PR5182 was merged, and the new package has no path collision. Live overlap freshness is recorded in the PR and canonical status." + }, + "preclaim_overlap": { + "open_prs": 334, + "open_prs_fetched_at": "2026-10-23T12:47:20.578244+00:00", + "discussion_records": 4438, + "discussions_fetched_at": "2026-10-23T12:48:27.232074+00:00", + "local_head_notes": 6996, + "complete_remote_pagination": true, + "scope": "Read exact released PR5182 handoff, current PR5182/3147 bodies, all-state targeted PR searches and recent krzysztofwojt claims. No competing equality-classification claim was found. Unpublished work and arbitrary historical diffs are outside coverage." + }, + "predecessors": [ + { + "pr": 3291, + "author": "Sagar Thakrar", + "head": "5d027c3c8724aec4501e0e2876388bebefa00ef7", + "contribution": "Local path inequality, sharp fifteen-owner floor and zero-C6 duad/perfect-matching example." + }, + { + "pr": 5182, + "author": "Nick Petalas", + "head": "a4a8956cb9c769cddd593d00b4c294d307b5fac5", + "contribution": "Cubic equality reduction, vertex-disjoint cycles, signed defect and exclusion of one C6; exact source cited without runtime import." + } + ], + "open_questions": [ + { + "question": "Can the four-six-cycle witness carry the actual selected route labels and scalar coefficient equations?", + "why_it_matters": "It is the unique nonzero-six-cycle abstract equality branch, so actual-route searches cannot discard it solely by the graph hypotheses.", + "first_step": "Impose the exact six-edge route relations on the four displayed cycles and remaining edges, then test coefficient compatibility.", + "blocked_by": "No route labeling or coefficient solution is supplied. Before a physical construction, require a favorable complete cost and dirty-restoration budget." + } + ] +} diff --git a/research/centre-equality-six-cycles/VERIFY.json b/research/centre-equality-six-cycles/VERIFY.json new file mode 100644 index 0000000000..4c4c82b85f --- /dev/null +++ b/research/centre-equality-six-cycles/VERIFY.json @@ -0,0 +1,43 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-W", "error", "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Complete reduced rooted family, all C4/C6 predicates, explicit witness isomorphisms and rejection controls." + }, + { + "argv": ["{python}", "-O", "-W", "error", "-B", "{package}/verify.py"], + "timeout_seconds": 120, + "checks": "The same full reduced classification with optimization enabled." + }, + { + "argv": ["{python}", "-W", "error", "-B", "{package}/independent.py"], + "timeout_seconds": 120, + "checks": "Unreduced eight-pattern enumeration using walk counts, all 432 survivors checked by literal DFS, witness and controls." + }, + { + "argv": ["{python}", "-O", "-W", "error", "-B", "{package}/independent.py"], + "timeout_seconds": 120, + "checks": "The same full unreduced enumeration with optimization enabled." + }, + { + "argv": ["{python}", "-W", "error", "-B", "{package}/literal_check.py"], + "timeout_seconds": 120, + "checks": "Independent literal witness and duad cycles, signed defect, malformed and omitted-cycle controls." + }, + { + "argv": ["{python}", "-O", "-W", "error", "-B", "{package}/literal_check.py"], + "timeout_seconds": 120, + "checks": "The same standalone literal graph checks with optimization enabled." + } + ] +} diff --git a/research/centre-equality-six-cycles/WITNESS.json b/research/centre-equality-six-cycles/WITNESS.json new file mode 100644 index 0000000000..2ae845076c --- /dev/null +++ b/research/centre-equality-six-cycles/WITNESS.json @@ -0,0 +1,16 @@ +{ + "schema_version": 1, + "description": "Rows B0..B14 list their neighbors in D0..D14. Both parts are distinct.", + "rows": [ + [1, 2, 3], [0, 2, 4], [0, 1, 5], [0, 6, 7], [1, 8, 9], + [2, 10, 11], [3, 6, 12], [3, 13, 14], [4, 8, 12], [4, 9, 13], + [5, 10, 12], [5, 11, 14], [6, 9, 11], [7, 8, 14], [7, 10, 13] + ], + "six_cycles": [ + {"B": [0, 1, 2], "D": [0, 1, 2]}, + {"B": [4, 8, 9], "D": [4, 8, 9]}, + {"B": [5, 10, 11], "D": [5, 10, 11]}, + {"B": [7, 13, 14], "D": [7, 13, 14]} + ], + "cycle_free_vertices": {"B": [3, 6, 12], "D": [3, 6, 12]} +} diff --git a/research/centre-equality-six-cycles/independent.py b/research/centre-equality-six-cycles/independent.py new file mode 100644 index 0000000000..14a1e0aa02 --- /dev/null +++ b/research/centre-equality-six-cycles/independent.py @@ -0,0 +1,222 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +# Copyright 2026 Krzysztof Wójt; substantial assistance from OpenAI Codex and Luna. +"""Finite evaluation of the supplied labeled family only; no global coverage claim.""" +from __future__ import annotations +import hashlib, json, time +from itertools import product +from pathlib import Path + +N, FREE = 15, (12, 13, 14) +PATTERNS = tuple(product((1, 2), repeat=3)) +EXPECTED = { + (1,1,1):(729,729,693,36,36,0), (1,1,2):(2916,2916,1908,1008,1008,0), + (1,2,1):(2916,2916,1908,1008,1008,0), (1,2,2):(11664,15552,8208,7344,7200,144), + (2,1,1):(2916,2916,1908,1008,1008,0), (2,1,2):(11664,15552,8208,7344,7200,144), + (2,2,1):(11664,15552,8208,7344,7200,144), (2,2,2):(46656,78336,60480,17856,17856,0), +} + +def require(ok, message): + if not ok: + raise RuntimeError(message) + +def pair_options(s_i): + if s_i == 1: + # The diagonal leaf needs one free neighbor; its mate needs two. + return tuple(((x,), tuple(y for y in FREE if y != x)) for x in FREE) + if s_i == 2: + # Preserve ordered leaf labels and choose distinct free labels. + return tuple(((x,), (y,)) for x in FREE for y in FREE if x != y) + raise ValueError(s_i) + +def fixed_rows(s): + rows = [set() for _ in range(N)] + def add(b, d): + require(d not in rows[b], ("duplicate fixed edge", b, d)); rows[b].add(d) + for i in range(3): + for j in range(3): + if i != j: add(i, j) + add(i, 3+i); add(3+i, i) + for k in range(2): + leaf = 6+2*i+k; add(3+i, leaf); add(leaf, 3+i) + for i, s_i in enumerate(s): + for k in range(s_i): + leaf = 6+2*i+k; add(leaf, leaf) + return tuple(tuple(sorted(row)) for row in rows) + +def matrix_index(): + index = {} + for mask in range(1 << 9): + rd = tuple(sum((mask >> (3*i+j)) & 1 for j in range(3)) for i in range(3)) + cd = tuple(sum((mask >> (3*i+j)) & 1 for i in range(3)) for j in range(3)) + index.setdefault((rd, cd), []).append(mask) + return index + +MATRIX_INDEX = matrix_index() + +def assemble_rows(base, b_attach, d_attach, mask): + rows = [list(row) for row in base] + for b, ds in b_attach.items(): rows[b].extend(ds) + for d, bs in d_attach.items(): + for b in bs: rows[b].append(d) + for i in range(3): + for j in range(3): + if (mask >> (3*i+j)) & 1: rows[12+i].append(12+j) + rows = tuple(tuple(sorted(row)) for row in rows) + require(all(len(r) == 3 and len(set(r)) == 3 for r in rows), "B cubic/simplicity") + cols = [0]*N + for row in rows: + for d in row: cols[d] += 1 + require(cols == [3]*N, "D cubic degree") + return rows + +def adjacency(rows): + adj = [[] for _ in range(2*N)] + for b, ds in enumerate(rows): + for d in ds: adj[b].append(N+d); adj[N+d].append(b) + return tuple(tuple(sorted(ns)) for ns in adj) + +def c4_by_trace(adj): + # For a simple graph, tr(A^4)=2m+4*sum_v C(deg(v),2)+8*C4. + trace = 0 + for v in range(len(adj)): + walks2 = {} + for u in adj[v]: + for w in adj[u]: walks2[w] = walks2.get(w, 0)+1 + trace += sum(x*x for x in walks2.values()) + m = sum(map(len, adj))//2 + baseline = 2*m + 4*sum(len(ns)*(len(ns)-1)//2 for ns in adj) + numerator = trace-baseline + require(numerator >= 0 and numerator % 8 == 0, ("trace(A^4) identity", trace, baseline)) + return numerator//8 + +def c6_by_length3_paths(rows): + # In a C4-free bipartite graph, distinct simple 3-paths between opposite + # nonneighbors are internally disjoint; choose(p3,2) counts C6s at each + # endpoint, which has a unique antipode. Call only after the C4 check. + d_to_b = [[] for _ in range(N)] + for b, ds in enumerate(rows): + for d in ds: d_to_b[d].append(b) + rowsets = [set(ds) for ds in rows]; p3 = [[0]*N for _ in range(N)] + for b, ds in enumerate(rows): + for d0 in ds: + for b1 in d_to_b[d0]: + if b1 != b: + for d1 in rows[b1]: + if d1 != d0 and d1 not in rowsets[b]: p3[b][d1] += 1 + through_b, through_d = [0]*N, [0]*N + for b in range(N): + for d in range(N): + if d not in rowsets[b]: + k = p3[b][d]; q = k*(k-1)//2 + through_b[b] += q; through_d[d] += q + tb, td = sum(through_b), sum(through_d) + require(tb == td and tb % 3 == 0, ("C6 antipode totals", tb, td)) + return tuple(through_b+through_d), tb//3 + +def literal_cycles(adj, length): + found = set() + for start in range(len(adj)): + path, used = [start], {start} + def visit(): + cur = path[-1] + if len(path) == length: + if start in adj[cur]: + fwd = tuple(path); rev = (start,)+tuple(reversed(path[1:])) + found.add(min(fwd, rev)) + return + for nxt in adj[cur]: + if nxt <= start or nxt in used: continue + used.add(nxt); path.append(nxt); visit(); path.pop(); used.remove(nxt) + visit() + return found + +def cycle_incidence(cycles): + counts = [0]*(2*N) + for cycle in cycles: + for v in cycle: counts[v] += 1 + return tuple(counts) + +def run_controls(witness): + c4rows = [[] for _ in range(N)]; c4rows[0], c4rows[1] = [0,1], [0,1] + a = adjacency(c4rows) + require(c4_by_trace(a) == 1 and len(literal_cycles(a, 4)) == 1, "planted C4 control") + # Two 6-cycles share B0, so its incidence must be two and C4 count zero. + overlap = [[] for _ in range(N)] + overlap[0] = [0,2,3,5] + overlap[1], overlap[2], overlap[3], overlap[4] = [0,1], [1,2], [3,4], [4,5] + a = adjacency(overlap); pi, pc = c6_by_length3_paths(overlap); cycles = literal_cycles(a, 6) + require(c4_by_trace(a) == 0 and pc == 2 and max(pi) == 2, "overlap C6 path control") + require(len(cycles) == 2 and cycle_incidence(cycles) == pi, "overlap C6 DFS control") + raw = witness.get("rows") + require(isinstance(raw, list) and len(raw) == N, "witness rows schema") + rows = tuple(tuple(sorted(r)) for r in raw) + require(all(len(r) == 3 and len(set(r)) == 3 for r in rows), "witness cubic rows") + declared = witness.get("six_cycles") + require(isinstance(declared, list) and len(declared) == 4, "witness declares four C6s") + a = adjacency(rows); pi, pc = c6_by_length3_paths(rows); cycles = literal_cycles(a, 6) + require(c4_by_trace(a) == 0 and pc == 4 and len(cycles) == 4, "witness C6 count") + require(cycle_incidence(cycles) == pi, "witness C6 incidence disagreement") + return rows, {"planted_c4":1, "overlap_c6s":2, "witness_c6s":len(cycles)} + +def main(): + witness = json.loads(Path(__file__).with_name("WITNESS.json").read_text(encoding="utf-8")) + witness_rows, controls = run_controls(witness) + witness_key = tuple(tuple(sorted(r)) for r in witness_rows); witness_seen = False + started = time.monotonic() + totals = dict(attachments=0, graphs=0, c4_rejected=0, c4_free=0, multi_c6_rejected=0) + winners, pattern_results, seen = [], [], set() + for s in PATTERNS: + if time.monotonic()-started > 240: raise TimeoutError("enumeration exceeded four minutes") + bo, do = tuple(pair_options(x) for x in s), tuple(pair_options(x) for x in s) + item = dict(s=list(s), attachments=0, graphs=0, c4_rejected=0, c4_free=0, + multi_c6_rejected=0, winners=0) + digest = hashlib.sha256(); base = fixed_rows(s) + for bchoices in product(*bo): + for dchoices in product(*do): + item["attachments"] += 1; totals["attachments"] += 1 + ba, da, rr, cc = {}, {}, [3]*3, [3]*3 + for i, pair in enumerate(bchoices): + for k, ds in enumerate(pair): + ba[6+2*i+k] = ds + for d in ds: cc[d-12] -= 1 + for i, pair in enumerate(dchoices): + for k, bs in enumerate(pair): + da[6+2*i+k] = bs + for b in bs: rr[b-12] -= 1 + require(min(rr+cc) >= 0 and sum(rr) == sum(cc), ("residual degrees", s)) + for mask in MATRIX_INDEX.get((tuple(rr), tuple(cc)), ()): + rows = assemble_rows(base, ba, da, mask); item["graphs"] += 1; totals["graphs"] += 1 + adj = adjacency(rows) + if c4_by_trace(adj): + item["c4_rejected"] += 1; totals["c4_rejected"] += 1; continue + item["c4_free"] += 1; totals["c4_free"] += 1 + incidence, count = c6_by_length3_paths(rows) + if max(incidence) > 1: + item["multi_c6_rejected"] += 1; totals["multi_c6_rejected"] += 1; continue + require(count == 4, ("admitted C6 count", s, count)) + key = tuple(tuple(r) for r in rows) + require(key not in seen, ("duplicate labeled graph", s)); seen.add(key) + witness_seen |= key == witness_key + digest.update(json.dumps(rows, separators=(",", ":")).encode("ascii")+b"\n") + item["winners"] += 1; winners.append((s, rows, adj, incidence, count)) + observed = tuple(item[k] for k in ("attachments", "graphs", "c4_rejected", "c4_free", "multi_c6_rejected", "winners")) + require(observed == EXPECTED[s], ("per-pattern count drift", s, observed, EXPECTED[s])) + item["rows_sha256"] = digest.hexdigest(); pattern_results.append(item) + require(totals == dict(attachments=91125, graphs=134469, c4_rejected=91521, c4_free=42948, + multi_c6_rejected=42516), ("global count drift", totals)) + require(len(winners) == 432 and len(seen) == 432, "winner total/uniqueness drift") + require(witness_seen, "WITNESS rows absent from admitted winners") + for s, rows, adj, incidence, count in winners: + cycles = literal_cycles(adj, 6) + require(len(cycles) == count and cycle_incidence(cycles) == incidence, ("literal DFS mismatch", s)) + result = {"marker":"PASS finite supplied-family evaluation", + "scope":"Explicit labeled normal-form family only; no global coverage claim.", + "per_pattern":pattern_results, + "totals":{**totals, "winners":len(winners), "literal_dfs_winners":len(winners)}, + "witness":{"canonical_rows_admitted":witness_seen, "literal_c6_count":controls["witness_c6s"]}, + "controls":controls} + print(json.dumps(result, sort_keys=True, separators=(",", ":"))) + +if __name__ == "__main__": + main() diff --git a/research/centre-equality-six-cycles/literal_check.py b/research/centre-equality-six-cycles/literal_check.py new file mode 100644 index 0000000000..aa18694204 --- /dev/null +++ b/research/centre-equality-six-cycles/literal_check.py @@ -0,0 +1,200 @@ +#!/usr/bin/env python3 +# Copyright 2026 Krzysztof Wójt +# Licensed under the Apache License, Version 2.0. +# Prepared with substantial OpenAI Codex and Luna assistance. +# Predecessor attribution is retained in the package README. +"""Independent literal-DFS verifier for WITNESS.json; standard library only.""" +from collections import Counter +from hashlib import sha256 +from itertools import combinations +import json +from pathlib import Path + +ROWS = ( + (1,2,3),(0,2,4),(0,1,5),(0,6,7),(1,8,9),(2,10,11),(3,6,12),(3,13,14), + (4,8,12),(4,9,13),(5,10,12),(5,11,14),(6,9,11),(7,8,14),(7,10,13), +) +C6 = frozenset({ + (0,16,2,15,1,17),(4,23,8,19,9,24), + (5,25,10,20,11,26),(7,28,14,22,13,29), +}) +C6_SETS = frozenset((tuple(sorted(v for v in c if v < 15)), + tuple(sorted(v-15 for v in c if v >= 15))) for c in C6) +FREE = {"B": (3,6,12), "D": (3,6,12)} + +def need(ok, msg): + if not ok: + raise RuntimeError(msg) +def digest(x): + return sha256(json.dumps(x, sort_keys=True, separators=(",", ":")).encode()).hexdigest() +def valid(rows): + if type(rows) is not list or len(rows) != 15: + return False + cols = [0]*15 + for row in rows: + if type(row) is not list or len(row) != 3: + return False + if any(type(d) is not int or not 0 <= d < 15 for d in row) or len(set(row)) != 3: + return False + for d in row: + cols[d] += 1 + return cols == [3]*15 +def graph(rows): + a = [[] for _ in range(30)] + for b, ds in enumerate(rows): + for d in ds: + a[b].append(15+d); a[15+d].append(b) + return tuple(tuple(sorted(x)) for x in a) +def canon(path): + p = tuple(path) + return min(q[i:]+q[:i] for q in (p, tuple(reversed(p))) for i in range(len(q))) +def cycles(adj, length, roots=None): + found = set() + for start in range(len(adj)) if roots is None else roots: + def dfs(path, used): + if len(path) == length: + if start in adj[path[-1]]: + found.add(canon(path)) + return + for v in adj[path[-1]]: + if v != start and v not in used: + dfs(path+(v,), used | {v}) + dfs((start,), {start}) + return found +def ncomponents(adj): + unseen, n = set(range(len(adj))), 0 + while unseen: + n += 1; todo = [unseen.pop()] + while todo: + for v in adj[todo.pop()]: + if v in unseen: + unseen.remove(v); todo.append(v) + return n +def mm(a, b): + bt = tuple(zip(*b)) + return [[sum(x*y for x,y in zip(row,col)) for col in bt] for row in a] +def cycle_sets(found): + return frozenset((tuple(sorted(v for v in c if v < 15)), + tuple(sorted(v-15 for v in c if v >= 15))) for c in found) +def witness_sets(w): + items = w.get("six_cycles") + need(type(items) is list and len(items) == 4, "six_cycles must have four records") + out = [] + for item in items: + need(type(item) is dict and set(item) == {"B","D"}, "malformed cycle record") + sides = [] + for side in ("B","D"): + xs = item[side] + need(type(xs) is list and len(xs) == 3 + and all(type(x) is int and 0 <= x < 15 for x in xs) + and len(set(xs)) == 3, "malformed cycle labels") + sides.append(tuple(sorted(xs))) + out.append(tuple(sides)) + need(len(set(out)) == len(out), "duplicate witness cycle") + return frozenset(out) +def perfect_matchings(points): + points = tuple(points) + if not points: + yield () + return + x = points[0] + for y in points[1:]: + rest = tuple(z for z in points[1:] if z != y) + for tail in perfect_matchings(rest): + yield tuple(sorted(((x,y),)+tail)) +def duad_baseline(): + duads = tuple(combinations(range(6),2)) + synthemes = tuple(sorted(set(perfect_matchings(range(6))))) + rows = [[j for j,m in enumerate(synthemes) if d in m] for d in duads] + need(len(synthemes) == 15 and valid(rows), "bad duad fixture") + a = graph(rows); c4, c6, c8 = cycles(a,4), cycles(a,6), cycles(a,8) + need(ncomponents(a) == 1 and not c4 and not c6 and len(c8) == 90, + "duad baseline failed") + return {"duads":15,"synthemes":15,"components":1,"c4":0,"c6":0,"c8":90, + "c8_digest":digest(sorted(c8))} + +def run(): + p = Path(__file__).with_name("WITNESS.json") + raw = p.read_bytes(); w = json.loads(raw) + need(type(w.get("schema_version")) is int and w["schema_version"] == 1, + "unsupported witness schema") + rows = w.get("rows") + need(valid(rows) and tuple(tuple(r) for r in rows) == ROWS, "rows fail strict/exact checks") + a = graph(rows); need(ncomponents(a) == 1, "candidate disconnected") + c4, c6, c8 = cycles(a,4), cycles(a,6), cycles(a,8) + need(not c4 and c6 == C6 and cycle_sets(c6) == C6_SETS, "C4/C6 census mismatch") + need(witness_sets(w) == C6_SETS, "WITNESS six_cycles mismatch") + seen_b = {v for c in c6 for v in c if v < 15} + seen_d = {v-15 for c in c6 for v in c if v >= 15} + free = {"B":tuple(v for v in range(15) if v not in seen_b), + "D":tuple(v for v in range(15) if v not in seen_d)} + need(len(seen_b) == len(seen_d) == 12 and free == FREE, "C6 disjointness/free set mismatch") + listed = w.get("cycle_free_vertices") + need(type(listed) is dict and set(listed) == {"B","D"}, "bad cycle_free_vertices") + for side in ("B","D"): + xs = listed[side] + need(type(xs) is list and all(type(x) is int for x in xs) + and tuple(xs) == free[side], "listed cycle-free vertices mismatch") + c = [[int(d in row) for d in range(15)] for row in rows] + ct = [list(x) for x in zip(*c)] + e = [[x-4*c[i][j]-1 for j,x in enumerate(row)] for i,row in enumerate(mm(mm(c,ct),c))] + hist = Counter(x for row in e for x in row) + need(hist == Counter({-1:12,0:201,1:12}), "defect histogram mismatch") + q = mm(e,ct); need(q == [list(x) for x in zip(*q)], "E C^T not symmetric") + pos = {(i,j) for i,r in enumerate(e) for j,x in enumerate(r) if x == 1} + neg = {(i,j) for i,r in enumerate(e) for j,x in enumerate(r) if x == -1} + partial = lambda s: len(s) == len({i for i,_ in s}) == len({j for _,j in s}) == 12 + need(partial(pos) and partial(neg), "defect supports not partial matchings") + ix, px = {}, {} + for k,cyc in enumerate(sorted(c6)): + for z,v in enumerate(cyc): + ix[v],px[v] = k,z + need(all(ix[b] == ix[d+15] and (px[b]-px[d+15]) % 6 == 3 for b,d in pos), + "positive support not opposite in same C6") + need(all(ix[b] != ix[d+15] for b,d in neg), "negative support does not cross cycles") + + # Strict malformed-label controls; bool is deliberately not an integer ID. + boolean = [list(r) for r in ROWS]; boolean[0][0] = True + duplicate = [list(r) for r in ROWS]; duplicate[0] = [1,1,3] + bad_range = [list(r) for r in ROWS]; bad_range[0] = [1,2,15] + need(not valid(boolean) and not valid(duplicate) and not valid(bad_range), + "malformed-row control accepted") + + # Degree-preserving 2-switch: removes one C6 and creates four. + switched = [set(r) for r in ROWS] + switched[0].remove(1); switched[0].add(0) + switched[1].remove(0); switched[1].add(1) + switched = [sorted(r) for r in switched]; sa = graph(switched) + s4, s6 = cycles(sa,4), cycles(sa,6) + need(valid(switched) and ncomponents(sa) == 1 and not s4 and len(s6) == 7 + and len(s6-c6) == 4 and len(c6-s6) == 1, "edge-mutation control failed") + sample = min(c6) + need({canon(q[i:]+q[:i]) for q in (sample,tuple(reversed(sample))) for i in range(6)} == {sample} + and (c6-{sample}) != C6, "rotation/reversal or omitted-cycle control failed") + + # Two squares joined by a bridge: all roots find both; root 0 alone misses one. + small = [[] for _ in range(8)] + for u,v in ((0,1),(1,2),(2,3),(3,0),(4,5),(5,6),(6,7),(7,4),(3,4)): + small[u].append(v); small[v].append(u) + all4, root4 = cycles(small,4), cycles(small,4,roots=(0,)) + need(ncomponents(small) == 1 and len(all4) == 2 and len(root4) == 1 + and len(all4-root4) == 1, "omitted-root control failed") + baseline = duad_baseline() + + result = { + "marker":"CENTRE_EQUALITY_SIX_CYCLES_LITERAL_V1","status":"PASS", + "checks":{"cubic_connected":True,"c4":0,"c6":4,"girth":6, + "cycle_free_vertices":True,"defect_symmetric":True, + "positive_opposite_matching":12,"negative_cross_cycle_matching":12}, + "counters":{"vertices":30,"edges":45,"c8":len(c8), + "defect_histogram":{str(k):hist[k] for k in (-1,0,1)}, + "mutation_c6":len(s6),"root_control":[len(all4),len(root4)]}, + "sha256":{"witness":sha256(raw).hexdigest(),"rows":digest(rows), + "c6":digest(sorted(c6)),"defect":digest(e)}, + "duad_perfect_matching_baseline":baseline, + "dfs":"literal simple paths from every root; closing-edge test; all rotations/reversal canonicalized", + } + print(json.dumps(result,sort_keys=True,separators=(",",":"))) + +if __name__ == "__main__": + run() diff --git a/research/centre-equality-six-cycles/verify.py b/research/centre-equality-six-cycles/verify.py new file mode 100644 index 0000000000..6658461baa --- /dev/null +++ b/research/centre-equality-six-cycles/verify.py @@ -0,0 +1,232 @@ +#!/usr/bin/env python3 +"""Exact rooted classification; standard library, read-only, no Git required. + +Prepared for Krzysztof Wójt with substantial OpenAI Codex assistance. +Apache-2.0. The mathematical coverage argument is in PROOF.md. +""" +from collections import Counter, defaultdict +from hashlib import sha256 +from itertools import combinations, permutations, product +import json +from pathlib import Path + + +PACKAGE = Path(__file__).resolve().parent +EXPECTED = ((1296, 2176, 496, 0), (1296, 1728, 816, 16), + (324, 324, 112, 0), (81, 81, 4, 0)) + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def encode(rows): + require(len(rows) == 15, "exactly fifteen rows required") + result = [] + for row in rows: + require(isinstance(row, (list, tuple)) and len(row) == 3, + "each row needs three distinct neighbors") + require(all(type(d) is int and 0 <= d < 15 for d in row), + "neighbor outside the fifteen-vertex part") + require(len(set(row)) == 3, "duplicate edge") + result.append(sum(1 << d for d in row)) + require(all(sum((row >> d) & 1 for row in result) == 3 for d in range(15)), + "column degree differs from three") + return tuple(result) + + +def six_cycles(rows): + """All (B triple, D triple) cycles, or None if a C4 exists. + + In a C4-free graph each pair of B vertices has at most one common D + neighbor. A triple forms a C6 exactly when its three common neighbors + exist and are distinct. A single shared D neighbor is a claw, not C6. + """ + common = {} + for a, b in combinations(range(15), 2): + mask = rows[a] & rows[b] + if mask.bit_count() > 1: + return None + if mask: + common[a, b] = mask.bit_length() - 1 + cycles = [] + for a, b, c in combinations(range(15), 3): + ds = (common.get((a, b)), common.get((a, c)), common.get((b, c))) + if None not in ds and len(set(ds)) == 3: + cycles.append(((a, b, c), tuple(sorted(ds)))) + return tuple(cycles) + + +def cycle_cap(cycles): + memberships = Counter((side, v) for cycle in cycles + for side, vertices in enumerate(cycle) for v in vertices) + return all(count <= 1 for count in memberships.values()) + + +def attachment_options(size): + """Neighbor sets in the three free vertices for an ordered inner pair.""" + if size == 2: + return tuple(((a,), (b,)) for a, b in permutations(range(3), 2)) + require(size == 1, "diagonal matching must have size one or two") + return tuple(((a,), tuple(b for b in range(3) if b != a)) for a in range(3)) + + +def fixed_rows(sizes): + rows = [0] * 15 + for i, size in enumerate(sizes): + rows[i] = sum(1 << j for j in range(3) if i != j) | (1 << (3 + i)) + rows[3 + i] = (1 << i) | (3 << (6 + 2 * i)) + for k in range(2): + rows[6 + 2 * i + k] = 1 << (3 + i) + for k in range(size): + rows[6 + 2 * i + k] |= 1 << (6 + 2 * i + k) + return rows + + +def free_blocks(): + """Every 3x3 Boolean matrix, indexed by its row and column sums.""" + result = defaultdict(list) + for mask in range(1 << 9): + rows = tuple((mask >> (3 * i)) & 7 for i in range(3)) + key = (tuple(row.bit_count() for row in rows), + tuple(sum((row >> j) & 1 for row in rows) for j in range(3))) + result[key].append(rows) + require(sum(map(len, result.values())) == 512, "incomplete free-block family") + return result + + +def complete_rows(sizes, b_options, d_options, blocks): + rows = fixed_rows(sizes) + for i in range(3): + for k in range(2): + for j in b_options[i][k]: + rows[6 + 2 * i + k] |= 1 << (12 + j) + for j in d_options[i][k]: + rows[12 + j] |= 1 << (6 + 2 * i + k) + margins = (tuple(3 - rows[12 + j].bit_count() for j in range(3)), + tuple(3 - sum((r >> (12 + j)) & 1 for r in rows) for j in range(3))) + for block in blocks.get(margins, ()): + full = rows[:] + for j in range(3): + full[12 + j] |= block[j] << 12 + require(all(row.bit_count() == 3 for row in full), "row completion failed") + require(all(sum((r >> d) & 1 for r in full) == 3 for d in range(15)), + "column completion failed") + yield tuple(full) + + +def enumerate_rooted(): + blocks = free_blocks() + report, winners = [], [] + for singles in range(4): + sizes = (1,) * singles + (2,) * (3 - singles) + choices = [attachment_options(size) for size in sizes] + # Independent permutations of the three free vertices on each side + # put the first pair's attachment into the first displayed option. + choices[0] = choices[0][:1] + counts = Counter() + for b_options in product(*choices): + for d_options in product(*choices): + counts["attachment_patterns"] += 1 + for rows in complete_rows(sizes, b_options, d_options, blocks): + counts["cubic_completions"] += 1 + cycles = six_cycles(rows) + if cycles is None: + continue + counts["c4_free"] += 1 + if cycle_cap(cycles): + winners.append(rows) + counts["admitted"] += 1 + require(len(cycles) == 4, "unexpected admissible cycle count") + actual = tuple(counts[key] for key in + ("attachment_patterns", "cubic_completions", "c4_free", "admitted")) + require(actual == EXPECTED[singles], f"rooted enumeration drift: {sizes}: {actual}") + report.append({"matching_sizes": sizes, **dict(zip( + ("attachment_patterns", "cubic_completions", "c4_free", "admitted"), actual))}) + require([row["matching_sizes"] for row in report] == + [(2, 2, 2), (1, 2, 2), (1, 1, 2), (1, 1, 1)], + "a matching-size pattern was omitted") + require(len(winners) == len(set(winners)) == 16, "winner count or duplicate drift") + return report, tuple(winners) + + +def relabel(rows, b_map, d_map): + require(sorted(b_map) == sorted(d_map) == list(range(15)), "invalid relabeling") + out = [0] * 15 + for b, row in enumerate(rows): + out[b_map[b]] = sum(1 << d_map[d] for d in range(15) if (row >> d) & 1) + return tuple(out) + + +def witness_orbit(rows): + """Sixteen explicit isomorphisms; no graph-isomorphism oracle is used.""" + orbit = set() + for flags in product((0, 1), repeat=4): + b_map, d_map = list(range(15)), list(range(15)) + if flags[0]: + b_map[13], b_map[14] = b_map[14], b_map[13] + if flags[1]: + d_map[13], d_map[14] = d_map[14], d_map[13] + for flag, start in zip(flags[2:], (8, 10)): + if flag: + b_map[start], b_map[start + 1] = b_map[start + 1], b_map[start] + d_map[start], d_map[start + 1] = d_map[start + 1], d_map[start] + orbit.add(relabel(rows, b_map, d_map)) + return orbit + + +def rejects(action): + try: + action() + except ValueError: + return True + return False + + +def controls(witness, cycles, winners): + decoded = [[d for d in range(15) if (r >> d) & 1] for r in witness] + require(rejects(lambda: encode(decoded[:-1])), "missing-row control survived") + bad = [row[:] for row in decoded] + bad[0] = [1, 1, 3] + require(rejects(lambda: encode(bad)), "duplicate-edge control survived") + bad[0] = [1, 2, 15] + require(rejects(lambda: encode(bad)), "out-of-range control survived") + bad[0] = [1, 2, True] + require(rejects(lambda: encode(bad)), "Boolean-label control survived") + bad[0] = [1, 2, 4] + require(rejects(lambda: encode(bad)), "column-degree control survived") + require(not cycle_cap(cycles + cycles[:1]), "repeated-cycle control survived") + require(set(winners[:-1]) != witness_orbit(witness), "omitted-winner control survived") + bad_masks = list(witness) + bad_masks[1] = bad_masks[0] + require(six_cycles(bad_masks) is None, "C4 control survived") + require(all(bs != (0, 6, 7) for bs, _ in cycles), "claw counted as a cycle") + return 9 + + +def main(): + fixture = json.loads((PACKAGE / "WITNESS.json").read_text(encoding="utf-8")) + witness = encode(fixture["rows"]) + cycles = six_cycles(witness) + require(cycles is not None and cycle_cap(cycles), "witness violates the graph hypotheses") + expected_cycles = tuple((tuple(x["B"]), tuple(x["D"])) for x in fixture["six_cycles"]) + require(cycles == expected_cycles and len(cycles) == 4, "witness cycle list differs") + report, winners = enumerate_rooted() + require(witness_orbit(witness) == set(winners), "the explicit isomorphisms miss a winner") + control_count = controls(witness, cycles, winners) + encoded = json.dumps(sorted(winners), separators=(",", ":")).encode("ascii") + print(json.dumps({ + "status": "PASS_CENTRE_EQUALITY_SIX_CYCLES", + "classification": "Every admissible graph containing a C6 is isomorphic to WITNESS.json", + "proof_boundary": "Written rooted-normal-form coverage plus exact finite enumeration", + "normalized_counts": report, + "normalized_winner_sha256": sha256(encoded).hexdigest(), + "explicit_isomorphism_images": len(witness_orbit(witness)), + "witness_six_cycles": fixture["six_cycles"], + "controls": control_count, + }, sort_keys=True, indent=2)) + + +if __name__ == "__main__": + main()