Prove optimal raw-broadcast headers for every mate-pair count

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.

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.

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"
+    }
+  ]
+}