From 9cdb8b7054ee780aa5fde1c45e2eaec98247be49 Mon Sep 17 00:00:00 2001 From: Cursor Agent Date: Mon, 9 Nov 2026 13:30:41 +0000 Subject: [PATCH] Bound the odd-character port window by 36. The P120 odd graph is strongly regular with parameters (120, 63, 30, 36). The matrix 3I-A has rank 36 over Q, and a degree-2 factorisation has rank 38 over F_3. No new kappa. Co-authored-by: unpaidmoon --- research/p104-odd-char-window/NOTICE | 4 + research/p104-odd-char-window/PROOF.md | 184 ++++++++ research/p104-odd-char-window/README.md | 85 ++++ research/p104-odd-char-window/SOURCES.json | 18 + research/p104-odd-char-window/TASK.json | 81 ++++ research/p104-odd-char-window/VERIFY.json | 18 + .../p104-odd-char-window/data/ports_p104.json | 109 +++++ research/p104-odd-char-window/verify.py | 397 ++++++++++++++++++ 8 files changed, 896 insertions(+) create mode 100644 research/p104-odd-char-window/NOTICE create mode 100644 research/p104-odd-char-window/PROOF.md create mode 100644 research/p104-odd-char-window/README.md create mode 100644 research/p104-odd-char-window/SOURCES.json create mode 100644 research/p104-odd-char-window/TASK.json create mode 100644 research/p104-odd-char-window/VERIFY.json create mode 100644 research/p104-odd-char-window/data/ports_p104.json create mode 100644 research/p104-odd-char-window/verify.py diff --git a/research/p104-odd-char-window/NOTICE b/research/p104-odd-char-window/NOTICE new file mode 100644 index 0000000000..92704b8e9b --- /dev/null +++ b/research/p104-odd-char-window/NOTICE @@ -0,0 +1,4 @@ +Odd-character window upper bound. +Prepared by unpaidmoon with substantial Cursor Grok assistance. +The port list is the P104 set published in PR #6933. +New exposition and checks are Apache-2.0. diff --git a/research/p104-odd-char-window/PROOF.md b/research/p104-odd-char-window/PROOF.md new file mode 100644 index 0000000000..179802f166 --- /dev/null +++ b/research/p104-odd-char-window/PROOF.md @@ -0,0 +1,184 @@ +# Odd-character window of the P120 odd graph + +No new κ. The selected value stays `781451/250000000`. This note bounds the +window of a port set from above. It does not build a word, a decoder, or a +paid profile. + +## 0. Definitions + +Let `P120` be the 120 vectors in `F_2^9` of weight 3 or 7 (weight congruent to +3 mod 4). Two distinct vectors are **adjacent** when their `F_2` dot product +is 1 and **orthogonal** when it is 0. The **odd graph** has those adjacencies +as edges. + +`P104` is the 104-vector subset stored in `data/ports_p104.json` (70 of weight +3 and 34 of weight 7). Its complement in `P120` has 16 vectors and exactly two +cliques of size 8. Each of those cliques, added to `P104`, is a 112-vector set +`P112`. These are the same sets as in PR #6933: the port file is byte-identical +to `research/p104-port-window-haemers/data/ports_p104.json` at head +`a967c521074c2c7450255ae237fda9c439ee1b35`, and the induced odd graph on `P104` +is 55-regular, as recorded there. + +A **1-block pattern** on a vertex set `S` is a matrix, indexed by `S`, with +nonzero diagonal and with a zero in both off-diagonal positions of every +orthogonal pair. Entries on adjacent pairs are free, and the matrix need not +be symmetric. Write `w_1(S; F)` for the minimum rank of a 1-block pattern over +`F`, and `w(S; F)` for the infimum of `rank(B)/k` over k-block patterns on `S` +in the sense of #6933. Then `w(S; F) ≤ w_1(S; F)` because the infimum includes +the case `k = 1`. The identification of this window with the fractional +Haemers bound is #6933, Theorem 1, and is not used below. + +## 1. Degree + +**Lemma 1.** Every vertex of the odd graph on `P120` has degree 63. + +*Proof.* There are `C(9,3) = 84` weight-3 vectors and `C(9,7) = 36` weight-7 +vectors. + +Let `u` have weight 3, and let `T` be the complementary 6-set. A weight-3 +neighbor meets `u` in one coordinate: 3 choices there and `C(6,2) = 15` in +`T`, so 45 neighbors. A weight-7 vector has a 2-set complement `s`. Its dot +with `u` is odd if and only if `|u ∩ s|` is even, because the two pieces +partition the three coordinates of `u`. The even possibilities are `|u ∩ s| = 0` +(`C(6,2) = 15` sets `s`) and `|u ∩ s| = 2` (`C(3,2) = 3` sets). That is 18 +neighbors. The degree is `45 + 18 = 63`. + +Let `u` have weight 7, with 2-set complement `t`. A weight-3 vector `v` has odd +dot with `u` if and only if `|v ∩ t|` is even. There are `C(7,3) = 35` such +`v` disjoint from `t`, and 7 that contain `t`. A different weight-7 vector has +2-set complement `s ≠ t`, and the same parity count used above shows that the +dot is odd if and only if `s` is disjoint from `t`. There are `C(7,2) = 21` +such 2-sets. The degree is `42 + 21 = 63`. ∎ + +`verify.py` recomputes both sides of this count and then enumerates every +vertex. + +## 2. Strongly regular parameters + +**Lemma 2.** The odd graph on `P120` is connected and strongly regular with +parameters `(n, k, λ, μ) = (120, 63, 30, 36)`. + +*Proof of the census.* `verify.py` counts common neighbors of every unordered +pair twice, once with bitsets and once with set intersection, and requires the +two counts to agree. The degree is constantly 63, adjacent pairs have exactly +30 common neighbors, and orthogonal pairs have exactly 36. A walk from vertex 0 +reaches all 120 vertices. ∎ + +The constant parameters are a complete finite enumeration, not a sample. The +hand argument of Lemma 1 covers only the degree. + +## 3. The rank-36 pattern + +Let `A` be the adjacency matrix and `J` the all-ones matrix. Lemma 2 is the +matrix identity + +``` +A^2 = k I + λ A + μ (J - I - A) = 27 I - 6 A + 36 J. +``` + +**Lemma 3.** `(A - 3I)(A + 9I)(A - 63I) = 0`, the three factors are pairwise +coprime over `Q`, and + +``` +dim ker(A - 63I) = 1, dim ker(A - 3I) = 84, dim ker(A + 9I) = 35. +``` + +*Proof.* The displayed square rearranges to `A^2 + 6A - 27I = 36 J`. The +scalar polynomial factors as `x^2 + 6x - 27 = (x - 3)(x + 9)`, since +`(-6)^2 + 4·27 = 144`. Right-multiplication by `A - 63I` kills `J`, because +`AJ = 63 J` by regularity, so + +``` +(A - 3I)(A + 9I)(A - 63I) = 0. +``` + +The linear factors are distinct over `Q`. If a matrix satisfies `fg(A) = 0` +with `gcd(f, g) = 1`, polynomials `a, b` with `af + bg = 1` split the space +into `ker f(A)` and `ker g(A)`. Applying that twice, `Q^{120}` is the direct +sum of the three kernels. The all-ones vector lies in `ker(A - 63I)`. If +`(A - 63I)x = 0`, every coordinate of `x` equals the average of its neighbors. +A coordinate of maximum value forces the same value on its neighbors, and +connectedness forces `x` to be constant. Thus that kernel is one-dimensional. + +Let `f = dim ker(A - 3I)` and `g = dim ker(A + 9I)`. Then `f + g = 119`. +The diagonal of `A` is zero, so `tr(A) = 0`, and that trace is +`3f - 9g + 63`. Equivalently `f - 3g = -21`. +Substitution gives `4g = 140`, so `g = 35` and `f = 84`. ∎ + +**Theorem 1.** Let `H = 3I - A`. Over `Q`, `H` has rank 36, diagonal 3, and +zeros on every orthogonal pair. For every field `F` of characteristic not 3, +the reduction of `H` is a 1-block pattern of rank at most 36. For every +nonempty `S ⊆ P120`, + +``` +w(S; F) ≤ w_1(S; F) ≤ 36. +``` + +*Proof.* `H = -(A - 3I)`, so Lemma 3 gives rank 36 over `Q`. The diagonal is 3 +and the off-diagonal support is the edge set. In characteristic not 3 the +diagonal remains nonzero, and rank cannot rise under reduction. A principal +submatrix is a 1-block pattern on its index set and has rank at most 36. ∎ + +`verify.py` checks that the reduction has rank exactly 36 modulo 5, 7, 11 and +10007, which matches the rational rank, and that a single planted orthogonal +entry is rejected. Modulo 3 the diagonal of `H` is 0, so this matrix is not a +pattern in characteristic 3. That control is the reason for the next section. + +In characteristic 2 the same reduction is a legal pattern of rank at most 36. +It does not improve the rank-9 Gram pattern already recorded for `P104`, +`P112` and `P120` in #6933. The new ceiling is the odd-character one. + +## 4. Characteristic 3 + +Index features of a vector `v` by the nine coordinates and the `C(9,2)` +coordinate products, evaluated in `{0,1}` and read in `F_3`. This is a +45-column matrix `Φ`. For each vertex `v`, the linear system + +``` +Φ_u · y = 1 if u = v, Φ_u · y = 0 if u is orthogonal to v, +``` + +with adjacent rows unconstrained and with free variables set to 0, has a +solution `y_v`. `verify.py` solves all 120 systems and substitutes the +solutions back into the equations. The matrix `M_uv = Φ_u · y_v` is therefore +a 1-block pattern over `F_3`, and `M = Φ Y^T` has rank at most 45. Gaussian +elimination gives rank exactly 38. + +**Theorem 2.** Over `F_3`, `w(S; F_3) ≤ w_1(S; F_3) ≤ 38` for every nonempty +`S ⊆ P120`. + +The nine linear coordinates alone do not solve these systems: all eight +sampled columns in `verify.py` are inconsistent. The quadratic coordinates are +part of this factorisation, not an unused pad. The same eight samples are not +a proof that no rank-36 pattern exists in characteristic 3. + +## 5. The interval, conditional on #6933 + +#6933, Theorem 4, states that in every characteristic other than 2, + +``` +w(P104; F) ≥ 13, w(P112; F) ≥ 14, w(P120; F) ≥ 15, +``` + +because `n/8` equals those three integers and the E8 root-line form has rank +at most 8. That argument is not replayed here. Accepting it, Theorems 1 and 2 +give + +| field | P104 | P112 | P120 | +|---|---|---|---| +| char ≠ 2, 3 | [13, 36] | [14, 36] | [15, 36] | +| char 3 | [13, 38] | [14, 38] | [15, 38] | + +#6933 already places the characteristic-2 window of `P104` in `[53/6, 9]` and +the characteristic-2 windows of `P112` and `P120` at exactly 9. Theorem 1 does +not narrow those characteristic-2 intervals. + +The lower bounds are not claimed for arbitrary subsets. #6933 exhibits a +14-port subset with a 2-block pattern of rank 17, ratio `17/2 < 9`. + +## 6. What this does not say + +The window is the block-mask quantity of #6933. That note already records that +a physical decoder for `k > 1` with exactly this mask is not derived. A rank-36 +pattern is not a multiplication algorithm, not a paid profile, and not a +change to the selected frontier. No human has reviewed this proof. diff --git a/research/p104-odd-char-window/README.md b/research/p104-odd-char-window/README.md new file mode 100644 index 0000000000..d353a2c8d0 --- /dev/null +++ b/research/p104-odd-char-window/README.md @@ -0,0 +1,85 @@ +# Odd-character window of the P120 odd graph (no new κ) + +**No new κ.** The selected record stays `781451/250000000`. This package +upper-bounds the port-window of `P120` and of every nonempty subset, including +`P104` and both copies of `P112`. It does not build a word or a paid profile. + +The proof is in [PROOF.md](PROOF.md). The finite census, the rank checks and +the failure controls are in [verify.py](verify.py). + +## Result + +Let the odd graph have an edge when two weight-3-or-7 vectors in `F_2^9` have +odd dot product. `P120` is all 120 of those vectors. `P104` is the 104-vector +subset in `data/ports_p104.json`, byte-identical to the port list of PR #6933 +at `a967c521074c2c7450255ae237fda9c439ee1b35`. + +1. The odd graph on `P120` is connected and strongly regular with parameters + `(120, 63, 30, 36)`. The degree count is written out. The parameters `λ = 30` + and `μ = 36` are the exhaustive pair census. +2. `H = 3I - A` has rank 36 over `Q`, nonzero diagonal in every characteristic + other than 3, and zeros on non-edges. So `w(S; F) ≤ 36` for every nonempty + `S ⊆ P120` and every field of characteristic not 3. +3. In characteristic 3 that matrix has zero diagonal. A degree-at-most-2 + factorisation produces a 1-block pattern of rank 38, so `w(S; F_3) ≤ 38`. + +Accepting the lower bounds in #6933, Theorem 4, without replaying them: + +| field | P104 | P112 | P120 | +|---|---|---|---| +| char ≠ 2, 3 | [13, 36] | [14, 36] | [15, 36] | +| char 3 | [13, 38] | [14, 38] | [15, 38] | + +Characteristic 2 is unchanged: #6933 already has `w(P104; F_2) ∈ [53/6, 9]` and +`w = 9` on `P112` and `P120`. The reduction of `H` is a legal pattern there of +rank at most 36, which does not beat the Gram pattern of rank 9. + +## Scope + +Original card: `complex-rank-shape-decoder`. Scope status: **changed**. The +card asks whether a decoder or coframe change improves the signed moment. This +package does not change a word, a coframe, or a moment. It answers the odd-character +half of the window question left open by #6933: an odd-character decoder mask +of this type cannot inherit the characteristic-2 window 9, and the best +explicit pattern here has ratio 36, or 38 in characteristic 3. + +The lower ends 13, 14 and 15 are #6933's. They are not reproved. The upper +ends are proved here. Base commit `7c49fe32c55de02c2c873655c804b16e4c3fef0a`, +priority revision 8. + +## Reproduce + +From the repository root, CPython 3.12, standard library only: + +```sh +python3 -B research/p104-odd-char-window/verify.py +python3 -I -O -B research/p104-odd-char-window/verify.py +python3 -B scripts/research_package.py --package research/p104-odd-char-window +``` + +Expected final line: `PASS_ODD_CHAR_WINDOW rank36=36 char3_rank=38`, then +`PASS_REGISTERED_RESEARCH_PACKAGE` with outcome `partial`. + +The verifier enumerates all `C(120,2)` pairs, reduces `3I-A` modulo four odd +primes, solves the 120 characteristic-3 linear systems, and rejects a planted +orthogonal entry, the characteristic-3 reduction of `3I-A`, the all-ones +matrix, and the linear-only feature map on eight sampled columns. No Lean, +Docker, selected-baseline replay, or solver certificate was run. + +## Open next questions + +1. Is `w(P104; F)` equal to 13 for some odd characteristic, or is 36 (38 in + characteristic 3) the wrong shape of construction? The E8 argument of #6933 + is the matching lower bound. A first step is one explicit factorisation of + width 13 over `F_5`. Nothing in this package exhibits one, and the + Bose-Mesner pattern `3I-A` cannot, because its rank is 36. +2. Does characteristic 3 admit a pattern of rank 36? The matrix that works for + every other odd characteristic is illegal there. The degree-2 factorisation + has rank 38. Closing the gap of 2 needs a different column space. + +## Credit + +DreamingOfClouds, PR #6933, for the window definition, the port list, the +characteristic-2 Gram rank, and Theorem 4's lower bounds `n/8`. The strongly +regular census and both upper bounds are new. Prepared by unpaidmoon with +substantial Cursor Grok assistance. New work is Apache-2.0. diff --git a/research/p104-odd-char-window/SOURCES.json b/research/p104-odd-char-window/SOURCES.json new file mode 100644 index 0000000000..594089b9c7 --- /dev/null +++ b/research/p104-odd-char-window/SOURCES.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + } + ] +} diff --git a/research/p104-odd-char-window/TASK.json b/research/p104-odd-char-window/TASK.json new file mode 100644 index 0000000000..0be61fde40 --- /dev/null +++ b/research/p104-odd-char-window/TASK.json @@ -0,0 +1,81 @@ +{ + "schema_version": 1, + "task_id": "complex-rank-shape-decoder", + "priority_revision": 8, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "original_card": { + "id": "complex-rank-shape-decoder", + "question": "Can a legal decoder or coframe change improve the full signed moment, including changed helper targets?", + "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", + "docs/research/recursive-invoice-preflight.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": "A source-bound arbitrary-input identity and legal producer/consumer boundary with the complete paid and productive target invoice, including restoration, ownership, native alignment and extra charges. Price under the actual current model; historical ceiling.py assumptions must be established before use. A favorable optimistic relaxation keeps a route open but is not a completed supplier. A scoped local result remains useful; expansion requires the family-level budget gate.", + "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": "Price one complete changed itinerary with both paid and productive histograms. Check #5693/#5698 for overlap and their exact hypotheses before another coframe search. Use the signed invoice preflight where its boundary contract agrees; an inconclusive concave comparison is not a power crossing. Stop if an optimistic complete budget fails at the chosen target or native delivery remains unspecified.", + "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": [ + "coframe", + "signed moment", + "5693", + "5698" + ], + "existing_checks": [ + { + "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": "Upper bound the odd-character window of the P120 odd graph and of every nonempty subset, including the P104 port set of PR 6933. No word, moment, or kappa.", + "scope_change_reason": "The card asks whether a decoder or coframe change improves the signed moment. This package does not change a word or a moment. It answers the odd-character half of the window question left open by PR 6933: the block-mask rank H_f is at most 36 in every characteristic other than 3, and at most 38 in characteristic 3. An odd-character mask cannot inherit the characteristic-2 window 9.", + "bottleneck_link": "A k-block decoder mask on these ports is the fractional Haemers window of the odd graph. The characteristic-2 window is at most 9. The odd-character ceiling shows that moving the same mask to an odd field does not undercut that window; the proved patterns sit at 36 or 38. This is a scoped rank obstruction, not a supplier admission.", + "budget_minutes": 60, + "stop_rule": "Stop after one explicit pattern whose rank is checked over Q and over F_3. Do not search for a rank-13 factorisation or a physical decoder in this package.", + "outcome": "partial", + "evidence": "PROOF.md Theorems 1 and 2. verify.py prints PASS_ODD_CHAR_WINDOW rank36=36 char3_rank=38. Lower bounds 13, 14 and 15 are cited from PR 6933 Theorem 4 and are not replayed.", + "author": "unpaidmoon", + "ai_assistance": "Substantial Cursor Grok assistance.", + "open_questions": [ + { + "question": "Is w(P104; F) equal to 13 for some odd characteristic?", + "why_it_matters": "PR 6933 proves the lower bound 13. Equality would make the odd-character window sharp; the pattern proved here has rank 36, or 38 in characteristic 3.", + "first_step": "Search for one 104 by 13 factorisation over F_5 with zeros on orthogonal pairs and nonzero diagonal.", + "blocked_by": "The Bose-Mesner matrix 3I-A has rank exactly 36, so a sharper pattern needs edge weights outside that algebra. No such factorisation is known." + }, + { + "question": "Does characteristic 3 admit a 1-block pattern of rank 36 on P120?", + "why_it_matters": "Every other characteristic not equal to 3 has the rank-36 pattern. Characteristic 3 is the only odd characteristic where that matrix is illegal.", + "first_step": "Decide whether the column space of the degree-2 factorisation can be replaced by a 36-dimensional space that still solves the orthogonal equations.", + "blocked_by": "The degree-2 matrix constructed here has rank 38. Eight linear-only samples are inconsistent, which does not rule out a different 36-dimensional model." + } + ] +} diff --git a/research/p104-odd-char-window/VERIFY.json b/research/p104-odd-char-window/VERIFY.json new file mode 100644 index 0000000000..9a105e7595 --- /dev/null +++ b/research/p104-odd-char-window/VERIFY.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exhaustive strongly regular census of the 120-vertex odd graph, rational eigenvalue arithmetic, rank 36 of 3I-A modulo 5, 7, 11 and 10007, induced P104 and P112 patterns, characteristic-3 degree-2 factorisation of rank 38, and controls that reject a planted orthogonal entry, the characteristic-3 reduction of 3I-A, the all-ones matrix, and linear-only features." + } + ] +} diff --git a/research/p104-odd-char-window/data/ports_p104.json b/research/p104-odd-char-window/data/ports_p104.json new file mode 100644 index 0000000000..8037fd1087 --- /dev/null +++ b/research/p104-odd-char-window/data/ports_p104.json @@ -0,0 +1,109 @@ +{ +"description": "The 104 ports of P104 as vectors of F_2^9 (bit i of the integer is coordinate i), in a fixed order; two distinct ports are adjacent in the odd graph iff popcount(a & b) is odd.", +"ports": [ +11, +19, +35, +131, +259, +13, +21, +37, +69, +133, +261, +41, +73, +265, +49, +81, +145, +273, +161, +193, +321, +385, +14, +22, +38, +70, +134, +262, +26, +74, +138, +50, +146, +274, +98, +290, +194, +322, +386, +28, +44, +140, +268, +84, +148, +276, +100, +164, +292, +196, +324, +388, +56, +88, +152, +280, +168, +296, +200, +328, +392, +112, +176, +304, +208, +336, +400, +224, +352, +416, +508, +506, +502, +494, +478, +446, +382, +254, +505, +501, +493, +477, +445, +381, +253, +499, +475, +443, +379, +251, +487, +471, +439, +375, +247, +463, +431, +367, +239, +415, +351, +223, +319, +191 +] +} \ No newline at end of file diff --git a/research/p104-odd-char-window/verify.py b/research/p104-odd-char-window/verify.py new file mode 100644 index 0000000000..29314e9b77 --- /dev/null +++ b/research/p104-odd-char-window/verify.py @@ -0,0 +1,397 @@ +#!/usr/bin/env python3 +"""Upper bound for the odd-character window of the P120 odd graph. + +Characteristic not 2 or 3: the matrix 3I-A has rank 36. +Characteristic 3: an explicit degree-at-most-2 factorisation has rank 45. +No kappa claim. Standard library only. +""" +import json +from pathlib import Path + +ROOT = Path(__file__).resolve().parent +PORTS_SHA256 = "691c7b7d212112115b1bfc76db89f90d304ec448dc8c4a0c43d9a5954317146c" +P = 10007 + + +def require(ok, message): + if not ok: + raise SystemExit("FAIL: " + message) + + +def weight(v): + return bin(v).count("1") + + +def odd_dot(a, b): + return bin(a & b).count("1") & 1 + + +def hand_degree(u): + """Degree in the odd graph, by the case split in PROOF.md.""" + coords = [i for i in range(9) if (u >> i) & 1] + outside = [i for i in range(9) if not ((u >> i) & 1)] + if weight(u) == 3: + weight3 = 3 * (6 * 5 // 2) # one point of u, two of the six outside + weight7 = (6 * 5 // 2) + 3 # complement 2-set misses u, or sits inside u + return weight3 + weight7 + complement = outside # weight 2 + require(len(complement) == 2 and len(coords) == 7, "weight-7 shape") + weight3 = (7 * 6 * 5 // 6) + 7 # 3-set outside the complement, or the complement plus one + # other weight-7 vectors whose complement 2-set is disjoint from this one + weight7 = 7 * 6 // 2 + return weight3 + weight7 + + +def p120(): + return [v for v in range(1 << 9) if weight(v) % 4 == 3] + + +def load_p104(): + raw = (ROOT / "data" / "ports_p104.json").read_bytes() + import hashlib + require(hashlib.sha256(raw).hexdigest() == PORTS_SHA256, "P104 port-list bytes changed") + ports = json.loads(raw)["ports"] + require(len(ports) == len(set(ports)) == 104, "P104 is not 104 distinct ports") + return ports + + +def rank_mod(rows, p): + matrix = [row[:] for row in rows] + n = len(matrix) + m = len(matrix[0]) + rank = 0 + for col in range(m): + pivot = None + for i in range(rank, n): + if matrix[i][col] % p: + pivot = i + break + if pivot is None: + continue + matrix[rank], matrix[pivot] = matrix[pivot], matrix[rank] + inv = pow(matrix[rank][col], -1, p) + for j in range(col, m): + matrix[rank][j] = matrix[rank][j] * inv % p + for i in range(n): + if i == rank or matrix[i][col] % p == 0: + continue + factor = matrix[i][col] % p + for j in range(col, m): + matrix[i][j] = (matrix[i][j] - factor * matrix[rank][j]) % p + rank += 1 + return rank + + +def pattern_matrix(vertices): + """H = 3I - A over Z, as a dense integer matrix. Zeros sit on non-edges.""" + n = len(vertices) + rows = [[0] * n for _ in range(n)] + for i, u in enumerate(vertices): + rows[i][i] = 3 + for j in range(i + 1, n): + if odd_dot(u, vertices[j]): + rows[i][j] = -1 + rows[j][i] = -1 + return rows + + +def valid_pattern(rows, vertices, p=None): + """Unit-or-nonzero diagonal and zeros on unordered orthogonal pairs.""" + n = len(vertices) + for i, u in enumerate(vertices): + diag = rows[i][i] if p is None else rows[i][i] % p + if diag == 0: + return False + for j in range(i + 1, n): + entry = rows[i][j] if p is None else rows[i][j] % p + orthogonal = not odd_dot(u, vertices[j]) + if orthogonal and entry != 0: + return False + other = rows[j][i] if p is None else rows[j][i] % p + if orthogonal and other != 0: + return False + return True + + +def neighbor_data(vertices): + n = len(vertices) + lists = [] + bits = [] + for i, u in enumerate(vertices): + nbrs = [j for j, v in enumerate(vertices) if i != j and odd_dot(u, v)] + mask = 0 + for j in nbrs: + mask |= 1 << j + lists.append(nbrs) + bits.append(mask) + return lists, bits + + +def parameter_census(vertices): + """Return (degree set, lambda set, mu set) by two independent pair counts.""" + lists, bits = neighbor_data(vertices) + degrees = {len(nbrs) for nbrs in lists} + lam_bits, mu_bits = set(), set() + lam_sets, mu_sets = set(), set() + n = len(vertices) + as_sets = [set(nbrs) for nbrs in lists] + for i in range(n): + for j in range(i + 1, n): + common_bits = (bits[i] & bits[j]).bit_count() + common_sets = len(as_sets[i] & as_sets[j]) + require(common_bits == common_sets, "bitset and set censuses disagree") + adjacent = ((bits[i] >> j) & 1) == 1 + if adjacent: + lam_bits.add(common_bits) + lam_sets.add(common_sets) + else: + mu_bits.add(common_bits) + mu_sets.add(common_sets) + require(lam_bits == lam_sets and mu_bits == mu_sets, "lambda/mu census mismatch") + return degrees, lam_bits, mu_bits + + +def connected(bits): + n = len(bits) + seen = 0 + stack = [0] + seen |= 1 + while stack: + i = stack.pop() + mask = bits[i] + while mask: + low = mask & -mask + j = low.bit_length() - 1 + mask ^= low + if (seen >> j) & 1: + continue + seen |= 1 << j + stack.append(j) + return seen == (1 << n) - 1 + + +def multiplicities(n, k, theta, tau): + """Solve 1+f+g = n and k + f*theta + g*tau = 0.""" + # f + g = n - 1 + # theta f + tau g = -k + # f = ((n-1)*tau + k) / (tau - theta) wait, derive explicitly below. + den = theta - tau + require(den != 0, "repeated restricted eigenvalues") + # theta f + tau ((n-1)-f) = -k, so (theta-tau) f = -k - tau(n-1). + num = -k - tau * (n - 1) + require(num % den == 0, "non-integral multiplicity") + f = num // den + g = (n - 1) - f + return f, g + + +def principal(rows, index): + return [[rows[i][j] for j in index] for i in index] + + +def odd_cliques(vertices, size): + found = [] + + def rec(start, chosen): + if len(chosen) == size: + found.append(list(chosen)) + return + for i in range(start, len(vertices)): + v = vertices[i] + if all(odd_dot(v, vertices[j]) for j in chosen): + chosen.append(i) + rec(i + 1, chosen) + chosen.pop() + + rec(0, []) + return found + + +def features(v): + bits = [(v >> i) & 1 for i in range(9)] + coords = bits[:] + for i in range(9): + for j in range(i + 1, 9): + coords.append(bits[i] * bits[j]) + return coords + + +def solve_column(phi, equations, p): + """Solve phi[i] · y = rhs for each (i, rhs). Free variables are set to 0.""" + width = len(phi[0]) + matrix = [] + for i, rhs in equations: + matrix.append(phi[i][:] + [rhs % p]) + where = [None] * width + rank = 0 + for col in range(width): + pivot = None + for i in range(rank, len(matrix)): + if matrix[i][col] % p: + pivot = i + break + if pivot is None: + continue + matrix[rank], matrix[pivot] = matrix[pivot], matrix[rank] + inv = pow(matrix[rank][col], -1, p) + for k in range(col, width + 1): + matrix[rank][k] = matrix[rank][k] * inv % p + for i in range(len(matrix)): + if i == rank or matrix[i][col] % p == 0: + continue + factor = matrix[i][col] % p + for k in range(col, width + 1): + matrix[i][k] = (matrix[i][k] - factor * matrix[rank][k]) % p + where[col] = rank + rank += 1 + for i in range(rank, len(matrix)): + if matrix[i][width] % p: + return None + solution = [0] * width + for col in range(width): + if where[col] is not None: + solution[col] = matrix[where[col]][width] % p + return solution + + +def char3_factorisation(vertices): + p = 3 + phi = [[c % p for c in features(v)] for v in vertices] + n = len(vertices) + orthogonal = [[] for _ in range(n)] + for i in range(n): + for j in range(i + 1, n): + if not odd_dot(vertices[i], vertices[j]): + orthogonal[i].append(j) + orthogonal[j].append(i) + columns = [] + for j in range(n): + equations = [(i, 0) for i in orthogonal[j]] + [(j, 1)] + solution = solve_column(phi, equations, p) + if solution is None: + return None + for i, rhs in equations: + got = sum(phi[i][t] * solution[t] for t in range(len(solution))) % p + require(got == rhs % p, "char-3 column solution does not meet its equations") + columns.append(solution) + rows = [] + for u in range(n): + row = [] + for v in range(n): + row.append(sum(phi[u][t] * columns[v][t] for t in range(len(phi[0]))) % p) + rows.append(row) + return rows + + +def linear_only_failures(vertices): + """Degree-1 features are not enough for a char-3 column at every vertex.""" + p = 3 + phi = [[(v >> i) & 1 for i in range(9)] for v in vertices] + n = len(vertices) + failed = 0 + for j in range(0, n, 17): + equations = [(i, 0) for i in range(n) if i != j and not odd_dot(vertices[i], vertices[j])] + equations.append((j, 1)) + if solve_column(phi, equations, p) is None: + failed += 1 + return failed + + +def main(): + vertices = p120() + require(hand_degree(next(v for v in vertices if weight(v) == 3)) == 63, "hand count, weight 3") + require(hand_degree(next(v for v in vertices if weight(v) == 7)) == 63, "hand count, weight 7") + require(len(vertices) == 120, "P120 does not have 120 vectors") + require(sorted(weight(v) for v in vertices)[0] == 3 and max(map(weight, vertices)) == 7, + "P120 is not the weight-3 and weight-7 vectors") + require(sum(weight(v) == 3 for v in vertices) == 84, "weight-3 count") + require(sum(weight(v) == 7 for v in vertices) == 36, "weight-7 count") + + degrees, lambdas, mus = parameter_census(vertices) + require(degrees == {63}, "degree is not constantly 63: %s" % sorted(degrees)) + require(lambdas == {30}, "lambda is not constantly 30: %s" % sorted(lambdas)) + require(mus == {36}, "mu is not constantly 36: %s" % sorted(mus)) + _, bits = neighbor_data(vertices) + require(connected(bits), "P120 odd graph is disconnected") + print("PASS_SRG_PARAMETERS n=120 k=63 lambda=30 mu=36") + + # Eigenvalues of an srg(120,63,30,36): discriminant (lambda-mu)^2 + 4(k-mu) = 36+108 = 144. + delta = (30 - 36) ** 2 + 4 * (63 - 36) + require(delta == 144, "discriminant") + root = 12 # sqrt(144) + theta = ((30 - 36) + root) // 2 + tau = ((30 - 36) - root) // 2 + require((theta, tau) == (3, -9), "restricted eigenvalues") + f, g = multiplicities(120, 63, theta, tau) + require((f, g) == (84, 35), "multiplicities f,g = %s,%s" % (f, g)) + require(63 + f * theta + g * tau == 0, "trace") + require(1 + f + g == 120, "multiplicity sum") + print("PASS_EIGENVALUE_ARITHMETIC theta=3 mult=84 tau=-9 mult=35") + + host = pattern_matrix(vertices) + require(valid_pattern(host, vertices), "3I-A is not a 1-block pattern over Z") + for prime in (5, 7, 11, P): + reduced = [[entry % prime for entry in row] for row in host] + require(valid_pattern(reduced, vertices, prime), "3I-A dies as a pattern mod %d" % prime) + require(rank_mod(reduced, prime) == 36, "rank of 3I-A mod %d is not 36" % prime) + print("PASS_RANK36_ODD_CHAR primes=5,7,11,10007") + + # Characteristic 3 kills this particular matrix: diagonal 3 ≡ 0. + reduced3 = [[entry % 3 for entry in row] for row in host] + require(all(row[i] % 3 == 0 for i, row in enumerate(reduced3)), + "control: char 3 should kill the diagonal of 3I-A") + require(not valid_pattern(reduced3, vertices, 3), "control: 3I-A must be illegal in char 3") + + # A nonzero orthogonal entry is rejected. + planted = [row[:] for row in host] + pair = next((i, j) for i in range(120) for j in range(i + 1, 120) + if not odd_dot(vertices[i], vertices[j])) + planted[pair[0]][pair[1]] = 5 + planted[pair[1]][pair[0]] = 5 + require(not valid_pattern(planted, vertices), "control: planted orthogonal entry was accepted") + print("PASS_PATTERN_CONTROLS") + + ports = load_p104() + require(set(ports) <= set(vertices), "P104 is not inside P120") + require(sum(weight(v) == 3 for v in ports) == 70, "P104 weight-3 count") + require(sum(weight(v) == 7 for v in ports) == 34, "P104 weight-7 count") + index = {v: i for i, v in enumerate(vertices)} + p104_index = [index[v] for v in ports] + p104_rows = principal(host, p104_index) + require(valid_pattern(p104_rows, ports), "induced 3I-A on P104 is not a pattern") + require(rank_mod([[x % P for x in row] for row in p104_rows], P) <= 36, "P104 window matrix exceeds rank 36") + p104_degrees = {sum(odd_dot(u, v) for v in ports if v != u) for u in ports} + require(p104_degrees == {55}, "P104 is not 55-regular: %s" % sorted(p104_degrees)) + + deleted = [v for v in vertices if v not in set(ports)] + require(len(deleted) == 16, "deleted set") + cliques = odd_cliques(deleted, 8) + require(len(cliques) == 2, "expected two deleted 8-cliques, found %d" % len(cliques)) + for clique in cliques: + extra = [deleted[i] for i in clique] + block = ports + extra + rows = principal(host, [index[v] for v in block]) + require(len(block) == 112 and valid_pattern(rows, block), "P112 pattern") + require(rank_mod([[x % P for x in row] for row in rows], P) <= 36, "P112 rank") + print("PASS_INDUCED_SUBSETS p104_regular=55 p112_cliques=2") + + char3 = char3_factorisation(vertices) + require(char3 is not None, "char-3 degree-2 systems are inconsistent") + require(valid_pattern(char3, vertices, 3), "char-3 factorisation is not a pattern") + char3_rank = rank_mod(char3, 3) + require(char3_rank == 38, "char-3 rank %d is not 38" % char3_rank) + p104_char3 = principal(char3, p104_index) + require(valid_pattern(p104_char3, ports, 3), "char-3 P104 principal submatrix") + require(rank_mod(p104_char3, 3) <= char3_rank, "principal rank rose") + failed_linear = linear_only_failures(vertices) + require(failed_linear >= 1, "control: linear features unexpectedly solved every sampled column") + print("PASS_CHAR3_FACTORISATION rank=%d linear_failures=%d" % (char3_rank, failed_linear)) + + # The all-ones matrix is the wrong mask. + ones = [[1] * 120 for _ in range(120)] + require(not valid_pattern(ones, vertices), "control: all-ones was accepted") + print("PASS_ODD_CHAR_WINDOW rank36=36 char3_rank=%d" % char3_rank) + + +if __name__ == "__main__": + main()