diff --git a/research/p104-two-channel-support/PORTS.json b/research/p104-two-channel-support/PORTS.json new file mode 100644 index 0000000000..b964c3ae2e --- /dev/null +++ b/research/p104-two-channel-support/PORTS.json @@ -0,0 +1 @@ +[11, 19, 35, 131, 259, 13, 21, 37, 69, 133, 261, 41, 73, 265, 49, 81, 145, 273, 161, 193, 321, 385, 14, 22, 38, 70, 134, 262, 26, 74, 138, 50, 146, 274, 98, 290, 194, 322, 386, 28, 44, 140, 268, 84, 148, 276, 100, 164, 292, 196, 324, 388, 56, 88, 152, 280, 168, 296, 200, 328, 392, 112, 176, 304, 208, 336, 400, 224, 352, 416, 508, 506, 502, 494, 478, 446, 382, 254, 505, 501, 493, 477, 445, 381, 253, 499, 475, 443, 379, 251, 487, 471, 439, 375, 247, 463, 431, 367, 239, 415, 351, 223, 319, 191] \ No newline at end of file diff --git a/research/p104-two-channel-support/PROOF.md b/research/p104-two-channel-support/PROOF.md new file mode 100644 index 0000000000..b01410b5a4 --- /dev/null +++ b/research/p104-two-channel-support/PROOF.md @@ -0,0 +1,154 @@ +# Exact second support weight of the P104 root code + +This contribution was produced by Nick Petalas. New material is Apache-2.0. + +## 1. Object and inherited input + +Use the ordered 104 odd-weight binary ports in `PORTS.json`, copied byte for +byte from Matarener's [PR6166 coordinate fixture](https://github.com/CrocSwap/integer-mult-bounds/blob/096938513138868f0ed27639061f1a5054900f96/research/p104-carrier-code-uniqueness/e8/ports.json). +Coordinates of a binary port are indexed 0 through 8. Its rational root is + +- `r(q) = e_i - e_j` for a weight-seven port with zeros `i < j`; +- `r(q) = sum_{i in supp(q)} e_i - (1/3) sum_{i=0}^8 e_i` for a weight-three port. + +Let `M[a,b] = r(q_a) . r(q_b) / 2`. Although the roots use thirds, every +entry of M is an integer or a half-integer. Reduce these entries modulo 3, +using `1/2 = 2`. The clique indices + +```text +T = (1, 5, 18, 20, 80, 85, 100, 103) +``` + +give `M[T,T] = I_8`, over both Q and F3. Write `G = M[T,:]` and let `C_Q` +and `C_3` be its row spaces over Q and F3 respectively. These definitions +specify the two codes independently of any word replay. + +The identification of `C_3`, up to coordinate signs, with every +8-dimensional ternary P104 decoding code is Matarener's PR6166 theorem. +Its code uniqueness, single-channel weight 49, and binary hyperplane port +capacity 60 are cited dependencies, not newly checked results here. The +predecessor's local-word lineage is Ali Romman PR5827 and DreamingOfClouds +PR5907/6030, with their retained E8/native/controller contributors. + +## 2. Statement + +For a linear code C define its second generalized support weight by + +```text +d_2(C) = min |supp(u) union supp(v)|, + over linearly independent u,v in C. +``` + +The finite certificate proves + +```text +d_2(C_3) = d_2(C_Q) = 72. +``` + +There are exactly 704 minimizing two-dimensional subcodes of `C_3`. +This count is a finite enumeration, not a classification up to symmetry. +The value 72 and these minimizers are the new result. The mathematical +notion of a generalized Hamming weight is standard. + +## 3. Exhaustive lower bound over F3 + +Since G restricts to the identity on T, the map `c -> cG` is injective on +`F3^8`. Every projective coefficient line has exactly one representative +whose first nonzero entry is 1. Enumerating the eight trits gives + +```text +(3^8 - 1)/2 = 3280 representatives. +``` + +Two distinct representatives are linearly independent. Every independent +pair of codewords has the same support union as one of the unordered +pairs of representatives. Thus all cases are covered by + +```text +binomial(3280,2) = 5377560 pairs. +``` + +`verify.py` evaluates each representative at all 104 coordinates and stores +its exact support as an integer bitset. For each distinct pair it computes +`(support_a | support_b).bit_count()`. The complete histogram, recomputed +on every replay and compared to `RESULT.json`, has minimum 72. + +An F3 plane has four projective lines and six unordered pairs. Every pair +in that plane spans it and has the same support union. The replay forms +the four canonical representatives of every minimizing plane as +`a, b, a+b, a+2b`, then groups their sorted tuples. It obtains 4224 pairs +in 704 groups and checks that every group occurs exactly six times. +The total number of planes covered by the pair census is 5377560/6 = 896260. +No support test is sampled or inferred from the minimum-weight distribution. + +The 832 Gram entries used to construct G are checked by two expressions: +the intersection-size formula and explicit nine-coordinate rational roots. +This is a construction check for this certificate, not a replay of the +predecessor's uniqueness proof or its word counts. + +## 4. Rational lower bound and sharp witness + +Suppose a two-dimensional subspace of `C_Q` is supported on a set S of +fewer than 72 coordinates. Its coefficient plane is in the kernel of +`G[:, outside(S)]^T`, so that rational matrix has rank at most six. +All its denominators are powers of two. Reduction modulo 3 cannot raise +its rank, since a nonzero reduced minor has a nonzero rational determinant. +Its F3 kernel therefore has dimension at least two. Injectivity of the +ternary coefficient map gives a two-dimensional subcode of `C_3` supported +inside S, contradicting section 3. Hence `d_2(C_Q) >= 72`. + +In the ordered eight-row basis G, take + +```text +a = (0,0,0,1,0,0,0,0) +b = (0,0,0,0,1,1,1,0). +``` + +Their coefficient minor on positions 3 and 4 is the identity. Their rational +codewords have individual weights 49 and 71, and their union has weight 72. +Over F3 their individual weights are 49 and 69 and their union is the same +72-coordinate set. The checker calculates every rational and ternary entry; +`RESULT.json` records the union as binary port values. This proves sharpness +in both fields. The rational assertion follows from exact arithmetic and +the rank argument, rather than identifying rational zeros with modular zeros. + +A useful transfer also applies to a 3-integral systematic generator H of an +8-dimensional rational code, if its reduction is coordinate-sign-equivalent +to `C_3`. The same minor argument proves `d_2(row_Q H) >= 72`. This is a +conditional implication; it does not classify rational decoding codes. + +## 5. Scoped common-frame consequence + +Assume a rational code has the reduction specified in the preceding +paragraph. If two independent channel rows in that code are both acquired +from ports in one binary frame F, then F contains their support union. +It therefore contains at least 72 ports. The cited PR6166 hyperplane +capacity is 60. Every proper subspace of `F2^9` is contained in a hyperplane, +so `F = F2^9`. + +Dually, suppose two independent receiver-coefficient columns are in a code +with the same support bound. If every receiver of either column must accept +its delivery in one common landing frame B, and partner l's legal frame is +inside `q_l^perp`, then + +```text +B subset intersection_{l in union of receiver supports} q_l^perp = {0}. +``` + +The equality holds because those at least 72 binary ports span `F2^9` by +the same capacity bound. Thus a common landing frame must be ZERO. + +This is a conditional obstruction to common-frame synchronization. It does +not say that two independently scheduled channels each require FULL-to-ZERO +descent. With distinct acquisition or delivery cuts, a nine-dimensional +partner code, extra canceling carrier directions, or public relays, the +common-frame hypotheses can fail. No additional paid cost is inferred +without an actual trajectory and complete invoice. + +## 6. Verification boundary + +The exhaustive claim is about the specified 104-coordinate codes. No +selected word, native operator, compiler, outer supplier, rounded multiplier, +or predecessor uniqueness certificate is replayed. The common-frame +consequence uses the named predecessor capacity and the stated code/support +hypotheses. Human and formal proof-kernel review are unclaimed. diff --git a/research/p104-two-channel-support/README.md b/research/p104-two-channel-support/README.md new file mode 100644 index 0000000000..a570b1ac58 --- /dev/null +++ b/research/p104-two-channel-support/README.md @@ -0,0 +1,100 @@ +# Two independent P104 root-code channels need 72 ports + +The exact second generalized support weight of the specified P104 root code +is **72**, both over F3 and over Q. There are **704** minimizing ternary +two-dimensional subcodes. This is a finite certificate with a scoped proof; +no new kappa or cheaper physical word is claimed. + +Matarener's [PR6166](https://github.com/CrocSwap/integer-mult-bounds/pull/6166) +identifies the ternary code and proves its single-channel minimum 49. The +new quantity is the minimum union of supports of two independent channels. +An explicit independent pair attains 72. The full 5,377,560 projective-pair +census proves the lower bound. [PROOF.md](PROOF.md) gives the coverage +argument and lifts the result to rational coefficients by a minor argument. +The predecessor theorem is cited, not independently validated here. + +The shared-frame consequence is narrow but useful. With PR6166's cited +binary hyperplane capacity 60, a common acquisition frame for two such +independent channels must be FULL. A common landing frame for two independent +receiver columns satisfying the same code hypothesis must be ZERO. These +are constraints on synchronized sharing; they do not exclude separately +scheduled carriers, relays or larger partner codes. + +## Reproduce + +From the repository root, using CPython 3.12 and its standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/p104-two-channel-support/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/p104-two-channel-support +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/p104-two-channel-support --check-source-history +``` + +Use any CPython 3.12 interpreter in place of the local path. Both registered +normal and optimized commands must print +`PASS_P104_TWO_CHANNEL_SUPPORT d2=72 pairs=5377560 minimizing_subcodes=704`. +The runner must print `PASS_REGISTERED_RESEARCH_PACKAGE`. + +Normal replay only reads files. The generated [RESULT.json](RESULT.json) +binds all seven proof/input/metadata files by SHA256 and records the complete +support histogram, census counts and rational/ternary witness. To regenerate +it explicitly, pass `--emit-receipt /path/to/RESULT.json`. A changed receipt +is rejected, including under optimized Python. + +## Source and scope + +`PORTS.json` retains the exact coordinate bytes from PR6166 at +`096938513138868f0ed27639061f1a5054900f96`. Its URL, SHA256 and source role are +in [SOURCES.json](SOURCES.json). That open PR head is external to this +publication's ancestry; the generic source-history check covers the canonical +catalogue and selected record, not the external head. The direct verifier +checks the retained coordinate bytes against their recorded hash and derives +all code entries locally. No predecessor executable or proof is copied. + +Base `3f0152a32eeebac0df11946dbd50cabe5a7f7839`, priority revision 8. +The selected source-binding baseline passed. The selected conditional +κ = 0.003125804 is unchanged. Main, merged-PR, live open-PR and Discussion +searches found no same-question result; these bounded searches do not prove +novelty. The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19267579) +states the ternary target. The same certificate also supplies the rational +lift, without another search. + +All loops have fixed bounds: 104 ports, nine root coordinates, eight +coefficient coordinates, 6561 coefficient tuples, 3280 projective words and +5,377,560 pairs. Minimizer storage is at most the finite pair count and in +this certificate holds 4224 pairs. Each function is under 60 lines. Checks +use explicit exceptions and remain active under `-O`. CPython and Fraction +allocate dynamically; this is a documented Power of Ten rule 3 deviation +bounded by these fixed census sizes and input dimensions. There is no +recursion, network, subprocess, dynamic code execution or normal replay write. +Warning-strict normal and optimized replay provide the recurring diagnostics. + +Limitations are mathematical as well as practical. This is not a theorem +about arbitrary nine-dimensional decoding codes or asynchronous relay +programs. Complete native, caller, restoration, stock/precision, compiler and +outer costs remain open and are not assigned zero. No Lean, selected-native +or complete multiplication replay is run. Independent human and formal +proof-kernel review are unclaimed. + +## Open next questions + +- Can an asynchronous relay use distinct acquisition and delivery cuts to + avoid the common-frame constraint and improve a complete invoice? Start + with two explicit independent channel rows and pay for every transition + and restoration in an actual caller. That caller and its invoice are missing. +- What joint-support bound holds for a specified nine-dimensional decoding + code outside the minimal-code reduction? First exhibit the code and two + delivered channels. Its decoding and physical delivery contracts remain + blockers. No larger-code census is included here. + +[TASK.json](TASK.json) records the same questions and scope change. + +## Credit + +This contribution was produced by Nick Petalas. Credit Matarener PR6166 for +the decoding-code identification, source coordinates, single-channel result +and cited frame capacity; Ali Romman PR5827 and DreamingOfClouds PR5907/6030 +for the retained local-word lineage; and their E8, native, helper, controller +and compiler predecessors. Generalized Hamming weights and rank reduction +by minors are standard. The new contribution is this exact joint-support +certificate, rational lift and scoped common-frame consequence. Apache-2.0. diff --git a/research/p104-two-channel-support/RESULT.json b/research/p104-two-channel-support/RESULT.json new file mode 100644 index 0000000000..436d974aa6 --- /dev/null +++ b/research/p104-two-channel-support/RESULT.json @@ -0,0 +1,154 @@ +{ + "claim_type": "finite certificate and scoped support/frame proof", + "independent_projective_pairs": 5377560, + "minimizing_pairs": 4224, + "minimizing_subcodes": 704, + "pair_support_histogram": { + "100": 2352, + "101": 384, + "72": 4224, + "74": 2472, + "76": 4224, + "77": 672, + "78": 11520, + "79": 4032, + "80": 1680, + "81": 288, + "82": 288, + "83": 10080, + "84": 62208, + "85": 127296, + "86": 167040, + "87": 138240, + "88": 103296, + "89": 124800, + "90": 247680, + "91": 267648, + "92": 739920, + "93": 1183296, + "94": 977280, + "95": 620352, + "96": 354720, + "97": 147840, + "98": 59520, + "99": 14208 + }, + "projective_words": 3280, + "second_support_weight": 72, + "source_hashes": { + "PORTS.json": "ba6a0b9cf76b7cccc1ce8b3d1aa78a4aa329b34d45aded694648f0cf43fc9fce", + "PROOF.md": "6b5ac6db79590c7fe8ad995fa2e570451470a1cfa1bc266fbd2a28df6898f128", + "README.md": "5c8419289c74d5a75d8749fa05d4f3638a9b92941e4d98ccca824064e102c88e", + "SOURCES.json": "05d31fb92bbfa27834410963cbb3cd8024309ab7f470e94040f30f6a129c3993", + "TASK.json": "5bb162d50d7d933da1d2a9e9d3fe89f08fb68df28b6775c2eba80dfd0a65d04d", + "VERIFY.json": "ee77ede2ed660e6b4eff616c68b333fda49f315d0ab1c37365d70ec603467b80", + "verify.py": "747383a46e0bc785f99fc68a9564b2d1e4768370c3049054b296df123569dbb1" + }, + "two_dimensional_subcodes": 896260, + "witness": { + "coefficients": [ + [ + 0, + 0, + 0, + 1, + 0, + 0, + 0, + 0 + ], + [ + 0, + 0, + 0, + 0, + 1, + 1, + 1, + 0 + ] + ], + "rational_individual_weights": [ + 49, + 71 + ], + "ternary_individual_weights": [ + 49, + 69 + ], + "union_ports": [ + 35, + 259, + 37, + 69, + 261, + 73, + 265, + 81, + 145, + 273, + 193, + 321, + 385, + 14, + 22, + 38, + 70, + 134, + 262, + 26, + 138, + 50, + 146, + 98, + 290, + 322, + 28, + 44, + 140, + 148, + 100, + 164, + 292, + 324, + 56, + 88, + 152, + 280, + 168, + 200, + 328, + 392, + 176, + 208, + 336, + 400, + 352, + 508, + 506, + 502, + 494, + 478, + 382, + 501, + 493, + 445, + 381, + 253, + 499, + 443, + 379, + 251, + 471, + 439, + 247, + 463, + 431, + 239, + 415, + 351, + 223, + 319 + ] + } +} diff --git a/research/p104-two-channel-support/SOURCES.json b/research/p104-two-channel-support/SOURCES.json new file mode 100644 index 0000000000..78a486e5d8 --- /dev/null +++ b/research/p104-two-channel-support/SOURCES.json @@ -0,0 +1,32 @@ +{ + "schema_version": 1, + "base_commit": "3f0152a32eeebac0df11946dbd50cabe5a7f7839", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + } + ], + "external_sources": [ + { + "repository": "CrocSwap/integer-mult-bounds", + "pr": 6166, + "author": "Matarener", + "head": "096938513138868f0ed27639061f1a5054900f96", + "path": "research/p104-carrier-code-uniqueness/e8/ports.json", + "url": "https://github.com/CrocSwap/integer-mult-bounds/blob/096938513138868f0ed27639061f1a5054900f96/research/p104-carrier-code-uniqueness/e8/ports.json", + "local_path": "PORTS.json", + "sha256": "ba6a0b9cf76b7cccc1ce8b3d1aa78a4aa329b34d45aded694648f0cf43fc9fce", + "role": "Exact coordinate fixture; predecessor theorem cited, not replayed.", + "history_limit": "The open PR head is external to publication ancestry. Its coordinate bytes are retained locally and hash-checked; no Git source-history claim is made for that head." + } + ] +} diff --git a/research/p104-two-channel-support/TASK.json b/research/p104-two-channel-support/TASK.json new file mode 100644 index 0000000000..a381d7d66c --- /dev/null +++ b/research/p104-two-channel-support/TASK.json @@ -0,0 +1,93 @@ +{ + "schema_version": 1, + "task_id": "complex-rank-shape-decoder", + "priority_revision": 8, + "base_commit": "3f0152a32eeebac0df11946dbd50cabe5a7f7839", + "original_card": { + "id": "complex-rank-shape-decoder", + "question": "Can a legal decoder or coframe change improve the full signed moment, including changed helper targets?", + "starting_points": [ + "docs/research/current-priorities.md", + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "docs/research/recursive-invoice-preflight.md" + ], + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "acceptance_gate": "A source-bound arbitrary-input identity and legal producer/consumer boundary with the complete paid and productive target invoice, including restoration, ownership, native alignment and extra charges. Price under the actual current model; historical ceiling.py assumptions must be established before use. A favorable optimistic relaxation keeps a route open but is not a completed supplier. A scoped local result remains useful; expansion requires the family-level budget gate.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "first_experiment": "Price one complete changed itinerary with both paid and productive histograms. Check #5693/#5698 for overlap and their exact hypotheses before another coframe search. Use the signed invoice preflight where its boundary contract agrees; an inconclusive concave comparison is not a power crossing. Stop if an optimistic complete budget fails at the chosen target or native delivery remains unspecified.", + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "allowed_variations": [ + "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes." + ], + "scope_change_triggers": [ + "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.", + "Treating an archived proposal or local numerical pass as complete supplier admission." + ], + "overlap_terms": [ + "coframe", + "signed moment", + "5693", + "5698" + ], + "existing_checks": [ + { + "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "status": "reviewed", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Exact second generalized support weight 72 of the specified ternary P104 root code, its rational lift, and a common-frame two-channel obstruction.", + "scope_change_reason": "The original decoder search is narrowed to a new joint-support invariant prompted by PR6166. This is a finite algebraic obstruction, not a cheaper decoder or a re-verification of code uniqueness.", + "bottleneck_link": "A common acquisition or common landing for two independent minimal-code channels must accommodate at least 72 ports. With the cited hyperplane capacity 60, its frame must be FULL or ZERO respectively. This constrains a specific synchronized sharing model, without excluding multi-stage relays.", + "budget_minutes": 60, + "stop_rule": "Stop after the first exact second-weight certificate and package it; do not extend to larger subcodes or classify nine-dimensional codes.", + "outcome": "completed", + "evidence": "PROOF.md; full projective-pair enumeration and rational witness in verify.py; generated hash-bound RESULT.json.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can an asynchronous relay avoid the FULL/ZERO common-frame constraint and still improve a complete paid/target invoice?", + "why_it_matters": "The obstruction applies only when both source supports or both receiver supports must share one frame.", + "first_step": "Specify two independent channel rows, their distinct acquisition and last-delivery cuts, and every paid frame transition and restoration.", + "blocked_by": "A chronological physical caller and full invoice; this support certificate does not supply them." + }, + { + "question": "What joint-support bounds hold for a nine-dimensional decoding code that is not constrained to the minimal root-code reduction?", + "why_it_matters": "The predecessor and this package leave a genuinely changed code space open.", + "first_step": "Exhibit a specified nine-dimensional code and an actual pair of independent delivered channels before optimizing a whole word.", + "blocked_by": "A new decoding code and legal delivery contract; no classification or search is supplied here." + } + ], + "source_question": { + "pr": 6166, + "author": "Matarener", + "scope": "New joint-support invariant for the multi-channel design question; the predecessor single-channel theorem is cited, not audited." + }, + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19267579", + "upstream_checkpoint": { + "commit": "3f0152a32eeebac0df11946dbd50cabe5a7f7839", + "priority_revision": 8, + "checked_utc": "2026-10-29T13:03:00.397486+00:00", + "selected_kappa": "781451/250000000" + } +} diff --git a/research/p104-two-channel-support/VERIFY.json b/research/p104-two-channel-support/VERIFY.json new file mode 100644 index 0000000000..9212753ddf --- /dev/null +++ b/research/p104-two-channel-support/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact root fixture/hash, independent rational Gram entries, all 3280 projective words and 5377560 independent pairs, complete support histogram, sharp rational witness, explicit hypothesis and receipt-rejection controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact root fixture/hash, independent rational Gram entries, all 3280 projective words and 5377560 independent pairs, complete support histogram, sharp rational witness, explicit hypothesis and receipt-rejection controls." + } + ] +} diff --git a/research/p104-two-channel-support/verify.py b/research/p104-two-channel-support/verify.py new file mode 100644 index 0000000000..1d036cb9b8 --- /dev/null +++ b/research/p104-two-channel-support/verify.py @@ -0,0 +1,197 @@ +#!/usr/bin/env python3 +"""Exact two-channel support certificate. Produced by Nick Petalas. Apache-2.0.""" +import argparse +from collections import Counter +from fractions import Fraction +import hashlib +from itertools import product +import json +from pathlib import Path + +CLIQUE = (1, 5, 18, 20, 80, 85, 100, 103) +WITNESS = ((0, 0, 0, 1, 0, 0, 0, 0), (0, 0, 0, 0, 1, 1, 1, 0)) +SOURCE_FILES = ("PORTS.json", "PROOF.md", "README.md", "SOURCES.json", + "TASK.json", "VERIFY.json", "verify.py") + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def reject(call, message): + try: + call() + except ValueError: + return + raise ValueError("control accepted: " + message) + + +def checked_ports(payload, expected_hash): + require(hashlib.sha256(payload).hexdigest() == expected_hash, "port source drift") + ports = json.loads(payload) + require(isinstance(ports, list) and len(ports) == 104, "port count") + require(all(type(q) is int and 0 < q < 512 for q in ports), "port range") + require(len(set(ports)) == 104, "duplicate ports") + require(all(q.bit_count() in (3, 7) for q in ports), "port type") + return ports + + +def inner(a, b): + """Integer root inner product in A8 coordinates, before dividing by two.""" + sa = {i for i in range(9) if a >> i & 1} + sb = {i for i in range(9) if b >> i & 1} + if len(sa) == 3 and len(sb) == 3: + return len(sa & sb) - 1 + if len(sa) == 3: + sa, sb = sb, sa + i, j = sorted(set(range(9)) - sa) + if len(sb) == 3: + return int(i in sb) - int(j in sb) + k, ell = sorted(set(range(9)) - sb) + return int(i == k) - int(i == ell) - int(j == k) + int(j == ell) + + +def root(q): + """Separate literal nine-coordinate rational root construction.""" + if q.bit_count() == 3: + return tuple(Fraction(2 if q >> i & 1 else -1, 3) for i in range(9)) + i, j = [i for i in range(9) if not (q >> i & 1)] + return tuple(Fraction(int(k == i) - int(k == j)) for k in range(9)) + + +def generators(ports): + roots = [root(q) for q in ports] + rational = [] + for t in CLIQUE: + row = [] + for q, vector in zip(ports, roots): + value = sum(a * b for a, b in zip(roots[t], vector)) / 2 + require(value == Fraction(inner(ports[t], q), 2), "Gram formula") + require(value.denominator in (1, 2), "non-dyadic Gram entry") + row.append(value) + rational.append(tuple(row)) + ternary = tuple(tuple(2 * inner(ports[t], q) % 3 for q in ports) for t in CLIQUE) + for i in range(8): + for j in range(8): + require(rational[i][CLIQUE[j]] == int(i == j), "systematic rational basis") + require(ternary[i][CLIQUE[j]] == int(i == j), "systematic ternary basis") + return tuple(rational), ternary + + +def canonical(vector): + require(len(vector) == 8 and all(x in (0, 1, 2) for x in vector), "coefficient shape") + lead = next((x for x in vector if x), None) + require(lead is not None, "zero projective vector") + return tuple(x * lead % 3 for x in vector) + + +def support(coefficients, columns, modulus=None): + result = 0 + for i, column in enumerate(columns): + value = sum(a * b for a, b in zip(coefficients, column)) + if modulus is not None: + value %= modulus + if value: + result |= 1 << i + return result + + +def plane_key(a, b): + plus = canonical(tuple((x + y) % 3 for x, y in zip(a, b))) + minus = canonical(tuple((x + 2 * y) % 3 for x, y in zip(a, b))) + points = tuple(sorted((a, b, plus, minus))) + require(len(set(points)) == 4, "dependent pair") + return points + + +def pair_census(coefficients, masks): + histogram = Counter() + minimum = 105 + minimizers = [] + for i in range(len(masks)): + for j in range(i): + weight = (masks[i] | masks[j]).bit_count() + histogram[weight] += 1 + if weight < minimum: + minimum = weight + minimizers = [(j, i)] + elif weight == minimum: + minimizers.append((j, i)) + planes = Counter(plane_key(coefficients[i], coefficients[j]) for i, j in minimizers) + require(all(count == 6 for count in planes.values()), "plane pair multiplicity") + require(sum(histogram.values()) == 5377560, "incomplete pair census") + require(minimum == 72, "second support weight") + return { + "projective_words": len(coefficients), "independent_projective_pairs": sum(histogram.values()), + "two_dimensional_subcodes": sum(histogram.values()) // 6, + "second_support_weight": minimum, "minimizing_pairs": len(minimizers), + "minimizing_subcodes": len(planes), + "pair_support_histogram": {str(k): v for k, v in sorted(histogram.items())}, + } + + +def checks(rational, ternary, ports, payload, port_hash): + coefficients = [c for c in product(range(3), repeat=8) if any(c) and canonical(c) == c] + require(len(coefficients) == 3280, "projective coverage") + columns = tuple(zip(*ternary)) + masks = [support(c, columns, 3) for c in coefficients] + require(all(mask for mask in masks), "noninjective coefficient map") + result = pair_census(coefficients, masks) + rational_columns = tuple(zip(*rational)) + q_masks = [support(c, rational_columns) for c in WITNESS] + f_masks = [support(c, columns, 3) for c in WITNESS] + require(q_masks[0] | q_masks[1] == f_masks[0] | f_masks[1], "witness lift support") + require((q_masks[0] | q_masks[1]).bit_count() == 72, "sharp rational witness") + require(WITNESS[0][3] * WITNESS[1][4] - WITNESS[0][4] * WITNESS[1][3] == 1, + "independent rational witness") + require(len(plane_key(*WITNESS)) == 4, "independent ternary witness") + require(support(tuple(2 * x % 3 for x in WITNESS[1]), columns, 3) == f_masks[1], + "projective scaling") + require(max(mask.bit_count() for mask in f_masks) < 72, "individual support is insufficient") + require(sum(mask.bit_count() for mask in f_masks) > 72, "support union is not a sum") + reject(lambda: canonical((0,) * 8), "zero projective word") + reject(lambda: plane_key(WITNESS[0], WITNESS[0]), "dependent pair") + reject(lambda: checked_ports(payload + b' ', port_hash), "changed source bytes") + result["witness"] = { + "coefficients": WITNESS, "rational_individual_weights": [x.bit_count() for x in q_masks], + "ternary_individual_weights": [x.bit_count() for x in f_masks], + "union_ports": [q for i, q in enumerate(ports) if (q_masks[0] | q_masks[1]) >> i & 1], + } + return result + + +def same_receipt(expected, actual): + require(expected == actual, "receipt differs from full recomputation") + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--emit-receipt", type=Path) + args = parser.parse_args() + package = Path(__file__).resolve().parent + metadata = json.loads((package / "SOURCES.json").read_text()) + external = metadata["external_sources"][0] + require(external["local_path"] == "PORTS.json", "coordinate fixture path") + payload = (package / "PORTS.json").read_bytes() + ports = checked_ports(payload, external["sha256"]) + rational, ternary = generators(ports) + result = checks(rational, ternary, ports, payload, external["sha256"]) + result["witness"]["coefficients"] = [list(c) for c in WITNESS] + result["source_hashes"] = {name: hashlib.sha256((package / name).read_bytes()).hexdigest() + for name in SOURCE_FILES} + result["claim_type"] = "finite certificate and scoped support/frame proof" + for value in (71, 73): + mutant = dict(result, second_support_weight=value) + reject(lambda: same_receipt(mutant, result), "changed second weight") + require(result["minimizing_subcodes"] == 704, "minimizer coverage") + if args.emit_receipt is not None: + args.emit_receipt.write_text(json.dumps(result, indent=2, sort_keys=True) + "\n") + else: + expected = json.loads((package / "RESULT.json").read_text()) + same_receipt(expected, result) + print("PASS_P104_TWO_CHANNEL_SUPPORT d2=72 pairs=5377560 minimizing_subcodes=704") + + +if __name__ == "__main__": + main()