Certify sharp nonlinear five-cycle recovery probabilities (no κ)

research/nonlinear-cycle-success/PROOF.md

@@ -0,0 +1,182 @@
+# Sharp nonlinear partial recovery on the binary five-cycle
+
+This contribution was produced by Nick Petalas. Claim type: a finite
+certificate with a scoped combinatorial proof. The finite enumeration is
+part of the evidence, rather than a formal proof-kernel certificate.
+
+## Contract
+
+There are five independent uniform bits x_0,...,x_4. An encoder sees the
+entire input and emits one value in a set of size at most M. Receiver i
+sees that value and the two original bits x_(i-1), x_(i+1), with indices
+modulo five, and must output x_i. All five answers must be correct for
+the input to count as successful. The encoder and the receiver functions
+are arbitrary deterministic functions. Let F(M) be the maximum number of
+successful inputs among the 32 possible inputs.
+
+The exact result is
+
+| M | 1 | 2 | 3 | 4 | 5 | 6 | 7 | >=8 |
+|---|---|---|---|---|---|---|---|---|
+| F(M) | 5 | 10 | 15 | 20 | 24 | 28 | 31 | 32 |
+
+Thus two fixed broadcast bits have sharp joint success probability 5/8.
+Seven message values can succeed on exactly 31/32 of uniform inputs, but
+eight values are necessary for zero error. These are message-alphabet
+counts, not recursive-child ranks or physical costs.
+
+## Reduction to disjoint correct classes
+
+Identify an input x with the integer sum_i 2^i*x_i. Two inputs x,y are
+confusable if some receiver has the same two observed neighbors on both
+inputs but a different demanded bit. Equivalently, x xor y has a one at
+some position whose two cyclic neighbors are zero.
+
+The successful inputs assigned to one message must be pairwise
+nonconfusable. Conversely, every pairwise nonconfusable class has
+consistent receiver lookup tables: each neighbor pair determines at most
+one demanded bit within the class. Complete every unused table entry by
+zero. Disjoint such classes therefore give a protocol correct on their
+union. Map inputs outside that union to message zero. Any additional
+successes only increase the achieved count.
+
+It follows that F(M) is exactly the maximum union size of at most M
+disjoint nonconfusable classes. In the forward direction, discard the
+unsuccessful inputs from each encoder fiber. This step is needed because
+an encoder fiber need not itself be correct everywhere.
+
+## Complete finite premises
+
+The two supplied enumerations establish the following exact premises.
+
+1. The numbers of nonconfusable classes of sizes 0 through 6 are
+   (1,32,256,640,480,32,0). In particular every correct class has size at
+   most five: a larger class would contain a six-element class.
+2. At most four size-five classes can be disjoint. There are exactly
+   1,600 unordered disjoint four-packs. Their 20-element unions are
+   distinct.
+3. For each of those four-packs, its 12-element complement cannot be
+   partitioned into three nonconfusable four-element classes.
+
+The primary enumeration tests every subset of sizes 1 through 6 using
+the explicit confusability predicate. It visits 3,249 partial packings
+of size-five classes, including the empty packing, and extends every
+one in increasing class-index order. There are no five-packs. For every
+four-pack it lists all four-classes in the complement. Across all
+complements, it tests exactly 25,280 unordered candidate pairs. Whenever
+the pair is disjoint, the remaining four inputs are not a valid class.
+
+The separate enumeration starts with unassigned receiver truth tables.
+For each input it imposes five context/output assignments. It extends a
+class precisely when these assignments remain consistent, without using
+the XOR confusability predicate. It obtains the same full inventory,
+not merely the same counts. Both canonical inventory digests are
+`a39ed8349b302d38efbdacb422c394044ec1c2042364c21f4d01ddda1a555c73`.
+It separately checks every four- and five-tuple of size-five classes.
+For the last premise it constructs the 69,780 distinct unions of two
+disjoint four-classes, then checks whether any complement minus one
+four-class is in that union set. No such match occurs.
+
+These are exhaustive finite premises about a 32-input problem. No
+predecessor scientific verifier, floating-point acceptance, optimization
+solver or external dependency is part of the submitted replay.
+
+## Upper bounds
+
+For M<=4, premise 1 gives F(M)<=5M.
+
+For M=5 or 6, at most four classes can have size five. All remaining
+classes have size at most four. Therefore F(M)<=20+4(M-4)=4M+4.
+
+For M=7, suppose every input succeeds. Fewer than seven nonempty
+classes would cover at most 28 inputs by the previous bound. With seven
+classes, at most four can have size five; covering 32 inputs forces
+exactly four size-five classes and three size-four classes. Premise 3
+excludes precisely that case. Hence F(7)<=31. Finally F(M)<=32 always.
+
+## Attainment
+
+The literal classes are in verify.py and in its generated receipt. For
+M=1,...,4, take the first M classes in this list:
+
+```
+0 3 12 27 29
+1 2 13 26 28
+4 7 8 25 31
+5 6 9 24 30
+```
+
+For M=5, the following disjoint classes have total size 24:
+
+```
+7 11 22 24
+0 12 15 17 23
+2 4 21 25 26
+5 9 10 18 20
+8 14 16 19 31
+```
+
+For M=6, the following have total size 28:
+
+```
+2 12 17 31
+3 13 18 30
+1 7 22 25 26
+4 8 11 19 21
+5 6 10 27 29
+9 15 20 23 24
+```
+
+For M=7, the following have total size 31:
+
+```
+1 25 30
+3 13 20 26
+9 14 18 21
+0 12 15 17 23
+2 4 19 28 31
+5 6 10 27 29
+7 8 11 16 22
+```
+
+The verifier constructs every receiver lookup table and executes it on
+all 32 inputs, including inputs outside these listed classes. The exact
+observed success counts equal the upper bounds. For M=8 use the usual
+three-bit message (x_0 xor x_1, x_2 xor x_3, x_4), which every receiver
+can decode with its two neighbors. For larger M, ignore additional
+message values.
+
+## Randomness and scope
+
+Independent public or private random seeds cannot improve the optimum
+joint success probability on uniform inputs. Condition on all random
+seeds of the encoder and every decoder. Each resulting deterministic
+protocol satisfies the bound, so averaging preserves it. Input-correlated
+side information is outside this argument.
+
+The theorem allows arbitrary nonlinear encoding but fixes one
+simultaneous broadcast, the five original neighbor observations, five
+unit binary payloads, and joint rather than per-receiver success. It
+does not compose the curve across calls, tensor powers or adaptive
+observations. It supplies no legal physical realization, restoration,
+frame, stock, precision, tape, compiler or outer recovery result.
+
+## Prior work and credit
+
+ywz65's PR2541 supplies the arbitrary-block linear paired-plane interface
+and its C5 obstruction. Tekalign's PR3362 and JoyboyBrian's PR5023 give
+the exact unequal-width linear query capacities. These are cited context;
+their constructions and numerical claims are not replayed here. Nick
+Petalas's PR5873 classifies exact binary linear fits at total payload
+seven and is not the source of this changed nonlinear partial-recovery
+question. Credit the retained Sagar Thakrar, Cinna Davis, Adam Gall and
+P112/query-mask lineage in those packages.
+
+Confusion graphs, binary five-cycle maximum guessing fixed-set size five and the
+zero-error eight-message endpoint are classical. See Ross Atkins, Puck
+Rombach and Fiona Skerman, [Guessing numbers of odd cycles](https://www.combinatorics.org/ojs/index.php/eljc/article/view/v24i1p45),
+and Lawrence Ong, [Optimal finite-length and asymptotic index codes for
+five or fewer receivers](https://arxiv.org/abs/1606.05982). No priority
+for those facts or for the general method is claimed. The contribution
+here is the complete partial-success curve, its explicit attainers and
+the standalone finite obstruction certificate in this repository.

research/nonlinear-cycle-success/README.md

@@ -0,0 +1,144 @@
+# Exact nonlinear recovery with a limited binary-cycle message
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+Claim type: finite certificate with a scoped combinatorial proof.
+Independent human and formal proof-kernel review are unclaimed.
+
+Five receivers each demand one independent uniform bit and observe the
+two original neighboring bits on a five-cycle. One encoder sees all five
+bits and broadcasts one of at most M message values. Arbitrary nonlinear
+encoders and decoders have the following sharp joint-success counts:
+
+| Message values M | 1 | 2 | 3 | 4 | 5 | 6 | 7 | >=8 |
+|---|---|---|---|---|---|---|---|---|
+| Successful inputs out of 32 | 5 | 10 | 15 | 20 | 24 | 28 | 31 | 32 |
+
+In particular, two fixed message bits have exact optimal success
+probability 5/8. A seven-value message can fail on just one input, but
+cannot recover all inputs. Independent public or private randomness
+does not improve these uniform-input joint-success probabilities.
+
+[PROOF.md](PROOF.md) reduces the problem to disjoint correct message
+classes, proves the upper bounds from complete finite premises and
+lists attaining classes. The verifier constructs literal encoders and
+all receiver lookup tables, then executes them on every input.
+
+## What this adds
+
+ywz65's [PR2541](https://github.com/CrocSwap/integer-mult-bounds/pull/2541)
+uses C5 to obstruct a linear paired-plane query interface. Tekalign's
+[PR3362](https://github.com/CrocSwap/integer-mult-bounds/pull/3362) and
+JoyboyBrian's [PR5023](https://github.com/CrocSwap/integer-mult-bounds/pull/5023)
+give exact unequal-width linear query capacities. Their results are
+cited context, not replay or audit targets.
+
+The new step changes both linearity and complete recovery: it computes
+the entire finite partial-success curve under arbitrary nonlinear
+encoding. Nick Petalas's PR5873 concerns exact linear fits with total
+payload seven; this result neither extends its orbit classification
+nor changes only its payload widths. The five bits here have unit width.
+
+Confusion graphs, the binary five-cycle maximum guessing fixed-set size five, and the
+zero-error eight-message endpoint are classical. The proof cites Atkins,
+Rombach and Skerman and Ong for that context. No literature priority for
+those endpoints or methods is claimed. New credit is for this complete
+partial-success table, its attainers and its repository certificate.
+The retained Sagar Thakrar, Cinna Davis, Adam Gall and P112/query-mask
+lineage remains credited in the predecessor packages.
+
+## Evidence and reproduction
+
+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/nonlinear-cycle-success/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/nonlinear-cycle-success/independent.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/nonlinear-cycle-success
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/nonlinear-cycle-success --check-source-history
+```
+
+Local CPython 3.12.15 normal/optimized primary checks took 1.043/0.977
+seconds; the separate checks took 0.051/0.050 seconds. All passed.
+These are check durations, not a performance improvement claim.
+
+A reviewer may substitute their CPython 3.12 executable. VERIFY.json
+registers both normal and optimized warning-strict runs of both checks.
+Expected markers are PASS_NONLINEAR_CYCLE_SUCCESS,
+PASS_NONLINEAR_CYCLE_TRUTH_TABLES and PASS_REGISTERED_RESEARCH_PACKAGE.
+
+The complete nonconfusable class inventory has sizes
+(1,32,256,640,480,32,0) for class sizes 0 through 6. The primary search
+visits 3,249 size-five partial packings, obtains all 1,600 four-packs and
+tests 25,280 complementary four-class pairs. Its separate truth-table
+implementation obtains the same full inventory and uses a different
+pair-union obstruction. All eight attaining protocols execute on all
+32 inputs; eight malformed-witness/decoder controls reject.
+
+The inventory digest is
+`a39ed8349b302d38efbdacb422c394044ec1c2042364c21f4d01ddda1a555c73`.
+The primary command generates a receipt bound to all seven package
+files and all three cited live inputs. It writes nothing. Redirect
+stdout outside the checkout to retain a receipt. No handwritten result
+receipt is included, and no predecessor scientific verifier is run.
+
+## Scope and remaining obligations
+
+The complex-rank-shape-decoder card changes to a finite interface side
+result. This is an exact benchmark for a changed decoder hypothesis,
+without a complete paid-moment improvement. The selected source-binding
+positive control passed; the selected record and frontier are unchanged.
+
+The result fixes five unit binary payloads, one simultaneous common
+message, the two original neighbor observations and joint success.
+It proves no direct-product, adaptive-observation, input-correlated
+side-information or general nonlinear native theorem. Physical reads,
+the nonlinear encoding operations, dirty restoration, ownership,
+frames, stock, precision, tapes, compiler and outer recovery are not
+priced or implemented. No physical supplier, new kappa or complete
+multiplication theorem is claimed. Lean, Docker and selected cold
+supplier replay are outside this contribution.
+
+Canonical base is 7c49fe32c55de02c2c873655c804b16e4c3fef0a, priority
+revision 8. [TASK.json](TASK.json) preserves the card, changed scope and
+[advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19375558).
+SOURCES.json pins the exact predecessor README bytes. Live claims,
+open and merged PR bodies and the main-tree README corpus were searched
+for nonlinear cycles, partial/joint success and the exact object.
+The final cached overlap covered 581 open PRs and 6,655 Discussion records with
+reported complete pagination, but only 132 of 8,917 local notes in the
+sparse checkout. Separate main-tree searches supplement those notes;
+arbitrary diffs, unindexed literature and unpublished work remain limits.
+
+## Implementation bounds
+
+Every search concerns at most 32 inputs, subsets through size six,
+32 size-five classes or 480 size-four classes. All functions fit within
+60 physical lines. There is no recursion, dynamic code, network access,
+external solver or third-party runtime dependency. Explicit exceptions
+retain every scientific check under optimization. Source and package
+files are bounded below one MiB; the declared source list has five rows.
+Both registered modes treat Python warnings as errors. No external
+static analyzer or independent proof kernel is claimed.
+
+Power of Ten rule 3 deviation: CPython dynamically allocates integers,
+tuples and bounded sets during these one-shot enumerations. Static
+allocation is unavailable in this runtime. The fixed 32-input domain
+bounds all live collections, including at most 114,960 four-class pairs
+and 1,600 four-pack unions. The separate enumerations and optimized
+replays check those capacities and the complete finite domain. A native
+steady-operation implementation would require fixed-capacity storage
+before removing this deviation.
+
+## Open next questions
+
+1. Can a legal source-owned physical query layer realize the two-bit
+   5/8-success witness with a useful complete bill? First specify all
+   original observations, arbitrary dirty fields and the whole encoder/
+   receiver operator. Nonlinear native operations, restoration and a
+   compatible complete caller remain blockers.
+2. What is the exact joint-success tradeoff for two copies with coupled
+   encoding? First form the 1,024-input confusion graph for one named
+   message budget. The present one-copy packing certificate gives no
+   direct-product theorem; coupled confusability is a separate obstacle.
+
+Research stops at this first verified finite result.

research/nonlinear-cycle-success/SOURCES.json

@@ -0,0 +1,36 @@
+{
+  "schema_version": 1,
+  "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+  "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"
+    },
+    {
+      "path": "research/odd-cycle-query-capacity/README.md",
+      "usage": "input",
+      "git_blob": "55514f7ff0e239472ed2ca9c872c4cb2b8c53968",
+      "sha256": "7da79bbc83e6612e094fc040d6857343c97254ee10415a386b86406413350961"
+    },
+    {
+      "path": "research/paired-plane-block-rank/README.md",
+      "usage": "input",
+      "git_blob": "d0d06862952ba99c25a732ce9f43cee7f0f039cb",
+      "sha256": "0d9e5849dc7440738526c3020a669cc239254a8e16413e7df69108f9572fcf1e"
+    },
+    {
+      "path": "research/unequal-cycle-payloads/README.md",
+      "usage": "input",
+      "git_blob": "8e1e01bb308b7a9147847446a7070b0c7bb9f354",
+      "sha256": "834cd8c46c3893962afe96bdf13eccf21f698fcf26e8fe0ac3c9efd1cea1e4c4"
+    }
+  ]
+}