From 6595ed483ae6d3030d327b7855594d83980c0384 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Fri, 23 Oct 2026 00:11:17 +0100 Subject: [PATCH] feat(research): bound nonlinear savings by coordinate restrictions --- .../eisenstein-nonlinear-restriction/PROOF.md | 127 +++++++++ .../README.md | 145 +++++++++++ .../SOURCES.json | 36 +++ .../TASK.json | 79 ++++++ .../VERIFY.json | 36 +++ .../restrictions.py | 86 +++++++ .../verify.py | 243 ++++++++++++++++++ 7 files changed, 752 insertions(+) create mode 100644 research/eisenstein-nonlinear-restriction/PROOF.md create mode 100644 research/eisenstein-nonlinear-restriction/README.md create mode 100644 research/eisenstein-nonlinear-restriction/SOURCES.json create mode 100644 research/eisenstein-nonlinear-restriction/TASK.json create mode 100644 research/eisenstein-nonlinear-restriction/VERIFY.json create mode 100644 research/eisenstein-nonlinear-restriction/restrictions.py create mode 100644 research/eisenstein-nonlinear-restriction/verify.py diff --git a/research/eisenstein-nonlinear-restriction/PROOF.md b/research/eisenstein-nonlinear-restriction/PROOF.md new file mode 100644 index 0000000000..af2a642cea --- /dev/null +++ b/research/eisenstein-nonlinear-restriction/PROOF.md @@ -0,0 +1,127 @@ +# Coordinate faces bound the possible nonlinear saving + +This contribution is produced by Nick Petalas. New work is Apache-2.0. + +## Model and credited premise + +Use Michael Fischler's [PR814 fixed-support nonlinear model](../eisenstein-message-copy-bound/PROOF.md). +There are forty Eisenstein E8 ports. Port t holds b_t independent binary +coordinates. Put N=sum_t b_t. Each fixed-width message Y_j=f_j(X_Aj) has +q_j bits, fixed source support A_j and fixed reader support R_j. Receiver t +recovers all its input bits on every input, using its received messages and +the inputs of ports orthogonal to t. Decoders need not be linear. + +The abstract charge is C=sum_j q_j c(R_j,A_j), where c is half the rational +pairing rank of the two line-generated subspaces. Charges add per bit. +This is a model premise, not a proved physical implementation price. + +We invoke Jose Manuel's [PR2017 fixed-support block-linear corollary](../eisenstein-reduction-copy-floor/README.md#fixed-support-block-linear-corollary). +If all messages are binary linear in the independent input coordinates, +then C is at least the total demand. This includes arbitrary unequal +demands, zero demands, arbitrary fixed supports, and nonlinear decoders. +An affine message has the same conclusion after its known constant is +subtracted at each reader. The good-reduction and Schur-rank proof are +credited premises; this package does not re-prove or replay them. + +## The new restriction lemma + +Fix a set S of h individual input coordinates to one specified assignment a. +Suppose that, on this coordinate face, every output bit of every message +is affine in the N-h unfixed coordinates. Then + + C >= N-h. (1) + +Proof. The unfixed coordinates still range independently over their full +binary product. Each port now demands exactly its own unfixed coordinates. +Every old decoder remains correct on the face. Its fixed coordinates are +known constants; its unfixed side information still comes only from +orthogonal ports. Subtract the known affine constants of the messages. +This gives a fixed-support block-linear protocol for total demand N-h. +It may retain the original supports and widths. Apply the credited +PR2017 theorem directly to obtain (1). Alternatively, remove inactive +sources and readers. Restricting the bilinear pairing to smaller spans +cannot increase its rank, so that version has charge at most the original +C and gives the same inequality. This proves the lemma. + +Let h_* be the minimum number of coordinates fixed on any such affine +face, allowing arbitrary specified zero or one values. A face always +exists, since fixing all N coordinates makes every message constant. Thus + + C >= N-h_*. (2) + +The face is a restriction used to prove an exact-code lower bound. +It is not an input-dependent free routing header. No execution is given +extra information about a random input. Arbitrary affine subspaces that +couple different ports are excluded: they need not preserve the product +of independent per-port demands required by the credited theorem. + +## An exact monomial hitting-set corollary + +Represent each transmitted bit by its unique squarefree algebraic normal +form over F2, in all N individual input coordinates. Form a hypergraph E +whose edges are all monomial supports of degree at least two appearing +in at least one output bit. Let tau(E) be its minimum vertex-cover size. +Here a vertex cover meets every edge, and the empty hypergraph has tau=0. + +Setting every variable in a cover S to zero removes every nonlinear +monomial. All surviving terms are affine. Conversely, after fixing S to +zero, every monomial disjoint from S survives unchanged, and distinct +surviving monomials cannot cancel. Hence zero fixing makes all messages +affine exactly when S meets every edge. The exact minimum zero-fixing +number is tau(E). In particular h_*<=tau(E), and + + C >= N-tau(E). (3) + +For quadratic messages, E is the ordinary interaction graph across all +output bits, so its vertex-cover number supplies the bound. +The minimum is not a claim about computing vertex cover in polynomial time. +The executable searches only the bounded domains stated in its README. + +Nonzero faces can improve (3). For one output with ANF + + x0*x1 + x0*x2 + x1*x2 + x0*x1*x2, + +the zero-face cover number is two, since all three edges of a triangle +occur. Fixing x2=1 instead leaves x0+x1, so h_*=1. The function is nonlinear +on the full cube, making this minimum exact. This distinguishes (2) from +the zero-face corollary. + +## Meaning for a cheaper nonlinear proposal + +Any proposed exact code with C<=N-d must satisfy h_*>=d and tau(E)>=d. +For equal b-bit demands, N=40b. A proposed C<=31b therefore needs both +parameters at least 9b. The number 31 is a conditional target, not an +attained charge. It is motivated by Maximooch's historical PR1794 format +screen, cited through PR2017; that screen is not replayed or assumed by +the restriction proof. The inherited unrestricted nonlinear floor of 22b remains +separate; combining it with (2) gives max(22b,40b-h_*). + +These inequalities do not prove a nonlinear code with C= N-h**. Consequently + + C >= N-h_* >= N-tau(E), + +where h_* is the minimum fixing over all coordinate faces and tau(E) is +the minimum hitting set of the nonlinear monomial supports across every +output bit's algebraic normal form. For zero-valued fixings the minimum +is exactly tau(E). Nonzero faces can give a strictly stronger bound. + +This is a scoped proof with finite corroboration. The new step is the +model-preserving restriction of a genuinely nonlinear message map to +Jose Manuel's credited block-linear theorem. It does not settle the +unrestricted nonlinear optimum or give a new kappa. + +## Result and relevance + +[PROOF.md](PROOF.md) gives the all-width argument and the exact monomial +criterion. A coordinate restriction leaves the unfixed bits independent +within and across ports. The old receivers still recover them. Known +affine constants can be subtracted, so the retained linear floor applies. +Removing inactive supports can only decrease their pairing ranks. + +A putative saving d below N therefore requires h_*>=d and tau(E)>=d. +For equal b-bit demands, a proposed charge at most 31b requires at least +9b fixed bits to linearize the message map, under either parameter. +These are necessary conditions, with no assertion that such a cheaper +nonlinear code exists. The inherited unrestricted nonlinear floor 22b +combines with this result as max(22b,40b-h_*). + +The new exact fixture uses ports 0,28,29,39, an orthogonal four-frame in +the pinned geometry. Its fourth message is x3+x0*x1*x2, and the first +three messages are their owners' input bits. The fourth receiver has +the other three frame inputs as permitted side information. Thirty-six +direct messages complete the code. Each of its forty message prices is +one, and h_*=tau=1. The new lower bound is 39; the exhibited code costs +40. This is no claim of an attaining cost-39 code. + +The strict-face example is x0*x1+x0*x2+x1*x2+x0*x1*x2. Its zero-fixing +minimum is two, while fixing x2=1 leaves x0+x1, so h_*=1. + +## Reproduce + +From the repository root, using Python 3.12 and the standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/eisenstein-nonlinear-restriction +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/eisenstein-nonlinear-restriction/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -O -B research/eisenstein-nonlinear-restriction/verify.py +``` + +Another Python 3.12 executable can replace the local interpreter path. +Each registered command has a 120-second limit. Expected final status: + +```text +PASS_EISENSTEIN_NONLINEAR_RESTRICTION {"faces":18086,"maps":366,"new_fixture_lower_bound":39,"rejections":9,"semantic_controls":3} +``` + +The checker enumerates every Boolean function through three variables +and 88 deterministic multibit maps in four and five variables, totaling +366 maps, 18,086 coordinate faces and 164,114 point/output substitution +checks. An independent truth-value affine oracle corroborates symbolic +substitution, including cancellations on nonzero faces. Exact minimizers +are compared with exhaustive face and zero-face scans. + +The code fixture checks sixteen frame inputs, 64 receiver observations, +and 72 separate direct-bit component cases, together with all forty +actual rational pairing prices. Its product argument is written in the +proof; the checker does not enumerate 2^40 full inputs. Nine rejected +inputs/contracts and three semantic controls cover malformed ANFs, +search bounds, missing side information, retained nonlinear terms, +cancellation and a deleted cubic term. Explicit checks remain enabled +with Python optimization. + +Default replay writes no files. To generate a receipt bound to the new +proof/code and declared source hashes, add `--output NEW_PATH` to a direct +command. Use a scratch path outside the checkout. Existing outputs are +never replaced. No receipt is handwritten or committed. + +`restrictions.py` accepts at most forty variables, forty outputs and 256 +monomials per output. The exact zero-cut search accepts at most twelve +variables, and the exact arbitrary-face search at most eight. The census +uses at most five. These executable limits do not limit the written proof. +The code has no recursive path; every search is finite. Managed Python +allocations and the fixed rejection-control callbacks are documented +Power of Ten deviations from static allocation and direct-only calls. +The input and iteration caps bound their lifetimes and target sets. +Warning-strict ordinary/optimized replay supplies the available runtime +diagnostics; no new static-analysis dependency is introduced. + +## Scope, provenance and credit + +[SOURCES.json](SOURCES.json) pins base +624de9dc66858af0945e5f8a0942488d62280d43, priority revision 7. The original +card was `complex-rank-shape-decoder`. [TASK.json](TASK.json) records the +change to a nonlinear interface obstruction, outside the already closed +linear search. The selected metadata orientation passed. The card's +predecessor scientific replay was skipped because this assignment asks +for original work and excludes predecessor re-verification. + +Credit Michael Fischler / shiftybitshiftr [#814](https://github.com/CrocSwap/integer-mult-bounds/pull/814) +for the nonlinear fixed-support model and its 22b lower bound, Jose Manuel / +jmbarrancoml [#2017](https://github.com/CrocSwap/integer-mult-bounds/pull/2017) +for good reduction and the block-linear total-demand floor, and Jonathan +Lam [#798](https://github.com/CrocSwap/integer-mult-bounds/pull/798) following +Joel Pulikkan / GamingPuzzled for the geometry and pairing-cost model. +Maximooch's historical #1794 format screen motivates the example target +31b, without supplying a current selected-frontier comparison here. +ywz65's [#2607](https://github.com/CrocSwap/integer-mult-bounds/pull/2607) +is the distinct adaptive public affine-query extension. No predecessor +verifier is imported, executed or independently certified here. Geometry +data is read unchanged to price only the new fixture. + +The overlap check covered live PR lists, this account's past-day work, +recent handoffs, main-package searches and the cached task search. +The latter reports 410 open PR records at 23:02:36 UTC and 3,919 Discussion +records at 23:03:21 UTC on October 22. The sparse local-note search was +incomplete, so a separate Git-tree source search was used. Closed-PR +metadata in the cache was older; live merged searches supplemented it. +These are bounded searches, not proof of novelty. + +The proof requires exact deterministic decoding, independent product +inputs, fixed supports/widths, orthogonal side information and additive +per-bit prices. Coupled cross-port affine restrictions, correlated inputs, +errors, adaptive/private routing and shared physical tariffs are excluded. +No physical supplier, compiler, hosting, precision or multiplication-theorem +obligation is discharged. Independent human and formal proof-kernel review +are unclaimed. The selected frontier is unchanged. + +## Open next questions + +- Can an exact genuinely nonlinear code have C= N-h_* for fixed-support nonlinear Eisenstein messages, where h_* is the minimum coordinate fixing making every output affine; derive the exact zero-face monomial-transversal corollary.", + "scope_change_reason": "The card points to the sharp linear Eisenstein floor. We change the encoder premise to genuinely nonlinear messages and prove a new dependence-sensitive obstruction rather than search an already excluded linear decoder class.", + "bottleneck_link": "This local abstract obstruction limits how much a nonlinear decoder with concentrated nonlinear dependence can save. It neither supplies a complete supplier nor applies the historical packing ceiling to the changed model.", + "budget_minutes": 60, + "stop_rule": "Stop at the first proved coordinate-restriction bound and bounded exact verifier. Do not extend into nonlinear-code optimization or physical compilation.", + "outcome": "completed", + "evidence": "PROOF.md; verify.py and restrictions.py; generated hash-bound receipts are external scratch outputs. No predecessor verifier replay.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can an exact nonlinear code have pairing charge strictly below N while all supports and per-bit tariffs remain fixed?", + "why_it_matters": "The unrestricted equal-demand interval remains 22b to 40b; this result excludes savings larger than the affine-coordinate restriction number.", + "first_step": "Give a small exact code with declared supports, enumerate every receiver observation, and compute an affine-face witness before enlarging it.", + "blocked_by": "No attaining nonlinear advantage or physical tariff is supplied here." + }, + { + "question": "Can a portwise affine-subspace restriction improve the coordinate-face bound?", + "why_it_matters": "Within-port changes of bit basis preserve independent per-port demands and may expose larger affine restrictions.", + "first_step": "Analyze one nonlinear block map under invertible binary changes inside each port, without coupling separate ports.", + "blocked_by": "A proved parameter and bounded search beyond coordinate faces remain absent." + } + ], + "verification_environment": "CPython 3.12.15, Python standard library, macOS; ordinary and optimized warning-strict commands." +} diff --git a/research/eisenstein-nonlinear-restriction/VERIFY.json b/research/eisenstein-nonlinear-restriction/VERIFY.json new file mode 100644 index 0000000000..0d33ff4c5d --- /dev/null +++ b/research/eisenstein-nonlinear-restriction/VERIFY.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/eisenstein-message-copy-bound/PROOF.md", + "research/eisenstein-reduction-copy-floor/README.md", + "research/eisenstein-message-copy-bound/certificate.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "New coordinate-face/ANF census, nonlinear message fixture, source hashes and controls" + }, + { + "argv": [ + "{python}", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Same new checks with Python assertions disabled" + } + ] +} diff --git a/research/eisenstein-nonlinear-restriction/restrictions.py b/research/eisenstein-nonlinear-restriction/restrictions.py new file mode 100644 index 0000000000..bb5e4a19c3 --- /dev/null +++ b/research/eisenstein-nonlinear-restriction/restrictions.py @@ -0,0 +1,86 @@ +"""Exact coordinate restrictions of Boolean algebraic normal forms. + +New work produced by Nick Petalas. Apache-2.0. +An output is a sorted tuple of distinct variable-subset masks, including +mask zero for the constant one. Arithmetic is over F2. +""" + +from itertools import combinations + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def validate(n, outputs): + require(type(n) is int and 0 <= n <= 40, "variable bound") + require(type(outputs) is tuple and 1 <= len(outputs) <= 40, "output bound") + for terms in outputs: + require(type(terms) is tuple and len(terms) <= 256, "term bound") + require(all(type(t) is int and 0 <= t < 1 << n for t in terms), + "monomial mask") + require(terms == tuple(sorted(set(terms))), "canonical terms") + + +def evaluate(terms, point): + return sum(point & term == term for term in terms) & 1 + + +def restrict(terms, fixed, ones): + """Substitute fixed bits, retaining cancellations over F2.""" + require(type(fixed) is int and type(ones) is int and fixed >= 0 + and ones >= 0 and ones & ~fixed == 0, "face assignment") + zero = fixed ^ ones + result = set() + for term in terms: + if term & zero == 0: + result.symmetric_difference_update((term & ~fixed,)) + return tuple(sorted(result)) + + +def is_affine(outputs): + return all(term.bit_count() <= 1 for terms in outputs for term in terms) + + +def minimum_zero_cut(n, outputs): + """Exact nonlinear-monomial transversal; at most 2^12 cuts.""" + validate(n, outputs) + require(n <= 12, "cut search bound") + edges = {t for terms in outputs for t in terms if t.bit_count() >= 2} + for size in range(n + 1): + for selected in combinations(range(n), size): + cut = sum(1 << i for i in selected) + if all(cut & edge for edge in edges): + return cut + raise ValueError("unreachable: fixing every variable kills each edge") + + +def minimum_affine_face(n, outputs): + """Exact minimum fixing, including nonzero faces; at most 3^8 faces.""" + validate(n, outputs) + require(n <= 8, "face search bound") + for size in range(n + 1): + for selected in combinations(range(n), size): + fixed = sum(1 << i for i in selected) + for word in range(1 << size): + ones = sum(((word >> j) & 1) << i + for j, i in enumerate(selected)) + if is_affine(tuple(restrict(t, fixed, ones) for t in outputs)): + return fixed, ones + raise ValueError("unreachable: a singleton face is constant") + + +def from_truth_table(table): + """Boolean Mobius inversion on truth tables with at most 32 entries.""" + require(type(table) is tuple and len(table) in (1, 2, 4, 8, 16, 32), + "truth table bound") + require(all(type(bit) is int and bit in (0, 1) for bit in table), + "truth table bits") + coefficients = list(table) + n = len(table).bit_length() - 1 + for i in range(n): + for mask in range(1 << n): + if mask & (1 << i): + coefficients[mask] ^= coefficients[mask ^ (1 << i)] + return tuple(i for i, bit in enumerate(coefficients) if bit) diff --git a/research/eisenstein-nonlinear-restriction/verify.py b/research/eisenstein-nonlinear-restriction/verify.py new file mode 100644 index 0000000000..c980465107 --- /dev/null +++ b/research/eisenstein-nonlinear-restriction/verify.py @@ -0,0 +1,243 @@ +"""Finite corroboration of the nonlinear coordinate-restriction lemma. + +New work produced by Nick Petalas. Apache-2.0. Predecessor theorems are +cited premises, never imported or replayed by this checker. +""" + +import argparse +from fractions import Fraction +from hashlib import sha256 +from itertools import combinations +import json +from pathlib import Path +from random import Random + +from restrictions import (evaluate, from_truth_table, is_affine, + minimum_affine_face, minimum_zero_cut, require, + restrict, validate) + + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parents[1] + + +def canonical(value): + return json.dumps(value, sort_keys=True, separators=(",", ":")) + + +def source_hashes(): + manifest = json.loads((PACKAGE / "SOURCES.json").read_text()) + hashes = {} + for row in manifest["files"]: + if row["usage"] == "input": + digest = sha256((ROOT / row["path"]).read_bytes()).hexdigest() + require(digest == row["sha256"], "changed input: " + row["path"]) + hashes[row["path"]] = digest + for name in ("verify.py", "restrictions.py", "PROOF.md", "SOURCES.json"): + hashes[name] = sha256((PACKAGE / name).read_bytes()).hexdigest() + return hashes + + +def truth_affine(n, outputs, fixed, ones): + """Independent oracle from values at a base point and its neighbors.""" + free = tuple(i for i in range(n) if not fixed & (1 << i)) + for terms in outputs: + constant = evaluate(terms, ones) + slopes = tuple(evaluate(terms, ones | 1 << i) ^ constant for i in free) + for word in range(1 << len(free)): + point = ones | sum(((word >> j) & 1) << i + for j, i in enumerate(free)) + expected = constant ^ (sum(slopes[j] * ((word >> j) & 1) + for j in range(len(free))) & 1) + if evaluate(terms, point) != expected: + return False + return True + + +def face_census(n, outputs): + validate(n, outputs) + require(n <= 5, "census bound") + best, zero_best, faces, points = n + 1, n + 1, 0, 0 + for fixed in range(1 << n): + for ones in range(1 << n): + if ones & ~fixed: + continue + restricted = tuple(restrict(terms, fixed, ones) for terms in outputs) + affine = truth_affine(n, outputs, fixed, ones) + require(affine == is_affine(restricted), "affine oracle disagreement") + for point in range(1 << n): + if point & fixed == ones: + for original, reduced in zip(outputs, restricted): + require(evaluate(original, point) == evaluate(reduced, point), + "substitution disagreement") + points += 1 + if affine: + best = min(best, fixed.bit_count()) + if ones == 0: + zero_best = min(zero_best, fixed.bit_count()) + faces += 1 + fixed, ones = minimum_affine_face(n, outputs) + cut = minimum_zero_cut(n, outputs) + require(fixed.bit_count() == best, "minimum face disagreement") + require(cut.bit_count() == zero_best, "transversal disagreement") + require(best <= zero_best, "zero face is an allowed face") + return faces, points + + +def polynomial_census(): + maps, faces, points = 0, 0, 0 + for n in range(4): + for word in range(1 << (1 << n)): + table = tuple((word >> x) & 1 for x in range(1 << n)) + terms = from_truth_table(table) + require(tuple(evaluate(terms, x) for x in range(1 << n)) == table, + "Mobius inversion") + f, p = face_census(n, (terms,)) + maps, faces, points = maps + 1, faces + f, points + p + rng = Random(2017814) + for n, count, width in ((4, 64, 3), (5, 24, 4)): + for _ in range(count): + outputs = tuple(tuple(t for t in range(1 << n) if rng.randrange(2)) + for _ in range(width)) + f, p = face_census(n, outputs) + maps, faces, points = maps + 1, faces + f, points + p + triangle = ((3, 5, 6, 7),) + cut = minimum_zero_cut(3, triangle) + fixed, ones = minimum_affine_face(3, triangle) + require(cut.bit_count() == 2 and fixed.bit_count() == 1, + "nonzero-face strict improvement") + return {"maps": maps, "faces": faces, "point_output_checks": points, + "strict_example": {"zero_cut": cut, "fixed": fixed, "ones": ones, + "restricted": restrict(triangle[0], fixed, ones)}} + + +def rational_rank(matrix): + rows = [list(map(Fraction, row)) for row in matrix] + pivot = 0 + for col in range(len(rows[0]) if rows else 0): + found = next((i for i in range(pivot, len(rows)) if rows[i][col]), None) + if found is None: + continue + rows[pivot], rows[found] = rows[found], rows[pivot] + divisor = rows[pivot][col] + rows[pivot] = [x / divisor for x in rows[pivot]] + for i in range(pivot + 1, len(rows)): + multiplier = rows[i][col] + rows[i] = [x - multiplier * y for x, y in zip(rows[i], rows[pivot])] + pivot += 1 + if pivot == len(rows): + break + return pivot + + +def dot(left, right): + return sum(x * y for x, y in zip(left, right)) + + +def fixture_geometry(): + data = json.loads((ROOT / "research/eisenstein-message-copy-bound/certificate.json") + .read_text())["geometry"] + reps, rotation = data["representatives"], data["rotation4"] + images = [tuple(sum(Fraction(rotation[i][j], 4) * r[j] for j in range(8)) + for i in range(8)) for r in reps] + frame = next(f for f in combinations(range(40), 4) + if all(dot(reps[i], reps[j]) == dot(reps[i], images[j]) == 0 + for i, j in combinations(f, 2))) + prices = [] + for reader in range(40): + sources = frame if reader == frame[-1] else (reader,) + vectors = [v for a in sources for v in (reps[a], images[a])] + matrix = [[dot(v, w) for w in vectors] + for v in (reps[reader], images[reader])] + rank = rational_rank(matrix) + require(rank == 2, "new fixture singleton pairing price") + prices.append(rank // 2) + return frame, prices + + +def observation_check(outputs, side): + """A receiver sees its own message and declared side-information bits.""" + seen = [dict() for _ in range(4)] + count = 0 + for point in range(16): + for t in range(4): + key = (evaluate(outputs[t], point), point & side[t]) + demanded = (point >> t) & 1 + require(key not in seen[t] or seen[t][key] == demanded, + "receiver observation conflict") + seen[t][key] = demanded + count += 1 + return count + + +def nonlinear_fixture(): + frame, prices = fixture_geometry() + outputs = ((1,), (2,), (4,), (7, 8)) + observations = observation_check(outputs, (0, 0, 0, 7)) + cut = minimum_zero_cut(4, outputs) + fixed, ones = minimum_affine_face(4, outputs) + require(cut.bit_count() == fixed.bit_count() == 1, "cubic restriction") + # Product embedding; no 2^40-input enumeration is claimed. + full = tuple((1 << i,) if i != frame[-1] + else tuple(sorted((1 << i, sum(1 << j for j in frame[:3])))) + for i in range(40)) + validate(40, full) + require(not is_affine(full), "full code is genuinely nonlinear") + restricted = tuple(restrict(t, 1 << frame[0], 0) for t in full) + require(is_affine(restricted), "one fixed bit linearizes the full code") + direct_checks = sum(evaluate((1,), bit) == bit + for _ in range(36) for bit in range(2)) + require(direct_checks == 72, "padded direct messages") + return {"frame": frame, "pairing_prices": prices, "charge": sum(prices), + "frame_inputs": 16, "receiver_observations": observations, + "direct_bit_checks": direct_checks, "total_demand": len(full), + "minimum_fixing": fixed.bit_count(), + "new_lower_bound": len(full) - fixed.bit_count()} + + +def controls(): + rejected = [] + cases = (("negative variables", lambda: validate(-1, ((1,),))), + ("boolean monomial", lambda: validate(1, ((True,),))), + ("duplicate monomial", lambda: validate(1, ((1, 1),))), + ("out-of-range monomial", lambda: validate(2, ((4,),))), + ("invalid face", lambda: restrict((3,), 1, 2)), + ("unbounded cut search", lambda: minimum_zero_cut(13, ((1,),))), + ("unbounded face search", lambda: minimum_affine_face(9, ((1,),))), + ("nonbinary truth table", lambda: from_truth_table((0, 2))), + ("missing side information", + lambda: observation_check(((1,), (2,), (4,), (7, 8)), (0, 0, 0, 6)))) + for name, action in cases: + try: + action() + except ValueError: + rejected.append(name) + else: + raise ValueError("control accepted: " + name) + require(not is_affine((restrict((3,), 0, 0),)), "empty cut leaves a product") + require(restrict((3, 5, 6, 7), 4, 4) == (1, 2), "XOR cancellation control") + require(evaluate((7, 8), 7) != evaluate((8,), 7), "omitted cubic detected") + return {"rejections": rejected, "semantic_controls": 3} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--output", type=Path, help="write a new generated receipt") + args = parser.parse_args() + hashes = source_hashes() + result = {"schema": "eisenstein-nonlinear-restriction/v1", "sources": hashes, + "polynomial_census": polynomial_census(), + "nonlinear_fixture": nonlinear_fixture(), "controls": controls()} + if args.output: + with args.output.open("x") as stream: + stream.write(json.dumps(result, sort_keys=True, indent=2) + "\n") + print("PASS_EISENSTEIN_NONLINEAR_RESTRICTION " + canonical({ + "maps": result["polynomial_census"]["maps"], + "faces": result["polynomial_census"]["faces"], + "new_fixture_lower_bound": result["nonlinear_fixture"]["new_lower_bound"], + "rejections": len(result["controls"]["rejections"]), + "semantic_controls": result["controls"]["semantic_controls"]})) + + +if __name__ == "__main__": + main()