diff --git a/research/e8-p111-pairing-floor/NOTICE.md b/research/e8-p111-pairing-floor/NOTICE.md new file mode 100644 index 0000000000..ea078298fa --- /dev/null +++ b/research/e8-p111-pairing-floor/NOTICE.md @@ -0,0 +1,34 @@ +# Attribution and scope + +Prepared by Cody Harris (@VibeCodyH), with substantial OpenAI Codex assistance +in proof development, implementation, verification and writing. No independent +human review is claimed. New material is under the repository's +[Apache-2.0 license](../../LICENSE). + +Predecessor credit: + +- **Joel Pulikkan / GamingPuzzled, #620:** the P111 pairing-rank question, + the discounted-copy mechanism, its 6/7/8 cost classification and the reported + cost-63 conclusion from SAT runs without proof logs. This contribution does + not claim priority for the conjectured or reported numerical floor. +- **DreamingOfClouds, #545:** the nine-puncture bit unit, rank-seven star + totals and cost-63 supplier. **eumemic, #555:** its subsequent supplier work. +- **eumemic, #493**, following **Dylan Crow / utcorvusvolat-dotcom, #370**: + the actual supplier's Hamming root coordinates and numbering, the source + skeleton and the bit word. The existing word is read as a pinned geometry + input, not copied or regenerated by this package. +- **DreamingOfClouds, #446 and #595:** the physical pairing-rank accounting + premise and the alternative Hamming geometry utility used in the numbering + control. The former remains a separately inherited premise. + +The new result is the basis-counting proof, the ten-term obstructions, and +an independent exact verifier bound to the shipped P111 geometry. No solver +code or numerical rank implementation from these predecessors is imported. +Coordinate conventions, the puncture choice and their attribution are retained. + +Concurrent #631 (Zhao Chi / vectorsss) treats star-decoder puncture thresholds; +#669 treats paired-hypercube stars; #703 (Douglas R. Colkitt / Mister-Meeseeks) +treats quaternionic E8; #717 (DreamingOfClouds) treats complex decoder floors. +Their scopes were checked for overlap. None supplies a premise of the finite +proof here. Exact observed heads and immutable local inputs are recorded in +[SOURCES.json](SOURCES.json). diff --git a/research/e8-p111-pairing-floor/PROOF.md b/research/e8-p111-pairing-floor/PROOF.md new file mode 100644 index 0000000000..6fa323a1b8 --- /dev/null +++ b/research/e8-p111-pairing-floor/PROOF.md @@ -0,0 +1,206 @@ +# Pairing rank for the shipped P111 label decoder + +This is a finite algebraic theorem about a fixed decoder and fixed rational +geometry. Its connection to physical copy accounting is conditional as stated +below. It makes no new kappa claim. + +## Definitions and finite premises + +Let `L[0],...,L[119]` be the Hamming-coordinate E8 root lines in the order used +by #493 and the #545 shipped word. Each has squared norm 4. Put + +```text +P = [39,52,57,71,76,78,103,109,114], +S = {0,...,119} minus P, +G[i,j] = /2, +B[i,j] = (1 + G[i,j]) mod 2, +C = B[P,P], M = C^(-1), W = B[S,P]. +``` + +All binary matrices in this note are over F2. Ranks of root spans and pairings +are over Q. The exact checker verifies that `C` is invertible, `rank(W)=9`, +and the restricted decoder is `B[S,S] = W M W^T`. + +For a nonzero binary column `x` of length nine, define + +```text +R(x) = {i in S : (W x)[i] = 1}, +E(x) = span_Q {L[i] : i in R(x)}, +beta(x,y) = rank_Q of the dot-product pairing E(x) x E(y). +``` + +We consider arbitrary finite decompositions + +```text +M = sum_j x_j y_j^T, x_j != 0, y_j != 0, +cost = sum_j beta(x_j,y_j). +``` + +Equivalently, these decompose `B[S,S]` into scalar totals whose individual +source and reader columns lie in `im(W)`. The full column rank of W makes the +equivalence exact. Repeated terms and cancellations are allowed. Zero terms +can be removed without changing the matrix or cost. + +The 511-support census proves these finite premises by rational elimination: + +1. `E(e_a) = L[P[a]]^perp`, of dimension seven, for all nine coordinate vectors. +2. Every other nonzero `x` has `E(x) = Q^8`. + +Consequently the complete term-cost table is + +```text +6 if x=e_a, y=e_b, a!=b, and =0; +7 if at least one factor is a coordinate vector, except the preceding case; +8 otherwise. +``` + +For two hyperplanes, the pairing has a one-dimensional kernel exactly when +their normals are orthogonal. A full Q^8 span pairs nondegenerately with the +other span. This proves the table from the two premises; the checker also +recomputes all 81 hyperplane-pair ranks directly. There are 36 cost-six, +9,081 cost-seven and 252,004 cost-eight ordered pairs. + +The small matrices needed below are recorded as binary-packed rows, with +bit `j` representing column `j` and all indices zero-based: + +```text +C = [17,314,284,462,471,418,472,248,382] +M = [380,422,147,25,381,307,401,326,499] +``` + +Every diagonal entry of C is one. The five diagonal ones of M are at positions +`{1,3,4,5,8}`. Its principal block at positions `{3,5}` is `I_2`, while +`C[3,5]=C[5,3]=0`. Thus every cost-six matrix unit vanishes throughout that +2-by-2 block. These facts are checked from the generated geometry, not assumed +as arbitrary input constants. + +## Theorem + +The minimum of `sum_j beta(x_j,y_j)` over the decompositions above is **63**. + +### Nine terms: each discount needs an expensive term + +More generally, let C be an invertible 9-by-9 binary matrix with unit diagonal. +Suppose `C^(-1) = X Y^T` has exactly nine nonzero rank-one terms. Both X and Y +are invertible, and + +```text +Y^T C X = I_9. +``` + +Let A be the set of coordinate indices occurring as unit columns of X, and D +the corresponding set for Y. Unit columns cannot repeat within a basis. If +`a` belongs to both A and D, let column `i` of X and column `j` of Y both be +`e_a`. Their pairing is `C[a,a]=1`, so duality forces `i=j`. Conversely, a term +`e_a e_a^T` gives such an intersection. + +Write `d` for the number of terms with two different unit factors, `s` for +the number with two equal unit factors, `t` for the number with exactly one +unit factor, and `u` for the number with neither factor a unit. Then + +```text +9 = d+s+t+u, +|A union D| = (2d+2s+t)-s = 9+d-u <= 9, +``` + +so `d <= u`. Every cost-six term is among the d terms; every cost-eight term +is among the u terms, and all u terms cost eight. If their counts are `n6` +and `n8`, respectively, `n6 <= d <= u = n8`. Hence + +```text +cost = 7*9 - n6 + n8 >= 63. +``` + +This is a counting proof for every nine-term factorization, not an enumeration +of bases. It uses no symmetry assumption on X or Y. + +### Ten terms: diagonal support or a rank-two obstruction + +For ten terms, write `n6+n7+n8=10`. Cost at most 62 requires + +```text +cost = 60+n7+2*n8 <= 62. +``` + +If `n8=0`, there are at most two cost-seven terms. Cost-six terms are +off-diagonal matrix units and contribute nothing to the diagonal. A +cost-seven term has a unit factor, so its diagonal is supported at at most +one coordinate. Two such terms cannot produce the five diagonal ones of M. + +If `n8=1`, the budget forces `n7=0` and `n6=9`. Every cost-six term vanishes +on the principal block `{3,5}`. The single remaining rank-one term would +therefore have to equal `I_2` on that block, which is impossible by rank. + +If `n8>=2`, cost is already at least 64. This exhausts the ten-term case. + +### All other term counts and attainment + +Fewer than nine rank-one terms cannot sum to the rank-nine matrix M. Eleven +or more nonzero terms cost at least `6*11=66`. Together with the preceding +arguments, this proves the lower bound for every finite term count. + +For the upper bound, use the nine column terms + +```text +x_j = column j of M, y_j = e_j. +``` + +Their sum is M. Every column of M has more than one nonzero entry, so each +term costs seven. The verifier checks all nine terms and their sum. This is +an attaining algebraic star decoder at cost 63; the existing #545/#555 +supplier is credited separately and is not replayed here. + +## Source numbering + +The order in `research/format-limits/scripts/e8units.py::hamming_e8` differs +from the order in `research/e8-bit-carrier-skeleton/code/skeleton/e8.py`. +Both generate the same set of 120 root lines. Expressed in the former's +sorted-tetrad order, the shipped punctures are + +```text +[111,52,9,119,76,78,31,37,66]. +``` + +Reusing `[39,52,57,71,76,78,103,109,114]` without this conversion instead +selects a different set, with 44 rather than 36 ordered orthogonal pairs. +The 44 count matches #620's report. Its `geo.py` imports an external +`e8units` module; that local runtime module is not shipped in its directory, +so this note does not assert which exact module bytes ran in the author's +environment. Numerical indices or the report's count alone do not certify a +binding to the shipped supplier. The present check regenerates the supplier's +order and compares every live coordinate directly to the pinned word. + +This distinction does not invalidate #620's reported SAT result for its +tested instance. The contribution here is a solver-free proof bound to the +actual shipped geometry, including an explicit rejection of the other order. + +## Physical interpretation and limits + +The finite optimization theorem above is self-contained given its explicitly +checked geometry. Interpreting beta as a lower bound on paid physical copy +rank additionally uses [#446, Theorem C, section 4](https://github.com/CrocSwap/integer-mult-bounds/blob/309482849b6ddf34db998f53612d34c19f6e3233/research/format-obstructions/PROOF.md): +each scalar total is gathered drop-free, propagated through its copy tree, +and read inside the relevant orthogonal frames. Summing the per-total bounds +requires the additive charging of these trees. That premise is not proved by +this finite checker and does not cover an unpriced shared multi-total primitive. + +Under this accounting, even granting free source access, helpers, frame +preparation, restoration and other recursive work cannot lower the copy +charge below the existing 63. Adding those nonnegative expenses cannot make +this particular copy-saving mechanism help. The inherited deficit expression +for this unit therefore remains bounded by + +```text +D/T <= (s-1)*111 - s*63 = 48*s - 111. +``` + +This excludes a cheaper copy charge in the specified factorization class, +not improvements to helper work or a universal bound on multiplication. +Different fitting decoder matrices, factors outside `im(W)`, other punctures, +vector-valued totals, different geometry or different accounting remain open. +No uniqueness claim about arbitrary fitting matrices is inferred from #620's +SAT runs. The selected frontier and all inherited asymptotic compiler, +realization, hosting, precision and analytic assumptions remain unchanged. + +The finite premise census and mutation controls are reproducible evidence, +not a machine-formal proof of this argument or of the multiplication theorem. diff --git a/research/e8-p111-pairing-floor/README.md b/research/e8-p111-pairing-floor/README.md new file mode 100644 index 0000000000..f341cb99e5 --- /dev/null +++ b/research/e8-p111-pairing-floor/README.md @@ -0,0 +1,66 @@ +# P111 bit decoder: an algebraic pairing-cost floor of 63 + +**Scoped negative result; no new kappa.** For the actual 111-port bit geometry +shipped in #545, every scalar label-factorization of its fixed decoder has +total rational pairing rank at least **63**, with arbitrarily many totals. +Nine rank-seven star totals attain the bound. + +The [proof](PROOF.md) supplies a solver-free counterpart to #620's reported +SAT exclusion: a counting argument for nine terms and two small matrix +obstructions for ten terms. +Fewer terms fail by rank; eleven or more already cost at least 66. The verifier +uses only exact integer and rational arithmetic, with no SAT solver or imported +predecessor code. + +The source binding matters: the same nine numerical puncture indices select +different roots in two repository utilities. The shipped geometry has **36** +ordered discounted pairs; the sorted-tetrad utility gives **44**. This package +compares all 111 live coordinates to the shipped word before using the bound. +See [the numbering check](PROOF.md#source-numbering). + +From the repository root, using Python 3.10 or newer: + +```sh +python3 -B research/e8-p111-pairing-floor/verify.py +``` + +Expected: + +```text +PASS_P111_PAIRING_FLOOR: cost 63; 511 exact supports; 261121 support pairs; 12 negative controls +``` + +The command verifies source hashes, regenerates the deterministic receipt and +compares it with [RESULTS.json](RESULTS.json). All controls run by default. +`--write /tmp/p111-result.json` writes a fresh receipt for comparison. + +An optional [independent check](independent_check.py) reads the parent's stored +coordinates directly and uses SymPy (tested with 1.14.0): + +```sh +python3 -B research/e8-p111-pairing-floor/independent_check.py +``` + +It checks all 511 rational support ranks and 81 pairing ranks, plus all 672 +dimension-three basis factorizations in its explicitly bounded calibration +domain. It does not import the main checker or its root generator. + +Coverage includes all 511 nonzero label functionals, exact Q-ranks of their +reader supports, all 81 hyperplane pairings, the classification of all 261,121 +ordered functional pairs, all 29 candidate count budgets of cost at most 62, +and an attaining cost-63 factorization. The 128 seeded basis changes are +calibration tests, not an exhaustive search or a proof of the nine-term lemma. + +The theorem fixes the decoder matrix and requires every individual source and +reader functional to lie in its nine-dimensional label space. It does not +exclude other fitting matrices, factorizations outside that space, vector +totals, other punctures or helper improvements. Translating pairing rank to +physical copy charges additionally inherits the separately stated tree and +additive accounting premises from #446. No physical supplier, full repository +replay, new asymptotic bound or formal multiplication theorem is claimed. + +Base: `66849e1475c930fd7732b1a0067ffee7e1e95f60`. The accepted conditional +kappa at that base remains `51110230636731/31250000000000000` (#626 with #543). +Source pins and related work are in [SOURCES.json](SOURCES.json); attribution +and substantial AI assistance are disclosed in [NOTICE.md](NOTICE.md). +Local execution details and limits are in [VALIDATION.md](VALIDATION.md). diff --git a/research/e8-p111-pairing-floor/RESULTS.json b/research/e8-p111-pairing-floor/RESULTS.json new file mode 100644 index 0000000000..417bafb293 --- /dev/null +++ b/research/e8-p111-pairing-floor/RESULTS.json @@ -0,0 +1,551 @@ +{ + "C_rows": [ + 17, + 314, + 284, + 462, + 471, + 418, + 472, + 248, + 382 + ], + "M_inverse_rows": [ + 380, + 422, + 147, + 25, + 381, + 307, + 401, + 326, + 499 + ], + "attaining_star": [ + { + "cost": 7, + "x": 380, + "y": 1 + }, + { + "cost": 7, + "x": 422, + "y": 2 + }, + { + "cost": 7, + "x": 147, + "y": 4 + }, + { + "cost": 7, + "x": 25, + "y": 8 + }, + { + "cost": 7, + "x": 381, + "y": 16 + }, + { + "cost": 7, + "x": 307, + "y": 32 + }, + { + "cost": 7, + "x": 401, + "y": 64 + }, + { + "cost": 7, + "x": 326, + "y": 128 + }, + { + "cost": 7, + "x": 499, + "y": 256 + } + ], + "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "calibration_nine_term_prices": { + "69": 1, + "70": 6, + "71": 23, + "72": 98 + }, + "calibration_seed": 45, + "cheap_rows": [ + 16, + 312, + 280, + 454, + 455, + 386, + 408, + 120, + 126 + ], + "conventions": "bit j is column j; puncture positions and ports are zero-based", + "diagonal_ones": [ + 1, + 3, + 4, + 5, + 8 + ], + "excluded_budgets_at_most_62": [ + { + "cost": 62, + "counts_6_7_8": [ + 1, + 8, + 0 + ], + "excluded_by": "basis-counting", + "n": 9 + }, + { + "cost": 61, + "counts_6_7_8": [ + 2, + 7, + 0 + ], + "excluded_by": "basis-counting", + "n": 9 + }, + { + "cost": 62, + "counts_6_7_8": [ + 2, + 6, + 1 + ], + "excluded_by": "basis-counting", + "n": 9 + }, + { + "cost": 60, + "counts_6_7_8": [ + 3, + 6, + 0 + ], + "excluded_by": "basis-counting", + "n": 9 + }, + { + "cost": 61, + "counts_6_7_8": [ + 3, + 5, + 1 + ], + "excluded_by": "basis-counting", + "n": 9 + }, + { + "cost": 62, + "counts_6_7_8": [ + 3, + 4, + 2 + ], + "excluded_by": "basis-counting", + "n": 9 + }, + { + "cost": 59, + "counts_6_7_8": [ + 4, + 5, + 0 + ], + "excluded_by": "basis-counting", + "n": 9 + }, + { + "cost": 60, + "counts_6_7_8": [ + 4, + 4, + 1 + ], + "excluded_by": "basis-counting", + "n": 9 + }, + { + "cost": 61, + "counts_6_7_8": [ + 4, + 3, + 2 + ], + "excluded_by": "basis-counting", + "n": 9 + }, + { + "cost": 62, + "counts_6_7_8": [ + 4, + 2, + 3 + ], + "excluded_by": "basis-counting", + "n": 9 + }, + { + "cost": 58, + "counts_6_7_8": [ + 5, + 4, + 0 + ], + "excluded_by": "basis-counting", + "n": 9 + }, + { + "cost": 59, + "counts_6_7_8": [ + 5, + 3, + 1 + ], + "excluded_by": "basis-counting", + "n": 9 + }, + { + "cost": 60, + "counts_6_7_8": [ + 5, + 2, + 2 + ], + "excluded_by": "basis-counting", + "n": 9 + }, + { + "cost": 61, + "counts_6_7_8": [ + 5, + 1, + 3 + ], + "excluded_by": "basis-counting", + "n": 9 + }, + { + "cost": 62, + "counts_6_7_8": [ + 5, + 0, + 4 + ], + "excluded_by": "basis-counting", + "n": 9 + }, + { + "cost": 57, + "counts_6_7_8": [ + 6, + 3, + 0 + ], + "excluded_by": "basis-counting", + "n": 9 + }, + { + "cost": 58, + "counts_6_7_8": [ + 6, + 2, + 1 + ], + "excluded_by": "basis-counting", + "n": 9 + }, + { + "cost": 59, + "counts_6_7_8": [ + 6, + 1, + 2 + ], + "excluded_by": "basis-counting", + "n": 9 + }, + { + "cost": 60, + "counts_6_7_8": [ + 6, + 0, + 3 + ], + "excluded_by": "basis-counting", + "n": 9 + }, + { + "cost": 56, + "counts_6_7_8": [ + 7, + 2, + 0 + ], + "excluded_by": "basis-counting", + "n": 9 + }, + { + "cost": 57, + "counts_6_7_8": [ + 7, + 1, + 1 + ], + "excluded_by": "basis-counting", + "n": 9 + }, + { + "cost": 58, + "counts_6_7_8": [ + 7, + 0, + 2 + ], + "excluded_by": "basis-counting", + "n": 9 + }, + { + "cost": 55, + "counts_6_7_8": [ + 8, + 1, + 0 + ], + "excluded_by": "basis-counting", + "n": 9 + }, + { + "cost": 56, + "counts_6_7_8": [ + 8, + 0, + 1 + ], + "excluded_by": "basis-counting", + "n": 9 + }, + { + "cost": 54, + "counts_6_7_8": [ + 9, + 0, + 0 + ], + "excluded_by": "basis-counting", + "n": 9 + }, + { + "cost": 62, + "counts_6_7_8": [ + 8, + 2, + 0 + ], + "excluded_by": "diagonal-support", + "n": 10 + }, + { + "cost": 61, + "counts_6_7_8": [ + 9, + 1, + 0 + ], + "excluded_by": "diagonal-support", + "n": 10 + }, + { + "cost": 62, + "counts_6_7_8": [ + 9, + 0, + 1 + ], + "excluded_by": "rank-two-block", + "n": 10 + }, + { + "cost": 60, + "counts_6_7_8": [ + 10, + 0, + 0 + ], + "excluded_by": "diagonal-support", + "n": 10 + } + ], + "forbidden_identity_block": [ + 3, + 5 + ], + "live_decoder_entries": 12321, + "live_label_rank": 9, + "minimum_pairing_cost": 63, + "negative_controls": [ + "zero-root", + "wrong-puncture", + "missing-diagonal-premise", + "wrong-inverse", + "forbidden-pair-discount", + "omitted-star-total", + "underpriced-star", + "changed-source-functional", + "unpunctured-rank-seven", + "missing-diagonal-obstruction", + "rank-one-in-place-of-rank-two", + "different-line-numbering" + ], + "numbering_control": { + "actual_supplier_cheap_pairs": 36, + "supplier_punctures_in_sorted_tetrad_order": [ + 111, + 52, + 9, + 119, + 76, + 78, + 31, + 37, + 66 + ], + "unchanged_indices_in_sorted_order_cheap_pairs": 44 + }, + "punctures": [ + 39, + 52, + 57, + 71, + 76, + 78, + 103, + 109, + 114 + ], + "scope": "Fixed B0 label factorizations on this P111 geometry; no new kappa or physical word", + "status": "PASS_P111_PAIRING_FLOOR", + "support_ranks": { + "7": 9, + "8": 502 + }, + "term_cost_histogram": { + "6": 36, + "7": 9081, + "8": 252004 + }, + "terms_at_least_eleven": "cost at least 6*n >= 66", + "terms_below_nine": "excluded by rank(M)=9", + "unit_pair_ranks": [ + [ + 7, + 7, + 7, + 7, + 6, + 7, + 7, + 7, + 7 + ], + [ + 7, + 7, + 7, + 6, + 6, + 6, + 7, + 7, + 6 + ], + [ + 7, + 7, + 7, + 6, + 6, + 7, + 7, + 7, + 6 + ], + [ + 7, + 6, + 6, + 7, + 7, + 7, + 6, + 6, + 6 + ], + [ + 6, + 6, + 6, + 7, + 7, + 7, + 6, + 6, + 6 + ], + [ + 7, + 6, + 7, + 7, + 7, + 7, + 7, + 6, + 6 + ], + [ + 7, + 7, + 7, + 6, + 6, + 7, + 7, + 6, + 6 + ], + [ + 7, + 7, + 7, + 6, + 6, + 6, + 6, + 7, + 7 + ], + [ + 7, + 6, + 6, + 6, + 6, + 6, + 6, + 7, + 7 + ] + ] +} diff --git a/research/e8-p111-pairing-floor/SOURCES.json b/research/e8-p111-pairing-floor/SOURCES.json new file mode 100644 index 0000000000..4f2edba002 --- /dev/null +++ b/research/e8-p111-pairing-floor/SOURCES.json @@ -0,0 +1,94 @@ +{ + "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "local_sha256": { + "certificates/selected-result.json": "b3bf402f31a69bde0629936a9b569bed48281568d7b16d5fba120b5311ea1f53", + "research/e8-punctured111-star/data/bitE8mut-v111-r489.json.gz": "c78317ab05ea175dc380f4dce2bafdbcd7e8b46f0c9d6baf350c2f604bb3ae4e", + "research/e8-punctured111-star/README.md": "1e376d9fc28860adb0c68a0e92123e035ccb903794c457c43ba1f05d61d54625", + "research/e8-decoder-floors-and-cold14-notes/s2-decoder/REPORT.md": "16c53bf8afd9f91eca02b2af9c9f5f09385823fc705dd1a48153508cfdff28b6", + "research/e8-decoder-floors-and-cold14-notes/s2-decoder/geo.py": "73f9c4e4fb7d424fcba45eb5da36bdab694b10020341924b7ebfe7276868716a", + "research/e8-decoder-floors-and-cold14-notes/s2-decoder/dec9sat.py": "1a1a41bb4195a238bff0c576d6cd8ba22f327670f39fd63495970e953f120788", + "research/format-limits/scripts/e8units.py": "3134443d8327d0bf2a8a66c26327cf5268cec6b7ffd85dde750b7e197ce63ef1", + "research/e8-bit-carrier-skeleton/code/skeleton/e8.py": "721d859a6517d665ca84d03ef89668da3aae7433ffb0ee47faf37f2aeb85450e", + "research/e8-bit-carrier-skeleton/data/bit/bitE8mut-r489.json.gz": "835eb96e147740fc7454f8cfb3dbd34ae89524b1dbd89a61e9288eae8ab6a5b9" + }, + "predecessors": [ + { + "pr": 493, + "author": "eumemic", + "role": "Actual supplier Hamming root ordering, following Dylan Crow / utcorvusvolat-dotcom #370" + }, + { + "pr": 545, + "author": "DreamingOfClouds", + "role": "P111 puncture, star cost 63, shipped geometry; inherited #493 eumemic skeleton" + }, + { + "pr": 555, + "author": "eumemic", + "role": "Later P111 supplier; context only" + }, + { + "pr": 620, + "author": "Joel Pulikkan / GamingPuzzled", + "retained_head": "419c7374c3bf5f2eee28f08b1e50c1d57934081c", + "observed_open_head": "e9cf03bbdf7094b5a83f6dbd1d74bfd77a05fb87", + "role": "Pairing-rank P111 question, 6/7/8 cost classification and reported unlogged SAT exclusion" + }, + { + "pr": 446, + "author": "DreamingOfClouds", + "head": "309482849b6ddf34db998f53612d34c19f6e3233", + "path": "research/format-obstructions/PROOF.md", + "role": "Theorem C physical tree-drop lower bound, a separately inherited premise; not imported or executed" + }, + { + "pr": 595, + "author": "DreamingOfClouds", + "role": "Hamming E8 coordinate conventions and accounting context" + } + ], + "overlap_context": [ + { + "pr": 631, + "head": "fb893b5ee1317c2da3b297e6fe78eca0857d1a76", + "scope": "Star-decoder puncture thresholds, not general label pairing rank" + }, + { + "pr": 669, + "head": "308f1e6ec3bb0b6ec0584cf7bfe219addc219b1e", + "scope": "Paired-hypercube decoders, different port family" + }, + { + "pr": 703, + "head": "358383e2f1b0f292d4d6eb897c06fd8558a4f5e6", + "scope": "Quaternionic E8, different ten-line geometry and arbitrary fitting decoders" + }, + { + "pr": 717, + "head": "67e9e846d9e8814b2dd01133251bb83fafa8f5b6", + "scope": "Complex P112 and punctured complex decoders, not rational bit P111", + "initial_observed_head": "07f4671a838088b59c6356ab2b5ffe30038d4b1a" + }, + { + "pr": 726, + "head": "a3041f751114df12453afcb7ac7d0066973797fa", + "scope": "E8 triple gather neighborhoods, not the label-factorization pairing-cost floor" + }, + { + "pr": 747, + "head": "aeaf0899179a14644b412e838ede14db967c765e", + "scope": "240-port paired-hypercube deletion classification, different geometry" + } + ], + "runtime_dependencies": "Python 3.10+ standard library. No predecessor Python module is imported. The verifier reads the pinned word only to bind port order and geometry; it does not replay that supplier.", + "optional_independent_check": "independent_check.py additionally requires SymPy and reads the pinned stored parent coordinates; it never imports verify.py.", + "assignment_seed": 45, + "assignment_track": "Structural decoder research", + "final_metadata_snapshot": { + "utc": "2026-10-13T05:06:00Z", + "open_pr_count": 567, + "highest_open_pr": 748, + "upstream_main": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "pinned_issues": [] + } +} diff --git a/research/e8-p111-pairing-floor/VALIDATION.md b/research/e8-p111-pairing-floor/VALIDATION.md new file mode 100644 index 0000000000..6c473d14a8 --- /dev/null +++ b/research/e8-p111-pairing-floor/VALIDATION.md @@ -0,0 +1,57 @@ +# Local validation + +Executed on Linux with CPython **3.14.8**, 2026-10-13. The optional independent +check used **SymPy 1.14.0**. No additional package was installed. Research +checks ran inside the contributor's shared CPU/memory cap. + +## Reproduction + +```sh +python3 -B research/e8-p111-pairing-floor/verify.py +python3 -I -B -O research/e8-p111-pairing-floor/verify.py +python3 -B research/e8-p111-pairing-floor/independent_check.py +python3 -B scripts/verify_selected_result.py +``` + +The first two commands produce the same deterministic receipt and report +cost 63, 511 exact support checks, 261,121 classified functional pairs and +12 rejected negative controls. The main checker uses explicit exceptions; +its proof-relevant checks remain active under optimized Python. + +The independent script passed all 511 support ranks and 81 pairings using +SymPy and coordinates read directly from the pinned parent word. Its separate +small-domain check exhausts four invertible symmetric 3-by-3 binary forms +with unit diagonal and all 168 binary bases, for 672 factorizations. These +examples calibrate the written general argument; they do not replace it. + +The selected-record check passed at +`51110230636731/31250000000000000`, verifying the original selected source +inventory and proof supplements. No selected-frontier files were edited. + +## Relocation and tampering controls + +A fresh temporary directory contained only this package and the nine inputs +listed in `SOURCES.json::local_sha256`. Running from an unrelated working +directory passed in normal and isolated optimized modes. A newly written +receipt compared byte-for-byte equal with the committed `RESULTS.json`. + +In that disposable copy: + +- Changing the receipt's minimum from 63 to 62 exited with code 1 and + `committed receipt differs`. +- Appending bytes to the pinned compressed supplier input exited with code 1 + at the source-hash check, before decoding the changed input. + +The default verifier's twelve mathematical/geometry controls reject a zero +root, changed puncture, missing diagonal premise, wrong inverse, forbidden +discount, omitted total, underpriced star, changed source functional, +unpunctured rank-seven claim, missing diagonal obstruction, rank-one block +substituted for rank two, and the alternative root numbering. + +## Scope of the checks + +The only changes are this research package. No existing generator or supplier +was changed; the expensive repository-wide `make verify` and selected cold +replay were not run. The targeted exact checks and selected-record integrity +check cover the changed scope. No remote CI pass, independent human review, +second Python-version pass or formal theorem verification is claimed. diff --git a/research/e8-p111-pairing-floor/independent_check.py b/research/e8-p111-pairing-floor/independent_check.py new file mode 100644 index 0000000000..7ad5a7e289 --- /dev/null +++ b/research/e8-p111-pairing-floor/independent_check.py @@ -0,0 +1,99 @@ +#!/usr/bin/env python3 +"""Optional cross-check with SymPy; does not import verify.py or its generator. + +Read the parent word's stored 120 coordinates directly, then independently +check the premises recorded in RESULTS.json. This is extra finite evidence, +not a formal proof or a replay of either supplier. +""" + +import gzip +import hashlib +from itertools import product +import json +from pathlib import Path + +from sympy import Matrix +import sympy + + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def read_pinned(path): + payload = (ROOT / path).read_bytes() + expected = json.loads((HERE / "SOURCES.json").read_text())["local_sha256"][path] + require(hashlib.sha256(payload).hexdigest() == expected, "source pin: " + path) + return json.loads(gzip.decompress(payload)) + + +def main(): + receipt = json.loads((HERE / "RESULTS.json").read_text()) + parent = read_pinned("research/e8-bit-carrier-skeleton/data/bit/bitE8mut-r489.json.gz") + child = read_pinned("research/e8-punctured111-star/data/bitE8mut-v111-r489.json.gz") + labels = Matrix(parent["lines"]) + p = child["punctured"] + live = child["ports_geom"] + require(labels.rows == 120 and labels.cols == 8, "parent geometry dimensions") + require(labels.extract(live, range(8)) == Matrix(child["lines"]), "parent/child coordinates") + gram = labels * labels.T / 2 + binary = gram.applyfunc(lambda x: (x + 1) % 2) + c = binary.extract(p, p) + m = c.inv_mod(2) + w = binary.extract(live, p) + require((w * m * w.T).applyfunc(lambda x: x % 2) == binary.extract(live, live), + "restricted decoder identity") + require([sum(int(m[i, j]) << j for j in range(9)) for i in range(9)] + == receipt["M_inverse_rows"], "independent inverse") + bases = {} + ranks = {7: 0, 8: 0} + for mask in range(1, 512): + x = Matrix([(mask >> j) & 1 for j in range(9)]) + response = (w * x).applyfunc(lambda z: z % 2) + support = [live[i] for i, z in enumerate(response) if z] + rows = labels.extract(support, range(8)) + basis = Matrix.vstack(*rows.rowspace()) + expected = 7 if mask & (mask - 1) == 0 else 8 + require(basis.rows == expected, "independent rational support rank") + ranks[expected] += 1 + if expected == 7: + bases[mask.bit_length() - 1] = basis + require(ranks == {7: 9, 8: 502}, "support rank census") + pairings = [[int((bases[i] * bases[j].T).rank()) for j in range(9)] for i in range(9)] + require(pairings == receipt["unit_pair_ranks"], "81 independent pairing ranks") + + # Exhaust every dimension-three unit-diagonal symmetric form and every + # binary basis. This checks the general counting lemma in a small domain; + # its proof, not these examples, covers dimension nine. + invertibles = [] + for entries in product((0, 1), repeat=9): + x = Matrix(3, 3, entries) + if x.det() % 2: + invertibles.append((x, x.inv_mod(2))) + forms, cases = 0, 0 + for a, b, d in product((0, 1), repeat=3): + c3 = Matrix([[1, a, b], [a, 1, d], [b, d, 1]]) + if not c3.det() % 2: + continue + forms += 1 + for x, xi in invertibles: + y = (xi * c3.inv_mod(2)).T.applyfunc(lambda z: z % 2) + different_units = generic = 0 + for j in range(3): + xu, yu = sum(x[:, j]) == 1, sum(y[:, j]) == 1 + different_units += xu and yu and x[:, j] != y[:, j] + generic += not xu and not yu + require(different_units <= generic, "dimension-three counting lemma") + cases += 1 + require((forms, len(invertibles), cases) == (4, 168, 672), "exhaustive small domain") + print(f"PASS_INDEPENDENT_P111: SymPy {sympy.__version__}; 511 supports; " + "81 pairings; 672 small-basis factorizations") + + +if __name__ == "__main__": + main() diff --git a/research/e8-p111-pairing-floor/verify.py b/research/e8-p111-pairing-floor/verify.py new file mode 100644 index 0000000000..f6fd0e7b82 --- /dev/null +++ b/research/e8-p111-pairing-floor/verify.py @@ -0,0 +1,393 @@ +#!/usr/bin/env python3 +"""Exact P111 pairing-rank certificate. Python 3.10+, standard library only. + +The all-factorization argument is in PROOF.md. This checks its finite premises, +attaining witness, budget cases and rejection controls; it is not a Lean proof. +No predecessor code, numerical rank routine or solver is imported. +""" + +import argparse +from collections import Counter +from fractions import Fraction +import gzip +import hashlib +from itertools import product +import json +from pathlib import Path +import random + + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +PUNCTURES = (39, 52, 57, 71, 76, 78, 103, 109, 114) +WORD = "research/e8-punctured111-star/data/bitE8mut-v111-r489.json.gz" +DIM = 9 +IDENTITY = [1 << i for i in range(DIM)] + + +class Rejected(ValueError): + pass + + +def require(condition, message): + if not condition: + raise Rejected(message) + + +def parity(n): + return n.bit_count() % 2 + + +def dot(a, b): + return sum(x * y for x, y in zip(a, b)) + + +def roots(supplier_order=True): + """Generate E8 lines, preserving the supplier's Hamming word ordering. + + The historical format-limits utility instead sorts its tetrads. It has the + same roots but different indices; this distinction is a rejection control. + """ + generators = ((15, 51, 85, 150) if supplier_order + else (15, 60, 240, 170)) + words = [] + for coefficients in product((0, 1), repeat=4): + word = 0 + for coefficient, generator in zip(coefficients, generators): + if coefficient: + word ^= generator + words.append(tuple((word >> j) & 1 for j in range(8))) + tetrads = [word for word in words if sum(word) == 4] + if not supplier_order: + tetrads.sort() + require(len(set(words)) == 16 and len(tetrads) == 14, "Hamming code") + lines = [tuple(2 * int(i == j) for j in range(8)) for i in range(8)] + for word in tetrads: + support = [j for j, bit in enumerate(word) if bit] + for signs in product((1, -1), repeat=3): + line = [0] * 8 + for j, sign in zip(support, (1,) + signs): + line[j] = sign + lines.append(tuple(line)) + return lines + + +def rational_basis(rows): + """Row basis over Q, using normalized Fraction elimination.""" + echelon, selected = {}, [] + for original in rows: + row = list(map(Fraction, original)) + for pivot, existing in sorted(echelon.items()): + coefficient = row[pivot] + if coefficient: + row = [x - coefficient * y for x, y in zip(row, existing)] + pivot = next((j for j, x in enumerate(row) if x), None) + if pivot is not None: + coefficient = row[pivot] + echelon[pivot] = [x / coefficient for x in row] + selected.append(original) + return selected + + +def binary_rank(rows): + pivots = {} + for row in rows: + while row: + pivot = row.bit_length() - 1 + if pivot not in pivots: + pivots[pivot] = row + break + row ^= pivots[pivot] + return len(pivots) + + +def inverse(rows): + n = len(rows) + augmented = [row | (1 << (n + i)) for i, row in enumerate(rows)] + for j in range(n): + pivot = next((i for i in range(j, n) if (augmented[i] >> j) & 1), None) + require(pivot is not None, "singular binary matrix") + augmented[j], augmented[pivot] = augmented[pivot], augmented[j] + for i in range(n): + if i != j and (augmented[i] >> j) & 1: + augmented[i] ^= augmented[j] + return [row >> n for row in augmented] + + +def multiply(a, b): + result = [] + for row in a: + value = 0 + for j, b_row in enumerate(b): + if (row >> j) & 1: + value ^= b_row + result.append(value) + return result + + +def columns(rows): + return [sum(((row >> j) & 1) << i for i, row in enumerate(rows)) + for j in range(DIM)] + + +def unit_index(x): + return x.bit_length() - 1 if x and x & (x - 1) == 0 else None + + +def factor_sum(terms): + rows = [0] * DIM + for x, y in terms: + require(0 < x < 512 and 0 < y < 512, "nonzero 9-bit factors") + for i in range(DIM): + if (x >> i) & 1: + rows[i] ^= y + return rows + + +def term_cost(x, y, cheap): + a, b = unit_index(x), unit_index(y) + if a is not None and b is not None and (cheap[a] >> b) & 1: + return 6 + return 7 if a is not None or b is not None else 8 + + +def validate_geometry(lines): + require(len(lines) == len(set(lines)) == 120, "120 distinct lines") + require(all(len(line) == 8 and dot(line, line) == 4 for line in lines), + "root norms") + require(all(dot(a, b) % 2 == 0 for a in lines for b in lines), "integral Gram") + require(all(abs(dot(lines[i], lines[j])) <= 2 + for i in range(120) for j in range(i)), "off-diagonal Gram") + + +def validate_word(lines, word): + live = [i for i in range(120) if i not in PUNCTURES] + require(word["punctured"] == list(PUNCTURES), "word punctures") + require(word["ports_geom"] == live, "word port order") + require(word["lines"] == [list(lines[i]) for i in live], "word geometry") + + +def validate_algebra(c, m, cheap): + require(len(c) == len(m) == len(cheap) == DIM, "matrix dimensions") + require(all(0 <= row < 512 for rows in (c, m, cheap) for row in rows), "matrix bits") + require(columns(c) == c, "symmetric C") + require(all((row >> i) & 1 for i, row in enumerate(c)), "unit diagonal C") + require(multiply(c, m) == multiply(m, c) == IDENTITY, "inverse identity") + require(cheap == [row ^ (1 << i) for i, row in enumerate(c)], "cheap mask") + return ten_term_obstructions(m, cheap) + + +def ten_term_obstructions(m, cheap): + diagonal = [i for i, row in enumerate(m) if (row >> i) & 1] + require(len(diagonal) > 2, "ten-term diagonal obstruction") + # A 2x2 block untouched by ANY cost-six term, yet rank two in M. + block = (3, 5) + require(all(((cheap[i] >> j) & 1) == 0 for i in block for j in block), + "ten-term forbidden block") + require(all(((m[i] >> j) & 1) == int(i == j) for i in block for j in block), + "ten-term rank-two block") + return diagonal, list(block) + + +def validate_factorization(terms, m, cheap, expected_cost=None): + require(factor_sum(terms) == m, "factorization identity") + counts = Counter(term_cost(x, y, cheap) for x, y in terms) + cost = sum(k * v for k, v in counts.items()) + if expected_cost is not None: + require(cost == expected_cost, "factorization price") + if len(terms) == DIM: + require(binary_rank(x for x, _ in terms) == DIM, "X basis") + require(binary_rank(y for _, y in terms) == DIM, "Y basis") + require(counts[6] <= counts[8], "nine-term discount compensation") + return cost, counts + + +def budget_cases(diagonal_size): + cases = [] + for n in (9, 10): + for n6 in range(n + 1): + for n8 in range(n - n6 + 1): + n7 = n - n6 - n8 + cost = 6 * n6 + 7 * n7 + 8 * n8 + if cost > 62: + continue + if n == 9: + require(n6 > n8, "nine-term budget exclusion") + reason = "basis-counting" + elif n8 == 0: + require(n7 < diagonal_size, "ten-term diagonal budget exclusion") + reason = "diagonal-support" + else: + require((n6, n7, n8) == (9, 0, 1), "ten-term remaining budget") + reason = "rank-two-block" + cases.append({"n": n, "counts_6_7_8": [n6, n7, n8], + "cost": cost, "excluded_by": reason}) + return cases + + +def source_pins(): + manifest = json.loads((HERE / "SOURCES.json").read_text()) + for path, expected in manifest["local_sha256"].items(): + require(hashlib.sha256((ROOT / path).read_bytes()).hexdigest() == expected, + "source pin: " + path) + return manifest + + +def verify(): + manifest = source_pins() + lines = roots() + validate_geometry(lines) + word = json.loads(gzip.decompress((ROOT / WORD).read_bytes())) + validate_word(lines, word) + live = [i for i in range(120) if i not in PUNCTURES] + gram = [[dot(a, b) // 2 for b in lines] for a in lines] + b = [sum(((1 + value) % 2) << j for j, value in enumerate(row)) for row in gram] + c = [sum(((b[i] >> j) & 1) << k for k, j in enumerate(PUNCTURES)) + for i in PUNCTURES] + m = inverse(c) + w = [sum(((b[i] >> j) & 1) << k for k, j in enumerate(PUNCTURES)) for i in live] + require(binary_rank(w) == DIM, "full-rank live label coordinates") + wm = multiply(w, m) + require(all(parity(wm[i] & w[j]) == ((b[s] >> t) & 1) + for i, s in enumerate(live) for j, t in enumerate(live)), "live decoder factor") + + support_bases, rank_counts = {}, Counter() + for x in range(1, 512): + support = [lines[i] for i, row in zip(live, w) if parity(row & x)] + basis = rational_basis(support) + support_bases[x] = basis + rank_counts[len(basis)] += 1 + a = unit_index(x) + require(len(basis) == (7 if a is not None else 8), "support rank classification") + if a is not None: + require(all(dot(v, lines[PUNCTURES[a]]) == 0 for v in support), "support hyperplane") + # For full spans the nondegenerate Q^8 pairing has rank equal to the other + # span's dimension. Only these 81 hyperplane/hyperplane pairs remain. + pair_ranks, cheap = [], [] + for a in range(DIM): + ranks, mask = [], 0 + for d in range(DIM): + left, right = support_bases[1 << a], support_bases[1 << d] + pairing = [[dot(v, u) for u in right] for v in left] + rank = len(rational_basis(pairing)) + expected = 6 if a != d and gram[PUNCTURES[a]][PUNCTURES[d]] == 0 else 7 + require(rank == expected, "pairing rank classification") + ranks.append(rank) + if rank == 6: + mask |= 1 << d + pair_ranks.append(ranks) + cheap.append(mask) + diagonal, block = validate_algebra(c, m, cheap) + histogram = Counter(term_cost(x, y, cheap) for x in range(1, 512) for y in range(1, 512)) + star = list(zip(columns(m), IDENTITY)) + require(all(x.bit_count() > 1 for x, _ in star), "nonunit star reader columns") + validate_factorization(star, m, cheap, 63) + cases = budget_cases(len(diagonal)) + + # Calibration: other decompositions of this same M, never used as a proof + # of the universal nine-term argument. A fixed seed makes them reproducible. + rng = random.Random(45) + x_rows = IDENTITY.copy() + prices = Counter() + for _ in range(128): + for _ in range(9): + a, d = rng.sample(range(DIM), 2) + x_rows[a] ^= x_rows[d] + y_transpose = multiply(inverse(x_rows), m) + cost, _ = validate_factorization(list(zip(columns(x_rows), y_transpose)), m, cheap) + prices[cost] += 1 + + controls = [] + + def reject(name, function): + try: + function() + except Rejected: + controls.append(name) + else: + raise Rejected("negative control accepted: " + name) + + bad_lines = lines.copy() + bad_lines[45] = (0,) * 8 + reject("zero-root", lambda: validate_geometry(bad_lines)) + bad_word = dict(word, punctured=list(PUNCTURES[:-1]) + [115]) + reject("wrong-puncture", lambda: validate_word(lines, bad_word)) + bad_c = c.copy() + bad_c[0] ^= 1 + reject("missing-diagonal-premise", lambda: validate_algebra(bad_c, m, cheap)) + bad_m = m.copy() + bad_m[0] ^= 1 + reject("wrong-inverse", lambda: validate_algebra(c, bad_m, cheap)) + bad_cheap = cheap.copy() + bad_cheap[3] |= 1 << 5 + reject("forbidden-pair-discount", lambda: validate_algebra(c, m, bad_cheap)) + reject("omitted-star-total", lambda: validate_factorization(star[:-1], m, cheap)) + reject("underpriced-star", lambda: validate_factorization(star, m, cheap, 62)) + changed_star = star.copy() + changed_star[0] = (changed_star[0][0] ^ 1, changed_star[0][1]) + reject("changed-source-functional", lambda: validate_factorization(changed_star, m, cheap)) + # Dropping all nine punctures is essential: at least one omitted direction + # has full support rank in the unpunctured 120-line geometry. + full_support = [lines[i] for i in range(120) if (b[i] >> PUNCTURES[0]) & 1] + reject("unpunctured-rank-seven", lambda: require(len(rational_basis(full_support)) == 7, + "unpunctured rank is eight")) + missing_diagonal = [row & ~(1 << i) for i, row in enumerate(m)] + reject("missing-diagonal-obstruction", lambda: ten_term_obstructions(missing_diagonal, cheap)) + missing_block = m.copy() + missing_block[3] ^= 1 << 5 + missing_block[5] ^= 1 << 3 + reject("rank-one-in-place-of-rank-two", lambda: ten_term_obstructions(missing_block, cheap)) + # A second abstract algebra instance is accepted, and a determinant-one + # rational rank example cannot collapse through floating-point rounding. + validate_algebra(IDENTITY, IDENTITY, [0] * DIM) + big = 2 ** 54 + require(len(rational_basis([[big, big - 1], [big + 1, big]])) == 2, "exact rank control") + legacy_lines = roots(supplier_order=False) + require(set(legacy_lines) == set(lines), "same E8 root set") + reject("different-line-numbering", lambda: validate_word(legacy_lines, word)) + legacy_indices = {line: i for i, line in enumerate(legacy_lines)} + mapped_punctures = [legacy_indices[lines[i]] for i in PUNCTURES] + legacy_cheap_pairs = sum(a != d and dot(legacy_lines[a], legacy_lines[d]) == 0 + for a in PUNCTURES for d in PUNCTURES) + + return { + "status": "PASS_P111_PAIRING_FLOOR", + "base_commit": manifest["base_commit"], + "punctures": list(PUNCTURES), + "conventions": "bit j is column j; puncture positions and ports are zero-based", + "C_rows": c, "M_inverse_rows": m, "cheap_rows": cheap, + "numbering_control": {"supplier_punctures_in_sorted_tetrad_order": mapped_punctures, + "unchanged_indices_in_sorted_order_cheap_pairs": legacy_cheap_pairs, + "actual_supplier_cheap_pairs": histogram[6]}, + "live_label_rank": binary_rank(w), "live_decoder_entries": len(live) ** 2, + "support_ranks": dict(sorted(rank_counts.items())), + "unit_pair_ranks": pair_ranks, + "term_cost_histogram": dict(sorted(histogram.items())), + "diagonal_ones": diagonal, "forbidden_identity_block": block, + "excluded_budgets_at_most_62": cases, + "terms_below_nine": "excluded by rank(M)=9", + "terms_at_least_eleven": "cost at least 6*n >= 66", + "attaining_star": [{"x": x, "y": y, "cost": term_cost(x, y, cheap)} for x, y in star], + "minimum_pairing_cost": 63, + "calibration_seed": 45, "calibration_nine_term_prices": dict(sorted(prices.items())), + "negative_controls": controls, + "scope": "Fixed B0 label factorizations on this P111 geometry; no new kappa or physical word", + } + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--write", type=Path, help="write the deterministic receipt instead of comparing it") + args = parser.parse_args() + result = verify() + payload = json.dumps(result, indent=2, sort_keys=True) + "\n" + if args.write: + args.write.write_text(payload) + else: + require(payload == (HERE / "RESULTS.json").read_text(), "committed receipt differs") + print("PASS_P111_PAIRING_FLOOR: cost 63; 511 exact supports; 261121 support pairs; " + + str(len(result["negative_controls"])) + " negative controls") + + +if __name__ == "__main__": + main()