From aeaf0899179a14644b412e838ede14db967c765e Mon Sep 17 00:00:00 2001 From: Alishan Ladhani Date: Tue, 13 Oct 2026 01:01:30 -0400 Subject: [PATCH] Research: classify optimal 240-port global-star punctures --- .../global-star-punctures/CERTIFICATE.json | 493 ++++++++++++++++++ research/global-star-punctures/CLAIM.json | 38 ++ research/global-star-punctures/README.md | 228 ++++++++ research/global-star-punctures/SOURCES.json | 65 +++ research/global-star-punctures/VALIDATION.md | 51 ++ .../build_certificate.py | 106 ++++ research/global-star-punctures/test_verify.py | 138 +++++ research/global-star-punctures/verify.py | 220 ++++++++ 8 files changed, 1339 insertions(+) create mode 100644 research/global-star-punctures/CERTIFICATE.json create mode 100644 research/global-star-punctures/CLAIM.json create mode 100644 research/global-star-punctures/README.md create mode 100644 research/global-star-punctures/SOURCES.json create mode 100644 research/global-star-punctures/VALIDATION.md create mode 100644 research/global-star-punctures/build_certificate.py create mode 100644 research/global-star-punctures/test_verify.py create mode 100644 research/global-star-punctures/verify.py diff --git a/research/global-star-punctures/CERTIFICATE.json b/research/global-star-punctures/CERTIFICATE.json new file mode 100644 index 0000000000..b8629f52b1 --- /dev/null +++ b/research/global-star-punctures/CERTIFICATE.json @@ -0,0 +1,493 @@ +{ + "format": "global-star-punctures-v1", + "assignment_seed": 42, + "instance": { + "p": 6, + "k": 4, + "target_index": 42, + "target_coordinates": [ + 1, + 2, + 5, + 10 + ], + "port_order": "pair combinations lexicographic, then sign tuples lexicographic; coordinate 2*pair+sign" + }, + "code": { + "ports": 240, + "proper_stars": 232, + "overlap_corrections": 3, + "rank": 155, + "dual_rank": 85, + "independent_star_indices": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 8, + 9, + 10, + 12, + 13, + 14, + 15, + 16, + 17, + 18, + 19, + 20, + 21, + 22, + 23, + 24, + 25, + 26, + 27, + 28, + 30, + 32, + 33, + 34, + 35, + 36, + 37, + 38, + 39, + 40, + 41, + 42, + 43, + 44, + 46, + 48, + 49, + 50, + 51, + 52, + 53, + 54, + 55, + 56, + 58, + 60, + 61, + 62, + 64, + 66, + 68, + 72, + 73, + 74, + 75, + 76, + 77, + 78, + 79, + 80, + 81, + 82, + 83, + 84, + 85, + 86, + 88, + 89, + 90, + 91, + 92, + 93, + 94, + 96, + 98, + 100, + 102, + 104, + 105, + 106, + 107, + 108, + 109, + 110, + 112, + 113, + 114, + 115, + 116, + 117, + 118, + 120, + 122, + 124, + 126, + 128, + 129, + 130, + 132, + 133, + 134, + 136, + 138, + 140, + 142, + 144, + 148, + 152, + 153, + 154, + 155, + 156, + 157, + 158, + 160, + 161, + 162, + 163, + 164, + 165, + 166, + 168, + 170, + 172, + 174, + 176, + 177, + 178, + 180, + 181, + 182, + 184, + 186, + 188, + 190, + 192, + 196, + 200, + 201, + 202, + 204, + 208, + 210, + 212, + 216, + 220, + 224 + ], + "information_set": [ + 7, + 11, + 13, + 14, + 15, + 23, + 27, + 29, + 30, + 31, + 33, + 35, + 37, + 39, + 41, + 43, + 45, + 46, + 47, + 51, + 55, + 59, + 61, + 62, + 63, + 65, + 67, + 69, + 71, + 73, + 75, + 77, + 78, + 79, + 81, + 82, + 83, + 85, + 86, + 87, + 89, + 90, + 91, + 93, + 94, + 95, + 99, + 101, + 102, + 103, + 107, + 109, + 110, + 111, + 113, + 115, + 117, + 118, + 119, + 121, + 123, + 125, + 126, + 127, + 129, + 130, + 131, + 133, + 134, + 135, + 137, + 138, + 139, + 141, + 142, + 143, + 145, + 146, + 147, + 148, + 149, + 150, + 151, + 153, + 154, + 155, + 156, + 157, + 158, + 159, + 163, + 165, + 166, + 167, + 169, + 170, + 171, + 172, + 173, + 174, + 175, + 177, + 179, + 181, + 182, + 183, + 185, + 186, + 187, + 188, + 189, + 190, + 191, + 193, + 194, + 195, + 197, + 198, + 199, + 201, + 202, + 203, + 204, + 205, + 206, + 207, + 209, + 210, + 211, + 212, + 213, + 214, + 215, + 217, + 218, + 219, + 220, + 221, + 222, + 223, + 225, + 226, + 227, + 228, + 229, + 230, + 231, + 232, + 233, + 234, + 235, + 236, + 237, + 238, + 239 + ], + "parity_checks_hex": [ + "888888888888aaaa82288888888800aa28288888a00a888828820000e881", + "000000008888000088880000888800008888888800008888288200002882", + "0000888800000000a0a0888800000000a0a08888a00a8888888800004884", + "000000000000000000000000000000000000888800008888888800008888", + "8888000000000000aa008888888800aa28280000a0a00000a0a000006090", + "000000000000000000000000888800008888000000000000a0a00000a0a0", + "00000000000000000000888800000000a0a00000a0a0000000000000c0c0", + "888888888888aaaa822800000000aa0000000000aa000000aa0000006900", + "000000008888000088880000000000000000000000000000aa000000aa00", + "0000888800000000a0a000000000000000000000aa00000000000000cc00", + "8888000000000000aa0000000000aa00000000000000000000000000f000", + "a0a0a0a0aaaa88888448a0a000aa88884848a00a888888882882e8810000", + "000000000000888888880000000088888888000088888888288228820000", + "0000a0a000000000c0c0a0a000000000c0c0a00a88888888888848840000", + "000000000000000000000000000000000000000088888888888888880000", + "a0a0000000000000cc00a0a000aa88884848a0a000000000a0a060900000", + "000000000000000000000000000088888888000000000000a0a0a0a00000", + "00000000000000000000a0a000000000c0c0a0a0000000000000c0c00000", + "a0a0a0a0aaaa888884480000aa0000000000aa0000000000aa0069000000", + "000000000000888888880000000000000000000000000000aa00aa000000", + "0000a0a000000000c0c00000000000000000aa00000000000000cc000000", + "a0a0000000000000cc000000aa00000000000000000000000000f0000000", + "c0c0c0c0cccc0cc00000c0c000ccc0c00000c00c00000000c00300000000", + "0000c0c00000c0c00000c0c00000c0c00000c00c00000000c00c00000000", + "c0c000000000cc000000c0c000ccc0c00000c0c000000000c03000000000", + "00000000000000000000c0c00000c0c00000c0c000000000c0c000000000", + "c0c0c0c0cccc0cc000000000cc0000000000cc0000000000c30000000000", + "0000c0c00000c0c000000000000000000000cc0000000000cc0000000000", + "c0c000000000cc0000000000cc0000000000000000000000f00000000000", + "aa00aaaaa0a0a0a0906000aaa0a0a0a06060a00aa00a6009000000000000", + "000000000000a0a0a0a000000000a0a0a0a00000a00aa00a000000000000", + "00000000a0a00000c0c00000a0a00000c0c0a00a0000c00c000000000000", + "aa00000000000000f00000aaa0a0a0a06060a0a0a0a06090000000000000", + "0000000000000000000000000000a0a0a0a00000a0a0a0a0000000000000", + "000000000000000000000000a0a00000c0c0a0a00000c0c0000000000000", + "aa00aaaaa0a0a0a09060aa00000000000000aa00aa006900000000000000", + "000000000000a0a0a0a000000000000000000000aa00aa00000000000000", + "00000000a0a00000c0c00000000000000000aa000000cc00000000000000", + "aa00000000000000f000aa0000000000000000000000f000000000000000", + "cc00ccccc0c030c0000000ccc0c0c0c00000c00cc0030000000000000000", + "00000000c0c0c0c000000000c0c0c0c00000c00cc00c0000000000000000", + "cc0000000000f000000000ccc0c0c0c00000c0c0c0300000000000000000", + "000000000000000000000000c0c0c0c00000c0c0c0c00000000000000000", + "cc00ccccc0c030c00000cc00000000000000cc00c3000000000000000000", + "00000000c0c0c0c000000000000000000000cc00cc000000000000000000", + "cc0000000000f0000000cc000000000000000000f0000000000000000000", + "f000f0f0f0000000000000f0000000000000000f00000000000000000000", + "f0000000f0000000000000f000000000000000f000000000000000000000", + "f000f0f0f00000000000f0000000000000000f0000000000000000000000", + "f0000000f00000000000f000000000000000f00000000000000000000000", + "aaaaaa00aa00aa00960000aa00aa00aa0069000000000000000000000000", + "000000000000aa00aa000000000000aa00aa000000000000000000000000", + "00000000aa000000cc00000000aa000000cc000000000000000000000000", + "0000aa0000000000f00000aa0000000000f0000000000000000000000000", + "aaaaaa00aa00aa009600aa00aa00aa006900000000000000000000000000", + "000000000000aa00aa0000000000aa00aa00000000000000000000000000", + "00000000aa000000cc000000aa000000cc00000000000000000000000000", + "0000aa0000000000f000aa0000000000f000000000000000000000000000", + "cccccc00cc003c00000000cc00cc00c30000000000000000000000000000", + "00000000cc00cc000000000000cc00cc0000000000000000000000000000", + "0000cc000000f000000000cc000000f00000000000000000000000000000", + "cccccc00cc003c000000cc00cc00c3000000000000000000000000000000", + "00000000cc00cc0000000000cc00cc000000000000000000000000000000", + "0000cc000000f0000000cc000000f0000000000000000000000000000000", + "f0f0f000f0000000000000f0000f00000000000000000000000000000000", + "0000f000f0000000000000f000f000000000000000000000000000000000", + "f0f0f000f00000000000f0000f0000000000000000000000000000000000", + "0000f000f00000000000f000f00000000000000000000000000000000000", + "ff00000000000000000000ff000000000000000000000000000000000000", + "ff000000000000000000ff00000000000000000000000000000000000000", + "aaaaaaaaaaaaaaaa96690000000000000000000000000000000000000000", + "000000000000aaaaaaaa0000000000000000000000000000000000000000", + "00000000aaaa0000cccc0000000000000000000000000000000000000000", + "0000aaaa00000000f0f00000000000000000000000000000000000000000", + "aaaa000000000000ff000000000000000000000000000000000000000000", + "cccccccccccc3cc300000000000000000000000000000000000000000000", + "00000000cccccccc00000000000000000000000000000000000000000000", + "0000cccc0000f0f000000000000000000000000000000000000000000000", + "cccc00000000ff0000000000000000000000000000000000000000000000", + "f0f0f0f0f00f000000000000000000000000000000000000000000000000", + "0000f0f0f0f0000000000000000000000000000000000000000000000000", + "f0f00000ff00000000000000000000000000000000000000000000000000", + "ff0000ff0000000000000000000000000000000000000000000000000000", + "ff00ff000000000000000000000000000000000000000000000000000000", + "ffff00000000000000000000000000000000000000000000000000000000" + ], + "empty_star_in_span": true + }, + "enumeration": { + "other_ports": 239, + "pairs": 28441, + "zero_single_pair_syndromes": 28681, + "translated_intersections": 0, + "triples": 2246839, + "triple_pair_hits": 40, + "optimal_deletion_sets": 4, + "minimum_deletions": 5 + }, + "optimal_deletions": [ + { + "deleted_indices": [ + 10, + 11, + 26, + 27, + 43 + ], + "star_coordinates": [ + 1, + 2, + 5 + ] + }, + { + "deleted_indices": [ + 34, + 180, + 182, + 196, + 198 + ], + "star_coordinates": [ + 2, + 5, + 10 + ] + }, + { + "deleted_indices": [ + 40, + 72, + 74, + 88, + 90 + ], + "star_coordinates": [ + 1, + 2, + 10 + ] + }, + { + "deleted_indices": [ + 46, + 124, + 126, + 140, + 142 + ], + "star_coordinates": [ + 1, + 5, + 10 + ] + } + ] +} diff --git a/research/global-star-punctures/CLAIM.json b/research/global-star-punctures/CLAIM.json new file mode 100644 index 0000000000..573bc41964 --- /dev/null +++ b/research/global-star-punctures/CLAIM.json @@ -0,0 +1,38 @@ +{ + "track": "Structural decoder research", + "assignment_seed": 42, + "random_source": "OS randomness via secrets.randbelow(100), drawn once", + "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "claimed_at_utc": "2026-10-13T04:43:35.636860+00:00", + "expected_finish_utc": "2026-10-13T05:25:00Z", + "coordination": "No pinned issue; sole open issue #650 concerns Discussions. Local claim used.", + "candidates": [ + "E8 mixed-port extensions beyond the minimal puncture equality case (adjacent to #715)", + "Off-target proper stars after puncturing paired hypercubes (explicitly outside #669 Theorem 2)", + "Alternative cross-stage corrector-rank compression beyond the fixed-role format of #446" + ], + "chosen_object": "One retained target in the (p,k)=(6,4) paired-port family, with arbitrary global proper-star coefficients and uniform overlap-class corrections", + "seed_use": "The tens digit selects k=4 and the units digit selects p-k=2; target index 42 in the documented lexicographic port order.", + "hypothesis": "Allowing off-target proper stars may lower the target-local deletion threshold 2(p-k)+1=5.", + "method": "Exact F2 incidence and dual-certificate calculations; seek a proof or an explicitly bounded finite result with a witness and negative controls.", + "stopping_rule": "One question only; finish experiment by 05:14 UTC and reserve remaining time for verification and handoff. No unbounded parameter sweep.", + "expected_deliverable": "Self-contained scoped research note, exact verifier, deterministic certificate, immutable source pins and one focused PR; no kappa claim.", + "overlap_check": { + "open_pr_count": 535, + "highest_pr": 716, + "relevant_pr": 669, + "relevant_head": "308f1e6ec3bb0b6ec0584cf7bfe219addc219b1e" + }, + "scope_refinement": { + "reason": "Final metadata refresh found concurrent #725 and #732, absent from the initial snapshot.", + "open_pr_count": 551, + "highest_pr": 732, + "new_emphasis": "Complete (6,4) equality classification (only four target-local optima), plus sharp 85-deletion algebraic all-target threshold and explicit information set. The already-completed rank and minimum-distance work is independent corroboration of #732.", + "experiment_changed": false, + "predecessors_credited": [ + 669, + 725, + 732 + ] + } +} diff --git a/research/global-star-punctures/README.md b/research/global-star-punctures/README.md new file mode 100644 index 0000000000..92fbc25377 --- /dev/null +++ b/research/global-star-punctures/README.md @@ -0,0 +1,228 @@ +# Exactly four optimal punctures in the 240-port global star code + +**Scoped negative result / exact finite classification; no new κ.** For the +240 paired ports with four coordinates chosen from six pairs, arbitrary +off-target proper stars do not reduce the five deletions needed to decode one +retained target. There are exactly four optimal deletion sets per target. Each +isolates one of its three-coordinate stars; no additional optimal support is +made possible by off-target stars. + +The same certificate gives the exact **algebraic all-target threshold: 85 +deletions**. The proper-star code has dimension 155. An explicit set of 155 +retained ports admits decoders for every target, while no larger surviving +family does. This is a statement about scalar identities, not their physical +implementation or cost. + +The original question came from Theorem 2 of +[Sam Sung's PR #669](https://github.com/CrocSwap/integer-mult-bounds/pull/669), +which leaves punctured global stars outside its scope. Two contributions +arrived during this experiment: [Luke Mansoor's #732](https://github.com/CrocSwap/integer-mult-bounds/pull/732) +proves the general minimum threshold and independently checks the same +240-port rank and distance; [Sagar Thakrar's #725](https://github.com/CrocSwap/integer-mult-bounds/pull/725) +classifies 67 optimal patterns in the smaller 80-port (5,4) case, only four of +which are target-local. Those threshold/rank results are credited, not claimed +as new here. + +This contribution adds the **complete equality classification for (6,4)**: +all four optimal patterns are target-local, and there are no off-target-only +optima. It also supplies the **sharp algebraic all-target threshold and an +explicit information set**, outside the one-target scope of both concurrent +notes. The overlapping minimum-distance calculation is separately implemented +corroboration. No code or proof from either concurrent package is imported. +The finite classification does not claim a general equality theorem for other +p or k. + +## Model + +There are six pairs `{2i, 2i+1}`, for `0 <= i < 6`. A port S is a four-element +set using four distinct pairs. Let P be all `2^4 * binom(6,4) = 240` ports. +Let D be the deleted ports, F=P\D the surviving ports, and T a retained target. +All input symbols x_S, for S in F, are independent over F₂. + +For every nonempty compatible coordinate set L of size less than four, define + +```text +star_L(F) = sum_{S in F, L subset S} x_S. +C_j(T,F) = sum_{S in F, |S intersect T| = j} x_S, j=1,2,3. +``` + +The allowed decoder is + +```text +x_T = sum_L a_(T,L) star_L(F) + sum_{j=1}^3 b_(T,j) C_j(T,F). +``` + +The 232 star coefficients may vary arbitrarily with both T and L, including +L outside T. The three correction coefficients may vary with T, but remain +uniform within each overlap class. No degree-four star or correction C_4 is +allowed: either would directly supply x_T. The global sum is optional here; +the certificate proves that it already belongs to the proper-star span for +this instance. Both stars and corrections are recomputed on F after deletion. + +## Why the problem reduces to one binary code + +Put `A_l(T,F) = sum_{L subset T, |L|=l} star_L(F)`. Coefficient comparison at +every surviving source gives + +```text +C_1 = A_1 + A_3, C_2 = A_2 + A_3, C_3 = A_3. +``` + +For a source intersecting T in r coordinates, A_l has coefficient +`binom(r,l) mod 2`. Substitution for r=0,...,4 proves these identities, +including r=4 where each right-hand side is zero. Deleting sources just +restricts these pointwise identities. Thus the correction columns add no +freedom, even after puncturing. + +Let C be the span in F₂^240 of all proper-star incidence vectors on P. A +decoder on F exists for T exactly when some c in C has c_T=1 and +`support(c) subset {T} union D`. This equivalence does not assume a symmetric +decoder, a bound on the number of totals, or an efficient implementation. + +## Certificate and exhaustive finite argument + +[CERTIFICATE.json](CERTIFICATE.json) contains 155 independent proper stars, +85 independent parity checks H, an information set of 155 ports, and the four +optimal puncture witnesses. The builder and verifier are separate programs; +the verifier does not import or execute the builder or a predecessor checker. + +The verifier independently constructs the coordinate sets and incidence +supports. It checks that every parity row annihilates **every** proper star +and overlap correction, and checks the two ranks using set elimination. +Since `155 + 85 = 240`, this proves `C = kernel(H)` and `dim(C)=155`. +It also checks H against the global sum. No solver status is trusted. + +Let h_i be column i of H. The assignment seed selects target index 42 in the +specified ordering (pair combinations, then sign tuples). Define A to contain +zero, every non-target h_i, and every sum h_i+h_j of distinct non-target +columns. Its **28,681 elements are all distinct**: + +```text +1 + 239 + binom(239,2) = 28,681. +``` + +Every set D of at most four non-target ports splits into two parts of size at +most two. Therefore `h_T = sum_{i in D} h_i` would imply +`A intersect (h_T+A)` is nonempty. The checker exhausts this intersection and +finds it empty. This excludes every allowed decoder with at most four +deletions, across all `2^155` codewords, without enumerating their coefficients. + +At the boundary, the checker exhausts all **2,246,839 triples** of non-target +ports and looks up the complementary pair syndrome. Unique pair syndromes +make this lookup lossless. Exactly 40 hits yield four distinct five-element +sets, each appearing `binom(5,2)=10` times. Overlapping pairs and triples are +handled by symmetric difference; they would produce a smaller support and +are rejected. Every five-element support has such a partition, so the census +is complete. Its fixed stopping rule is exhaustion of these lists, not a time +limit or a heuristic search. + +For each resulting set D, a three-coordinate J contained in T satisfies +`star_J(F)=x_T`. The verifier checks every surviving source coefficient. These +four J are exactly the four triples in T. Equivalently, D consists of the five +other ports containing J. The fifth deletion is necessary: restoring any one +of them breaks the identity, and the direct equation solver also rejects it. + +Permutations of the six coordinate pairs and independent swaps within pairs +act transitively on ports and preserve the full star family and overlap +classes. Hence the result for index 42 applies to **every target** in this +fixed geometry. Every nonzero codeword contains a target, so C has minimum +distance six; its minimum words are precisely the 160 triple-star supports +(`240 * 4 / 6 = 160`, also `2^3 * binom(6,3)`). This is a finite, +computer-assisted classification, not a formalized proof of multiplication. + +## All-target corollary + +For a surviving family F, the available decoder vectors are the projection +`C|F`, including all the correction classes by the identities above. Decoding +every target requires all unit vectors and thus `C|F = F₂^F`. Its dimension is +at most 155, so `|F| <= 155`: at least 85 ports must be deleted. + +The certificate's `information_set` attains this. Restricting its 155 +independent star rows to those 155 coordinates has rank 155. The independent +tests additionally solve for all 155 unit vectors and check their literal +incidences. These are algebraic decoders with unrestricted star use. No +favorable copy cost, frame schedule, or restoration circuit is inferred. + +## Reproduce + +Python 3.9 or newer, standard library only; no downloads or external solvers: + +```sh +python3 -I -B research/global-star-punctures/verify.py +``` + +Expected final line: + +```text +PASS_GLOBAL_STAR_PUNCTURES ports=240 rank=155 dual=85 minimum_deletions=5 optimal_sets=4 all_target_deletions=85 triples=2246839 controls=8 restored_ports=20 kappa=unchanged +``` + +Eight default negative-control categories cover a changed parity bit, +dependent dual rows, duplicate primal rows, omitted minimum supports, +incomplete coverage receipts, deletion of the target, all 20 one-port +restorations, and a wrong coordinate sign. Checks remain active under `-O`. + +Additional direct equation checks and certificate regeneration: + +```sh +python3 -I -O -B research/global-star-punctures/test_verify.py +python3 -I -B research/global-star-punctures/build_certificate.py --output /tmp/global-star-certificate.json +cmp research/global-star-punctures/CERTIFICATE.json /tmp/global-star-certificate.json +``` + +The five test groups use an independent ternary-word port enumeration and +solve the actual decoder equations, without parity certificates, for all four +optima, their 20 one-port restorations, and 20 wrong five-port punctures. They +also check all 155 information-set targets, positive controls outside the +obstruction (degree-four stars, k=3, and p=k=4 with one puncture), the vacuity +of dropping the target equation, and optimized subprocess rejection of four +corrupted certificates. See [VALIDATION.md](VALIDATION.md) for actual runs. + +## Scope, budget, provenance and credit + +The proposed escape was to allow off-target stars to beat the known +target-local puncture threshold. It fails here already at scalar exactness. +Giving helpers, source access, frame changes, copies, restoration and recursive +children zero cost cannot make the excluded identities hold. The attaining +five-deletion witnesses are the predecessor's isolated-star mechanism; their +paid implementation is not supplied. The 85-deletion information set is not +a proposed improved supplier, and no complete-cost or κ improvement is claimed. + +Other p or k, higher-degree totals, source-dependent correction coefficients, +other fields/geometries, nonlinear decoders and alternative stage structures +remain outside this result. No global bound on integer multiplication follows. + +Exact base: `66849e1475c930fd7732b1a0067ffee7e1e95f60`. +[SOURCES.json](SOURCES.json) pins the predecessor heads and inspected source +bytes. [CLAIM.json](CLAIM.json) records the OS-random seed **42**, three candidate +tasks, selected object, stopping rule, and overlap checks. No pinned sprint +issue existed. Only this package is added; `upstream/` and the frontier are +unchanged. The accepted conditional κ remains +`51110230636731/31250000000000000 = 0.001635527380375392`, from #626/#622/#623 +with #543. Its construction was read for context, not re-certified here. +All inherited compiler, common-label/mutable-basis, hosting, restoration, +precision/tape/recovery and analytic obligations remain. + +Credit: Joel Pulikkan / GamingPuzzled's +[#231](https://github.com/CrocSwap/integer-mult-bounds/pull/231) supplied the +symmetric parity obstruction, following icekylinx's #144 and eumemic's paired +cube identity. Sam Sung / @the-missionary-company's +[#669](https://github.com/CrocSwap/integer-mult-bounds/pull/669), pinned at +`308f1e6ec3bb0b6ec0584cf7bfe219addc219b1e`, supplied the global unpunctured +obstruction, target-local puncture theorem, and explicit remaining question. +No predecessor code is copied or executed. E8 puncture and extension work in +#620/#631/#715 has a different geometry and was checked for overlap. + +Concurrent credit: **Luke Mansoor (@lukemansoor), #732**, at +`80431a74c31e807581f5c2258c87abe2084caacd`, supplies the general star-code +distance theorem and the same (6,4) rank/distance. **Sagar Thakrar +(@thakrarsagar), #725**, at `6eadc4eb4ebc355b13fa36a3138d97a583ea7f37`, +supplies the (5,4) equality classification. Their source README hashes are +pinned in SOURCES.json. The change in emphasis after their arrival is recorded +in CLAIM.json; the scientific certificate and its enumeration domain did not +change. + +Prepared by **Alishan Ladhani (@aladh)** with substantial **OpenAI Codex +assistance** in research, proofs, implementation, verification and writing. +No independent human peer review is claimed. New files are under the +repository's [Apache-2.0 license](../../LICENSE). diff --git a/research/global-star-punctures/SOURCES.json b/research/global-star-punctures/SOURCES.json new file mode 100644 index 0000000000..a94f4c68d2 --- /dev/null +++ b/research/global-star-punctures/SOURCES.json @@ -0,0 +1,65 @@ +{ + "repository": "https://github.com/CrocSwap/integer-mult-bounds", + "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "context_sha256_at_base": { + "CONTRIBUTING.md": "a10dd640ec6f4b1d8b6acc31220af512335dc093f634cd25f601acb07ac53d53", + "certificates/selected-result.json": "b3bf402f31a69bde0629936a9b569bed48281568d7b16d5fba120b5311ea1f53", + "docs/research/current-status.md": "197319a6edf04340ec3623d09d03714fcd6a981359f22bdcefdd06e7e2f4174d", + "docs/research/pr-ledger.md": "2e811684201e08007377ee97b1c35c0f0b3c026dd8207e7b0de3ff7cd1e13a91", + "docs/research/community-k492-review.md": "3b731d30e80010b15408a289b0b32192700885474c8b36d48ee3320a7a8c5c47", + "research/hypercube-decoder-parity/README.md": "2dc89289d1d979aec6709b8c55a2af7cd39d97297bc20fb94adc7d4cdf867cd1", + "research/hypercube-decoder-parity/check.py": "82b7ad8d54662db3e159301aaf3cf87edfbe934b6ed5bdc01243812966b2ea40", + "research/community-k492-audit/pr626/replay/ASSEMBLY.json": "6127732e2fcdd470dab349c1c51d03cd9f0787ad0309b1b4a7c811a908028f4e" + }, + "predecessors": [ + { + "pr": 231, + "head": "3c11e696a2fb2c454585d72710de27cd6bd3be68", + "author": "Joel Pulikkan / GamingPuzzled", + "contribution": "Symmetric paired-hypercube parity obstruction; retained in main." + }, + { + "pr": 669, + "head": "308f1e6ec3bb0b6ec0584cf7bfe219addc219b1e", + "author": "Sam Sung / the-missionary-company", + "contribution": "Global full-family obstruction and target-local puncture theorem; explicitly leaves global punctures outside its scope.", + "path": "research/asymmetric-hypercube-decoder/README.md", + "sha256": "69b624112d6294f519682fdf762d7f670063ea3f2b05ec0f25ce26e93c481c17" + } + ], + "selected_context": { + "kappa": "51110230636731/31250000000000000", + "decimal": "0.001635527380375392", + "source_prs": [ + 626, + 623, + 622, + 543 + ], + "pr626_head": "660de893d27bb7abd1d5b01b1640207528a5c851", + "scope": "Context only; this package does not replay the selected supplier." + }, + "dependencies": "Python >=3.9 standard library. No predecessor code, external solver, or downloaded data is imported at runtime.", + "pin_scope": "Historical source/context pins, not a requirement that later main retain these selected-status bytes. The complete scientific instance is specified in README.md and CERTIFICATE.json.", + "contributor": "Alishan Ladhani (@aladh)", + "ai_assistance": "Substantial OpenAI Codex assistance in research, proof development, implementation, verification and documentation; no independent human peer review claimed.", + "license": "Apache-2.0", + "concurrent_contributions": [ + { + "pr": 725, + "head": "6eadc4eb4ebc355b13fa36a3138d97a583ea7f37", + "author": "Sagar Thakrar / thakrarsagar", + "contribution": "67 equality cases at (5,4); distinct smaller geometry.", + "path": "research/global-star-puncture/README.md", + "sha256": "b50aa319fff5f22a8b29745d17bac0b9f650f1129310722deea6dbae1d82c7fa" + }, + { + "pr": 732, + "head": "80431a74c31e807581f5c2258c87abe2084caacd", + "author": "Luke Mansoor / lukemansoor", + "contribution": "General minimum-distance theorem and corroborated (6,4) rank/distance; no (6,4) equality classification or all-target information set.", + "path": "research/global-star-puncture/README.md", + "sha256": "87825a4dd666d8c32df025fe838aca4cdc23a5d3965f79c9aca4913567dba6d4" + } + ] +} diff --git a/research/global-star-punctures/VALIDATION.md b/research/global-star-punctures/VALIDATION.md new file mode 100644 index 0000000000..ee55d126f0 --- /dev/null +++ b/research/global-star-punctures/VALIDATION.md @@ -0,0 +1,51 @@ +# Validation receipt + +Scientific base: `66849e1475c930fd7732b1a0067ffee7e1e95f60`. +Local platform: macOS arm64. New package: standard-library Python only. +No Linux CI, Lean, full multiplication theorem, or human peer review is claimed. + +The following passed on **CPython 3.9.6** and **CPython 3.12.14**: + +- Exact certificate verification, including isolated optimized (`-I -O -B`) + execution, all 2,246,839 triples, 40 pair/triple hits, four minimum supports, + both ranks, the 155-port information set, all eight rejection categories, + and all 20 individual restored-port failures. +- All five independent test groups. These directly solve 45 principal decoder + systems (four accepted optima, 20 one-port restorations, 20 wrong five-port + sets, and the full family), check the scope controls, construct all 155 + information-set decoders, and reject four corrupted certificates in + optimized subprocesses. +- Independent certificate generation gives byte-identical JSON across both + Python versions. The verifier imports no generator or predecessor module. + +`make selected-record-check` passed, checking the current exact κ, original +source inventory, and proof supplements. The selected assembly's SHA-256 +matches the selected-result record. The inspected base/source pins are retained +in SOURCES.json. These integrity checks are not a cold supplier replay. + +The repository-wide `make verify` was attempted on a **separate detached +checkout of the unchanged base**, protecting the contribution from generated +artifact changes. It did not complete: + +1. With system Python 3.9.6, the existing copied-reversed producer uses + `int.bit_count`, unavailable on that interpreter. +2. After installing Python 3.12.14 inside the task's scratch directory and + retrying, that existing producer reaches C++ compilation, where the local + compiler cannot find the standard `` header. It exits from + `scripts/endpoint_gauge/match_complex_general.cpp` before the later groups. + +These are observed baseline/environment failures, not a successful full-suite +run or a finding against the mathematics. The Python-only contribution has no +C++ dependency. No further unrelated toolchain repair or repeated aggregate +suite was attempted. `frontier626-verify` was not run separately because no +selected-construction file changes. + +Final clean-package replay, staged whitespace validation and publication +metadata are recorded in the handoff. Only `research/global-star-punctures/` +is added. There are no changes to `upstream/`, existing generators, suppliers, +or the selected-frontier pointer. + +All checks and proof review in this contribution used substantial OpenAI +Codex assistance. The separate direct-equation implementation is an algorithmic +cross-check by the same AI-assisted contributor, not a claim of separate human +review or a proof-assistant result. diff --git a/research/global-star-punctures/build_certificate.py b/research/global-star-punctures/build_certificate.py new file mode 100644 index 0000000000..c8e87c099f --- /dev/null +++ b/research/global-star-punctures/build_certificate.py @@ -0,0 +1,106 @@ +#!/usr/bin/env python3 +"""Construct a finite F2 certificate; the separate verifier imports none of this. + +Copyright 2026 Alishan Ladhani. SPDX-License-Identifier: Apache-2.0 +Prepared with substantial OpenAI Codex assistance. +""" +import argparse +from itertools import combinations, product +import json +from pathlib import Path + + +def ports(p, k): + return [sum(1 << (2 * pair + sign) for pair, sign in zip(pairs, signs)) + for pairs in combinations(range(p), k) + for signs in product((0, 1), repeat=k)] + + +def coordinates(mask): + return [i for i in range(12) if mask >> i & 1] + + +def build(): + family = ports(6, 4) + stars = [s for degree in (1, 2, 3) for s in ports(6, degree)] + generators = [sum(1 << i for i, s in enumerate(family) if s & l == l) + for l in stars] + basis, independent = {}, [] + for index, vector in enumerate(generators): + while vector: + pivot = vector.bit_length() - 1 + if pivot in basis: + vector ^= basis[pivot] + else: + basis[pivot] = vector + independent.append(index) + break + + def remainder(vector): + for pivot in sorted(basis, reverse=True): + if vector >> pivot & 1: + vector ^= basis[pivot] + return vector + + remainders = [remainder(1 << i) for i in range(240)] + free = [i for i in range(240) if i not in basis] + checks = [sum(1 << i for i, r in enumerate(remainders) if r >> f & 1) + for f in free] + syndromes = [sum(1 << j for j, h in enumerate(checks) if h >> i & 1) + for i in range(240)] + target = 42 + other = [i for i in range(240) if i != target] + pair_map = {} + for a, b in combinations(other, 2): + key = syndromes[a] ^ syndromes[b] + if key in pair_map: + raise ValueError("pair syndromes are not unique") + pair_map[key] = (a, b) + short = {0} | {syndromes[i] for i in other} | set(pair_map) + intersections = len(short & {syndromes[target] ^ v for v in short}) + solutions, hits, triples = set(), 0, 0 + for a, b, c in combinations(other, 3): + triples += 1 + pair = pair_map.get(syndromes[target] ^ syndromes[a] ^ syndromes[b] ^ syndromes[c]) + if pair is not None: + deleted = tuple(sorted(set(pair) ^ {a, b, c})) + if len(deleted) != 5: + raise ValueError("unexpected smaller support") + solutions.add(deleted) + hits += 1 + witnesses = [] + for deleted in sorted(solutions): + support = sum(1 << i for i in (target,) + deleted) + matches = [i for i, g in enumerate(generators) if g == support] + if len(matches) != 1: + raise ValueError("minimum support is not a unique proper star") + witnesses.append({"deleted_indices": list(deleted), + "star_coordinates": coordinates(stars[matches[0]])}) + return { + "format": "global-star-punctures-v1", + "assignment_seed": 42, + "instance": {"p": 6, "k": 4, "target_index": target, + "target_coordinates": coordinates(family[target]), + "port_order": "pair combinations lexicographic, then sign tuples lexicographic; coordinate 2*pair+sign"}, + "code": {"ports": 240, "proper_stars": 232, "overlap_corrections": 3, + "rank": len(basis), "dual_rank": len(checks), + "independent_star_indices": independent, + "information_set": sorted(basis), + "parity_checks_hex": [format(h, '060x') for h in checks], + "empty_star_in_span": remainder((1 << 240) - 1) == 0}, + "enumeration": {"other_ports": len(other), "pairs": len(pair_map), + "zero_single_pair_syndromes": len(short), + "translated_intersections": intersections, + "triples": triples, "triple_pair_hits": hits, + "optimal_deletion_sets": len(solutions), + "minimum_deletions": 5}, + "optimal_deletions": witnesses, + } + + +if __name__ == '__main__': + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--output', type=Path, required=True) + args = parser.parse_args() + args.output.write_text(json.dumps(build(), indent=2) + '\n', encoding='utf-8') + print('WROTE_GLOBAL_STAR_PUNCTURES', args.output) diff --git a/research/global-star-punctures/test_verify.py b/research/global-star-punctures/test_verify.py new file mode 100644 index 0000000000..ab08d9feb2 --- /dev/null +++ b/research/global-star-punctures/test_verify.py @@ -0,0 +1,138 @@ +#!/usr/bin/env python3 +"""Direct decoder-equation checks, without the certificate generator or syndromes. + +Copyright 2026 Alishan Ladhani. SPDX-License-Identifier: Apache-2.0 +Prepared with substantial OpenAI Codex assistance. +""" +from itertools import combinations, product +import json +from pathlib import Path +import subprocess +import sys +import tempfile +import unittest + +HERE = Path(__file__).resolve().parent + + +def word_family(p, k): + # Ternary words independently describe absent / first / second coordinates. + # Convert to the certificate's ordering only after generating the family. + family = [tuple(2 * i + x - 1 for i, x in enumerate(word) if x) + for word in product((0, 1, 2), repeat=p) if sum(x != 0 for x in word) == k] + return sorted(family, key=lambda port: (tuple(c // 2 for c in port), tuple(c % 2 for c in port))) + + +def decoder_exists(p, k, target, deleted, include_target_star=False, allow_missing_target=False): + family = word_family(p, k) + if target in deleted and not allow_missing_target: + raise ValueError('target not retained') + terms = [set(s) for d in range(1, k) for s in word_family(p, d)] + if include_target_star: + terms.append(set(family[target])) + rhs = len(terms) + k - 1 + pivots = {} + for index, port in enumerate(family): + if index in deleted: + continue + source = set(port) + row = {i for i, term in enumerate(terms) if term <= source} + overlap = len(source & set(family[target])) + if 0 < overlap < k: + row.add(len(terms) + overlap - 1) + if index == target: + row.add(rhs) + while row: + pivot = min(row) + if pivot == rhs: + return False + if pivot not in pivots: + pivots[pivot] = row + break + row = row ^ pivots[pivot] + return True + + +class DecoderChecks(unittest.TestCase): + @classmethod + def setUpClass(cls): + cls.certificate = json.loads((HERE / 'CERTIFICATE.json').read_text()) + + def test_all_optima_and_every_one_port_restoration(self): + for witness in self.certificate['optimal_deletions']: + deleted = set(witness['deleted_indices']) + self.assertTrue(decoder_exists(6, 4, 42, deleted)) + for restored in deleted: + self.assertFalse(decoder_exists(6, 4, 42, deleted - {restored})) + self.assertFalse(decoder_exists(6, 4, 42, set())) + + def test_same_size_wrong_punctures_fail(self): + for witness in self.certificate['optimal_deletions']: + deleted = set(witness['deleted_indices']) + outside = next(i for i in range(240) if i not in deleted and i != 42) + for removed in deleted: + candidate = deleted - {removed} | {outside} + self.assertFalse(decoder_exists(6, 4, 42, candidate)) + + def test_scope_positive_controls(self): + self.assertTrue(decoder_exists(6, 4, 42, set(), include_target_star=True)) + self.assertTrue(decoder_exists(4, 3, 0, set())) + self.assertTrue(decoder_exists(4, 4, 0, {1})) + with self.assertRaises(ValueError): + decoder_exists(6, 4, 42, {42}) + self.assertTrue(decoder_exists(6, 4, 42, {42}, allow_missing_target=True)) + + def test_information_set_decodes_every_retained_target(self): + # Independently invert the restricted star matrix with coefficient + # tracking, then check all 155 unit vectors against actual incidences. + family = word_family(6, 4) + stars = [set(s) for d in (1, 2, 3) for s in word_family(6, d)] + retained = self.certificate['code']['information_set'] + columns = [{position for position, index in enumerate(retained) + if star <= set(family[index])} for star in stars] + pivots = {} + for i, original in enumerate(columns): + row, coefficients = set(original), {i} + while row: + pivot = min(row) + if pivot in pivots: + row ^= pivots[pivot][0] + coefficients ^= pivots[pivot][1] + else: + pivots[pivot] = row, coefficients + break + self.assertEqual(len(pivots), 155) + for target in range(155): + row, coefficients = {target}, set() + while row: + pivot = min(row) + row ^= pivots[pivot][0] + coefficients ^= pivots[pivot][1] + result = set() + for i in coefficients: + result ^= columns[i] + self.assertEqual(result, {target}) + + def test_certificate_corruption_rejected_under_optimization(self): + with tempfile.TemporaryDirectory() as directory: + for mutation in ('target', 'check', 'coverage', 'solution'): + changed = json.loads(json.dumps(self.certificate)) + if mutation == 'target': + changed['instance']['target_index'] = 41 + elif mutation == 'check': + changed['code']['parity_checks_hex'][0] = '0' * 60 + elif mutation == 'coverage': + changed['enumeration']['triples'] -= 1 + else: + changed['optimal_deletions'].pop() + path = Path(directory) / (mutation + '.json') + path.write_text(json.dumps(changed)) + run = subprocess.run([sys.executable, '-I', '-O', '-B', str(HERE / 'verify.py'), + '--certificate', str(path)], capture_output=True, text=True) + self.assertNotEqual(run.returncode, 0) + self.assertIn('ValueError', run.stderr) + self.assertNotIn('PASS_GLOBAL_STAR_PUNCTURES', run.stdout) + + +if __name__ == '__main__': + unittest.main(verbosity=2) diff --git a/research/global-star-punctures/verify.py b/research/global-star-punctures/verify.py new file mode 100644 index 0000000000..19c94cff18 --- /dev/null +++ b/research/global-star-punctures/verify.py @@ -0,0 +1,220 @@ +#!/usr/bin/env python3 +"""Check the finite certificate using sets and a separately written incidence model. + +Python 3.9+, standard library only. All checks stay active under -O. +Copyright 2026 Alishan Ladhani. SPDX-License-Identifier: Apache-2.0 +Prepared with substantial OpenAI Codex assistance. +""" +import argparse +from copy import deepcopy +from itertools import combinations, product +import json +from math import comb +from pathlib import Path + +HERE = Path(__file__).resolve().parent + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def physical_sets(p, size): + return [frozenset(2 * pair + sign for pair, sign in zip(pairs, signs)) + for pairs in combinations(range(p), size) + for signs in product(range(2), repeat=size)] + + +def sparse_rank(rows): + """Set elimination, independent of the builder's integer-vector reduction.""" + pivots = {} + for original in rows: + row = set(original) + while row: + pivot = min(row) + if pivot in pivots: + row.symmetric_difference_update(pivots[pivot]) + else: + pivots[pivot] = row + break + return len(pivots) + + +def read_model(certificate): + require(certificate['format'] == 'global-star-punctures-v1', 'certificate format') + require(certificate['assignment_seed'] == 42, 'assignment seed') + family = physical_sets(6, 4) + stars = [s for degree in (1, 2, 3) for s in physical_sets(6, degree)] + target = 42 + require(certificate['instance'] == { + 'p': 6, 'k': 4, 'target_index': target, + 'target_coordinates': sorted(family[target]), + 'port_order': 'pair combinations lexicographic, then sign tuples lexicographic; coordinate 2*pair+sign' + }, 'instance or port ordering changed') + supports = [{i for i, source in enumerate(family) if star <= source} for star in stars] + corrections = [{i for i, source in enumerate(family) if len(source & family[target]) == j} + for j in (1, 2, 3)] + code = certificate['code'] + require((code['ports'], code['proper_stars'], code['overlap_corrections']) == (240, 232, 3), + 'generator census') + checks = [] + for encoded in code['parity_checks_hex']: + value = int(encoded, 16) + require(0 < value < 1 << 240 and format(value, '060x') == encoded, 'invalid parity row') + checks.append({i for i in range(240) if value >> i & 1}) + require(len(checks) == code['dual_rank'] == 85, 'dual row count') + require(sparse_rank(checks) == 85, 'dependent parity checks') + for check in checks: + require(all(len(check & support) % 2 == 0 for support in supports + corrections), + 'parity check does not annihilate a generator') + indices = code['independent_star_indices'] + require(len(indices) == len(set(indices)) == code['rank'] == 155, 'primal basis census') + require(all(type(i) is int and 0 <= i < 232 for i in indices), 'primal basis index') + require(sparse_rank(supports[i] for i in indices) == 155, 'dependent primal basis') + require(code['rank'] + code['dual_rank'] == len(family), 'rank-nullity') + retained = code['information_set'] + require(len(retained) == len(set(retained)) == 155 and + all(type(i) is int and 0 <= i < 240 for i in retained), 'invalid information set') + require(sparse_rank(supports[i] & set(retained) for i in indices) == 155, + 'information set is not independent') + # Together the two rank checks prove that ker(H) is exactly the star code. + require(code['empty_star_in_span'] is True and all(len(h) % 2 == 0 for h in checks), + 'empty star span claim') + # Independently verify the written overlap-correction identities on each source. + for j, correction in enumerate(corrections, 1): + expansion = set() + for star, support in zip(stars, supports): + if star <= family[target] and len(star) >= j and comb(len(star), j) % 2: + expansion.symmetric_difference_update(support) + require(expansion == correction, 'overlap correction expansion') + syndromes = [sum(1 << j for j, check in enumerate(checks) if i in check) + for i in range(240)] + return family, target, supports, syndromes + + +def enumerate_supports(syndromes, target): + """Every support of size <=4 splits into two parts of size <=2. + + Every support of size 5 splits into a pair and a triple. XOR permits + overlapping parts; overlaps cancel and cannot conceal a smaller support. + """ + other = [i for i in range(len(syndromes)) if i != target] + singles = [syndromes[i] for i in other] + pairs = {} + for i, j in combinations(other, 2): + syndrome = syndromes[i] ^ syndromes[j] + require(syndrome not in pairs, 'pair syndromes must be unique for this enumerator') + pairs[syndrome] = (i, j) + short = {0, *singles, *pairs} + require(len(short) == 1 + len(other) + comb(len(other), 2), 'short syndromes collide') + intersection_count = sum((syndromes[target] ^ s) in short for s in short) + require(intersection_count == 0, 'a decoder with at most four deletions exists') + solutions, hits, triple_count = set(), 0, 0 + for triple in combinations(other, 3): + triple_count += 1 + value = syndromes[target] + for i in triple: + value ^= syndromes[i] + pair = pairs.get(value) + if pair is not None: + support = tuple(sorted(set(pair).symmetric_difference(triple))) + require(len(support) == 5, 'smaller support appeared at the boundary') + solutions.add(support) + hits += 1 + require(triple_count == comb(len(other), 3), 'incomplete triple coverage') + require(hits == 10 * len(solutions), 'five-set partition multiplicity') + return { + 'other_ports': len(other), 'pairs': len(pairs), + 'zero_single_pair_syndromes': len(short), + 'translated_intersections': intersection_count, + 'triples': triple_count, 'triple_pair_hits': hits, + 'optimal_deletion_sets': len(solutions), 'minimum_deletions': 5, + }, solutions + + +def validate_witness(family, target, witness): + deleted = witness['deleted_indices'] + require(len(deleted) == len(set(deleted)) and all(type(i) is int and 0 <= i < 240 for i in deleted), + 'invalid deletion set') + require(target not in deleted, 'the target must survive') + coordinates = witness['star_coordinates'] + require(len(coordinates) == len(set(coordinates)) == 3, 'witness must be a three-coordinate star') + require(all(type(i) is int and 0 <= i < 12 for i in coordinates), 'invalid coordinate') + star = frozenset(coordinates) + require(len({c // 2 for c in star}) == 3 and star <= family[target], 'invalid target-local star') + survivors = set(range(240)) - set(deleted) + require({i for i in survivors if star <= family[i]} == {target}, + 'witness fails a surviving source coefficient') + + +def check_result(certificate, family, target, enumeration, solutions): + require(certificate['enumeration'] == enumeration, 'enumeration receipt mismatch') + witnesses = certificate['optimal_deletions'] + recorded = [tuple(w['deleted_indices']) for w in witnesses] + require(recorded == sorted(solutions) and len(solutions) == 4, 'minimum-support list mismatch') + for witness in witnesses: + validate_witness(family, target, witness) + triples = {frozenset(w['star_coordinates']) for w in witnesses} + require(triples == {frozenset(s) for s in combinations(sorted(family[target]), 3)}, + 'minimum supports are not exactly the four target triples') + + +def expect_rejection(function, label): + try: + function() + except (ValueError, KeyError, TypeError, IndexError): + return + raise ValueError('negative control accepted: ' + label) + + +def negative_controls(certificate, family, target, enumeration, solutions): + mutated = deepcopy(certificate) + mutated['code']['parity_checks_hex'][0] = format( + int(mutated['code']['parity_checks_hex'][0], 16) ^ (1 << target), '060x') + expect_rejection(lambda: read_model(mutated), 'changed parity bit') + mutated = deepcopy(certificate) + mutated['code']['parity_checks_hex'][0] = mutated['code']['parity_checks_hex'][1] + expect_rejection(lambda: read_model(mutated), 'dependent checks') + mutated = deepcopy(certificate) + mutated['code']['independent_star_indices'][0] = mutated['code']['independent_star_indices'][1] + expect_rejection(lambda: read_model(mutated), 'duplicate primal row') + mutated = deepcopy(certificate) + mutated['optimal_deletions'].pop() + expect_rejection(lambda: check_result(mutated, family, target, enumeration, solutions), 'omitted solution') + mutated = deepcopy(certificate) + mutated['enumeration']['triples'] -= 1 + expect_rejection(lambda: check_result(mutated, family, target, enumeration, solutions), 'short coverage receipt') + witness = deepcopy(certificate['optimal_deletions'][0]) + witness['deleted_indices'].append(target) + expect_rejection(lambda: validate_witness(family, target, witness), 'deleted target') + restored = 0 + for original in certificate['optimal_deletions']: + for index in original['deleted_indices']: + witness = deepcopy(original) + witness['deleted_indices'].remove(index) + expect_rejection(lambda: validate_witness(family, target, witness), 'restored puncture') + restored += 1 + witness = deepcopy(certificate['optimal_deletions'][0]) + witness['star_coordinates'][0] ^= 1 + expect_rejection(lambda: validate_witness(family, target, witness), 'wrong star sign') + require(restored == 20, 'restoration control count') + return 8 + + +def verify(path): + certificate = json.loads(path.read_text(encoding='utf-8')) + family, target, _, syndromes = read_model(certificate) + enumeration, solutions = enumerate_supports(syndromes, target) + check_result(certificate, family, target, enumeration, solutions) + controls = negative_controls(certificate, family, target, enumeration, solutions) + print('PASS_GLOBAL_STAR_PUNCTURES ports=240 rank=155 dual=85 minimum_deletions=5 ' + 'optimal_sets=4 all_target_deletions=85 triples=2246839 controls=%d ' + 'restored_ports=20 kappa=unchanged' % controls) + + +if __name__ == '__main__': + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--certificate', type=Path, default=HERE / 'CERTIFICATE.json') + args = parser.parse_args() + verify(args.certificate)