Negative result: P112 fixed-reader two-total COPY at source union 48 — two-column loss bound exactly 5 (attained), full-rank lower bound 65, COPY >= 64 extends (PR2382 OQ1)

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.

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.