diff --git a/research/class-c-dominance-campaign/README.md b/research/class-c-dominance-campaign/README.md new file mode 100644 index 0000000000..8a7702c444 --- /dev/null +++ b/research/class-c-dominance-campaign/README.md @@ -0,0 +1,172 @@ +# Class-C campaign coverage through dimension dominance + +**Scoped correction and conditional scheduling result; no geometric span pass.** +The source tables list particular covers, rather than their full upward closure +in flat dimension. PR #3315's initial audited head `c4fe4244b52bb9111b9117aba066229316fc58ab` +correctly finds a three-configuration literal cover +of the 16 coverable HARD rows. That is not the geometric campaign minimum: +**`6554` at target `T=7`, together with `5555` at `T=8`, would suffice** if both +complete uniform span checks passed. Row 37 remains outside this implication. + +There is also a concrete correction to that head's all-row statement. Its named +literal set `{5544,5555,6554}` covers only **55 of the 64** table-coverable rows, +missing **4,5,6,17,20,28,33,66,69** (zero-based `row_idx`, exactly as in the CSV). +The literal minimum over all 70 source rows is four configurations, versus +three over the HARD subset. Both implementations independently find these +minima. The PR's vendored `rows70.csv` and the original help-package file have +the same Git blob, `ee12fc8e3c528a509a06274c3ed264508c2c06a8`. + +After our advance claim, the author adopted dimension closure at head +`240e7f68c6be0cd7193abdd1d686ec5b90ab5355`, explicitly credited the observation, +and left the same-target substitution lemma as an open premise in the +[correction](https://github.com/CrocSwap/integer-mult-bounds/discussions/2954#discussioncomment-19006436). +This package discharges that implication and retains threshold-aware certificates. +It does not describe the amended checker as still using literal incidence. + +With the proved dimension transfer, **two configurations suffice conditionally +for all 64 table-coverable rows**: `6554@T6` and `5555@T8`. +This does not prove that either requested span bound is true, that a census will +finish, or that this plan is fastest. In particular, a lower target can increase +work or expose a crack; no CPU-hour saving is claimed. + +## Precise implication and proof + +Use the model in [DreamingOfClouds' discussion #2954](https://github.com/CrocSwap/integer-mult-bounds/discussions/2954). +For a binary flat `V` in `F_2^9`, let `Lambda(V)` be the P112 lines whose binary +labels lie in `V`. Thus `V subset W` directly implies `Lambda(V) subset Lambda(W)`. +For four +flats define `X(V)=union_i Lambda(V_i)` and + +``` +H(V) = { h : rank_F2(labels(Off(h) minus X(V))) <= 7 }. +``` + +A complete *uniform* span certificate for dimension tuple `b` at target `T` +means `dim_R span H(W) <= T-1` for **every** four-flat tuple `W` of those +dimensions. It is not a sampled pair, one orbit representative, or one shard. +We inherit the source row/config coverage assertions and Lemma B's implication: +a row with dimension `d` is excluded by such a bound at `T <= d` on a cover of +its required basis. We do not re-prove Lemma B or the original weight census. + +**Extension lemma.** Sort both dimension tuples decreasingly. If `c_i <= b_i` +for all four indices, any tuple `V` of dimensions `c` can be extended, after a +permutation of roles, to `W_i` with `V_i subset W_i` and `dim W_i=b_i`. +All target dimensions are at most six, below the ambient nine. This model has +no requirement that the four flats be mutually disjoint. The union and `H` +are symmetric in the four roles. + +Then `X(V) subset X(W)`. For every direction `h`, its residual labels outside +`X(W)` are a subset of those outside `X(V)`. Removing labels cannot increase +binary rank. Thus **`H(V) subset H(W)`**, and consequently the real span of +`H(V)` has no larger dimension. A uniform target certificate transfers to every +source tuple at the **same** threshold `T`. + +The source's size budget remains explicit: for +`g(1..7)=(1,2,4,8,12,20,36)`, `sum g(6554)=52` and `sum g(5555)=48`. +Both meet the inherited budget `<=52`. The tempting single target `6555` +exceeds it (56). If a future model adds coupled-flat constraints, a particular +prescribed extension, or different access rules, this lemma needs reassessment. + +This proof uses only a listed cover and flat extension; it does **not** require +the unpublished weight-multiset-to-config generator to be complete. The +geometric `s4z.c` consumes directions and flat dimensions, not the row CSVs; +recovering that generator remains a separate question. + +## Exact campaign and source reconciliation + +`RESULT.json` records all 169 ordered comparisons within the 13 listed +configurations, every resulting row incidence, both complete campaign witness +lists, and the exhaustive minimum-cover solutions. In each row witness, the +`source` cover is literally in that row; the `target` dominates it; the target +budget is at most 52; and `threshold <= d`. + +| Target | Literal rows | Rows after dimension transfer | HARD rows after transfer | +|---|---:|---:|---:| +| 6554 | 39 | 62 | 15 | +| 5555 | 21 | 27 | 9 | +| Union | — | 64 | 16 | + +The original #2954 totals are `6554:62`, `5555:27`, `6544:40`, `5554:23`, +`6543:16`. Our closure reproduces **all five**, so their earlier coverage +information retains credit. The new contribution is the explicit implication, +the correction to the recent literal scheduling claim, threshold-aware row +certificates, and independently implemented replay. + +For the HARD table, assign every row except 35 and 37 to `6554@T7`, then row 35 +(`d=8`) to `5555@T8`. For all table-coverable rows, `6554@T6` handles 62 rows; +rows 35 and 45 (`d=8`) go to `5555@T8`. Rows `3,12,24,37,54,61` have no listed +cover and remain unresolved here. No RRC assertion is needed for the all-row +implication. Calling the 17 rows HARD merely preserves the source classification; +its RRC exclusions remain under audit. + +Within this **listed-alphabet dominance model**, two target configurations are +minimal: row 35 can be served only by 5555, and row 36 only by 6554. This is not +a minimum over all geometric proofs, unlisted configurations, or alternative +packing mechanisms. The literal HARD minimum is three, with four different +minimizers, not a unique named triple. + +The target checker argument orders would be `(a,b,c,d)=(4,6,5,5)` for 6554 and +`(5,5,5,5)` for 5555. This package does not launch those expensive campaigns. +Using `T=8` for both fails the required implication on HARD rows 7,8,13, whose +`d=7`; the receipt explicitly rejects that tempting weakening. + +## Reproduction and evidence + +```sh +python3.12 -B research/class-c-dominance-campaign/verify.py +python3.12 -B research/class-c-dominance-campaign/independent.py +python3.12 -B scripts/research_package.py --package research/class-c-dominance-campaign +``` + +Standard library only; each direct check takes less than a second on the local +Mac. `verify.py --write` regenerates the deterministic receipt. Ordinary replay +compares the complete regenerated object to its committed bytes and checks +four rejecting certificate mutants: weaker threshold, false dominance, invented +source cover, and over-budget target. Positive controls retain valid extension +and both admissible target budgets. + +The separately written `independent.py` uses injective permutations of flat +roles, not the primary sorted-coordinate test, and independently enumerates +minimum covers. It compares the complete incidence object and checks both +threshold plans. It shares source data and the stated model; it is not an +independent geometry, RRC, human, or proof-kernel audit. Both scripts use explicit +exceptions, so their acceptance checks remain active under `-O`. + +The two CSVs and help README are verbatim copies from DreamingOfClouds' commit +`1b25759bff5486293a9083ebbe0097b5f6642e08`. Exact original paths, SHA256 and Git +blob IDs are in `SOURCES.json.external_inputs`. Every replay authenticates the +three files. They are external byte pins, not generic runner Git-provenance rows; +the runner separately pins the selected record and originating task card at +main `463113d675af7410ac91d53a4fed51ec6494eb9a`. No pending Git objects are needed +for the direct scripts. + +## Limits and credit + +No actual four-flat span bound, new residue exclusion, exhaustive config-list +completeness, RRC proof, global decoder floor, physical/native consumer, supplier, +new kappa, or selected-frontier update is claimed. The conditional row coverage +and cardinality function are inherited. The full `s4z` campaign, historical +geometry censuses, selected cold replay, Lean and Docker were not run. This +small scheduling audit neither admits nor refutes those mathematical premises. + +Credit **DreamingOfClouds** for the help package, original coverage counts, +geometry, Lemma B/kill criterion, and #2816/#2826/#2862 lineage; +**muatfannajm-dot / PR #3315** for the literal table audit and explicit +completeness handoff; **Tekalign / PR #2975 and #3000** for the separate +requirement and mask-filter accelerations; and the retained source contributors. +Written by **Krzysztof Wojt with substantial OpenAI Codex assistance**, including +Luna agents for source/overlap extraction and the separate combinatorial check. +Apache-2.0; original input attribution is retained. + +## Open next questions + +1. Can either required uniform span bound actually be proved or falsified? + Start with a bounded exact witness search for 6554 at T=7 (T=6 for all rows) + and 5555 at T=8; stop at a real crack before proposing a full campaign. + Geometry and direction-list completeness remain separate inherited premises. +2. What exact rule generated the sparse row/config incidence list? + Obtain its original generator and test completeness; `s4z.c` does not contain + that row-weight rule. This package only closes the missing monotone implication. +3. Does a smaller target at a weaker permitted threshold cost less in practice? + Compare bounded identical slices with exact coverage preserved. Two target + configurations alone do not prove a runtime advantage over three. diff --git a/research/class-c-dominance-campaign/RESULT.json b/research/class-c-dominance-campaign/RESULT.json new file mode 100644 index 0000000000..edd95e5c7a --- /dev/null +++ b/research/class-c-dominance-campaign/RESULT.json @@ -0,0 +1,1100 @@ +{ + "all_campaign": { + "targets": [ + [ + "6554", + 6 + ], + [ + "5555", + 8 + ] + ], + "uncovered": [ + 3, + 12, + 24, + 37, + 54, + 61 + ], + "witnesses": [ + { + "d": 6, + "row": 0, + "source": "5544", + "target": "6554", + "threshold": 6 + }, + { + "d": 6, + "row": 1, + "source": "6444", + "target": "6554", + "threshold": 6 + }, + { + "d": 6, + "row": 2, + "source": "6543", + "target": "6554", + "threshold": 6 + }, + { + "d": 6, + "row": 4, + "source": "6443", + "target": "6554", + "threshold": 6 + }, + { + "d": 6, + "row": 5, + "source": "6533", + "target": "6554", + "threshold": 6 + }, + { + "d": 7, + "row": 6, + "source": "6443", + "target": "6554", + "threshold": 6 + }, + { + "d": 7, + "row": 7, + "source": "5554", + "target": "6554", + "threshold": 6 + }, + { + "d": 7, + "row": 8, + "source": "6544", + "target": "6554", + "threshold": 6 + }, + { + "d": 7, + "row": 9, + "source": "6544", + "target": "6554", + "threshold": 6 + }, + { + "d": 7, + "row": 10, + "source": "6544", + "target": "6554", + "threshold": 6 + }, + { + "d": 7, + "row": 11, + "source": "6553", + "target": "6554", + "threshold": 6 + }, + { + "d": 7, + "row": 13, + "source": "5544", + "target": "6554", + "threshold": 6 + }, + { + "d": 7, + "row": 14, + "source": "5544", + "target": "6554", + "threshold": 6 + }, + { + "d": 7, + "row": 15, + "source": "5544", + "target": "6554", + "threshold": 6 + }, + { + "d": 7, + "row": 16, + "source": "5553", + "target": "6554", + "threshold": 6 + }, + { + "d": 7, + "row": 17, + "source": "6444", + "target": "6554", + "threshold": 6 + }, + { + "d": 7, + "row": 18, + "source": "6444", + "target": "6554", + "threshold": 6 + }, + { + "d": 7, + "row": 19, + "source": "6543", + "target": "6554", + "threshold": 6 + }, + { + "d": 7, + "row": 20, + "source": "6443", + "target": "6554", + "threshold": 6 + }, + { + "d": 8, + "row": 21, + "source": "5554", + "target": "6554", + "threshold": 6 + }, + { + "d": 8, + "row": 22, + "source": "6544", + "target": "6554", + "threshold": 6 + }, + { + "d": 8, + "row": 23, + "source": "6553", + "target": "6554", + "threshold": 6 + }, + { + "d": 8, + "row": 25, + "source": "5554", + "target": "6554", + "threshold": 6 + }, + { + "d": 8, + "row": 26, + "source": "5544", + "target": "6554", + "threshold": 6 + }, + { + "d": 8, + "row": 27, + "source": "5553", + "target": "6554", + "threshold": 6 + }, + { + "d": 8, + "row": 28, + "source": "6444", + "target": "6554", + "threshold": 6 + }, + { + "d": 8, + "row": 29, + "source": "6444", + "target": "6554", + "threshold": 6 + }, + { + "d": 8, + "row": 30, + "source": "6543", + "target": "6554", + "threshold": 6 + }, + { + "d": 8, + "row": 31, + "source": "5444", + "target": "6554", + "threshold": 6 + }, + { + "d": 8, + "row": 32, + "source": "5543", + "target": "6554", + "threshold": 6 + }, + { + "d": 8, + "row": 33, + "source": "6443", + "target": "6554", + "threshold": 6 + }, + { + "d": 8, + "row": 34, + "source": "6554", + "target": "6554", + "threshold": 6 + }, + { + "d": 8, + "row": 35, + "source": "5555", + "target": "5555", + "threshold": 8 + }, + { + "d": 8, + "row": 36, + "source": "6554", + "target": "6554", + "threshold": 6 + }, + { + "d": 8, + "row": 38, + "source": "6554", + "target": "6554", + "threshold": 6 + }, + { + "d": 8, + "row": 39, + "source": "6554", + "target": "6554", + "threshold": 6 + }, + { + "d": 8, + "row": 40, + "source": "6554", + "target": "6554", + "threshold": 6 + }, + { + "d": 8, + "row": 41, + "source": "6554", + "target": "6554", + "threshold": 6 + }, + { + "d": 8, + "row": 42, + "source": "6554", + "target": "6554", + "threshold": 6 + }, + { + "d": 8, + "row": 43, + "source": "6554", + "target": "6554", + "threshold": 6 + }, + { + "d": 8, + "row": 44, + "source": "6554", + "target": "6554", + "threshold": 6 + }, + { + "d": 8, + "row": 45, + "source": "5555", + "target": "5555", + "threshold": 8 + }, + { + "d": 8, + "row": 46, + "source": "5554", + "target": "6554", + "threshold": 6 + }, + { + "d": 8, + "row": 47, + "source": "6544", + "target": "6554", + "threshold": 6 + }, + { + "d": 8, + "row": 48, + "source": "5554", + "target": "6554", + "threshold": 6 + }, + { + "d": 8, + "row": 49, + "source": "5554", + "target": "6554", + "threshold": 6 + }, + { + "d": 8, + "row": 50, + "source": "5554", + "target": "6554", + "threshold": 6 + }, + { + "d": 8, + "row": 51, + "source": "5554", + "target": "6554", + "threshold": 6 + }, + { + "d": 8, + "row": 52, + "source": "5554", + "target": "6554", + "threshold": 6 + }, + { + "d": 8, + "row": 53, + "source": "5554", + "target": "6554", + "threshold": 6 + }, + { + "d": 8, + "row": 55, + "source": "6544", + "target": "6554", + "threshold": 6 + }, + { + "d": 8, + "row": 56, + "source": "6544", + "target": "6554", + "threshold": 6 + }, + { + "d": 8, + "row": 57, + "source": "6544", + "target": "6554", + "threshold": 6 + }, + { + "d": 8, + "row": 58, + "source": "6544", + "target": "6554", + "threshold": 6 + }, + { + "d": 8, + "row": 59, + "source": "6544", + "target": "6554", + "threshold": 6 + }, + { + "d": 8, + "row": 60, + "source": "6553", + "target": "6554", + "threshold": 6 + }, + { + "d": 8, + "row": 62, + "source": "5544", + "target": "6554", + "threshold": 6 + }, + { + "d": 8, + "row": 63, + "source": "5544", + "target": "6554", + "threshold": 6 + }, + { + "d": 8, + "row": 64, + "source": "5544", + "target": "6554", + "threshold": 6 + }, + { + "d": 8, + "row": 65, + "source": "5553", + "target": "6554", + "threshold": 6 + }, + { + "d": 8, + "row": 66, + "source": "6444", + "target": "6554", + "threshold": 6 + }, + { + "d": 8, + "row": 67, + "source": "6444", + "target": "6554", + "threshold": 6 + }, + { + "d": 8, + "row": 68, + "source": "6543", + "target": "6554", + "threshold": 6 + }, + { + "d": 8, + "row": 69, + "source": "6443", + "target": "6554", + "threshold": 6 + } + ] + }, + "claimed_three_literal_misses": [ + 4, + 5, + 6, + 17, + 20, + 28, + 33, + 66, + 69 + ], + "coverage": { + "cover_all": { + "5444": [ + 31 + ], + "5543": [ + 32 + ], + "5544": [ + 0, + 13, + 14, + 15, + 26, + 31, + 32, + 62, + 63, + 64 + ], + "5553": [ + 14, + 16, + 27, + 32, + 63, + 65 + ], + "5554": [ + 0, + 7, + 13, + 14, + 15, + 16, + 21, + 25, + 26, + 27, + 31, + 32, + 46, + 48, + 49, + 50, + 51, + 52, + 53, + 62, + 63, + 64, + 65 + ], + "5555": [ + 0, + 7, + 13, + 14, + 15, + 16, + 21, + 25, + 26, + 27, + 31, + 32, + 34, + 35, + 44, + 45, + 46, + 48, + 49, + 50, + 51, + 52, + 53, + 62, + 63, + 64, + 65 + ], + "6443": [ + 4, + 6, + 20, + 33, + 69 + ], + "6444": [ + 1, + 4, + 6, + 13, + 17, + 18, + 20, + 28, + 29, + 31, + 33, + 62, + 66, + 67, + 69 + ], + "6533": [ + 5 + ], + "6543": [ + 2, + 4, + 5, + 6, + 14, + 17, + 19, + 20, + 28, + 30, + 32, + 33, + 63, + 66, + 68, + 69 + ], + "6544": [ + 0, + 1, + 2, + 4, + 5, + 6, + 8, + 9, + 10, + 13, + 14, + 15, + 17, + 18, + 19, + 20, + 22, + 26, + 28, + 29, + 30, + 31, + 32, + 33, + 46, + 47, + 48, + 50, + 55, + 56, + 57, + 58, + 59, + 62, + 63, + 64, + 66, + 67, + 68, + 69 + ], + "6553": [ + 2, + 4, + 5, + 6, + 9, + 11, + 14, + 16, + 17, + 19, + 20, + 23, + 27, + 28, + 30, + 32, + 33, + 48, + 49, + 52, + 55, + 58, + 60, + 63, + 65, + 66, + 68, + 69 + ], + "6554": [ + 0, + 1, + 2, + 4, + 5, + 6, + 7, + 8, + 9, + 10, + 11, + 13, + 14, + 15, + 16, + 17, + 18, + 19, + 20, + 21, + 22, + 23, + 25, + 26, + 27, + 28, + 29, + 30, + 31, + 32, + 33, + 34, + 36, + 38, + 39, + 40, + 41, + 42, + 43, + 44, + 46, + 47, + 48, + 49, + 50, + 51, + 52, + 53, + 55, + 56, + 57, + 58, + 59, + 60, + 62, + 63, + 64, + 65, + 66, + 67, + 68, + 69 + ] + }, + "cover_hard": { + "5444": [], + "5543": [], + "5544": [ + 13, + 62 + ], + "5553": [], + "5554": [ + 7, + 13, + 21, + 46, + 50, + 53, + 62 + ], + "5555": [ + 7, + 13, + 21, + 34, + 35, + 46, + 50, + 53, + 62 + ], + "6443": [], + "6444": [ + 13, + 62 + ], + "6533": [], + "6543": [], + "6544": [ + 8, + 13, + 46, + 47, + 50, + 57, + 62 + ], + "6553": [], + "6554": [ + 7, + 8, + 13, + 21, + 34, + 36, + 40, + 42, + 43, + 46, + 47, + 50, + 53, + 57, + 62 + ] + }, + "dominance": { + "5444": [ + "5444" + ], + "5543": [ + "5543" + ], + "5544": [ + "5444", + "5543", + "5544" + ], + "5553": [ + "5543", + "5553" + ], + "5554": [ + "5444", + "5543", + "5544", + "5553", + "5554" + ], + "5555": [ + "5444", + "5543", + "5544", + "5553", + "5554", + "5555" + ], + "6443": [ + "6443" + ], + "6444": [ + "5444", + "6443", + "6444" + ], + "6533": [ + "6533" + ], + "6543": [ + "5543", + "6443", + "6533", + "6543" + ], + "6544": [ + "5444", + "5543", + "5544", + "6443", + "6444", + "6533", + "6543", + "6544" + ], + "6553": [ + "5543", + "5553", + "6443", + "6533", + "6543", + "6553" + ], + "6554": [ + "5444", + "5543", + "5544", + "5553", + "5554", + "6443", + "6444", + "6533", + "6543", + "6544", + "6553", + "6554" + ] + } + }, + "dominance_minimum_all": { + "size": 2, + "solutions": [ + [ + "5555", + "6554" + ] + ] + }, + "dominance_minimum_hard": { + "size": 2, + "solutions": [ + [ + "5555", + "6554" + ] + ] + }, + "hard_campaign": { + "targets": [ + [ + "6554", + 7 + ], + [ + "5555", + 8 + ] + ], + "uncovered": [ + 37 + ], + "witnesses": [ + { + "d": 7, + "row": 7, + "source": "5554", + "target": "6554", + "threshold": 7 + }, + { + "d": 7, + "row": 8, + "source": "6544", + "target": "6554", + "threshold": 7 + }, + { + "d": 7, + "row": 13, + "source": "5544", + "target": "6554", + "threshold": 7 + }, + { + "d": 8, + "row": 21, + "source": "5554", + "target": "6554", + "threshold": 7 + }, + { + "d": 8, + "row": 34, + "source": "6554", + "target": "6554", + "threshold": 7 + }, + { + "d": 8, + "row": 35, + "source": "5555", + "target": "5555", + "threshold": 8 + }, + { + "d": 8, + "row": 36, + "source": "6554", + "target": "6554", + "threshold": 7 + }, + { + "d": 8, + "row": 40, + "source": "6554", + "target": "6554", + "threshold": 7 + }, + { + "d": 8, + "row": 42, + "source": "6554", + "target": "6554", + "threshold": 7 + }, + { + "d": 8, + "row": 43, + "source": "6554", + "target": "6554", + "threshold": 7 + }, + { + "d": 8, + "row": 46, + "source": "5554", + "target": "6554", + "threshold": 7 + }, + { + "d": 8, + "row": 47, + "source": "6544", + "target": "6554", + "threshold": 7 + }, + { + "d": 8, + "row": 50, + "source": "5554", + "target": "6554", + "threshold": 7 + }, + { + "d": 8, + "row": 53, + "source": "5554", + "target": "6554", + "threshold": 7 + }, + { + "d": 8, + "row": 57, + "source": "6544", + "target": "6554", + "threshold": 7 + }, + { + "d": 8, + "row": 62, + "source": "5544", + "target": "6554", + "threshold": 7 + } + ] + }, + "literal_minimum_all": { + "size": 4, + "solutions": [ + [ + "5544", + "5555", + "6543", + "6554" + ], + [ + "5544", + "5555", + "6544", + "6554" + ], + [ + "5554", + "5555", + "6543", + "6554" + ], + [ + "5555", + "6444", + "6543", + "6554" + ] + ] + }, + "literal_minimum_hard": { + "size": 3, + "solutions": [ + [ + "5544", + "5555", + "6554" + ], + [ + "5554", + "5555", + "6554" + ], + [ + "5555", + "6444", + "6554" + ], + [ + "5555", + "6544", + "6554" + ] + ] + }, + "schema_version": 1, + "scope": "conditional scheduling implication; no geometric span pass or new exclusion", + "source_sha256": { + "help-README.md": "aba39c91e262edfb495cf1ccaf7c7555199ee9c0b87e99ecd22e4f1bb14c292f", + "rows17.csv": "9ebe7fc1ecd74148e7bdefa1f6bb2ed00551884b1a4a6558d7f129f7eef4efd5", + "rows70.csv": "c0eb6bb88498bf39a8b2020b1d0d600181f6e13eb9dd6a6e5f90794f0895754a" + } +} diff --git a/research/class-c-dominance-campaign/SOURCES.json b/research/class-c-dominance-campaign/SOURCES.json new file mode 100644 index 0000000000..b744583272 --- /dev/null +++ b/research/class-c-dominance-campaign/SOURCES.json @@ -0,0 +1,47 @@ +{ + "schema_version": 1, + "base_commit": "463113d675af7410ac91d53a4fed51ec6494eb9a", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5", + "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0" + } + ], + "external_inputs": [ + { + "path": "research/class-c-dominance-campaign/inputs/rows70.csv", + "repository": "DreamingOfClouds/integer-mult-bounds", + "commit": "1b25759bff5486293a9083ebbe0097b5f6642e08", + "original_path": "research/k2-class-c-help/rows70.csv", + "git_blob": "ee12fc8e3c528a509a06274c3ed264508c2c06a8", + "sha256": "c0eb6bb88498bf39a8b2020b1d0d600181f6e13eb9dd6a6e5f90794f0895754a", + "verification": "Verbatim bytes authenticated in verify.py; source blob read back through GitHub. External input, not a generic Git-provenance pin." + }, + { + "path": "research/class-c-dominance-campaign/inputs/rows17.csv", + "repository": "DreamingOfClouds/integer-mult-bounds", + "commit": "1b25759bff5486293a9083ebbe0097b5f6642e08", + "original_path": "research/k2-class-c-help/rows17.csv", + "git_blob": "ef453f30c2ccd567214ce5487fad51a9c7609390", + "sha256": "9ebe7fc1ecd74148e7bdefa1f6bb2ed00551884b1a4a6558d7f129f7eef4efd5", + "verification": "Verbatim bytes authenticated in verify.py; source blob read back through GitHub. External input, not a generic Git-provenance pin." + }, + { + "path": "research/class-c-dominance-campaign/inputs/help-README.md", + "repository": "DreamingOfClouds/integer-mult-bounds", + "commit": "1b25759bff5486293a9083ebbe0097b5f6642e08", + "original_path": "research/k2-class-c-help/README.md", + "git_blob": "7d8337893059adfe2979847e7b641ef8623b7401", + "sha256": "aba39c91e262edfb495cf1ccaf7c7555199ee9c0b87e99ecd22e4f1bb14c292f", + "verification": "Verbatim bytes authenticated in verify.py; source blob read back through GitHub. External input, not a generic Git-provenance pin." + } + ] +} diff --git a/research/class-c-dominance-campaign/TASK.json b/research/class-c-dominance-campaign/TASK.json new file mode 100644 index 0000000000..075770318e --- /dev/null +++ b/research/class-c-dominance-campaign/TASK.json @@ -0,0 +1,117 @@ +{ + "schema_version": 1, + "task_id": "census-pruning-audit", + "priority_revision": 6, + "base_commit": "463113d675af7410ac91d53a4fed51ec6494eb9a", + "original_card": { + "id": "census-pruning-audit", + "question": "Does the reported word-census parity-pruning error invalidate a specific exclusion we still rely on, and what bounded repair is justified?", + "starting_points": [ + "research/f7-weight-parity-census-correction/README.md", + "docs/research/research-family-status.md" + ], + "methods": [ + "Independently reconstruct the tiny counterexample and trace one affected exclusion to its exact pruning code.", + "Compare corrected and unpruned enumeration on a small exhaustive domain, then audit the changed pruning implication." + ], + "acceptance_gate": "Pin the old and proposed corrected engines, distinguish a disproved pruning rule from a disproved final bound, and state exactly which downstream exclusions need revalidation. #2973 is an author-checked source archive; neither its new f(7) claim nor all old conclusions are automatically accepted or rejected.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read #2973 error description and MATH.md; manually reconstruct the prefix states of 01021323 before running any large census.", + "scope": "Source-binding orientation only; no full enumeration or mathematical validation." + }, + "first_experiment": "Reconstruct the eight prefix states of 01021323 and compare bit-0 versus Hamming-weight parity budgets independently. Trace the reported false prune to one pinned predecessor (#2542, #2634 or #2691), then test a small exhaustive domain. Stop after a source-impact handoff or corrected-prune proof; a full seven-label replay needs a separate resource budget and a named research decision it can change.", + "bottleneck_link": "An unsound exclusion can wrongly close a mechanism; correcting its dependency boundary is more useful than extending the same census.", + "allowed_variations": [ + "One predecessor pruning rule, one independently exhaustive small domain, or one downstream dependency audit." + ], + "scope_change_triggers": [ + "Launching a larger census before validating the prune and explaining which active decision it changes.", + "Treating a small-domain counterexample to the old rule as a counterexample to every reported seven-label bound." + ], + "overlap_terms": [ + "2973", + "2542", + "2634", + "2691", + "weight parity", + "bit-0", + "01021323", + "census pruning" + ] + }, + "scope_status": "changed", + "actual_scope": "Prove dimension-dominance transfer for the class-C four-flat campaign, correct literal all-row coverage, and certify threshold-aware two-target schedules.", + "scope_change_reason": "Handoff-first choice of PR3315 question 1 on Discussion2954; this is a census scheduling implication, not the original parity-pruning mechanism. The original row generator is unavailable, so the scope closes monotone transfer from already-listed covers without claiming list completeness.", + "bottleneck_link": "Avoid unsupported campaign coverage claims and redundant four-flat proof obligations before expensive class-C decoder searches; no supplier or exponent improvement is asserted.", + "budget_minutes": 60, + "stop_rule": "Stop after the same-threshold implication, exact row certificates and controls; no geometric census or dependent construction expansion.", + "outcome": "completed", + "evidence": "README proof; RESULT.json complete incidence, minimum-cover and per-row certificates; verify.py and separately implemented independent.py; explicit rejection controls.", + "author": "Krzysztof Wojt", + "ai_assistance": "Substantial OpenAI Codex assistance. Luna agents supported read-only overlap/source extraction and independently implemented the combinatorial checker. No human or proof-kernel review is claimed.", + "open_questions": [ + { + "question": "Can the required uniform span bounds be proved or falsified?", + "why_it_matters": "Only an actual span certificate can exclude a row.", + "first_step": "Bounded exact witness search for 6554@T7 or 5555@T8, with the full model preserved.", + "blocked_by": "No geometric span pass is provided; full campaign cost and source model admission remain separate." + }, + { + "question": "What generated the sparse row/config table?", + "why_it_matters": "Dominance closure does not establish completeness of the original packing predicate.", + "first_step": "Obtain and pin the original weight-multiset generator; compare it to rows70.csv.", + "blocked_by": "The generator is absent from the help package; s4z.c consumes directions, not weights." + }, + { + "question": "Which threshold-aware campaign is actually fastest?", + "why_it_matters": "A smaller number of configurations need not reduce compute cost.", + "first_step": "Compare bounded exact slices for the same covered rows and thresholds.", + "blocked_by": "No runtime or full-campaign performance experiment has been conducted." + } + ], + "coordination": { + "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/2954#discussioncomment-19006125", + "overlap": { + "open_prs": 370, + "open_prs_at": "2026-10-17T21:46:13.187031+00:00", + "discussion_records": 2112, + "discussions_at": "2026-10-17T21:48:07.624956+00:00", + "complete_pagination": true, + "limits": "No arbitrary diff or unpublished-work coverage; sparse local checkout and no closed-PR remote snapshot." + }, + "predecessor_pr": 3315, + "predecessor_head": "c4fe4244b52bb9111b9117aba066229316fc58ab", + "predecessor_refreshed_head": "240e7f68c6be0cd7193abdd1d686ec5b90ab5355", + "predecessor_correction": "https://github.com/CrocSwap/integer-mult-bounds/discussions/2954#discussioncomment-19006436", + "predecessor_change": "Author adopted the dominance observation after our claim and explicitly left the same-target substitution lemma open. This package supplies that implication; initial literal arithmetic is historical.", + "submission_overlap": { + "open_prs": { + "fetched_at": "2026-10-17T21:59:37.877947+00:00", + "complete_pagination": true, + "records": 248 + }, + "discussions": { + "fetched_at": "2026-10-17T22:01:04.820007+00:00", + "complete_pagination": true, + "records": 2170 + }, + "warnings": [] + }, + "submission_main": "b0186c6b75280913969f101c169fe3fb07afd137", + "submission_guidance": "Priority revision 6 and selected record unchanged. Read changed P104 navigation in current-priorities.md; unrelated to this class-C scope. New source-history publication preflight is optional; direct exported replay is self-contained." + }, + "verification": { + "python": "3.12.12 (main, Oct 9 2025, 11:07:00) [Clang 17.0.0 (clang-1700.4.4.1)]", + "platform": "macOS-26.5.2-arm64-arm-64bit", + "registered_replay": "PASS_REGISTERED_RESEARCH_PACKAGE research/class-c-dominance-campaign outcome=completed", + "commit_byte_check": "PASS at e7269dbed047ad6ac89c1642db18ee3413a85a09, 10 files; final publication bytes will be rechecked", + "optimized_direct_scripts": "Both passed under Python3.12 -O -B", + "internal_review": "A separate Luna task reviewed the actual README proof, both checkers, RESULT and pinned inputs; reran both optimized scripts and found no blocking mismatch. Its Lambda-inclusion clarification was incorporated. This is internal AI review, not independent human, geometry or proof-kernel validation." + } +} diff --git a/research/class-c-dominance-campaign/VERIFY.json b/research/class-c-dominance-campaign/VERIFY.json new file mode 100644 index 0000000000..b148abaa88 --- /dev/null +++ b/research/class-c-dominance-campaign/VERIFY.json @@ -0,0 +1,31 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/class-c-dominance-campaign/inputs/rows70.csv", + "research/class-c-dominance-campaign/inputs/rows17.csv", + "research/class-c-dominance-campaign/inputs/help-README.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 30, + "checks": "Exact full source-bound dominance and threshold certificates, literal minima, and four rejecting certificate mutants." + }, + { + "argv": [ + "{python}", + "-B", + "{package}/independent.py" + ], + "timeout_seconds": 30, + "checks": "Separately implemented injective-role matching, all incidence comparisons, exhaustive minimum covers and threshold controls." + } + ] +} diff --git a/research/class-c-dominance-campaign/independent.py b/research/class-c-dominance-campaign/independent.py new file mode 100644 index 0000000000..bc7a2237f8 --- /dev/null +++ b/research/class-c-dominance-campaign/independent.py @@ -0,0 +1,340 @@ +#!/usr/bin/env python3 +"""Independent dimension-dominance and threshold audit for the Class-C tables. + +This checker reads the two pinned CSV inputs directly. It does not import the +package's primary verifier or reproduce the underlying E8/P112 geometry. +""" + +from __future__ import annotations + +import csv +import hashlib +import itertools +import json +import re +import sys +from dataclasses import dataclass +from io import StringIO +from pathlib import Path +from typing import Any + + +PACKAGE = Path(__file__).resolve().parent +EXPECTED_HASHES = { + "rows70.csv": "c0eb6bb88498bf39a8b2020b1d0d600181f6e13eb9dd6a6e5f90794f0895754a", + "rows17.csv": "9ebe7fc1ecd74148e7bdefa1f6bb2ed00551884b1a4a6558d7f129f7eef4efd5", +} +EXPECTED_TABLE_COVERABLE = {"rows70.csv": 64, "rows17.csv": 16} +EXPECTED_HARD_T8_FAILURES = {7, 8, 13} + + +class CheckFailure(Exception): + """A failed data, consistency, or expected-result check.""" + + +def require(condition: bool, message: str) -> None: + if not condition: + raise CheckFailure(message) + + +@dataclass(frozen=True) +class Row: + row_idx: int | str + depth: int + configs: tuple[str, ...] + + +def normalized_header(value: str) -> str: + return re.sub(r"[^a-z0-9]+", "_", value.strip().lower()).strip("_") + + +def choose_column(headers: list[str], aliases: tuple[str, ...], pattern: str) -> str: + by_normalized = {normalized_header(name): name for name in headers} + for alias in aliases: + if alias in by_normalized: + return by_normalized[alias] + candidates = [name for name in headers if re.search(pattern, normalized_header(name))] + if len(candidates) == 1: + return candidates[0] + raise CheckFailure( + "cannot identify CSV column; headers=" + repr(headers) + "; candidates=" + repr(candidates) + ) + + +def parse_row_id(value: str) -> int | str: + cleaned = value.strip() + if re.fullmatch(r"-?\d+", cleaned): + return int(cleaned) + if not cleaned: + raise CheckFailure("empty row index in CSV") + return cleaned + + +def row_id_sort_key(value: int | str) -> tuple[int, int | str]: + if isinstance(value, int): + return (0, value) + return (1, value) + + +def parse_configs(value: str) -> tuple[str, ...]: + text = value.strip() + if not text or text.lower() in {"none", "null", "n/a", "-", "[]"}: + return () + + found = re.findall(r"(? list[Row]: + try: + content = raw.decode("utf-8-sig") + except UnicodeDecodeError as error: + raise CheckFailure(f"{path.name} is not UTF-8: {error}") from error + reader = csv.DictReader(StringIO(content)) + headers = reader.fieldnames + require(headers is not None and len(headers) > 0, f"{path.name} has no CSV header") + + id_column = choose_column( + headers, + ("row_idx", "row_id", "row", "id", "index"), + r"(^|_)(row|idx|index|id)($|_)", + ) + depth_column = choose_column(headers, ("d", "dimension_d", "d_value"), r"(^|_)d($|_)|dimension") + config_column = choose_column( + headers, + ("configs", "covering_configs", "covering_4flat_configs", "configurations"), + r"config", + ) + + rows: list[Row] = [] + for line_number, record in enumerate(reader, start=2): + if not record or all(value is None or not value.strip() for value in record.values()): + continue + try: + depth = int((record.get(depth_column) or "").strip()) + except ValueError as error: + raise CheckFailure(f"{path.name}:{line_number}: invalid d value") from error + rows.append( + Row( + row_idx=parse_row_id(record.get(id_column) or ""), + depth=depth, + configs=parse_configs(record.get(config_column) or ""), + ) + ) + + ids = [row.row_idx for row in rows] + require(len(ids) == len(set(ids)), f"{path.name} contains duplicate row indices") + return rows + + +def config_dimensions(config: str) -> tuple[int, ...]: + require(bool(re.fullmatch(r"[1-7]{4}", config)), f"invalid config label {config!r}") + return tuple(int(value) for value in config) + + +def injectively_dominates(larger: str, smaller: str) -> bool: + """Test role matching by trying every injection of smaller roles into larger.""" + large_roles = config_dimensions(larger) + small_roles = config_dimensions(smaller) + if len(small_roles) > len(large_roles): + return False + for assigned_positions in itertools.permutations(range(len(large_roles)), len(small_roles)): + if all(small_roles[index] <= large_roles[position] for index, position in enumerate(assigned_positions)): + return True + return False + + +def check_rows_are_consistent(rows70: list[Row], rows17: list[Row]) -> None: + all_by_id = {row.row_idx: row for row in rows70} + for row in rows17: + require(row.row_idx in all_by_id, f"hard row {row.row_idx!r} is absent from rows70.csv") + full = all_by_id[row.row_idx] + require( + (row.depth, row.configs) == (full.depth, full.configs), + f"hard row {row.row_idx!r} differs between the two input tables", + ) + + +def make_coverage(rows70: list[Row], rows17: list[Row]) -> tuple[dict[str, Any], list[str]]: + configs = sorted({config for row in rows70 for config in row.configs}) + require(len(configs) == 13, f"expected 13 distinct configs, found {len(configs)}: {configs}") + require(all(config in configs for row in rows17 for config in row.configs), "rows17 has a config absent from rows70") + + # Ordered target/source comparisons. A target includes itself through the + # non-strict, injective role relation. + dominance: dict[str, list[str]] = {} + for target in configs: + dominance[target] = sorted( + source for source in configs if injectively_dominates(target, source) + ) + + def rows_covered(rows: list[Row], target: str) -> list[int | str]: + dominated_sources = set(dominance[target]) + return sorted( + (row.row_idx for row in rows if dominated_sources.intersection(row.configs)), + key=row_id_sort_key, + ) + + coverage: dict[str, Any] = { + "dominance": dominance, + "cover_all": {target: rows_covered(rows70, target) for target in configs}, + "cover_hard": {target: rows_covered(rows17, target) for target in configs}, + } + return coverage, configs + + +def literal_coverage(rows: list[Row], configs: list[str]) -> dict[str, set[int | str]]: + return {config: {row.row_idx for row in rows if config in row.configs} for config in configs} + + +def exhaustive_min_covers( + rows: list[Row], configs: list[str], cover_map: dict[str, set[int | str]] +) -> tuple[int, list[tuple[str, ...]], int]: + targets = {row.row_idx for row in rows if row.configs} + require(bool(targets), "no table-coverable rows in minimum-cover calculation") + for size in range(1, len(configs) + 1): + winners: list[tuple[str, ...]] = [] + for selection in itertools.combinations(configs, size): + covered: set[int | str] = set() + for config in selection: + covered.update(cover_map[config]) + if targets <= covered: + winners.append(selection) + if winners: + return size, winners, len(targets) + raise CheckFailure("no cover found from the complete config alphabet") + + +def threshold_coverage( + rows: list[Row], target: str, threshold: int, dominance: dict[str, list[str]] +) -> set[int | str]: + # A pass at T yields span <= T-1; to kill a row with dimension d one needs + # T-1 <= d-1, hence T <= d. Using T >= d reverses the implication. + dominated_sources = set(dominance[target]) + return { + row.row_idx + for row in rows + if threshold <= row.depth and dominated_sources.intersection(row.configs) + } + + +def compare_result(actual: dict[str, Any], result_path: Path) -> None: + try: + result = json.loads(result_path.read_text(encoding="utf-8")) + except FileNotFoundError as error: + raise CheckFailure(f"missing expected result file: {result_path}") from error + except json.JSONDecodeError as error: + raise CheckFailure(f"invalid JSON in {result_path}: {error}") from error + expected = result.get("coverage") + require(isinstance(expected, dict), "RESULT.json must contain an object at ['coverage']") + if actual != expected: + mismatch = { + key: {"expected": expected.get(key), "actual": actual.get(key)} + for key in sorted(set(expected) | set(actual)) + if expected.get(key) != actual.get(key) + } + raise CheckFailure("independent coverage differs from RESULT.json: " + json.dumps(mismatch, sort_keys=True)) + + +def main() -> int: + input_dir = PACKAGE / "inputs" + raw_inputs: dict[str, bytes] = {} + for name, expected_hash in EXPECTED_HASHES.items(): + path = input_dir / name + try: + raw = path.read_bytes() + except FileNotFoundError as error: + raise CheckFailure(f"missing pinned input: {path}") from error + actual_hash = hashlib.sha256(raw).hexdigest() + require(actual_hash == expected_hash, f"{name} SHA256 mismatch: {actual_hash}") + raw_inputs[name] = raw + + rows70 = read_rows(input_dir / "rows70.csv", raw_inputs["rows70.csv"]) + rows17 = read_rows(input_dir / "rows17.csv", raw_inputs["rows17.csv"]) + require(len(rows70) == 70, f"expected 70 rows in rows70.csv, found {len(rows70)}") + require(len(rows17) == 17, f"expected 17 rows in rows17.csv, found {len(rows17)}") + check_rows_are_consistent(rows70, rows17) + + coverage, configs = make_coverage(rows70, rows17) + compare_result(coverage, PACKAGE / "RESULT.json") + + hard_coverable = [row for row in rows17 if row.configs] + all_coverable = [row for row in rows70 if row.configs] + require( + len(hard_coverable) == EXPECTED_TABLE_COVERABLE["rows17.csv"], + f"expected 16 table-coverable hard rows, found {len(hard_coverable)}", + ) + require( + len(all_coverable) == EXPECTED_TABLE_COVERABLE["rows70.csv"], + f"expected 64 table-coverable rows, found {len(all_coverable)}", + ) + + expected_minima = {"rows70": (4, 2), "rows17": (3, 2)} + for label, rows in (("rows70", rows70), ("rows17", rows17)): + literal_min, literal_solutions, count = exhaustive_min_covers( + rows, configs, literal_coverage(rows, configs) + ) + dominance_cover_map = { + config: set(coverage["cover_all" if label == "rows70" else "cover_hard"][config]) + for config in configs + } + dominance_min, dominance_solutions, dominance_count = exhaustive_min_covers( + rows, configs, dominance_cover_map + ) + require(count == dominance_count, f"coverable-row count differs for {label}") + require( + (literal_min, dominance_min) == expected_minima[label], + f"expected literal/dominance minima {expected_minima[label]} for {label}, " + f"got {literal_min}/{dominance_min}", + ) + print( + f"{label}: coverable={count}, literal_min={literal_min}, " + f"dominance_min={dominance_min}, example_dominance_cover={dominance_solutions[0]}" + ) + if not literal_solutions or not dominance_solutions: + raise CheckFailure(f"missing exhaustive minimum-cover witness for {label}") + + hard_ids = {row.row_idx for row in hard_coverable} + all_ids = {row.row_idx for row in all_coverable} + hard_plan = threshold_coverage(rows17, "6554", 7, coverage["dominance"]) | threshold_coverage( + rows17, "5555", 8, coverage["dominance"] + ) + all_plan = threshold_coverage(rows70, "6554", 6, coverage["dominance"]) | threshold_coverage( + rows70, "5555", 8, coverage["dominance"] + ) + require(hard_plan == hard_ids, f"6554@T7 + 5555@T8 misses/adds hard rows: {sorted(hard_ids ^ hard_plan, key=row_id_sort_key)}") + require(all_plan == all_ids, f"6554@T6 + 5555@T8 misses/adds rows: {sorted(all_ids ^ all_plan, key=row_id_sort_key)}") + + t8_only = threshold_coverage(rows17, "6554", 8, coverage["dominance"]) | threshold_coverage( + rows17, "5555", 8, coverage["dominance"] + ) + missing_at_t8 = hard_ids - t8_only + require(not hard_ids <= t8_only, "T8-only plan unexpectedly covers all table-coverable hard rows") + require( + EXPECTED_HARD_T8_FAILURES <= missing_at_t8, + f"T8-only plan did not fail rows 7, 8, 13: missing={sorted(missing_at_t8, key=row_id_sort_key)}", + ) + + print(f"configs={len(configs)}, ordered_config_pairs={len(configs) ** 2}") + print(f"6554@T7 + 5555@T8: covers {len(hard_plan)} hard/table-coverable rows") + print(f"6554@T6 + 5555@T8: covers {len(all_plan)} all/table-coverable rows") + print("T8-only hard rows missed:", sorted(missing_at_t8, key=row_id_sort_key)) + print("SCOPE: independent table/matching audit; shared CSV and config premise, no geometry proof") + print("PASS_INDEPENDENT_CLASS_C_DOMINANCE") + return 0 + + +if __name__ == "__main__": + try: + raise SystemExit(main()) + except CheckFailure as error: + print(f"FAIL_INDEPENDENT_CLASS_C_DOMINANCE: {error}", file=sys.stderr) + raise SystemExit(1) diff --git a/research/class-c-dominance-campaign/inputs/help-README.md b/research/class-c-dominance-campaign/inputs/help-README.md new file mode 100644 index 0000000000..7d83378930 --- /dev/null +++ b/research/class-c-dominance-campaign/inputs/help-README.md @@ -0,0 +1,16 @@ +# Class C cells of the one-sided K2 residue: help package (no kappa claim) + +Companion of a Discussion thread asking for help with the "class C" cells (4-flat span questions). Nothing here is a claim about kappa; the relative-root-counting kills used to shrink the list are under audit. + +Files +* `s4z.c` -- 4-flat span checker (a,b,c,d label flats, s = 0). `s3z.c` -- the 3-flat checker it generalises (S3FLAT lineage, exact match checked on sampled slices). +* `gens.txt` -- generators of the frame stabilizer acting on the 112 lines (used for orbit representatives). +* `data88.txt` -- complete direction list |Off| <= 88 (E8 frame split, P112), 18100 directions. +* `rows70.csv` -- the 70 class C rows (d, s, weights, e, status, covering 4-flat configs); `rows17.csv` -- the 17 rows not killed by relative root counting. +* `validate.sh` -- compiles both, reproduces the (6,6,4) s0 crack at T=5 (rep 82, V2idx 103676) and a T=6 pass slice, about 25 s. + +Usage: `s4z data88.txt a b c d 88 T M rem` (a >= ... as the dims of V1..V4 with V1 over orbit representatives; the run splits V1 reps into M chunks, `rem` selects one). Env: `ONLY=r1,r2` restrict reps, `JMOD=J JREM=j` split V2 into J slices, `EXITCRACK=1` stop at first CRACK, `PAIRLOG=1` per-pair log. Output: `CRACK? target T span S ...` if some pair has relaxed span >= T, and an `OVERALL ... max span` summary. A complete run with no CRACK at target T proves span <= T-1 for that config in the relaxed model (kill needs span <= d-1). + +Arguments: for a config {f1>=f2>=f3>=f4}, b = f1 (the largest flat, V2, enumerated), a = one other flat (V1, over orbit representatives; chosen to minimise pairs), c <= d the remaining two (never enumerated, d <= 5). E.g. (6,5,4,3) is `a=3 b=6 c=4 d=5`, T=8 `s4z data88.txt 3 6 4 5 88 8 M rem`. Pair counts: (6,5,4,3) a3 b6 c4 d5 2.6e7 pairs; (6,5,4,4)/(6,5,5,4) a4 b6 1.1e8; (5,5,5,4)/(5,5,5,5) a5 b5 3.3e8. + +Cost at T=8: 70-100% of pairs survive the relaxed gate; 4-10 s per pair for the closure; ETA ~4e4 CPU-h for (6,5,4,3), ~3e5 for the others. diff --git a/research/class-c-dominance-campaign/inputs/rows17.csv b/research/class-c-dominance-campaign/inputs/rows17.csv new file mode 100644 index 0000000000..ef453f30c2 --- /dev/null +++ b/research/class-c-dominance-campaign/inputs/rows17.csv @@ -0,0 +1,18 @@ +row_idx,d,s,weights,e,covering_4flat_configs +7,7,7,"[7, 7, 6, 6, 6, 6, 6, 5, 5, 5, 4]",4,5554 5555 6554 +8,7,7,"[7, 7, 6, 6, 6, 6, 6, 6, 4, 4, 4, 1]",5,6544 6554 +13,7,7,"[7, 7, 7, 6, 6, 6, 6, 5, 4, 4, 4, 1]",5,5544 6444 5554 6544 +21,8,6,"[7, 7, 7, 6, 6, 6, 6, 6, 5, 5, 5, 4]",4,5554 5555 6554 +34,8,7,"[7, 7, 7, 6, 6, 6, 6, 6, 5, 5, 5, 4, 1]",5,5555 6554 +35,8,7,"[7, 7, 7, 6, 6, 6, 6, 6, 5, 5, 5, 5]",4,5555 +36,8,7,"[7, 7, 7, 6, 6, 6, 6, 6, 6, 4, 4, 4, 1, 1]",6,6554 +37,8,7,"[7, 7, 7, 6, 6, 6, 6, 6, 6, 4, 4, 4, 2]",5, +40,8,7,"[7, 7, 7, 6, 6, 6, 6, 6, 6, 5, 4, 4, 1]",5,6554 +42,8,7,"[7, 7, 7, 6, 6, 6, 6, 6, 6, 5, 5, 3, 1]",5,6554 +43,8,7,"[7, 7, 7, 6, 6, 6, 6, 6, 6, 5, 5, 4]",4,6554 +46,8,7,"[7, 7, 7, 7, 6, 6, 6, 6, 5, 4, 4, 4, 1, 1]",6,5554 6544 5555 6554 +47,8,7,"[7, 7, 7, 7, 6, 6, 6, 6, 5, 4, 4, 4, 2]",5,6544 6554 +50,8,7,"[7, 7, 7, 7, 6, 6, 6, 6, 5, 5, 4, 4, 1]",5,5554 6544 5555 6554 +53,8,7,"[7, 7, 7, 7, 6, 6, 6, 6, 5, 5, 5, 4]",4,5554 5555 6554 +57,8,7,"[7, 7, 7, 7, 6, 6, 6, 6, 6, 4, 4, 4, 1]",5,6544 6554 +62,8,7,"[7, 7, 7, 7, 7, 6, 6, 6, 5, 4, 4, 4, 1]",5,5544 6444 5554 6544 diff --git a/research/class-c-dominance-campaign/inputs/rows70.csv b/research/class-c-dominance-campaign/inputs/rows70.csv new file mode 100644 index 0000000000..ee12fc8e3c --- /dev/null +++ b/research/class-c-dominance-campaign/inputs/rows70.csv @@ -0,0 +1,71 @@ +row_idx,d,s,weights,e,rrc_status,covering_4flat_configs +0,6,7,"[7, 6, 6, 6, 6, 6, 5, 5, 4, 4]",4,RRC-killed(under audit),5544 5554 6544 5555 +1,6,7,"[7, 6, 6, 6, 6, 6, 6, 4, 4, 4]",4,RRC-killed(under audit),6444 6544 6554 +2,6,7,"[7, 6, 6, 6, 6, 6, 6, 5, 4, 3]",4,RRC-killed(under audit),6543 6544 6553 6554 +3,6,7,"[7, 6, 6, 6, 6, 6, 6, 6, 3, 3]",4,RRC-killed(under audit), +4,6,7,"[7, 7, 6, 6, 6, 6, 6, 4, 4, 3]",4,RRC-killed(under audit),6443 6444 6543 6544 +5,6,7,"[7, 7, 6, 6, 6, 6, 6, 5, 3, 3]",4,RRC-killed(under audit),6533 6543 6544 6553 +6,7,6,"[7, 7, 7, 6, 6, 6, 6, 6, 4, 4, 3]",4,RRC-killed(under audit),6443 6444 6543 6544 +7,7,7,"[7, 7, 6, 6, 6, 6, 6, 5, 5, 5, 4]",4,HARD,5554 5555 6554 +8,7,7,"[7, 7, 6, 6, 6, 6, 6, 6, 4, 4, 4, 1]",5,HARD,6544 6554 +9,7,7,"[7, 7, 6, 6, 6, 6, 6, 6, 5, 4, 3, 1]",5,RRC-killed(under audit),6544 6553 6554 +10,7,7,"[7, 7, 6, 6, 6, 6, 6, 6, 5, 4, 4]",4,RRC-killed(under audit),6544 6554 +11,7,7,"[7, 7, 6, 6, 6, 6, 6, 6, 5, 5, 3]",4,RRC-killed(under audit),6553 6554 +12,7,7,"[7, 7, 6, 6, 6, 6, 6, 6, 6, 4, 3]",4,RRC-killed(under audit), +13,7,7,"[7, 7, 7, 6, 6, 6, 6, 5, 4, 4, 4, 1]",5,HARD,5544 6444 5554 6544 +14,7,7,"[7, 7, 7, 6, 6, 6, 6, 5, 5, 4, 3, 1]",5,RRC-killed(under audit),5544 5553 6543 5554 +15,7,7,"[7, 7, 7, 6, 6, 6, 6, 5, 5, 4, 4]",4,RRC-killed(under audit),5544 5554 6544 5555 +16,7,7,"[7, 7, 7, 6, 6, 6, 6, 5, 5, 5, 3]",4,RRC-killed(under audit),5553 5554 6553 5555 +17,7,7,"[7, 7, 7, 6, 6, 6, 6, 6, 4, 4, 3, 1]",5,RRC-killed(under audit),6444 6543 6544 6553 +18,7,7,"[7, 7, 7, 6, 6, 6, 6, 6, 4, 4, 4]",4,RRC-killed(under audit),6444 6544 6554 +19,7,7,"[7, 7, 7, 6, 6, 6, 6, 6, 5, 4, 3]",4,RRC-killed(under audit),6543 6544 6553 6554 +20,7,7,"[7, 7, 7, 7, 6, 6, 6, 6, 4, 4, 3]",4,RRC-killed(under audit),6443 6444 6543 6544 +21,8,6,"[7, 7, 7, 6, 6, 6, 6, 6, 5, 5, 5, 4]",4,HARD,5554 5555 6554 +22,8,6,"[7, 7, 7, 6, 6, 6, 6, 6, 6, 5, 4, 4]",4,RRC-killed(under audit),6544 6554 +23,8,6,"[7, 7, 7, 6, 6, 6, 6, 6, 6, 5, 5, 3]",4,RRC-killed(under audit),6553 6554 +24,8,6,"[7, 7, 7, 6, 6, 6, 6, 6, 6, 6, 4, 3]",4,RRC-killed(under audit), +25,8,6,"[7, 7, 7, 7, 6, 6, 6, 5, 5, 5, 5, 4]",4,RRC-killed(under audit),5554 5555 6554 +26,8,6,"[7, 7, 7, 7, 6, 6, 6, 6, 5, 5, 4, 4]",4,RRC-killed(under audit),5544 5554 6544 5555 +27,8,6,"[7, 7, 7, 7, 6, 6, 6, 6, 5, 5, 5, 3]",4,RRC-killed(under audit),5553 5554 6553 5555 +28,8,6,"[7, 7, 7, 7, 6, 6, 6, 6, 6, 4, 4, 3, 1]",5,RRC-killed(under audit),6444 6543 6544 6553 +29,8,6,"[7, 7, 7, 7, 6, 6, 6, 6, 6, 4, 4, 4]",4,RRC-killed(under audit),6444 6544 6554 +30,8,6,"[7, 7, 7, 7, 6, 6, 6, 6, 6, 5, 4, 3]",4,RRC-killed(under audit),6543 6544 6553 6554 +31,8,6,"[7, 7, 7, 7, 7, 6, 6, 6, 5, 4, 4, 4]",4,RRC-killed(under audit),5444 5544 6444 5554 +32,8,6,"[7, 7, 7, 7, 7, 6, 6, 6, 5, 5, 4, 3]",4,RRC-killed(under audit),5543 5544 5553 6543 +33,8,6,"[7, 7, 7, 7, 7, 6, 6, 6, 6, 4, 4, 3]",4,RRC-killed(under audit),6443 6444 6543 6544 +34,8,7,"[7, 7, 7, 6, 6, 6, 6, 6, 5, 5, 5, 4, 1]",5,HARD,5555 6554 +35,8,7,"[7, 7, 7, 6, 6, 6, 6, 6, 5, 5, 5, 5]",4,HARD,5555 +36,8,7,"[7, 7, 7, 6, 6, 6, 6, 6, 6, 4, 4, 4, 1, 1]",6,HARD,6554 +37,8,7,"[7, 7, 7, 6, 6, 6, 6, 6, 6, 4, 4, 4, 2]",5,HARD, +38,8,7,"[7, 7, 7, 6, 6, 6, 6, 6, 6, 5, 4, 3, 1, 1]",6,RRC-killed(under audit),6554 +39,8,7,"[7, 7, 7, 6, 6, 6, 6, 6, 6, 5, 4, 3, 2]",5,RRC-killed(under audit),6554 +40,8,7,"[7, 7, 7, 6, 6, 6, 6, 6, 6, 5, 4, 4, 1]",5,HARD,6554 +41,8,7,"[7, 7, 7, 6, 6, 6, 6, 6, 6, 5, 5, 2, 2]",5,RRC-killed(under audit),6554 +42,8,7,"[7, 7, 7, 6, 6, 6, 6, 6, 6, 5, 5, 3, 1]",5,HARD,6554 +43,8,7,"[7, 7, 7, 6, 6, 6, 6, 6, 6, 5, 5, 4]",4,HARD,6554 +44,8,7,"[7, 7, 7, 7, 6, 6, 6, 5, 5, 5, 5, 4, 1]",5,RRC-killed(under audit),5555 6554 +45,8,7,"[7, 7, 7, 7, 6, 6, 6, 5, 5, 5, 5, 5]",4,RRC-killed(under audit),5555 +46,8,7,"[7, 7, 7, 7, 6, 6, 6, 6, 5, 4, 4, 4, 1, 1]",6,HARD,5554 6544 5555 6554 +47,8,7,"[7, 7, 7, 7, 6, 6, 6, 6, 5, 4, 4, 4, 2]",5,HARD,6544 6554 +48,8,7,"[7, 7, 7, 7, 6, 6, 6, 6, 5, 5, 4, 3, 1, 1]",6,RRC-killed(under audit),5554 6544 6553 5555 +49,8,7,"[7, 7, 7, 7, 6, 6, 6, 6, 5, 5, 4, 3, 2]",5,RRC-killed(under audit),5554 6553 5555 6554 +50,8,7,"[7, 7, 7, 7, 6, 6, 6, 6, 5, 5, 4, 4, 1]",5,HARD,5554 6544 5555 6554 +51,8,7,"[7, 7, 7, 7, 6, 6, 6, 6, 5, 5, 5, 2, 2]",5,RRC-killed(under audit),5554 5555 6554 +52,8,7,"[7, 7, 7, 7, 6, 6, 6, 6, 5, 5, 5, 3, 1]",5,RRC-killed(under audit),5554 6553 5555 6554 +53,8,7,"[7, 7, 7, 7, 6, 6, 6, 6, 5, 5, 5, 4]",4,HARD,5554 5555 6554 +54,8,7,"[7, 7, 7, 7, 6, 6, 6, 6, 6, 4, 3, 3, 3]",5,RRC-killed(under audit), +55,8,7,"[7, 7, 7, 7, 6, 6, 6, 6, 6, 4, 4, 3, 1, 1]",6,RRC-killed(under audit),6544 6553 6554 +56,8,7,"[7, 7, 7, 7, 6, 6, 6, 6, 6, 4, 4, 3, 2]",5,RRC-killed(under audit),6544 6554 +57,8,7,"[7, 7, 7, 7, 6, 6, 6, 6, 6, 4, 4, 4, 1]",5,HARD,6544 6554 +58,8,7,"[7, 7, 7, 7, 6, 6, 6, 6, 6, 5, 4, 3, 1]",5,RRC-killed(under audit),6544 6553 6554 +59,8,7,"[7, 7, 7, 7, 6, 6, 6, 6, 6, 5, 4, 4]",4,RRC-killed(under audit),6544 6554 +60,8,7,"[7, 7, 7, 7, 6, 6, 6, 6, 6, 5, 5, 3]",4,RRC-killed(under audit),6553 6554 +61,8,7,"[7, 7, 7, 7, 6, 6, 6, 6, 6, 6, 4, 3]",4,RRC-killed(under audit), +62,8,7,"[7, 7, 7, 7, 7, 6, 6, 6, 5, 4, 4, 4, 1]",5,HARD,5544 6444 5554 6544 +63,8,7,"[7, 7, 7, 7, 7, 6, 6, 6, 5, 5, 4, 3, 1]",5,RRC-killed(under audit),5544 5553 6543 5554 +64,8,7,"[7, 7, 7, 7, 7, 6, 6, 6, 5, 5, 4, 4]",4,RRC-killed(under audit),5544 5554 6544 5555 +65,8,7,"[7, 7, 7, 7, 7, 6, 6, 6, 5, 5, 5, 3]",4,RRC-killed(under audit),5553 5554 6553 5555 +66,8,7,"[7, 7, 7, 7, 7, 6, 6, 6, 6, 4, 4, 3, 1]",5,RRC-killed(under audit),6444 6543 6544 6553 +67,8,7,"[7, 7, 7, 7, 7, 6, 6, 6, 6, 4, 4, 4]",4,RRC-killed(under audit),6444 6544 6554 +68,8,7,"[7, 7, 7, 7, 7, 6, 6, 6, 6, 5, 4, 3]",4,RRC-killed(under audit),6543 6544 6553 6554 +69,8,7,"[7, 7, 7, 7, 7, 7, 6, 6, 6, 4, 4, 3]",4,RRC-killed(under audit),6443 6444 6543 6544 diff --git a/research/class-c-dominance-campaign/verify.py b/research/class-c-dominance-campaign/verify.py new file mode 100644 index 0000000000..eb430bcd28 --- /dev/null +++ b/research/class-c-dominance-campaign/verify.py @@ -0,0 +1,202 @@ +#!/usr/bin/env python3 +"""Exact conditional campaign audit; no geometric span computation. + +Krzysztof Wojt, with substantial OpenAI Codex assistance. Apache-2.0. +""" +import argparse +import copy +import csv +import hashlib +import itertools +import json +from pathlib import Path + +HERE = Path(__file__).resolve().parent +G = (0, 1, 2, 4, 8, 12, 20, 36) +PINS = { + "rows70.csv": "c0eb6bb88498bf39a8b2020b1d0d600181f6e13eb9dd6a6e5f90794f0895754a", + "rows17.csv": "9ebe7fc1ecd74148e7bdefa1f6bb2ed00551884b1a4a6558d7f129f7eef4efd5", + "help-README.md": "aba39c91e262edfb495cf1ccaf7c7555199ee9c0b87e99ecd22e4f1bb14c292f", +} + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def dims(config): + require(isinstance(config, str) and len(config) == 4, "need four dimensions") + require(all(c in "1234567" for c in config), "dimension outside 1..7") + values = tuple(map(int, config)) + require(values == tuple(sorted(values, reverse=True)), "noncanonical dimensions") + return values + + +def dominates(target, source): + return all(a >= b for a, b in zip(dims(target), dims(source))) + + +def admissible(config): + return sum(G[d] for d in dims(config)) <= 52 + + +def load_rows(): + for name, expected in PINS.items(): + actual = hashlib.sha256((HERE / "inputs" / name).read_bytes()).hexdigest() + require(actual == expected, "source drift: " + name) + with (HERE / "inputs/rows70.csv").open(newline="") as handle: + rows = list(csv.DictReader(handle)) + with (HERE / "inputs/rows17.csv").open(newline="") as handle: + hard = list(csv.DictReader(handle)) + require([int(r["row_idx"]) for r in rows] == list(range(70)), "row identity/order") + hard_projection = [{k: v for k, v in r.items() if k != "rrc_status"} + for r in rows if r["rrc_status"] == "HARD"] + require(len(hard) == 17 and hard == hard_projection, + "HARD table differs from source subset") + for row in rows: + weights = json.loads(row["weights"]) + require(int(row["d"]) + int(row["e"]) == len(weights), "dimension ledger") + require(all(type(w) is int and 1 <= w <= 7 for w in weights), "piece weight") + configs = row["covering_4flat_configs"].split() + require(len(configs) == len(set(configs)), "duplicate configuration") + require(all(admissible(c) for c in configs), "inadmissible listed configuration") + return rows, hard + + +def covers(row, target, relation=dominates): + return any(relation(target, source) for source in row["covering_4flat_configs"].split()) + + +def minimum_covers(rows, configs, relation): + needed = {int(r["row_idx"]) for r in rows if r["covering_4flat_configs"]} + sets = {c: {int(r["row_idx"]) for r in rows if covers(r, c, relation)} for c in configs} + for size in range(1, len(configs) + 1): + solutions = [list(choice) for choice in itertools.combinations(configs, size) + if set().union(*(sets[c] for c in choice)) == needed] + if solutions: + return {"size": size, "solutions": solutions} + raise ValueError("no campaign covers the listed incidences") + + +def plan(rows, targets): + witnesses, uncovered = [], [] + for row in rows: + match = next(((target, threshold, source) for target, threshold in targets + if threshold <= int(row["d"]) + for source in row["covering_4flat_configs"].split() + if dominates(target, source)), None) + if match is None: + uncovered.append(int(row["row_idx"])) + else: + target, threshold, source = match + witnesses.append({"row": int(row["row_idx"]), "d": int(row["d"]), + "source": source, "target": target, "threshold": threshold}) + return {"targets": [[c, t] for c, t in targets], "witnesses": witnesses, + "uncovered": uncovered} + + +def validate_plan(rows, receipt): + by_id = {int(r["row_idx"]): r for r in rows} + seen = set() + declared = {tuple(t) for t in receipt["targets"]} + for target, threshold in declared: + require(admissible(target), "target exceeds the 52-label budget") + require(type(threshold) is int and threshold >= 1, "invalid threshold") + for w in receipt["witnesses"]: + require(w["row"] in by_id and w["row"] not in seen, "missing/duplicate row") + seen.add(w["row"]) + row = by_id[w["row"]] + require(w["d"] == int(row["d"]), "changed row dimension") + require(w["source"] in row["covering_4flat_configs"].split(), "invented cover") + require((w["target"], w["threshold"]) in declared, "undeclared target") + require(dominates(w["target"], w["source"]), "invalid extension") + require(w["threshold"] <= int(row["d"]), "span threshold too weak") + require(seen.isdisjoint(receipt["uncovered"]), "covered row also uncovered") + require(seen | set(receipt["uncovered"]) == set(by_id), "incomplete row partition") + + +def result(rows, hard): + configs = sorted({c for r in rows for c in r["covering_4flat_configs"].split()}) + coverage = { + "dominance": {c: [s for s in configs if dominates(c, s)] for c in configs}, + "cover_all": {c: [int(r["row_idx"]) for r in rows if covers(r, c)] for c in configs}, + "cover_hard": {c: [int(r["row_idx"]) for r in hard if covers(r, c)] for c in configs}, + } + hard_plan = plan(hard, [("6554", 7), ("5555", 8)]) + all_plan = plan(rows, [("6554", 6), ("5555", 8)]) + validate_plan(hard, hard_plan) + validate_plan(rows, all_plan) + return { + "schema_version": 1, + "scope": "conditional scheduling implication; no geometric span pass or new exclusion", + "coverage": coverage, + "literal_minimum_hard": minimum_covers(hard, configs, lambda a, b: a == b), + "literal_minimum_all": minimum_covers(rows, configs, lambda a, b: a == b), + "claimed_three_literal_misses": [int(r["row_idx"]) for r in rows + if r["covering_4flat_configs"] and not any( + c in r["covering_4flat_configs"].split() + for c in ("5544", "5555", "6554"))], + "dominance_minimum_hard": minimum_covers(hard, configs, dominates), + "dominance_minimum_all": minimum_covers(rows, configs, dominates), + "hard_campaign": hard_plan, "all_campaign": all_plan, "source_sha256": PINS, + } + + +def controls(hard, receipt): + require(dominates("6554", "5544") and not dominates("6554", "5555"), "extension control") + require(admissible("6554") and admissible("5555") and not admissible("6555"), + "budget control") + weak = plan(hard, [("6554", 8), ("5555", 8)]) + require(weak["uncovered"] == [7, 8, 13, 37], "T8-only must miss lower-d rows") + require(receipt["hard_campaign"]["uncovered"] == [37], "hard remainder changed") + require(receipt["all_campaign"]["uncovered"] == [3, 12, 24, 37, 54, 61], + "no-config rows must stay unresolved") + require(receipt["literal_minimum_hard"]["size"] == 3, "literal control changed") + require(receipt["literal_minimum_all"]["size"] == 4, "all-row literal minimum changed") + require(receipt["claimed_three_literal_misses"] == [4, 5, 6, 17, 20, 28, 33, 66, 69], + "literal three-config claim control changed") + require(receipt["dominance_minimum_hard"]["solutions"] == [["5555", "6554"]], + "two-target minimum changed") + mutations = [] + bad = copy.deepcopy(receipt["hard_campaign"]) + bad["witnesses"][0]["threshold"] = 8 + bad["targets"].append(["6554", 8]) + mutations.append(("weak threshold", bad)) + bad = copy.deepcopy(receipt["hard_campaign"]) + w = next(w for w in bad["witnesses"] if w["row"] == 35) + w["target"], w["threshold"] = "6554", 7 + mutations.append(("false dominance", bad)) + bad = copy.deepcopy(receipt["hard_campaign"]) + bad["witnesses"][0]["source"] = "1111" + mutations.append(("invented inherited cover", bad)) + bad = copy.deepcopy(receipt["hard_campaign"]) + bad["witnesses"][0]["target"] = "6555" + bad["targets"].append(["6555", 7]) + mutations.append(("over-budget target", bad)) + for name, bad in mutations: + try: + validate_plan(hard, bad) + except ValueError: + continue + raise ValueError("accepted mutant: " + name) + return len(mutations) + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--write", action="store_true", help="regenerate deterministic receipt") + args = parser.parse_args() + rows, hard = load_rows() + receipt = result(rows, hard) + rejected = controls(hard, receipt) + target = HERE / "RESULT.json" + if args.write: + target.write_text(json.dumps(receipt, indent=2, sort_keys=True) + "\n", encoding="utf-8") + else: + require(receipt == json.loads(target.read_text()), "committed receipt differs") + print(f"PASS_CLASS_C_DOMINANCE hard=16 all=64 targets=2 rejected={rejected} no_span_pass") + + +if __name__ == "__main__": + main()