diff --git a/research/nonlinear-cycle-success/PROOF.md b/research/nonlinear-cycle-success/PROOF.md new file mode 100644 index 0000000000..bb8f2c7b0d --- /dev/null +++ b/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. diff --git a/research/nonlinear-cycle-success/README.md b/research/nonlinear-cycle-success/README.md new file mode 100644 index 0000000000..cdb209a827 --- /dev/null +++ b/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. diff --git a/research/nonlinear-cycle-success/SOURCES.json b/research/nonlinear-cycle-success/SOURCES.json new file mode 100644 index 0000000000..cdc67611eb --- /dev/null +++ b/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" + } + ] +} diff --git a/research/nonlinear-cycle-success/TASK.json b/research/nonlinear-cycle-success/TASK.json new file mode 100644 index 0000000000..ada854d891 --- /dev/null +++ b/research/nonlinear-cycle-success/TASK.json @@ -0,0 +1,82 @@ +{ + "schema_version": 1, + "task_id": "complex-rank-shape-decoder", + "priority_revision": 8, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "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": "Sharp nonlinear partial-recovery success curve on five independent binary cycle payloads, with one common M-value broadcast and original neighbor side information.", + "scope_change_reason": "The current card asks for a fully paid decoder gain. This side result changes linearity and exact recovery to arbitrary nonlinear encoding with partial joint recovery, quantifying a finite interface obstruction without claiming physical or moment improvement.", + "bottleneck_link": "Distinguishes exact linear query-capacity exclusions from a changed nonlinear decoder contract; gives an exact cost-versus-joint-error benchmark before any proposed physical construction.", + "budget_minutes": 60, + "stop_rule": "Ship the first sharp verified curve; no larger alphabets, other graphs, tensor powers or physical implementation in this contribution.", + "outcome": "completed", + "evidence": "PROOF.md; exhaustive class/packing/complement certificates; separately implemented truth-table enumeration; eight literal attaining protocols and eight rejection controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can a legal source-owned physical query layer realize the two-bit 5/8-success witness with a useful full paid bill?", + "why_it_matters": "The finite encoder has no native price or restoration guarantee.", + "first_step": "Specify original source observations, arbitrary dirty fields and the complete encoder/receiver operator; charge every nonlinear operation and return.", + "blocked_by": "No physical nonlinear native alphabet, restoration program or compatible complete caller is supplied." + }, + { + "question": "What is the exact joint-success tradeoff for two independent copies when encoding may couple their payloads?", + "why_it_matters": "A one-copy success curve does not prove a direct-product theorem.", + "first_step": "Form the 1024-input coupled confusion graph and seek a bounded certificate for one named message budget.", + "blocked_by": "Confusability and joint failure couple across copies; the one-copy packing proof does not transfer automatically." + } + ], + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19375558" +} diff --git a/research/nonlinear-cycle-success/VERIFY.json b/research/nonlinear-cycle-success/VERIFY.json new file mode 100644 index 0000000000..286dd264ea --- /dev/null +++ b/research/nonlinear-cycle-success/VERIFY.json @@ -0,0 +1,63 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/odd-cycle-query-capacity/README.md", + "research/paired-plane-block-rank/README.md", + "research/unequal-cycle-payloads/README.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Complete finite nonlinear success certificate and literal attainers/controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Complete finite nonlinear success certificate and literal attainers/controls." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/independent.py" + ], + "timeout_seconds": 120, + "checks": "Separate receiver truth-table inventory and independent four/five-class and complementary-pair obstruction." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/independent.py" + ], + "timeout_seconds": 120, + "checks": "Separate receiver truth-table inventory and independent four/five-class and complementary-pair obstruction." + } + ] +} diff --git a/research/nonlinear-cycle-success/independent.py b/research/nonlinear-cycle-success/independent.py new file mode 100644 index 0000000000..56cdd0aee6 --- /dev/null +++ b/research/nonlinear-cycle-success/independent.py @@ -0,0 +1,94 @@ +"""Separate enumeration from receiver truth-table consistency.""" + +import hashlib +import itertools +import json + + +def check(condition, message): + if not condition: + raise ValueError(message) + + +def local_tables(): + assignments = [] + for value in range(32): + digits = tuple(int(c) for c in f"{value:05b}"[::-1]) + zero, one = 0, 0 + for receiver in range(5): + neighbors = (digits[(receiver + 4) % 5], + digits[(receiver + 1) % 5]) + slot = 4 * receiver + neighbors[0] + 2 * neighbors[1] + if digits[receiver]: + one |= 1 << slot + else: + zero |= 1 << slot + assignments.append((zero, one)) + return assignments + + +def class_inventory(): + assignments = local_tables() + levels = [set() for _ in range(7)] + levels[0].add(0) + states = [(0, 0, 0)] + for size in range(1, 7): + following = [] + for members, zero, one in states: + for value in range(members.bit_length(), 32): + new_zero, new_one = assignments[value] + if not (zero & new_one or one & new_zero): + mask = members | (1 << value) + levels[size].add(mask) + following.append((mask, zero | new_zero, one | new_one)) + states = following + check(not states, "six-input truth-table fiber") + return [sorted(level) for level in levels] + + +def packing_certificate(levels): + fives, fours = levels[5], levels[4] + check(len(fives) == 32 and len(fours) == 480, "inventory sizes") + four_unions = [] + for count in (4, 5): + for chosen in itertools.combinations(fives, count): + union = 0 + for mask in chosen: + if union & mask: + break + union |= mask + else: + check(count == 4, "five disjoint maximal fibers") + four_unions.append(union) + check(len(four_unions) == 1600, "four-fiber inventory") + pair_unions = set() + for a, b in itertools.combinations(fours, 2): + if not a & b: + pair_unions.add(a | b) + for union in four_unions: + remaining = ((1 << 32) - 1) ^ union + for a in fours: + if a & remaining == a: + check((remaining ^ a) not in pair_unions, + "complete seven-message decoder") + return len(pair_unions) + + +def main(): + levels = class_inventory() + check(tuple(map(len, levels)) == (1, 32, 256, 640, 480, 32, 0), + "truth-table class counts") + pairs = packing_certificate(levels) + serialized = json.dumps(levels, separators=(",", ":")).encode() + digest = hashlib.sha256(serialized).hexdigest() + check(digest == + "a39ed8349b302d38efbdacb422c394044ec1c2042364c21f4d01ddda1a555c73", + "complete truth-table inventory digest") + print(json.dumps({"status": "PASS_NONLINEAR_CYCLE_TRUTH_TABLES", + "class_counts_by_size": list(map(len, levels)), + "inventory_sha256": digest, + "disjoint_four_pair_unions": pairs}, sort_keys=True)) + + +if __name__ == "__main__": + main() diff --git a/research/nonlinear-cycle-success/verify.py b/research/nonlinear-cycle-success/verify.py new file mode 100644 index 0000000000..b4ebfe7e4c --- /dev/null +++ b/research/nonlinear-cycle-success/verify.py @@ -0,0 +1,217 @@ +"""Exact finite certificate for nonlinear binary C5 partial recovery.""" + +import hashlib +import itertools +import json +from pathlib import Path + + +EXPECTED = (5, 10, 15, 20, 24, 28, 31, 32) +FULL = (1 << 32) - 1 +PACKAGE = Path(__file__).resolve().parent +FILES = ("README.md", "PROOF.md", "TASK.json", "SOURCES.json", + "VERIFY.json", "verify.py", "independent.py") +FOUR_FIVES = ((0, 3, 12, 27, 29), (1, 2, 13, 26, 28), + (4, 7, 8, 25, 31), (5, 6, 9, 24, 30)) +WITNESSES = { + 5: ((7, 11, 22, 24), (0, 12, 15, 17, 23), (2, 4, 21, 25, 26), + (5, 9, 10, 18, 20), (8, 14, 16, 19, 31)), + 6: ((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)), + 7: ((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)), +} + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def confuse(x, y): + difference = x ^ y + return any((difference >> i) & 1 + and not (difference >> ((i - 1) % 5)) & 1 + and not (difference >> ((i + 1) % 5)) & 1 + for i in range(5)) + + +def enumerate_classes(): + levels = [[0]] + for size in range(1, 7): + current = [] + for members in itertools.combinations(range(32), size): + if all(not confuse(x, y) + for x, y in itertools.combinations(members, 2)): + current.append(sum(1 << x for x in members)) + levels.append(sorted(current)) + require(not levels[6], "a six-input correct message class exists") + require(tuple(map(len, levels)) == (1, 32, 256, 640, 480, 32, 0), + "complete class inventory differs") + return levels + + +def five_packings(fives): + stack = [(0, 0, ())] + complete = [] + nodes = 0 + for _ in range(1 + sum(32 ** k for k in range(1, 6))): + if not stack: + break + start, union, chosen = stack.pop() + nodes += 1 + require(len(chosen) <= 4, "five disjoint five-input classes exist") + if len(chosen) == 4: + complete.append(union) + for index in range(start, len(fives)): + if not union & fives[index]: + stack.append((index + 1, union | fives[index], + chosen + (index,))) + require(not stack, "packing work bound exhausted") + require(nodes == 3249 and len(complete) == 1600, "packing inventory") + require(len(set(complete)) == 1600, "four-pack unions are not distinct") + return sorted(complete), nodes + + +def exclude_seven(packings, fours): + four_set = set(fours) + checks = 0 + for union in packings: + remaining = FULL ^ union + candidates = [a for a in fours if a & remaining == a] + for a, b in itertools.combinations(candidates, 2): + checks += 1 + if not a & b: + require((remaining ^ a ^ b) not in four_set, + "a complete seven-message protocol exists") + require(checks == 25280, "complement pair inventory") + return checks + + +def standard_classes(): + classes = [[] for _ in range(8)] + for x in range(32): + bits = tuple((x >> i) & 1 for i in range(5)) + label = (bits[0] ^ bits[1]) + 2 * (bits[2] ^ bits[3]) + 4 * bits[4] + classes[label].append(x) + return tuple(tuple(c) for c in classes) + + +def protocol(classes): + require(1 <= len(classes) <= 8, "message alphabet size") + encoder = [0] * 32 + tables = [[[None] * 4 for _ in range(5)] for _ in classes] + seen = set() + for label, members in enumerate(classes): + require(1 <= len(members) <= 5, "message class size") + for x in members: + require(type(x) is int and 0 <= x < 32, "binary input") + require(x not in seen, "message classes overlap") + seen.add(x) + encoder[x] = label + for i in range(5): + left = (x >> ((i - 1) % 5)) & 1 + right = (x >> ((i + 1) % 5)) & 1 + context = left + 2 * right + old = tables[label][i][context] + bit = (x >> i) & 1 + require(old is None or old == bit, "conflicting decoder output") + tables[label][i][context] = bit + for table in tables: + for row in table: + for context in range(4): + if row[context] is None: + row[context] = 0 + return encoder, tables + + +def execute(encoder, tables): + successful = [] + for x in range(32): + label = encoder[x] + answers = [] + for i in range(5): + left = (x >> ((i - 1) % 5)) & 1 + right = (x >> ((i + 1) % 5)) & 1 + answers.append(tables[label][i][left + 2 * right]) + if answers == [(x >> i) & 1 for i in range(5)]: + successful.append(x) + return successful + + +def witnesses(): + plans = {m: FOUR_FIVES[:m] for m in range(1, 5)} + plans.update(WITNESSES) + plans[8] = standard_classes() + for messages in range(1, 9): + encoder, tables = protocol(plans[messages]) + successful = execute(encoder, tables) + require(len(successful) == EXPECTED[messages - 1], "attaining protocol") + return plans + + +def controls(): + bad = ((), ((0, 1),), ((0,), (0,)), ((32,),), ((True,),), + (tuple(range(6)),), tuple((x,) for x in range(9))) + for classes in bad: + try: + protocol(classes) + except ValueError: + continue + raise ValueError("malformed or false witness accepted") + encoder, tables = protocol(FOUR_FIVES) + tables[0][0][0] ^= 1 + require(len(execute(encoder, tables)) < 20, "decoder mutation undetected") + return len(bad) + 1 + + +def source_hashes(): + root = PACKAGE.parents[1] + manifest = json.loads((PACKAGE / "SOURCES.json").read_text()) + require(len(manifest["files"]) == 5, "source declaration count") + result = {} + for row in manifest["files"]: + if row["usage"] == "input": + data = (root / row["path"]).read_bytes() + require(len(data) < 1 << 20, "source size") + digest = hashlib.sha256(data).hexdigest() + require(digest == row["sha256"], "changed cited input") + result[row["path"]] = digest + require(len(result) == 3, "live source count") + return result + + +def main(): + sources = source_hashes() + levels = enumerate_classes() + packings, nodes = five_packings(levels[5]) + pairs = exclude_seven(packings, levels[4]) + plans = witnesses() + control_count = controls() + inventory = json.dumps(levels, separators=(",", ":")).encode() + inventory_digest = hashlib.sha256(inventory).hexdigest() + require(inventory_digest == + "a39ed8349b302d38efbdacb422c394044ec1c2042364c21f4d01ddda1a555c73", + "complete class inventory digest") + package_hashes = {} + for name in FILES: + data = (PACKAGE / name).read_bytes() + require(len(data) < 1 << 20, "package file size") + package_hashes[name] = hashlib.sha256(data).hexdigest() + receipt = { + "status": "PASS_NONLINEAR_CYCLE_SUCCESS", + "claim_type": "finite certificate with a scoped combinatorial proof", + "message_values": list(range(1, 9)), "success_counts": list(EXPECTED), + "class_counts_by_size": list(map(len, levels)), + "inventory_sha256": inventory_digest, + "packing_nodes": nodes, "four_five_packings": len(packings), + "complement_pair_checks": pairs, "controls": control_count, + "attainers": {str(m): plans[m] for m in range(1, 9)}, + "package_sha256": package_hashes, "input_sha256": sources, + } + print(json.dumps(receipt, sort_keys=True)) + + +if __name__ == "__main__": + main()