diff --git a/research/p112-two-total-union48-seed30/PROOF.md b/research/p112-two-total-union48-seed30/PROOF.md new file mode 100644 index 0000000000..7b38113a59 --- /dev/null +++ b/research/p112-two-total-union48-seed30/PROOF.md @@ -0,0 +1,158 @@ +# Two-column retained loss at source union 48 + +This is a scoped exact matrix statement with a finite premise certificate. It +is not a formal proof of the multiplication theorem or a proof-assistant +theorem. The geometry, the separate-total COPY model and the added-term price +lemma are inherited (PR845, PR1432, PR1787, PR1827, PR1197, PR2382). + +## Setting + +`X` is the pinned integer `112 x 8` matrix, `l_t` the source labels and `v_i` +the dual labels of `research/p112-single-lift/reference-geometry.json`. +`S_j = supp(x_j)`, `|S_j| = 56`. The pairing rank is + + beta(d, s) = rank_F2 [(v_i . l_t)]_(i in supp d, t in supp s). + +For reader `j` let `C_j` be the F2 span of the literal pairing rows +`t -> v_i . l_t` (`t in S_j`, `i in S_j`). For a port set `V` put +`K_j(V) = {c in C_j : supp c subset V}` and `g_j(U) = dim K_j(U)`; +`L(U) = sum_j g_j(U)` is the geometric loss of a deletion set `U`. + +A two-column correction is `Y = X - W`, `W = Z A^t`, `Z` `112 x 2`, `A` +`8 x 2`, so `rank W <= 2` over `C`; `U` is the set of nonzero rows of `Z`. The +retained loss is `delta_j = 8 - beta(x_j, y_j)`. + +## Finite premises (all checked by `verify.py`, no symmetry assumed) + +P1. Each `C_j` has 256 words with weights `0^1 24^63 28^128 32^63 56^1`, and +the duals `{v_i : i in S_j}` span an 8-dimensional F2 space. Hence +`u -> (u . l_t)_(t in S_j)` is a bijection from the reader's dual span onto +`C_j`. + +P2. For every ordered pair `j != k`, `|S_j cap S_k| = 24`; the cut +`C_jk = S_j cap S_k` is a word of both `C_j` and `C_k`; it is the only nonzero +word of `C_k` inside `S_j`; every other nonzero word of `C_k` has at least 12 +ports outside `S_j`. + +P3. The 112 source labels are distinct. On each of the 28 cuts, the product +`x_j x_k` takes the value `+1` on 12 ports and `-1` on 12 ports. + +P4. Closed supports (unions of codewords) of each `C_j` up to size 48 are +enumerated completely by breadth-first union (any closed support is reached +through prefix unions, which only grow). Per reader: sizes 24..32 have +dimension 1; dimension 2 has sizes 36, 40, 44; dimension 3 has 44, 46, 48; +dimension 4 occurs only at size 48 (315 supports). No closed support has size +33..35. + +## Reduction to configurations + +Let `kappa_j` be the kernel of the pairing map of reader `j` against +`supp y_j`; `dim kappa_j = delta_j` (P1). For `u in kappa_j`, the word `c_u` +vanishes on `supp y_j cap S_j`. Off `U`, `y_j = x_j`, which is nonzero on +`S_j`, so `supp c_u subset U`, and `y_j = 0` on `supp c_u`. Let `P_j` be the +union of `supp c_u` over `kappa_j`. Then + +* `P_j` is a closed support of `C_j`, `P_j subset U`, + `delta_j <= dim K_j(P_j)`; +* `W[t, j] = X[t, j]` for every `t in P_j`. + +**Condition N.** For every set `K` of at least three readers with `P_k` +nonempty, let `R_K` be the intersection of the `P_k`. Then +`X[R_K, K] = W[R_K, K]`, so `rank_Q X[R_K, K] <= 2`. This is necessary for +any two-column correction; it uses no reality, positivity, full-rank or +on-column hypothesis. + +So the realizable retained loss is at most the maximum of +`sum_k dim K_k(P_k)` over configurations of closed supports with +`|union P_k| <= |U|` that satisfy N. N is monotone (adding a reader only adds +constraints), so depth-first search may prune on failure. + +## Complete case split on the largest support `s = max |P_k|` (reader `j`) + +* `s > 36`, or `s = 36` with cap 47. Every other `P_k` satisfies + `|P_k \ P_j| <= cap - s < 12`. By P2 each word in `P_k` is then the cut + word, so `P_k = C_jk`. The search runs over all closed `P_j` and all + cut-reader subsets. +* `s = 36` with cap 48. All other closed supports with + `|P_k| <= 36` and `|P_k \ P_j| <= 12` are enumerated (words and + 36-port planes). +* `s <= 32`. Every `P_k` is a single codeword (P4). All tuples of words + from distinct readers with union `<= 48` are enumerated, with pairwise + compatibility pruning. + +The same split, with `L(U)` evaluated exactly for each union, gives the +geometric maximum. When `s > 36`, the union is a closed support of `C_j`, and +`L = dim K_j(U) + #{k : C_jk subset U}`. + +## Results + +| union cap | geometric max `L` | max loss passing N | price min | full-rank COPY floor | +|---|---|---|---|---| +| 47 | 5 | 4 | 6 | 66 | +| 48 | **8** | **5** | 6 | **65** | + +At cap 47 this is an independent reproduction of PR2382's statements (geometric +maximum 5, rank-two bound 4, floor 66). The census of single-word unions also +matches PR2382 exactly: `2032, 280252, 9072, 42, 0` by reader-subset size. + +At 48 the geometric maximum jumps to 8. For example, reader 0 has a +four-dimensional 48-port support containing four cuts: loss vector +`(4,0,1,1,1,1,0,0)`. There are also seven 8-reader single-word unions. Every +such configuration violates N: the recorded witness has a rank-3 integer minor +on rows `{0,1,2,3,12,13,14,15}` and columns `{0,2,3}`. + +N-passing configurations with total loss 5 occur in shapes `4+1`, `3+1+1`, +`2+1+1+1` (lead dimension at least 2) and `1+1+1+1+1` (448 single-word +tuples). Nothing passes at 6 or more. + +**Attainment.** Let `V` be the first four-dimensional 48-port support of reader +0 that contains a cut, here `C_01`. Take `Z = [x_0 1_V, x_1 1_(C_01)]`, +`A = [e_0, e_1]`. Both have rank 2, `U = V` has 48 ports, and `rank[X Z] = 10`. +The identity `XX^t = XY^t + (XA)Z^t` is checked on all 12,544 ordered pairs. +The exact retained COPY ranks are `(4,7,8,8,8,8,8,8)`, so retained loss is 5. +The added COPY ranks are `(8,7)`, giving a total bill of **74**. + +So PR2382's "retained loss at most 4" bound, which PR2382 states only through +47, **does not extend to 48**: the two-column bound there is exactly 5. The +representative `A = [e_0, e_1]` lies in PR1197's disjoint-coefficient class; +the same `W = ZA^t` in an overlapping basis (`Z -> ZG`, `A -> A G^{-t}`) +keeps retained loss 5, but that representative's added bill was not computed. + +**Floor.** In the full-rank on-column (PR1197 residual) case both added terms are nonzero. By the +inherited PR845/PR1432 price lemma, an added source with `m` active labels +has COPY rank at least `p(m) = min{r >= 1 : m <= 2^(r+1)}`. By P3, +`m_1 + m_2 >= 48`. The exhaustive integer minimum is `p(1)+p(47) = 6`. So the +COPY rank sum is at least `64 - 5 + 6 = 65` when `|U| = 48` (a lower bound, +not an attained minimum). The result does +**not** show that 65 is attained: the loss-5 witness costs 74. PR1197's +complementary rank-one/off-column reductions are inherited unchanged, as in +PR2382, so the general fixed-reader no-saving statement (COPY at least 64) +holds at union 48 as well. + +**Partial sharpening for shape `4+1`.** Here `P_j` is a four-dimensional +48-port support, and `P_k = C_jk` must lie inside it, since the budget is 0. +In the full-rank case, `col Z = col W = span(w_j, w_k)`. On `C_jk`, a +combination `a w_j + b w_k` equals `a x_j + b x_k`. + +- If `a` and `b` are both nonzero, it vanishes only where `x_j x_k = -a/b`. + By P3 at least 12 of the 24 ports remain nonzero. +- If `b = 0`, the support has at least 48 ports. +- If `a = 0`, the support has at least 24 ports. + +So both added sources have at least 12 active labels. With +`m_1 + m_2 >= 48`, the price minimum is then `p(16) + p(32) = 7`, and every +`4+1` correction has COPY at least `59 + 7 = 66`. This is a written +argument; verify.py machine-checks its premise P3 but not the constrained +price minimum 7 (independently recomputed by review). The shapes `3+1+1`, +`2+1+1+1` and `1^5` are not analysed this way. Hence the overall floor +stated is still 65. + +## Scope + +All helpers, source access, frames, restoration and recursion are free in this +screen. Only the separate-total pairing-rank sum is bounded. Condition N is a +necessary condition; except for `4+1`, the sufficiency of the N-passing +shapes is not decided, and it is not needed for the stated floor. Bands 49 and +above, changed readers, masked exactness and physical delivery are +unexamined. A finite enumeration is not a formal proof of the written +implications. diff --git a/research/p112-two-total-union48-seed30/README.md b/research/p112-two-total-union48-seed30/README.md new file mode 100644 index 0000000000..0a3b80db8d --- /dev/null +++ b/research/p112-two-total-union48-seed30/README.md @@ -0,0 +1,177 @@ +# P112 two-total correction at source union 48 + +**Negative result / research note. No new κ, supplier or decoder.** + +At source union **48**, the deletion geometry of the eight P112 coordinate +readers changes. One deletion set can remove **eight** rank units (up from +five at 44–47). A two-column correction `ZA^t` can realize retained loss +**exactly 5** there. PR2382's bound of 4 was stated only through 47 and does +not extend to 48. + +- **Upper bound (5).** Every configuration with loss 6 or more contains a + fully specified column subset of rank 3, which a rank-two correction cannot + match. +- **Attainment (5).** An explicit full-rank two-column decoder attains it, + with total bill 74. Its representative `A = [e_0, e_1]` lies in PR1197's + disjoint-coefficient class; the same `W` in an overlapping basis + (`Z -> ZG`, `A -> A G^{-t}`) keeps retained loss 5, but that + representative's added bill was not computed. + +Charging both added terms with the inherited price lemma gives a +**provable lower bound of 65 on the full-rank on-column (PR1197 residual) +fixed-reader two-total COPY sum at union 48** (attainment open; the explicit +loss-5 witness costs 74). The provable bound is one less than the 66 that +holds for unions 44..47, but still above 64; this does not mean a cheaper +decoder exists. For the realized +`4+1` shape, a further support argument raises the bill to at least 66; the +other loss-5 shapes are not analysed this way (written argument in +PROOF.md; verify.py machine-checks its premise P3, the 12/12 cut sign +balance, not the constrained price minimum 7). With PR1197's complementary +reductions inherited unchanged, the fixed-reader two-total no-saving +statement (COPY rank sum at least 64) **extends to union 48**. The chain is: +PR1787 (merged) and PR1827 for unions of at most 43; this package's +independent cap-47 replay (price minimum 6 for `M = 44..47`) for 44..47; the +new band-48 result; and PR1197. It does not rely on PR2382, which is open. The 65 floor is a relaxation; its attainment is open, since the +explicit witness costs 74. This closes band 48 of PR2382's open next +question 1. It is not a route to a cheaper decoder. + +## What is checked + +[verify.py](verify.py) is an independent stdlib re-implementation that +imports no predecessor checker. It uses exact `Fraction` and F2 arithmetic. + +1. It builds the reader codes `C_j` from the **literal pairing rows** and + checks P1–P3 of [PROOF.md](PROOF.md): weights, dual-span dimension 8, + unique cut word with 12-port margin, and distinct labels. +2. It enumerates all closed supports up to 48 ports for every reader. The + census at dimension 4 has 315 supports, all of size 48. +3. It enumerates every retained-loss configuration with union at most 47 or + at most 48, using the lead-support case split of PROOF.md. For each + configuration it computes the geometric loss and applies the rank-two + **condition N** (exact rational rank of every fully specified column + subset of size at least 3). +4. It builds the explicit loss-5 witness: readers 0 and 1, `U` a + four-dimensional 48-port support of reader 0 containing the cut `C_01`. + It checks the identity `XX^t = XY^t + (XA)Z^t` on all 12,544 pairs and + computes exact retained and added COPY ranks, `(4,7,8,8,8,8,8,8)` and + `(8,7)`. +5. It computes the PR1432/PR845 price relaxation for `M = 44..48`. The + minimum is 6 for each. + +| union cap | geometric max loss | two-column loss bound | full-rank floor | +|---|---|---|---| +| ≤ 47 (positive control; floor for `M = 44..47`, PR1827 below 44) | 5 | 4 | 66 | +| ≤ 48 | **8** | **5** (attained) | **65** | + +The cap-47 run reproduces PR2382 independently. It matches the geometric +maximum 5, the rank-two bound 4, the floor 66 and the single-word union +census `2032, 280252, 9072, 42, 0`. + +New at 48: + +- 8-loss sets, such as `(4,0,1,1,1,1,0,0)` and seven 8-reader single-word + unions, all excluded by a rank-3 minor; +- N-passing loss-5 shapes `4+1`, `3+1+1`, `2+1+1+1` and `1^5`. + +Only `4+1` is realized explicitly. Sufficiency is not decided for the other +shapes. + +**Negative controls** (must be rejected): a one-byte corrupted geometry +(sha256 pin), a perturbed minor (third column replaced by the sum of the +first two, rank 3 → 2), a three-column fake profile (retained loss 6 but +`rank W = 3`, so not a two-column correction), and a corrupted receipt (the +same `receipt_matches` function used for the real comparison must reject a +copy of RESULT.json with the floor field incremented; an end-to-end mutation +of RESULT.json on disk was also checked by review to give `FAIL RESULT.json +mismatch`). + +## Reproduce + +From the repository root (CPython 3.12+, standard library only; measured on CPython 3.14, +Linux x86-64, one core: about 165 s and peak RSS about 175 MB): + +```sh +python3 -I -B research/p112-two-total-union48-seed30/verify.py +``` + +Expected final line: + +``` +PASS_P112_TWO_TOTAL_UNION48 geometric_max_47=5 geometric_max_48=8 two_column_loss_bound_47=4 two_column_loss_bound_48=5 loss5_witness_bill=74 full_rank_copy_floor_48=65 no_new_kappa +``` + +Package metadata: `python3 scripts/research_package.py --package research/p112-two-total-union48-seed30`. +A fresh receipt can be written with `--write /new/path.json`; overwriting is +refused. + +## Scope, inherited assumptions, unresolved obligations + +- **Base commit:** `0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2`. +- **Input pin:** `research/p112-single-lift/reference-geometry.json`, sha256 + `4f44af36…7a080`; see [SOURCES.json](SOURCES.json). +- **Selected record:** unchanged (`certificates/selected-result.json`, + κ 0.001672660197076918). +- **Inherited:** the separate-total COPY model; the PR845/PR1432 added-term + price lemma `r >= p(m)`, which is not re-proved here; and PR1197's rank-one, + off-column and disjoint-coefficient reductions for the general ≥64 + statement. +- **Proved here:** the two-column retained-loss bound uses only + `rank(ZA^t) <= 2`. It holds for complex, off-column or rank-deficient + factors. +- **Not shown:** + - that the 65 floor is attained; + - whether the N-passing shapes other than `4+1` are realizable; + - anything about unions of 49 or more, changed readers, masked exactness, + power sums or physical delivery. +- **Unchanged and out of scope:** the inherited all-size/compiler, + mutable-source/hosting, precision/tape, analytic-transfer and bit H1–H5 + obligations listed by PR1197 and the selected record. + + All helper, access, frame, restoration and recursive costs are free in this + screen. +- **Status of the argument:** the written argument in PROOF.md, together with + the finite enumeration, is not a formal proof. + +## Open next questions + +Structured versions with relevance, first steps and blockers are in +[TASK.json](TASK.json). + +1. **Is the 65 relaxation floor attained at 48?** This needs a loss-5 + two-column correction one of whose sources has at most four active + labels. If none exists, the 66 floor extends to 48. For shape `4+1` it + cannot happen: by the 12/12 sign balance of `x_j x_k` on every cut, every + nonzero vector of `col W` has at least 12 ports, so that shape costs at + least 66 (PROOF.md). The remaining shapes `3+1+1`, `2+1+1+1` and `1^5` + need the same minimum-support analysis of `col W` from their patterns. + Blocker: their free entries make this a joint price/realizability + question. +2. **Bands 49–51.** The census has no closed supports of size 37–39, so at + 49 every lead with `s > 36` has `s >= 40` and budget at most 9 < 12, and + that branch stays cut-only. What changes is the `s = 36` branch (budget + 13) and any new supports of size 49 or more, so extend the census past 48 + and widen the `s = 36` enumeration. Geometric losses already reach 8. +3. **Realizability of `3+1+1`, `2+1+1+1` and `1^5` at 48.** First step: + solve the per-row conditions `x_r|K_r in col(A[K_r,:])` exactly in `A`. + +## Credit + +This package continues PR2382 by Sricharan Vagvala (@theon199), head +`2d7807f6`, which is open. PR2382 is cited, and its numbers at ≤47 are +reproduced independently; its code is not imported. + +Further predecessors: + +- Philipp/mightyOil: PR1827 (joint losses through 43) and PR1197 + (complementary reductions); +- Josie Elliston: PR1787 (support threshold); +- Mihir Srivastava: PR845 (P112 geometry and added-reader premise); +- woklerx: PR998; +- Hanson Sun/bbMisk: PR1432 (price from rank); +- commdata2338: PR1375; +- DreamingOfClouds: the separate-total COPY model and the PR717 geometry + arrays (pinned via PR845's snapshot); +- Joel Pulikkan/GamingPuzzled: PR620 (COPY-64 lineage). + +Prepared by thakrarsagar with substantial AI assistance from Claude +(Anthropic, Claude Opus 5.5). Apache-2.0. diff --git a/research/p112-two-total-union48-seed30/RESULT.json b/research/p112-two-total-union48-seed30/RESULT.json new file mode 100644 index 0000000000..54185762cc --- /dev/null +++ b/research/p112-two-total-union48-seed30/RESULT.json @@ -0,0 +1,472 @@ +{ + "bands": { + "47": { + "geometric_max_L": 5, + "lead_dim_ge2": { + "N_passing_config_shapes_total_ge5": {}, + "N_passing_max": 4, + "geometric_max": 5, + "geometric_value_histogram": { + "2": 75936, + "3": 68096, + "4": 34216, + "5": 672 + } + }, + "price_min": 6, + "single_words": { + "N_passing_max": 3, + "N_passing_tuples_by_size": { + "1": 2032, + "2": 287308, + "3": 5544 + }, + "distinct_unions_by_reader_subset_size": { + "1": 2032, + "2": 280252, + "3": 9072, + "4": 42 + }, + "geometric_max_readers": 4, + "word_tuples_by_size": { + "1": 2032, + "2": 287308, + "3": 11424, + "4": 42 + } + }, + "two_column_retained_loss_upper_bound": 4 + }, + "48": { + "geometric_max_L": 8, + "geometric_witness": { + "N_violation": { + "cols": [ + 0, + 2, + 3 + ], + "rank": 3, + "rows": [ + 0, + 1, + 2, + 3, + 12, + 13, + 14, + 15 + ] + }, + "U_ports": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 12, + 13, + 14, + 15, + 16, + 17, + 18, + 19, + 48, + 49, + 50, + 51, + 52, + 53, + 54, + 55, + 56, + 57, + 58, + 59, + 60, + 61, + 62, + 63, + 64, + 65, + 66, + 67, + 68, + 69, + 70, + 71, + 72, + 73, + 74, + 75, + 76, + 77, + 78, + 79 + ], + "U_size": 48, + "lead_reader": 0, + "loss_vector": [ + 4, + 0, + 1, + 1, + 1, + 1, + 0, + 0 + ] + }, + "lead_dim_ge2": { + "N_passing_config_shapes_total_ge5": { + "2+1+1+1": 896, + "3+1+1": 2016, + "4+1": 3360 + }, + "N_passing_max": 5, + "geometric_max": 8, + "geometric_value_histogram": { + "2": 75936, + "3": 287616, + "4": 145320, + "5": 21280, + "6": 6048, + "8": 7224 + } + }, + "price_min": 6, + "single_word_five_tuple_passing_N_example": { + "0": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 8, + 9, + 10, + 11, + 12, + 13, + 14, + 15, + 16, + 17, + 18, + 19, + 20, + 21, + 22, + 23 + ], + "1": [ + 1, + 3, + 4, + 6, + 8, + 10, + 13, + 15, + 16, + 18, + 20, + 22, + 83, + 85, + 86, + 87, + 88, + 95, + 96, + 103, + 104, + 105, + 106, + 108 + ], + "2": [ + 0, + 1, + 2, + 3, + 12, + 13, + 14, + 15, + 80, + 81, + 82, + 83, + 84, + 85, + 86, + 87, + 104, + 105, + 106, + 107, + 108, + 109, + 110, + 111 + ], + "4": [ + 4, + 5, + 6, + 7, + 16, + 17, + 18, + 19, + 80, + 81, + 86, + 87, + 88, + 89, + 94, + 95, + 96, + 97, + 102, + 103, + 104, + 105, + 110, + 111 + ], + "6": [ + 8, + 9, + 10, + 11, + 20, + 21, + 22, + 23, + 82, + 83, + 84, + 85, + 88, + 89, + 94, + 95, + 96, + 97, + 102, + 103, + 106, + 107, + 108, + 109 + ] + }, + "single_words": { + "N_passing_max": 5, + "N_passing_tuples_by_size": { + "1": 2032, + "2": 699132, + "3": 37856, + "4": 2576, + "5": 448 + }, + "distinct_unions_by_reader_subset_size": { + "1": 2032, + "2": 692076, + "3": 55832, + "4": 3850, + "5": 448, + "6": 196, + "7": 56, + "8": 7 + }, + "geometric_max_readers": 8, + "word_tuples_by_size": { + "1": 2032, + "2": 699132, + "3": 85400, + "4": 6986, + "5": 1232, + "6": 196, + "7": 56, + "8": 7 + } + }, + "two_column_retained_loss_upper_bound": 5 + } + }, + "closed_support_census_each_reader_cap48": { + "dim1_size24": 63, + "dim1_size28": 128, + "dim1_size32": 63, + "dim2_size36": 336, + "dim2_size40": 4977, + "dim2_size44": 5040, + "dim3_size44": 1260, + "dim3_size46": 10752, + "dim3_size48": 35280, + "dim4_size48": 315 + }, + "floors": { + "full_rank_two_total_copy_floor_at_48": 65, + "full_rank_two_total_copy_floor_cap47": 66, + "relaxation_floor_attained_by_loss_bound_at_48": true + }, + "geometry": { + "path": "research/p112-single-lift/reference-geometry.json", + "sha256": "4f44af368e046002553d632ee90c6470990827cea3fae41f0f54018522d7a080" + }, + "negative_controls": { + "corrupted_geometry_pin": "rejected", + "perturbed_minor": { + "original_rank": 3, + "perturbed_rank": 2, + "status": "rejected" + }, + "three_column_fake_profile": { + "rank_W": 3, + "readers": [ + 0, + 1, + 3 + ], + "retained_loss": 6, + "status": "rejected" + } + }, + "premises": { + "code_weights_all_readers": [ + [ + 0, + 1 + ], + [ + 24, + 63 + ], + [ + 28, + 128 + ], + [ + 32, + 63 + ], + [ + 56, + 1 + ] + ], + "cuts_with_sign_balance_12_12": 28, + "distinct_source_labels": 112, + "ordered_pairs_with_unique_cut_word_and_margin_12": 56 + }, + "price_min_by_M": { + "44": 6, + "45": 6, + "46": 6, + "47": 6, + "48": 6 + }, + "two_column_loss5_witness": { + "U_ports": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 8, + 9, + 10, + 11, + 12, + 13, + 14, + 15, + 16, + 17, + 18, + 19, + 20, + 21, + 22, + 23, + 50, + 51, + 52, + 53, + 56, + 57, + 58, + 59, + 60, + 61, + 62, + 63, + 64, + 65, + 66, + 67, + 68, + 69, + 70, + 71, + 74, + 75, + 76, + 77 + ], + "U_size": 48, + "added_copy_ranks": [ + 8, + 7 + ], + "identity_pairs_checked": 12544, + "kernel_dim_at_j_via_code": 4, + "rank_A": 2, + "rank_W": 2, + "rank_X_Z": 10, + "rank_Z": 2, + "reader_j": 0, + "reader_k": 1, + "retained_copy_ranks": [ + 4, + 7, + 8, + 8, + 8, + 8, + 8, + 8 + ], + "retained_losses": [ + 4, + 1, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "retained_sum": 59, + "total_copy_bill": 74, + "z_support_sizes": [ + 48, + 24 + ] + } +} diff --git a/research/p112-two-total-union48-seed30/SOURCES.json b/research/p112-two-total-union48-seed30/SOURCES.json new file mode 100644 index 0000000000..155fdf522c --- /dev/null +++ b/research/p112-two-total-union48-seed30/SOURCES.json @@ -0,0 +1,48 @@ +{ + "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/p112-single-lift/reference-geometry.json", + "usage": "input", + "git_blob": "d862663d3c0ffe3c72df510e89997beb85cef640", + "sha256": "4f44af368e046002553d632ee90c6470990827cea3fae41f0f54018522d7a080" + }, + { + "path": "research/p112-two-total-rank-one-seed21/PROOF.md", + "usage": "provenance", + "git_blob": "4ec1af4cc9f7d47872a725fc37f3d400e9c2b3c3", + "sha256": "7209dd082f47dca3d096ceb30b9efd674d6332d5ca0e4decd22337b0b3b87d6f" + }, + { + "path": "research/p112-joint-support-loss-audit/PROOF.md", + "usage": "provenance", + "git_blob": "d0b0ba257cc7fb8d0f18dc5a029dcec30cb09207", + "sha256": "7910ab892db60688540c78b2b2086ffeacefdd89674bcd2d1e9b4d4f696cbc74" + }, + { + "path": "research/p112-two-total-support-threshold/PROOF.md", + "usage": "provenance", + "git_blob": "0adcdee227ac6f68029a38988ab8ea88dcb61475", + "sha256": "10380b65a022e56eac6e6e5d5e7178666a1819eb1a65d90b8172e39d198c0988" + }, + { + "path": "research/p112-single-lift/PROOF.md", + "usage": "provenance", + "git_blob": "609a2b1f83f17523a570a1a2e1731817c87a587a", + "sha256": "02147aa2a93a449dcbd15886b42d993bd0dbb554d7c15d347a9567fbe2a442e1" + } + ] +} diff --git a/research/p112-two-total-union48-seed30/TASK.json b/research/p112-two-total-union48-seed30/TASK.json new file mode 100644 index 0000000000..7c840b24b5 --- /dev/null +++ b/research/p112-two-total-union48-seed30/TASK.json @@ -0,0 +1,99 @@ +{ + "schema_version": 1, + "task_id": "complex-rank-shape-decoder", + "priority_revision": 4, + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "original_card": { + "id": "complex-rank-shape-decoder", + "question": "Can a decoder deliver the local paid mass in fewer, larger-rank children (block frame climbs instead of rank-1 to rank-3 steps)?", + "starting_points": [ + "research/complex-local-word-ceiling/README.md", + "research/complex-decoder-field-extension-seed44/README.md", + "research/complex-frame-pair-decoders/README.md", + "research/selected-k8-unrestricted-ends/README.md", + "research/eisenstein-reduction-copy-floor/README.md" + ], + "methods": [ + "Find one exact small decoding identity whose frame path climbs in blocks, and price its complete per-call profile.", + "Bound the best effective child rank achievable for one fixed support alphabet, including copies, frames and restoration." + ], + "acceptance_gate": "A per-call local profile, with all copied information, frames and restoration counted, whose ceiling exceeds the selected word's by at least 5%; masked or overcomplete supports must change an assumption of the eight-term all-pairs bound.", + "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": "Before any synthesis, write the candidate per-call local profile (and centre charge / unpaid coordinates if changed) and screen it with ceiling.ceiling(); reject it if even the ideal ceiling does not beat the selected word's by your stated margin. Ideal budget: rank-16 delivery is 2.31x (levers.py).", + "bottleneck_link": "Rank-1 children are about half of recursive cost; the selected word's effective child rank is about 3.9. Larger-rank delivery lowers recursive cost per unit of paid mass.", + "allowed_variations": [ + "One masked, overcomplete or block decoder family with exact labels and supports.", + "A scoped lower bound on effective rank for one alphabet.", + "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": [ + "Repacking idle remainders of an unchanged word (covered by the packing ceiling).", + "Repeating the eight-term all-pairs search inside its proved scope.", + "Only changing helper terminal subspaces and monotone frames within the fixed scalar word, entrances and cleanup contract already covered by #1995/#2013.", + "Searching below C=40 in the #2017 Eisenstein binary scalar-rectangle or fixed-support block-linear additive pairing model; specify a changed premise instead. This bound does not cover every complex decoder." + ], + "overlap_terms": [ + "rank shape", + "block climb", + "masked decoder", + "overcomplete", + "effective rank" + ] + }, + "scope_status": "changed", + "actual_scope": "In the pinned P112 fixed-reader exact two-total decoder XX^t = XY^t + (XA)Z^t, Y = X - ZA^t (A 8x2, Z 112x2), with deletion union U = supp(z1) u supp(z2) of size at most 48: what is the exact geometric maximum retained loss L(U), what is the maximum retained loss realizable by a rank-two correction ZA^t, and what COPY rank-sum floor follows when both added terms are charged (PR2382 open next question 1, band 48)?", + "scope_change_reason": "The card asks for block-climb decoders; this package answers a concrete, unclaimed open boundary of the complex supplier's P112 decoder COPY bill (PR2382 OQ1, discussion 2369 handoff). It decides whether the separate-total no-saving range extends to source union 48 and records the new loss geometry there.", + "bottleneck_link": "Side result on the complex supplier's P112 decoder COPY bill: a fixed-reader two-total decoder could only lower copied information if its COPY rank sum drops below 64. This package shows that at source union 48 it cannot in the full-rank on-column case (provable lower bound 65; attainment open, the explicit loss-5 witness costs 74), so it is not a route to a new kappa.", + "budget_minutes": 90, + "stop_rule": "Stop once band 48 is closed: complete enumeration of all closed-support configurations plus an exact rank-two necessary condition and an explicit realization proving the stated floor, or an explicit realizable profile with its bill. Bands 49+ out of scope. Hard stop 2026-10-15T15:03:33Z for experiments.", + "outcome": "negative-result", + "evidence": "verify.py (stdlib, exact Fraction/F2 arithmetic, ~165 s, peak RSS ~175 MB on CPython 3.14) recomputes all closed supports of the eight reader codes up to size 48, enumerates every retained-loss configuration with union <= 47 and <= 48 by a lead-support case split, applies the rank-two necessary condition to every fully specified column subset, and checks an explicit two-column witness on all 12,544 identity pairs. Results: geometric max L = 5 (<=47, reproducing PR2382) and 8 (48); rank-two retained loss bound 4 (<=47) and 5 (48), the latter attained (bill 74); price minimum 6; full-rank on-column COPY lower bound 66 (unions 44..47) and 65 (48; attainment open, witness bill 74). RESULT.json is compared exactly; four negative controls must be rejected.", + "author": "thakrarsagar", + "ai_assistance": "Substantial AI assistance from Claude (Anthropic, Claude Opus 5.5) for mathematics, implementation, checks and writing, in an automated research-sprint loop; author-run evidence, no independent human review.", + "open_questions": [ + { + "question": "Is the relaxation floor 65 at union 48 attained by an actual decoder, i.e. is there a two-column correction with retained loss 5 whose two added COPY ranks sum to 6?", + "why_it_matters": "The only explicit loss-5 witness has bill 74; if no loss-5 correction can have a source of at most four active labels, the full-rank floor at 48 is at least 66 and the PR2382 bound extends unchanged.", + "first_step": "Shape 4+1 costs >= 66 by a written argument in PROOF.md (12/12 cut sign balance, machine-checked as premise P3, forces >= 12 ports for every nonzero vector of col W; the constrained price minimum 7 is not scripted). For shapes 3+1+1, 2+1+1+1 and 1^5, derive the minimum support of a nonzero vector in col W from their patterns and free entries.", + "blocked_by": "Requires a joint price/realizability argument (sufficiency of the rank-two completion for each shape is not decided here)." + }, + { + "question": "Do bands 49..51 keep the two-column retained loss at most 6 (COPY >= 64)?", + "why_it_matters": "It would extend the fixed-reader two-total no-saving range beyond 48; geometric losses already reach 8 at 48.", + "first_step": "Re-run the lead-support case split with cap 49: no closed supports of size 37..39 exist, so leads with s>36 have s>=40 and stay cut-only; widen the s=36 branch to 13 outside ports and extend the closed-support census past 48.", + "blocked_by": "Closed-support enumeration grows quickly above 48; the s=36 branch budget rises to 13." + }, + { + "question": "Which of the N-passing shapes 3+1+1, 2+1+1+1 and 1^5 at union 48 are actually realizable by a rank-two correction?", + "why_it_matters": "Only 4+1 is realized explicitly; the minor test is necessary, not sufficient. A complete classification would show which loss geometries a two-column decoder can use.", + "first_step": "For each shape class, parametrize A (8x2) and solve the per-row linear conditions x_r|K_r in col(A[K_r,:]) exactly.", + "blocked_by": "Polynomial feasibility in A; not needed for the floor because 5 is already attained." + } + ], + "predecessors": { + "PR2382": "Sricharan Vagvala/theon199, head 2d7807f60f19146947ad24cb22719d4048a92be3 (open; cited, not imported)", + "PR1827": "Philipp/mightyOil, research/p112-joint-support-loss-audit", + "PR1197": "Philipp/mightyOil, research/p112-two-total-rank-one-seed21", + "PR1787": "Josie Elliston, research/p112-two-total-support-threshold", + "PR845": "Mihir Srivastava, research/p112-single-lift", + "PR998": "woklerx", + "PR1432": "Hanson Sun/bbMisk", + "PR1375": "commdata2338", + "model": "DreamingOfClouds separate-total COPY model" + }, + "assignment": { + "seed": 30, + "seed_source": "OS random 0..99, drawn once", + "track": "20-39 Complex supplier", + "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1163#discussioncomment-18950859" + } +} diff --git a/research/p112-two-total-union48-seed30/VERIFY.json b/research/p112-two-total-union48-seed30/VERIFY.json new file mode 100644 index 0000000000..fa975e1244 --- /dev/null +++ b/research/p112-two-total-union48-seed30/VERIFY.json @@ -0,0 +1,21 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/p112-single-lift/reference-geometry.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 540, + "checks": "Source pin; reader codes from literal pairing rows; closed-support census to size 48; complete lead-support configuration enumeration at caps 47 and 48 with exact rank-two minor screening; explicit loss-5 two-column witness (identity on 12,544 pairs, exact F2 pairing ranks, bill 74); price relaxation; corrupted-pin, perturbed-minor, three-column fake-profile and corrupted-receipt controls; exact comparison with RESULT.json. Prints PASS_P112_TWO_TOTAL_UNION48 ... full_rank_copy_floor_48=65 no_new_kappa." + } + ] +} diff --git a/research/p112-two-total-union48-seed30/verify.py b/research/p112-two-total-union48-seed30/verify.py new file mode 100644 index 0000000000..e9e6665b57 --- /dev/null +++ b/research/p112-two-total-union48-seed30/verify.py @@ -0,0 +1,604 @@ +#!/usr/bin/env python3 +"""P112 fixed-reader two-total correction at source union 48 (PR2382 OQ1). + +Independent stdlib re-implementation; imports no predecessor checker. + +Computes, from the pinned P112 geometry and the literal pairing rows: + * the eight reader codes C_j and all their closed supports of size <= 48; + * the exact geometric maximum L(U) = sum_j g_j(U) over |U| <= 47 and <= 48; + * the maximum total retained loss of any configuration that passes the + rank-two necessary condition N (every fully specified column subset of + size >= 3 has exact rational rank <= 2), at caps 47 and 48; + * an explicit two-column correction attaining retained loss 5 at |U| = 48, + with exact pairing ranks and its complete separate-total COPY bill; + * the PR1432/PR845 added-term price relaxation at M = 44..48; + * negative controls (corrupted geometry pin, perturbed minor, three-column + fake profile, corrupted receipt) which must be rejected. + +Usage: python3 -B verify.py (compare with RESULT.json, print PASS) + python3 -B verify.py --write P (write a fresh receipt to new path P) + +Prepared by thakrarsagar with substantial AI assistance from Claude +(Anthropic, Claude Opus 5.5). Apache-2.0. +""" +import hashlib +import itertools +import json +import os +import sys +from fractions import Fraction + +HERE = os.path.dirname(os.path.abspath(__file__)) +ROOT = os.path.dirname(os.path.dirname(HERE)) +GEOM_REL = "research/p112-single-lift/reference-geometry.json" +GEOM_SHA = "4f44af368e046002553d632ee90c6470990827cea3fae41f0f54018522d7a080" +NPORT = 112 +NREAD = 8 + + +class CheckFailure(Exception): + pass + + +def require(cond, msg): + if not cond: + raise CheckFailure(msg) + + +def pc(x): + return bin(x).count("1") + + +def load_geometry(raw): + require(hashlib.sha256(raw).hexdigest() == GEOM_SHA, "geometry sha256 mismatch") + return json.loads(raw.decode("utf-8")) + + +def par(a): + return pc(a) & 1 + + +def f2_rank(rows): + basis = {} + r = 0 + for v in rows: + while v: + h = v.bit_length() - 1 + if h in basis: + v ^= basis[h] + else: + basis[h] = v + r += 1 + break + return r + + +def q_rank(M): + M = [[Fraction(v) for v in row] for row in M] + if not M: + return 0 + r = 0 + for c in range(len(M[0])): + p = next((i for i in range(r, len(M)) if M[i][c] != 0), None) + if p is None: + continue + M[r], M[p] = M[p], M[r] + for i in range(len(M)): + if i != r and M[i][c] != 0: + f = M[i][c] / M[r][c] + M[i] = [a - f * b for a, b in zip(M[i], M[r])] + r += 1 + return r + + +def mask_list(m): + return [r for r in range(NPORT) if m >> r & 1] + + +class Geometry: + def __init__(self, G): + self.X = G["X"] + self.lab = G["labels"] + self.dua = G["duals"] + require(len(self.X) == NPORT and all(len(r) == NREAD for r in self.X), "X shape") + self.S = [[r for r in range(NPORT) if self.X[r][j] != 0] for j in range(NREAD)] + self.SM = [sum(1 << r for r in s) for s in self.S] + # literal pairing rows: row i of reader j is the word t -> v_i . l_t on S_j + self.codes = [] + for j in range(NREAD): + span = {0} + for i in self.S[j]: + w = 0 + for t in self.S[j]: + if par(self.dua[i] & self.lab[t]): + w |= 1 << t + if w not in span: + span |= {s ^ w for s in span} + self.codes.append(sorted(span)) + self.cut = [[self.SM[j] & self.SM[k] for k in range(NREAD)] for j in range(NREAD)] + + def beta(self, reader_support, source_support): + """Independent engine: literal F2 rank of the pairing matrix.""" + rows = [] + for i in range(NPORT): + if reader_support >> i & 1: + w = 0 + for t in range(NPORT): + if source_support >> t & 1 and par(self.dua[i] & self.lab[t]): + w |= 1 << t + rows.append(w) + return f2_rank(rows) + + def kdim(self, j, V): + n = sum(1 for c in self.codes[j] if c & ~V == 0) + d = n.bit_length() - 1 + require(n == 1 << d, "kernel not a subspace") + return d + + +def premises(g): + out = {} + wd = [] + for j in range(NREAD): + c = g.codes[j] + require(len(c) == 256, "code size") + dist = {} + for w in c: + dist[pc(w)] = dist.get(pc(w), 0) + 1 + wd.append(sorted(dist.items())) + # dual span of reader j has F2 dimension 8, so u -> c_u is a bijection + require(f2_rank([g.dua[i] for i in g.S[j]]) == 8, "dual span dim") + require(all(w == wd[0] for w in wd), "weight distributions differ") + require(wd[0] == [(0, 1), (24, 63), (28, 128), (32, 63), (56, 1)], "weights") + out["code_weights_all_readers"] = [list(x) for x in wd[0]] + margins = set() + for j in range(NREAD): + for k in range(NREAD): + if j == k: + continue + cjk = g.cut[j][k] + require(pc(cjk) == 24, "cut size") + require(cjk in g.codes[j] and cjk in g.codes[k], "cut word") + inside = [c for c in g.codes[k] if c and c & ~g.SM[j] == 0] + require(inside == [cjk], "unique word of C_k inside S_j") + margins.add(min(pc(c & ~g.SM[j]) for c in g.codes[k] if c and c != cjk)) + require(margins == {12}, "outside margin") + out["ordered_pairs_with_unique_cut_word_and_margin_12"] = 56 + # distinct source labels, so |supp z_h| active ports give |supp z_h| labels + require(len(set(g.lab)) == NPORT, "source labels not distinct") + out["distinct_source_labels"] = NPORT + # sign balance of x_j x_k on every cut (used for the 4+1 support remark) + for j in range(NREAD): + for k in range(j + 1, NREAD): + pr = [g.X[r][j] * g.X[r][k] for r in mask_list(g.cut[j][k])] + require(sorted(set(pr)) == [-1, 1] and pr.count(1) == 12 and pr.count(-1) == 12, + "cut sign balance") + out["cuts_with_sign_balance_12_12"] = 28 + return out + + +def closed_supports(g, cap): + """All unions of codewords of C_j of size <= cap, with dim K_j(V).""" + res = [] + for j in range(NREAD): + words = [c for c in g.codes[j] if c and pc(c) <= cap] + seen = set(words) + fr = list(seen) + while fr: + nf = [] + for V in fr: + for c in words: + W = V | c + if W != V and W not in seen and pc(W) <= cap: + seen.add(W) + nf.append(W) + fr = nf + res.append({V: g.kdim(j, V) for V in seen}) + return res + + +class NCheck: + """Necessary condition for a rank-<=2 correction W = Z A^t with + W[r,k] = X[r,k] on pattern rows P_k: every column subset K with |K| >= 3 + has exact rational rank X[intersection of P_k, K] <= 2.""" + + def __init__(self, X): + self.X = X + self.cache = {} + + def rk(self, rows, cols): + key = (rows, tuple(cols)) + v = self.cache.get(key) + if v is None: + rl = mask_list(rows) + v = q_rank([[self.X[r][c] for c in cols] for r in rl]) if len(rl) >= 3 else len(rl) + self.cache[key] = v + return v + + def ok_add(self, cfg, newk): + others = [k for k in cfg if k != newk] + for s in range(2, len(others) + 1): + for sub in itertools.combinations(others, s): + R = cfg[newk] + for k in sub: + R &= cfg[k] + if pc(R) >= 3 and self.rk(R, tuple(sorted(sub + (newk,)))) >= 3: + return False + return True + + def first_violation(self, cfg): + ks = sorted(cfg) + for s in range(3, len(ks) + 1): + for sub in itertools.combinations(ks, s): + R = (1 << NPORT) - 1 + for k in sub: + R &= cfg[k] + if pc(R) >= 3 and self.rk(R, sub) >= 3: + return R, sub + return None + + +def lead_search(g, closed, cap, nc): + """All configurations whose largest closed support V (at lead reader j) + has size >= 36, i.e. dimension >= 2.""" + st = {"geo_max": 0, "real_max": 0, "geo_wit": None} + geo_hist = {} + real_shapes = {} + small = [sorted((W, dw) for W, dw in closed[k].items() if pc(W) <= 36) for k in range(NREAD)] + for j in range(NREAD): + others = [k for k in range(NREAD) if k != j] + for V in sorted(closed[j]): + d = closed[j][V] + s = pc(V) + if s > cap or s < 36: + continue + if s > 36 or cap - 36 < 12: + # Budget < 12 outside V: by the margin-12 premise only cut words + # C_jk fit; U = V u cuts is then a closed support of C_j itself. + gl = d + sum(1 for k in others if g.cut[j][k] & ~V == 0) + geo_hist[gl] = geo_hist.get(gl, 0) + 1 + if gl > st["geo_max"]: + st["geo_max"] = gl + st["geo_wit"] = (j, V) + + def dfs(idx, U, cfg, K): + tot = d + len(K) + st["real_max"] = max(st["real_max"], tot) + if tot >= 5: + shp = "+".join(map(str, sorted([d] + [1] * len(K), reverse=True))) + real_shapes[shp] = real_shapes.get(shp, 0) + 1 + for t in range(idx, len(others)): + k = others[t] + U2 = U | g.cut[j][k] + if pc(U2) > cap: + continue + cfg[k] = g.cut[j][k] + if nc.ok_add(cfg, k): + dfs(t + 1, U2, cfg, K + [k]) + del cfg[k] + + dfs(0, V, {j: V}, []) + else: + # s == 36 with a 12-port budget: enumerate all other supports + cand = {k: [(W, dw) for W, dw in small[k] if pc(W & ~V) <= cap - 36] + for k in others} + + def dfs2(idx, U, cfg, dims, okN): + L = sum(g.kdim(k, U & g.SM[k]) for k in range(NREAD)) + geo_hist[L] = geo_hist.get(L, 0) + 1 + if L > st["geo_max"]: + st["geo_max"] = L + st["geo_wit"] = (j, U) + if okN: + tot = sum(dims) + st["real_max"] = max(st["real_max"], tot) + if tot >= 5: + shp = "+".join(map(str, sorted(dims, reverse=True))) + real_shapes[shp] = real_shapes.get(shp, 0) + 1 + for t in range(idx, len(others)): + k = others[t] + for W, dw in cand[k]: + U2 = U | W + if pc(U2) > cap: + continue + cfg[k] = W + ok2 = okN and nc.ok_add(cfg, k) + dfs2(t + 1, U2, cfg, dims + [dw], ok2) + del cfg[k] + + dfs2(0, V, {j: V}, [d], True) + return st["geo_max"], st["real_max"], geo_hist, real_shapes, st["geo_wit"] + + +def single_word_search(g, cap_hi, caps, nc): + """All configurations of single codewords (closed supports of size <= 32) + from distinct readers with union <= cap.""" + W = [] + R = [] + for j in range(NREAD): + for c in g.codes[j]: + if c and pc(c) <= 32: + W.append(c) + R.append(j) + n = len(W) + compat = [0] * n + for a in range(n): + m = 0 + for b in range(a + 1, n): + if R[b] > R[a] and pc(W[a] | W[b]) <= cap_hi: + m |= 1 << b + compat[a] = m + rmask = [sum(1 << i for i in range(n) if R[i] == j) for j in range(NREAD)] + unions = {cap: {} for cap in caps} + tuples = {cap: {} for cap in caps} + passing = {cap: {} for cap in caps} + wit = {} + + def dfs(U, cand, cfg, okN): + m = len(cfg) + u = pc(U) + rs = tuple(sorted(cfg)) + for cap in caps: + if u <= cap: + unions[cap].setdefault(rs, set()).add(U) + tuples[cap][m] = tuples[cap].get(m, 0) + 1 + if okN: + passing[cap][m] = passing[cap].get(m, 0) + 1 + if m >= 5 and (cap, m) not in wit: + wit[(cap, m)] = dict(cfg) + c = cand + while c: + b = c & -c + i = b.bit_length() - 1 + c ^= b + U2 = U | W[i] + if pc(U2) <= cap_hi: + k = R[i] + cfg[k] = W[i] + ok2 = okN and nc.ok_add(cfg, k) + dfs(U2, cand & compat[i] & ~((1 << (i + 1)) - 1) & ~rmask[k], cfg, ok2) + del cfg[k] + + for a in range(n): + dfs(W[a], compat[a], {R[a]: W[a]}, True) + out = {} + for cap in caps: + ucount = {} + for rs, us in unions[cap].items(): + ucount[len(rs)] = ucount.get(len(rs), 0) + len(us) + out[cap] = { + "distinct_unions_by_reader_subset_size": {str(k): v for k, v in sorted(ucount.items())}, + "word_tuples_by_size": {str(k): v for k, v in sorted(tuples[cap].items())}, + "N_passing_tuples_by_size": {str(k): v for k, v in sorted(passing[cap].items())}, + "geometric_max_readers": max(tuples[cap]), + "N_passing_max": max(passing[cap]), + } + return out, wit + + +def price(m): + r = 1 + while m > 2 ** (r + 1): + r += 1 + return r + + +def price_min(M): + best = None + for m1 in range(1, M + 1): + for m2 in range(m1, M + 1): + if m1 + m2 >= M: + v = price(m1) + price(m2) + best = v if best is None else min(best, v) + return best + + +def realize(g, cols): + """Correction W with W[:,k] = x_k on pattern rows cols[k], zero elsewhere. + Returns retained losses (exact F2 pairing ranks of x_k against + y_k = x_k - w_k), the exact rational rank of W, W and Y.""" + X = g.X + Wm = [[0] * NREAD for _ in range(NPORT)] + for k, P in cols.items(): + for r in mask_list(P): + Wm[r][k] = X[r][k] + Y = [[X[r][c] - Wm[r][c] for c in range(NREAD)] for r in range(NPORT)] + losses = [] + for k in range(NREAD): + ysup = sum(1 << r for r in range(NPORT) if Y[r][k] != 0) + losses.append(8 - g.beta(g.SM[k], ysup)) + return losses, q_rank(Wm), Wm, Y + + +def first_4plus1(g, closed, need=1): + for j in range(NREAD): + for V in sorted(closed[j]): + if closed[j][V] == 4 and pc(V) == 48: + ks = [k for k in range(NREAD) if k != j and g.cut[j][k] & ~V == 0] + if len(ks) >= need: + return (j, V) + tuple(ks[:need]) + return None + + +def check_witness(g, j, V, k): + X = g.X + losses, rW, Wm, Y = realize(g, {j: V, k: g.cut[j][k]}) + Z = [[Wm[r][j], Wm[r][k]] for r in range(NPORT)] + A = [[0, 0] for _ in range(NREAD)] + A[j] = [1, 0] + A[k] = [0, 1] + require(q_rank(Z) == 2 and q_rank(A) == 2, "full-rank factors") + U = sum(1 << r for r in range(NPORT) if Z[r][0] != 0 or Z[r][1] != 0) + XA = [[sum(X[r][c] * A[c][h] for c in range(NREAD)) for h in range(2)] for r in range(NPORT)] + for a in range(NPORT): + for b in range(NPORT): + lhs = sum(X[a][c] * X[b][c] for c in range(NREAD)) + rhs = (sum(X[a][c] * Y[b][c] for c in range(NREAD)) + + sum(XA[a][h] * Z[b][h] for h in range(2))) + require(lhs == rhs, "decoder identity") + added = [] + for h in range(2): + dsup = sum(1 << r for r in range(NPORT) if XA[r][h] != 0) + zsup = sum(1 << r for r in range(NPORT) if Z[r][h] != 0) + added.append(g.beta(dsup, zsup)) + retained = [8 - l for l in losses] + return { + "reader_j": j, + "reader_k": k, + "U_ports": mask_list(U), + "U_size": pc(U), + "kernel_dim_at_j_via_code": g.kdim(j, V), + "z_support_sizes": [pc(V), pc(g.cut[j][k])], + "rank_Z": 2, + "rank_A": 2, + "rank_W": rW, + "retained_losses": losses, + "retained_copy_ranks": retained, + "retained_sum": sum(retained), + "added_copy_ranks": added, + "total_copy_bill": sum(retained) + sum(added), + "rank_X_Z": q_rank([X[r] + Z[r] for r in range(NPORT)]), + "identity_pairs_checked": NPORT * NPORT, + } + + +def run(raw_geom): + g = Geometry(load_geometry(raw_geom)) + res = {"geometry": {"path": GEOM_REL, "sha256": GEOM_SHA}} + res["premises"] = premises(g) + closed = closed_supports(g, 48) + census = [] + for j in range(NREAD): + c = {} + for V, d in closed[j].items(): + key = "dim%d_size%d" % (d, pc(V)) + c[key] = c.get(key, 0) + 1 + census.append(c) + require(all(c == census[0] for c in census), "closed census differs by reader") + res["closed_support_census_each_reader_cap48"] = dict(sorted(census[0].items())) + nc = NCheck(g.X) + bands = {} + sw, swwit = single_word_search(g, 48, (47, 48), nc) + for cap in (47, 48): + gm, rm, gh, rs, gw = lead_search(g, closed, cap, nc) + bands[str(cap)] = { + "lead_dim_ge2": { + "geometric_max": gm, + "N_passing_max": rm, + "geometric_value_histogram": {str(k): v for k, v in sorted(gh.items())}, + "N_passing_config_shapes_total_ge5": dict(sorted(rs.items())), + }, + "single_words": sw[cap], + "geometric_max_L": max(gm, sw[cap]["geometric_max_readers"]), + "two_column_retained_loss_upper_bound": max(rm, sw[cap]["N_passing_max"]), + "price_min": price_min(cap), + } + if cap == 48: + j, U = gw + vec = [g.kdim(k, U & g.SM[k]) for k in range(NREAD)] + vec2 = [8 - g.beta(g.SM[k], g.SM[k] & ~U) for k in range(NREAD)] + require(vec == vec2, "two loss engines disagree") + require(sum(vec) == bands["48"]["geometric_max_L"], "geometric witness") + cfgV = {} + for k in range(NREAD): + if vec[k] > 0: + acc = 0 + for c in g.codes[k]: + if c & ~U == 0: + acc |= c + cfgV[k] = acc + viol = nc.first_violation(cfgV) + require(viol is not None, "geometric maximum configuration should violate N") + R, sub = viol + bands["48"]["geometric_witness"] = { + "lead_reader": j, "U_ports": mask_list(U), "U_size": pc(U), + "loss_vector": vec, + "N_violation": {"rows": mask_list(R), "cols": list(sub), "rank": nc.rk(R, sub)}} + if (48, 5) in swwit: + bands["48"]["single_word_five_tuple_passing_N_example"] = { + str(k): mask_list(v) for k, v in sorted(swwit[(48, 5)].items())} + res["bands"] = bands + res["price_min_by_M"] = {str(M): price_min(M) for M in range(44, 49)} + w = first_4plus1(g, closed, 1) + require(w is not None, "no 4+1 witness") + wit = check_witness(g, *w) + require(sum(wit["retained_losses"]) == 5 and wit["rank_W"] == 2 and wit["U_size"] == 48, + "two-column witness does not attain loss 5 at 48") + res["two_column_loss5_witness"] = wit + f48 = 64 - bands["48"]["two_column_retained_loss_upper_bound"] + price_min(48) + f47 = 64 - bands["47"]["two_column_retained_loss_upper_bound"] + price_min(47) + res["floors"] = { + "full_rank_two_total_copy_floor_cap47": f47, + "full_rank_two_total_copy_floor_at_48": f48, + "relaxation_floor_attained_by_loss_bound_at_48": ( + sum(wit["retained_losses"]) == bands["48"]["two_column_retained_loss_upper_bound"]), + } + # ---- negative controls (each must be rejected) ---- + ncs = {} + bad = bytearray(raw_geom) + pos = bad.index(b'"X"') + 10 + bad[pos:pos + 1] = b"7" if bad[pos:pos + 1] != b"7" else b"8" + try: + load_geometry(bytes(bad)) + ncs["corrupted_geometry_pin"] = "ACCEPTED" + except CheckFailure: + ncs["corrupted_geometry_pin"] = "rejected" + viol = bands["48"]["geometric_witness"]["N_violation"] + M = [[g.X[r][c] for c in viol["cols"]] for r in viol["rows"]] + Mp = [row[:2] + [row[0] + row[1]] + row[3:] for row in M] + ncs["perturbed_minor"] = {"original_rank": q_rank(M), "perturbed_rank": q_rank(Mp), + "status": "rejected" if q_rank(M) >= 3 and q_rank(Mp) <= 2 else "ACCEPTED"} + fake = first_4plus1(g, closed, 2) + require(fake is not None, "no fake profile") + j, V, k, l = fake + losses, rW, _, _ = realize(g, {j: V, k: g.cut[j][k], l: g.cut[j][l]}) + bound = bands["48"]["two_column_retained_loss_upper_bound"] + ncs["three_column_fake_profile"] = { + "readers": [j, k, l], "retained_loss": sum(losses), "rank_W": rW, + "status": "rejected" if (rW >= 3 and sum(losses) > bound) else "ACCEPTED"} + res["negative_controls"] = ncs + return res + + +def receipt_matches(rec, res): + return rec == res + + +def main(argv): + if len(argv) >= 2 and argv[0] == "--write": + require(not os.path.exists(argv[1]), "refusing to overwrite") + raw = open(os.path.join(ROOT, GEOM_REL), "rb").read() + res = json.loads(json.dumps(run(raw), sort_keys=True)) + ncs = res["negative_controls"] + require(ncs["corrupted_geometry_pin"] == "rejected", "NC1 corrupted pin accepted") + require(ncs["perturbed_minor"]["status"] == "rejected", "NC2 perturbed minor accepted") + require(ncs["three_column_fake_profile"]["status"] == "rejected", "NC3 fake profile accepted") + if len(argv) >= 2 and argv[0] == "--write": + with open(argv[1], "w") as f: + json.dump(res, f, indent=1, sort_keys=True) + f.write("\n") + print("WROTE", argv[1]) + return + rec = json.load(open(os.path.join(HERE, "RESULT.json"))) + require(receipt_matches(rec, res), "RESULT.json mismatch") + # NC4: the same comparison function must reject a receipt whose floor is altered. + bad = json.loads(json.dumps(rec)) + bad["floors"]["full_rank_two_total_copy_floor_at_48"] += 1 + require(not receipt_matches(bad, res), "NC4 corrupted receipt accepted") + b = res["bands"] + print("PASS_P112_TWO_TOTAL_UNION48 geometric_max_47=%d geometric_max_48=%d " + "two_column_loss_bound_47=%d two_column_loss_bound_48=%d loss5_witness_bill=%d " + "full_rank_copy_floor_48=%d no_new_kappa" % ( + b["47"]["geometric_max_L"], b["48"]["geometric_max_L"], + b["47"]["two_column_retained_loss_upper_bound"], + b["48"]["two_column_retained_loss_upper_bound"], + res["two_column_loss5_witness"]["total_copy_bill"], + res["floors"]["full_rank_two_total_copy_floor_at_48"])) + + +if __name__ == "__main__": + try: + main(sys.argv[1:]) + except CheckFailure as e: + print("FAIL", e) + sys.exit(1)