diff --git a/.github/workflows/global-star-puncture.yml b/.github/workflows/global-star-puncture.yml new file mode 100644 index 0000000000..a6226d300a --- /dev/null +++ b/.github/workflows/global-star-puncture.yml @@ -0,0 +1,39 @@ +name: Global proper-star puncture evidence + +on: + workflow_dispatch: + pull_request: + paths: + - 'research/global-star-puncture/**' + - '.github/workflows/global-star-puncture.yml' + push: + branches: [main, research/seed43-decoder] + paths: + - 'research/global-star-puncture/**' + - '.github/workflows/global-star-puncture.yml' + +permissions: + contents: read + +jobs: + replay: + runs-on: ubuntu-24.04 + timeout-minutes: 10 + strategy: + fail-fast: false + matrix: + python: ['3.11', '3.13'] + steps: + - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # repository baseline pin + with: + persist-credentials: false + - uses: actions/setup-python@5fda3b95a4ea91299a34e894583c3862153e4b97 # repository baseline pin + with: + python-version: ${{ matrix.python }} + - name: Exact receipt and failure detection + run: | + python -I -O -B research/global-star-puncture/verify.py + python -I -O -B research/global-star-puncture/test_verify.py + python -B scripts/verify_selected_result.py + - name: Require checkout unchanged + run: test -z "$(git status --porcelain)" diff --git a/research/global-star-puncture/CLAIM.json b/research/global-star-puncture/CLAIM.json new file mode 100644 index 0000000000..0ac8f14d16 --- /dev/null +++ b/research/global-star-puncture/CLAIM.json @@ -0,0 +1,54 @@ +{ + "assignment_seed": 43, + "randomness": "OS System.Security.Cryptography.RandomNumberGenerator; unbiased UInt32 rejection then modulo 100", + "track": "structural decoder research", + "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "started_utc": "2026-10-13T04:30:04Z", + "expected_finish_utc": "2026-10-13T05:10:04Z", + "verification_reserve_starts_utc": "2026-10-13T05:00:04Z", + "coordination": "Only open issue #650 asks for Discussions; no pinned sprint coordination issue exists. Claim recorded locally.", + "object": "Paired power-of-two k-port decoder, arbitrary off-target stars of degree below k, target-dependent overlap-class corrections, target-retaining punctures", + "method": "Exact F2 incidence-code dual labels and bounded meet-in-middle minimum-support search; attempt a combinatorial lower-bound proof", + "initial_domain": [ + [ + 5, + 4 + ], + [ + 6, + 4 + ] + ], + "seed_diversification": "Seed 43 selects k=4 and primary p=k+(seed mod 3)=5; target index 43 modulo family size", + "deliverable": "One scoped structural decoder note, exact portable verifier, receipt, negative controls and handoff; no kappa claim", + "candidates": [ + { + "task": "Extend PR669's target-local puncture result to arbitrary off-target stars", + "decision": "selected; explicitly left open by predecessor, new coefficient/support class" + }, + { + "task": "Price a non-B_K stage schedule with fewer idle bridge splits", + "decision": "deferred; physical and boundary recurrence would exceed this bounded session" + }, + { + "task": "Resolve PR620's unfinished extra-total E8 pairing-rank search", + "decision": "deferred; more solver time without a new mechanism does not justify reopening it" + } + ], + "predecessors": [ + { + "pr": 669, + "head": "308f1e6ec3bb0b6ec0584cf7bfe219addc219b1e" + }, + { + "pr": 231, + "head": "3c11e696a2fb2c454585d72710de27cd6bd3be68" + } + ], + "overlap": "Read selected review, PR ledger and PR620/631/669/703 plus structural PR search; no matching off-target puncture result found. PR669 comments refreshed immediately before local claim.", + "status": "completed", + "result": "Proved d(C_p,k)=2(p-k+1) for all k>=2; global proper-star one-target puncture threshold2(p-k)+1 at power-of-two k; exact nonlocal sharp witness", + "result_url": "https://github.com/lukemansoor/integer-mult-bounds/tree/research/seed43-decoder/research/global-star-puncture", + "finished_utc": "2026-10-13T04:50:00Z", + "overlap_refresh": "Refreshed through PR721 and read669/715/717 descriptions; no matching off-target paired-port puncture result" +} diff --git a/research/global-star-puncture/NOTICE.md b/research/global-star-puncture/NOTICE.md new file mode 100644 index 0000000000..204d4e5e50 --- /dev/null +++ b/research/global-star-puncture/NOTICE.md @@ -0,0 +1,11 @@ +# Attribution and license + +Copyright 2026 Luke Mansoor. New files are under the repository Apache-2.0 license. + +Prepared by Luke Mansoor (@lukemansoor), with substantial OpenAI Codex assistance in research, proof development, implementation, verification and writing. Separate Codex workers developed the restriction proof, built an independent list-valued verifier and audited the proof and implementation. This is independent AI review, not independent human peer review or proof-assistant verification. + +Joel Pulikkan / GamingPuzzled's PR231 supplies the symmetric paired-port decoder and binomial parity obstruction, following icekylinx's PR144 paired-cube work and eumemic's paired-cube bit identity. That source discloses Anthropic Claude assistance. Sam Sung / the-missionary-company's PR669 supplies the full-family obstruction for arbitrary global stars and the sharp target-local puncture theorem; it discloses substantial OpenAI Codex assistance. Its all-parameter local result and unpunctured global result are predecessor work, not claimed as new here. The new theorem closes its explicitly open off-target puncture class using a different restriction and generalized-cube argument. No predecessor code or text is copied into either implementation. + +The accepted construction is contextual only: Chafik Boukhalfa's PR626 allocation on Jeremy Kothe's PR622/623 K-triangle providers, with eumemic's PR543 bit supplier. GamingPuzzled's PR620, DreamingOfClouds' format/cold-helper work, Rohan Arun's recurrence correction and the cumulative OpenAI/community lineage remain credited through the maintainer review and original notices. The contribution does not rebuild or replace those constructions. + +PR631 studies E8 root-line punctures; PR703 studies asymmetric Hurwitz copy floors. They use different geometries and are neither prerequisites nor priority competitors for the theorem here. Original repository source attribution and license files are unchanged. Source commits, blob IDs and SHA-256 hashes are recorded in SOURCES.json. diff --git a/research/global-star-puncture/README.md b/research/global-star-puncture/README.md new file mode 100644 index 0000000000..356a8ea149 --- /dev/null +++ b/research/global-star-puncture/README.md @@ -0,0 +1,154 @@ +# Sharp puncture threshold for arbitrary off-target proper stars + +**Research note / scoped negative result; no new kappa.** + +For the paired-port model of PR231 and PR669, arbitrary off-target stars cannot lower the one-target puncture threshold below `2(p-k)+1` at a power-of-two k. This closes the punctured global-star class that PR669 explicitly leaves open. The local intersection-cell criterion does not extend: the concrete ten-star example below reaches the threshold while every intersection cell survives. + +## Algebraic class + +Let p >= k >= 2 and let P_{p,k} be the signed k-ports: choose k of p disjoint coordinate pairs and one coordinate from each chosen pair. Over F_2, let C_{p,k} be the evaluation space spanned by the functions + + m_L(S) = 1[L subset S], 0 <= |L| < k, + +where L itself is a partial signed port. This includes the empty star as a strengthening of the stipulated decoder class. A function in C_{p,k} is the evaluation of a multilinear polynomial of total degree less than k on P_{p,k}. + +**Theorem.** The smallest nonzero Hamming weight in C_{p,k} is exactly + + d(C_{p,k}) = 2(p-k+1). + +This statement holds for every k, not only powers of two. Consequently, for power-of-two k, a retained target T can be decoded by arbitrary global proper stars and permitted target overlap-class corrections only after deleting at least 2(p-k)+1 other ports. A single (k-1)-star containing T attains that threshold. + +The theorem concerns one retained target and scalar identities. It supplies no simultaneous decoder, paid recursive profile, circuit construction, restoration guarantee, or new kappa. + +## Lemma 1: parity on a generalized cube + +Take k slots. Slot i has two distinct coordinates a_i and b_i. Suppose the pair indices used by different slots are disjoint; a_i and b_i may belong to the same original pair or to two different original pairs. Every one of the 2^k selections of one coordinate per slot is then a valid signed k-port, and all these ports are distinct. Call the resulting family G a generalized cube. + +For every monomial m_L of degree |L|= 2^(r+1). + +If r >= m, no such nonempty W exists, because fixing all m coordinates isolates any chosen point. + +Proof by induction on m. For r=0 the entire cube is a face, so nonempty W has even cardinality, hence at least two. For r>=1, split W into its two first-coordinate slices. If both are nonempty, each slice inherits the even-face property up to r-1 additional fixed coordinates; the induction hypothesis gives at least 2^r points in each slice. If only one slice is nonempty, that slice inherits the property up to r fixed coordinates, because a face fixing other coordinates has the same intersection with W as its corresponding face in the surviving slice. If r>=m-1 this would isolate a point and is impossible; otherwise induction gives at least 2^(r+1) points in the surviving slice. This proves the lemma. + +## Proof of the minimum distance theorem + +Put q=p-k and induct on q while keeping k fixed. + +For q=0 the whole family is one ordinary sign cube. Lemma 1 makes every nonzero weight even, hence at least two. A monomial m_J for any (k-1)-port J has exactly two extensions, so the distance is two. + +Now take q>=1 and assume the claimed lower bound for p-1 pairs, namely 2q. Suppose for contradiction that a nonzero f in C_{p,k} has weight w<2(q+1). Its total weight is even by Lemma 1, so w<=2q. Choose a support port T, and let Q be its k pair indices. + +For each of the q pairs r outside Q, restrict f to ports avoiding pair r. All monomials containing a coordinate of r become zero; all other monomials still have degree less than k. Thus the restriction belongs to C_{p-1,k}. It remains nonzero because it contains T. By induction its weight is at least 2q. This restriction has weight at most w<=2q, so equality holds and no support port of f contains pair r. Repeating for every outside pair shows that all of f's support lies in the ordinary sign cube on Q, and w=2q. + +Fix any face of that ordinary cube obtained by fixing a set A of s<=min(q,k) signs. For each fixed slot i in A, choose a distinct outside pair r_i, and use in slot i the fixed coordinate of Q together with either coordinate of r_i. For each remaining slot use both coordinates of its original Q pair. These slot pair indices are disjoint, so this is a generalized cube. Its intersection with the original ordinary cube is exactly the chosen face: selecting an outside alternative leaves Q, whereas selecting all fixed coordinates leaves the other signs free. + +Because f vanishes outside the ordinary cube, its sum on this generalized cube equals the support cardinality in that face. Lemma 1 makes this cardinality even. Therefore every face fixing at most q signs is even. If q>=k this contradicts the presence of T directly. If q= 2^(q+1) > 2q, + +again a contradiction. The strict inequality holds for every q>=1 (base 4>2, and induction or elementary doubling). + +This proves the lower bound. For sharpness, choose any (k-1)-port J. Its extensions consist of choosing one of the p-(k-1)=q+1 remaining pairs and one of its two coordinates. Thus m_J has exactly 2(q+1) nonzero evaluations. The distance theorem follows. + +## Absorbing overlap corrections when k is a power of two + +Fix T and write j=|S intersect T|. For 1<=l= wt(f) >= 2(p-k+1). + +Thus |D|>=2(p-k)+1, even after granting the empty star. Conversely, choose J subset T of size k-1 and delete every other extension of J. This deletes exactly 2(p-k)+1 ports and leaves star_J(F)=x_T. The lower and upper bounds agree. + +## A sharp off-target witness that defeats the local cell criterion + +Take p=5, k=4, and T={1,2,7,9}, using coordinate pairs {0,1}, {2,3}, ..., {8,9}. Delete exactly + + {0,2,4,6}, {0,2,5,6}, {1,2,7,8}. + +The following ten nonempty proper stars sum to x_T on the surviving family: + + {2}; {0,2}, {2,4}, {2,5}, {2,6}; + {0,2,4}, {0,2,5}, {0,2,6}, {2,4,6}, {2,5,6}. + +One compact description of their coefficient function is + + 1[2 in S] * (1+a+b+c+ab+ac+bc), + a=1[0 in S], b=1[4 in S]+1[5 in S], c=1[6 in S]. + +All arithmetic is in F2. The two summands in b are disjoint because a port cannot contain both coordinates of one pair. The parenthesized expression is one exactly at (a,b,c)=(0,0,0) or (1,1,1). Its complete support is the three deleted ports together with T. This is a degree-three expression with no empty-star term. + +No intersection cell S intersect T is emptied: the first two deleted ports occupy a seven-port cell {2}, and the third occupies a three-port cell {1,2,7}. Therefore PR669's target-local cell criterion excludes a local decoder for this deletion set. The exact full coefficient calculation in verify.py also checks local infeasibility directly. The example shows why extending the minimum threshold must not be confused with extending that criterion. + +## Provenance and distinction + +The symmetric binomial obstruction is the retained PR231 result (Joel Pulikkan / GamingPuzzled). PR669 (Sam Sung / the-missionary-company; source head 308f1e6ec3bb0b6ec0584cf7bfe219addc219b1e) already proves the full-family obstruction for arbitrary global stars and proves the sharp threshold only for target-local stars. This proof addresses PR669's explicitly unclosed arbitrary off-target puncture class. Its restriction induction and generalized-cube face bound apply to arbitrary global coefficients; they do not use the local intersection-cell argument. + +The stronger space including the empty star is deliberate: its exact minimum-distance result implies the required no-empty-star lower bound, while sharpness uses a nonempty (k-1)-star. No implementation of a supplier or accepted-frontier change is inferred. + + +## Reproduce and inspect the evidence + +From the repository root, with Python 3.10 or newer and no third-party dependencies: + +```sh +python3 -B research/global-star-puncture/verify.py +``` + +Expected: + +```text +PASS_GLOBAL_STAR_PUNCTURE: sharp deletion thresholds 3/5; 2 independent F2 engines; 960 correction rows; 12 negative controls +``` + +The default command recomputes and compares the entire committed RESULTS.json, without writing files. `--write PATH` additionally exports the same receipt after all checks. The checks remain active under `python3 -I -O -B`. The standalone independent implementation is `independent.py` (use `--json` for its full receipt). + +The two implementations generate actual ports separately. verify.py computes the star row space and its quotient map with packed integer elimination. independent.py uses list-valued RREF and a full nullspace parity-check matrix, checking its rank and every orthogonality equation. Neither imports predecessor or supplier code. + +| Domain | Ports | Star rank / dual rank | Exact minimum weight | Pair sums checked | +|---|---:|---:|---:|---:| +| p=5, k=4 | 80 | 65 / 15 | 4 | 3,160; 1,345 distinct | +| p=6, k=4 | 240 | 155 / 85 | 6 | all 28,680 distinct | + +Even codeword weights and distinct nonzero dual columns exclude weights one through three. In the second domain, distinct unordered-pair sums also exclude weight four; parity excludes weight five. Single three-stars attain four and six. Full syndrome columns, selected targets, sharp deletions, independent nullspace data and the off-target witness are in RESULTS.json. All 960 target-specific overlap corrections are checked in both implementations, including overlaps zero and k. + +Additional complete coverage comprises all codewords for (p,k)=(2,2),(3,2),(4,2),(5,2),(6,2),(3,3),(4,4), and all binary support sets in dimensions one through four for every face-codimension budget. This includes q>=k cases of the induction. For the two principal domains, all faces fixing at most p-k coordinates at the seed-selected target are realized by valid generalized cubes and checked against every star, by both packed and direct incidence counts. These finite checks support the written general proof; they are not its logical replacement or a proof-assistant formalization. + +The twelve named controls reject single-entry incidence corruption, parity-preserving two-entry corruption, forbidden degree-k singleton stars, forbidden overlap-zero corrections, damaged dual columns, and invalid generalized cubes, in each principal domain. The independent engine repeats both incidence controls. A positive k=3 control uses a permitted overlap correction to isolate a target on the unpunctured family, demonstrating why the power-of-two condition is necessary for the decoder corollary. + +## Scope, cost and stopping rule + +This is an exact scalar decoder obstruction and an attaining scalar identity for **one specified retained target**. It permits target-dependent coefficients, arbitrary off-target support, arbitrarily many stars, and even the empty star for the lower bound. The upper witnesses use nonempty stars. Stars and corrections are recomputed on the surviving family. + +A proposal to isolate a target with fewer than 2(p-k)+1 deleted ports fails the identity even if all helpers, source reads, copies, frame changes, restoration and recursive children are free. It therefore cannot become a paid supplier in this decoder class. At or above the threshold, no complete cost is asserted. Simultaneous all-target decoding, cost of preparing the totals, arbitrary dirty restoration, reader frames, hosting, outer assembly and other decoder geometries remain separate questions. Source-dependent coefficients inside an overlap class, degree-k stars and nonlinear mechanisms are outside the corollary. + +This was a bounded structural experiment, with OS-random assignment seed 43. The seed selected k=4, primary p=k+(43 mod 3)=5, and target index 43 in the deterministic port order; p=6 supplied an adjacent region. The initial finite quotient experiment led to a restriction/face-parity proof, not a larger solver search. The finite domain, complete enumerations and all stopping conditions are fixed in verify.py; no uncompleted heuristic search is reported as an impossibility theorem. CLAIM.json records the three candidate tasks and narrow local claim. No pinned coordination issue existed; no separate reservation issue was opened. + +Exact base: `66849e1475c930fd7732b1a0067ffee7e1e95f60`. SOURCES.json records context and predecessor source pins. At that base, the accepted conditional result is `51110230636731/31250000000000000`, from #626/#622/#623 with #543. The selected pointer, accepted construction and upstream/ are unchanged. Its all-size compiler, mutable-source/common-label realization, whole-call hosting, precision/tape/exact recovery and analytic-transfer obligations remain inherited; this result discharges none of them. + +## Attribution and validation + +Prepared by Luke Mansoor (@lukemansoor) with substantial OpenAI Codex assistance in proof development, implementation, independent AI implementation/review and writing. No independent human review is claimed. New work is Apache-2.0 under the repository license. NOTICE.md preserves predecessor and selected-context credit. VALIDATION.md records completed local checks separately from GitHub CI. diff --git a/research/global-star-puncture/RESULTS.json b/research/global-star-puncture/RESULTS.json new file mode 100644 index 0000000000..de6aa10f76 --- /dev/null +++ b/research/global-star-puncture/RESULTS.json @@ -0,0 +1,941 @@ +{ + "assignment_seed": 43, + "bitset_quotient": [ + { + "correction_rows": 240, + "deleted_ports": [ + [ + 1, + 2, + 4, + 7 + ], + [ + 1, + 2, + 5, + 7 + ], + [ + 1, + 2, + 7, + 8 + ] + ], + "distinct_pair_syndromes": 1345, + "distinct_syndrome_columns": 80, + "dual_rank": 15, + "generalized_face_cubes": 9, + "generator_rank": 65, + "k": 4, + "minimum_one_target_deletions": 3, + "minimum_weight": 4, + "negative_controls": [ + "single incidence flip", + "even-parity two-entry flip", + "forbidden degree-k singleton star", + "forbidden overlap-zero correction", + "zeroed dual column", + "generalized cube reusing a physical pair" + ], + "p": 5, + "pair_count": 3160, + "ports": 80, + "quotient_columns_hex": [ + "0x1", + "0x2", + "0x4", + "0x7", + "0x10", + "0x13", + "0x15", + "0x16", + "0x100", + "0x103", + "0x105", + "0x106", + "0x111", + "0x112", + "0x114", + "0x117", + "0x10000", + "0x10003", + "0x40000", + "0x40003", + "0x100000", + "0x100003", + "0x150000", + "0x150003", + "0x1000000", + "0x1000003", + "0x1050000", + "0x1050003", + "0x1110000", + "0x1110003", + "0x1140000", + "0x1140003", + "0x100000000", + "0x100000005", + "0x100050000", + "0x100050005", + "0x1000000000", + "0x1000000005", + "0x1000050000", + "0x1000050005", + "0x10000000000", + "0x10000000005", + "0x10000050000", + "0x10000050005", + "0x11100000000", + "0x11100000005", + "0x11100050000", + "0x11100050005", + "0x1000000000000", + "0x1000000000011", + "0x1000000110000", + "0x1000000110011", + "0x1001100000000", + "0x1001100000011", + "0x1001100110000", + "0x1001100110011", + "0x100000000000000", + "0x100000000000011", + "0x100000000110000", + "0x100000000110011", + "0x100001100000000", + "0x100001100000011", + "0x100001100110000", + "0x100001100110011", + "0x10000000000000000", + "0x10000000000000101", + "0x10000000001010000", + "0x10000000001010101", + "0x10000010100000000", + "0x10000010100000101", + "0x10000010101010000", + "0x10000010101010101", + "0x10101000000000000", + "0x10101000000000101", + "0x10101000001010000", + "0x10101000001010101", + "0x10101010100000000", + "0x10101010100000101", + "0x10101010101010000", + "0x10101010101010101" + ], + "star": [ + 1, + 2, + 7 + ], + "stars_including_empty": 131, + "target": [ + 1, + 2, + 7, + 9 + ], + "target_index": 43 + }, + { + "correction_rows": 720, + "deleted_ports": [ + [ + 1, + 2, + 5, + 6 + ], + [ + 1, + 2, + 5, + 7 + ], + [ + 1, + 2, + 5, + 8 + ], + [ + 1, + 2, + 5, + 9 + ], + [ + 1, + 2, + 5, + 10 + ] + ], + "distinct_pair_syndromes": 28680, + "distinct_syndrome_columns": 240, + "dual_rank": 85, + "generalized_face_cubes": 33, + "generator_rank": 155, + "k": 4, + "minimum_one_target_deletions": 5, + "minimum_weight": 6, + "negative_controls": [ + "single incidence flip", + "even-parity two-entry flip", + "forbidden degree-k singleton star", + "forbidden overlap-zero correction", + "zeroed dual column", + "generalized cube reusing a physical pair" + ], + "p": 6, + "pair_count": 28680, + "ports": 240, + "quotient_columns_hex": [ + "0x1", + "0x2", + "0x4", + "0x8", + "0x10", + "0x20", + "0x40", + "0x7f", + "0x100", + "0x200", + "0x400", + "0x70f", + "0x1000", + "0x1333", + "0x1555", + "0x1669", + "0x10000", + "0x20000", + "0x40000", + "0x80000", + "0x100000", + "0x200000", + "0x400000", + "0x7f0000", + "0x1000000", + "0x2000000", + "0x4000000", + "0x70f0000", + "0x10000000", + "0x13330000", + "0x15550000", + "0x16690000", + "0x100000000", + "0x100030003", + "0x400000000", + "0x4000c000c", + "0x1000000000", + "0x1000300030", + "0x4000000000", + "0x40003f003f", + "0x10000000000", + "0x10003000300", + "0x40000000000", + "0x400030f030f", + "0x100000000000", + "0x100003330333", + "0x155500000000", + "0x1555033c033c", + "0x1000000000000", + "0x2000000000000", + "0x4000000000000", + "0x70000000f000f", + "0x10000000000000", + "0x20000000000000", + "0x40000000000000", + "0x700000000f000f", + "0x100000000000000", + "0x200000000000000", + "0x400000000000000", + "0x7000000000f000f", + "0x1000000000000000", + "0x1333000000000000", + "0x1555000000000000", + "0x16660000000f000f", + "0x10000000000000000", + "0x10003000000000005", + "0x40000000000000000", + "0x400030000000f0005", + "0x100000000000000000", + "0x100030000000000050", + "0x400000000000000000", + "0x4000300000000f0050", + "0x1000000000000000000", + "0x1000300000000000500", + "0x4000000000000000000", + "0x40003000000000f0500", + "0x10000000000000000000", + "0x10000333000000000555", + "0x15550000000000000000", + "0x155503330000000f0555", + "0x100000000000000000000", + "0x100000005000000050000", + "0x100050000000500000000", + "0x10005000500050005000f", + "0x1000000000000000000000", + "0x1000000050000000500000", + "0x1000500000005000000000", + "0x100050005000500050000f", + "0x10000000000000000000000", + "0x10000000500000005000000", + "0x10005000000050000000000", + "0x1000500050005000500000f", + "0x100000000000000000000000", + "0x100000000555000005550000", + "0x100005550000055500000000", + "0x10000555055505550555000f", + "0x1000000000000000000000000", + "0x2000000000000000000000000", + "0x4000000000000000000000000", + "0x7000000000000000000330033", + "0x10000000000000000000000000", + "0x13000000000033000000000055", + "0x15000000000055000000550000", + "0x16000000000066000000660066", + "0x100000000000000000000000000", + "0x200000000000000000000000000", + "0x400000000000000000000000000", + "0x700000000000000000000330033", + "0x1000000000000000000000000000", + "0x1300000000000033000000000055", + "0x1500000000000055000000550000", + "0x1600000000000066000000660066", + "0x10000000000000000000000000000", + "0x10003000000000000000000000011", + "0x40000000000000000000000000000", + "0x40003000000000000000000330011", + "0x100000000000000000000000000000", + "0x100003000000000033000000000011", + "0x150000000000550000005500000000", + "0x150003000000550033005500330011", + "0x1000000000000000000000000000000", + "0x1000300000000000000000000001100", + "0x4000000000000000000000000000000", + "0x4000300000000000000000000331100", + "0x10000000000000000000000000000000", + "0x10000300000000000033000000001100", + "0x15000000000000550000005500000000", + "0x15000300000000550033005500331100", + "0x100000000000000000000000000000000", + "0x100000005000000000000000000110000", + "0x100050000000000000000001100000000", + "0x100050005000000000000001100110033", + "0x1000000000000000000000000000000000", + "0x1000000005000000000055000000110000", + "0x1000050000000000550000001100000000", + "0x1000050005000000550055001100110033", + "0x10000000000000000000000000000000000", + "0x10000000500000000000000000011000000", + "0x10005000000000000000000110000000000", + "0x10005000500000000000000110011000033", + "0x100000000000000000000000000000000000", + "0x100000000500000000000055000011000000", + "0x100005000000000000550000110000000000", + "0x100005000500000000550055110011000033", + "0x1000000000000000000000000000000000000", + "0x1000000000011000000000011000000000000", + "0x1000000110000000000110000000000000000", + "0x1000000110011000000110011000000000055", + "0x1001100000000001100000000000000000000", + "0x1001100000011001100000011000000550000", + "0x1001100110000001100110000005500000000", + "0x1001100110011001100110011005500550055", + "0x100000000000000000000000000000000000000", + "0x100000000001100000000001100000000000000", + "0x100000011000000000011000000000000000000", + "0x100000011001100000011001100000000000055", + "0x100110000000000110000000000000000000000", + "0x100110000001100110000001100000000550000", + "0x100110011000000110011000000005500000000", + "0x100110011001100110011001100005500550055", + "0x10000000000000000000000000000000000000000", + "0x20000000000000000000000000000000000000000", + "0x40000000000000000000000000000000000000000", + "0x70000000000000000000000000000000003030303", + "0x100000000000000000000000000000000000000000", + "0x130000000000000000000000000303000000000505", + "0x150000000000000000000000000505000005050000", + "0x160000000000000000000000000606000006060606", + "0x1000000000000000000000000000000000000000000", + "0x1030000000000000303000000000000000000001111", + "0x1050000000000000505000000000000000011110000", + "0x1060000000000000606000000000000000012121212", + "0x1110000000000001111000000001111000000000000", + "0x1120000000000001212000000001212000000001414", + "0x1140000000000001414000000001414000014140000", + "0x1170000000000001717000000001717000017171717", + "0x100000000000000000000000000000000000000000000", + "0x100030000000000000000000000000000000000000101", + "0x400000000000000000000000000000000000000000000", + "0x400030000000000000000000000000000000003030101", + "0x1000000000000000000000000000000000000000000000", + "0x1000030000000000000000000000000303000000000101", + "0x1500000000000000000000000005050000050500000000", + "0x1500030000000000000000000005050303050503030101", + "0x10000000000000000000000000000000000000000000000", + "0x10000030000000000000303000000000000000000000101", + "0x10500000000000005050000000000000000111100000000", + "0x10500030000000005050303000000000000111103030101", + "0x11100000000000011110000000011110000000000000000", + "0x11100030000000011110303000011110303000000000101", + "0x11400000000000014140000000014140000141400000000", + "0x11400030000000014140303000014140303141403030101", + "0x1000000000000000000000000000000000000000000000000", + "0x1000000050000000000000000000000000000000001010000", + "0x1000500000000000000000000000000000000010100000000", + "0x1000500050000000000000000000000000000010101010303", + "0x10000000000000000000000000000000000000000000000000", + "0x10000000050000000000000000000000000505000001010000", + "0x10000500000000000000000000000005050000010100000000", + "0x10000500050000000000000000000005050505010101010303", + "0x100000000000000000000000000000000000000000000000000", + "0x100000000050000000000000505000000000000000001010000", + "0x100000500000000000005050000000000000000010100000000", + "0x100000500050000000005050505000000000000010101010303", + "0x111000000000000111100000000111100000000000000000000", + "0x111000000050000111100000505111100000505000001010000", + "0x111000500000000111105050000111105050000010100000000", + "0x111000500050000111105050505111105050505010101010303", + "0x10000000000000000000000000000000000000000000000000000", + "0x10000000000110000000000000000000000000101000000000000", + "0x10000001100000000000000000000000001010000000000000000", + "0x10000001100110000000000000000000001010101000000000505", + "0x10011000000000000000000000000010100000000000000000000", + "0x10011000000110000000000000000010100000101000005050000", + "0x10011001100000000000000000000010101010000050500000000", + "0x10011001100110000000000000000010101010101050505050505", + "0x1000000000000000000000000000000000000000000000000000000", + "0x1000000000000110000000000001111000000000101000000000000", + "0x1000000001100000000000011110000000001010000000000000000", + "0x1000000001100110000000011111111000001010101000000000505", + "0x1000011000000000000111100000000010100000000000000000000", + "0x1000011000000110000111100001111010100000101000005050000", + "0x1000011001100000000111111110000010101010000050500000000", + "0x1000011001100110000111111111111010101010101050505050505", + "0x100000000000000000000000000000000000000000000000000000000", + "0x100000000000001010000000000000101000000000000000000000000", + "0x100000000010100000000000001010000000000000000000000000000", + "0x100000000010101010000000001010101000000000000000000001111", + "0x100000101000000000000010100000000000000000000000000000000", + "0x100000101000001010000010100000101000000000000000011110000", + "0x100000101010100000000010101010000000000000000111100000000", + "0x100000101010101010000010101010101000000000000111111111111", + "0x101010000000000000101000000000000000000000000000000000000", + "0x101010000000001010101000000000101000000001111000000000000", + "0x101010000010100000101000001010000000011110000000000000000", + "0x101010000010101010101000001010101000011111111000000001111", + "0x101010101000000000101010100000000111100000000000000000000", + "0x101010101000001010101010100000101111100001111000011110000", + "0x101010101010100000101010101010000111111110000111100000000", + "0x101010101010101010101010101010101111111111111111111111111" + ], + "star": [ + 1, + 2, + 5 + ], + "stars_including_empty": 233, + "target": [ + 1, + 2, + 5, + 11 + ], + "target_index": 43 + } + ], + "complete_small_spans": [ + { + "codewords": 8, + "k": 2, + "minimum_weight": 2, + "p": 2, + "ports": 4, + "rank": 3 + }, + { + "codewords": 64, + "k": 2, + "minimum_weight": 4, + "p": 3, + "ports": 12, + "rank": 6 + }, + { + "codewords": 256, + "k": 2, + "minimum_weight": 6, + "p": 4, + "ports": 24, + "rank": 8 + }, + { + "codewords": 1024, + "k": 2, + "minimum_weight": 8, + "p": 5, + "ports": 40, + "rank": 10 + }, + { + "codewords": 4096, + "k": 2, + "minimum_weight": 10, + "p": 6, + "ports": 60, + "rank": 12 + }, + { + "codewords": 128, + "k": 3, + "minimum_weight": 2, + "p": 3, + "ports": 8, + "rank": 7 + }, + { + "codewords": 32768, + "k": 4, + "minimum_weight": 2, + "p": 4, + "ports": 16, + "rank": 15 + } + ], + "even_face_exhaustion": [ + { + "admitted_nonempty": 1, + "codimension_budget": 0, + "dimension": 1, + "minimum_weight": 2, + "support_sets": 3 + }, + { + "admitted_nonempty": 0, + "codimension_budget": 1, + "dimension": 1, + "minimum_weight": null, + "support_sets": 3 + }, + { + "admitted_nonempty": 7, + "codimension_budget": 0, + "dimension": 2, + "minimum_weight": 2, + "support_sets": 15 + }, + { + "admitted_nonempty": 1, + "codimension_budget": 1, + "dimension": 2, + "minimum_weight": 4, + "support_sets": 15 + }, + { + "admitted_nonempty": 0, + "codimension_budget": 2, + "dimension": 2, + "minimum_weight": null, + "support_sets": 15 + }, + { + "admitted_nonempty": 127, + "codimension_budget": 0, + "dimension": 3, + "minimum_weight": 2, + "support_sets": 255 + }, + { + "admitted_nonempty": 15, + "codimension_budget": 1, + "dimension": 3, + "minimum_weight": 4, + "support_sets": 255 + }, + { + "admitted_nonempty": 1, + "codimension_budget": 2, + "dimension": 3, + "minimum_weight": 8, + "support_sets": 255 + }, + { + "admitted_nonempty": 0, + "codimension_budget": 3, + "dimension": 3, + "minimum_weight": null, + "support_sets": 255 + }, + { + "admitted_nonempty": 32767, + "codimension_budget": 0, + "dimension": 4, + "minimum_weight": 2, + "support_sets": 65535 + }, + { + "admitted_nonempty": 2047, + "codimension_budget": 1, + "dimension": 4, + "minimum_weight": 4, + "support_sets": 65535 + }, + { + "admitted_nonempty": 31, + "codimension_budget": 2, + "dimension": 4, + "minimum_weight": 8, + "support_sets": 65535 + }, + { + "admitted_nonempty": 1, + "codimension_budget": 3, + "dimension": 4, + "minimum_weight": 16, + "support_sets": 65535 + }, + { + "admitted_nonempty": 0, + "codimension_budget": 4, + "dimension": 4, + "minimum_weight": null, + "support_sets": 65535 + } + ], + "list_rref_nullspace": [ + { + "all_generator_rows_even": true, + "check_rank": 15, + "distinct_pair_syndromes": 1345, + "first_pair_collision": [ + [ + 0, + 3 + ], + [ + 1, + 2 + ] + ], + "generator_rank": 65, + "incidence_parity_preserving_pair_flip_rejected": true, + "incidence_single_flip_rejected": true, + "k": 4, + "minimum_nonzero_weight": 4, + "nonzero_distinct_syndrome_columns": 80, + "nullspace_free_columns": [ + 15, + 30, + 31, + 45, + 46, + 47, + 59, + 61, + 62, + 63, + 71, + 75, + 77, + 78, + 79 + ], + "overlap_rows_checked": 240, + "p": 5, + "pair_count": 3160, + "ports": 80, + "proper_stars_including_empty": 131, + "three_star_witness": [ + 0, + 2, + 4 + ], + "witness_port_indices": [ + 0, + 1, + 16, + 17 + ], + "witness_ports": [ + [ + 0, + 2, + 4, + 6 + ], + [ + 0, + 2, + 4, + 7 + ], + [ + 0, + 2, + 4, + 8 + ], + [ + 0, + 2, + 4, + 9 + ] + ] + }, + { + "all_generator_rows_even": true, + "check_rank": 85, + "distinct_pair_syndromes": 28680, + "first_pair_collision": null, + "generator_rank": 155, + "incidence_parity_preserving_pair_flip_rejected": true, + "incidence_single_flip_rejected": true, + "k": 4, + "minimum_nonzero_weight": 6, + "nonzero_distinct_syndrome_columns": 240, + "nullspace_free_columns": [ + 15, + 30, + 31, + 46, + 47, + 61, + 62, + 63, + 76, + 77, + 78, + 79, + 92, + 93, + 94, + 95, + 107, + 109, + 110, + 111, + 122, + 123, + 124, + 125, + 126, + 127, + 137, + 138, + 139, + 140, + 141, + 142, + 143, + 153, + 154, + 155, + 156, + 157, + 158, + 159, + 167, + 171, + 173, + 174, + 175, + 182, + 183, + 186, + 187, + 188, + 189, + 190, + 191, + 197, + 198, + 199, + 201, + 202, + 203, + 204, + 205, + 206, + 207, + 211, + 213, + 214, + 215, + 217, + 218, + 219, + 220, + 221, + 222, + 223, + 227, + 229, + 230, + 231, + 233, + 234, + 235, + 236, + 237, + 238, + 239 + ], + "overlap_rows_checked": 720, + "p": 6, + "pair_count": 28680, + "ports": 240, + "proper_stars_including_empty": 233, + "three_star_witness": [ + 0, + 2, + 4 + ], + "witness_port_indices": [ + 0, + 1, + 16, + 17, + 32, + 33 + ], + "witness_ports": [ + [ + 0, + 2, + 4, + 6 + ], + [ + 0, + 2, + 4, + 7 + ], + [ + 0, + 2, + 4, + 8 + ], + [ + 0, + 2, + 4, + 9 + ], + [ + 0, + 2, + 4, + 10 + ], + [ + 0, + 2, + 4, + 11 + ] + ] + } + ], + "non_power_of_two_escape_control": "PASS", + "nonlocal_sharp_witness": { + "all_intersection_cells_survive": true, + "control": "The minimum threshold extends globally; the local cell criterion does not", + "deleted_indices": [ + 0, + 2, + 42 + ], + "deleted_ports": [ + [ + 0, + 2, + 4, + 6 + ], + [ + 0, + 2, + 5, + 6 + ], + [ + 1, + 2, + 7, + 8 + ] + ], + "global_decoder_passes": true, + "k": 4, + "p": 5, + "stars": [ + [ + 2 + ], + [ + 0, + 2 + ], + [ + 2, + 4 + ], + [ + 2, + 5 + ], + [ + 2, + 6 + ], + [ + 0, + 2, + 4 + ], + [ + 0, + 2, + 5 + ], + [ + 0, + 2, + 6 + ], + [ + 2, + 4, + 6 + ], + [ + 2, + 5, + 6 + ] + ], + "support_indices": [ + 0, + 2, + 42, + 43 + ], + "target": [ + 1, + 2, + 7, + 9 + ], + "target_index": 43, + "target_local_decoder_infeasible": true + }, + "scope": "Exact finite evidence for README's written general proof; no new kappa", + "status": "PASS" +} diff --git a/research/global-star-puncture/SOURCES.json b/research/global-star-puncture/SOURCES.json new file mode 100644 index 0000000000..48d75de8a3 --- /dev/null +++ b/research/global-star-puncture/SOURCES.json @@ -0,0 +1,70 @@ +{ + "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "context": [ + { + "git_blob": "bce5be99d7094777b6ba5661ee2cfebce3879ec5", + "path": "CONTRIBUTING.md", + "sha256": "a10dd640ec6f4b1d8b6acc31220af512335dc093f634cd25f601acb07ac53d53" + }, + { + "git_blob": "92a10096dee76479af88a897714b3818d8263141", + "path": "certificates/selected-result.json", + "sha256": "b3bf402f31a69bde0629936a9b569bed48281568d7b16d5fba120b5311ea1f53" + }, + { + "git_blob": "630009d642d4656c9cb27ce1fb83aace895eaf71", + "path": "docs/research/current-status.md", + "sha256": "197319a6edf04340ec3623d09d03714fcd6a981359f22bdcefdd06e7e2f4174d" + }, + { + "git_blob": "18af0567fca0ab08fcba5df89cbaa5dbf2fc5990", + "path": "docs/research/pr-ledger.md", + "sha256": "2e811684201e08007377ee97b1c35c0f0b3c026dd8207e7b0de3ff7cd1e13a91" + }, + { + "git_blob": "11efcd07ae2b9d93d355c6adaf773dca70dbce91", + "path": "docs/research/community-k492-review.md", + "sha256": "3b731d30e80010b15408a289b0b32192700885474c8b36d48ee3320a7a8c5c47" + }, + { + "git_blob": "6751eba6f617292fc919e58d5a9f9f06ab037391", + "path": "research/e8-bit-r420/README.md", + "sha256": "9807be57c6adf26b30e4f54e2f8160075bbc05091f1a6d157e43d2a4620c1c9f" + }, + { + "git_blob": "58722c1a496f0c806e77c9d762eb00b0c53254f0", + "path": "research/complex-k492-owner-repair/README.md", + "sha256": "ee5a1ace4828f7a073be97e95c2d931988774dd3a29a877e65abdf429aeec902" + }, + { + "git_blob": "3a13dfd89b801a0a72db7ef50be7d324addc7949", + "path": "research/hypercube-decoder-parity/README.md", + "sha256": "2dc89289d1d979aec6709b8c55a2af7cd39d97297bc20fb94adc7d4cdf867cd1" + } + ], + "dependency_scope": "Sources are context/provenance pins; the new proof is elementary and both implementations are independent.", + "predecessors": [ + { + "contributor": "Joel Pulikkan / GamingPuzzled", + "pr": 231, + "retained_note": { + "git_blob": "3a13dfd89b801a0a72db7ef50be7d324addc7949", + "path": "research/hypercube-decoder-parity/README.md", + "sha256": "2dc89289d1d979aec6709b8c55a2af7cd39d97297bc20fb94adc7d4cdf867cd1" + }, + "source_commit": "3c11e696a2fb2c454585d72710de27cd6bd3be68" + }, + { + "contributor": "Sam Sung / the-missionary-company", + "pr": 669, + "source": { + "git_blob": "4dad05a71c61444253add9c03cb78531b157e7f0", + "path": "research/asymmetric-hypercube-decoder/README.md", + "sha256": "69b624112d6294f519682fdf762d7f670063ea3f2b05ec0f25ce26e93c481c17" + }, + "source_commit": "308f1e6ec3bb0b6ec0584cf7bfe219addc219b1e" + } + ], + "runtime_dependencies": "Python >=3.10 standard library only; no predecessor code imports", + "selected_kappa": "51110230636731/31250000000000000" +} diff --git a/research/global-star-puncture/VALIDATION.md b/research/global-star-puncture/VALIDATION.md new file mode 100644 index 0000000000..a693be52bd --- /dev/null +++ b/research/global-star-puncture/VALIDATION.md @@ -0,0 +1,24 @@ +# Validation and handoff scope + +Local verification on Windows 11, Python 3.13.5, October 12, 2026 PDT: + +```sh +python3 -B research/global-star-puncture/verify.py +python3 -I -O -B research/global-star-puncture/verify.py +python3 -I -O -B research/global-star-puncture/independent.py +python3 -I -O -B research/global-star-puncture/test_verify.py +python3 -B scripts/verify_selected_result.py +git diff --cached --check +``` + +The exact receipt passes in normal and isolated optimized execution. Both F2 implementations agree on ranks, minimum weights, pair-syndrome counts and all 960 correction rows. Twelve primary mathematical controls and the independent engine's repeated incidence controls pass. Four harness tests pass: relocation/export from a minimal copy launched outside the copied root, corrupted receipt rejection with existing output preserved, changed contextual source bytes rejected, and changed source-pin digest rejected. The first harness attempt used this sandbox's inaccessible default temporary directory; placing its freshly created temporary tree inside the checkout fixed the environment problem. Each test verifies its cleanup target before removal. No failed run is counted as a pass. + +A separate Codex worker reviewed the written induction, binary-face lemma and generalized-cube construction, then reviewed both implementation methods and replayed the exact receipt. It independently enumerated the nonlocal example using coordinate combinations and all 131,072 local coefficient assignments: the ten-star identity holds, all 16 intersection cells survive, and no target-local decoder exists. This extra finite check is supporting local review evidence; the production verifier independently checks local infeasibility by exact elimination. No independent human peer review or proof-assistant theorem build is claimed. + +The selected-record check passes with exact kappa `51110230636731/31250000000000000`; all pinned contextual source bytes match. Neither `make verify` nor the expensive `frontier626-verify` cold supplier replay was repeated for this additive decoder research package. No supplier, assembly, generator, selected record, or `upstream/` file changes. Scoped replay covers the new mathematical work; no full repository-suite success is claimed. + +The new scoped workflow copies the existing repository's checkout and setup-python action pins, runs this package and selected-record integrity on Linux/Python 3.11 and 3.13, and requires a clean checkout. Hosted CI status is separate from local execution and is not asserted here before execution. + +Exact base: `66849e1475c930fd7732b1a0067ffee7e1e95f60`. A final main fetch retains that base. PR metadata was refreshed through #721, including the actual descriptions of #669, #715 and #717. #669 leaves the arbitrary off-target puncture problem open; #715 is an E8 mixed-port equality case and #717 studies E8 complex decoder floors. None duplicates the paired-port minimum-distance argument or its global/local distinction. PR669's source remains pinned at `308f1e6ec3bb0b6ec0584cf7bfe219addc219b1e`. + +The proof establishes a scalar statement for one retained target. It neither certifies simultaneous all-target delivery nor supplies a complete paid word, dirty restoration, frame schedule, recursive profile, physical host or new multiplication exponent. The review target is the general proof and finite evidence, not the selected construction. diff --git a/research/global-star-puncture/independent.py b/research/global-star-puncture/independent.py new file mode 100644 index 0000000000..92c6559dee --- /dev/null +++ b/research/global-star-puncture/independent.py @@ -0,0 +1,242 @@ +#!/usr/bin/env python3 +"""Independent parity-check replay for the finite proper-star puncture cases. + +Ports and incidence are regenerated locally. The parity-check matrix H is +the full kernel of the proper-star incidence matrix G, found by list-valued +GF2 RREF, rather than packed-integer row-space membership. No other verifier +or prototype is imported. Exact completeness follows from checked ranks +and G H^T = 0. The replay concerns only (p, k) = (5, 4), (6, 4); it is not a +formal proof of a general puncture theorem or the multiplication theorem. + +Copyright 2026 Luke Mansoor. Apache-2.0. +Prepared with substantial OpenAI Codex assistance. +""" +import argparse +from itertools import combinations, product +import json +from math import comb + + +EXPECTED = { + 5: {"ports": 80, "stars": 131, "rank": 65, "check_rank": 15, + "pair_syndromes": 1345, "minimum_weight": 4}, + 6: {"ports": 240, "stars": 233, "rank": 155, "check_rank": 85, + "pair_syndromes": 28680, "minimum_weight": 6}, +} + + +class VerificationError(RuntimeError): + """A proof-relevant obligation failed, also under python -O.""" + + +def require(condition, message): + if not condition: + raise VerificationError(message) + + +def enumerate_ports(pair_count, size): + """Sorted-coordinate tuples, one coordinate per selected pair.""" + return [tuple(2 * pair + sign for pair, sign in zip(pair_ids, signs)) + for pair_ids in combinations(range(pair_count), size) + for signs in product((0, 1), repeat=size)] + + +def incidence(stars, ports): + return [[int(all(coordinate in port for coordinate in star)) + for port in ports] for star in stars] + + +def rref(matrix): + """Exact GF2 RREF, mutating a copy; no packed integer arithmetic.""" + rows = [list(row) for row in matrix] + if not rows: + return [], [] + require(all(len(row) == len(rows[0]) for row in rows), + "RREF matrix is not rectangular") + require(all(value in (0, 1) for row in rows for value in row), + "RREF matrix has a nonbinary entry") + pivot_columns = [] + next_row = 0 + for column in range(len(rows[0])): + source = next((r for r in range(next_row, len(rows)) + if rows[r][column]), None) + if source is None: + continue + rows[next_row], rows[source] = rows[source], rows[next_row] + for r in range(len(rows)): + if r != next_row and rows[r][column]: + rows[r] = [a ^ b for a, b in zip(rows[r], rows[next_row])] + pivot_columns.append(column) + next_row += 1 + if next_row == len(rows): + break + return rows[:next_row], pivot_columns + + +def parity_check(generator): + """Construct H: free entry 1 and pivot entries from corresponding G rows.""" + reduced, pivots = rref(generator) + port_count = len(generator[0]) + free = [column for column in range(port_count) if column not in pivots] + result = [] + for column in free: + equation = [0] * port_count + equation[column] = 1 + for row, pivot in zip(reduced, pivots): + equation[pivot] = row[column] + result.append(equation) + return result, pivots, free + + +def dot(a, b): + require(len(a) == len(b), "dot product dimension mismatch") + return sum(x * y for x, y in zip(a, b)) % 2 + + +def orthogonal(generator, check): + return all(dot(row, equation) == 0 + for row in generator for equation in check) + + +def add_columns(a, b): + require(len(a) == len(b), "syndrome dimension mismatch") + return tuple(x ^ y for x, y in zip(a, b)) + + +def verify(pair_count): + """Return a deterministic finite receipt; raise on every failed obligation.""" + require(pair_count in EXPECTED, "only p=5 or p=6 is certified") + expected_case = EXPECTED[pair_count] + size = 4 + ports = enumerate_ports(pair_count, size) + stars = [star for level in range(size) + for star in enumerate_ports(pair_count, level)] + generator = incidence(stars, ports) + check, pivots, free = parity_check(generator) + port_count = len(ports) + require(port_count == (2 ** size) * comb(pair_count, size) + == expected_case["ports"], "port count changed") + require(len(stars) == sum((2 ** level) * comb(pair_count, level) + for level in range(size)) + == expected_case["stars"], "proper-star count changed") + require(len(pivots) == expected_case["rank"], "generator rank changed") + require(orthogonal(generator, check), "G H^T is nonzero") + h_reduced, h_pivots = rref(check) + require(len(h_reduced) == len(free) == port_count - len(pivots) + == expected_case["check_rank"], "nullspace completeness failed") + require(all(sum(row) % 2 == 0 for row in generator), + "a proper star has odd weight") + + columns = [tuple(row[column] for row in check) + for column in range(port_count)] + zero = (0,) * len(check) + require(all(column != zero for column in columns), + "weight-one codeword detected") + require(len(set(columns)) == port_count, + "weight-two codeword detected") + + pair_syndromes = {} + first_collision = None + for left, right in combinations(range(port_count), 2): + syndrome = add_columns(columns[left], columns[right]) + require(syndrome != zero, "zero pair syndrome detected") + if syndrome in pair_syndromes and first_collision is None: + first_collision = [list(pair_syndromes[syndrome]), [left, right]] + pair_syndromes.setdefault(syndrome, (left, right)) + require(len(pair_syndromes) == expected_case["pair_syndromes"], + "distinct pair-syndrome count changed") + + # Attaining witness: a single 3-star with its complete port support. + witness_star = (0, 2, 4) + witness = generator[stars.index(witness_star)] + witness_support = [i for i, value in enumerate(witness) if value] + require(all(dot(witness, equation) == 0 for equation in check), + "attaining witness has nonzero syndrome") + require(len(witness_support) == 2 * (pair_count - 3) + == expected_case["minimum_weight"], "witness weight changed") + if pair_count == 5: + # Nonzero distinct H columns exclude weight 1/2; parity excludes 3. + require(first_collision is not None, "expected weight-four collision absent") + minimum_distance = 4 + else: + # Unique pair sums exclude weight 4; row parity excludes odd weights. + require(first_collision is None, "weight-four codeword detected") + require(len(pair_syndromes) == comb(port_count, 2), + "pair-syndrome enumeration is incomplete") + minimum_distance = 6 + + # Every target and overlap correction: C_j = sum_{l=j}^3 C(l,j) B_l, + # where B_l is the sum of l-stars contained in the target. + star_indices = {star: index for index, star in enumerate(stars)} + overlap_rows_checked = 0 + for target in ports: + b_rows = {} + for level in range(1, size): + rows = [generator[star_indices[subset]] + for subset in combinations(target, level)] + b_rows[level] = [sum(row[s] for row in rows) % 2 + for s in range(port_count)] + for overlap in range(1, size): + supplied = [sum(comb(level, overlap) * b_rows[level][s] + for level in range(overlap, size)) % 2 + for s in range(port_count)] + expected = [int(sum(c in source for c in target) == overlap) + for source in ports] + require(supplied == expected, "overlap/star identity failed") + require(all(dot(expected, equation) == 0 for equation in check), + "overlap correction lies outside proper-star span") + overlap_rows_checked += 1 + require(overlap_rows_checked == 3 * port_count, + "overlap-row enumeration is incomplete") + + # Retain the independently derived H while corrupting G. Two flips in + # the same row preserve even parity, so orthogonality must detect them. + damaged_single = [row[:] for row in generator] + damaged_single[0][0] ^= 1 + require(not orthogonal(damaged_single, check), + "single-entry incidence corruption escaped detection") + require(sum(damaged_single[0]) % 2 == 1, "single-flip parity control failed") + damaged_pair = [row[:] for row in generator] + damaged_pair[0][0] ^= 1 + damaged_pair[0][1] ^= 1 + require(sum(damaged_pair[0]) % 2 == 0, "pair-flip parity control failed") + require(not orthogonal(damaged_pair, check), + "even-parity incidence corruption escaped detection") + + return { + "p": pair_count, "k": size, "ports": port_count, + "proper_stars_including_empty": len(stars), + "generator_rank": len(pivots), "check_rank": len(h_pivots), + "all_generator_rows_even": True, + "nonzero_distinct_syndrome_columns": port_count, + "pair_count": comb(port_count, 2), + "distinct_pair_syndromes": len(pair_syndromes), + "first_pair_collision": first_collision, + "minimum_nonzero_weight": minimum_distance, + "three_star_witness": list(witness_star), + "witness_port_indices": witness_support, + "witness_ports": [list(ports[i]) for i in witness_support], + "overlap_rows_checked": overlap_rows_checked, + "incidence_single_flip_rejected": True, + "incidence_parity_preserving_pair_flip_rejected": True, + "nullspace_free_columns": free, + } + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--json", action="store_true", help="emit the full deterministic receipt") + args = parser.parse_args() + results = [verify(p) for p in (5, 6)] + if args.json: + print(json.dumps({"status": "PASS", "method": "list-RREF-nullspace", + "results": results}, indent=2)) + else: + for result in results: + print("PASS independent p={p} k={k}: rank={generator_rank}/{ports}, " + "check-rank={check_rank}, minimum-weight={minimum_nonzero_weight}, " + "overlap-rows={overlap_rows_checked}, incidence-controls=2/2".format(**result)) + + +if __name__ == "__main__": + main() diff --git a/research/global-star-puncture/test_verify.py b/research/global-star-puncture/test_verify.py new file mode 100644 index 0000000000..2b6db983b9 --- /dev/null +++ b/research/global-star-puncture/test_verify.py @@ -0,0 +1,80 @@ +#!/usr/bin/env python3 +"""Relocation and failure-detection tests for the exact research receipt. + +Copyright 2026 Luke Mansoor. Apache-2.0. Substantial OpenAI Codex assistance. +""" +import json +from pathlib import Path +import shutil +import subprocess +import sys +import tempfile +import unittest + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] + + +class ReceiptTests(unittest.TestCase): + def setUp(self): + self.scratch = tempfile.TemporaryDirectory(prefix="global-star-puncture-",dir=ROOT) + self.root = Path(self.scratch.name).resolve() + self.package = self.root / "research/global-star-puncture" + self.package.mkdir(parents=True) + for name in ("verify.py","independent.py","SOURCES.json","RESULTS.json"): + shutil.copyfile(HERE / name, self.package / name) + for item in json.loads((HERE / "SOURCES.json").read_text(encoding="utf-8"))["context"]: + target = self.root / item["path"] + target.parent.mkdir(parents=True,exist_ok=True) + shutil.copyfile(ROOT / item["path"],target) + + def tearDown(self): + # The cleanup target is exactly the temporary directory created above. + self.assertEqual(self.root, Path(self.scratch.name).resolve()) + self.assertEqual(self.root.parent, ROOT.resolve()) + self.scratch.cleanup() + + def run_checker(self, *arguments): + return subprocess.run([sys.executable,"-I","-O","-B", + str(self.package / "verify.py"),*arguments], + cwd=self.root.parent,capture_output=True,text=True,timeout=30) + + def test_relocated_export(self): + exported = self.root / "export.json" + result = self.run_checker("--write",str(exported)) + self.assertEqual(result.returncode,0,result.stderr) + self.assertIn("PASS_GLOBAL_STAR_PUNCTURE",result.stdout) + self.assertEqual(json.loads(exported.read_text()), + json.loads((HERE / "RESULTS.json").read_text())) + + def test_receipt_corruption_preserves_output(self): + receipt = self.package / "RESULTS.json" + changed = json.loads(receipt.read_text()) + changed["bitset_quotient"][0]["minimum_weight"] = 3 + receipt.write_text(json.dumps(changed),encoding="utf-8") + exported = self.root / "existing.json" + exported.write_text("preserve me",encoding="utf-8") + result = self.run_checker("--write",str(exported)) + self.assertNotEqual(result.returncode,0) + self.assertIn("committed receipt differs",result.stderr) + self.assertEqual(exported.read_text(),"preserve me") + + def test_context_corruption(self): + with (self.root / "CONTRIBUTING.md").open("a",encoding="utf-8") as handle: + handle.write("\nchanged provenance\n") + result = self.run_checker() + self.assertNotEqual(result.returncode,0) + self.assertIn("pinned context bytes changed",result.stderr) + + def test_source_pin_corruption(self): + source = self.package / "SOURCES.json" + changed = json.loads(source.read_text()) + changed["context"][0]["sha256"] = "0" * 64 + source.write_text(json.dumps(changed),encoding="utf-8") + result = self.run_checker() + self.assertNotEqual(result.returncode,0) + self.assertIn("pinned context bytes changed",result.stderr) + + +if __name__ == "__main__": + unittest.main() diff --git a/research/global-star-puncture/verify.py b/research/global-star-puncture/verify.py new file mode 100644 index 0000000000..17815e755c --- /dev/null +++ b/research/global-star-puncture/verify.py @@ -0,0 +1,319 @@ +#!/usr/bin/env python3 +"""Exact evidence for the global proper-star puncture theorem; standard library. + +Copyright 2026 Luke Mansoor. Apache-2.0. +Prepared with substantial OpenAI Codex assistance. Finite replay is not a +formal proof of the general theorem or of integer multiplication. +""" +import argparse +from hashlib import sha256 +import importlib.util +from itertools import combinations, product +import json +from math import comb +from pathlib import Path + +HERE = Path(__file__).resolve().parent +SEED = 43 + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def ports(p, k): + return [sum(1 << (2 * q + s) for q, s in zip(qs, signs)) + for qs in combinations(range(p), k) + for signs in product((0, 1), repeat=k)] + + +def generator(p, k): + family = ports(p, k) + stars = [s for degree in range(k) for s in ports(p, degree)] + rows = [sum(1 << i for i, source in enumerate(family) + if source & star == star) for star in stars] + return family, stars, rows + + +def echelon(rows): + basis = {} + for original in rows: + row = original + while row: + pivot = row.bit_length() - 1 + if pivot in basis: + row ^= basis[pivot] + else: + basis[pivot] = row + break + return basis + + +def reduce(row, basis): + for pivot in sorted(basis, reverse=True): + if row >> pivot & 1: + row ^= basis[pivot] + return row + + +def syndrome(row, columns): + value = 0 + while row: + bit = row & -row + value ^= columns[bit.bit_length() - 1] + row ^= bit + return value + + +def coordinates(port): + return [i for i in range(port.bit_length()) if port >> i & 1] + + +def cube(slots, p, k): + require(len(slots) == k and all(len(set(s)) == 2 for s in slots), + "cube needs k slots with two distinct alternatives") + used = set() + for a, b in slots: + require(0 <= a < 2 * p and 0 <= b < 2 * p, "cube coordinate range") + pairs = {a // 2, b // 2} + require(not used & pairs, "cube slots share a physical pair") + used |= pairs + vertices = [sum(1 << c for c in chosen) for chosen in product(*slots)] + require(len(set(vertices)) == 1 << k, "cube vertices repeat") + require(all(v.bit_count() == k and len({c // 2 for c in coordinates(v)}) == k + for v in vertices), "cube contains an invalid port") + return vertices + + +def generalized_face_checks(p, k, family, stars, rows, target): + qs = sorted(c // 2 for c in coordinates(target)) + outside = [q for q in range(p) if q not in qs] + lookup = {port: i for i, port in enumerate(family)} + ordinary = set(cube([(2*q, 2*q+1) for q in qs], p, k)) + count = 0 + for codimension in range(min(len(outside), k) + 1): + for fixed in combinations(range(k), codimension): + for signs in product((0, 1), repeat=codimension): + assignment = dict(zip(fixed, signs)) + slots = [(2*q, 2*q+1) for q in qs] + for position, slot in enumerate(fixed): + slots[slot] = (2*qs[slot] + assignment[slot], + 2*outside[position] + (SEED + position) % 2) + vertices = cube(slots, p, k) + face = {v for v in ordinary + if all(v >> (2*qs[i] + sign) & 1 + for i, sign in assignment.items())} + require(set(vertices) & ordinary == face, "generalized cube face intersection") + mask = sum(1 << lookup[v] for v in vertices) + require(all((mask & row).bit_count() % 2 == 0 for row in rows), + "proper star has odd generalized-cube parity") + # Independent direct monomial count checks the packed predicate. + require(all(sum(v & s == s for v in vertices) % 2 == 0 for s in stars), + "direct generalized-cube monomial count") + count += 1 + return count + + +def finite_case(p, k): + family, stars, rows = generator(p, k) + n = len(family) + basis = echelon(rows) + labels = [reduce(1 << i, basis) for i in range(n)] + require(all(syndrome(row, labels) == 0 for row in rows), "quotient fails to annihilate G") + require(len(echelon(labels)) == n - len(basis), "quotient rank-nullity") + require(all(row.bit_count() % 2 == 0 for row in rows), "odd proper-star weight") + require(all(labels) and len(set(labels)) == n, "zero or repeated syndrome column") + pair_values = {labels[a] ^ labels[b] for a, b in combinations(range(n), 2)} + if p == 6: + require(len(pair_values) == comb(n, 2), "weight-four codeword exists") + target_index = SEED % n + target = family[target_index] + jstar = sum(1 << c for c in coordinates(target)[:-1]) + witness = rows[stars.index(jstar)] + support = [i for i in range(n) if witness >> i & 1] + require(target_index in support, "attaining star misses target") + require(len(support) == 2*(p-k+1), "sharp witness weight") + require(syndrome(witness, labels) == 0, "attaining star fails dual") + correction_count = 0 + for t in family: + for overlap in range(1, k): + exact = sum(1 << i for i, s in enumerate(family) + if (s & t).bit_count() == overlap) + absorbed = 0 + for degree in range(overlap, k): + if comb(degree, overlap) % 2: + for star in ports(p, degree): + if star & t == star: + absorbed ^= rows[stars.index(star)] + require(exact == absorbed, "overlap correction absorption fails") + require(syndrome(exact, labels) == 0, "correction not in star span") + correction_count += 1 + controls = [] + for name, changed in [("single incidence flip", rows[0] ^ 1), + ("even-parity two-entry flip", rows[0] ^ 3), + ("forbidden degree-k singleton star", 1 << target_index)]: + require(syndrome(changed, labels) != 0, "negative control accepted: " + name) + controls.append(name) + overlap_zero = sum(1 << i for i, s in enumerate(family) if not s & target) + require(syndrome(overlap_zero, labels) != 0, "overlap-zero control accepted") + controls.append("forbidden overlap-zero correction") + damaged = labels[:] + damaged[target_index] = 0 + require(any(syndrome(row, damaged) != 0 for row in rows), "damaged dual accepted") + controls.append("zeroed dual column") + slots = [(2*q, 2*q+1) for q in range(k)] + slots[0] = (0, 2) + try: + cube(slots, p, k) + except ValueError: + controls.append("generalized cube reusing a physical pair") + else: + raise ValueError("invalid cube accepted") + return dict(p=p, k=k, ports=n, stars_including_empty=len(stars), + generator_rank=len(basis), dual_rank=n-len(basis), + minimum_weight=len(support), minimum_one_target_deletions=len(support)-1, + distinct_syndrome_columns=len(set(labels)), + pair_count=comb(n, 2), distinct_pair_syndromes=len(pair_values), + quotient_columns_hex=[hex(label) for label in labels], + target_index=target_index, target=coordinates(target), star=coordinates(jstar), + deleted_ports=[coordinates(family[i]) for i in support if i != target_index], + correction_rows=correction_count, + generalized_face_cubes=generalized_face_checks(p,k,family,stars,rows,target), + negative_controls=controls) + + +def face_lemma_exhaustion(): + results = [] + for dimension in range(1, 5): + n = 1 << dimension + for budget in range(dimension + 1): + faces = [] + for codimension in range(budget + 1): + for fixed in combinations(range(dimension), codimension): + for values in product((0, 1), repeat=codimension): + faces.append(sum(1 << point for point in range(n) + if all(point >> bit & 1 == value + for bit, value in zip(fixed, values)))) + admitted = [s for s in range(1, 1 << n) + if all((s & f).bit_count() % 2 == 0 for f in faces)] + minimum = min((s.bit_count() for s in admitted), default=None) + require(minimum == (1 << (budget + 1) if budget < dimension else None), + "even-face lemma finite minimum differs") + results.append(dict(dimension=dimension, codimension_budget=budget, + support_sets=(1 << n)-1, admitted_nonempty=len(admitted), + minimum_weight=minimum)) + return results + + +def span_exhaustion(): + results = [] + for p,k in [(2,2),(3,2),(4,2),(5,2),(6,2),(3,3),(4,4)]: + family, _, rows = generator(p,k) + basis = list(echelon(rows).values()) + span = [0] + for row in basis: + span += [value ^ row for value in span] + minimum = min(value.bit_count() for value in span if value) + require(minimum == 2*(p-k+1), "complete small-span distance mismatch") + results.append(dict(p=p,k=k,ports=len(family),rank=len(basis), + codewords=len(span),minimum_weight=minimum)) + # At non-power-of-two k, the allowed corrections escape the star code: + # target-local 1-stars plus overlap-1 isolate a target for k=3. + family, stars, rows = generator(4,3) + target = family[SEED % len(family)] + coefficient = 0 + for coordinate in coordinates(target): + coefficient ^= rows[stars.index(1 << coordinate)] + coefficient ^= sum(1 << i for i,s in enumerate(family) if (s & target).bit_count() == 1) + require(coefficient == 1 << family.index(target), "non-power-of-two positive control") + require(reduce(coefficient, echelon(rows)) != 0, "power-of-two scope control failed") + return results + + +def nonlocal_sharp_witness(): + family, stars, rows = generator(5,4) + target_index = SEED + target = family[target_index] + sets = [(2,), (0,2), (2,4), (2,5), (2,6), + (0,2,4), (0,2,5), (0,2,6), (2,4,6), (2,5,6)] + coefficient = 0 + for subset in sets: + coefficient ^= rows[stars.index(sum(1 << c for c in subset))] + support = [i for i in range(len(family)) if coefficient >> i & 1] + require(support == [0,2,42,43], "nonlocal sharp witness support differs") + deleted = [0,2,42] + live_mask = sum(1 << i for i in range(len(family)) if i not in deleted) + require(coefficient & live_mask == 1 << target_index, "global punctured identity fails") + local_rows = [row & live_mask for s,row in zip(stars,rows) if s and s & target == s] + for j in (1,2,3): + local_rows.append(sum(1 << i for i,s in enumerate(family) + if i not in deleted and (s & target).bit_count() == j)) + require(reduce(1 << target_index,echelon(local_rows)) != 0, + "target-local cell criterion unexpectedly survives off-target witness") + intersections = {s & target for s in family} + surviving = {s & target for i,s in enumerate(family) if i not in deleted} + require(intersections == surviving, "nonlocal example empties an intersection cell") + return dict(p=5,k=4,target_index=target_index,target=coordinates(target), + stars=[list(s) for s in sets], support_indices=support, + deleted_indices=deleted, deleted_ports=[coordinates(family[i]) for i in deleted], + all_intersection_cells_survive=True, global_decoder_passes=True, + target_local_decoder_infeasible=True, + control="The minimum threshold extends globally; the local cell criterion does not") + + +def verify(): + spec = importlib.util.spec_from_file_location("independent_global_star", HERE / "independent.py") + module = importlib.util.module_from_spec(spec) + spec.loader.exec_module(module) + cases = [finite_case(p,4) for p in (5,6)] + independent = [module.verify(p) for p in (5,6)] + for a,b in zip(cases,independent): + for left,right in [("ports","ports"),("generator_rank","generator_rank"), + ("dual_rank","check_rank"),("minimum_weight","minimum_nonzero_weight"), + ("distinct_pair_syndromes","distinct_pair_syndromes"), + ("correction_rows","overlap_rows_checked")]: + require(a[left] == b[right], "independent implementations disagree: " + left) + return dict(status="PASS", assignment_seed=SEED, + scope="Exact finite evidence for README's written general proof; no new kappa", + bitset_quotient=cases, list_rref_nullspace=independent, + even_face_exhaustion=face_lemma_exhaustion(), + complete_small_spans=span_exhaustion(), + nonlocal_sharp_witness=nonlocal_sharp_witness(), + non_power_of_two_escape_control="PASS") + + +def verify_provenance(): + source = json.loads((HERE / "SOURCES.json").read_text(encoding="utf-8")) + require(source["base_commit"] == "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "unexpected provenance base") + require(source["selected_kappa"] == "51110230636731/31250000000000000", + "unexpected selected context") + root = HERE.parents[1] + for item in source["context"]: + path = (root / item["path"]).resolve() + require(path.is_relative_to(root.resolve()), "context pin escapes repository") + require(sha256(path.read_bytes()).hexdigest() == item["sha256"], + "pinned context bytes changed: " + item["path"]) + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--write", type=Path, help="write a recomputed receipt after all checks") + args = parser.parse_args() + verify_provenance() + result = verify() + expected_path = HERE / "RESULTS.json" + if expected_path.exists(): + require(result == json.loads(expected_path.read_text(encoding="utf-8")), + "committed receipt differs from recomputed evidence") + else: + require(args.write is not None, "missing committed receipt") + if args.write: + args.write.write_text(json.dumps(result, indent=2, sort_keys=True) + "\n", encoding="utf-8") + print("PASS_GLOBAL_STAR_PUNCTURE: sharp deletion thresholds 3/5; " + "2 independent F2 engines; 960 correction rows; 12 negative controls") + + +if __name__ == "__main__": + main()