From 507b511e3e42e9bf0c804496f04c2d5eac39b963 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Tue, 27 Oct 2026 09:22:16 +0000 Subject: [PATCH] feat(research): classify optimal paired raw-broadcast headers --- .../paired-raw-header-classification/PROOF.md | 161 ++++++++++ .../README.md | 143 +++++++++ .../SOURCES.json | 36 +++ .../TASK.json | 113 +++++++ .../VERIFY.json | 38 +++ .../verify.py | 282 ++++++++++++++++++ 6 files changed, 773 insertions(+) create mode 100644 research/paired-raw-header-classification/PROOF.md create mode 100644 research/paired-raw-header-classification/README.md create mode 100644 research/paired-raw-header-classification/SOURCES.json create mode 100644 research/paired-raw-header-classification/TASK.json create mode 100644 research/paired-raw-header-classification/VERIFY.json create mode 100644 research/paired-raw-header-classification/verify.py diff --git a/research/paired-raw-header-classification/PROOF.md b/research/paired-raw-header-classification/PROOF.md new file mode 100644 index 0000000000..80795eecd7 --- /dev/null +++ b/research/paired-raw-header-classification/PROOF.md @@ -0,0 +1,161 @@ +# Optimal one-bit headers for paired raw broadcasts + +This scoped proof and its finite corroboration were produced by Nick Petalas. +Apache-2.0. Independent human and formal proof-kernel review are unclaimed. + +## Contract and result + +Let n >= 1. There are 2n independent uniform bits X_0,...,X_(2n-1). +Receiver i demands X_i and initially knows only X_(i xor 1). Sources and +receivers are distinct roles. A central encoder sends the mandatory one-bit +public header h(X), charged two units, even if h is constant. On branch r, +it broadcasts a fixed list of raw source bits, charged one per transmitted +bit. Every receiver receives the list and header. The list, its order and +its length depend only on r. All inputs must decode exactly. Arbitrary +nonlinear h and decoders are allowed. There are no other messages, private +metadata, relays or extra free side information. + +This is an abstract matching contract. Its n=5 instance uses the public-header +and singleton-broadcast tariffs of Jerry Chen's PR912 Hurwitz model. It +restricts that predecessor's arbitrary payload alphabet to raw broadcasts. +No geometry with arbitrarily many Hurwitz lines is asserted. + +Write P(h) for the set of pairs j such that + + h(x xor e_(2j)) = h(x) xor 1, + h(x xor e_(2j+1)) = h(x) xor 1 for every x. + +Equivalently, j belongs to P(h) exactly when + + h(x) = x_(2j) xor x_(2j+1) xor g(x outside pair j) + +for some Boolean function g. Let C_raw(h) be the least expected charge for +the fixed header h over all allowed branch-dependent raw lists. + +**Theorem.** For every n >= 1, + +1. C_raw(h) = 2n if and only if P(h) is nonempty. +2. If P(h) is empty, then C_raw(h) >= 2n+1. This one-unit separation is sharp. +3. Every cost-2n code broadcasts each source outside one complete pair exactly + once on each branch. The omitted pair on each branch belongs to P(h), + and the two branches can choose any two members of P(h) independently. + +List order does not affect decoding. Repetitions can be deleted, so first +work with the set S_r of transmitted source indices. A repeated bit can +never occur in an attaining code, since deleting it strictly lowers expected +charge on its nonempty branch. We count payload sets, not their permutations. + +## Fibre capacity + +Fix a nonempty header fibre F_r, a transmitted set S, and its omitted +indices U. Let a be the number of pairs with both bits omitted and b the +number with exactly one omitted bit. Thus k=a+b pairs are touched and + + |S| = 2n-2a-b. + +Fix the values of X_S. For a singly omitted bit, its receiver's mate is +already fixed, so the decoder permits at most one value for that bit. +For a doubly omitted pair, either bit determines the other through its +receiver's decoder, so at most two pair assignments occur. This conclusion +does not assume independence inside the fibre. Projecting the fibre into +the omitted pairs bounds its size by the product of these local capacities. +There are at most 2^|S| choices of X_S. Consequently + + |F_r| <= 2^(|S|+a) = 2^(2n-k), + p_r = Pr[h(X)=r] <= 2^(-k). (1) + +Also the number s=|U| of omitted bits obeys s=2a+b <= 2k. +For k=0 no bits are omitted. The bound applies to every zero-error branch, +including nonlinear decoders and arbitrary correlations caused by h. + +## Expected cost and equality + +First suppose h is unbalanced, including a constant h. Its larger fibre has +probability greater than 1/2. Equation (1) forces that branch to transmit all +2n source bits. If the smaller nonempty branch touches k>=1 pairs, its +expected saving in raw bits is at most + + p_small s_small <= 2k / 2^k <= 1. + +The last inequality follows from k <= 2^(k-1) for every positive integer k. +If the smaller fibre is empty, or touches no pair, its saving is zero. +Therefore every unbalanced-header code has expected cost at least 2n+1. + +Now suppose both fibres have probability 1/2. Equation (1) gives k<=1 on +each branch, so at most two raw bits can be omitted per branch. Expected +cost is at least 2n. If a branch omits both bits of a pair, take either +coordinate i of that pair. Two points x and x xor e_i cannot both belong +to F_r: their raw broadcasts and mate bits agree, while receiver i's demand +differs. The edges {x,x xor e_i} partition the whole cube into 2^(2n-1) +disjoint pairs. Since F_r has that exact size, it contains one point from +each edge. Thus h flips under coordinate i on the whole cube. Applying this +to both coordinates proves that the omitted pair belongs to P(h). + +If P(h) is empty, neither balanced branch can omit two bits. Each transmits +at least 2n-1 bits, and the cost is at least 2n+1. If cost is exactly 2n, +both branches must omit two bits, so they omit a full pair in P(h). + +Conversely choose j in P(h). Broadcast all 2n-2 bits outside j. Every +receiver outside j receives its demand directly. A receiver inside j +computes g from the broadcasts and recovers its demand as + + header xor g(broadcasts) xor its mate bit. + +This costs 2+(2n-2)=2n on every input. The same construction works if each +branch selects a different member of P(h). This proves all three claims. + +Sharpness of the one-unit separation follows for every n from h(X)=X_0. +Broadcast all bits except X_0. Receiver 0 uses the header; the others read +their raw demands. The cost is exactly 2n+1 and P(h) is empty. There is also +an unbalanced attaining example for every n>=2: let h be the OR of the first +two pair parities. On its probability-1/4 zero branch, omit all four bits +of those pairs. On its other branch transmit every bit. The expected raw +count is 2n-1, giving total 2n+1. Both cases are checked directly at n=3. + +## Closed-form classification count + +For each pair j, let A_j be the Boolean headers that flip in both coordinates +of j. If a specified set of k pairs has this property, the header is the +XOR of those k pair parities and an arbitrary Boolean function of the +remaining 2(n-k) bits. Hence that intersection has exactly + + 2^(2^(2(n-k))) + +headers. Inclusion-exclusion counts all optimal headers: + + N_n = sum_(k=1)^n (-1)^(k+1) binom(n,k) 2^(2^(2(n-k))). (2) + +The number with exactly k full parity pairs is + + E_(n,k) = binom(n,k) sum_(j=0)^(n-k) + (-1)^j binom(n-k,j) 2^(2^(2(n-k-j))). (3) + +For three pairs the new enumeration gives + + E_(3,1)=196518, E_(3,2)=42, E_(3,3)=2, + N_3=196562. + +It also enumerates all sum_k k^2 E_(3,k)=196704 optimal ordered pairs of +branch payload sets and decodes both omitted demands on every input. +The predecessor's two-pair result is cited rather than replayed. Formula (2) +specializes to its 30 headers, but our unrestricted-payload claim does not +extend beyond that predecessor's domain. For n>=3 the theorem here concerns +the stated raw-broadcast contract only. + +## Consequence and limits + +Allowing the raw payload set to depend on the header creates more optimal +protocols but no additional optimal headers. Every such header already has +an optimal code using the same omitted pair on both branches. To find more +optimal headers at three or more pairs, one must change the payload alphabet +or another stated contract hypothesis. This conclusion does not exclude +cheaper general nonlinear payloads or different physical realizations. + +The universal statement rests on the written proof. The finite verifier +corroborates the new three-pair domain with independently computed Boolean +derivatives, literal decoders and exhaustive raw-subset oracles on a declared +sample of headers. It does not enumerate all 2^64 three-pair Boolean headers. +No integer multiplication theorem, new kappa, physical supplier, all-size +compiler, native operator, ownership, precision/tape or analytic admission +is proved. Classical fibre counting and inclusion-exclusion retain their +mathematical credit. diff --git a/research/paired-raw-header-classification/README.md b/research/paired-raw-header-classification/README.md new file mode 100644 index 0000000000..a64a32a80b --- /dev/null +++ b/research/paired-raw-header-classification/README.md @@ -0,0 +1,143 @@ +# Exact optimal headers for paired raw broadcasts + +This contribution was produced by Nick Petalas. Apache-2.0. + +**Scoped proof with finite corroboration.** For any n independent uniform +mate pairs, a mandatory one-bit public header of price two and branch-dependent +raw source broadcasts of price one attain expected charge 2n exactly when + +```text +h = one complete pair's parity XOR any Boolean function of the other bits. +``` + +Every other header costs at least 2n+1 in this contract. The one-unit gap is +sharp. Every optimal branch omits one complete pair and broadcasts all other +sources once. Allowing the omitted pair to depend on the header creates more +optimal protocols but no additional optimal headers. + +The new all-n classification has the closed-form count + +```text +N_n = sum_(k=1)^n (-1)^(k+1) binom(n,k) 2^(2^(2(n-k))). +``` + +For three pairs, the verifier enumerates **196,562** distinct optimal headers +and **196,704** ordered choices of the two branch payload sets. It performs +**25,178,112** literal decodes of omitted demands. Exactly 196,518 headers +have one full parity pair, 42 have two, and two have three. + +Jerry Chen's merged [#912](https://github.com/CrocSwap/integer-mult-bounds/pull/912) +establishes the two-pair classification with arbitrary allowed payloads. +Here the number of pairs increases while the payload alphabet is restricted +to raw broadcasts. Its original census and predecessor geometry are cited, +not audited or replayed. General nonlinear payload optimality at n>=3 is +unclaimed. The n=5 instance uses the original ten-port Hurwitz tariffs; for +other n the theorem concerns the explicitly stated abstract matching model. + +## Proof and evidence + +[PROOF.md](PROOF.md) proves that a branch omitting bits from k mate pairs +contains at most a 2^-k fraction of all inputs. A balanced optimal branch +must omit both bits of one pair. Saturation forces the header to flip under +each coordinate of that pair. Inclusion-exclusion then counts the class. +The written argument applies to every n>=1. Finite checks corroborate it. + +The new verifier imports and executes no predecessor implementation. It: + +- Enumerates all three-pair templates in Gray order, independently computes + their full-pair Boolean derivatives and checks the exact intersection counts. +- Decodes both omitted demands for every optimal ordered branch-payload choice + and every six-bit input. The other four demands are directly broadcast. +- Exhausts both branches and all 64 raw subsets on 386 declared headers, + including all 128 affine headers, 256 reproducible additional tables and + two explicit nonlinear tables. These 49,408 subset checks find 1,879 feasible + branch subsets. They independently compute minimum charges and check the + fibre bound, the attaining class and the one-unit gap. +- Rejects five invalid protocols and four invalid dimension arguments. It + checks balanced and unbalanced sharp-gap witnesses and demonstrates why + pricing the same valid header at one would defeat the stated floor. + +The finite oracle sample contains 75 optimal and 311 other headers. It is not +an enumeration of all 2^64 Boolean headers on three pairs. Exclusion of that +entire complement is the written theorem. The sorted new header/pair-mask +record has SHA256 +`0cd84486e9ad2f78b21d1816832353ae35ced2c0b92bf6d3efda8b2609cdee49`. +Checks compare counts, actual derivatives and literal decodes rather than +this digest alone. + +## Reproduce + +From the repository root, CPython 3.12 and the standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/paired-raw-header-classification +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/paired-raw-header-classification/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/paired-raw-header-classification/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/paired-raw-header-classification --check-source-history +``` + +Substitute another CPython 3.12 executable on another machine. The direct +marker is `PASS_PAIRED_RAW_HEADER_CLASSIFICATION`. Normal runs write nothing. +An optional `--receipt /absolute/new/path.json` produces a fresh receipt bound +to every package file and the three declared predecessor documentation inputs. +The destination must be outside the checkout and must not already exist. +All mathematical checks remain active under optimized Python. + +## Scope and verification design + +One-bit sources, independent uniform inputs, mate-only free side information, +zero error, a mandatory public one-bit header of price two, and raw broadcasts +of price one are hypotheses. All receivers get every payload. Payload order, +length and source selection depend only on that header. Header preparation, +physical copying, decoding, source access, storage and cleanup are unpriced. +This is an optimistic abstract interface result, not a physical saving. + +The code has no recursion, subprocesses, dynamic imports or external libraries. +Its enumeration fixes three pairs, at most 3*65,536 generated records, 64 inputs +and 386 oracle tables. Supporting dimension arguments are limited to 1..5; +the universal theorem is not inferred from that executable limit. All functions +fit within 60 lines. Source inputs and receipt files have explicit size bounds. +Boundary errors raise exceptions. Warning-strict normal and optimized replay +provide interpreted-code diagnostics; no separate static type checker is +required by this package. + +Power-of-Ten rule 3 has a managed-runtime deviation. Python dictionaries and +integers allocate while checking. The record count and integer widths are +bounded, the oracle processes one header at a time, and file reads are limited +to one MiB each. Fixed-capacity allocation would require a different +implementation language. Registered replay checks these limits; any future +larger enumerator must revisit them before expansion. + +No selected cold replay, native/all-size compiler, owned-erasure, +precision/tape or analytic-recovery proof is run or discharged. No new kappa, +supplier admission or complete multiplication theorem is claimed. Independent +human and formal proof-kernel review are unclaimed. + +## Open next questions + +- Can three-pair headers outside this class attain cost six with general + nonlinear payloads under the original pairing-rank tariff? First try a + balanced conditional choice between two pair parities and charge each + nonlinear payload's complete source/reader span. The raw-broadcast theorem + gives no answer for that enlarged alphabet. +- For a public header with two or more bits, characterize the headers that + attain the matching copy floor with branch-dependent raw broadcasts. First + analyze three pairs and four equal-size fibres. The binary-fibre saturation + argument used here does not directly cover four branches. + +## Credit and provenance + +Credit Jerry Chen / CubeJerry #912 for the paid adaptive-header model, its +two-pair result and the explicit raw-bit witnesses. Alexander Templeton #785 +supplies the nonlinear transcript framework, following Douglas R. Colkitt +#703 and Joel Pulikkan / GamingPuzzled #620 for the Hurwitz geometry, pairing +tariff and copy floor. DreamingOfClouds #446/#595/#717 retain their separate +format-accounting credit. Classical fibre counting and inclusion-exclusion +are used without a literature-priority claim. + +[SOURCES.json](SOURCES.json) pins the unchanged #912 README, proof and notice +at canonical main `de5ec2e7a6074068452f45b1a191b5c72832df4a`. The original +notice and every predecessor credit line remain unchanged. The new step is +the all-n raw-broadcast classification, exact three-pair count, sharp gap +and full description of optimal branch payload sets. The selected record, +shared code, upstream sources and frozen evidence remain unchanged. diff --git a/research/paired-raw-header-classification/SOURCES.json b/research/paired-raw-header-classification/SOURCES.json new file mode 100644 index 0000000000..5fa81301d8 --- /dev/null +++ b/research/paired-raw-header-classification/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8", + "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/hurwitz-adaptive-routing/NOTICE.md", + "usage": "input", + "git_blob": "3e5eb2d7e8b842d58d6fc9e107cfdafd8aef6b25", + "sha256": "b34c1aacb8cec1c9b235426e4f48b1f40da6f8c2dce91715d7c813516dcd0e8e" + }, + { + "path": "research/hurwitz-adaptive-routing/PROOF.md", + "usage": "input", + "git_blob": "915a91663e8ae2eb96a2c248224a40ec052e6fda", + "sha256": "612d1723fd855503384943217b78f18a80adaca074196aa677b7124845d9e4d1" + }, + { + "path": "research/hurwitz-adaptive-routing/README.md", + "usage": "input", + "git_blob": "5be90a8b72e0f4dd79b1c94dadf63432707409e4", + "sha256": "f1d52e60d3f9010565073ac0fc362e1b0f0fc83e7bf77ed838abb659e59323db" + } + ] +} diff --git a/research/paired-raw-header-classification/TASK.json b/research/paired-raw-header-classification/TASK.json new file mode 100644 index 0000000000..7832abaaf8 --- /dev/null +++ b/research/paired-raw-header-classification/TASK.json @@ -0,0 +1,113 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 8, + "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a", + "original_card": { + "id": "formal-interface-lemma", + "question": "Can one uncovered interface implication be formalized with exact caller and certificate bindings?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/gate-operand-parity-lean/README.md", + "research/staged544-certified-endpoint/README.md", + "research/unconditional-batched-crt/README.md" + ], + "methods": [ + "Formalize a missing boundary lemma identified by the selected review.", + "Audit a formal theorem-to-certificate binding independently." + ], + "acceptance_gate": "State the exact formalized proposition and remaining assumptions; avoid duplicate arithmetic formalizations already present.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.", + "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse." + }, + "first_experiment": "Write one missing statement with quantified hypotheses, actual caller and existing coverage. A compact-switch lemma is a candidate only after its mathematical contract is reviewed. Establish a bounded proof plan before a separately budgeted proof-assistant build; do not rerun large Lean jobs as orientation.", + "bottleneck_link": "A missing interface proof can reduce the conditional gap even if it does not change kappa.", + "allowed_variations": [ + "Narrow to one formal lemma or one theorem-to-certificate binding." + ], + "scope_change_triggers": [ + "Formalizing already-covered arithmetic and claiming the full multiplication theorem." + ], + "overlap_terms": [ + "hyperplane end", + "formal interface", + "Lean binding", + "3807", + "3857", + "4100", + "gate-operand-parity-lean", + "staged544-certified-endpoint", + "unconditional-batched-crt" + ], + "existing_checks": [ + { + "scope": "PR #3807: scoped gate-operand parity formalization.", + "evidence": "research/gate-operand-parity-lean/README.md", + "remaining": "Exact theorem-to-caller binding and genuinely uncovered interface lemmas.", + "status": "author-checked", + "source_commit": "4c3530f42a6abcc48e7a6bcffd6c901911dc8269", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #3857: certified real-power moment/endpoint arithmetic.", + "evidence": "research/staged544-certified-endpoint/README.md", + "remaining": "Uniform algorithmic implications, not another endpoint digit.", + "status": "author-checked", + "source_commit": "ef4315b8caa605e47a2515004845eb2d2ed71a86", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4100: compact-switch formalization proposed as future validation.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Audit the statement and assumptions before a formal proof campaign.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Classify every optimal one-bit public header for branch-dependent raw broadcasts on n independent uniform mate pairs; prove a sharp one-unit gap and closed-form counts.", + "scope_change_reason": "This is an abstract decoder-interface side theorem extending Jerry Chen PR912 beyond two pairs under the explicitly narrower raw-broadcast alphabet. It is a written proof, not a proof-assistant formalization or selected-caller admission.", + "bottleneck_link": "Determines whether changing only raw payload selection can enlarge the optimal paid-header class. It cannot, so a broader search must change payload functions or the stated contract.", + "budget_minutes": 60, + "stop_rule": "Stop at the first proved new classification and completed three-pair corroboration; do not extend the payload alphabet.", + "outcome": "completed", + "evidence": "PROOF.md; verify.py enumerates 196562 headers and 196704 optimal branch-payload choices, with 25178112 literal decodes, 49408 independent raw-subset checks and semantic controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can a three-pair header outside the class attain cost six with general nonlinear payloads?", + "why_it_matters": "Would separate the original pairing-rank payload model from raw broadcasts.", + "first_step": "Test a balanced conditional choice between two pair parities and charge every payload source/reader span.", + "blocked_by": "No matching nonlinear delivery protocol or exclusion proof is supplied." + }, + { + "question": "Which wider public headers attain the floor with raw broadcasts?", + "why_it_matters": "Tests whether multi-branch conditioning escapes the one-bit classification.", + "first_step": "Analyze three pairs and four equal-size fibres with header price four.", + "blocked_by": "The two-fibre saturation proof does not directly cover four branches." + } + ], + "coordination": { + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19213579", + "upstream_checked": "de5ec2e7a6074068452f45b1a191b5c72832df4a", + "priority_revision": 8, + "checked_at_utc": "2026-10-27T09:10:00Z", + "coverage": "Live snapshot: 405 open PRs, 5293 Discussion records; all-main targeted README grep and merged PR searches. Sparse local-note inventory and unpublished work remain coverage limits." + }, + "environment": { + "python": "CPython 3.12.15", + "dependencies": "standard library only", + "playbook": "engineering-mode investigation" + } +} diff --git a/research/paired-raw-header-classification/VERIFY.json b/research/paired-raw-header-classification/VERIFY.json new file mode 100644 index 0000000000..57a1bb5785 --- /dev/null +++ b/research/paired-raw-header-classification/VERIFY.json @@ -0,0 +1,38 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/hurwitz-adaptive-routing/NOTICE.md", + "research/hurwitz-adaptive-routing/PROOF.md", + "research/hurwitz-adaptive-routing/README.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Complete new three-pair header/protocol enumeration, Boolean derivatives, literal decoders, independent raw-subset minima, sharp gap and invalid-protocol controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Repeat all mathematical and boundary checks under optimized Python with explicit checks enabled." + } + ] +} diff --git a/research/paired-raw-header-classification/verify.py b/research/paired-raw-header-classification/verify.py new file mode 100644 index 0000000000..6a04683e8e --- /dev/null +++ b/research/paired-raw-header-classification/verify.py @@ -0,0 +1,282 @@ +#!/usr/bin/env python3 +"""Exact corroboration of the paired raw-broadcast header theorem. + +No predecessor implementation is imported or executed. Normal execution is +read-only. The optional receipt is generated outside the repository. +""" + +import argparse +import hashlib +import json +from math import comb +from pathlib import Path +import sys +import time + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def dimensions(n): + require(type(n) is int and 1 <= n <= 5, "pair count must be in 1..5") + return 2 * n, 1 << (2 * n) + + +def full_pair_counts(n): + """Inclusion-exclusion by the exact number of full parity pairs.""" + dimensions(n) + return { + k: comb(n, k) * sum( + (-1) ** j * comb(n - k, j) * (1 << (1 << (2 * (n - k - j)))) + for j in range(n - k + 1) + ) + for k in range(1, n + 1) + } + + +def template_data(n, pair): + bits, size = dimensions(n) + require(type(pair) is int and 0 <= pair < n, "invalid pair") + raw = tuple(i for i in range(bits) if i // 2 != pair) + columns = [0] * (1 << len(raw)) + parity = 0 + for x in range(size): + index = sum(((x >> bit) & 1) << j for j, bit in enumerate(raw)) + columns[index] |= 1 << x + parity |= (((x >> (2 * pair)) ^ (x >> (2 * pair + 1))) & 1) << x + require(sum(c.bit_count() for c in columns) == size, "template partition") + return parity, tuple(columns) + + +def generate_three_pair_headers(): + """Enumerate each pair family in Gray order, retaining its union.""" + headers = {} + for pair in range(3): + current, columns = template_data(3, pair) + for step in range(1 << len(columns)): + if step: + changed = (step & -step).bit_length() - 1 + current ^= columns[changed] + headers[current] = headers.get(current, 0) | (1 << pair) + require(len(headers) <= 3 * 65536, "header capacity") + return headers + + +def parity_pairs(n, header): + """Test literal Boolean derivatives, without using template labels.""" + _, size = dimensions(n) + require(type(header) is int and 0 <= header < (1 << size), "invalid table") + result = 0 + universe = (1 << size) - 1 + for pair in range(n): + good = True + for bit in (2 * pair, 2 * pair + 1): + distance = 1 << bit + low = sum(1 << x for x in range(size) if not x & distance) + flipped = ((header & low) << distance) | ((header >> distance) & low) + good = good and (header ^ flipped == universe) + if good: + result |= 1 << pair + require(result < (1 << n), "pair-mask range") + return result + + +def literal_decoder_check(header, first_pair, second_pair): + """Actually decode the two omitted demands on every three-pair input.""" + comparisons = 0 + for x in range(64): + r = (header >> x) & 1 + pair = (first_pair, second_pair)[r] + a, b = 2 * pair, 2 * pair + 1 + raw_value = x & ~(3 << a) + g_value = (header >> raw_value) & 1 + for bit, mate in ((a, b), (b, a)): + decoded = r ^ g_value ^ ((x >> mate) & 1) + require(decoded == ((x >> bit) & 1), "literal decoder conflict") + comparisons += 1 + return comparisons + + +def enumerate_new_domain(): + headers = generate_three_pair_headers() + histogram = {1: 0, 2: 0, 3: 0} + digest = hashlib.sha256() + protocols = comparisons = 0 + for header, declared in sorted(headers.items()): + actual = parity_pairs(3, header) + require(actual == declared, "family versus Boolean-derivative mismatch") + histogram[actual.bit_count()] += 1 + digest.update(header.to_bytes(8, "little") + bytes([actual])) + choices = tuple(j for j in range(3) if actual & (1 << j)) + for first in choices: + for second in choices: + comparisons += literal_decoder_check(header, first, second) + protocols += 1 + require(histogram == {1: 196518, 2: 42, 3: 2}, "three-pair histogram") + require(histogram == full_pair_counts(3), "closed-form count mismatch") + require(protocols == 196704, "optimal payload-set protocol count") + return {"headers": len(headers), "exact_pair_histogram": histogram, + "payload_set_protocols": protocols, "omitted_demand_decodes": comparisons, + "sorted_header_pair_sha256": digest.hexdigest()} + + +def feasible_raw_payload(fibre, raw, bits): + """Independent zero-error oracle using each receiver's observation table.""" + for bit in range(bits): + observed = {} + for x in fibre: + key = (x & raw, (x >> (bit ^ 1)) & 1) + wanted = (x >> bit) & 1 + if key in observed and observed[key] != wanted: + return False + observed[key] = wanted + return True + + +def oracle_header(header): + """Exhaust every raw subset separately on both header branches.""" + minima = [] + sizes = [] + feasible = 0 + for r in (0, 1): + fibre = tuple(x for x in range(64) if (header >> x) & 1 == r) + best = 6 + for raw in range(64): + if feasible_raw_payload(fibre, raw, 6): + touched = sum((raw & (3 << (2 * j))) != (3 << (2 * j)) + for j in range(3)) + require(len(fibre) <= 1 << (6 - touched), "fibre capacity bound") + best = min(best, raw.bit_count()) + feasible += 1 + minima.append(best) + sizes.append(len(fibre)) + numerator = 2 * 64 + sum(a * b for a, b in zip(minima, sizes)) + return numerator, feasible + + +def sample_headers(): + headers = set() + for coefficients in range(64): + for constant in (0, 1): + headers.add(sum((((x & coefficients).bit_count() & 1) ^ constant) << x + for x in range(64))) + require(len(headers) == 128, "affine sample capacity") + state = 0xD1B54A32D192ED03 + for _ in range(256): + state = (6364136223846793005 * state + 1442695040888963407) % (1 << 64) + headers.add(state) + headers.add(sum(((((x >> 0) ^ (x >> 1)) & 1) + | (((x >> 2) ^ (x >> 3)) & 1)) << x for x in range(64))) + headers.add(sum((((x ^ (x >> 1)) & 1) + ^ (((x >> 2) & (x >> 3) & (x >> 4)) & 1)) << x + for x in range(64))) + require(len(headers) <= 386, "oracle sample capacity") + return tuple(sorted(headers)) + + +def check_oracles(): + headers = sample_headers() + optimal = nonoptimal = feasible = 0 + for header in headers: + numerator, count = oracle_header(header) + feasible += count + if parity_pairs(3, header): + require(numerator == 6 * 64, "optimal-header cost") + optimal += 1 + else: + require(numerator >= 7 * 64, "nonclass header one-unit gap") + nonoptimal += 1 + coordinate = sum(((x >> 0) & 1) << x for x in range(64)) + unbalanced = sum(((((x ^ (x >> 1)) & 1) + | (((x >> 2) ^ (x >> 3)) & 1))) << x for x in range(64)) + require(oracle_header(coordinate)[0] == 7 * 64, "balanced sharp gap") + require(oracle_header(unbalanced)[0] == 7 * 64, "unbalanced sharp gap") + return {"headers": len(headers), "raw_subsets_examined": 128 * len(headers), + "feasible_branch_subsets": feasible, "optimal_headers": optimal, + "nonclass_headers": nonoptimal, "sharp_gap": 1} + + +def check_controls(): + parity = sum(((x ^ (x >> 1)) & 1) << x for x in range(64)) + zero = tuple(x for x in range(64) if not (parity >> x) & 1) + one = tuple(x for x in range(64) if (parity >> x) & 1) + require(feasible_raw_payload(zero, 60, 6), "positive branch zero") + require(feasible_raw_payload(one, 60, 6), "positive branch one") + require(not feasible_raw_payload(tuple(range(64)), 60, 6), "constant header") + require(not feasible_raw_payload(zero, 56, 6), "missing third payload bit") + damaged = parity ^ 1 + bad_fibre = tuple(x for x in range(64) if (damaged >> x) & 1) + require(not feasible_raw_payload(bad_fibre, 60, 6), "damaged truth table") + require(not feasible_raw_payload(zero, 51, 6), "wrong omitted pair") + require(not feasible_raw_payload(zero, 54, 6), "two different pairs omitted") + underpriced_charge = 1 + (60).bit_count() + require(underpriced_charge < 6, "underpriced-header boundary") + invalid = (0, 6, True, 1.5) + for n in invalid: + try: + dimensions(n) + except ValueError: + continue + raise ValueError("invalid dimension accepted") + return {"semantic_rejections": 5, "invalid_dimensions": len(invalid), + "underpriced_header_counterexample_cost": underpriced_charge} + + +def authenticate_sources(package): + manifest = json.loads((package / "SOURCES.json").read_text()) + root = package.parent.parent + rows = manifest["files"] + require(len(rows) <= 16, "source row bound") + checked = {} + for row in rows: + if row.get("usage") == "input": + path = root / row["path"] + require(path.is_file() and path.stat().st_size <= 1048576, "source size") + digest = hashlib.sha256(path.read_bytes()).hexdigest() + require(digest == row["sha256"], "source hash: " + row["path"]) + checked[row["path"]] = digest + require(len(checked) == 3, "source input count") + return checked + + +def write_receipt(path, package, result): + require(path.expanduser().is_absolute(), "receipt path must be absolute") + destination = path.expanduser().resolve() + root = package.parent.parent + require(destination.is_absolute() and not destination.is_relative_to(root), + "receipt must be outside the repository") + files = tuple(sorted(package.iterdir())) + require(len(files) <= 16, "package file bound") + hashes = {} + for file in files: + require(file.is_file() and file.stat().st_size <= 1048576, "package file size") + hashes[file.name] = hashlib.sha256(file.read_bytes()).hexdigest() + payload = {"result": result, "package_sha256": hashes} + serialized = json.dumps(payload, sort_keys=True, indent=2) + "\n" + with destination.open("x") as output: + require(output.write(serialized) == len(serialized), "incomplete receipt write") + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--receipt", type=Path) + args = parser.parse_args() + package = Path(__file__).resolve().parent + sources = authenticate_sources(package) + start = time.monotonic() + result = {"claim_type": "scoped proof with finite corroboration", + "three_pair_enumeration": enumerate_new_domain(), + "independent_raw_subset_oracles": check_oracles(), + "controls": check_controls(), "source_sha256": sources, + "python": sys.version.split()[0]} + result["elapsed_seconds"] = round(time.monotonic() - start, 6) + if args.receipt: + write_receipt(args.receipt, package, result) + print(json.dumps(result, sort_keys=True)) + print("PASS_PAIRED_RAW_HEADER_CLASSIFICATION") + + +if __name__ == "__main__": + main()