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..393db5def1 --- /dev/null +++ b/research/paired-plane-minrank-bracket-audit/CERTIFICATE.json @@ -0,0 +1,644 @@ +{ + "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_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", + "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..a3bdd766b4 --- /dev/null +++ b/research/paired-plane-minrank-bracket-audit/README.md @@ -0,0 +1,230 @@ +# Exact scalar fitting rank 49 for PR2471's fixed paired-plane mask + +**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 +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. 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) + +`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 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 +`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 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, +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 (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 +`(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. +- 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. + +## 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..f87fccefd7 --- /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 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": [ + { + "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..55831bc391 --- /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; 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 new file mode 100644 index 0000000000..9488f621ae --- /dev/null +++ b/research/paired-plane-minrank-bracket-audit/verify.py @@ -0,0 +1,632 @@ +#!/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. + 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 = [] + 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, 'fractional colouring (LP dual) 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'])) + # 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)) + 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 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) + 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)