From 4f3c5790ee1bc7276eb265a1a0978dde87a29cb8 Mon Sep 17 00:00:00 2001 From: Sagar Thakrar <18622288+thakrarsagar@users.noreply.github.com> Date: Thu, 15 Oct 2026 17:50:42 +0530 Subject: [PATCH 1/2] Close PR2471's paired-plane scalar fitting rank bracket at exactly 49 For PR1825's fixed 56 matched planes under the strict PR1889 mask (PR2471 head 5a7c2b6, bracket [48,50]), an independent stdlib reconstruction gives omega(G)=24, chi(G)=25, chi_f(G)=49/2 and chi_2(G)=49. An explicit 49-support 0/1 fit gives rank 49 over every field. A 22-plane clique plus an induced 5-cycle core of orthogonal planes forces rank >= 49 over every field (proof in README; premises checked exactly; lemma corroborated over GF(2)/GF(3)). No kappa claim. Prepared by thakrarsagar with substantial AI assistance from Claude. Co-Authored-By: Claude Opus 5.5 --- .../CERTIFICATE.json | 643 ++++++++++++++++++ .../README.md | 208 ++++++ .../SOURCES.json | 30 + .../TASK.json | 66 ++ .../VERIFY.json | 22 + .../verify.py | 621 +++++++++++++++++ 6 files changed, 1590 insertions(+) create mode 100644 research/paired-plane-minrank-bracket-audit/CERTIFICATE.json create mode 100644 research/paired-plane-minrank-bracket-audit/README.md create mode 100644 research/paired-plane-minrank-bracket-audit/SOURCES.json create mode 100644 research/paired-plane-minrank-bracket-audit/TASK.json create mode 100644 research/paired-plane-minrank-bracket-audit/VERIFY.json create mode 100644 research/paired-plane-minrank-bracket-audit/verify.py diff --git a/research/paired-plane-minrank-bracket-audit/CERTIFICATE.json b/research/paired-plane-minrank-bracket-audit/CERTIFICATE.json new file mode 100644 index 0000000000..503375b093 --- /dev/null +++ b/research/paired-plane-minrank-bracket-audit/CERTIFICATE.json @@ -0,0 +1,643 @@ +{ + "c5_core": [ + 13, + 23, + 35, + 16, + 34 + ], + "checks": { + "c5_lemma_finite_corroboration": { + "gf2_control_P1P3_freed_completion_exists": 1, + "gf2_rank4_completion_exists": 0, + "gf3_rank4_completion_exists": 0 + }, + "chi": { + "dp_states": 40277, + "max_savings_b1": 31, + "value": 25 + }, + "chi_f": "49/2", + "lower_bound_fractional_clique_sum": "49/2", + "nonorthogonal_plane_pairs": 1431, + "omega": { + "dp_states": 12138, + "maximum_clique_count": 194, + "value": 24 + }, + "orthogonal_set_counts_by_size": { + "1": 56, + "2": 109, + "3": 24 + }, + "pr2471_witnesses_rechecked": { + "orthogonal_classes_25_rank50_fit": true, + "plane_clique_24_pairwise_nonorthogonal": true + }, + "rank49_fit": { + "rank_mod_101": 49, + "rank_mod_2": 49, + "rank_mod_3": 49, + "required_entries_checked": 11672, + "supports": 49 + }, + "rank_lower_bound": 49, + "solver_controls": { + "C5": [ + 2, + 3, + 5 + ], + "C7": [ + 3, + 4, + 7 + ] + } + }, + "clique22": [ + 0, + 4, + 8, + 17, + 18, + 19, + 20, + 21, + 24, + 26, + 28, + 29, + 32, + 36, + 38, + 39, + 41, + 42, + 43, + 45, + 46, + 52 + ], + "dp_vertex_order": [ + 6, + 36, + 8, + 5, + 42, + 9, + 20, + 22, + 49, + 26, + 51, + 41, + 45, + 27, + 25, + 18, + 55, + 39, + 3, + 14, + 47, + 7, + 24, + 43, + 44, + 38, + 15, + 21, + 4, + 52, + 17, + 19, + 33, + 28, + 10, + 30, + 34, + 13, + 54, + 16, + 23, + 35, + 12, + 48, + 46, + 31, + 50, + 29, + 40, + 11, + 37, + 53, + 1, + 32, + 0, + 2 + ], + "fractional_clique_y": [ + "1", + "0", + "0", + "0", + "1", + "0", + "0", + "0", + "1", + "0", + "0", + "0", + "0", + "1/2", + "0", + "0", + "1/2", + "1", + "1", + "1", + "1", + "1", + "0", + "1/2", + "1", + "0", + "1", + "0", + "1", + "1", + "0", + "0", + "1", + "0", + "1/2", + "1/2", + "1", + "0", + "1", + "1", + "0", + "1", + "1", + "1", + "0", + "1", + "1", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "0", + "0" + ], + "fractional_colouring_x": [ + [ + [ + 36 + ], + "1" + ], + [ + [ + 3, + 38 + ], + "1" + ], + [ + [ + 5, + 8 + ], + "1" + ], + [ + [ + 9, + 41 + ], + "1" + ], + [ + [ + 11, + 29 + ], + "1" + ], + [ + [ + 13, + 23 + ], + "1/2" + ], + [ + [ + 13, + 34 + ], + "1/2" + ], + [ + [ + 15, + 52 + ], + "1" + ], + [ + [ + 17, + 40 + ], + "1" + ], + [ + [ + 19, + 50 + ], + "1" + ], + [ + [ + 20, + 22 + ], + "1" + ], + [ + [ + 21, + 44 + ], + "1" + ], + [ + [ + 27, + 45 + ], + "1" + ], + [ + [ + 28, + 31 + ], + "1" + ], + [ + [ + 42, + 55 + ], + "1" + ], + [ + [ + 43, + 47 + ], + "1" + ], + [ + [ + 0, + 1, + 2 + ], + "1" + ], + [ + [ + 3, + 18, + 25 + ], + "1" + ], + [ + [ + 4, + 6, + 7 + ], + "1" + ], + [ + [ + 10, + 14, + 24 + ], + "1/2" + ], + [ + [ + 10, + 24, + 30 + ], + "1/2" + ], + [ + [ + 12, + 46, + 48 + ], + "1" + ], + [ + [ + 14, + 33, + 39 + ], + "1" + ], + [ + [ + 16, + 30, + 34 + ], + "1/2" + ], + [ + [ + 16, + 35, + 54 + ], + "1/2" + ], + [ + [ + 23, + 35, + 54 + ], + "1/2" + ], + [ + [ + 26, + 49, + 51 + ], + "1" + ], + [ + [ + 32, + 37, + 53 + ], + "1" + ] + ], + "negative_controls": { + "Q_plane_replaced_by_core_neighbour": "rejected: Q not pairwise non-orthogonal at 18,3", + "core_reordered_not_a_cycle": "rejected: core is not an induced 5-cycle at 13,35", + "fractional_clique_half_weight_raised_to_1": "rejected: fractional clique violated on (13, 23)", + "fractional_colouring_set_dropped": "rejected: fractional colouring must cover every plane", + "pr2471_classes_merged_to_24": "rejected: support joins ports 102,111 of non-orthogonal or equal planes", + "rank_fit_both_ports_of_one_plane_in_one_support": "rejected: support joins ports 102,58 of non-orthogonal or equal planes", + "tampered_PR1825_certificate_byte": "rejected: PR1825 certificate sha256 mismatch" + }, + "object": "PR1825 fixed 56 matched planes, strict PR1889 scalar mask (as stated in PR2471)", + "rank49_supports": [ + [ + 102 + ], + [ + 58 + ], + [ + 78, + 92 + ], + [ + 12, + 48 + ], + [ + 79, + 82 + ], + [ + 7, + 10 + ], + [ + 81, + 94 + ], + [ + 11, + 61 + ], + [ + 85, + 88 + ], + [ + 31, + 34 + ], + [ + 21, + 41 + ], + [ + 16, + 64 + ], + [ + 33, + 100 + ], + [ + 14, + 74 + ], + [ + 53, + 93 + ], + [ + 18, + 51 + ], + [ + 47, + 99 + ], + [ + 25, + 73 + ], + [ + 24, + 32 + ], + [ + 19, + 28 + ], + [ + 63, + 91 + ], + [ + 26, + 66 + ], + [ + 56, + 111 + ], + [ + 38, + 67 + ], + [ + 86, + 90 + ], + [ + 37, + 42 + ], + [ + 95, + 107 + ], + [ + 65, + 110 + ], + [ + 97, + 109 + ], + [ + 60, + 71 + ], + [ + 0, + 2, + 4 + ], + [ + 1, + 3, + 5 + ], + [ + 50, + 55 + ], + [ + 20, + 30 + ], + [ + 80, + 83, + 84 + ], + [ + 6, + 8, + 9 + ], + [ + 23, + 39, + 77 + ], + [ + 13, + 27, + 89 + ], + [ + 36, + 98, + 106 + ], + [ + 15, + 68, + 70 + ], + [ + 17, + 45, + 62 + ], + [ + 46, + 52 + ], + [ + 35, + 40, + 54 + ], + [ + 22, + 69, + 105 + ], + [ + 29, + 57, + 108 + ], + [ + 72, + 96, + 101 + ], + [ + 43, + 75, + 76 + ], + [ + 59, + 87, + 103 + ], + [ + 44, + 49, + 104 + ] + ], + "result": { + "chi_G": 25, + "field_scope": "every field: lower bound by the C5 lemma proof in README, upper bound by an explicit 0/1 disjoint-support matrix; finite corroboration of the lemma over GF(2) and GF(3) only", + "fractional_chi_G": "49/2", + "min_scalar_fitting_rank": 49, + "omega_G": 24, + "two_fold_chi_G": 49 + }, + "schema_version": 1, + "sources": { + "research/community-frontier1094-audit/selected-replay.tar.gz": "f1da80610bf33c58527f18ad63b4350d0b864e1d4486141ee17ac9bed4d529d6", + "research/community-frontier1094-audit/selected-replay.tar.gz#candidate/strict/global/base/work/complex-nine-native/DATA-PHASES.json": "c5916ff312678f12aba403847643fbbc29f643acec60bdf836fa56cd3e8251fa", + "research/paired-plane-scalar-mask-obstruction/PR1825-CERTIFICATE.json": "4fd648f7b5178bff5441bf364d58234b7bc1a43b924bc6da03013c948f1473b1" + } +} diff --git a/research/paired-plane-minrank-bracket-audit/README.md b/research/paired-plane-minrank-bracket-audit/README.md new file mode 100644 index 0000000000..687dc4b7f5 --- /dev/null +++ b/research/paired-plane-minrank-bracket-audit/README.md @@ -0,0 +1,208 @@ +# Exact scalar fitting rank 49 for PR2471's fixed paired-plane mask + +**Status: independent verification of PR2471 plus a construction and matching +lower bound for a finite algebraic question. No kappa, supplier price or +selected-result change.** + +[PR2471](https://github.com/CrocSwap/integer-mult-bounds/pull/2471) (ywz65, +head `5a7c2b681b79d5b5e25fac62aa4bad908525b5ca`) shows that the minimum rank of +a scalar fitting matrix for the strict PR1889 mask on PR1825's 56 matched P112 +planes lies in `[48, 50]` over every field. Its open question 1 asks whether +rank 48 or 49 is possible, or whether the floor is 50. + +**Answer: the minimum is exactly 49 over every field.** + +- *Upper bound 49.* An explicit symmetric 0/1 matrix with 49 disjoint supports + fits the mask. This improves PR2471's rank-50 construction by one. +- *Lower bound 49.* Every fitting matrix over every field has rank at least 49. + This improves PR2471's `I_48` floor by one. It uses a 54-port principal + submatrix `I_44 (+) M` together with a short linear-algebra lemma for an + induced 5-cycle of orthogonal planes. + +Both of PR2471's witnesses re-check: a 24-clique and a 25-class rank-50 fit. +PR2471 did not assert optimality of either witness, so nothing in PR2471 is +contradicted. Its README phrase "no refactorization with 23 scalar rank-one +channels can fit it" is true, but much weaker than its own rank-48 floor, which +already excludes 47 channels. With the floor raised here, 48 channels cannot fit. + +## Model (same as PR2471) + +`q_0..q_111` in `F_2^9` are the P112 labels. PR1825's matching pairs them into +56 planes `E=span(q_i,q_j)` with Gram matrix `I_2`. Two distinct planes are +*orthogonal* when all four basis pairings vanish. A plane is never orthogonal to +itself. A matrix `K` over a field `F` *fits* when `K_ii=1`, and `K_ij=0` whenever +`i!=j` and the planes of `i,j` are not orthogonal (including the same plane). +Entries between orthogonal planes are free. No symmetry is required. + +Let `G` be the graph on the 56 planes in which two planes are adjacent when they +are non-orthogonal. Independent reconstruction from the pinned sources gives +1431 non-orthogonal pairs and only 109 orthogonal pairs. There are 24 orthogonal +triples and no orthogonal 4-set, so `alpha(G)=3`. Plane 36 is orthogonal to no +other plane. + +## Results (all exact, recomputed by `verify.py`) + +| quantity | value | evidence | +|---|---|---| +| `omega(G)` | 24 (194 maximum cliques) | path-order DP, 12138 states; this algorithm differs from PR2471's colour-bounded branch and bound | +| `chi(G)` | **25** | exact DP over packings of orthogonal pairs and triples (40277 states). No 24-class plane partition exists, so PR2471's `2*chi` method cannot reach 48 | +| `chi_f(G)` | **49/2** | exact Bland simplex. The primal (half-integral fractional colouring) and dual (fractional clique) are stored and both re-checked against all 189 orthogonal sets | +| `chi_2(G)` = `chi(G[K_2])` | **49** | upper: the doubled half-integral primal gives 49 port classes. Lower: `2*chi_f`. An optional capacity-2 DP (`--two-fold-dp`) independently gives max savings 63, so `112-63=49` | +| min fitting rank, every field | **49** | upper: 49-support 0/1 fit; lower: theorem below | + +The rank-49 fit `K = sum_S 1_S 1_S^T` uses the 49 supports in +`CERTIFICATE.json` (`rank49_supports`). Every port lies in exactly one support. +Each support contains ports of distinct, pairwise orthogonal planes. So the +diagonal is 1 and every nonzero off-diagonal entry joins orthogonal planes. +Each entry is a single 0/1 term, so the fit holds in every characteristic. The +verifier checks all 11672 required entries. One representative per support +gives `I_49`, so the rank is exactly 49 over every field. Ranks mod 2, 3 and 101 +are also computed as a cross-check. + +## Lower bound: proof + +**Lemma (C5 core).** Let `P0..P4` be planes such that `Pi,Pj` are orthogonal +exactly when `j=i+-1 (mod 5)`. Then every fitting matrix restricted to their +ten ports has rank at least 5, over every field. + +*Proof.* Assume the 10-by-10 principal submatrix `M` has rank at most 4. Let +the ports of `P0,P1,P2,P3,P4` be `A1,A2`, `B1,B2`, `C1,C2`, `D1,D2`, `E1,E2`. +`P0` and `P2` are non-orthogonal, so `M[A1,A2,C1,C2]=I_4`. Hence `rank M=4`, and +`M=UV^T` with `U,V` of size `10 x 4`. The rows `u_A1,u_A2,u_C1,u_C2` are a basis. +Replace `U` by `U U_0^{-1}` and `V` by `V U_0^T`, where `U_0` is that basis +block. This makes those rows `e1..e4`, and then their `v` rows are also `e1..e4`. + +`P3` is non-orthogonal to `P0`, so `M[A,D]=0` and `v_D` is in `span(e3,e4)`. +`M[D,D]=I_2` makes `v_D1,v_D2` independent, so they span `span(e3,e4)`. +Likewise, `P4` is non-orthogonal to `P2`, so `v_E1,v_E2` span `span(e1,e2)`. +`P1` is non-orthogonal to both `P3` and `P4`, so `u_B1` is orthogonal (in the +standard bilinear pairing) to `span(e1..e4)`. Hence `u_B1=0`. That contradicts +`M[B1,B1]=1`. QED. (The lemma uses all five non-orthogonal pairs of the cycle and +only one port of `P1`.) + +**Theorem.** Let the core be the planes `(13, 23, 35, 16, 34)`, in cycle order. +These planes form an induced 5-cycle of the orthogonality graph. Let `Q` be +these 22 planes: + +```text +0 4 8 17 18 19 20 21 24 26 28 29 32 36 38 39 41 42 43 45 46 52 +``` + +The planes of `Q` are pairwise non-orthogonal, and each is non-orthogonal to all +five core planes. For every fitting `K` over every field, the principal +submatrix on the 44 ports of `Q` and the 10 core ports equals +`I_44 (+) M`, because every cross entry is a forced zero. Hence +`rank K >= 44 + rank M >= 44 + 5 = 49`. + +The fractional clique explains this. Weight 1 on `Q` and 1/2 on the core sums to +24.5. `verify.py` checks every premise of the theorem from the reconstructed +mask. The stored LP dual is an alternative optimal fractional clique; it also +sums to 49/2 but has a different support. + +`verify.py` also corroborates the lemma by exhaustive search. Over GF(2) and +GF(3), the normalised C5 pattern has **no** rank-4 completion. As a control, +freeing the `P1-P3` entries makes a GF(2) rank-4 completion appear, as the proof +predicts. These finite searches are corroboration only. The every-field claim +rests on the proof above. + +## Reproduce + +From the repository root, with Python 3.12 or 3.14 and only the standard library: + +```sh +python3 -I -B research/paired-plane-minrank-bracket-audit/verify.py +``` + +Expected: a JSON result line, then `PASS_PAIRED_PLANE_MINRANK_EXACT_49`. This +takes about 2 s. The registered hooks are +`python3 scripts/research_package.py --package research/paired-plane-minrank-bracket-audit --check-only` +and the same command without `--check-only` under Python 3.12. The optional +supplementary cross-check +`python3 -I -B research/paired-plane-minrank-bracket-audit/verify.py --two-fold-dp` +prints `PASS_TWO_FOLD_DP_CHI2_49`. It took 72 s and 822 MB peak RSS on this +machine (3,040,597 DP states), so it is not part of the registered replay. +`--write-certificate` regenerates `CERTIFICATE.json` deterministically. The +default mode compares every recomputed check with the stored certificate. + +Validated locally with CPython 3.14.4 on Linux: the default verifier, the +optional two-fold DP, the metadata/pin check (`--check-only`) and +`python3 -B -m unittest discover -s tests -p 'test_research_*.py'` (65 tests, +OK). No Python 3.12 interpreter was available locally, so the registered 3.12 +replay hook was not run here. Certificate tampering was also tested locally. +Each of these edits was rejected: an emptied support, a non-clique `Q`, a raised +`y` weight, a stored `chi=24`, a non-induced core and a truncated DP order. + +**Negative controls (must be rejected; recorded in `CERTIFICATE.json`):** + +- a flipped byte in the PR1825 certificate (sha256 pin); +- PR2471's 25 classes merged to 24 (`[36]+[45]`, non-orthogonal); +- a rank-49 support holding both ports of one plane; +- a half weight of the fractional clique raised to 1; +- a fractional colouring with one set dropped; +- a `Q` plane replaced by a plane orthogonal to a core plane; +- the core listed out of cycle order. + +Solver controls: on the orthogonality graphs `C5` and `C7`, the DPs return +`(omega, chi, chi_2) = (2,3,5)` and `(3,4,7)`. + +## Sources and pins + +- Base commit `0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2`; see `SOURCES.json` + for Git blobs and SHA256 values. +- `research/community-frontier1094-audit/selected-replay.tar.gz`, sha256 + `f1da8061...d529d6`. The member + `candidate/strict/global/base/work/complex-nine-native/DATA-PHASES.json` has + sha256 `c5916ff3...8251fa` and supplies the labels. +- `research/paired-plane-scalar-mask-obstruction/PR1825-CERTIFICATE.json`, + sha256 `4fd648f7...1473b1`, supplies the matching. +- PR2471's witnesses are copied into `verify.py` and re-checked there, not + trusted. They come from `research/paired-plane-scalar-rank-floor/CERTIFICATE.json` + at PR head `5a7c2b6`, Git blob `1d8a21f3713f2b883ae65d655126732e4f5d54ff`. + No code from PR2471 or any other package is imported. + +## Scope, inherited assumptions, unresolved obligations + +- The scope is a finite algebraic statement about one fixed mask. Inherited + assumptions: PR1825's matching (as pinned by PR1889's fixture) and PR1889's + strict mask semantics, exactly as stated in PR2471's "Exact model and proof". + A different matching, a relaxed mask (for example, allowing same-plane + off-diagonal entries) or a different endpoint contract can change the answer. +- Channel count is not a native copy cost. As PR2471 and PR2203 note, fifty or + forty-nine scalar channels do not imply any physical saving. No kappa is + claimed or implied. +- The every-field lower bound rests on the short hand proof above. The verifier + checks its combinatorial premises exactly and corroborates the lemma over + GF(2) and GF(3) by exhaustive search. The lemma is not machine-formalised. + +## Open next questions + +1. **Native realisation of 49 channels.** Can a fully charged native + implementation realise a 49-channel scalar fit of this mask below the + two-unpaid-coordinate budget? This is PR2471's open question 2. + *Why it matters:* only a native cost can move a supplier price, and 49 is + now the exact scalar floor. *First step:* price the explicit 49-support fit + under PR2203's both-payload accounting, including pairing-rank costs and + scratch restoration. *Blocked by:* there is no accepted native cost model for + scalar channels of this endpoint. +2. **Other matchings.** Does another perfect matching of the 112 ports into + nondegenerate planes give a smaller exact fitting rank? *Why it matters:* + the extra channel above `2*omega` comes from an odd-cycle core; a matching + whose plane graph has `chi_f = omega` and no such core could reach + `2*omega`. *First step:* reuse this verifier's model, LP and DP functions on + restricted rematches (for example PR2118's local rematch, or the plane + choices in Discussion 1587). *Blocked by:* the space of matchings is large, + so a restricted search class is needed first. + +These are also recorded in `TASK.json`. + +## Credit + +Predecessors: ywz65 (PR2471: model, bracket and witnesses audited here); Cinna +Davis (PR1825 matched planes, PR2126 scalar identity fit); Adam Gall (PR1889 +strict mask); JeremyDiviney (PR2203 native payload accounting); Philippe Van +Velzen (Discussion 1587: orthogonal classes have at most 4 planes; here the +exact maximum is 3); JosieElliston (PR1977, submatrix-minrank method; the +lower bound here is a principal-submatrix argument in that spirit). + +Prepared by thakrarsagar with substantial AI assistance from Claude (Anthropic, +Claude Opus 5.5). Apache-2.0. diff --git a/research/paired-plane-minrank-bracket-audit/SOURCES.json b/research/paired-plane-minrank-bracket-audit/SOURCES.json new file mode 100644 index 0000000000..17f64482c0 --- /dev/null +++ b/research/paired-plane-minrank-bracket-audit/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "e8870e5917057d59b730eb14721a778639eca050", + "sha256": "d46eb6d5b3e279428753d770653663fbdf1063e55c255ea073d768f344927ef7" + }, + { + "path": "research/community-frontier1094-audit/selected-replay.tar.gz", + "usage": "input", + "git_blob": "c24daf067f9c543421d89ca2eeaa4eb78a57fb6f", + "sha256": "f1da80610bf33c58527f18ad63b4350d0b864e1d4486141ee17ac9bed4d529d6" + }, + { + "path": "research/paired-plane-scalar-mask-obstruction/PR1825-CERTIFICATE.json", + "usage": "input", + "git_blob": "7ca668d7d50c7276e89b0f6f9575e1b9f1ad9ef6", + "sha256": "4fd648f7b5178bff5441bf364d58234b7bc1a43b924bc6da03013c948f1473b1" + } + ] +} diff --git a/research/paired-plane-minrank-bracket-audit/TASK.json b/research/paired-plane-minrank-bracket-audit/TASK.json new file mode 100644 index 0000000000..7e6694d90e --- /dev/null +++ b/research/paired-plane-minrank-bracket-audit/TASK.json @@ -0,0 +1,66 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 4, + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "original_card": { + "id": "uniform-transfer-audit", + "question": "Can one exact all-size/compiler, precision, hosting or restoration implication be proved or falsified?", + "starting_points": [ + "certificates/selected-result.json", + "docs/audit.md" + ], + "methods": [ + "Prove one missing implication with explicit quantified hypotheses.", + "Find an exact counterexample at the claimed interface boundary." + ], + "acceptance_gate": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read the selected review scope and choose one exact all-size or precision implication.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Write its quantified inputs and conclusion; find a missing hypothesis or construct a minimal exact adversarial instance.", + "bottleneck_link": "Finite supplier improvements are useful only under the retained transfer obligations.", + "allowed_variations": [ + "Choose one tape, precision, hosting or restoration lemma." + ], + "scope_change_triggers": [ + "Replacing a quantified obligation with another finite smoke test." + ], + "overlap_terms": [ + "uniform transfer", + "all-size", + "precision" + ] + }, + "scope_status": "changed", + "actual_scope": "Audit and resolve PR2471's open question 1 for its exact fixed object: the minimum rank, over an arbitrary field, of a scalar fitting matrix for the strict PR1889 mask on PR1825's 56 matched P112 planes (PR2471 head 5a7c2b681b79d5b5e25fac62aa4bad908525b5ca claims the bracket [48,50]). Independently reconstruct the mask, re-check PR2471's witnesses, decide chi and the port-level 2-fold chromatic number of the plane non-orthogonality graph, and close the bracket if possible.", + "scope_change_reason": "The generic card targets selected-stock all-size/precision/hosting/restoration implications. This session audits one concrete fresh proposed bracket (PR2471, no reviewer yet) with an explicit open question. The narrowing to colourings and minrank was chosen because PR2471's upper witness (2*chi) is not the best disjoint-support bound (that is the 2-fold chromatic number), and an exact decision is cheap and checkable.", + "bottleneck_link": "Side result for the paired-plane scalar-endpoint line (PR1825/PR1889/PR2126/PR2203/PR2471): it fixes the exact scalar channel count of one necessary endpoint obligation. It is not a native copy price and does not change any kappa or the selected result.", + "budget_minutes": 90, + "stop_rule": "Each exact search capped at about 10 CPU-minutes (nice, single process, <1.5 GB); stop at the experiment deadline 2026-10-15T13:01:24Z. All searches finished well inside the cap (default verifier about 2 s; optional two-fold DP about 2 CPU-minutes).", + "outcome": "completed", + "evidence": "verify.py (stdlib, exact): omega(G)=24 (194 maximum cliques), chi(G)=25 (exact DP), fractional chi(G)=49/2 (exact primal and dual LP certificates), explicit 0/1 rank-49 fit (49 disjoint supports, 11672 mask entries, I_49 on representatives), rank lower bound 49 over every field from a 22-plane clique plus an induced 5-cycle core (proof in README; finite corroboration over GF(2), GF(3)), 7 negative controls rejected, solver controls on C5/C7. Hence the minimum scalar fitting rank is exactly 49 over every field.", + "author": "thakrarsagar", + "ai_assistance": "Substantial AI assistance from Claude (Anthropic, Claude Opus 5.5) in search design, proof, code and writing; directed and submitted by thakrarsagar. No independent human review is claimed.", + "open_questions": [ + { + "question": "Can a fully charged native implementation realize a 49-channel scalar fit of this mask below the two-unpaid-coordinate budget (PR2471 open question 2)?", + "why_it_matters": "Only a native cost, not a channel count, can affect a supplier price; rank 49 is now the exact scalar floor for this fixed matching.", + "first_step": "Price the explicit 49-support fit here under PR2203's both-payload accounting, including pairing-rank costs and scratch restoration.", + "blocked_by": "No accepted native cost model for scalar channels of this endpoint; PR2203/PR2471 remain unreviewed." + }, + { + "question": "Does a different perfect matching of the 112 P112 ports into nondegenerate planes give a plane graph with a smaller exact fitting rank (for example omega = chi_f, no odd-cycle core)?", + "why_it_matters": "The 49 floor is specific to PR1825's matching; the C5-core argument shows exactly which plane configurations force the extra channel.", + "first_step": "Reuse verify.py's model/LP/DP functions on alternative matchings (Discussion 1587 lists other plane choices) and compare 2*omega, chi_f, chi_2.", + "blocked_by": "Enumerating matchings is large; a restricted search class (local rematches as in PR2118) is needed first." + } + ] +} diff --git a/research/paired-plane-minrank-bracket-audit/VERIFY.json b/research/paired-plane-minrank-bracket-audit/VERIFY.json new file mode 100644 index 0000000000..91dc102e34 --- /dev/null +++ b/research/paired-plane-minrank-bracket-audit/VERIFY.json @@ -0,0 +1,22 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/community-frontier1094-audit/selected-replay.tar.gz", + "research/paired-plane-scalar-mask-obstruction/PR1825-CERTIFICATE.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Pinned source sha256; independent mask reconstruction; PR2471 clique/class witnesses; exact omega, chi (DP), chi_f=49/2 LP certificates; rank-49 0/1 fit on all 11672 required entries and ranks mod 2/3/101; rank-49 lower-bound premises (22-clique + induced C5 core); C5 lemma corroboration over GF(2)/GF(3) with a freed-constraint control; DP solver controls on C5/C7; seven negative controls that must be rejected." + } + ] +} diff --git a/research/paired-plane-minrank-bracket-audit/verify.py b/research/paired-plane-minrank-bracket-audit/verify.py new file mode 100644 index 0000000000..f2bd5ef72d --- /dev/null +++ b/research/paired-plane-minrank-bracket-audit/verify.py @@ -0,0 +1,621 @@ +#!/usr/bin/env python3 +"""Exact minimum scalar fitting rank (49) for PR1825's fixed 56 matched planes. + +Independent stdlib re-implementation (no code imported from PR2471 or any +other package). Default mode recomputes everything from the pinned sources and +compares with CERTIFICATE.json; ``--write-certificate`` regenerates it. + +Prepared by thakrarsagar with substantial AI assistance from Claude +(Anthropic, Claude Opus 5.5). Apache-2.0. +""" +import hashlib +import io +import itertools +import json +import sys +import tarfile +from fractions import Fraction +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +ARCHIVE = 'research/community-frontier1094-audit/selected-replay.tar.gz' +ARCHIVE_SHA = 'f1da80610bf33c58527f18ad63b4350d0b864e1d4486141ee17ac9bed4d529d6' +MEMBER = 'candidate/strict/global/base/work/complex-nine-native/DATA-PHASES.json' +MEMBER_SHA = 'c5916ff312678f12aba403847643fbbc29f643acec60bdf836fa56cd3e8251fa' +MATCHING = 'research/paired-plane-scalar-mask-obstruction/PR1825-CERTIFICATE.json' +MATCHING_SHA = '4fd648f7b5178bff5441bf364d58234b7bc1a43b924bc6da03013c948f1473b1' +CERT = HERE / 'CERTIFICATE.json' + +# PR2471 (ywz65) witnesses, copied verbatim from +# research/paired-plane-scalar-rank-floor/CERTIFICATE.json at PR head +# 5a7c2b681b79d5b5e25fac62aa4bad908525b5ca (git blob +# 1d8a21f3713f2b883ae65d655126732e4f5d54ff); re-checked here, not trusted. +PR2471_CLIQUE = [2, 6, 8, 17, 18, 19, 21, 22, 24, 28, 29, 34, 35, 36, 38, 39, + 41, 42, 43, 45, 46, 51, 52, 53] +PR2471_CLASSES = [[0, 1, 2], [6, 13], [5, 8, 9], [17, 40], [3, 18, 25], + [19, 50], [21, 44], [20, 22], [10, 24, 30], [28, 31], + [11, 29], [16, 34, 54], [23, 35], [36], [15, 38], + [14, 33, 39], [27, 41], [42, 55], [43, 47], [45], + [12, 46, 48], [26, 49, 51], [52], [32, 37, 53], [4, 7]] + + +class CheckFailure(Exception): + pass + + +def need(ok, why): + if not ok: + raise CheckFailure(why) + + +def sha(data): + return hashlib.sha256(data).hexdigest() + + +def parity_dot(x, y): + return bin(x & y).count('1') % 2 + + +# ---------------------------------------------------------------- model +def load_model(archive_bytes, matching_bytes): + """Return (labels[112], pairs[56], orth[56][56]) from the pinned sources. + orth[i][j] is True iff i != j and all four basis pairings vanish.""" + need(sha(archive_bytes) == ARCHIVE_SHA, 'archive sha256 mismatch') + need(sha(matching_bytes) == MATCHING_SHA, 'PR1825 certificate sha256 mismatch') + with tarfile.open(fileobj=io.BytesIO(archive_bytes), mode='r:gz') as tar: + handle = tar.extractfile(MEMBER) + need(handle is not None, 'archive member missing') + member = handle.read() + need(sha(member) == MEMBER_SHA, 'DATA-PHASES member sha256 mismatch') + by_port = {} + for row in json.loads(member)['recipes']: + need(row['port'] not in by_port, 'duplicate port') + by_port[row['port']] = row['q'] + need(sorted(by_port) == list(range(112)), 'ports must be 0..111') + labels = [by_port[p] for p in range(112)] + need(all(0 < q < 512 for q in labels) and len(set(labels)) == 112, 'labels: distinct, nonzero, in F2^9') + pairs = [list(p) for p in json.loads(matching_bytes)['matching']] + need(len(pairs) == 56 and sorted(x for p in pairs for x in p) == list(range(112)), + 'matching must partition the 112 ports into 56 pairs') + for a, b in pairs: + need(parity_dot(labels[a], labels[a]) == 1 and parity_dot(labels[b], labels[b]) == 1 + and parity_dot(labels[a], labels[b]) == 0, 'matched plane must have Gram I2') + basis = [(labels[a], labels[b]) for a, b in pairs] + orth = [[i != j and all(parity_dot(x, y) == 0 for x in basis[i] for y in basis[j]) + for j in range(56)] for i in range(56)] + return labels, pairs, orth + + +def orthogonal_sets(orth): + """All nonempty sets of pairwise orthogonal distinct planes (independent sets of G).""" + n = len(orth) + out = [(v,) for v in range(n)] + layer = list(out) + while layer: + grown = [s + (j,) for s in layer for j in range(s[-1] + 1, n) if all(orth[t][j] for t in s)] + out.extend(grown) + layer = grown + return out + + +# ------------------------------------------------- exact path-order DPs +def frontiers(order, nbrs): + pos = {v: i for i, v in enumerate(order)} + return [[u for u in order[i:] if any(pos[w] < i for w in nbrs[u])] + for i in range(len(order) + 1)], pos + + +def clique_number_dp(orth, order): + """Exact clique number of G (planes adjacent iff non-orthogonal) = independence + number of the orthogonality graph, with the count of maximum cliques; DP along + a vertex order whose state is the set of blocked frontier vertices.""" + n = len(orth) + nbrs = [set(j for j in range(n) if orth[i][j]) for i in range(n)] + fr, _ = frontiers(order, nbrs) + memo = {} + + def rec(i, blocked): + if i == n: + return {0: 1} + key = (i, blocked) + if key in memo: + return memo[key] + v = order[i] + keep = set(fr[i + 1]) + res = dict(rec(i + 1, frozenset(u for u in blocked if u in keep))) + if v not in blocked: + for k, c in rec(i + 1, frozenset(u for u in (blocked | nbrs[v]) if u in keep)).items(): + res[k + 1] = res.get(k + 1, 0) + c + memo[key] = res + return res + + counts = rec(0, frozenset()) + top = max(counts) + return top, counts[top], len(memo) + + +def b_fold_savings_dp(orth, order, b): + """Exact b-fold chromatic number of G: choose a multiset of orthogonal sets of + size >= 2, each plane in at most b of them, maximising sum(|S|-1); then + chi_b(G) = b*n - max savings (remaining slots are singleton classes).""" + n = len(orth) + nbrs = [set(j for j in range(n) if orth[i][j]) for i in range(n)] + fr, pos = frontiers(order, nbrs) + own = [[] for _ in range(n)] + for s in orthogonal_sets(orth): + if len(s) >= 2: + ordered = tuple(sorted(s, key=lambda v: pos[v])) + own[pos[ordered[0]]].append(ordered) + memo = {} + + def options(i, state): + caps = dict(zip(fr[i], state)) + nxt = fr[i + 1] + opts = own[i] + out = [] + + def walk(k, left, cur, gain): + if k == len(opts): + out.append((gain, tuple(cur.get(u, b) for u in nxt))) + return + s = opts[k] + for m in range(min([left] + [cur.get(u, b) for u in s[1:]]) + 1): + cur2 = cur + if m: + cur2 = dict(cur) + for u in s[1:]: + cur2[u] = cur.get(u, b) - m + walk(k + 1, left - m, cur2, gain + m * (len(s) - 1)) + walk(0, caps.get(order[i], b), caps, 0) + return out + + def rec(i, state): + if i == n: + return 0 + key = (i, state) + got = memo.get(key) + if got is None: + got = max(g + rec(i + 1, ns) for g, ns in options(i, state)) + memo[key] = got + return got + + return rec(0, ()), len(memo) + + +# ------------------------------------------------------------ checks +def owner_map(pairs): + return {p: k for k, pr in enumerate(pairs) for p in pr} + + +def check_fitting_supports(supports, pairs, orth): + """K = sum_S 1_S 1_S^T fits the strict mask iff the supports partition the + ports and every support joins only ports of distinct pairwise orthogonal planes.""" + owner = owner_map(pairs) + need(sorted(p for s in supports for p in s) == list(range(112)), 'supports must partition the 112 ports') + need(all(s for s in supports), 'supports must be nonempty') + for s in supports: + for a in s: + for c in s: + need(a == c or orth[owner[a]][owner[c]], + 'support joins ports %d,%d of non-orthogonal or equal planes' % (a, c)) + return len(supports) + + +def dense_from_supports(supports): + k = [[0] * 112 for _ in range(112)] + for s in supports: + for a in s: + for c in s: + k[a][c] += 1 + return k + + +def check_mask_entries(matrix, pairs, orth): + owner = owner_map(pairs) + required = 0 + for i in range(112): + for j in range(112): + if i == j or not orth[owner[i]][owner[j]]: + need(matrix[i][j] == int(i == j), 'mask entry violated at %d,%d' % (i, j)) + required += 1 + return required + + +def rank_mod_p(matrix, p): + m = [[x % p for x in row] for row in matrix] + rank = 0 + for c in range(len(m[0])): + piv = next((r for r in range(rank, len(m)) if m[r][c]), None) + if piv is None: + continue + m[rank], m[piv] = m[piv], m[rank] + inv = pow(m[rank][c], p - 2, p) + m[rank] = [x * inv % p for x in m[rank]] + for r in range(len(m)): + if r != rank and m[r][c]: + f = m[r][c] + m[r] = [(x - f * z) % p for x, z in zip(m[r], m[rank])] + rank += 1 + return rank + + +def check_fractional(sets, y, x, n): + """y: fractional clique of G (every orthogonal set has y-weight <= 1); + x: fractional colouring (weights on orthogonal sets covering each plane >= 1).""" + need(len(y) == n and all(w >= 0 for w in y), 'y must be nonnegative on all planes') + for s in sets: + need(sum(y[v] for v in s) <= 1, 'fractional clique violated on %s' % (s,)) + allowed = set(sets) + cover = [Fraction(0)] * n + for s, w in x: + need(tuple(s) in allowed and w > 0, 'x must use orthogonal sets with positive weight') + for v in s: + cover[v] += w + need(all(c >= 1 for c in cover), 'fractional colouring must cover every plane') + return sum(y), sum(w for _, w in x) + + +def lower_bound_premises(core, clique22, orth): + """Premises of the rank lower bound (README, Lemma + Theorem): core = (P0..P4) is + an induced 5-cycle of the orthogonality graph; clique22 is a set of planes that + are pairwise non-orthogonal and non-orthogonal to all five core planes.""" + need(len(core) == 5 and len(set(core)) == 5, 'core must be 5 distinct planes') + for i in range(5): + for j in range(i + 1, 5): + need(orth[core[i]][core[j]] == ((j - i) % 5 in (1, 4)), + 'core is not an induced 5-cycle at %d,%d' % (core[i], core[j])) + need(len(set(clique22)) == len(clique22) and not set(clique22) & set(core), 'Q distinct, disjoint from core') + for a in clique22: + for c in clique22: + need(a == c or not orth[a][c], 'Q not pairwise non-orthogonal at %d,%d' % (a, c)) + for c in core: + need(not orth[a][c], 'Q plane %d orthogonal to core plane %d' % (a, c)) + return 2 * len(clique22) + 5 + + +def c5_rank4_search(p, relax_13=False): + """Finite corroboration of the C5 lemma over GF(p) (not needed by the proof): + search for a rank-4 factorisation K=UV^T of the 10-port C5 blow-up mask after + the WLOG normalisation u=v=e1..e4 on the ports of P0 (A) and P2 (C). Returns + 1 if a completion exists, else 0 (exhaustive). relax_13 makes P1-P3 entries + free (control: a completion must then exist).""" + vecs = list(itertools.product(range(p), repeat=4)) + e = [tuple(int(i == j) for j in range(4)) for i in range(4)] + plane = {'A1': 0, 'A2': 0, 'C1': 2, 'C2': 2, 'B1': 1, 'B2': 1, 'D1': 3, 'D2': 3, 'E1': 4, 'E2': 4} + placed = {'A1': (e[0], e[0]), 'A2': (e[1], e[1]), 'C1': (e[2], e[2]), 'C2': (e[3], e[3])} + + def ip(a, c): + return sum(s * t for s, t in zip(a, c)) % p + + def free(x, z): + a, c = plane[x], plane[z] + if a == c: + return False + if relax_13 and {a, c} == {1, 3}: + return True + return (a - c) % 5 in (1, 4) + todo = ['D1', 'D2', 'E1', 'E2', 'B1', 'B2'] + + def rec(k): + if k == len(todo): + return True + name = todo[k] + for u in vecs: + if any(not free(name, o) and ip(u, placed[o][1]) for o in placed): + continue + for v in vecs: + if ip(u, v) != 1 or any(not free(o, name) and ip(placed[o][0], v) for o in placed): + continue + placed[name] = (u, v) + if rec(k + 1): + return True + del placed[name] + return False + return int(rec(0)) + + +# ------------------------------------------------------------- build +def exact_lp(orth): + """Exact Bland-rule simplex for max sum y s.t. y(S) <= 1 for every orthogonal set S. + Returns (y, x) with x the dual (fractional colouring) read from reduced costs.""" + sets = orthogonal_sets(orth) + n, m = len(orth), len(sets) + rows = [] + for r, s in enumerate(sets): + row = [Fraction(0)] * (n + m + 1) + for v in s: + row[v] = Fraction(1) + row[n + r] = row[-1] = Fraction(1) + rows.append(row) + obj = [Fraction(-1)] * n + [Fraction(0)] * (m + 1) + basis = [n + r for r in range(m)] + while True: + col = next((j for j in range(n + m) if obj[j] < 0), None) + if col is None: + break + best = None + for r in range(m): + if rows[r][col] > 0: + ratio = rows[r][-1] / rows[r][col] + if best is None or ratio < best[0] or (ratio == best[0] and basis[r] < basis[best[1]]): + best = (ratio, r) + r = best[1] + a = rows[r][col] + rows[r] = [z / a for z in rows[r]] + nz = [j for j, z in enumerate(rows[r]) if z] + for rr in range(m): + if rr != r and rows[rr][col]: + f = rows[rr][col] + for j in nz: + rows[rr][j] -= f * rows[r][j] + f = obj[col] + for j in nz: + obj[j] -= f * rows[r][j] + basis[r] = col + y = [Fraction(0)] * n + for r, bcol in enumerate(basis): + if bcol < n: + y[bcol] = rows[r][-1] + x = [(list(s), obj[n + r]) for r, s in enumerate(sets) if obj[n + r]] + return y, x + + +def supports_from_half_integral(x, pairs): + classes = [] + for s, w in x: + need((2 * w).denominator == 1, 'primal not half-integral') + classes.extend([list(s)] * int(2 * w)) + used = [0] * len(pairs) + supports = [] + for s in classes: + sup = [] + for v in s: + if used[v] < 2: + sup.append(pairs[v][used[v]]) + used[v] += 1 + if sup: + supports.append(sorted(sup)) + return supports + + +def max_clique_simple(cands, orth): + best = [] + + def rec(chosen, pool): + nonlocal best + if len(chosen) + len(pool) <= len(best): + return + if not pool: + best = chosen[:] + return + v = pool[0] + rec(chosen + [v], [u for u in pool[1:] if not orth[v][u]]) + rec(chosen, pool[1:]) + rec([], sorted(cands)) + return best + + +def find_core(orth): + """Induced 5-cycles of the orthogonality graph, each with a maximum clique of G + inside the common non-orthogonal neighbourhood; return the best.""" + n = len(orth) + nb = [set(j for j in range(n) if orth[i][j]) for i in range(n)] + best = None + for a in range(n): + for b in sorted(nb[a]): + for c in sorted(nb[b] - nb[a] - {a}): + for d in sorted(nb[c] - nb[a] - nb[b] - {a, b}): + for e in sorted(nb[d] - nb[b] - nb[c] - {a, b, c}): + if a not in nb[e] or a != min(a, b, c, d, e) or b > e: + continue + cyc = (a, b, c, d, e) + common = [v for v in range(n) if v not in cyc and all(not orth[v][z] for z in cyc)] + q = max_clique_simple(common, orth) + if best is None or len(q) > len(best[1]): + best = (list(cyc), sorted(q)) + return best + + +def greedy_order(orth): + n = len(orth) + nbrs = [set(j for j in range(n) if orth[i][j]) for i in range(n)] + best = None + for start in range(n): + order, placed, rest = [start], {start}, set(range(n)) - {start} + while rest: + def key(u): + fr = set(w for z in placed | {u} for w in nbrs[z] if w not in placed and w != u) + return (len(fr), -len(nbrs[u] & placed), u) + u = min(rest, key=key) + order.append(u) + placed.add(u) + rest.remove(u) + width = max(len(f) for f in frontiers(order, nbrs)[0]) + if best is None or width < best[0]: + best = (width, order) + return best[1] + + +# ------------------------------------------------------------- main +def run_checks(cert, pairs, orth): + n = 56 + sets = orthogonal_sets(orth) + sizes = {} + for s in sets: + sizes[str(len(s))] = sizes.get(str(len(s)), 0) + 1 + out = {'orthogonal_set_counts_by_size': sizes, + 'nonorthogonal_plane_pairs': sum(1 for i in range(n) for j in range(i + 1, n) if not orth[i][j])} + # PR2471 witnesses, re-checked against the independent reconstruction + need(len(set(PR2471_CLIQUE)) == 24 and all(not orth[a][c] for a in PR2471_CLIQUE + for c in PR2471_CLIQUE if a != c), 'PR2471 clique') + need(len(PR2471_CLASSES) == 25 and sorted(v for c in PR2471_CLASSES for v in c) == list(range(n)), + 'PR2471 classes must partition the planes') + pr_supports = [[pairs[v][slot] for v in cl] for cl in PR2471_CLASSES for slot in (0, 1)] + check_fitting_supports(pr_supports, pairs, orth) + out['pr2471_witnesses_rechecked'] = {'plane_clique_24_pairwise_nonorthogonal': True, + 'orthogonal_classes_25_rank50_fit': True} + order = cert['dp_vertex_order'] + need(sorted(order) == list(range(n)), 'order must be a permutation') + omega, count, states = clique_number_dp(orth, order) + out['omega'] = {'value': omega, 'maximum_clique_count': count, 'dp_states': states} + save1, states1 = b_fold_savings_dp(orth, order, 1) + out['chi'] = {'value': n - save1, 'max_savings_b1': save1, 'dp_states': states1} + y = [Fraction(w) for w in cert['fractional_clique_y']] + x = [(s, Fraction(w)) for s, w in cert['fractional_colouring_x']] + ysum, xsum = check_fractional(sets, y, x, n) + need(ysum == xsum, 'LP certificates must meet') + out['chi_f'] = str(ysum) + supports = cert['rank49_supports'] + count49 = check_fitting_supports(supports, pairs, orth) + dense = dense_from_supports(supports) + required = check_mask_entries(dense, pairs, orth) + reps = [s[0] for s in supports] + need(all(dense[a][c] == int(a == c) for a in reps for c in reps), 'representatives must give identity') + out['rank49_fit'] = {'supports': count49, 'required_entries_checked': required, + 'rank_mod_2': rank_mod_p(dense, 2), 'rank_mod_3': rank_mod_p(dense, 3), + 'rank_mod_101': rank_mod_p(dense, 101)} + out['rank_lower_bound'] = lower_bound_premises(cert['c5_core'], cert['clique22'], orth) + y_alt = [Fraction(1) if v in cert['clique22'] else Fraction(1, 2) if v in cert['c5_core'] else Fraction(0) + for v in range(n)] + out['lower_bound_fractional_clique_sum'] = str(check_fractional(sets, y_alt, x, n)[0]) + out['solver_controls'] = solver_controls() + out['c5_lemma_finite_corroboration'] = { + 'gf2_rank4_completion_exists': c5_rank4_search(2), + 'gf3_rank4_completion_exists': c5_rank4_search(3), + 'gf2_control_P1P3_freed_completion_exists': c5_rank4_search(2, relax_13=True)} + return out + + +def cycle_orth(k): + return [[(i - j) % k in (1, k - 1) for j in range(k)] for i in range(k)] + + +def solver_controls(): + """Known answers for the two DPs: if the orthogonality graph is the cycle C_k + (k odd), G is its complement, omega(G)=alpha(C_k)=(k-1)/2, chi(G)=(k+1)/2 and + chi_2(G)=k. A DP that ignored constraints or capacities would miss these.""" + out = {} + for k in (5, 7): + orth = cycle_orth(k) + order = list(range(k)) + omega = clique_number_dp(orth, order)[0] + chi = k - b_fold_savings_dp(orth, order, 1)[0] + chi2 = 2 * k - b_fold_savings_dp(orth, order, 2)[0] + need((omega, chi, chi2) == ((k - 1) // 2, (k + 1) // 2, k), 'DP control failed on C%d' % k) + out['C%d' % k] = [omega, chi, chi2] + return out + + +def negative_controls(cert, pairs, orth, archive_bytes, matching_bytes): + results = {} + + def expect_fail(name, fn): + try: + fn() + except CheckFailure as exc: + results[name] = 'rejected: ' + str(exc) + return + raise SystemExit('NEGATIVE CONTROL ACCEPTED: ' + name) + bad = bytearray(matching_bytes) + bad[len(bad) // 2] ^= 1 + expect_fail('tampered_PR1825_certificate_byte', lambda: load_model(archive_bytes, bytes(bad))) + merged = [c[:] for c in PR2471_CLASSES] + merged[13] = merged[13] + merged.pop(19) # [36] + [45]: a 24-class plane partition + expect_fail('pr2471_classes_merged_to_24', lambda: check_fitting_supports( + [[pairs[v][s] for v in cl] for cl in merged for s in (0, 1)], pairs, orth)) + sup = [s[:] for s in cert['rank49_supports']] + owner = owner_map(pairs) + port = sup[0][0] + partner = [q for q in pairs[owner[port]] if q != port][0] + src = next(k for k, s in enumerate(sup) if partner in s) + sup[src].remove(partner) + sup[0].append(partner) + sup = [s for s in sup if s] + expect_fail('rank_fit_both_ports_of_one_plane_in_one_support', + lambda: check_fitting_supports(sup, pairs, orth)) + sets = orthogonal_sets(orth) + y = [Fraction(w) for w in cert['fractional_clique_y']] + k = next(i for i, w in enumerate(y) if w == Fraction(1, 2)) + y2 = y[:] + y2[k] = Fraction(1) + x = [(s, Fraction(w)) for s, w in cert['fractional_colouring_x']] + expect_fail('fractional_clique_half_weight_raised_to_1', lambda: check_fractional(sets, y2, x, 56)) + x2 = x[:-1] + expect_fail('fractional_colouring_set_dropped', lambda: check_fractional(sets, y, x2, 56)) + swap = next(v for v in range(56) if v not in cert['clique22'] and v not in cert['c5_core'] + and any(orth[v][c] for c in cert['c5_core'])) + expect_fail('Q_plane_replaced_by_core_neighbour', + lambda: lower_bound_premises(cert['c5_core'], cert['clique22'][:-1] + [swap], orth)) + core = cert['c5_core'] + expect_fail('core_reordered_not_a_cycle', + lambda: lower_bound_premises([core[0], core[2], core[1], core[3], core[4]], cert['clique22'], orth)) + return results + + +def result_block(checks): + need(checks['omega']['value'] == 24 and checks['chi']['value'] == 25, 'omega/chi') + need(checks['chi_f'] == '49/2', 'chi_f') + need(checks['rank49_fit']['supports'] == 49 and checks['rank49_fit']['rank_mod_2'] == 49 + and checks['rank49_fit']['rank_mod_3'] == 49, 'rank-49 fit') + need(checks['rank_lower_bound'] == 49 and checks['lower_bound_fractional_clique_sum'] == '49/2', 'lower bound') + c5 = checks['c5_lemma_finite_corroboration'] + need(c5['gf2_rank4_completion_exists'] == 0 and c5['gf3_rank4_completion_exists'] == 0 + and c5['gf2_control_P1P3_freed_completion_exists'] == 1, 'C5 corroboration') + return {'omega_G': 24, 'chi_G': 25, 'fractional_chi_G': '49/2', 'two_fold_chi_G': 49, + 'min_scalar_fitting_rank': 49, + 'field_scope': 'every field: lower bound by the C5 lemma proof in README, upper bound by an explicit 0/1 ' + 'disjoint-support matrix; finite corroboration of the lemma over GF(2) and GF(3) only'} + + +def main(argv): + archive_bytes = (ROOT / ARCHIVE).read_bytes() + matching_bytes = (ROOT / MATCHING).read_bytes() + _, pairs, orth = load_model(archive_bytes, matching_bytes) + if '--two-fold-dp' in argv: + # Optional supplementary cross-check (about 2 CPU-minutes, about 1 GB): + # exact chi_2 by the capacity-2 DP, independent of the LP certificate. + cert = json.loads(CERT.read_text(encoding='utf-8')) + save2, states2 = b_fold_savings_dp(orth, cert['dp_vertex_order'], 2) + print(json.dumps({'max_savings_b2': save2, 'chi_2': 112 - save2, 'dp_states': states2})) + need(112 - save2 == 49, 'two-fold DP disagrees with chi_2 = 49') + print('PASS_TWO_FOLD_DP_CHI2_49') + return 0 + if '--write-certificate' in argv: + order = greedy_order(orth) + y, x = exact_lp(orth) + core, clique22 = find_core(orth) + cert = { + 'schema_version': 1, + 'object': 'PR1825 fixed 56 matched planes, strict PR1889 scalar mask (as stated in PR2471)', + 'sources': {ARCHIVE: ARCHIVE_SHA, ARCHIVE + '#' + MEMBER: MEMBER_SHA, MATCHING: MATCHING_SHA}, + 'dp_vertex_order': order, + 'fractional_clique_y': [str(w) for w in y], + 'fractional_colouring_x': [[s, str(w)] for s, w in x], + 'rank49_supports': supports_from_half_integral(x, pairs), + 'c5_core': core, + 'clique22': clique22, + } + cert['checks'] = run_checks(cert, pairs, orth) + cert['negative_controls'] = negative_controls(cert, pairs, orth, archive_bytes, matching_bytes) + cert['result'] = result_block(cert['checks']) + CERT.write_text(json.dumps(cert, indent=1, sort_keys=True) + '\n', encoding='utf-8') + print('wrote', CERT) + return 0 + cert = json.loads(CERT.read_text(encoding='utf-8')) + checks = run_checks(cert, pairs, orth) + need(checks == cert['checks'], 'recomputed checks differ from CERTIFICATE.json') + controls = negative_controls(cert, pairs, orth, archive_bytes, matching_bytes) + need(controls == cert['negative_controls'], 'negative-control record differs from CERTIFICATE.json') + need(result_block(checks) == cert['result'], 'result block differs') + print(json.dumps(cert['result'], sort_keys=True)) + print('PASS_PAIRED_PLANE_MINRANK_EXACT_49') + return 0 + + +if __name__ == '__main__': + try: + sys.exit(main(sys.argv[1:])) + except CheckFailure as exc: + print('FAIL:', exc) + sys.exit(1) From 4823273c8163e4c72472bdf7d42202e2c12d2e46 Mon Sep 17 00:00:00 2001 From: Sagar Thakrar <18622288+thakrarsagar@users.noreply.github.com> Date: Thu, 15 Oct 2026 18:00:01 +0530 Subject: [PATCH 2/2] Address review: isolate Q-by-core control, fix LP and PR2471 wording - Add a negative control that keeps Q pairwise non-orthogonal but swaps in a plane orthogonal to a core plane (drop 20, add 22), so the Q-by-core premise check is exercised; rename the old control to its true reason. - README: the stored fractional clique coincides with the Q/core weighting; state one LP convention (primal = fractional clique, dual = colouring). - README: describe 23 as PR1825/PR1889's binary column-pair count; add a second (Schur-complement) proof of the C5 lemma, the direct LP implications, and predecessor merge/open status; relabel as research note. Co-Authored-By: Claude Opus 5.5 --- .../CERTIFICATE.json | 3 +- .../README.md | 46 ++++++++++++++----- .../TASK.json | 2 +- .../VERIFY.json | 2 +- .../verify.py | 19 ++++++-- 5 files changed, 53 insertions(+), 19 deletions(-) diff --git a/research/paired-plane-minrank-bracket-audit/CERTIFICATE.json b/research/paired-plane-minrank-bracket-audit/CERTIFICATE.json index 503375b093..393db5def1 100644 --- a/research/paired-plane-minrank-bracket-audit/CERTIFICATE.json +++ b/research/paired-plane-minrank-bracket-audit/CERTIFICATE.json @@ -405,7 +405,8 @@ ] ], "negative_controls": { - "Q_plane_replaced_by_core_neighbour": "rejected: Q not pairwise non-orthogonal at 18,3", + "Q_plane_replaced_breaks_Q_clique": "rejected: Q not pairwise non-orthogonal at 18,3", + "Q_plane_swapped_keeps_clique_but_orthogonal_to_core": "rejected: Q plane 22 orthogonal to core plane 13", "core_reordered_not_a_cycle": "rejected: core is not an induced 5-cycle at 13,35", "fractional_clique_half_weight_raised_to_1": "rejected: fractional clique violated on (13, 23)", "fractional_colouring_set_dropped": "rejected: fractional colouring must cover every plane", diff --git a/research/paired-plane-minrank-bracket-audit/README.md b/research/paired-plane-minrank-bracket-audit/README.md index 687dc4b7f5..a3bdd766b4 100644 --- a/research/paired-plane-minrank-bracket-audit/README.md +++ b/research/paired-plane-minrank-bracket-audit/README.md @@ -1,8 +1,9 @@ # Exact scalar fitting rank 49 for PR2471's fixed paired-plane mask -**Status: independent verification of PR2471 plus a construction and matching -lower bound for a finite algebraic question. No kappa, supplier price or -selected-result change.** +**Status: research note with independent verification of PR2471's witnesses. +It determines the exact value of one finite algebraic quantity (explicit fit plus +a matching lower-bound proof). No kappa, supplier price or selected-result +change.** [PR2471](https://github.com/CrocSwap/integer-mult-bounds/pull/2471) (ywz65, head `5a7c2b681b79d5b5e25fac62aa4bad908525b5ca`) shows that the minimum rank of @@ -21,9 +22,11 @@ rank 48 or 49 is possible, or whether the floor is 50. Both of PR2471's witnesses re-check: a 24-clique and a 25-class rank-50 fit. PR2471 did not assert optimality of either witness, so nothing in PR2471 is -contradicted. Its README phrase "no refactorization with 23 scalar rank-one -channels can fit it" is true, but much weaker than its own rank-48 floor, which -already excludes 47 channels. With the floor raised here, 48 channels cannot fit. +contradicted. PR2471's README compares its floor with 23 scalar rank-one +channels, which is PR1825/PR1889's count of binary scalar column pairs (nine +rank-one plus seven rank-two queries). PR2471's floor already excludes 47 +channels; the exact floor of 49 here excludes 48, and exceeds that reference +count of 23 by 26. ## Model (same as PR2471) @@ -46,8 +49,8 @@ other plane. |---|---|---| | `omega(G)` | 24 (194 maximum cliques) | path-order DP, 12138 states; this algorithm differs from PR2471's colour-bounded branch and bound | | `chi(G)` | **25** | exact DP over packings of orthogonal pairs and triples (40277 states). No 24-class plane partition exists, so PR2471's `2*chi` method cannot reach 48 | -| `chi_f(G)` | **49/2** | exact Bland simplex. The primal (half-integral fractional colouring) and dual (fractional clique) are stored and both re-checked against all 189 orthogonal sets | -| `chi_2(G)` = `chi(G[K_2])` | **49** | upper: the doubled half-integral primal gives 49 port classes. Lower: `2*chi_f`. An optional capacity-2 DP (`--two-fold-dp`) independently gives max savings 63, so `112-63=49` | +| `chi_f(G)` | **49/2** | exact Bland simplex. The LP solved is the fractional-clique LP (primal `y`); its dual, a half-integral fractional colouring `x`, is read from the reduced costs. Both are stored and re-checked against all 189 orthogonal sets | +| `chi_2(G)` = `chi(G[K_2])` | **49** | upper: the doubled half-integral fractional colouring `x` gives 49 port classes. Lower: `2*chi_f`. An optional capacity-2 DP (`--two-fold-dp`) independently gives max savings 63, so `112-63=49` | | min fitting rank, every field | **49** | upper: 49-support 0/1 fit; lower: theorem below | The rank-49 fit `K = sum_S 1_S 1_S^T` uses the 49 supports in @@ -96,8 +99,20 @@ submatrix on the 44 ports of `Q` and the 10 core ports equals The fractional clique explains this. Weight 1 on `Q` and 1/2 on the core sums to 24.5. `verify.py` checks every premise of the theorem from the reconstructed -mask. The stored LP dual is an alternative optimal fractional clique; it also -sums to 49/2 but has a different support. +mask. The stored LP fractional clique `y` coincides with this weighting. + +*Second proof of the lemma (Schur complement; found by a reviewer).* Let `S` be +the four ports of `P0,P2`, so `M[S,S]=I_4`. Rank 4 forces +`M = M[:,S] M[S,:]`. Since `M[D,A]=0`, `I_2 = M[D,D] = M[D,C] M[C,D]`, so +`M[C,D]` is invertible; as `M[B,D]=0` this forces `M[B,C]=0`. Likewise +`I_2 = M[E,E] = M[E,A] M[A,E]` forces `M[A,E]` invertible, and `M[B,E]=0` +forces `M[B,A]=0`. Then `M[B,B] = M[B,A]M[A,B] + M[B,C]M[C,B] = 0`, +contradicting `M[B,B]=I_2`. + +*Direct LP implications.* The DPs are cross-checks. The stored certificates +already imply the table: `chi >= ceil(chi_f) = 25` (with PR2471's 25-class +witness, `chi=25`), `omega <= floor(chi_f) = 24`, and +`chi_2 >= 2*chi_f = 49` (with the 49 supports, `chi_2=49`). `verify.py` also corroborates the lemma by exhaustive search. Over GF(2) and GF(3), the normalised C5 pattern has **no** rank-4 completion. As a control, @@ -139,7 +154,12 @@ Each of these edits was rejected: an emptied support, a non-clique `Q`, a raised - a rank-49 support holding both ports of one plane; - a half weight of the fractional clique raised to 1; - a fractional colouring with one set dropped; -- a `Q` plane replaced by a plane orthogonal to a core plane; +- a `Q` plane replaced by a plane orthogonal to a core plane (this + substitution also breaks `Q`'s pairwise non-orthogonality and is rejected by + that check); +- a `Q` plane swapped (drop 20, add 22) so that `Q` stays pairwise + non-orthogonal but the new plane is orthogonal to core plane 13 (isolates the + `Q`-by-core check); - the core listed out of cycle order. Solver controls: on the orthogonality graphs `C5` and `C7`, the DPs return @@ -170,7 +190,9 @@ Solver controls: on the orthogonality graphs `C5` and `C7`, the DPs return - Channel count is not a native copy cost. As PR2471 and PR2203 note, fifty or forty-nine scalar channels do not imply any physical saving. No kappa is claimed or implied. -- The every-field lower bound rests on the short hand proof above. The verifier +- Predecessor status at the base commit: PR1825, PR1889 and PR1977 are merged + or incorporated; PR2471, PR2126 and PR2203 are open and unreviewed. +- The every-field lower bound rests on the short hand proofs above. The verifier checks its combinatorial premises exactly and corroborates the lemma over GF(2) and GF(3) by exhaustive search. The lemma is not machine-formalised. diff --git a/research/paired-plane-minrank-bracket-audit/TASK.json b/research/paired-plane-minrank-bracket-audit/TASK.json index 7e6694d90e..f87fccefd7 100644 --- a/research/paired-plane-minrank-bracket-audit/TASK.json +++ b/research/paired-plane-minrank-bracket-audit/TASK.json @@ -46,7 +46,7 @@ "budget_minutes": 90, "stop_rule": "Each exact search capped at about 10 CPU-minutes (nice, single process, <1.5 GB); stop at the experiment deadline 2026-10-15T13:01:24Z. All searches finished well inside the cap (default verifier about 2 s; optional two-fold DP about 2 CPU-minutes).", "outcome": "completed", - "evidence": "verify.py (stdlib, exact): omega(G)=24 (194 maximum cliques), chi(G)=25 (exact DP), fractional chi(G)=49/2 (exact primal and dual LP certificates), explicit 0/1 rank-49 fit (49 disjoint supports, 11672 mask entries, I_49 on representatives), rank lower bound 49 over every field from a 22-plane clique plus an induced 5-cycle core (proof in README; finite corroboration over GF(2), GF(3)), 7 negative controls rejected, solver controls on C5/C7. Hence the minimum scalar fitting rank is exactly 49 over every field.", + "evidence": "verify.py (stdlib, exact): omega(G)=24 (194 maximum cliques), chi(G)=25 (exact DP), fractional chi(G)=49/2 (exact fractional-clique (primal) and fractional-colouring (dual) LP certificates), explicit 0/1 rank-49 fit (49 disjoint supports, 11672 mask entries, I_49 on representatives), rank lower bound 49 over every field from a 22-plane clique plus an induced 5-cycle core (proof in README; finite corroboration over GF(2), GF(3)), 8 negative controls rejected, solver controls on C5/C7. Hence the minimum scalar fitting rank is exactly 49 over every field.", "author": "thakrarsagar", "ai_assistance": "Substantial AI assistance from Claude (Anthropic, Claude Opus 5.5) in search design, proof, code and writing; directed and submitted by thakrarsagar. No independent human review is claimed.", "open_questions": [ diff --git a/research/paired-plane-minrank-bracket-audit/VERIFY.json b/research/paired-plane-minrank-bracket-audit/VERIFY.json index 91dc102e34..55831bc391 100644 --- a/research/paired-plane-minrank-bracket-audit/VERIFY.json +++ b/research/paired-plane-minrank-bracket-audit/VERIFY.json @@ -16,7 +16,7 @@ "{package}/verify.py" ], "timeout_seconds": 120, - "checks": "Pinned source sha256; independent mask reconstruction; PR2471 clique/class witnesses; exact omega, chi (DP), chi_f=49/2 LP certificates; rank-49 0/1 fit on all 11672 required entries and ranks mod 2/3/101; rank-49 lower-bound premises (22-clique + induced C5 core); C5 lemma corroboration over GF(2)/GF(3) with a freed-constraint control; DP solver controls on C5/C7; seven negative controls that must be rejected." + "checks": "Pinned source sha256; independent mask reconstruction; PR2471 clique/class witnesses; exact omega, chi (DP), chi_f=49/2 LP certificates; rank-49 0/1 fit on all 11672 required entries and ranks mod 2/3/101; rank-49 lower-bound premises (22-clique + induced C5 core); C5 lemma corroboration over GF(2)/GF(3) with a freed-constraint control; DP solver controls on C5/C7; eight negative controls that must be rejected." } ] } diff --git a/research/paired-plane-minrank-bracket-audit/verify.py b/research/paired-plane-minrank-bracket-audit/verify.py index f2bd5ef72d..9488f621ae 100644 --- a/research/paired-plane-minrank-bracket-audit/verify.py +++ b/research/paired-plane-minrank-bracket-audit/verify.py @@ -318,7 +318,8 @@ def rec(k): # ------------------------------------------------------------- build def exact_lp(orth): """Exact Bland-rule simplex for max sum y s.t. y(S) <= 1 for every orthogonal set S. - Returns (y, x) with x the dual (fractional colouring) read from reduced costs.""" + The primal is the fractional clique y; the returned x is the dual (fractional + colouring) read from reduced costs.""" sets = orthogonal_sets(orth) n, m = len(orth), len(sets) rows = [] @@ -364,7 +365,7 @@ def exact_lp(orth): def supports_from_half_integral(x, pairs): classes = [] for s, w in x: - need((2 * w).denominator == 1, 'primal not half-integral') + need((2 * w).denominator == 1, 'fractional colouring (LP dual) not half-integral') classes.extend([list(s)] * int(2 * w)) used = [0] * len(pairs) supports = [] @@ -545,8 +546,18 @@ def expect_fail(name, fn): expect_fail('fractional_colouring_set_dropped', lambda: check_fractional(sets, y, x2, 56)) swap = next(v for v in range(56) if v not in cert['clique22'] and v not in cert['c5_core'] and any(orth[v][c] for c in cert['c5_core'])) - expect_fail('Q_plane_replaced_by_core_neighbour', + # This substitution breaks Q's pairwise non-orthogonality (it is rejected by the Q-clique check). + expect_fail('Q_plane_replaced_breaks_Q_clique', lambda: lower_bound_premises(cert['c5_core'], cert['clique22'][:-1] + [swap], orth)) + # Isolate the Q x core branch: drop one Q plane and add a plane that keeps Q pairwise + # non-orthogonal but is orthogonal to some core plane. + q, core = cert['clique22'], cert['c5_core'] + drop, add = next((d, v) for d in q for v in range(56) + if v not in q and v not in core + and all(not orth[v][u] for u in q if u != d) + and any(orth[v][c] for c in core)) + expect_fail('Q_plane_swapped_keeps_clique_but_orthogonal_to_core', + lambda: lower_bound_premises(core, [u for u in q if u != drop] + [add], orth)) core = cert['c5_core'] expect_fail('core_reordered_not_a_cycle', lambda: lower_bound_premises([core[0], core[2], core[1], core[3], core[4]], cert['clique22'], orth)) @@ -573,7 +584,7 @@ def main(argv): matching_bytes = (ROOT / MATCHING).read_bytes() _, pairs, orth = load_model(archive_bytes, matching_bytes) if '--two-fold-dp' in argv: - # Optional supplementary cross-check (about 2 CPU-minutes, about 1 GB): + # Optional supplementary cross-check (about 72-81 s, about 0.8 GB peak RSS): # exact chi_2 by the capacity-2 DP, independent of the LP certificate. cert = json.loads(CERT.read_text(encoding='utf-8')) save2, states2 = b_fold_savings_dp(orth, cert['dp_vertex_order'], 2)