diff --git a/research/pr2297-principal-rank-floor/CERTIFICATE.json b/research/pr2297-principal-rank-floor/CERTIFICATE.json new file mode 100644 index 000000000..f67771df1 --- /dev/null +++ b/research/pr2297-principal-rank-floor/CERTIFICATE.json @@ -0,0 +1,1471 @@ +{ + "denominator": 1000000, + "sets": [ + { + "groups": [ + 4, + 11, + 12, + 15 + ], + "weight_numerator": 79543 + }, + { + "groups": [ + 4, + 9, + 10, + 17 + ], + "weight_numerator": 64123 + }, + { + "groups": [ + 8, + 15, + 17, + 18 + ], + "weight_numerator": 52244 + }, + { + "groups": [ + 4, + 10, + 15, + 20 + ], + "weight_numerator": 19941 + }, + { + "groups": [ + 0, + 2, + 7, + 8, + 9, + 15 + ], + "weight_numerator": 123160 + }, + { + "groups": [ + 1, + 4, + 5, + 9, + 14, + 16 + ], + "weight_numerator": 39846 + }, + { + "groups": [ + 2, + 5, + 7, + 8, + 14, + 18 + ], + "weight_numerator": 117917 + }, + { + "groups": [ + 1, + 2, + 3, + 6, + 16, + 20 + ], + "weight_numerator": 35526 + }, + { + "groups": [ + 4, + 6, + 8, + 11, + 17, + 20 + ], + "weight_numerator": 184830 + }, + { + "groups": [ + 0, + 5, + 6, + 7, + 9, + 12, + 14 + ], + "weight_numerator": 60520 + }, + { + "groups": [ + 1, + 4, + 8, + 10, + 11, + 15, + 16 + ], + "weight_numerator": 63338 + }, + { + "groups": [ + 2, + 7, + 8, + 9, + 12, + 13, + 18 + ], + "weight_numerator": 155790 + }, + { + "groups": [ + 1, + 2, + 11, + 13, + 15, + 16, + 18 + ], + "weight_numerator": 29576 + }, + { + "groups": [ + 4, + 11, + 12, + 13, + 19, + 20, + 21 + ], + "weight_numerator": 106643 + }, + { + "groups": [ + 0, + 2, + 4, + 8, + 9, + 21, + 22 + ], + "weight_numerator": 2016 + }, + { + "groups": [ + 1, + 5, + 6, + 7, + 12, + 14, + 15, + 17 + ], + "weight_numerator": 117775 + }, + { + "groups": [ + 5, + 6, + 8, + 9, + 14, + 15, + 17, + 18 + ], + "weight_numerator": 42640 + }, + { + "groups": [ + 2, + 6, + 7, + 8, + 10, + 12, + 14, + 20 + ], + "weight_numerator": 69089 + }, + { + "groups": [ + 0, + 5, + 6, + 7, + 9, + 11, + 15, + 20 + ], + "weight_numerator": 10217 + }, + { + "groups": [ + 1, + 4, + 6, + 7, + 9, + 15, + 17, + 20 + ], + "weight_numerator": 199863 + }, + { + "groups": [ + 1, + 3, + 9, + 11, + 16, + 17, + 18, + 21 + ], + "weight_numerator": 95983 + }, + { + "groups": [ + 0, + 2, + 9, + 11, + 16, + 17, + 20, + 21 + ], + "weight_numerator": 20818 + }, + { + "groups": [ + 2, + 3, + 12, + 16, + 17, + 18, + 19, + 22 + ], + "weight_numerator": 32503 + }, + { + "groups": [ + 3, + 5, + 7, + 8, + 11, + 12, + 14, + 15, + 17 + ], + "weight_numerator": 174909 + }, + { + "groups": [ + 1, + 4, + 12, + 13, + 14, + 16, + 17, + 18, + 19 + ], + "weight_numerator": 62709 + }, + { + "groups": [ + 0, + 2, + 4, + 8, + 11, + 12, + 15, + 16, + 20 + ], + "weight_numerator": 16632 + }, + { + "groups": [ + 0, + 1, + 3, + 6, + 10, + 11, + 16, + 17, + 20 + ], + "weight_numerator": 24625 + }, + { + "groups": [ + 2, + 3, + 6, + 10, + 11, + 13, + 15, + 18, + 20 + ], + "weight_numerator": 285292 + }, + { + "groups": [ + 1, + 6, + 7, + 12, + 15, + 16, + 17, + 18, + 21 + ], + "weight_numerator": 157780 + }, + { + "groups": [ + 0, + 9, + 11, + 12, + 13, + 17, + 18, + 21, + 22 + ], + "weight_numerator": 35803 + }, + { + "groups": [ + 0, + 4, + 7, + 8, + 9, + 10, + 11, + 13, + 15, + 18 + ], + "weight_numerator": 34420 + }, + { + "groups": [ + 2, + 4, + 5, + 6, + 9, + 11, + 13, + 14, + 16, + 18 + ], + "weight_numerator": 45354 + }, + { + "groups": [ + 0, + 3, + 4, + 5, + 8, + 10, + 12, + 17, + 18, + 19 + ], + "weight_numerator": 72353 + }, + { + "groups": [ + 4, + 5, + 9, + 10, + 12, + 13, + 15, + 17, + 18, + 19 + ], + "weight_numerator": 2047 + }, + { + "groups": [ + 0, + 1, + 2, + 4, + 5, + 6, + 9, + 10, + 16, + 20 + ], + "weight_numerator": 118712 + }, + { + "groups": [ + 2, + 3, + 4, + 7, + 9, + 11, + 13, + 15, + 19, + 20 + ], + "weight_numerator": 60284 + }, + { + "groups": [ + 2, + 6, + 10, + 12, + 13, + 15, + 16, + 18, + 19, + 21 + ], + "weight_numerator": 12621 + }, + { + "groups": [ + 0, + 2, + 3, + 11, + 12, + 14, + 16, + 18, + 20, + 21 + ], + "weight_numerator": 85647 + }, + { + "groups": [ + 0, + 1, + 2, + 4, + 13, + 14, + 16, + 19, + 20, + 21 + ], + "weight_numerator": 186704 + }, + { + "groups": [ + 2, + 4, + 7, + 9, + 13, + 15, + 17, + 19, + 20, + 21 + ], + "weight_numerator": 18629 + }, + { + "groups": [ + 1, + 2, + 3, + 7, + 8, + 12, + 16, + 17, + 18, + 22 + ], + "weight_numerator": 1849 + }, + { + "groups": [ + 2, + 3, + 4, + 8, + 10, + 11, + 12, + 15, + 19, + 22 + ], + "weight_numerator": 311623 + }, + { + "groups": [ + 0, + 2, + 5, + 6, + 9, + 10, + 14, + 15, + 20, + 22 + ], + "weight_numerator": 140600 + }, + { + "groups": [ + 0, + 1, + 3, + 9, + 10, + 11, + 12, + 15, + 17, + 18, + 19 + ], + "weight_numerator": 5499 + }, + { + "groups": [ + 0, + 4, + 5, + 7, + 12, + 13, + 15, + 16, + 17, + 19, + 20 + ], + "weight_numerator": 47280 + }, + { + "groups": [ + 2, + 4, + 5, + 6, + 8, + 9, + 10, + 12, + 14, + 17, + 21 + ], + "weight_numerator": 173295 + }, + { + "groups": [ + 1, + 4, + 6, + 7, + 11, + 12, + 13, + 16, + 17, + 18, + 21 + ], + "weight_numerator": 208172 + }, + { + "groups": [ + 0, + 5, + 6, + 7, + 9, + 10, + 12, + 13, + 14, + 19, + 21 + ], + "weight_numerator": 210044 + }, + { + "groups": [ + 0, + 1, + 2, + 4, + 8, + 9, + 10, + 11, + 17, + 20, + 21 + ], + "weight_numerator": 57729 + }, + { + "groups": [ + 3, + 4, + 6, + 8, + 12, + 13, + 14, + 17, + 19, + 20, + 21 + ], + "weight_numerator": 24079 + }, + { + "groups": [ + 0, + 2, + 8, + 9, + 11, + 12, + 15, + 18, + 19, + 20, + 22 + ], + "weight_numerator": 178054 + }, + { + "groups": [ + 0, + 2, + 3, + 4, + 8, + 9, + 10, + 13, + 14, + 16, + 18, + 19 + ], + "weight_numerator": 411091 + }, + { + "groups": [ + 0, + 1, + 2, + 3, + 5, + 9, + 10, + 11, + 12, + 14, + 20, + 21 + ], + "weight_numerator": 33628 + }, + { + "groups": [ + 1, + 3, + 4, + 8, + 11, + 12, + 15, + 16, + 18, + 19, + 20, + 21 + ], + "weight_numerator": 81766 + }, + { + "groups": [ + 1, + 2, + 5, + 8, + 9, + 10, + 12, + 13, + 14, + 15, + 16, + 17, + 19 + ], + "weight_numerator": 27215 + }, + { + "groups": [ + 0, + 1, + 4, + 5, + 6, + 7, + 10, + 11, + 12, + 14, + 15, + 16, + 21 + ], + "weight_numerator": 169249 + }, + { + "groups": [ + 1, + 2, + 3, + 4, + 6, + 8, + 10, + 12, + 13, + 14, + 15, + 16, + 21 + ], + "weight_numerator": 4984 + }, + { + "groups": [ + 2, + 3, + 4, + 6, + 10, + 11, + 12, + 13, + 15, + 16, + 17, + 19, + 21 + ], + "weight_numerator": 20186 + }, + { + "groups": [ + 3, + 4, + 6, + 7, + 9, + 10, + 11, + 13, + 15, + 16, + 18, + 19, + 21 + ], + "weight_numerator": 72108 + }, + { + "groups": [ + 0, + 3, + 5, + 8, + 9, + 12, + 13, + 14, + 17, + 18, + 20, + 21, + 22 + ], + "weight_numerator": 128005 + }, + { + "groups": [ + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 9, + 10, + 15, + 16, + 18, + 19, + 20 + ], + "weight_numerator": 150366 + }, + { + "groups": [ + 1, + 2, + 3, + 4, + 6, + 7, + 8, + 12, + 13, + 14, + 16, + 17, + 19, + 21 + ], + "weight_numerator": 155692 + }, + { + "groups": [ + 2, + 3, + 4, + 5, + 7, + 9, + 10, + 12, + 14, + 15, + 16, + 18, + 19, + 21 + ], + "weight_numerator": 4427 + }, + { + "groups": [ + 0, + 1, + 3, + 5, + 7, + 12, + 13, + 14, + 15, + 16, + 17, + 18, + 20, + 21 + ], + "weight_numerator": 262810 + }, + { + "groups": [ + 1, + 3, + 5, + 7, + 10, + 11, + 12, + 13, + 16, + 17, + 18, + 19, + 20, + 21 + ], + "weight_numerator": 146872 + }, + { + "groups": [ + 1, + 3, + 4, + 5, + 6, + 7, + 10, + 11, + 12, + 14, + 15, + 16, + 17, + 18, + 20 + ], + "weight_numerator": 64509 + }, + { + "groups": [ + 1, + 2, + 5, + 7, + 9, + 10, + 11, + 12, + 13, + 14, + 15, + 16, + 17, + 19, + 20 + ], + "weight_numerator": 75026 + }, + { + "groups": [ + 0, + 1, + 3, + 4, + 5, + 6, + 7, + 9, + 10, + 11, + 12, + 13, + 15, + 19, + 21 + ], + "weight_numerator": 52357 + }, + { + "groups": [ + 0, + 1, + 2, + 5, + 6, + 7, + 8, + 9, + 14, + 15, + 17, + 18, + 19, + 20, + 21 + ], + "weight_numerator": 196740 + }, + { + "groups": [ + 0, + 2, + 3, + 5, + 6, + 8, + 9, + 11, + 14, + 16, + 18, + 19, + 20, + 21, + 22 + ], + "weight_numerator": 171389 + }, + { + "groups": [ + 0, + 1, + 2, + 3, + 5, + 6, + 7, + 9, + 10, + 12, + 13, + 14, + 15, + 17, + 18, + 19 + ], + "weight_numerator": 55158 + }, + { + "groups": [ + 0, + 1, + 2, + 4, + 5, + 6, + 8, + 9, + 10, + 13, + 14, + 16, + 18, + 20, + 21, + 22 + ], + "weight_numerator": 79869 + }, + { + "groups": [ + 0, + 2, + 3, + 4, + 5, + 6, + 7, + 8, + 10, + 11, + 12, + 13, + 14, + 15, + 17, + 19, + 20 + ], + "weight_numerator": 61870 + }, + { + "groups": [ + 1, + 2, + 3, + 6, + 7, + 9, + 10, + 11, + 12, + 13, + 15, + 16, + 17, + 18, + 19, + 20, + 21 + ], + "weight_numerator": 151008 + }, + { + "groups": [ + 0, + 1, + 3, + 5, + 6, + 7, + 8, + 9, + 10, + 11, + 12, + 13, + 14, + 15, + 16, + 17, + 19, + 21 + ], + "weight_numerator": 163852 + }, + { + "groups": [ + 0, + 1, + 2, + 3, + 4, + 5, + 7, + 8, + 9, + 10, + 11, + 12, + 13, + 14, + 17, + 19, + 20, + 21 + ], + "weight_numerator": 281245 + }, + { + "groups": [ + 0, + 1, + 3, + 4, + 5, + 7, + 8, + 9, + 11, + 12, + 13, + 14, + 15, + 16, + 17, + 19, + 20, + 21 + ], + "weight_numerator": 192275 + }, + { + "groups": [ + 0, + 1, + 3, + 4, + 5, + 6, + 7, + 8, + 10, + 12, + 14, + 16, + 17, + 18, + 19, + 20, + 21, + 22 + ], + "weight_numerator": 161960 + }, + { + "groups": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 8, + 9, + 10, + 11, + 13, + 15, + 16, + 17, + 18, + 19, + 21 + ], + "weight_numerator": 278201 + }, + { + "groups": [ + 0, + 1, + 4, + 5, + 6, + 7, + 8, + 10, + 11, + 12, + 13, + 14, + 15, + 16, + 17, + 18, + 19, + 20, + 22 + ], + "weight_numerator": 74052 + }, + { + "groups": [ + 0, + 1, + 4, + 5, + 6, + 7, + 8, + 9, + 10, + 11, + 13, + 14, + 15, + 16, + 17, + 18, + 20, + 21, + 22 + ], + "weight_numerator": 111343 + }, + { + "groups": [ + 0, + 1, + 3, + 4, + 5, + 6, + 7, + 9, + 10, + 11, + 13, + 15, + 16, + 17, + 18, + 19, + 20, + 21, + 22 + ], + "weight_numerator": 121589 + }, + { + "groups": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 8, + 10, + 11, + 12, + 13, + 14, + 15, + 16, + 18, + 19, + 20, + 21 + ], + "weight_numerator": 53186 + }, + { + "groups": [ + 0, + 2, + 3, + 4, + 5, + 6, + 7, + 8, + 9, + 10, + 11, + 12, + 14, + 15, + 16, + 17, + 18, + 19, + 20, + 21 + ], + "weight_numerator": 14738 + }, + { + "groups": [ + 0, + 2, + 3, + 4, + 5, + 6, + 7, + 8, + 10, + 11, + 12, + 13, + 14, + 15, + 16, + 17, + 18, + 19, + 20, + 21 + ], + "weight_numerator": 45196 + }, + { + "groups": [ + 0, + 1, + 2, + 3, + 5, + 6, + 7, + 8, + 10, + 11, + 12, + 13, + 14, + 15, + 16, + 18, + 19, + 20, + 21, + 22 + ], + "weight_numerator": 116443 + }, + { + "groups": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 8, + 9, + 10, + 11, + 13, + 14, + 16, + 17, + 18, + 19, + 20, + 21, + 22 + ], + "weight_numerator": 137542 + }, + { + "groups": [ + 0, + 1, + 2, + 3, + 5, + 6, + 8, + 9, + 10, + 11, + 13, + 14, + 15, + 16, + 17, + 18, + 19, + 20, + 21, + 22 + ], + "weight_numerator": 195347 + } + ] +} \ No newline at end of file diff --git a/research/pr2297-principal-rank-floor/PROOF.md b/research/pr2297-principal-rank-floor/PROOF.md new file mode 100644 index 000000000..72048e827 --- /dev/null +++ b/research/pr2297-principal-rank-floor/PROOF.md @@ -0,0 +1,141 @@ +# Principal-rank floor for scalar decoders on the PR2297 cover + +All statements concern the exact PR2297 five-frame cover authenticated by +`verify.py`. The cover has 112 ports in 23 groups. Twenty-two groups are +orthonormal five-frames `E_g` in `F_2^9`, each carried by five ports. One +orthonormal pair `E_22` is carried by two ports. The pairing is the dot +product on `F_2^9`. Every port carries its group's **whole** space (the +full-port tariff of PR #2879 and PR #2532). + +## Theorem + +Let `k` be any field (in particular `Q`), `c in k` nonzero, and + + c I_112 = A diag(c_t) B^T, c_t != 0, + +any finite factorization over `k`. For term `t` let `L_t` (`R_t`) be the sum of +the port spaces on which column `t` of `A` (`B`) is nonzero. Let +`rho_t = rank_F2(pairing on L_t x R_t)` and `C = sum_t rho_t`. Then + + C >= 554, + +and the direct decoder (one term per port) attains 554. No restriction is placed +on the number of terms, supports, span matching, signs or denominators. + +**Corollary.** The zero-saving bound `C <= 492` is unreachable. With unpaid +budget `(8/9) * 554 = 4432/9`, every scalar decoder has deficit at most +`4432/9 - 554 = -554/9` (deficit = budget minus cost). On this cover the u=5 +coverage lever row (the k=5 port-group route of PR #2532 and PR #2879) has no +positive saving under the scalar-decoder contract. + +## 1. Principal-rank count + +The PR #2532 mask rule: for ports `i != j`, the entry `K_ij` is free (may be +nonzero) only if `E_j <= E_i^perp`; the diagonal is a common nonzero `c`. A +**free pair** is a pair of groups with `E_h <= E_g^perp`. This mask has none. +The verifier checks that every two distinct group spaces have a nonzero +pairing, and distinct ports of one group share a nondegenerate space. So the +scalar contract forces `K = c I_112`. + +On this cover, the closest precedent is PR #2879 §1 (Arham Tahir, +`research/support-balanced-port-floor`): its matching lemma notes that a +pairwise nonorthogonal group set `J` forces `K[J,J] = c I` and uses that +nonsingular block over `Q`. Lemma 1 replaces its injection by a count of the +terms that hit `S` on both sides. The weighted principal-block rank count +follows the C5 packages of PR #3232 and PR #3256 (thakrarsagar), PR #3271 +(Nick Petalas) and PR #3281 (Krzysztof Wójt). + +For a set `S` of groups, write `ports(S)` and `f(S) = |ports(S)| = sum_{g in S} d_g`. +Say term `t` **hits** `S` when both `A[ports(S), t]` and `B[ports(S), t]` are +nonzero. + +**Lemma 1.** `h(S) := #{t : t hits S} >= f(S)` for every nonempty `S`. + +*Proof.* `K[S,S] = c I_{f(S)}` equals `sum_t c_t A[ports(S),t] B[ports(S),t]^T`. +Only terms that hit `S` survive. A sum of `h(S)` matrices of rank at most one +has rank at most `h(S)`, so `h(S) >= f(S)`. ∎ + +This is a statement about ranks over `k`. It needs no reduction modulo 2, so +denominators play no role. It is false when a principal block has free entries: +for three mutually orthogonal lines every off-diagonal entry is free, and +`K = J = 1 1^T` is admissible with one term of principal rank 1 < 3. The +verifier's premise check in `cover()` rejects a mutated cover with a free pair. + +## 2. Group supports and flats + +Let `P_t` (`Q_t`) be the set of groups containing a port where column `t` of `A` +(`B`) is nonzero. Then `L_t = E_{P_t} := sum_{g in P_t} E_g`, likewise +`R_t = E_{Q_t}`, so `rho_t = rho(E_{P_t}, E_{Q_t})`. Term `t` hits `S` exactly when +`S` meets both `P_t` and `Q_t`. + +A **flat** is a subspace `E_P` for a nonempty group set `P`. Its closed group +set is `cl(E_P) = {g : E_g ⊆ E_P}`. It contains `P` and spans `E_P`. This cover +has exactly 107 flats. The verifier finds them in two independent ways. +(a) A breadth-first closure of the single-group spans under adding one group. +(b) The canonical reduced-echelon spans of all group subsets of size at most +five. It then checks that family (b) contains every single group and is closed +under adding any group. Hence (b) contains every flat. + +## 3. Dual certificate + +**Lemma 2.** Let `y_S >= 0` be weights on a finite family of group sets such that, +for every ordered pair of flats `(F, F')`, + + sum { y_S : S meets cl(F) and S meets cl(F') } <= rho(F, F'). (*) + +Then every decoder of the theorem satisfies `C >= sum_S y_S f(S)`. + +*Proof.* Discard terms with a zero column (they cost nothing and hit nothing). +For term `t` put `F = E_{P_t}` and `F' = E_{Q_t}`. Any `S` hit by `t` meets +`P_t ⊆ cl(F)` and `Q_t ⊆ cl(F')`. By (*), `sum_{S hit by t} y_S <= rho(F,F') = rho_t`. +Summing over `t`, exchanging the sums and applying Lemma 1 gives + + C >= sum_S y_S h(S) >= sum_S y_S f(S). ∎ + +This is LP duality for the relaxation that keeps only Lemma 1's +principal-rank constraints. The relaxation is tight to within `0.0036` on this +cover: the certified value lies in `[553.996479, 554]`, and after integer +rounding the floor equals the direct cost 554. That the LP optimum is exactly +554 is not certified (the solver's value is a float). + +## 4. The certificate and the floor + +`CERTIFICATE.json` lists 88 group sets with positive integer numerators over +`10^6`. The verifier checks (*) exactly in integers for all `107^2 = 11449` +ordered flat pairs. The minimum slack is `6/10^6`. The value is +`sum_S y_S f(S) = 553996479/1000000 > 553`. `C` is a sum of integer ranks, +so `C >= 554`. Both pairing-rank methods give the same `rho(F,F')`: packed +elimination of the Gram matrix, and the count `dim F - dim(F ∩ F'^perp)` over all +512 vectors. + +The certificate's shape explains the floor. Each five-frame lies in total +weight just under 5 (between 4.99996 and 5), and the residual pair in total +weight just under 2 (1.999987). The constraints `(E_g, E_g)`, which cost `d_g`, +cap these totals at `d_g`. The total weight is `449997/50000 < 9`. This is +the constraint `(F_2^9, F_2^9)`: a term meeting every group on both sides costs +9 and hits every set. Sets have sizes 4 to 20. By (*) on single-group flats, +two groups whose pairing has rank `r` lie together in total weight at most `r`. +This is how the certificate charges the off-block corrections that a cheap +shared term creates. + +## 5. Scope + +- Complete for scalar decoders of this exact mask and full-port tariff, over + any field. It contains PR #2879's equal-span floor and the 2-integral floor + (philippeVV, Discussion #1587 Theorem 1, applied in PR #2532) for this cover. + It settles the open unmatched-span, even-denominator class: PR #2879 §4 showed + a saving would need at least 16 unmatched-span terms with total asymmetry + credit `sum delta_t >= 62`. No such decoder exists. The achievable + even-denominator saving for k=5 is zero: every decoder costs at least 554. +- It does not apply to masks with free pairs. There a principal block need not + be `c I` and Lemma 1 can fail. Examples are the PR2041 triad cover and the + plane and line masks of Discussion #1587. E8-type savings are known only on + the line masks; no decoder below the naive cost is known on the plane masks + or on PR2041. This agrees with philippeVV's follow-up 4: bounds that also hold + for line ports cap at 128 on plane covers. Lemma 1 does not hold for line + masks with free pairs. +- It covers only the scalar-decoder contract. Operator- or block-valued + decoders and other call contracts on this cover (PR2297's `C_E^2` blocks, + PR #3480 by Gonzalo Mier) are not addressed. +- It prices no native frame, restoration, hosting, precision, consumer, other + cover or other `u`. No supplier or κ follows. diff --git a/research/pr2297-principal-rank-floor/README.md b/research/pr2297-principal-rank-floor/README.md new file mode 100644 index 000000000..668565a11 --- /dev/null +++ b/research/pr2297-principal-rank-floor/README.md @@ -0,0 +1,251 @@ +# PR2297 principal-rank floor: every scalar decoder costs at least 554 + +**Result: a scoped proof plus an exact finite certificate. No κ claim and no supplier.** + +On the exact PR2297 five-frame cover, take any finite factorization +`c I_112 = A diag(c_t) B^T` over `Q`, or over any field. Under the full-port +tariff `rho_t = rank_F2(pairing on L_t x R_t)`, where `L_t` (`R_t`) is the sum +of the group spaces of the ports on which column `t` of `A` (`B`) is nonzero, +its cost is + + C = sum_t rho_t >= 554. + +The direct one-term-per-port decoder attains 554, so the bound is sharp. The +zero-saving bound `C <= 492` is therefore unreachable. The unpaid budget is +`4432/9`, so every scalar decoder has deficit (budget minus cost) at most +`-554/9`, i.e. a loss of at least `554/9`. Here the **u=5 coverage lever row** is +the k=5 port-group route of the `coverage-law-change` card (five unpaid +coordinates per port, each port carrying its five-dimensional group space; +PR #2532 and PR #2879). **On this cover that row +has no positive saving under the scalar-decoder contract.** That holds for every +number of terms, every support pattern (matched or unmatched spans), every sign +and every denominator. Non-scalar endpoint contracts are not covered (see Scope). + +The proof is in [PROOF.md](PROOF.md). It has two parts. + +1. **Lemma 1 (principal-rank count).** For a set `S` of groups, `K[S,S] = c I`. + Hence at least `f(S) = sum_{g in S} d_g` terms must be nonzero on `S` on both + sides. This is a rank statement over the base field. It needs no reduction + modulo 2, so even denominators do not matter. +2. **Lemma 2 (LP duality over flats).** Give nonnegative weights `y_S` to group + sets. Suppose that for every pair of flats `(F, F')`, the sets meeting both + closed group sets have total weight at most `rho(F,F')`. Then + `C >= sum_S y_S f(S)`. A flat is the span of a nonempty group set. This + cover has 107 of them. + +[CERTIFICATE.json](CERTIFICATE.json) holds 88 sets with integer weights over +`10^6`. It satisfies all 11,449 ordered flat-pair constraints exactly, with +minimum slack `6/10^6`. Its value is `553996479/1000000 > 553`, and `C` is an +integer, so `C >= 554`. + +## What is new + +- **Predecessors.** PR #2879 (Arham Tahir, `research/support-balanced-port-floor`) + proved 554 only for terms with equal complete spans. For the general case it + gave a necessary condition: at least 16 unmatched-span terms with total + asymmetry credit `sum delta_t >= 62`. philippeVV's Theorem 1 (Discussion #1587, applied to this cover in + PR #2532) proved 554 only for 2-integral decoders. The general + unmatched-span, even-denominator class was the open question of both packages. +- **This package** closes that class. It does so by counting ranks over the base + field, not by a 2-adic argument. The counting constraints are weighted by an + exact dual certificate over the cover's flats. The certified relaxation value + lies in `[553.996479, 554]`, within `0.0036` of the direct cost; after integer + rounding the floor equals the direct cost 554. (That the LP optimum is exactly + 554 is not certified.) This also answers PR #2532's open question + "even-denominator gain for k=5": the achievable even-denominator saving is + zero, because every decoder costs at least 554. +- **Method precedent.** The principal-block rank count and the weighted rank + cover are not new. They were used on C5 masks in PR #3232 and PR #3256 + (thakrarsagar, `research/c5-gram-rank-cover`, `research/c5-asymmetric-cost-floor`), + PR #3271 (Nick Petalas, `research/c5-residual-weighted-cover`) and PR #3281 + (Krzysztof Wójt, `research/c5-four-residual-floors`, exact rational separation + certificates). New here are the application to the PR2297 cover, the + flat-indexed LP-dual certificate and the verifier. +- **Why Lemma 1 is available here.** The mask has no free pair, so every + principal block is `c I` (as PR #2879 §1 already notes for pairwise + nonorthogonal sets; Lemma 1 replaces its injection by a term count). On masks with free pairs, Lemma 1 holds only for + group sets that contain no free pair. Examples are the PR2041 triad cover and + the plane and line masks of Discussion #1587. E8-type savings are known only + on the line masks; no decoder below the naive cost is known on the plane masks + or on PR2041. This agrees with philippeVV's follow-up 4: bounds that also hold + for line ports cap at 128 on plane covers. + +## Reproduce + +From the repository root, with Python 3.12 or later and the standard library +only (about 2 s and 35 MB): + +```sh +python3 -B research/pr2297-principal-rank-floor/verify.py +``` + +The expected final line is `PASS_PR2297_PRINCIPAL_RANK_FLOOR`. The printed JSON +includes: + + "flats": 107, "flat_pairs": 11449, "certificate_sets": 88, + "certificate_value": "553996479/1000000", "min_slack_numerator": 6, + "floor": 554, "direct_decoder_cost": 554, "unpaid_budget": "4432/9", + "exact_instance_cost": 691 + +The generic hook is +`python3.12 scripts/research_package.py --package research/pr2297-principal-rank-floor`. + +### What the verifier checks + +1. **Inputs.** It authenticates both pinned inputs (SHA256 and Git blob), the + selected-replay member (SHA256) and the 112 labels. +2. **Cover.** There are 22 orthonormal five-frames and one orthonormal pair, and + no orthogonal group pair. This is the premise `K = c I_112`. +3. **Flats.** It finds the 107 flats twice: by breadth-first closure, and from + all group subsets of size at most five plus a closedness check. +4. **Pairing ranks.** It computes `rho(F,F')` for all flat pairs twice: by + packed Gram elimination, and as `dim F - dim(F ∩ F'^perp)` by vector + counting. +5. **Certificate.** It checks the dual constraint (*) for all 11,449 ordered + flat pairs in exact integers, and computes the exact value. +6. **Sharpness.** The direct decoder costs 554. +7. **Non-closed supports.** It tries 2,000 seeded random support pairs `(P, Q)` + that are not closed. Each satisfies (*) with ranks computed directly. This is + a second check of the closure reduction. +8. **Exact instance.** It builds a random exact rational decoder with + denominators 2, 4 and 8: a unit-triangular `A` with up to 160 cross entries, + and `B^T = c0 diag(c)^{-1} A^{-1}`. It checks `K = c0 I_112` entrywise and + checks the chain `C = 691 >= sum y_S h(S) >= sum y_S f(S)`. + +**Negative controls**, each of which must be rejected: + +- one certificate weight inflated by 1; +- `rho(F_2^9, F_2^9)` replaced by 8, as if the ambient pairing were degenerate; +- the line-label tariff (cost 1 per single-group pair) instead of the full-port + tariff; +- the doubled certificate; +- method B of step 3 fed a group list with one group dropped (its flats must + disagree with method A); +- a mutated cover whose residual pair is moved into `E_0^perp`, creating a free + (orthogonal) group pair: `cover()` must reject it for exactly that reason. + +The verifier also computes the zero-saving threshold `floor(4432/9) = 492` from +the unpaid budget. PROOF.md §1 notes why Lemma 1 fails with free pairs (three +orthogonal lines admit `K = J` with one term). + +`find_certificate.py` is a provenance helper and **not** part of verification. +It shows how the certificate was found: the HiGHS LP over 3,252 distinct +candidate sets against all flat pairs. The candidates are all 23 singletons, all +253 pairs, the full set and seeded random sets. The weights are rounded down to +`10^-6` and shrunk by 2 ppm. It needs numpy 2.5.4 and scipy 1.18.1, which are not +verifier requirements. With those pins it reproduced the shipped certificate +byte for byte. Any feasible certificate with value above 553 proves the same +floor. + +## Sources and pins + +- **Base commit:** `20ecf2891d80b5acf18d980b2164fb44ea7faa90` (priority revision 6). +- **Live inputs** (also in [SOURCES.json](SOURCES.json) and `VERIFY.json`): + - `research/community-frontier1094-audit/selected-replay.tar.gz`, + sha256 `f1da80610bf33c58527f18ad63b4350d0b864e1d4486141ee17ac9bed4d529d6`. + Its member `candidate/strict/global/base/work/complex-nine-native/DATA-PHASES.json` + has sha256 `c5916ff312678f12aba403847643fbbc29f643acec60bdf836fa56cd3e8251fa`. + - `research/kport-group-scalar-endpoint-audit/fixtures/PR2297-CANDIDATE.json`, + sha256 `5b69c7a873f19a64ed73a1c1281d20398d2675b3281fd4fa259aed9cf91a86c0`. + This is Cinna Davis's PR2297 cover as retained by PR #2532. +- **Certificate:** `CERTIFICATE.json`, sha256 `7c8005882d34aeef545bd3256e6da2d3cb5aa881dc70ff97363111a80adcc525`. + +## Scope, inherited assumptions and obligations + +- **Scope.** The exact PR2297 cover, the scalar-decoder contract and the + full-port tariff, as defined in PR #2532 and PR #2879. This is a scoped proof + plus a finite certificate. It is not a complete multiplication theorem. +- **Not addressed: non-scalar endpoint contracts on this cover.** PR #2532 left + an operator- or block-valued interpretation and other call contracts open. + PR2297's own `C_E^2` correction blocks and PR #3480 (Gonzalo Mier, head + `8e6fcaa557d2bff56c914f167e19929b0b656e1f`, deferred corrections under a shared + register; family thread Discussion #2292) work outside the scalar contract. + This package says nothing about them. +- **Inherited assumptions.** The tariff charges each touched port's complete + group space. The planning law is the portwise, nine-stage law of PR #2879 §3, + which gives the unpaid budget `(8/9) sum d_i`. Both are taken as given; this + package does not re-derive them. The conclusion does not hinge on the 8/9 + law alone: 554 also exceeds the incumbent-tie threshold 455-460 of PR #2532 + and the u=5 rank-32 copy budget 488 of PR #3344 (Matarener, + `research/complex-multi-unpaid-copy-budgets`). +- **Unresolved obligations.** + - Lemmas 1 and 2 are elementary and written out, but have not been checked + by a proof assistant. + - Native frames, restoration, hosting, precision and the complete consumer + are unpriced. They are moot for this row only because no decoder saves. + - Other covers, other `u` values and masks with free pairs are not covered. +- **No change** to the selected result or κ. + +## Open next questions + +The structured versions are in [TASK.json](TASK.json). + +1. **Clique-restricted principal-rank LP on the PR2041 triad cover.** Lemma 1 + still holds for group sets that contain no free (orthogonal) pair. + - *Why it matters:* PR #2879's 297 is an equal-span floor only; the + unmatched-span class on the literal PR2041 cover is still open. A clique LP + value of 297 or more would close the literal cover's general class. A value + of 299 or more would also exclude the uniform-three completion (budget + `896/3 ≈ 298.67`), provided the certificate's sets avoid the completed + group and the tariff is monotone under the completion. + - *First step:* run `find_certificate.py`'s LP with the candidate sets + restricted to orthogonal-pair-free group sets of the PR2041 cover. + - *Related, check first:* the rank-57 triad line, PR #2757 and PR #3684 + (flyingviper) and PR #3505, #3513, #3527 and #3538 (Nick Petalas). +2. **Free-pair masks.** Is there a principal-rank analogue for masks with free + pairs, using only cliques of the nonorthogonality graph, that is not also + valid for line ports? + - *Why it matters:* philippeVV's follow-up 4 shows that line-valid bounds + cap at 128 on plane covers, so any useful version must be plane-specific. + - *First step:* compute the clique-restricted LP on philippeVV's a23 plane + assignment and compare it with 128. + - *Related, check first:* the concurrent lost-free plane-mask line, open + PRs #3625 (Matarener), #3674 (ToikY), #3676 and #3756 (James Reed). +3. **Changed contracts.** The u=5 row on PR2297 is now closed for scalar + decoders. A k-port coverage saving on this row needs something other than a + different scalar decoder: a mask with free pairs, another tariff, another + cover, or another endpoint contract (an operator- or block-valued decoder + with its own complete identity and charges, such as PR2297's `C_E^2` blocks + or PR #3480). + - *Why it matters:* this marks which contract change still has room. + - *First step:* state which of these a proposed k-port contract changes + before pricing a decoder. + +## Credit and provenance + +- **Arham Tahir (Arham-Tahir64).** PR #2879, head + `17183900660480a4e8f031f117f04d79474cf63d`, + `research/support-balanced-port-floor`. Matching lemma, equal-span floor, + asymmetry budget and the exact cover analysis this package extends. +- **Philippe Van Velzen (philippeVV).** Discussion #1587, comments 18927273 + (Theorem 1, top-layer lemma), 18932906 (Smith lemma) and 18942562 (follow-up 4 + barriers). The full-port pricing and the 2-adic route this package bypasses. +- **Sagar Thakrar (thakrarsagar).** PR #2532, `research/kport-group-scalar-endpoint-audit`, + commit `bcb6f278503bd2a6b3ffb9bdcfcda9f36c18d2f4`. The k-port masks, the + 2-integral floor and the retained PR2297 fixture. +- **Cinna Davis (1337isnot1337).** PR2297 cover, commit + `49f9c1a08bf1fe67a62bd6d2825aa0d03e1b1518`. +- **Adam Gall (adamgall).** PR1889 mask and tariff foundations. +- **Tekalign (tekuuu).** PR2782, the Gram denominator gate, commit + `002a9983079a3244c10221b4e16d0cff7e70da40`. +- **Method precedent.** PR #3232 (head `9d75ed2b5bc9`) and PR #3256 (head + `1ea98246dabb`) by thakrarsagar; PR #3271 by Nick Petalas (petalas, head + `1bbe044ba2c7`); PR #3281 by Krzysztof Wójt (krzysztofwojt, head + `a3a7306c15c7`). Principal-block rank counts, weighted rank covers and exact + rational separation certificates on C5 masks. +- **ywz65.** PR #2528, the mixed-cover weighted unpaid dimension `554/112 = 277/56`. + It agrees with the budget `(8/9) * 554 = 4432/9`, whose integer part 492 is the + zero-saving threshold used here. + +The application to the PR2297 cover, the flat-indexed LP-dual certificate and +the verifier are new; the principal-block rank count and the weighted rank +cover follow the C5 packages above. The cross-checks are an independent flat +enumeration, a second rank method, random non-closed supports and an exact +rational instance. They were run by the same AI-assisted session. The package +was reviewed in two rounds of independent AI review passes in the same loop +(reproducibility, mathematics, provenance, referee); two of those passes +recomputed the certificate with separate scripts. There has been no human +review. + +Prepared by Sagar Thakrar (thakrarsagar) with substantial AI assistance from +Claude (Anthropic, Claude Opus 5.5). Apache-2.0. diff --git a/research/pr2297-principal-rank-floor/SOURCES.json b/research/pr2297-principal-rank-floor/SOURCES.json new file mode 100644 index 000000000..15a56c2f1 --- /dev/null +++ b/research/pr2297-principal-rank-floor/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5", + "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0" + }, + { + "path": "research/community-frontier1094-audit/selected-replay.tar.gz", + "usage": "input", + "git_blob": "c24daf067f9c543421d89ca2eeaa4eb78a57fb6f", + "sha256": "f1da80610bf33c58527f18ad63b4350d0b864e1d4486141ee17ac9bed4d529d6" + }, + { + "path": "research/kport-group-scalar-endpoint-audit/fixtures/PR2297-CANDIDATE.json", + "usage": "input", + "git_blob": "ca69901755dde5f6e8adf7dd6df936dc3ab0142d", + "sha256": "5b69c7a873f19a64ed73a1c1281d20398d2675b3281fd4fa259aed9cf91a86c0" + } + ] +} diff --git a/research/pr2297-principal-rank-floor/TASK.json b/research/pr2297-principal-rank-floor/TASK.json new file mode 100644 index 000000000..1e06777d2 --- /dev/null +++ b/research/pr2297-principal-rank-floor/TASK.json @@ -0,0 +1,77 @@ +{ + "schema_version": 1, + "task_id": "coverage-law-change", + "priority_revision": 6, + "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "original_card": { + "id": "coverage-law-change", + "question": "Can a template or call contract leave two or more unpaid coordinates per live family?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/complex-local-word-ceiling/README.md", + "research/idle-axis-hosting/PROOF.md", + "certificates/selected-result.json" + ], + "methods": [ + "State a replacement for the coverage identity (mass = 72W + 64N) and the contract change that realizes it, with its implementation cost.", + "Find an obstruction: show which data-endpoint obligation forces exactly one unpaid coordinate in the current template." + ], + "acceptance_gate": "An explicit replacement identity, verified on a small complete instance with dirty inputs, priced with ceiling.ceiling(unpaid=...). A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "research/complex-local-word-ceiling/verify.py" + ], + "expected": "PASS_COMPLEX_LOCAL_WORD_CEILING", + "inspect": "Read the selected word's per-call local profile, its packing ceiling and the lever table; run levers.py for the ideal budget of the lever you target.", + "scope": "Positive control and planning budget only; this is not a new construction or full cold replay." + }, + "first_experiment": "Explain where the single unpaid coordinate per family comes from in the hosted template; propose one change and price it. Ideal budget: two unpaid coordinates per family is 3.77x (levers.py).", + "bottleneck_link": "The deficit is one coordinate per family minus the centre charge; doubling unpaid coordinates per family scales it directly.", + "allowed_variations": [ + "One template change or one endpoint-contract change.", + "If the coverage law, template or guard changes, derive an applicable fully charged replacement bound instead of applying the incumbent ceiling outside its scope." + ], + "scope_change_triggers": [ + "Counting a coordinate as unpaid while leaving it unadvanced in the data endpoint.", + "Continuing a partial cost improvement while leaving the same unpriced consumer, restoration or central-readout obligation unresolved; refresh the family expansion decision first. Local product-retiming evidence has a narrow scope and is not a ban on changed graphs or contracts." + ], + "overlap_terms": [ + "coverage identity", + "unpaid coordinate", + "deficit law", + "W - 64N" + ] + }, + "scope_status": "changed", + "actual_scope": "Scalar decoders c*I_112 = A diag(c_t) B^T (any field, any denominators) on the exact PR2297 five-frame cover with the full-port tariff: is every decoder above the zero-saving bound C <= 492 for the u=5 coverage lever row?", + "scope_change_reason": "The card asks for a coverage-law change in general. This package answers the single open residual of the k-port (u=5) lever row on the PR2297 cover: the unmatched-span, even-denominator scalar decoders left open by PR #2879 (equal spans) and philippeVV Theorem 1 / PR #2532 (2-integral). Deciding it settles whether that lever row can save anything.", + "bottleneck_link": "The coverage-law card asks for contracts with more unpaid coordinates per family. The k-port scalar decoder row (u=5, the k=5 port-group route) was a candidate on the PR2297 cover. Proving C >= 554 for every scalar decoder (budget 4432/9, deficit = budget minus cost <= -554/9) closes that row for scalar decoders: a saving there needs something other than a different scalar decoder (a mask with free pairs, another tariff, another cover, or another endpoint contract such as an operator- or block-valued decoder, e.g. PR2297's C_E^2 blocks or PR #3480).", + "budget_minutes": 90, + "stop_rule": "Hard gate 2026-10-19T00:35Z: either a complete checkable proof route or an explicit exact decoder with C <= 492, otherwise no PR. Gate passed at 00:25Z with an exact dual certificate; no large searches; stdlib verifier under 50 MB.", + "outcome": "completed", + "evidence": "PROOF.md: principal-rank count (Lemma 1, rank over the base field, no 2-adic step) plus LP duality over the 107 flats (Lemma 2). CERTIFICATE.json: 88 group sets, integer weights over 10^6, all 11449 ordered flat-pair constraints checked exactly (min slack 6/10^6), value 553996479/1000000 > 553, so C >= 554 by integrality; the direct decoder attains 554. verify.py (stdlib, ~2 s) also enumerates flats and pairing ranks by two methods each, checks 2000 random non-closed supports, an exact rational decoder instance (cost 691) and six negative controls (including a mutated cover with a free group pair, rejected by the premise check). PASS_PR2297_PRINCIPAL_RANK_FLOOR.", + "author": "Sagar Thakrar (thakrarsagar)", + "ai_assistance": "Substantial AI assistance from Claude (Anthropic, Claude Opus 5.5) in the proof idea, LP search, verifier, certificate and writing, within one automated research loop session. Reviewed in two rounds of independent AI review passes in the same loop (reproducibility, mathematics, provenance, referee); two of those passes recomputed the certificate with separate scripts; no human review.", + "open_questions": [ + { + "question": "Does the clique-restricted principal-rank LP (group sets with no orthogonal pair) reach 297, or 299, on the PR2041 triad cover?", + "why_it_matters": "PR #2879's 297 is an equal-span floor only, so the unmatched-span class on the literal PR2041 cover is still open; a clique LP value >= 297 closes it. A value >= 299 also excludes the uniform-three completion (budget 896/3 = 298.67), provided the certificate's sets avoid the completed group and the tariff is monotone under the completion.", + "first_step": "Check the rank-57 triad line first (PR #2757 and PR #3684 by flyingviper; PR #3505, #3513, #3527 and #3538 by Nick Petalas). Then run the find_certificate.py LP with candidate sets restricted to orthogonal-pair-free group sets of the PR2041 cover, and certify exactly.", + "blocked_by": "nothing" + }, + { + "question": "Is there a principal-rank analogue for masks with free pairs (cliques of the nonorthogonality graph only) that is not also valid for line ports?", + "why_it_matters": "philippeVV's follow-up 4 shows line-valid bounds cap at 128 on plane covers, so a useful bound must be plane-specific.", + "first_step": "Check the concurrent lost-free plane-mask line first (open PRs #3625 by Matarener, #3674 by ToikY, #3676 and #3756 by James Reed). Then compute the clique-restricted LP on philippeVV's a23 plane assignment and compare with 128.", + "blocked_by": "needs the a23 plane assignment from philippeVV/integer-mult-bounds@5c81aa40 pinned in this repository" + }, + { + "question": "Which k-port change (a mask with free pairs, another tariff, another cover, or a non-scalar endpoint contract) still has room for a coverage saving now that the PR2297 u=5 scalar row is closed?", + "why_it_matters": "It identifies which routes remain for the k-port lever row; the scalar-decoder route on this cover is closed.", + "first_step": "For a proposed k-port contract, state which of the four it changes before pricing a decoder; for operator- or block-valued decoders (PR2297's C_E^2 blocks, PR #3480 by Gonzalo Mier) state their complete identity and charges.", + "blocked_by": "nothing" + } + ] +} diff --git a/research/pr2297-principal-rank-floor/VERIFY.json b/research/pr2297-principal-rank-floor/VERIFY.json new file mode 100644 index 000000000..e66d2db36 --- /dev/null +++ b/research/pr2297-principal-rank-floor/VERIFY.json @@ -0,0 +1,21 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/community-frontier1094-audit/selected-replay.tar.gz", + "research/kport-group-scalar-endpoint-audit/fixtures/PR2297-CANDIDATE.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Authenticated PR2297 cover; two flat enumerations (107); two pairing-rank methods; exact dual certificate over all 11449 flat pairs, value 553996479/1000000 > 553 so C >= 554; direct decoder 554; 2000 random non-closed supports; exact rational decoder instance; six negative controls rejected." + } + ] +} diff --git a/research/pr2297-principal-rank-floor/find_certificate.py b/research/pr2297-principal-rank-floor/find_certificate.py new file mode 100644 index 000000000..0174176b2 --- /dev/null +++ b/research/pr2297-principal-rank-floor/find_certificate.py @@ -0,0 +1,61 @@ +#!/usr/bin/env python3 +"""Provenance helper (NOT part of verification): how CERTIFICATE.json was found. + +Solves the principal-rank LP relaxation's dual over a finite family of group sets +(all singletons and pairs, the full set, 3000 seeded random sets) against every +pair of flats, then rounds the weights down to integers over 10**6 and shrinks by +2 ppm. verify.py re-checks the result exactly; any feasible certificate with +value > 553 proves the same floor. Requires numpy 2.5.4 and scipy 1.18.1 (HiGHS); +other versions may return a different optimal vertex. Usage: + python3 research/pr2297-principal-rank-floor/find_certificate.py OUT.json +Prepared by Sagar Thakrar (thakrarsagar) with substantial AI assistance from +Claude (Anthropic, Claude Opus 5.5). Apache-2.0. +""" +import itertools +import json +import random +import sys +from pathlib import Path + +import numpy as np +from scipy.optimize import linprog + +sys.path.insert(0, str(Path(__file__).resolve().parent)) +import verify as V # noqa: E402 + +DEN = 10 ** 6 + + +def main(out): + labels, groups = V.sources() + spaces, gm = V.cover(labels, groups) + d = [len(s) for s in spaces] + n = len(d) + flats = sorted(V.flats_closure(gm), key=lambda F: (V.dim(F), F)) + pmap = V.closure_sets(flats, gm) + P = [sum(1 << g for g in pmap[F]) for F in flats] + rho = [[V.rho_elimination(L, R) for R in flats] for L in flats] + m = len(P) + rng = random.Random(20261019) + cols = {1 << g for g in range(n)} | {(1 << a) | (1 << b) for a, b in itertools.combinations(range(n), 2)} + cols |= {sum(1 << g for g in rng.sample(range(n), rng.randint(3, 20))) for _ in range(3000)} + cols.add((1 << n) - 1) + cols = sorted(cols) + pairs = [(i, j) for i in range(m) for j in range(i, m)] + hit = np.array([[(P[i] & S) != 0 for S in cols] for i in range(m)]) + A = np.array([hit[i] & hit[j] for i, j in pairs], dtype=float) + b = np.array([rho[i][j] for i, j in pairs], dtype=float) + c = -np.array([sum(d[g] for g in range(n) if S >> g & 1) for S in cols], dtype=float) + res = linprog(c, A_ub=A, b_ub=b, bounds=(0, None), method='highs') + assert res.status == 0, res.message + print('LP value', -res.fun) + rows = [(S, int(v * DEN * (1 - 2e-6))) for S, v in zip(cols, res.x) if v > 1e-9] + rows = [(S, w) for S, w in rows if w > 0] + data = {'denominator': DEN, 'sets': [{'groups': [g for g in range(n) if S >> g & 1], 'weight_numerator': w} + for S, w in sorted(rows, key=lambda x: (bin(x[0]).count('1'), x[0]))]} + Path(out).write_text(json.dumps(data, indent=1)) + print('wrote', out, len(rows), 'sets') + + +if __name__ == '__main__': + main(sys.argv[1]) diff --git a/research/pr2297-principal-rank-floor/verify.py b/research/pr2297-principal-rank-floor/verify.py new file mode 100644 index 000000000..fadb31606 --- /dev/null +++ b/research/pr2297-principal-rank-floor/verify.py @@ -0,0 +1,378 @@ +#!/usr/bin/env python3 +"""Exact principal-rank floor C >= 554 for every scalar decoder of c*I_112 on the +PR2297 five-frame cover (full-port tariff). Standard library only. + +Prepared by Sagar Thakrar (thakrarsagar) with substantial AI assistance from +Claude (Anthropic, Claude Opus 5.5). Apache-2.0. +""" +import hashlib +import io +import itertools +import json +import random +import sys +import tarfile +from fractions import Fraction as Q +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +ARCHIVE = 'research/community-frontier1094-audit/selected-replay.tar.gz' +FIXTURE = 'research/kport-group-scalar-endpoint-audit/fixtures/PR2297-CANDIDATE.json' +MEMBER = 'candidate/strict/global/base/work/complex-nine-native/DATA-PHASES.json' +PAYLOAD_SHA = 'c5916ff312678f12aba403847643fbbc29f643acec60bdf836fa56cd3e8251fa' +EXPECTED = dict(groups=23, flats=107, pairs=107 * 107, support=88, floor=554, direct=554, unpaid='4432/9') + + +class Reject(Exception): + pass + + +def need(condition, message): + if not condition: + raise Reject(message) + + +def sources(): + manifest = json.loads((HERE / 'SOURCES.json').read_text()) + bound = {} + for pin in manifest['files']: + if pin['usage'] != 'input': + continue + raw = (ROOT / pin['path']).read_bytes() + need(hashlib.sha256(raw).hexdigest() == pin['sha256'], 'source SHA256: ' + pin['path']) + need(hashlib.sha1(b'blob %d\0' % len(raw) + raw).hexdigest() == pin['git_blob'], 'source blob: ' + pin['path']) + bound[pin['path']] = raw + need(set(bound) == {ARCHIVE, FIXTURE}, 'exactly the two pinned inputs') + with tarfile.open(fileobj=io.BytesIO(bound[ARCHIVE]), mode='r:gz') as archive: + stream = archive.extractfile(MEMBER) + need(stream is not None, 'selected member missing') + payload = stream.read(2_000_001) + need(len(payload) <= 2_000_000 and hashlib.sha256(payload).hexdigest() == PAYLOAD_SHA, 'selected member SHA256') + recipes = sorted(json.loads(payload)['recipes'], key=lambda r: r['port']) + need([r['port'] for r in recipes] == list(range(112)), '112 selected ports') + labels = [r['q'] for r in recipes] + need(len(set(labels)) == 112 and all(type(q) is int and 0 < q < 512 for q in labels), 'labels in F2^9') + candidate = json.loads(bound[FIXTURE]) + candidate = candidate.get('candidate', candidate) + groups = candidate.get('blocks', candidate.get('groups')) + need(sorted(p for g in groups for p in g) == list(range(112)), 'port partition') + return labels, groups + + +def dot(a, b): + return (a & b).bit_count() & 1 + + +def reduce_basis(vectors): + pivots = {} + for v in vectors: + while v: + b = v.bit_length() - 1 + if b not in pivots: + pivots[b] = v + break + v ^= pivots[b] + return list(pivots.values()) + + +def rref_key(vectors): + """Canonical reduced echelon basis (a complete invariant of the span).""" + rows = sorted(reduce_basis(vectors), reverse=True) + for i, r in enumerate(rows): + b = r.bit_length() - 1 + for j in range(len(rows)): + if j != i and rows[j] >> b & 1: + rows[j] ^= r + return tuple(sorted(rows)) + + +def members(vectors): + """Membership mask (bit x set iff x in span) of the F2-span of vectors.""" + elems = [0] + for v in reduce_basis(vectors): + elems += [x ^ v for x in elems] + mask = 0 + for x in elems: + mask |= 1 << x + return mask + + +def elems(mask): + return [x for x in range(512) if mask >> x & 1] + + +def dim(mask): + count = mask.bit_count() + need(count & (count - 1) == 0, 'not a subspace') + return count.bit_length() - 1 + + +def rank_packed(rows): + pivots = {} + for v in rows: + while v: + b = v.bit_length() - 1 + if b not in pivots: + pivots[b] = v + break + v ^= pivots[b] + return len(pivots) + + +_BASIS = {} + + +def basis(mask): + if mask not in _BASIS: + _BASIS[mask] = sorted(reduce_basis(elems(mask))) + return _BASIS[mask] + + +def rho_elimination(left, right): + """Method 1: F2 rank of the pairing matrix between bases (bit-packed elimination).""" + bl, br = basis(left), basis(right) + return rank_packed([sum(dot(a, b) << j for j, b in enumerate(br)) for a in bl]) + + +_PERP = {} + + +def rho_counting(left, right): + """Method 2: dim L - dim(L meet R-perp), by counting vectors of F2^9.""" + if right not in _PERP: + _PERP[right] = sum(1 << x for x in range(512) if all(dot(x, r) == 0 for r in basis(right))) + return dim(left) - dim(left & _PERP[right]) + + +def cover(labels, groups): + spaces = [[labels[p] for p in g] for g in groups] + need(len(groups) == EXPECTED['groups'] and sorted(map(len, groups)) == [2] + [5] * 22, '22 five-frames and one pair') + for sp in spaces: + need(all(dot(a, b) == (i == j) for i, a in enumerate(sp) for j, b in enumerate(sp)), 'orthonormal group') + gm = [members(sp) for sp in spaces] + need(all(dim(m) == len(sp) for m, sp in zip(gm, spaces)), 'independent frame') + # Premise of the principal-rank count: no orthogonal (free) pair anywhere, so K = c I_112. + for i, j in itertools.combinations(range(len(gm)), 2): + need(rho_elimination(gm[i], gm[j]) > 0, 'free (orthogonal) group pair %d,%d' % (i, j)) + need(dim(members(labels)) == 9, 'ambient F2^9') + return spaces, gm + + +def flats_closure(gm): + """Method A: breadth-first closure of single-group spans under adding one group.""" + seen = set(gm) + frontier = list(seen) + while frontier: + nxt = [] + for L in frontier: + for g in gm: + if g & ~L: + M = members(basis(L) + basis(g)) + if M not in seen: + seen.add(M) + nxt.append(M) + frontier = nxt + return seen + + +def flats_small_subsets(gm): + """Method B: spans of all group subsets of size <= 5 (independent enumeration), + then a check that this family contains every single group and is closed + under adding any group, hence contains every span of a nonempty group set.""" + gb = [basis(g) for g in gm] + keys = set() + + def walk(start, vectors, size): + keys.add(rref_key(vectors)) + if size < 5: + for g in range(start, len(gb)): + walk(g + 1, vectors + gb[g], size + 1) + + for g in range(len(gb)): + walk(g + 1, list(gb[g]), 1) + for key in list(keys): + for b in gb: + need(rref_key(list(key) + b) in keys, 'small-subset family not closed') + return {members(list(key)) for key in keys} + + +def closure_sets(flats, gm): + return {F: frozenset(i for i, g in enumerate(gm) if g & ~F == 0) for F in flats} + + +def certificate(path=HERE / 'CERTIFICATE.json'): + data = json.loads(Path(path).read_text()) + den = data['denominator'] + need(type(den) is int and den > 0, 'denominator') + rows = [] + for row in data['sets']: + S = frozenset(row['groups']) + w = row['weight_numerator'] + need(type(w) is int and w > 0 and S and S <= frozenset(range(23)), 'certificate row') + rows.append((S, w)) + need(len({S for S, _ in rows}) == len(rows), 'distinct sets') + return den, rows + + +def check_dual(den, rows, P, rho): + """Exact dual feasibility over every ordered pair of flats.""" + hits = [[i for i in range(len(P)) if S & P[i]] for S, _ in rows] + load = [[0] * len(P) for _ in P] + for (S, w), h in zip(rows, hits): + hs = set(h) + for i in h: + row = load[i] + for j in hs: + row[j] += w + worst = None + for i in range(len(P)): + for j in range(len(P)): + need(load[i][j] <= rho[i][j] * den, 'dual constraint violated at flat pair %d,%d' % (i, j)) + slack = rho[i][j] * den - load[i][j] + worst = slack if worst is None else min(worst, slack) + return worst + + +def objective(den, rows, d): + return Q(sum(w * sum(d[g] for g in S) for S, w in rows), den) + + +def random_pairs_check(den, rows, gm, trials, seed): + """Second check of the closure reduction: arbitrary (non-closed) supports P, Q.""" + rng = random.Random(seed) + n = len(gm) + for _ in range(trials): + P = frozenset(rng.sample(range(n), rng.randint(1, n))) + Qs = frozenset(rng.sample(range(n), rng.randint(1, 3 if rng.random() < .5 else n))) + bl = reduce_basis([v for g in P for v in basis(gm[g])]) + br = reduce_basis([v for g in Qs for v in basis(gm[g])]) + rank = rank_packed([sum(dot(a, b) << j for j, b in enumerate(br)) for a in bl]) + lhs = sum(w for S, w in rows if S & P and S & Qs) + need(lhs <= rank * den, 'non-closed support pair violates the dual') + + +def exact_instance(spaces, gm, groups, den, rows, seed=2297): + """End-to-end exact rational instance: a random unit-triangular decoder with + even denominators, K = A diag(c) B^T = c0 I_112 checked entrywise, then the + chain C >= sum_S y_S hits(S) >= sum_S y_S f(S).""" + rng = random.Random(seed) + n = 112 + group_of = {p: gi for gi, g in enumerate(groups) for p in g} + A = [[Q(int(i == j)) for j in range(n)] for i in range(n)] + for _ in range(160): + i, j = sorted(rng.sample(range(n), 2)) + A[j][i] = Q(rng.choice([1, -1, 3, -3]), rng.choice([1, 2, 4, 8])) + c = [Q(rng.choice([1, -1, 1, 3]), rng.choice([1, 2, 4])) for _ in range(n)] + c0 = Q(1, 2) + inv = [[Q(0)] * n for _ in range(n)] # A^{-1} by forward substitution + for col in range(n): + x = [Q(0)] * n + for i in range(n): + x[i] = Q(int(i == col)) - sum((A[i][k] * x[k] for k in range(i) if A[i][k]), Q(0)) + for i in range(n): + inv[i][col] = x[i] + Bt = [[c0 * inv[t][j] / c[t] for j in range(n)] for t in range(n)] # B^T + for i in range(n): + Ai = [(t, A[i][t] * c[t]) for t in range(n) if A[i][t]] + for j in range(n): + need(sum((a * Bt[t][j] for t, a in Ai), Q(0)) == (c0 if i == j else 0), 'exact identity') + cost = 0 + hits = {S: 0 for S, _ in rows} + for t in range(n): + P = frozenset(group_of[i] for i in range(n) if A[i][t]) + Qs = frozenset(group_of[j] for j in range(n) if Bt[t][j]) + bl = reduce_basis([v for g in P for v in spaces[g]]) + br = reduce_basis([v for g in Qs for v in spaces[g]]) + cost += rank_packed([sum(dot(a, b) << j for j, b in enumerate(br)) for a in bl]) + for S in hits: + hits[S] += bool(S & P) and bool(S & Qs) + d = [len(sp) for sp in spaces] + need(all(hits[S] >= sum(d[g] for g in S) for S in hits), 'principal-rank count on instance') + need(Q(cost) >= Q(sum(w * hits[S] for S, w in rows), den) >= objective(den, rows, d), 'chain') + need(cost >= 554, 'instance below floor') + return cost + + +def controls(den, rows, P, rho, gm, labels, groups, spaces): + rejected = [] + + def rejects(name, fn): + try: + fn() + except Reject: + rejected.append(name) + return + raise SystemExit('FAIL: negative control was accepted: ' + name) + + rejects('inflated certificate weight', lambda: check_dual(den, [(rows[0][0], rows[0][1] + den)] + rows[1:], P, rho)) + top = max(range(len(P)), key=lambda i: len(P[i])) + bad = [row[:] for row in rho] + bad[top][top] = 8 + rejects('ambient pairing pretended degenerate (rho(all,all)=8)', lambda: check_dual(den, rows, P, bad)) + line = [[1 if len(P[i]) == 1 and len(P[j]) == 1 else rho[i][j] for j in range(len(P))] for i in range(len(P))] + rejects('line-label tariff instead of full-port tariff', lambda: check_dual(den, rows, P, line)) + rejects('doubled certificate (value 1108 > direct cost)', lambda: check_dual(den, [(S, 2 * w) for S, w in rows], P, rho)) + # Method B fed a mutated input (one group dropped) must disagree with method A. + rejects('method B fed a group list missing one group', lambda: need( + flats_small_subsets(gm[:-1]) == flats_closure(gm), 'flat mismatch')) + # Premise check: move the residual pair into E_0-perp, creating an orthogonal (free) + # group pair; cover() must reject it for exactly that reason. + perp0 = [x for x in range(1, 512) if dot(x, x) and not any(dot(x, v) for v in spaces[0])] + a, b = next((a, b) for a, b in itertools.combinations(perp0, 2) if not dot(a, b)) + mutated = list(labels) + mutated[groups[-1][0]], mutated[groups[-1][1]] = a, b + + def free_pair_cover(): + try: + cover(mutated, groups) + except Reject as exc: + if 'free (orthogonal) group pair' not in str(exc): + raise SystemExit('FAIL: free-pair control rejected for the wrong reason: %s' % exc) + raise + rejects('cover with a free (orthogonal) group pair', free_pair_cover) + return rejected + + +def main(): + labels, groups = sources() + spaces, gm = cover(labels, groups) + d = [len(sp) for sp in spaces] + fa = flats_closure(gm) + fb = flats_small_subsets(gm) + need(fa == fb and len(fa) == EXPECTED['flats'], 'two flat enumerations agree') + flats = sorted(fa, key=lambda F: (dim(F), F)) + Pmap = closure_sets(flats, gm) + P = [Pmap[F] for F in flats] + rho = [[rho_elimination(L, R) for R in flats] for L in flats] + need(rho == [[rho_counting(L, R) for R in flats] for L in flats], 'two pairing-rank methods agree') + need(all(rho[i][j] == rho[j][i] for i in range(len(P)) for j in range(len(P))), 'symmetric tariff') + den, rows = certificate() + need(len(rows) == EXPECTED['support'], 'certificate support size') + slack = check_dual(den, rows, P, rho) + value = objective(den, rows, d) + need(553 < value <= 554, 'certificate value in (553, 554]') + floor = 554 # C is an integer sum of ranks and C >= value > 553 + direct = sum(len(g) * rho_elimination(m, m) for g, m in zip(groups, gm)) + need(direct == EXPECTED['direct'] == floor, 'direct decoder attains the floor') + unpaid = Q(8, 9) * sum(len(g) * len(g) for g in groups) + threshold = unpaid.numerator // unpaid.denominator # largest integer cost with no loss + need(str(unpaid) == EXPECTED['unpaid'] and threshold == 492 and floor > threshold, 'no saving at the zero-saving threshold') + random_pairs_check(den, rows, gm, 2000, 554) + inst = exact_instance(spaces, gm, groups, den, rows) + rej = controls(den, rows, P, rho, gm, labels, groups, spaces) + result = dict(status='PASS_PR2297_PRINCIPAL_RANK_FLOOR', flats=len(P), flat_pairs=len(P) ** 2, + certificate_sets=len(rows), certificate_denominator=den, + certificate_value=str(value), certificate_value_float=float(value), min_slack_numerator=slack, + floor=floor, direct_decoder_cost=direct, zero_saving_threshold=threshold, unpaid_budget=str(unpaid), + exact_instance_cost=inst, rejected_controls=rej) + print(json.dumps(result, indent=1)) + print('PASS_PR2297_PRINCIPAL_RANK_FLOOR') + + +if __name__ == '__main__': + try: + main() + except Reject as exc: + print('FAIL:', exc) + sys.exit(1)