From 2b821b14a7cd5888df95531c98d18ee3797e36c3 Mon Sep 17 00:00:00 2001 From: Josie Elliston Date: Wed, 14 Oct 2026 05:57:08 -0400 Subject: [PATCH] =?UTF-8?q?Research:=20P112=20coordinate=20support=20weigh?= =?UTF-8?q?ts=20and=20a=20two-total=20COPY=20floor=20through=20source=20un?= =?UTF-8?q?ion=2043=20(no=20new=20=CE=BA)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Exact generalized support weights (24,36,44,48,52,54,55,56) of the eight P112 coordinate evaluation codes, cross-reader cut thresholds, and an added-term charge that together with #1197's reductions give COPY >= 64 for every exact two-total decoder retaining the coordinate readers with source union at most 43. Prepared by OpenAI Codex (offline session 17); reviewed, corrected and published by Claude (session 19). Co-Authored-By: Claude Opus 5.5 --- .../p112-two-total-support-threshold/PROOF.md | 202 + .../README.md | 111 + .../RESULT.json | 4906 +++++++++++++++++ .../SOURCES.json | 36 + .../TASK.json | 72 + .../VERIFY.json | 23 + .../verify.py | 478 ++ 7 files changed, 5828 insertions(+) create mode 100644 research/p112-two-total-support-threshold/PROOF.md create mode 100644 research/p112-two-total-support-threshold/README.md create mode 100644 research/p112-two-total-support-threshold/RESULT.json create mode 100644 research/p112-two-total-support-threshold/SOURCES.json create mode 100644 research/p112-two-total-support-threshold/TASK.json create mode 100644 research/p112-two-total-support-threshold/VERIFY.json create mode 100644 research/p112-two-total-support-threshold/verify.py diff --git a/research/p112-two-total-support-threshold/PROOF.md b/research/p112-two-total-support-threshold/PROOF.md new file mode 100644 index 0000000000..0adcdee227 --- /dev/null +++ b/research/p112-two-total-support-threshold/PROOF.md @@ -0,0 +1,202 @@ +# Exact support thresholds for the fixed P112 coordinate readers + +## Contract and statement + +Use the P112 coordinate matrix `X` and binary labels/duals from +`research/p112-single-lift/reference-geometry.json`. Write `x_j` for its +eight columns, `S_j = supp(x_j)`, and + + beta(d,s) = rank_F2 (v_i dot l_t)_(i in supp(d), t in supp(s)). + +The pinned geometry has `|S_j|=56` and `beta(x_j,x_j)=8`. For any set of +ports `T`, let `b_j(T)=beta(x_j, 1_(S_j\T) x_j)`: only the source columns in +`S_j\T` are retained. Then the exact thresholds for `b_j(T) <= 8-d`, +`d=1,...,8`, are, **for every** `j`, respectively + + w_d = (24,36,44,48,52,54,55,56). + +In particular, deleting at most 23 sites from a coordinate source cannot +lower its COPY rank. At 24 sites, all 63 first-drop sets for each reader +are enumerated. Across the eight readers there are 476 distinct sets: +448 belong to one reader, and 28 belong to two, exactly one common set for +each pair of readers. None belongs to three. The smallest port set which can +lower three coordinate ranks simultaneously has size 40. The three-reader +statement is about a *freely chosen deletion set*, not the attainable cost +of a two-total factorization. + +For the exact ten-term identity considered by Philipp / @mightyOil, + + XX^T = XT^T + DZ^T, D=XA, T=X-ZA^T, + +let `T_source = supp(z_1) union supp(z_2)`. Any retained source `t_j` +agrees with `x_j` outside `T_source`; it may also have additional nonzero +positions. Adding source columns cannot decrease binary rank, so + + beta(x_j,t_j) >= b_j(T_source). + +Consequently `|T_source| <= 23` forces all eight retained costs to remain +eight, and the two added costs are nonnegative. The complete separate-total +COPY sum is at least 64, for **arbitrary complex coefficients**, without +assuming independence or a particular coefficient support. The added-term +argument below extends this no-saving range to `|T_source| <= 43`, using +the predecessor's rank-one/off-column theorem. More generally, +`|T_source| < w_d` prevents a rank drop of `d` in any retained term. If +`|T_source| < 40`, fewer than three retained terms can drop at all. These +are necessary support restrictions; no floor is claimed beyond the +`|T_source|<=43` corollary. + +## Why the finite enumeration proves the thresholds + +For fixed `j`, put `V_j = span_F2{v_i : i in S_j}`. The source-bound +geometry gives `dim V_j=8`. Define the linear evaluation map + + E_j : V_j -> F2^(S_j), q -> (q dot l_t)_(t in S_j). + +Its image `C_j` has dimension eight, since `beta(x_j,x_j)=8`. For deleted +ports `T`, the nullity of evaluation on `S_j\T` is `8-b_j(T)`. +Thus `b_j(T)<=8-d` exactly when a `d`-dimensional subspace `U` of `C_j` +has its coordinate support contained in `T`. The minimum possible size +of `T` is the `d`-th generalized support weight of `C_j`. + +`verify.py` constructs eight independent evaluation words from the actual +duals and labels, then enumerates every subspace of `F2^8` once by its +unique reduced row echelon basis. For each pivot set it allows exactly the +entries right of a pivot and outside all pivot columns to vary. The number +of enumerated spaces by dimension is + + 255, 10795, 97155, 200787, 97155, 10795, 255, 1. + +The support of a subspace is the bitwise union of its basis words, because +all combinations vanish at a coordinate exactly when all basis words do. +The minimum over all spaces gives `w_d`. The verifier checks these counts, +all eight weight sequences, each explicit minimizing witness, and that +removing any single port from such a witness restores at least one rank +unit using a **direct restricted-pairing rank** calculation. It also +reconstructs the geometry from the pinned root generator and checks every +Gram and binary pairing entry; no floating-point or finite-field proxy for +complex matrix rank is used. + +Each `C_j` has one zero word and nonzero weight distribution +`24^63, 28^128, 32^63, 56^1`. For the cross-reader statement, the +verifier maps all 63 weight-24 words for each reader back to the common +112-port index set and compares them exactly. To exclude a triple below +40, it considers all 254 nonzero words of weight below 40 for each reader. +For every reader triple, it forms all pair unions of size below 40 and +checks that none can be enlarged by a third word while staying below 40. +An explicit union of three weight-24 words has size 40, and direct +restricted-pairing ranks confirm all three drops. This does not assume the +three deletions can be produced by two source columns. + +## Added-total charge and the 43-port floor + +The preceding argument controls only retained terms. To price added terms +in the predecessor's remaining full-rank case, `verify.py` also replays an +exact 511-functional census independently of the predecessor checker. For +each nonzero nine-bit `q`, it computes the rational rank of `X[I_q,:]`, +where `I_q={i:q dot v_i=1}`. Exactly 503 matrices have rank eight. The +other eight have rank seven, with one coordinate-axis kernel each. None +of the 112 distinct live source labels equals an exceptional `q`. + +Let `d=Xa` be a nonzero added reader with arbitrary complex coefficients. +If the span of its active dual labels had dimension below eight, two +independent binary functionals `q_1,q_2` would annihilate every active +dual, and so would `q_1+q_2`. Each of these three nonzero `q` places +`a` in the kernel of `X[I_q,:]`. A full-rank `X[I_q,:]` forces `a=0`; +otherwise all three are exceptional, and the census shows the eight +exceptional kernels are distinct coordinate axes, so again `a=0`. +Thus its dual span has dimension at least eight. Further, +every live source label is visible to `d`: an invisible label would be +an exceptional `q`, but no source label is exceptional. Rational and +complex ranks agree for these integer matrices, so complex cancellation +does not invalidate the argument. + +For a nonzero source `z` with `m` distinct live support sites, let +`r=beta(d,z)`. Evaluation on the reader's dual span has a kernel of +dimension at most one in the nine-bit label space. The `m` distinct source +labels all lie in the preimage of an `r`-dimensional image space, which +contains at most `2^(r+1)` labels. The visibility fact also gives `r>=1`. +Therefore + + beta(d,z) >= min {r>=1 : m <= 2^(r+1)}. (A) + +This is the rank-nullity support bound of Hanson Sun / @bbMisk's PR1432 +(there sharpened to `m <= 2^(r+1)-1` because labels are nonzero), applied +to an arbitrary nonzero on-column reader. The 511-functional census is +Mihir Srivastava's #845 premise (503 full-rank functionals, eight +coordinate kernels), recomputed independently here. The weaker form (A) +already suffices through union 43. + +Now assume the exact two-total factorization has both `A` and `Z` of +complex rank two. Both added reader and source columns are nonzero. If +their source support sizes are `m_1,m_2`, their union `M` satisfies +`m_1+m_2>=M`. The verifier minimizes the sum of (A) over all positive +`m_1,m_2<=M` with this constraint, for every `M=1,...,43`. For `M<24` +the retained rank loss is zero. For `24<=M<36`, each reader loses at most +one rank unit and fewer than three readers can drop, so total loss is at +most two; the added bill is at least five. For `36<=M<40`, each reader +loses at most two units and still fewer than three readers can drop, so +total loss is at most four; the added bill is at least five. + +For `40<=M<44`, each reader loses at most two rank units, since its third +generalized weight is 44. The complete cross-reader cut census shows at +most four readers can drop: every union of four nonzero cut words below 44 +is one of exactly 42 sets of size 40, and every fifth reader's cut needs at +least four further ports. Also, the original coordinate supports meet +pairwise in exactly 24 ports. Two readers each losing two rank units would +need a union of at least `36+36-24=48` ports, so at most one of the four +can lose two. Total retained loss is at most five, while the added bill is +at least six. The full-rank case therefore has COPY sum **strictly above +64** throughout `M<=43`. + +Philipp / @mightyOil's predecessor theorem already proves COPY sum at +least 64 if either added matrix has rank at most one, either reader leaves +`col_C(X)`, or the coordinate coefficient supports are disjoint. Combining +that result with this full-rank on-column screen proves the no-saving +corollary for **every exact two-total factorization retaining the eight +coordinate readers with source union at most 43**, regardless of complex +coefficients. The new part is the bounded-support argument; the theorem +does not independently re-prove the predecessor's complementary cases. + +## Sharp two-total rank-drop fixture + +For readers 0 and 1, the common 24-port minimum cut is ports `0..23`. +Let `C` be that set and let `x_0|C`, `x_1|C` be the two coordinate vectors +restricted to it. Set + + a_0 = (1,1), a_1 = (1,-1), a_j=(0,0) for j>=2, + z_1 = (x_0|C + x_1|C)/2, + z_2 = (x_0|C - x_1|C)/2. + +The two `A` columns overlap on both coordinates and have complex rank two. +The sources are nonzero on disjoint twelve-port halves, so `Z` also has +rank two. `D=XA` and `T=X-ZA^T` make the complete 112-by-112 identity exact. +The retained COPY ranks are `(7,7,8,8,8,8,8,8)`; both added terms cost +seven, for **total 76**. Removing port 0 from both sources restores all +retained costs to eight (total 78). The verifier checks every matrix entry +and all ten restricted pairing ranks. This proves the 24-site rank-drop +threshold is attained *inside* the predecessor's remaining rank-two, +overlapping-coefficient case; it is not a cheaper decoder. + +## Limits and predecessor credit + +This result does not bound arbitrary large source unions, certify a +ten-term COPY optimum, or price frames, preparation, restoration, hosting, +recursive children or an all-size supplier. `beta` is the inherited +separate-total pairing-rank charge under DreamingOfClouds' PR446/PR717 +model. A different delivery architecture could have a different bill. + +Philipp / @mightyOil established the predecessor rank-one, off-column and +disjoint-coordinate-support reductions. The single-lift floor is due to +Mihir Srivastava (#845) and its complex extension to @woklerx (#998). +The P112 coordinate geometry and cost descend from DreamingOfClouds and +Joel Pulikkan / GamingPuzzled, with earlier E8 work cited by those packages. +The first weight `w_1=24` is @commdata2338's PR1375 erasure distance of +a coordinate support (`research/p112-two-coordinate-small-rectangle/`). +This note adds the higher weights `w_2..w_8`, the cross-reader cut +thresholds, and their combination with the added-term charge in the +predecessor's remaining two-total case. PR669 (the-missionary-company) +computes generalized weights of signed proper-star codes, a different +code. Prepared for Josie Elliston by OpenAI Codex (offline session 17); +reviewed, corrected and published by Claude (Anthropic, session 19). +Substantial AI assistance. Apache-2.0; no independent human review or +full multiplication theorem. diff --git a/research/p112-two-total-support-threshold/README.md b/research/p112-two-total-support-threshold/README.md new file mode 100644 index 0000000000..11fade8743 --- /dev/null +++ b/research/p112-two-total-support-threshold/README.md @@ -0,0 +1,111 @@ +# P112 two-total source-support thresholds + +**Scoped exact support obstruction; no cheaper decoder or new κ.** With the +eight P112 coordinate readers retained, two added totals cannot lower the +separate-total COPY rank below 64 if the union of their source supports has +at most **43 of the 112 ports**. This holds for arbitrary complex +coefficients and even when both added factor matrices have rank two with +overlapping coordinate supports. The open unrestricted two-total case +remains open. + +The exact source-deletion thresholds for one retained reader to lose +`d=1,...,8` rank units are + +| Rank units lost | 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | +|---|---:|---:|---:|---:|---:|---:|---:|---:| +| Minimum deleted source ports | 24 | 36 | 44 | 48 | 52 | 54 | 55 | 56 | + +Every coordinate has this same sequence. The first entry, 24, is the +erasure distance of a coordinate support found by @commdata2338's PR1375 +(`research/p112-two-coordinate-small-rectangle/`); the higher entries +36..56 and the cross-reader statements are new here. Each of the 28 reader pairs +shares exactly one first-drop set of size 24; no such set hits three +readers. A freely chosen deletion set requires at least 40 ports to lower +three coordinate ranks. These are exact finite code properties, not +physical source costs. At union size below 44, at most four readers can +drop, and at most one can lose two rank units. The verifier finds exactly +42 four-reader cuts of size 40 and excludes a fifth reader with fewer +than four more ports. + +The 43-port floor also charges both added totals. An exact +511-functional census (re-implemented here; the 503/8 split is Mihir +Srivastava's #845 premise, also rechecked by @adamgall's +`research/p112-gram-support-seed80/`) shows every nonzero added reader in +`col_C(X)` has binary dual span at least eight and sees every live source +label. If an added source has `m` nonzero sites, its COPY rank is at least +the smallest `r>=1` satisfying `m<=2^(r+1)`. This support-from-rank step +is the same rank-nullity argument as Hanson Sun / @bbMisk's PR1432 +(`research/p112-two-product-compensation/`, "compensation rank controls +support size"), applied here to every on-column added reader. Through source union 43, this lower bill +strictly exceeds every possible retained-rank loss in the full-rank +on-column case. The predecessor covers rank-one and off-column cases; +this package uses that result rather than re-proving it. + +The 24 threshold is sharp even with two full-rank added matrices and +overlapping coordinate coefficient supports: an explicit exact ten-term +fixture drops the retained ranks from `(8,8)` to `(7,7)`. Its added terms +cost 14, so its total COPY rank is **76**, versus the baseline 64. +Removing one source port restores both retained ranks to eight. See +[PROOF.md](PROOF.md) for the quantified reduction, enumeration proof, +fixture and limitations. + +## Reproduce + +From the repository root, Python 3.10 or later, standard library only: + +```sh +python3.12 -I -B research/p112-two-total-support-threshold/verify.py +python3.12 scripts/research_package.py --package research/p112-two-total-support-threshold --check-only +python3.12 scripts/research_package.py --package research/p112-two-total-support-threshold +``` + +The verifier is read-only by default, compares every field with +`RESULT.json`, and remains active under `-O`. It pins the predecessor's +P112 geometry and exact root generator by SHA-256 and Git blob, rebuilds +the geometry, checks all 112² Gram/pairing entries, enumerates every +subspace of all eight 8-dimensional evaluation codes, replays the 511 +exact rational-rank premises for the added-term bound, and recomputes the +cross-reader cuts and complete 112² fixture identity. Direct-rank witness +checks, all one-port-short controls, source drift and geometry consistency +checks are part of the same command. The final marker is +`PASS_P112_TWO_TOTAL_SUPPORT_THRESHOLD`. + +To regenerate a receipt for comparison without replacing the submitted +one, run `verify.py --write /new/path.json`; the path must not exist. +`SOURCES.json` binds the exact base `a18b4b01`, predecessor proof and +geometry. `TASK.json` declares the scope change from the rank-shape card: +this package supplies a search-pruning algebraic side result, not the +card's physically priced 5% construction target. The selected #1094 +record, predecessor packages, `upstream/` and frozen evidence are unchanged. + +## Open next questions + +1. **Can the remaining full-rank, overlapping two-total case beat COPY 64?** + A physical decoder gain needs the total bill, including both added + terms. Start a source-support-aware exact search at union support 44 + or higher, using the 24/36/40 thresholds and preserving the non-free + choice of two-total basis. + The present lower bound on added-term COPY ranks is insufficient to + settle larger source unions. +2. **Do larger cross-reader erosion thresholds guide a paid design?** + Search unions of minimal evaluation-code supports for four or more + readers, then impose actual two-source coefficient constraints and + charge preparation, frames and restoration. An arbitrary union need + not be realizable by two complex source columns. + +Credit: Philipp / @mightyOil's predecessor two-total reductions (#1197), +Mihir Srivastava's #845 single-lift floor and 511-functional census, +@woklerx's #998 complex extension, @commdata2338's PR1375 erasure +distance 24, Hanson Sun / @bbMisk's PR1432 support-from-rank lemma, +@adamgall's seed-80 census recheck, DreamingOfClouds' E8 decoder model +and Joel Pulikkan / GamingPuzzled's coordinate COPY-64 lineage. +Adjacent but distinct: @just-mn's PR1689 bounds masked Walsh totals +that leave `col(X)`, and PR1633 (Hanson Sun) classifies overcomplete +ten-term residual forms without a COPY floor. PR669 +(the-missionary-company) computes generalized weights of signed +proper-star codes, a different code from these coordinate evaluation +codes. Prepared for Josie Elliston by OpenAI Codex (offline session 17 +of an overnight donated run: mathematics, verifier, controls and +writing), then reviewed, corrected and published by Claude (Anthropic; +session 19). Substantial AI assistance; Apache-2.0; no independent +human review or full multiplication theorem is claimed. diff --git a/research/p112-two-total-support-threshold/RESULT.json b/research/p112-two-total-support-threshold/RESULT.json new file mode 100644 index 0000000000..53543243ac --- /dev/null +++ b/research/p112-two-total-support-threshold/RESULT.json @@ -0,0 +1,4906 @@ +{ + "added_reader_span_census": { + "distinct_live_labels": 112, + "exceptions": [ + { + "functional": 5, + "zero_coordinate": 5 + }, + { + "functional": 17, + "zero_coordinate": 3 + }, + { + "functional": 65, + "zero_coordinate": 1 + }, + { + "functional": 85, + "zero_coordinate": 7 + }, + { + "functional": 129, + "zero_coordinate": 0 + }, + { + "functional": 149, + "zero_coordinate": 6 + }, + { + "functional": 197, + "zero_coordinate": 4 + }, + { + "functional": 209, + "zero_coordinate": 2 + } + ], + "rank_counts": { + "7": 8, + "8": 503 + } + }, + "base_commit": "a18b4b0136d647529971e9fcb99fa83f5b9a0b81", + "cross_reader_cuts": { + "common_minimum_cuts": { + "0,1": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 8, + 9, + 10, + 11, + 12, + 13, + 14, + 15, + 16, + 17, + 18, + 19, + 20, + 21, + 22, + 23 + ], + "0,2": [ + 0, + 1, + 2, + 3, + 12, + 13, + 14, + 15, + 48, + 49, + 50, + 51, + 52, + 53, + 54, + 55, + 72, + 73, + 74, + 75, + 76, + 77, + 78, + 79 + ], + "0,3": [ + 0, + 1, + 2, + 3, + 12, + 13, + 14, + 15, + 56, + 57, + 58, + 59, + 60, + 61, + 62, + 63, + 64, + 65, + 66, + 67, + 68, + 69, + 70, + 71 + ], + "0,4": [ + 4, + 5, + 6, + 7, + 16, + 17, + 18, + 19, + 48, + 49, + 54, + 55, + 56, + 57, + 62, + 63, + 64, + 65, + 70, + 71, + 72, + 73, + 78, + 79 + ], + "0,5": [ + 4, + 5, + 6, + 7, + 16, + 17, + 18, + 19, + 50, + 51, + 52, + 53, + 58, + 59, + 60, + 61, + 66, + 67, + 68, + 69, + 74, + 75, + 76, + 77 + ], + "0,6": [ + 8, + 9, + 10, + 11, + 20, + 21, + 22, + 23, + 48, + 49, + 54, + 55, + 58, + 59, + 60, + 61, + 66, + 67, + 68, + 69, + 72, + 73, + 78, + 79 + ], + "0,7": [ + 8, + 9, + 10, + 11, + 20, + 21, + 22, + 23, + 50, + 51, + 52, + 53, + 56, + 57, + 62, + 63, + 64, + 65, + 70, + 71, + 74, + 75, + 76, + 77 + ], + "1,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 + ], + "1,3": [ + 0, + 1, + 2, + 3, + 12, + 13, + 14, + 15, + 88, + 89, + 90, + 91, + 92, + 93, + 94, + 95, + 96, + 97, + 98, + 99, + 100, + 101, + 102, + 103 + ], + "1,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 + ], + "1,5": [ + 4, + 5, + 6, + 7, + 16, + 17, + 18, + 19, + 82, + 83, + 84, + 85, + 90, + 91, + 92, + 93, + 98, + 99, + 100, + 101, + 106, + 107, + 108, + 109 + ], + "1,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 + ], + "1,7": [ + 8, + 9, + 10, + 11, + 20, + 21, + 22, + 23, + 80, + 81, + 86, + 87, + 90, + 91, + 92, + 93, + 98, + 99, + 100, + 101, + 104, + 105, + 110, + 111 + ], + "2,3": [ + 0, + 1, + 2, + 3, + 12, + 13, + 14, + 15, + 24, + 25, + 26, + 27, + 28, + 29, + 30, + 31, + 32, + 33, + 34, + 35, + 36, + 37, + 38, + 39 + ], + "2,4": [ + 24, + 25, + 26, + 27, + 32, + 33, + 34, + 35, + 48, + 49, + 54, + 55, + 72, + 73, + 78, + 79, + 80, + 81, + 86, + 87, + 104, + 105, + 110, + 111 + ], + "2,5": [ + 24, + 25, + 26, + 27, + 32, + 33, + 34, + 35, + 50, + 51, + 52, + 53, + 74, + 75, + 76, + 77, + 82, + 83, + 84, + 85, + 106, + 107, + 108, + 109 + ], + "2,6": [ + 28, + 29, + 30, + 31, + 36, + 37, + 38, + 39, + 48, + 49, + 54, + 55, + 72, + 73, + 78, + 79, + 82, + 83, + 84, + 85, + 106, + 107, + 108, + 109 + ], + "2,7": [ + 28, + 29, + 30, + 31, + 36, + 37, + 38, + 39, + 50, + 51, + 52, + 53, + 74, + 75, + 76, + 77, + 80, + 81, + 86, + 87, + 104, + 105, + 110, + 111 + ], + "3,4": [ + 24, + 25, + 26, + 27, + 32, + 33, + 34, + 35, + 56, + 57, + 62, + 63, + 64, + 65, + 70, + 71, + 88, + 89, + 94, + 95, + 96, + 97, + 102, + 103 + ], + "3,5": [ + 24, + 25, + 26, + 27, + 32, + 33, + 34, + 35, + 58, + 59, + 60, + 61, + 66, + 67, + 68, + 69, + 90, + 91, + 92, + 93, + 98, + 99, + 100, + 101 + ], + "3,6": [ + 28, + 29, + 30, + 31, + 36, + 37, + 38, + 39, + 58, + 59, + 60, + 61, + 66, + 67, + 68, + 69, + 88, + 89, + 94, + 95, + 96, + 97, + 102, + 103 + ], + "3,7": [ + 28, + 29, + 30, + 31, + 36, + 37, + 38, + 39, + 56, + 57, + 62, + 63, + 64, + 65, + 70, + 71, + 90, + 91, + 92, + 93, + 98, + 99, + 100, + 101 + ], + "4,5": [ + 4, + 5, + 6, + 7, + 16, + 17, + 18, + 19, + 24, + 25, + 26, + 27, + 32, + 33, + 34, + 35, + 40, + 41, + 42, + 43, + 44, + 45, + 46, + 47 + ], + "4,6": [ + 40, + 41, + 42, + 43, + 44, + 45, + 46, + 47, + 48, + 49, + 54, + 55, + 72, + 73, + 78, + 79, + 88, + 89, + 94, + 95, + 96, + 97, + 102, + 103 + ], + "4,7": [ + 40, + 41, + 42, + 43, + 44, + 45, + 46, + 47, + 56, + 57, + 62, + 63, + 64, + 65, + 70, + 71, + 80, + 81, + 86, + 87, + 104, + 105, + 110, + 111 + ], + "5,6": [ + 40, + 41, + 42, + 43, + 44, + 45, + 46, + 47, + 58, + 59, + 60, + 61, + 66, + 67, + 68, + 69, + 82, + 83, + 84, + 85, + 106, + 107, + 108, + 109 + ], + "5,7": [ + 40, + 41, + 42, + 43, + 44, + 45, + 46, + 47, + 50, + 51, + 52, + 53, + 74, + 75, + 76, + 77, + 90, + 91, + 92, + 93, + 98, + 99, + 100, + 101 + ], + "6,7": [ + 8, + 9, + 10, + 11, + 20, + 21, + 22, + 23, + 28, + 29, + 30, + 31, + 36, + 37, + 38, + 39, + 40, + 41, + 42, + 43, + 44, + 45, + 46, + 47 + ] + }, + "four_reader_cut_sizes": [ + 40 + ], + "four_reader_cuts_below_44": 42, + "minimum_cut_multiplicity": { + "1": 448, + "2": 28 + }, + "reader_support_pair_intersection": 24, + "triple_minimum_union": 40, + "triple_witness_ports": [ + 0, + 1, + 2, + 3, + 12, + 13, + 14, + 15, + 56, + 57, + 58, + 59, + 60, + 61, + 62, + 63, + 64, + 65, + 66, + 67, + 68, + 69, + 70, + 71, + 80, + 81, + 82, + 83, + 84, + 85, + 86, + 87, + 104, + 105, + 106, + 107, + 108, + 109, + 110, + 111 + ] + }, + "generalized_weights": { + "minimizer_counts": [ + [ + 63, + 336, + 1260, + 315, + 2898, + 1540, + 56, + 1 + ], + [ + 63, + 336, + 1260, + 315, + 2898, + 1540, + 56, + 1 + ], + [ + 63, + 336, + 1260, + 315, + 2898, + 1540, + 56, + 1 + ], + [ + 63, + 336, + 1260, + 315, + 2898, + 1540, + 56, + 1 + ], + [ + 63, + 336, + 1260, + 315, + 2898, + 1540, + 56, + 1 + ], + [ + 63, + 336, + 1260, + 315, + 2898, + 1540, + 56, + 1 + ], + [ + 63, + 336, + 1260, + 315, + 2898, + 1540, + 56, + 1 + ], + [ + 63, + 336, + 1260, + 315, + 2898, + 1540, + 56, + 1 + ] + ], + "subspace_counts": [ + 255, + 10795, + 97155, + 200787, + 97155, + 10795, + 255, + 1 + ], + "weights": [ + [ + 24, + 36, + 44, + 48, + 52, + 54, + 55, + 56 + ], + [ + 24, + 36, + 44, + 48, + 52, + 54, + 55, + 56 + ], + [ + 24, + 36, + 44, + 48, + 52, + 54, + 55, + 56 + ], + [ + 24, + 36, + 44, + 48, + 52, + 54, + 55, + 56 + ], + [ + 24, + 36, + 44, + 48, + 52, + 54, + 55, + 56 + ], + [ + 24, + 36, + 44, + 48, + 52, + 54, + 55, + 56 + ], + [ + 24, + 36, + 44, + 48, + 52, + 54, + 55, + 56 + ], + [ + 24, + 36, + 44, + 48, + 52, + 54, + 55, + 56 + ] + ], + "witnesses": [ + [ + { + "deleted_ports": [ + 0, + 1, + 2, + 3, + 12, + 13, + 14, + 15, + 56, + 57, + 58, + 59, + 60, + 61, + 62, + 63, + 64, + 65, + 66, + 67, + 68, + 69, + 70, + 71 + ], + "rref_rows": [ + 5 + ] + }, + { + "deleted_ports": [ + 0, + 1, + 2, + 3, + 4, + 5, + 12, + 13, + 14, + 15, + 16, + 17, + 48, + 49, + 50, + 51, + 56, + 57, + 58, + 59, + 60, + 61, + 62, + 63, + 64, + 65, + 66, + 67, + 68, + 69, + 70, + 71, + 76, + 77, + 78, + 79 + ], + "rref_rows": [ + 5, + 10 + ] + }, + { + "deleted_ports": [ + 0, + 1, + 2, + 3, + 4, + 5, + 12, + 13, + 14, + 15, + 16, + 17, + 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 + ], + "rref_rows": [ + 9, + 10, + 12 + ] + }, + { + "deleted_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 + ], + "rref_rows": [ + 17, + 18, + 20, + 24 + ] + }, + { + "deleted_ports": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 12, + 13, + 14, + 15, + 16, + 17, + 18, + 19, + 20, + 21, + 22, + 23, + 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 + ], + "rref_rows": [ + 1, + 2, + 4, + 8, + 16 + ] + }, + { + "deleted_ports": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 8, + 9, + 12, + 13, + 14, + 15, + 16, + 17, + 18, + 19, + 20, + 21, + 22, + 23, + 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 + ], + "rref_rows": [ + 1, + 2, + 4, + 8, + 16, + 32 + ] + }, + { + "deleted_ports": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 8, + 9, + 10, + 12, + 13, + 14, + 15, + 16, + 17, + 18, + 19, + 20, + 21, + 22, + 23, + 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 + ], + "rref_rows": [ + 1, + 2, + 4, + 8, + 16, + 32, + 192 + ] + }, + { + "deleted_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, + 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 + ], + "rref_rows": [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128 + ] + } + ], + [ + { + "deleted_ports": [ + 0, + 1, + 2, + 3, + 12, + 13, + 14, + 15, + 88, + 89, + 90, + 91, + 92, + 93, + 94, + 95, + 96, + 97, + 98, + 99, + 100, + 101, + 102, + 103 + ], + "rref_rows": [ + 5 + ] + }, + { + "deleted_ports": [ + 0, + 1, + 2, + 3, + 4, + 5, + 12, + 13, + 14, + 15, + 16, + 17, + 80, + 81, + 82, + 83, + 88, + 89, + 90, + 91, + 92, + 93, + 94, + 95, + 96, + 97, + 98, + 99, + 100, + 101, + 102, + 103, + 108, + 109, + 110, + 111 + ], + "rref_rows": [ + 5, + 10 + ] + }, + { + "deleted_ports": [ + 0, + 1, + 2, + 3, + 4, + 5, + 12, + 13, + 14, + 15, + 16, + 17, + 80, + 81, + 82, + 83, + 84, + 85, + 86, + 87, + 88, + 89, + 90, + 91, + 92, + 93, + 94, + 95, + 96, + 97, + 98, + 99, + 100, + 101, + 102, + 103, + 104, + 105, + 106, + 107, + 108, + 109, + 110, + 111 + ], + "rref_rows": [ + 9, + 10, + 12 + ] + }, + { + "deleted_ports": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 12, + 13, + 14, + 15, + 16, + 17, + 18, + 19, + 80, + 81, + 82, + 83, + 84, + 85, + 86, + 87, + 88, + 89, + 90, + 91, + 92, + 93, + 94, + 95, + 96, + 97, + 98, + 99, + 100, + 101, + 102, + 103, + 104, + 105, + 106, + 107, + 108, + 109, + 110, + 111 + ], + "rref_rows": [ + 17, + 18, + 20, + 24 + ] + }, + { + "deleted_ports": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 12, + 13, + 14, + 15, + 16, + 17, + 18, + 19, + 20, + 21, + 22, + 23, + 80, + 81, + 82, + 83, + 84, + 85, + 86, + 87, + 88, + 89, + 90, + 91, + 92, + 93, + 94, + 95, + 96, + 97, + 98, + 99, + 100, + 101, + 102, + 103, + 104, + 105, + 106, + 107, + 108, + 109, + 110, + 111 + ], + "rref_rows": [ + 1, + 2, + 4, + 8, + 16 + ] + }, + { + "deleted_ports": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 8, + 9, + 12, + 13, + 14, + 15, + 16, + 17, + 18, + 19, + 20, + 21, + 22, + 23, + 80, + 81, + 82, + 83, + 84, + 85, + 86, + 87, + 88, + 89, + 90, + 91, + 92, + 93, + 94, + 95, + 96, + 97, + 98, + 99, + 100, + 101, + 102, + 103, + 104, + 105, + 106, + 107, + 108, + 109, + 110, + 111 + ], + "rref_rows": [ + 1, + 2, + 4, + 8, + 16, + 32 + ] + }, + { + "deleted_ports": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 8, + 9, + 11, + 12, + 13, + 14, + 15, + 16, + 17, + 18, + 19, + 20, + 21, + 22, + 23, + 80, + 81, + 82, + 83, + 84, + 85, + 86, + 87, + 88, + 89, + 90, + 91, + 92, + 93, + 94, + 95, + 96, + 97, + 98, + 99, + 100, + 101, + 102, + 103, + 104, + 105, + 106, + 107, + 108, + 109, + 110, + 111 + ], + "rref_rows": [ + 1, + 2, + 4, + 8, + 16, + 32, + 192 + ] + }, + { + "deleted_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, + 80, + 81, + 82, + 83, + 84, + 85, + 86, + 87, + 88, + 89, + 90, + 91, + 92, + 93, + 94, + 95, + 96, + 97, + 98, + 99, + 100, + 101, + 102, + 103, + 104, + 105, + 106, + 107, + 108, + 109, + 110, + 111 + ], + "rref_rows": [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128 + ] + } + ], + [ + { + "deleted_ports": [ + 0, + 1, + 2, + 3, + 12, + 13, + 14, + 15, + 24, + 25, + 26, + 27, + 28, + 29, + 30, + 31, + 32, + 33, + 34, + 35, + 36, + 37, + 38, + 39 + ], + "rref_rows": [ + 5 + ] + }, + { + "deleted_ports": [ + 0, + 1, + 2, + 3, + 12, + 13, + 14, + 15, + 24, + 25, + 26, + 27, + 28, + 29, + 30, + 31, + 32, + 33, + 34, + 35, + 36, + 37, + 38, + 39, + 49, + 50, + 51, + 55, + 73, + 74, + 75, + 79, + 83, + 84, + 107, + 108 + ], + "rref_rows": [ + 5, + 154 + ] + }, + { + "deleted_ports": [ + 0, + 1, + 2, + 3, + 12, + 13, + 14, + 15, + 30, + 31, + 38, + 39, + 48, + 49, + 50, + 51, + 52, + 53, + 54, + 55, + 72, + 73, + 74, + 75, + 76, + 77, + 78, + 79, + 80, + 81, + 82, + 83, + 84, + 85, + 86, + 87, + 104, + 105, + 106, + 107, + 108, + 109, + 110, + 111 + ], + "rref_rows": [ + 9, + 10, + 116 + ] + }, + { + "deleted_ports": [ + 0, + 1, + 2, + 3, + 12, + 13, + 14, + 15, + 24, + 25, + 30, + 31, + 32, + 33, + 38, + 39, + 48, + 49, + 50, + 51, + 52, + 53, + 54, + 55, + 72, + 73, + 74, + 75, + 76, + 77, + 78, + 79, + 80, + 81, + 82, + 83, + 84, + 85, + 86, + 87, + 104, + 105, + 106, + 107, + 108, + 109, + 110, + 111 + ], + "rref_rows": [ + 17, + 18, + 116, + 24 + ] + }, + { + "deleted_ports": [ + 0, + 1, + 12, + 13, + 14, + 15, + 24, + 25, + 28, + 29, + 30, + 31, + 32, + 33, + 34, + 35, + 36, + 37, + 38, + 39, + 48, + 49, + 50, + 51, + 52, + 53, + 54, + 55, + 72, + 73, + 74, + 75, + 76, + 77, + 78, + 79, + 80, + 81, + 82, + 83, + 84, + 85, + 86, + 87, + 104, + 105, + 106, + 107, + 108, + 109, + 110, + 111 + ], + "rref_rows": [ + 1, + 2, + 36, + 72, + 80 + ] + }, + { + "deleted_ports": [ + 0, + 1, + 2, + 3, + 12, + 13, + 14, + 15, + 24, + 25, + 26, + 27, + 30, + 31, + 32, + 33, + 34, + 35, + 36, + 37, + 38, + 39, + 48, + 49, + 50, + 51, + 52, + 53, + 54, + 55, + 72, + 73, + 74, + 75, + 76, + 77, + 78, + 79, + 80, + 81, + 82, + 83, + 84, + 85, + 86, + 87, + 104, + 105, + 106, + 107, + 108, + 109, + 110, + 111 + ], + "rref_rows": [ + 1, + 2, + 68, + 8, + 16, + 32 + ] + }, + { + "deleted_ports": [ + 0, + 1, + 2, + 3, + 12, + 13, + 14, + 15, + 24, + 25, + 26, + 27, + 28, + 29, + 30, + 32, + 33, + 34, + 35, + 36, + 37, + 38, + 39, + 48, + 49, + 50, + 51, + 52, + 53, + 54, + 55, + 72, + 73, + 74, + 75, + 76, + 77, + 78, + 79, + 80, + 81, + 82, + 83, + 84, + 85, + 86, + 87, + 104, + 105, + 106, + 107, + 108, + 109, + 110, + 111 + ], + "rref_rows": [ + 1, + 2, + 132, + 8, + 16, + 32, + 64 + ] + }, + { + "deleted_ports": [ + 0, + 1, + 2, + 3, + 12, + 13, + 14, + 15, + 24, + 25, + 26, + 27, + 28, + 29, + 30, + 31, + 32, + 33, + 34, + 35, + 36, + 37, + 38, + 39, + 48, + 49, + 50, + 51, + 52, + 53, + 54, + 55, + 72, + 73, + 74, + 75, + 76, + 77, + 78, + 79, + 80, + 81, + 82, + 83, + 84, + 85, + 86, + 87, + 104, + 105, + 106, + 107, + 108, + 109, + 110, + 111 + ], + "rref_rows": [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128 + ] + } + ], + [ + { + "deleted_ports": [ + 0, + 1, + 2, + 3, + 12, + 13, + 14, + 15, + 88, + 89, + 90, + 91, + 92, + 93, + 94, + 95, + 96, + 97, + 98, + 99, + 100, + 101, + 102, + 103 + ], + "rref_rows": [ + 9 + ] + }, + { + "deleted_ports": [ + 0, + 1, + 2, + 3, + 12, + 13, + 14, + 15, + 24, + 25, + 32, + 33, + 56, + 57, + 58, + 59, + 64, + 65, + 66, + 67, + 88, + 89, + 90, + 91, + 92, + 93, + 94, + 95, + 96, + 97, + 98, + 99, + 100, + 101, + 102, + 103 + ], + "rref_rows": [ + 9, + 18 + ] + }, + { + "deleted_ports": [ + 0, + 1, + 2, + 3, + 12, + 13, + 14, + 15, + 30, + 31, + 38, + 39, + 56, + 57, + 58, + 59, + 60, + 61, + 62, + 63, + 64, + 65, + 66, + 67, + 68, + 69, + 70, + 71, + 88, + 89, + 90, + 91, + 92, + 93, + 94, + 95, + 96, + 97, + 98, + 99, + 100, + 101, + 102, + 103 + ], + "rref_rows": [ + 9, + 10, + 116 + ] + }, + { + "deleted_ports": [ + 0, + 1, + 2, + 3, + 12, + 13, + 14, + 15, + 24, + 25, + 30, + 31, + 32, + 33, + 38, + 39, + 56, + 57, + 58, + 59, + 60, + 61, + 62, + 63, + 64, + 65, + 66, + 67, + 68, + 69, + 70, + 71, + 88, + 89, + 90, + 91, + 92, + 93, + 94, + 95, + 96, + 97, + 98, + 99, + 100, + 101, + 102, + 103 + ], + "rref_rows": [ + 17, + 18, + 116, + 24 + ] + }, + { + "deleted_ports": [ + 0, + 1, + 12, + 13, + 14, + 15, + 24, + 25, + 28, + 29, + 30, + 31, + 32, + 33, + 34, + 35, + 36, + 37, + 38, + 39, + 56, + 57, + 58, + 59, + 60, + 61, + 62, + 63, + 64, + 65, + 66, + 67, + 68, + 69, + 70, + 71, + 88, + 89, + 90, + 91, + 92, + 93, + 94, + 95, + 96, + 97, + 98, + 99, + 100, + 101, + 102, + 103 + ], + "rref_rows": [ + 1, + 2, + 36, + 72, + 80 + ] + }, + { + "deleted_ports": [ + 0, + 1, + 2, + 3, + 12, + 13, + 14, + 15, + 24, + 25, + 26, + 27, + 30, + 31, + 32, + 33, + 34, + 35, + 36, + 37, + 38, + 39, + 56, + 57, + 58, + 59, + 60, + 61, + 62, + 63, + 64, + 65, + 66, + 67, + 68, + 69, + 70, + 71, + 88, + 89, + 90, + 91, + 92, + 93, + 94, + 95, + 96, + 97, + 98, + 99, + 100, + 101, + 102, + 103 + ], + "rref_rows": [ + 1, + 2, + 68, + 8, + 16, + 32 + ] + }, + { + "deleted_ports": [ + 0, + 1, + 2, + 3, + 12, + 13, + 14, + 15, + 24, + 25, + 26, + 27, + 28, + 29, + 31, + 32, + 33, + 34, + 35, + 36, + 37, + 38, + 39, + 56, + 57, + 58, + 59, + 60, + 61, + 62, + 63, + 64, + 65, + 66, + 67, + 68, + 69, + 70, + 71, + 88, + 89, + 90, + 91, + 92, + 93, + 94, + 95, + 96, + 97, + 98, + 99, + 100, + 101, + 102, + 103 + ], + "rref_rows": [ + 1, + 2, + 132, + 8, + 16, + 32, + 64 + ] + }, + { + "deleted_ports": [ + 0, + 1, + 2, + 3, + 12, + 13, + 14, + 15, + 24, + 25, + 26, + 27, + 28, + 29, + 30, + 31, + 32, + 33, + 34, + 35, + 36, + 37, + 38, + 39, + 56, + 57, + 58, + 59, + 60, + 61, + 62, + 63, + 64, + 65, + 66, + 67, + 68, + 69, + 70, + 71, + 88, + 89, + 90, + 91, + 92, + 93, + 94, + 95, + 96, + 97, + 98, + 99, + 100, + 101, + 102, + 103 + ], + "rref_rows": [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128 + ] + } + ], + [ + { + "deleted_ports": [ + 4, + 5, + 6, + 7, + 16, + 17, + 18, + 19, + 24, + 25, + 26, + 27, + 32, + 33, + 34, + 35, + 40, + 41, + 42, + 43, + 44, + 45, + 46, + 47 + ], + "rref_rows": [ + 5 + ] + }, + { + "deleted_ports": [ + 4, + 5, + 6, + 7, + 16, + 17, + 18, + 19, + 24, + 25, + 26, + 27, + 32, + 33, + 34, + 35, + 40, + 41, + 42, + 43, + 44, + 45, + 46, + 47, + 49, + 55, + 56, + 57, + 62, + 63, + 73, + 79, + 89, + 95, + 96, + 102 + ], + "rref_rows": [ + 5, + 154 + ] + }, + { + "deleted_ports": [ + 4, + 5, + 6, + 7, + 16, + 17, + 18, + 19, + 42, + 43, + 46, + 47, + 48, + 49, + 54, + 55, + 56, + 57, + 62, + 63, + 64, + 65, + 70, + 71, + 72, + 73, + 78, + 79, + 80, + 81, + 86, + 87, + 88, + 89, + 94, + 95, + 96, + 97, + 102, + 103, + 104, + 105, + 110, + 111 + ], + "rref_rows": [ + 9, + 10, + 116 + ] + }, + { + "deleted_ports": [ + 4, + 5, + 6, + 7, + 16, + 17, + 18, + 19, + 24, + 25, + 26, + 27, + 42, + 43, + 46, + 47, + 48, + 49, + 54, + 55, + 56, + 57, + 62, + 63, + 64, + 65, + 70, + 71, + 72, + 73, + 78, + 79, + 80, + 81, + 86, + 87, + 88, + 89, + 94, + 95, + 96, + 97, + 102, + 103, + 104, + 105, + 110, + 111 + ], + "rref_rows": [ + 17, + 18, + 116, + 24 + ] + }, + { + "deleted_ports": [ + 4, + 5, + 16, + 17, + 18, + 19, + 24, + 25, + 26, + 27, + 34, + 35, + 40, + 41, + 42, + 43, + 44, + 45, + 46, + 47, + 48, + 49, + 54, + 55, + 56, + 57, + 62, + 63, + 64, + 65, + 70, + 71, + 72, + 73, + 78, + 79, + 80, + 81, + 86, + 87, + 88, + 89, + 94, + 95, + 96, + 97, + 102, + 103, + 104, + 105, + 110, + 111 + ], + "rref_rows": [ + 1, + 2, + 36, + 72, + 80 + ] + }, + { + "deleted_ports": [ + 4, + 5, + 6, + 7, + 16, + 17, + 18, + 19, + 24, + 25, + 26, + 27, + 32, + 33, + 34, + 35, + 42, + 43, + 44, + 45, + 46, + 47, + 48, + 49, + 54, + 55, + 56, + 57, + 62, + 63, + 64, + 65, + 70, + 71, + 72, + 73, + 78, + 79, + 80, + 81, + 86, + 87, + 88, + 89, + 94, + 95, + 96, + 97, + 102, + 103, + 104, + 105, + 110, + 111 + ], + "rref_rows": [ + 1, + 2, + 68, + 8, + 16, + 32 + ] + }, + { + "deleted_ports": [ + 4, + 5, + 6, + 7, + 16, + 17, + 18, + 19, + 24, + 25, + 26, + 27, + 32, + 33, + 34, + 35, + 40, + 41, + 42, + 44, + 45, + 46, + 47, + 48, + 49, + 54, + 55, + 56, + 57, + 62, + 63, + 64, + 65, + 70, + 71, + 72, + 73, + 78, + 79, + 80, + 81, + 86, + 87, + 88, + 89, + 94, + 95, + 96, + 97, + 102, + 103, + 104, + 105, + 110, + 111 + ], + "rref_rows": [ + 1, + 2, + 132, + 8, + 16, + 32, + 64 + ] + }, + { + "deleted_ports": [ + 4, + 5, + 6, + 7, + 16, + 17, + 18, + 19, + 24, + 25, + 26, + 27, + 32, + 33, + 34, + 35, + 40, + 41, + 42, + 43, + 44, + 45, + 46, + 47, + 48, + 49, + 54, + 55, + 56, + 57, + 62, + 63, + 64, + 65, + 70, + 71, + 72, + 73, + 78, + 79, + 80, + 81, + 86, + 87, + 88, + 89, + 94, + 95, + 96, + 97, + 102, + 103, + 104, + 105, + 110, + 111 + ], + "rref_rows": [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128 + ] + } + ], + [ + { + "deleted_ports": [ + 4, + 5, + 6, + 7, + 16, + 17, + 18, + 19, + 82, + 83, + 84, + 85, + 90, + 91, + 92, + 93, + 98, + 99, + 100, + 101, + 106, + 107, + 108, + 109 + ], + "rref_rows": [ + 9 + ] + }, + { + "deleted_ports": [ + 4, + 5, + 6, + 7, + 16, + 17, + 18, + 19, + 24, + 25, + 26, + 27, + 50, + 51, + 52, + 53, + 58, + 59, + 60, + 61, + 82, + 83, + 84, + 85, + 90, + 91, + 92, + 93, + 98, + 99, + 100, + 101, + 106, + 107, + 108, + 109 + ], + "rref_rows": [ + 9, + 18 + ] + }, + { + "deleted_ports": [ + 4, + 5, + 6, + 7, + 16, + 17, + 18, + 19, + 42, + 43, + 46, + 47, + 50, + 51, + 52, + 53, + 58, + 59, + 60, + 61, + 66, + 67, + 68, + 69, + 74, + 75, + 76, + 77, + 82, + 83, + 84, + 85, + 90, + 91, + 92, + 93, + 98, + 99, + 100, + 101, + 106, + 107, + 108, + 109 + ], + "rref_rows": [ + 9, + 10, + 116 + ] + }, + { + "deleted_ports": [ + 4, + 5, + 6, + 7, + 16, + 17, + 18, + 19, + 24, + 25, + 26, + 27, + 42, + 43, + 46, + 47, + 50, + 51, + 52, + 53, + 58, + 59, + 60, + 61, + 66, + 67, + 68, + 69, + 74, + 75, + 76, + 77, + 82, + 83, + 84, + 85, + 90, + 91, + 92, + 93, + 98, + 99, + 100, + 101, + 106, + 107, + 108, + 109 + ], + "rref_rows": [ + 17, + 18, + 116, + 24 + ] + }, + { + "deleted_ports": [ + 4, + 5, + 16, + 17, + 18, + 19, + 24, + 25, + 26, + 27, + 34, + 35, + 40, + 41, + 42, + 43, + 44, + 45, + 46, + 47, + 50, + 51, + 52, + 53, + 58, + 59, + 60, + 61, + 66, + 67, + 68, + 69, + 74, + 75, + 76, + 77, + 82, + 83, + 84, + 85, + 90, + 91, + 92, + 93, + 98, + 99, + 100, + 101, + 106, + 107, + 108, + 109 + ], + "rref_rows": [ + 1, + 2, + 36, + 72, + 80 + ] + }, + { + "deleted_ports": [ + 4, + 5, + 6, + 7, + 16, + 17, + 18, + 19, + 24, + 25, + 26, + 27, + 32, + 33, + 34, + 35, + 42, + 43, + 44, + 45, + 46, + 47, + 50, + 51, + 52, + 53, + 58, + 59, + 60, + 61, + 66, + 67, + 68, + 69, + 74, + 75, + 76, + 77, + 82, + 83, + 84, + 85, + 90, + 91, + 92, + 93, + 98, + 99, + 100, + 101, + 106, + 107, + 108, + 109 + ], + "rref_rows": [ + 1, + 2, + 68, + 8, + 16, + 32 + ] + }, + { + "deleted_ports": [ + 4, + 5, + 6, + 7, + 16, + 17, + 18, + 19, + 24, + 25, + 26, + 27, + 32, + 33, + 34, + 35, + 40, + 41, + 43, + 44, + 45, + 46, + 47, + 50, + 51, + 52, + 53, + 58, + 59, + 60, + 61, + 66, + 67, + 68, + 69, + 74, + 75, + 76, + 77, + 82, + 83, + 84, + 85, + 90, + 91, + 92, + 93, + 98, + 99, + 100, + 101, + 106, + 107, + 108, + 109 + ], + "rref_rows": [ + 1, + 2, + 132, + 8, + 16, + 32, + 64 + ] + }, + { + "deleted_ports": [ + 4, + 5, + 6, + 7, + 16, + 17, + 18, + 19, + 24, + 25, + 26, + 27, + 32, + 33, + 34, + 35, + 40, + 41, + 42, + 43, + 44, + 45, + 46, + 47, + 50, + 51, + 52, + 53, + 58, + 59, + 60, + 61, + 66, + 67, + 68, + 69, + 74, + 75, + 76, + 77, + 82, + 83, + 84, + 85, + 90, + 91, + 92, + 93, + 98, + 99, + 100, + 101, + 106, + 107, + 108, + 109 + ], + "rref_rows": [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128 + ] + } + ], + [ + { + "deleted_ports": [ + 8, + 9, + 10, + 11, + 20, + 21, + 22, + 23, + 28, + 29, + 30, + 31, + 36, + 37, + 38, + 39, + 40, + 41, + 42, + 43, + 44, + 45, + 46, + 47 + ], + "rref_rows": [ + 5 + ] + }, + { + "deleted_ports": [ + 8, + 9, + 10, + 11, + 20, + 21, + 22, + 23, + 28, + 29, + 30, + 31, + 36, + 37, + 38, + 39, + 40, + 41, + 42, + 43, + 44, + 45, + 46, + 47, + 54, + 55, + 58, + 59, + 60, + 61, + 78, + 79, + 94, + 95, + 96, + 97 + ], + "rref_rows": [ + 5, + 154 + ] + }, + { + "deleted_ports": [ + 8, + 9, + 10, + 11, + 20, + 21, + 22, + 23, + 44, + 45, + 46, + 47, + 48, + 49, + 54, + 55, + 58, + 59, + 60, + 61, + 66, + 67, + 68, + 69, + 72, + 73, + 78, + 79, + 82, + 83, + 84, + 85, + 88, + 89, + 94, + 95, + 96, + 97, + 102, + 103, + 106, + 107, + 108, + 109 + ], + "rref_rows": [ + 9, + 10, + 116 + ] + }, + { + "deleted_ports": [ + 8, + 9, + 10, + 11, + 20, + 21, + 22, + 23, + 28, + 29, + 30, + 31, + 44, + 45, + 46, + 47, + 48, + 49, + 54, + 55, + 58, + 59, + 60, + 61, + 66, + 67, + 68, + 69, + 72, + 73, + 78, + 79, + 82, + 83, + 84, + 85, + 88, + 89, + 94, + 95, + 96, + 97, + 102, + 103, + 106, + 107, + 108, + 109 + ], + "rref_rows": [ + 17, + 18, + 116, + 24 + ] + }, + { + "deleted_ports": [ + 8, + 9, + 20, + 21, + 22, + 23, + 28, + 29, + 30, + 31, + 38, + 39, + 40, + 41, + 42, + 43, + 44, + 45, + 46, + 47, + 48, + 49, + 54, + 55, + 58, + 59, + 60, + 61, + 66, + 67, + 68, + 69, + 72, + 73, + 78, + 79, + 82, + 83, + 84, + 85, + 88, + 89, + 94, + 95, + 96, + 97, + 102, + 103, + 106, + 107, + 108, + 109 + ], + "rref_rows": [ + 1, + 2, + 36, + 72, + 80 + ] + }, + { + "deleted_ports": [ + 8, + 9, + 10, + 11, + 20, + 21, + 22, + 23, + 28, + 29, + 30, + 31, + 36, + 37, + 38, + 39, + 42, + 43, + 44, + 45, + 46, + 47, + 48, + 49, + 54, + 55, + 58, + 59, + 60, + 61, + 66, + 67, + 68, + 69, + 72, + 73, + 78, + 79, + 82, + 83, + 84, + 85, + 88, + 89, + 94, + 95, + 96, + 97, + 102, + 103, + 106, + 107, + 108, + 109 + ], + "rref_rows": [ + 1, + 2, + 68, + 8, + 16, + 32 + ] + }, + { + "deleted_ports": [ + 8, + 9, + 10, + 11, + 20, + 21, + 22, + 23, + 28, + 29, + 30, + 31, + 36, + 37, + 38, + 39, + 40, + 41, + 42, + 43, + 44, + 46, + 47, + 48, + 49, + 54, + 55, + 58, + 59, + 60, + 61, + 66, + 67, + 68, + 69, + 72, + 73, + 78, + 79, + 82, + 83, + 84, + 85, + 88, + 89, + 94, + 95, + 96, + 97, + 102, + 103, + 106, + 107, + 108, + 109 + ], + "rref_rows": [ + 1, + 2, + 132, + 8, + 16, + 32, + 64 + ] + }, + { + "deleted_ports": [ + 8, + 9, + 10, + 11, + 20, + 21, + 22, + 23, + 28, + 29, + 30, + 31, + 36, + 37, + 38, + 39, + 40, + 41, + 42, + 43, + 44, + 45, + 46, + 47, + 48, + 49, + 54, + 55, + 58, + 59, + 60, + 61, + 66, + 67, + 68, + 69, + 72, + 73, + 78, + 79, + 82, + 83, + 84, + 85, + 88, + 89, + 94, + 95, + 96, + 97, + 102, + 103, + 106, + 107, + 108, + 109 + ], + "rref_rows": [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128 + ] + } + ], + [ + { + "deleted_ports": [ + 8, + 9, + 10, + 11, + 20, + 21, + 22, + 23, + 80, + 81, + 86, + 87, + 90, + 91, + 92, + 93, + 98, + 99, + 100, + 101, + 104, + 105, + 110, + 111 + ], + "rref_rows": [ + 9 + ] + }, + { + "deleted_ports": [ + 8, + 9, + 10, + 11, + 20, + 21, + 22, + 23, + 28, + 29, + 30, + 31, + 50, + 51, + 52, + 53, + 56, + 57, + 62, + 63, + 80, + 81, + 86, + 87, + 90, + 91, + 92, + 93, + 98, + 99, + 100, + 101, + 104, + 105, + 110, + 111 + ], + "rref_rows": [ + 9, + 18 + ] + }, + { + "deleted_ports": [ + 8, + 9, + 10, + 11, + 20, + 21, + 22, + 23, + 44, + 45, + 46, + 47, + 50, + 51, + 52, + 53, + 56, + 57, + 62, + 63, + 64, + 65, + 70, + 71, + 74, + 75, + 76, + 77, + 80, + 81, + 86, + 87, + 90, + 91, + 92, + 93, + 98, + 99, + 100, + 101, + 104, + 105, + 110, + 111 + ], + "rref_rows": [ + 9, + 10, + 116 + ] + }, + { + "deleted_ports": [ + 8, + 9, + 10, + 11, + 20, + 21, + 22, + 23, + 28, + 29, + 30, + 31, + 44, + 45, + 46, + 47, + 50, + 51, + 52, + 53, + 56, + 57, + 62, + 63, + 64, + 65, + 70, + 71, + 74, + 75, + 76, + 77, + 80, + 81, + 86, + 87, + 90, + 91, + 92, + 93, + 98, + 99, + 100, + 101, + 104, + 105, + 110, + 111 + ], + "rref_rows": [ + 17, + 18, + 116, + 24 + ] + }, + { + "deleted_ports": [ + 8, + 9, + 20, + 21, + 22, + 23, + 28, + 29, + 30, + 31, + 38, + 39, + 40, + 41, + 42, + 43, + 44, + 45, + 46, + 47, + 50, + 51, + 52, + 53, + 56, + 57, + 62, + 63, + 64, + 65, + 70, + 71, + 74, + 75, + 76, + 77, + 80, + 81, + 86, + 87, + 90, + 91, + 92, + 93, + 98, + 99, + 100, + 101, + 104, + 105, + 110, + 111 + ], + "rref_rows": [ + 1, + 2, + 36, + 72, + 80 + ] + }, + { + "deleted_ports": [ + 8, + 9, + 10, + 11, + 20, + 21, + 22, + 23, + 28, + 29, + 30, + 31, + 36, + 37, + 38, + 39, + 42, + 43, + 44, + 45, + 46, + 47, + 50, + 51, + 52, + 53, + 56, + 57, + 62, + 63, + 64, + 65, + 70, + 71, + 74, + 75, + 76, + 77, + 80, + 81, + 86, + 87, + 90, + 91, + 92, + 93, + 98, + 99, + 100, + 101, + 104, + 105, + 110, + 111 + ], + "rref_rows": [ + 1, + 2, + 68, + 8, + 16, + 32 + ] + }, + { + "deleted_ports": [ + 8, + 9, + 10, + 11, + 20, + 21, + 22, + 23, + 28, + 29, + 30, + 31, + 36, + 37, + 38, + 39, + 40, + 41, + 42, + 43, + 45, + 46, + 47, + 50, + 51, + 52, + 53, + 56, + 57, + 62, + 63, + 64, + 65, + 70, + 71, + 74, + 75, + 76, + 77, + 80, + 81, + 86, + 87, + 90, + 91, + 92, + 93, + 98, + 99, + 100, + 101, + 104, + 105, + 110, + 111 + ], + "rref_rows": [ + 1, + 2, + 132, + 8, + 16, + 32, + 64 + ] + }, + { + "deleted_ports": [ + 8, + 9, + 10, + 11, + 20, + 21, + 22, + 23, + 28, + 29, + 30, + 31, + 36, + 37, + 38, + 39, + 40, + 41, + 42, + 43, + 44, + 45, + 46, + 47, + 50, + 51, + 52, + 53, + 56, + 57, + 62, + 63, + 64, + 65, + 70, + 71, + 74, + 75, + 76, + 77, + 80, + 81, + 86, + 87, + 90, + 91, + 92, + 93, + 98, + 99, + 100, + 101, + 104, + 105, + 110, + 111 + ], + "rref_rows": [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128 + ] + } + ] + ] + }, + "schema_version": 1, + "source_geometry_sha256": "4f44af368e046002553d632ee90c6470990827cea3fae41f0f54018522d7a080", + "two_total_fixture": { + "at_23": { + "added_ranks": [ + 7, + 7 + ], + "retained_ranks": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8 + ], + "source_union_size": 23, + "total_copy_rank": 78 + }, + "at_24": { + "added_ranks": [ + 7, + 7 + ], + "retained_ranks": [ + 7, + 7, + 8, + 8, + 8, + 8, + 8, + 8 + ], + "source_union_size": 24, + "total_copy_rank": 76 + } + }, + "two_total_small_support_screen": { + "minimum_full_rank_margin": 1, + "records": [ + { + "maximum_retained_loss": 0, + "minimum_added_rank": 2, + "union_size": 1 + }, + { + "maximum_retained_loss": 0, + "minimum_added_rank": 2, + "union_size": 2 + }, + { + "maximum_retained_loss": 0, + "minimum_added_rank": 2, + "union_size": 3 + }, + { + "maximum_retained_loss": 0, + "minimum_added_rank": 2, + "union_size": 4 + }, + { + "maximum_retained_loss": 0, + "minimum_added_rank": 2, + "union_size": 5 + }, + { + "maximum_retained_loss": 0, + "minimum_added_rank": 2, + "union_size": 6 + }, + { + "maximum_retained_loss": 0, + "minimum_added_rank": 2, + "union_size": 7 + }, + { + "maximum_retained_loss": 0, + "minimum_added_rank": 2, + "union_size": 8 + }, + { + "maximum_retained_loss": 0, + "minimum_added_rank": 3, + "union_size": 9 + }, + { + "maximum_retained_loss": 0, + "minimum_added_rank": 3, + "union_size": 10 + }, + { + "maximum_retained_loss": 0, + "minimum_added_rank": 3, + "union_size": 11 + }, + { + "maximum_retained_loss": 0, + "minimum_added_rank": 3, + "union_size": 12 + }, + { + "maximum_retained_loss": 0, + "minimum_added_rank": 4, + "union_size": 13 + }, + { + "maximum_retained_loss": 0, + "minimum_added_rank": 4, + "union_size": 14 + }, + { + "maximum_retained_loss": 0, + "minimum_added_rank": 4, + "union_size": 15 + }, + { + "maximum_retained_loss": 0, + "minimum_added_rank": 4, + "union_size": 16 + }, + { + "maximum_retained_loss": 0, + "minimum_added_rank": 4, + "union_size": 17 + }, + { + "maximum_retained_loss": 0, + "minimum_added_rank": 4, + "union_size": 18 + }, + { + "maximum_retained_loss": 0, + "minimum_added_rank": 4, + "union_size": 19 + }, + { + "maximum_retained_loss": 0, + "minimum_added_rank": 4, + "union_size": 20 + }, + { + "maximum_retained_loss": 0, + "minimum_added_rank": 5, + "union_size": 21 + }, + { + "maximum_retained_loss": 0, + "minimum_added_rank": 5, + "union_size": 22 + }, + { + "maximum_retained_loss": 0, + "minimum_added_rank": 5, + "union_size": 23 + }, + { + "maximum_retained_loss": 2, + "minimum_added_rank": 5, + "union_size": 24 + }, + { + "maximum_retained_loss": 2, + "minimum_added_rank": 5, + "union_size": 25 + }, + { + "maximum_retained_loss": 2, + "minimum_added_rank": 5, + "union_size": 26 + }, + { + "maximum_retained_loss": 2, + "minimum_added_rank": 5, + "union_size": 27 + }, + { + "maximum_retained_loss": 2, + "minimum_added_rank": 5, + "union_size": 28 + }, + { + "maximum_retained_loss": 2, + "minimum_added_rank": 5, + "union_size": 29 + }, + { + "maximum_retained_loss": 2, + "minimum_added_rank": 5, + "union_size": 30 + }, + { + "maximum_retained_loss": 2, + "minimum_added_rank": 5, + "union_size": 31 + }, + { + "maximum_retained_loss": 2, + "minimum_added_rank": 5, + "union_size": 32 + }, + { + "maximum_retained_loss": 2, + "minimum_added_rank": 5, + "union_size": 33 + }, + { + "maximum_retained_loss": 2, + "minimum_added_rank": 5, + "union_size": 34 + }, + { + "maximum_retained_loss": 2, + "minimum_added_rank": 5, + "union_size": 35 + }, + { + "maximum_retained_loss": 4, + "minimum_added_rank": 5, + "union_size": 36 + }, + { + "maximum_retained_loss": 4, + "minimum_added_rank": 6, + "union_size": 37 + }, + { + "maximum_retained_loss": 4, + "minimum_added_rank": 6, + "union_size": 38 + }, + { + "maximum_retained_loss": 4, + "minimum_added_rank": 6, + "union_size": 39 + }, + { + "maximum_retained_loss": 5, + "minimum_added_rank": 6, + "union_size": 40 + }, + { + "maximum_retained_loss": 5, + "minimum_added_rank": 6, + "union_size": 41 + }, + { + "maximum_retained_loss": 5, + "minimum_added_rank": 6, + "union_size": 42 + }, + { + "maximum_retained_loss": 5, + "minimum_added_rank": 6, + "union_size": 43 + } + ] + } +} diff --git a/research/p112-two-total-support-threshold/SOURCES.json b/research/p112-two-total-support-threshold/SOURCES.json new file mode 100644 index 0000000000..285849c34b --- /dev/null +++ b/research/p112-two-total-support-threshold/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "a18b4b0136d647529971e9fcb99fa83f5b9a0b81", + "files": [ + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "06c96f5579bb67ed1b86d334e78fbed7da6945f1", + "sha256": "6686ad58f1fbdbc87134a78901b60fd53a20d3984355e91defbbebc9e9fa8075" + }, + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "research/p112-single-lift/reference-geometry.json", + "usage": "input", + "git_blob": "d862663d3c0ffe3c72df510e89997beb85cef640", + "sha256": "4f44af368e046002553d632ee90c6470990827cea3fae41f0f54018522d7a080" + }, + { + "path": "research/p112-single-lift/geometry.py", + "usage": "input", + "git_blob": "34c1abf059d7be5fe5e5044cf01a09b843071c68", + "sha256": "3857c11ec731a602b8059d85d58fbb3b641bab687bb33016a0e54f7567752c8a" + }, + { + "path": "research/p112-two-total-rank-one-seed21/PROOF.md", + "usage": "input", + "git_blob": "4ec1af4cc9f7d47872a725fc37f3d400e9c2b3c3", + "sha256": "7209dd082f47dca3d096ceb30b9efd674d6332d5ca0e4decd22337b0b3b87d6f" + } + ] +} diff --git a/research/p112-two-total-support-threshold/TASK.json b/research/p112-two-total-support-threshold/TASK.json new file mode 100644 index 0000000000..cda0348d3e --- /dev/null +++ b/research/p112-two-total-support-threshold/TASK.json @@ -0,0 +1,72 @@ +{ + "schema_version": 1, + "task_id": "complex-rank-shape-decoder", + "priority_revision": 3, + "base_commit": "a18b4b0136d647529971e9fcb99fa83f5b9a0b81", + "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" + ], + "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." + ], + "overlap_terms": [ + "rank shape", + "block climb", + "masked decoder", + "overcomplete", + "effective rank" + ] + }, + "scope_status": "changed", + "actual_scope": "Exact generalized binary support weights for the eight selected P112 coordinate readers, cross-reader minimum-cut overlaps, and an added-term source-support bound proving no two-total COPY saving through union size 43.", + "scope_change_reason": "The original card seeks a physically priced larger-rank child profile. Nearby open PR1633/PR1671 and discussions 1596/1659 cover obvious rank-shape directions; this is a narrower algebraic search-pruning result in Philipp’s still-open coupled rank-two two-total case. It does not meet the 5% construction gate.", + "bottleneck_link": "A cheaper complex decoder could change the binding complex supplier. This exact support obstruction rules out one small-source route to reducing the separate-total COPY charge, but does not price or improve a supplier.", + "budget_minutes": 185, + "stop_rule": "Stop after all eight P112 coordinate codes, complete RREF subspace census for dimensions 1..8, cross-reader size-24 overlap and triple/four-reader thresholds, 511-functional added-reader span census, union sizes 1..43 bill, one exact full-rank two-total boundary fixture, source pins, failure controls and registered replay. Do not search arbitrary larger complex source unions or claim a full ten-term floor.", + "outcome": "completed", + "evidence": "RESULT.json and stdlib verify.py: all eight coordinate codes have generalized support weights 24,36,44,48,52,54,55,56; every coordinate pair shares one minimal 24-cut; three reader rank drops require union at least 40, while all four-reader cuts below 44 are 42 size-40 sets and a fifth needs four more ports; the exact 511-functional span census and source-label count give an added-term charge proving no COPY saving for exact two-total source unions through 43 (with predecessor reductions); exact full-rank coupled fixture first drops two retained ranks at 24 but costs 76.", + "author": "Josie Elliston", + "ai_assistance": "Substantial AI assistance: prepared by OpenAI Codex (offline session 17: mathematical analysis, exact verifier, controls and writing); reviewed, corrected and published by Claude (Anthropic, session 19). No independent human review.", + "open_questions": [ + { + "question": "Can the remaining full-rank, overlapping two-total P112 case lower the total separate-total COPY sum below 64?", + "why_it_matters": "A genuine rank-shape decoder improvement needs the complete two-source tradeoff, including added-term charges.", + "first_step": "Use the 24/36/40 support thresholds to prune a source-support-aware exact search beginning at union size 44, retaining the non-free basis dependence of beta.", + "blocked_by": "The present theorem proves the complete COPY floor only through source union 43; larger unions may have several retained rank drops and need sharper added-term bounds." + }, + { + "question": "Are the exact cross-reader support thresholds for four or more rank drops useful to a physically priced decoder?", + "why_it_matters": "They could restrict candidate source alphabets or reveal a shared-source pattern.", + "first_step": "Enumerate unions of minimal evaluation-code supports with source coefficient constraints, then price all added terms and restoration.", + "blocked_by": "The current result proves the triple threshold and the four-reader census only below union 44, and an unconstrained union need not be attainable by two complex source columns." + } + ] +} diff --git a/research/p112-two-total-support-threshold/VERIFY.json b/research/p112-two-total-support-threshold/VERIFY.json new file mode 100644 index 0000000000..e5bb3b3fa4 --- /dev/null +++ b/research/p112-two-total-support-threshold/VERIFY.json @@ -0,0 +1,23 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/p112-single-lift/reference-geometry.json", + "research/p112-single-lift/geometry.py", + "research/p112-two-total-rank-one-seed21/PROOF.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Pinned P112 source and exact E8 geometry; complete F2 subspace census; eight generalized weight tables; cross-reader cut thresholds; independent exact 511-functional reader-span census and union-size 1..43 added-cost screen; full-rank two-total identity and rank boundary; mutation/one-port-short controls; full receipt comparison" + } + ] +} diff --git a/research/p112-two-total-support-threshold/verify.py b/research/p112-two-total-support-threshold/verify.py new file mode 100644 index 0000000000..c80d773609 --- /dev/null +++ b/research/p112-two-total-support-threshold/verify.py @@ -0,0 +1,478 @@ +#!/usr/bin/env python3 +"""Exact support thresholds for fixed P112 coordinate readers (stdlib).""" + +import argparse +from collections import Counter +from fractions import Fraction +from hashlib import sha1, sha256 +import importlib.util +from itertools import combinations, product +import json +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +WEIGHTS = (24, 36, 44, 48, 52, 54, 55, 56) +SUBSPACE_COUNTS = (255, 10795, 97155, 200787, 97155, 10795, 255, 1) + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def parity(value): + return value.bit_count() & 1 + + +def rank_f2(rows): + pivots = {} + for original in rows: + value = original + while value: + pivot = value.bit_length() - 1 + if pivot in pivots: + value ^= pivots[pivot] + else: + pivots[pivot] = value + break + return len(pivots) + + +def rank_q(rows): + basis = {} + for original in rows: + row = list(map(Fraction, original)) + for pivot, previous in sorted(basis.items()): + coefficient = row[pivot] + if coefficient: + row = [a - coefficient * b for a, b in zip(row, previous)] + pivot = next((i for i, a in enumerate(row) if a), None) + if pivot is not None: + coefficient = row[pivot] + basis[pivot] = [a / coefficient for a in row] + return len(basis) + + +def basis_f2(rows): + result = [] + for row in rows: + if rank_f2(result + [row]) > len(result): + result.append(row) + return result + + +def check_sources(): + manifest = json.loads((HERE / 'SOURCES.json').read_text()) + require(manifest['base_commit'] == + 'a18b4b0136d647529971e9fcb99fa83f5b9a0b81', 'base commit') + for entry in manifest['files']: + if entry['usage'] == 'provenance': + continue # Bound to base Git by research_package.py, not live input. + raw = (ROOT / entry['path']).read_bytes() + require(sha256(raw).hexdigest() == entry['sha256'], + 'source SHA-256: ' + entry['path']) + blob = sha1(b'blob ' + str(len(raw)).encode() + b'\0' + raw).hexdigest() + require(blob == entry['git_blob'], 'source Git blob: ' + entry['path']) + + +def dot(a, b): + return sum(x * y for x, y in zip(a, b)) + + +def check_geometry(data): + roots, frame = data['roots'], data['frame'] + labels, duals, x = data['labels'], data['duals'], data['X'] + require(len(roots) == len(labels) == len(duals) == len(x) == 112, + 'P112 port count') + require(len(frame) == 8 and len({tuple(v) for v in roots}) == 112, + 'frame and distinct root lines') + require(all(len(v) == 8 and dot(v, v) == 8 for v in roots), + 'scaled E8 root norms') + require(all(len(v) == 8 and dot(v, v) == 8 for v in frame), + 'scaled frame norms') + require(all(dot(frame[j], frame[k]) == 0 + for j, k in combinations(range(8), 2)), 'frame orthogonality') + require(all(0 <= v < 512 for v in labels + duals), 'nine-bit labels') + require(0 not in labels and len(set(labels)) == 112, + 'distinct nonzero live source labels') + require(rank_f2(labels) == 9 and rank_f2(duals) == 9, + 'full label and dual spans') + for i in range(112): + require(x[i] == [dot(roots[i], f) // 4 for f in frame] + and all(dot(roots[i], f) % 4 == 0 for f in frame), + 'coordinate columns bound to E8 roots') + require(all(v in (-1, 0, 1) for v in x[i]), 'coordinate alphabet') + for k in range(112): + gram4 = dot(roots[i], roots[k]) + require(gram4 % 4 == 0, 'integral Gram') + gram = gram4 // 4 + require(dot(x[i], x[k]) == 2 * gram, 'XX^T = 2G') + require(parity(duals[i] & labels[k]) == ((1 + gram) & 1), + 'binary pairing identity') + + +def geometry_mutation_controls(data): + for field, index, bit in [('labels', 0, 1), ('duals', 0, 1)]: + bad = dict(data) + bad[field] = list(data[field]) + bad[field][index] ^= bit + try: + check_geometry(bad) + except ValueError: + pass + else: + raise ValueError('undetected geometry mutation: ' + field) + bad = dict(data) + bad['X'] = [list(row) for row in data['X']] + bad['X'][0][0] = 0 + try: + check_geometry(bad) + except ValueError: + pass + else: + raise ValueError('undetected coordinate mutation') + + +def reader_rows(data, j): + return [i for i, row in enumerate(data['X']) if row[j] != 0] + + +def term_rank(data, j, sources): + """Direct rank of the actual restricted reader/source pairing matrix.""" + rows = reader_rows(data, j) + labels, duals = data['labels'], data['duals'] + return rank_f2(sum(parity(duals[i] & labels[t]) << p + for p, t in enumerate(sources)) for i in rows) + + +def code_for_reader(data, j): + """The eight-dimensional binary evaluation code on this reader's support.""" + ports = reader_rows(data, j) + require(len(ports) == 56, 'coordinate support size') + dual_basis = basis_f2(data['duals'][i] for i in ports) + require(len(dual_basis) == 8, 'reader dual span dimension') + basis = [sum(parity(v & data['labels'][i]) << t + for t, i in enumerate(ports)) for v in dual_basis] + require(rank_f2(basis) == 8, 'baseline COPY rank eight') + code = [0] * 256 + for a in range(1, 256): + low = a & -a + code[a] = code[a ^ low] ^ basis[low.bit_length() - 1] + require(len(set(code)) == 256, 'distinct evaluation words') + # A second description enumerates every ambient nine-bit functional. + ambient = {sum(parity(q & data['labels'][i]) << t + for t, i in enumerate(ports)) for q in range(512)} + require(ambient == set(code), 'ambient quotient code agreement') + require(Counter(v.bit_count() for v in code) == + {0: 1, 24: 63, 28: 128, 32: 63, 56: 1}, + 'single-word weight distribution') + return ports, code + + +def added_reader_span_census(data): + """Exact all-functional premise for arbitrary complex on-column readers.""" + exceptions = [] + ranks = Counter() + for q in range(1, 512): + rows = [row for row, dual in zip(data['X'], data['duals']) + if parity(q & dual)] + rank = rank_q(rows) + ranks[rank] += 1 + if rank == 7: + zero_columns = [j for j in range(8) + if all(row[j] == 0 for row in rows)] + require(len(zero_columns) == 1, + 'rank-seven coordinate-axis kernel') + exceptions.append({'functional': q, + 'zero_coordinate': zero_columns[0]}) + else: + require(rank == 8, 'unexpected functional rational rank') + require(ranks == {7: 8, 8: 503}, 'complete 511-functional census') + require(sorted(e['zero_coordinate'] for e in exceptions) == + list(range(8)), 'one exceptional kernel per coordinate') + require(not ({e['functional'] for e in exceptions} & set(data['labels'])), + 'no live source label is exceptional') + return {'rank_counts': {str(k): v for k, v in sorted(ranks.items())}, + 'exceptions': exceptions, + 'distinct_live_labels': len(set(data['labels']))} + + +def source_price_lower(sites): + """If the on-column reader span is >=8, its source rank obeys this.""" + require(sites >= 1, 'nonempty source support') + return next(r for r in range(1, 10) if sites <= 1 << (r + 1)) + + +def two_total_small_support_screen(): + """A lower bill for full-rank on-column factors at union size <=43.""" + records = [] + for union_size in range(1, 44): + # Distinct source labels imply m<=2^(r+1): the preimage of an + # r-dimensional image under a map with kernel dimension <=1. + minimum_added = min(source_price_lower(m1) + source_price_lower(m2) + for m1 in range(1, union_size + 1) + for m2 in range(1, union_size + 1) + if m1 + m2 >= union_size) + if union_size < 24: + maximum_retained_loss = 0 + elif union_size < 36: + maximum_retained_loss = 2 + elif union_size < 40: + maximum_retained_loss = 4 + else: + maximum_retained_loss = 5 + require(minimum_added > maximum_retained_loss, + 'strict full-rank COPY floor through 43') + records.append({'union_size': union_size, + 'minimum_added_rank': minimum_added, + 'maximum_retained_loss': maximum_retained_loss}) + return {'records': records, + 'minimum_full_rank_margin': min(r['minimum_added_rank'] - + r['maximum_retained_loss'] + for r in records)} + + +def rref_subspaces(k): + """Enumerate every k-space of F2^8 once by its unique RREF matrix.""" + for pivots in combinations(range(8), k): + free = [tuple(c for c in range(p + 1, 8) if c not in pivots) + for p in pivots] + choices = [tuple((1 << p) | + sum(1 << col for b, col in enumerate(cols) + if mask >> b & 1) + for mask in range(1 << len(cols))) + for p, cols in zip(pivots, free)] + yield from product(*choices) + + +def global_mask(local_mask, ports): + return sum(1 << ports[t] for t in range(56) if local_mask >> t & 1) + + +def rank_of_surviving_columns(data, j, deleted): + sources = [i for i in reader_rows(data, j) if i not in deleted] + return term_rank(data, j, sources) + + +def generalized_weights(data): + codes = [code_for_reader(data, j) for j in range(8)] + minima = [[57] * 8 for _ in range(8)] + minimizer_counts = [[0] * 8 for _ in range(8)] + witnesses = [[None] * 8 for _ in range(8)] + subspace_counts = [] + for d in range(1, 9): + count = 0 + for rows in rref_subspaces(d): + count += 1 + for j, (ports, code) in enumerate(codes): + support = 0 + for row in rows: + support |= code[row] + weight = support.bit_count() + if weight < minima[j][d - 1]: + minima[j][d - 1] = weight + minimizer_counts[j][d - 1] = 1 + witnesses[j][d - 1] = { + 'rref_rows': list(rows), + 'deleted_ports': [ports[t] for t in range(56) + if support >> t & 1], + } + elif weight == minima[j][d - 1]: + minimizer_counts[j][d - 1] += 1 + subspace_counts.append(count) + require(tuple(subspace_counts) == SUBSPACE_COUNTS, + 'complete RREF subspace counts') + require(all(tuple(row) == WEIGHTS for row in minima), + 'generalized support weights') + for j in range(8): + for d in range(1, 9): + deleted = set(witnesses[j][d - 1]['deleted_ports']) + require(len(deleted) == WEIGHTS[d - 1], 'witness support size') + require(rank_of_surviving_columns(data, j, deleted) <= 8 - d, + 'independent direct-rank witness') + # Removing any one site from a minimum d-erosion witness + # must restore at least one rank unit. + require(all(rank_of_surviving_columns(data, j, deleted - {i}) + >= 9 - d for i in deleted), + 'one-port-short control') + return codes, { + 'weights': minima, + 'subspace_counts': subspace_counts, + 'minimizer_counts': minimizer_counts, + 'witnesses': witnesses, + } + + +def cross_reader_cuts(data, codes): + supports = [sum(1 << i for i in reader_rows(data, j)) for j in range(8)] + require(all((supports[a] & supports[b]).bit_count() == 24 + for a, b in combinations(range(8), 2)), + 'reader support pair intersections') + cuts = [] + for ports, code in codes: + cuts.append({global_mask(v, ports) for v in code if v.bit_count() == 24}) + require(all(len(c) == 63 for c in cuts), '63 minimum cuts per reader') + overlaps = Counter(c for family in cuts for c in family) + require(Counter(overlaps.values()) == {1: 448, 2: 28}, + 'size-24 cross-reader multiplicities') + common = {} + for a, b in combinations(range(8), 2): + intersection = cuts[a] & cuts[b] + require(len(intersection) == 1, 'one common cut per reader pair') + common[f'{a},{b}'] = sorted(i for i in range(112) + if next(iter(intersection)) >> i & 1) + # Any rank drop requires the source deletion set to contain a nonzero + # evaluation word. Search all pair unions below 40 and rule out a third. + under_40 = [{global_mask(v, ports) for v in code + if 0 < v.bit_count() < 40} for ports, code in codes] + require(all(len(c) == 254 for c in under_40), 'all cuts below 40') + triple_witness = None + for a, b, c in combinations(range(8), 3): + pair_unions = {x | y for x in under_40[a] for y in under_40[b] + if (x | y).bit_count() < 40} + require(all((u | z).bit_count() >= 40 + for u in pair_unions for z in under_40[c]), + 'no triple rank drop below 40 source sites') + if triple_witness is None: + options = ((x | y | z, x, y, z) + for x in cuts[a] for y in cuts[b] for z in cuts[c]) + triple_witness = next((t for t in options if t[0].bit_count() == 40), + None) + require(triple_witness is not None, 'triple combinatorial threshold 40') + triple_ports = [i for i in range(112) + if triple_witness[0] >> i & 1] + require(all(rank_of_surviving_columns(data, j, set(triple_ports)) <= 7 + for j in (0, 1, 2)), 'three-reader direct-rank witness') + # The word weights jump from 32 to 56, so under_40 is also the full + # nonzero cut inventory below 44. Every four-reader drop below 44 + # contains one of these exact unions. + # Their 42 minimal supports have size 40; a fifth reader needs >=4 + # additional sites. Along with w_2=36 and pairwise |S_a cap S_b|=24, + # at most one of four dropping readers can lose a second rank unit. + pair_unions_44 = {} + for a, b in combinations(range(8), 2): + pair_unions_44[a, b] = {x | y for x in under_40[a] + for y in under_40[b] + if (x | y).bit_count() < 44} + four_masks = set() + for a, b, c, d in combinations(range(8), 4): + four_masks.update(x | y for x in pair_unions_44[a, b] + for y in pair_unions_44[c, d] + if (x | y).bit_count() < 44) + require(len(four_masks) == 42 and + all(x.bit_count() == 40 for x in four_masks), + 'all four-reader cuts below 44') + for mask in four_masks: + hit = [j for j in range(8) + if any((word & ~mask) == 0 for word in under_40[j])] + require(len(hit) == 4, 'four-reader cut hits exactly four') + require(all((word & ~mask).bit_count() >= 4 + for j in range(8) if j not in hit + for word in under_40[j]), + 'fifth reader needs four more ports') + return {'minimum_cut_multiplicity': + {str(k): v for k, v in sorted(Counter(overlaps.values()).items())}, + 'common_minimum_cuts': common, + 'triple_minimum_union': 40, + 'triple_witness_ports': triple_ports, + 'four_reader_cuts_below_44': len(four_masks), + 'four_reader_cut_sizes': sorted({x.bit_count() for x in four_masks}), + 'reader_support_pair_intersection': 24} + + +def two_total_fixture(data, common_ports): + """Full-rank coupled two-total identity at the sharp 24-site boundary.""" + c = set(common_ports) + require(len(c) == 24, 'fixture cut length') + x = [[row[j] for row in data['X']] for j in range(8)] + + def evaluate(deleted): + # A has rows (1,1), (1,-1), then six zero rows. Its columns + # overlap at both retained coordinates and have rank two. + z1 = [(x[0][i] + x[1][i]) // 2 if i in deleted else 0 + for i in range(112)] + z2 = [(x[0][i] - x[1][i]) // 2 if i in deleted else 0 + for i in range(112)] + require(all((x[0][i] + x[1][i]) % 2 == 0 and + (x[0][i] - x[1][i]) % 2 == 0 for i in deleted), + 'integral fixture sources') + require(any(z1[i] * z2[k] != z2[i] * z1[k] + for i in range(112) for k in range(i + 1, 112)), + 'independent source columns') + d1 = [a + b for a, b in zip(x[0], x[1])] + d2 = [a - b for a, b in zip(x[0], x[1])] + t0 = [a - b - c0 for a, b, c0 in zip(x[0], z1, z2)] + t1 = [a - b + c0 for a, b, c0 in zip(x[1], z1, z2)] + t = [t0, t1] + x[2:] + # The identity is checked entrywise, independently of supports. + for i in range(112): + for k in range(112): + lhs = sum(col[i] * col[k] for col in x) + rhs = sum(col[i] * src[k] for col, src in zip(x, t)) + rhs += d1[i] * z1[k] + d2[i] * z2[k] + require(lhs == rhs, 'full ten-term matrix identity') + require(any(d1[i] * z1[k] for i in range(112) for k in range(112)) + and any(d2[i] * z2[k] for i in range(112) for k in range(112)), + 'either omitted added term changes the matrix') + def beta(reader, source): + rs = [i for i, value in enumerate(reader) if value] + ss = [i for i, value in enumerate(source) if value] + return rank_f2(sum(parity(data['duals'][i] & + data['labels'][k]) << p + for p, k in enumerate(ss)) for i in rs) + costs = [beta(r, s) for r, s in zip(x + [d1, d2], t + [z1, z2])] + return {'source_union_size': len(deleted), 'retained_ranks': costs[:8], + 'added_ranks': costs[8:], 'total_copy_rank': sum(costs)} + + full = evaluate(c) + short = evaluate(c - {min(c)}) + require(full['retained_ranks'] == [7, 7] + [8] * 6 and + short['retained_ranks'] == [8] * 8, 'sharp 24-site boundary') + require(full['total_copy_rank'] >= 64 and + short['total_copy_rank'] >= 64, 'no fixture cost claim') + return {'at_24': full, 'at_23': short} + + +def main(): + parser = argparse.ArgumentParser() + parser.add_argument('--write', type=Path, help='write a new receipt path') + args = parser.parse_args() + check_sources() + data = json.loads((ROOT / 'research/p112-single-lift/reference-geometry.json').read_text()) + check_geometry(data) + geometry_mutation_controls(data) + # Rebuild from the predecessor's exact root-coordinate generator and + # compare every geometry field. No previous cost or proof checker is imported. + geometry_file = ROOT / 'research/p112-single-lift/geometry.py' + spec = importlib.util.spec_from_file_location('p112_reference_geometry', geometry_file) + module = importlib.util.module_from_spec(spec) + spec.loader.exec_module(module) + require(module.build() == data, 'independent geometry reconstruction') + codes, weights = generalized_weights(data) + cuts = cross_reader_cuts(data, codes) + span_census = added_reader_span_census(data) + screen = two_total_small_support_screen() + fixture = two_total_fixture(data, cuts['common_minimum_cuts']['0,1']) + result = {'schema_version': 1, 'base_commit': + 'a18b4b0136d647529971e9fcb99fa83f5b9a0b81', + 'source_geometry_sha256': sha256((ROOT / + 'research/p112-single-lift/reference-geometry.json').read_bytes()).hexdigest(), + 'generalized_weights': weights, 'cross_reader_cuts': cuts, + 'added_reader_span_census': span_census, + 'two_total_small_support_screen': screen, + 'two_total_fixture': fixture} + if args.write: + with args.write.open('x', encoding='utf-8') as out: + json.dump(result, out, sort_keys=True, indent=2) + out.write('\n') + else: + expected = json.loads((HERE / 'RESULT.json').read_text()) + require(result == expected, 'full RESULT.json comparison') + print('PASS_P112_TWO_TOTAL_SUPPORT_THRESHOLD weights=24,36,44,48,52,54,55,56 ' + 'union_floor=43 triple=40 fixture=24 ' + 'controls=source,geometry,omission,one-port-short') + + +if __name__ == '__main__': + main()