From 83e78085ae9c110a34bff87e71387292d85e47c0 Mon Sep 17 00:00:00 2001 From: Alexander Templeton <10369436+azide0x37@users.noreply.github.com> Date: Tue, 13 Oct 2026 00:31:11 -0500 Subject: [PATCH] Add scoped nonlinear Hurwitz copy-floor proof and exact replay --- .../hurwitz-nonlinear-copy-floor/CLAIM.md | 60 ++ .../hurwitz-nonlinear-copy-floor/PROOF.md | 153 ++++ .../hurwitz-nonlinear-copy-floor/README.md | 92 ++ .../hurwitz-nonlinear-copy-floor/RESULTS.json | 824 ++++++++++++++++++ .../hurwitz-nonlinear-copy-floor/SOURCES.json | 39 + .../VALIDATION.md | 84 ++ .../test_verify.py | 109 +++ .../hurwitz-nonlinear-copy-floor/verify.py | 344 ++++++++ 8 files changed, 1705 insertions(+) create mode 100644 research/hurwitz-nonlinear-copy-floor/CLAIM.md create mode 100644 research/hurwitz-nonlinear-copy-floor/PROOF.md create mode 100644 research/hurwitz-nonlinear-copy-floor/README.md create mode 100644 research/hurwitz-nonlinear-copy-floor/RESULTS.json create mode 100644 research/hurwitz-nonlinear-copy-floor/SOURCES.json create mode 100644 research/hurwitz-nonlinear-copy-floor/VALIDATION.md create mode 100644 research/hurwitz-nonlinear-copy-floor/test_verify.py create mode 100644 research/hurwitz-nonlinear-copy-floor/verify.py diff --git a/research/hurwitz-nonlinear-copy-floor/CLAIM.md b/research/hurwitz-nonlinear-copy-floor/CLAIM.md new file mode 100644 index 0000000000..5f13f6fb2f --- /dev/null +++ b/research/hurwitz-nonlinear-copy-floor/CLAIM.md @@ -0,0 +1,60 @@ +# Sprint claim: fixed-support nonlinear Hurwitz messages + +- Track: structural decoder research; OS-random assignment seed **42**. +- Random draw: `3666255942` from `od -An -N4 -tu4 /dev/urandom`; below + the unbiased rejection cutoff `4294967200`; residue modulo 100 is 42. +- Exact base: `66849e1475c930fd7732b1a0067ffee7e1e95f60`. +- Claim time: 2026-10-13 05:17 UTC; expected finish: 05:55 UTC. +- Object: ten Hurwitz E8 lines with perfect-matching orthogonality; finite, + deterministic, zero-error messages with fixed source and reader supports, + arbitrary binary block width, and potentially nonlinear joint decoding. +- Hypothesis: under the explicit per-message charge `q * c(R,A)`, where q + is transmitted bit width and c is the predecessor's quaternionic pairing + rank, allowing vector and nonlinear messages still costs at least the + sum of demanded bit widths. The physical width-pricing premise is assumed, + not proved for arbitrary physical suppliers. +- Method: replace scalar rank subadditivity by conditional transcript + injectivity; average over all 32 orthogonal-pair transversals. Verify the + finite geometric inequalities and genuinely nonlinear attaining examples. +- Deliverable: scoped negative-result proof, exact reproducible certificate, + source pins, and controls that exercise the boundary assumptions. + +Three candidates considered, in seed-selected order (`42 mod 3 = 0`): + +1. Nonlinear and vector messages on the Hurwitz perfect-matching geometry. + Chosen: #703 explicitly excludes this model, and a counting argument is a + different method from its binary rank proof. +2. Extend the degenerate-label quotient argument in format-limits-corrected + C.4 to repeated/vector labels. Deferred: first requires a more precise + interface for how partial subspace messages are physically copied. +3. Mixed-port E8 replacement. Not chosen: #715 already proves saturation in + the minimal-deletion class; #747 covers the nearby star-puncture problem. + +The selected certificate, actual #626/#622/#623 construction and maintainer +review, current status, contribution-review index and PR ledger were read. +Selected kappa remains `51110230636731/31250000000000000`, conditional on +the recorded implementation and analytic assumptions. + +No pinned coordination issue exists (fresh GitHub query immediately before +this local claim). No reservation issue was opened. Open-PR searches for +`Hurwitz nonlinear` and `entropy copy` returned no matches. Inspected #703 +and #738 (scalar-total floors), and #757/#761 (fixed-label scalar P111 +floors); they leave the nonlinear model outside scope. #740 is our previous, +separate inventory-provenance contribution. No worker delegation is used. + +Orientation and selection ended here. The final quarter of this bounded +iteration is reserved for verification, refreshed overlap checks and handoff. + +## Result update + +Completed the scoped negative result and exact replay: the fixed-support, +additively width-priced nonlinear message model has minimum copy charge +10b on the ten Hurwitz lines. The proof is by transcript injectivity, with +nonlinear attaining codes, all support inequalities, twelve mathematical +rejection controls and two artifact mutation controls. It does not prove +the physical width-pricing premise or claim a new kappa. The refreshed +overlap review is recorded in [VALIDATION.md](VALIDATION.md). + +Reviewable result: +[contribution branch](https://github.com/azide0x37/integer-mult-bounds/tree/codex/seed42-hurwitz-nonlinear-copy-floor/research/hurwitz-nonlinear-copy-floor). +This is the single additional PR requested after #740; stop after submission. diff --git a/research/hurwitz-nonlinear-copy-floor/PROOF.md b/research/hurwitz-nonlinear-copy-floor/PROOF.md new file mode 100644 index 0000000000..9811bf6317 --- /dev/null +++ b/research/hurwitz-nonlinear-copy-floor/PROOF.md @@ -0,0 +1,153 @@ +# A counting extension of the Hurwitz copy floor + +**Scoped result.** For the ten Hurwitz E8 lines, fixed-support, deterministic, +zero-error messages of arbitrary binary widths have minimum charge +`C = sum_t b_t`, when port t demands b_t independent bits and a q-bit message +with reader/source sets R,A is charged `q c(R,A)`. In particular, equal +block width b costs at least 10b quaternionic units, or 40b rational units. +Encoders and decoders may be nonlinear. No bound on the number of messages +is imposed, other than finiteness. + +This extends the scalar-total argument of Douglas R. Colkitt's +[#703](https://github.com/CrocSwap/integer-mult-bounds/pull/703), at commit +`358383e2f1b0f292d4d6eb897c06fd8558a4f5e6`. The perfect-matching geometry, +pairing charge, transversal weights and scalar optimum are predecessor work. +The addition here is conditional transcript injectivity in place of binary +rank, together with nonlinear attaining examples and assumption controls. + +## 1. Geometry and the pricing premise + +Use the E8 roots in doubled coordinates: vectors in Q^8 with either two +entries in {2,-2} and the rest zero, or eight entries in {1,-1} and an even +number of minus signs. Regard Q^8 as H_Q^2 and take the spans of the four +left multiples 1,i,j,k of each root. These are ten four-dimensional rational +subspaces. Their orthogonality graph is five disjoint pairs; write mate(t) +for the unique orthogonal line. Any two distinct lines span Q^8. + +For concatenated row bases V_R and V_A, set + + c(R,A) = rank_Q(V_R V_A^T) / 4. + +The exact charge table is: + +- 0 if a set is empty, or R and A are singletons at orthogonal mates; +- 1 otherwise if a nonempty set is a singleton; +- 2 if both sets have at least two elements. + +Two spanning sets have rank-eight pairing. A singleton against a spanning +set has rank four. Nonorthogonal singletons have rank-four pairing; mates +have zero pairing. The verifier reconstructs all roots and line bases, +checks every singleton pairing and every two-line span over the integers, +then checks every support pair against the transversal inequality below. + +**Explicit pricing premise:** a message of fixed width q_j, sent from source +set A_j to reader set R_j, is charged `q_j c(R_j,A_j)` quaternionic units. +Charges add over messages. Every transmitted bit is priced, even if the +encoder combines coordinates nonlinearly. This is the chosen block-message +model. It is **not** a derivation of nonlinear physical copy costs from +#446's scalar pairing-rank theorem. A supplier that shares physical work +between message coordinates more cheaply is outside this result. + +## 2. Information model + +There are independent inputs X_t ranging freely over {0,1}^{b_t}; b_t are +nonnegative integers. Message j has a fixed nonnegative integer width q_j +and is a deterministic function + + Y_j = f_j((X_a)_{a in A_j}) in {0,1}^{q_j}. + +The supports, widths and functions do not depend on the input. Every reader +t in R_j receives the same full Y_j; it may process those bits arbitrarily. +Receiver t must reconstruct X_t for **every** input tuple, using its received +messages and free side information X_mate(t). The decoder may jointly use +all those messages and need not be linear. Granting the entire mate input +is an optimistic relaxation of orthogonal residual correction. + +Source access, encoding, decoding and side-information preparation are free +in this model. There is no interactive relay, adaptive support, input +correlation, decoding error or additional nonorthogonal side information. +The theorem also covers a scalar fitting decoder from #703: each rank-one +total is one width-one message, and its mate contamination can be removed +using the granted side information. Fixed-support block-linear codes are +included as well, without requiring coordinatewise encoding. + +## 3. Transcript injectivity + +A transversal T chooses exactly one endpoint of each of the five mate +pairs. For this T define + + J_T = { j : R_j intersects T and A_j intersects T }. + +Fix **any** assignment of all inputs outside T. The map + + X_T -> (Y_j)_{j in J_T} + +is injective. To see this, suppose two different X_T assignments have the +same displayed transcript. Every message received by a receiver in T is +either in J_T or has A_j disjoint from T. Messages in the latter class are +identical because their source inputs were fixed. Every receiver's mate is +outside T, so all its side information is also identical. Its deterministic +decoder would therefore return the same X_t in both assignments, for all +t in T, contradicting the distinct X_T assignments. + +Consequently, counting possible transcripts gives + + 2^(sum_{t in T} b_t) <= 2^(sum_{j in J_T} q_j), + sum_{t in T} b_t <= sum_j q_j a_T(R_j,A_j), (1) + +where a_T is 1 exactly when both supports meet T. No probabilistic, +asymptotic or linearity assumption is used. The proof is for every finite +block width and every finite number of messages, not an extrapolation from +the truth tables used as controls. + +## 4. Average over the 32 transversals + +Each line lies in 16 transversals. For every R,A the predecessor inequality +is + + sum_T a_T(R,A) <= 16 c(R,A). (2) + +If c=0 no transversal hits both supports. If c=1 a singleton support occurs +in only 16 transversals. If c=2 the total number of transversals is 32. +Thus (2) follows in all cases. Summing (1) and dividing by 16 gives + + sum_t b_t <= sum_j q_j (sum_T a_T(R_j,A_j))/16 + <= sum_j q_j c(R_j,A_j) = C. + +The bound is sharp in the abstract model for arbitrary b_t: send X_t +directly from {t} to {t} with width b_t. This costs sum_t b_t. For equal +width b, another attaining code broadcasts the five mate-pair XORs in a +single 5b-bit message with all ports as sources and readers. Its charge is +`2 * 5b = 10b`. Apply any bijection of its 5b bits before transmission; +receivers invert it and recover their pair XOR using their mate input. +For example, the reversible update `z_2 ^= z_0 & z_1` makes the encoder +nonlinear and preserves both correctness and charge. The replay verifies +this example on all 1,024 inputs for ten one-bit ports, and a vector example +on all 256 inputs for four two-bit ports in the matching geometry. + +## 5. Optimistic complete-budget screen + +If, in addition, these b-fold ports satisfy the inherited Dfc stage +accounting with v=10, k=4b and cst=4C, then + + D/T = (s-1) * 40b - s * 4C <= -40b + +for every positive integer s and b. Helpers, source access, frame changes, +copies beyond this lower bound, restoration and recursive children were +all granted zero additional expense in this screen. Any nonnegative charge +for them cannot repair its negative deficit. There is no positive supplier +saving to feed into an assembly, regardless of the other supplier. +Accordingly no circuit implementation or kappa optimization is attempted. +The algebraic inequality supplies the all-s conclusion; the receipt's +finite arithmetic examples are only error controls. + +The use of Dfc and the conversion from message width to physical rank are +explicit additional assumptions. This note does not establish them for +nonlinear circuits. It does not bound interactive/adaptive codes, variable +length or average-cost communication, fractional physical sub-line copying, +correlated demands, other geometries or different stage accounting. + +Prepared by Alexander Templeton (@azide0x37) with substantial OpenAI Codex +assistance in the proof extension, implementation, checks and writing. +This is a written mathematical argument with finite exact checks, not a +proof-assistant formalization or a verification of integer multiplication. diff --git a/research/hurwitz-nonlinear-copy-floor/README.md b/research/hurwitz-nonlinear-copy-floor/README.md new file mode 100644 index 0000000000..42c7ebb72b --- /dev/null +++ b/research/hurwitz-nonlinear-copy-floor/README.md @@ -0,0 +1,92 @@ +# Nonlinear messages under the Hurwitz copy-charge model + +**Scoped negative result; no new kappa.** Fixed-support, zero-error vector or +nonlinear messages cannot reduce the ten-line Hurwitz E8 copy floor **if a +q-bit message is charged q times its reader/source pairing rank**. For b +independent bits per port the minimum is 10b quaternionic units, or 40b +rational units. Unequal widths have minimum charge equal to their sum. + +The width-pricing assumption is essential and is not established here for +arbitrary physical nonlinear suppliers. The [proof](PROOF.md) replaces the +scalar rank argument from [#703](https://github.com/CrocSwap/integer-mult-bounds/pull/703) +with a transcript-counting argument. It permits arbitrary nonlinear encoding +and joint decoding, any finite number of fixed-width messages, and free +mate-port side information. It does not cover cheaper shared copying between +coordinates, adaptive or interactive messages, correlated inputs, error, +additional nonorthogonal side information, or changed stage accounting. + +This is an application of elementary zero-error counting, with no claim of +novelty for that general method. The contribution makes explicit which +vector/nonlinear extension of the predecessor's model still has its floor. + +## Reproduce + +From the repository root, with UV and CPython 3.10+ (standard library only): + +```sh +uv run --offline python -B research/hurwitz-nonlinear-copy-floor/verify.py +``` + +Expected: + +```text +PASS_HURWITZ_NONLINEAR_COPY: 1048576 support pairs; 3 attaining codes; 12 rejection controls; conditional floor 10b +``` + +The default command recomputes and checks [RESULTS.json](RESULTS.json). It +does not overwrite it. `--write /tmp/hurwitz-results.json` emits a separate +receipt for comparison. Neither network access nor another PR's files are +required at runtime. Source references and exact hashes are in +[SOURCES.json](SOURCES.json); the verifier binds that manifest to its receipt +but does not fetch or authenticate external GitHub content during replay. + +The replay reconstructs all 240 roots, ten line bases, 100 singleton Gram +blocks, 45 two-line spans, and all 1,048,576 ordered support pairs. It checks +32 weighted transversals and three exact attaining truth tables: ten one-bit +ports with a nonlinear encoder, four two-bit ports with nonlinear coordinate +mixing and a free mate-only message, and unequal widths including zero. +There are 33,856 conditional transcript checks across those examples. + +Twelve negative controls reject bad geometry/weights, underdeclared width, +missing sources/readers and corrupted transmissions. A boundary example +shows why the side-information premise matters: if every other input is +free, one global parity bit costs only 2 instead of 10 and decodes correctly. + +Additional independent checks: + +```sh +uv run --offline python -B research/hurwitz-nonlinear-copy-floor/test_verify.py +``` + +These compare every geometric obligation with a separate Fraction-based +column algorithm, explicitly invert the nonlinear codes on all 1,280 inputs, +exhaust all 65,536 one-bit encoders in a four-port instance, and reject receipt +and manifest mutations in a relocated optimized-mode replay. The finite +checks support the written proof; they are not its all-width justification. + +## Budget, scope and attribution + +Under the additional inherited Dfc accounting with k=4b, even the optimistic +complete budget is `D/T <= (s-1)40b - s40b = -40b`. All helper, source-access, +frame-change, restoration and recursive expenses were granted zero before +this screen. A paid construction cannot help under these premises, so none +was attempted. No selected certificate, supplier, `upstream/` file or +repository-wide generator changes. + +Base: `66849e1475c930fd7732b1a0067ffee7e1e95f60`. The selected conditional +result remains `51110230636731/31250000000000000`; none of its compiler, +realization, hosting, precision, tape or analytic obligations is discharged. +See [CLAIM.md](CLAIM.md) for seed 42, candidate selection and scope, and +[VALIDATION.md](VALIDATION.md) for the completed checks and overlap refresh. + +Credit Douglas R. Colkitt / Mister-Meeseeks (#703) for the exact scalar floor +and weighted-transversal certificate, Joel Pulikkan / GamingPuzzled (#620) +for the extension-ring investigation, and DreamingOfClouds (#446 and the +corrected format note) for the inherited accounting framework. Sagar +Thakrar's concurrent #738 develops the related scalar weighted-clique method +on Gaussian E8; this package does not claim its geometry or numeric result. + +Prepared by Alexander Templeton (@azide0x37) with substantial OpenAI Codex +assistance in proof development, implementation, verification and writing. +Apache-2.0. No independent human review or proof-assistant verification is +claimed. diff --git a/research/hurwitz-nonlinear-copy-floor/RESULTS.json b/research/hurwitz-nonlinear-copy-floor/RESULTS.json new file mode 100644 index 0000000000..ad9bca9fc4 --- /dev/null +++ b/research/hurwitz-nonlinear-copy-floor/RESULTS.json @@ -0,0 +1,824 @@ +{ + "attaining_examples": { + "nonlinear_ten_ports": { + "cost": 10, + "cut_states": 32768, + "floor": 10, + "messages": 1, + "nonlinear_witness": { + "a": [ + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "b": [ + 0, + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "nonzero_second_difference": 4 + }, + "states": 1024, + "widths": [ + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ] + }, + "nonlinear_vector_with_free_mate": { + "cost": 8, + "cut_states": 1024, + "floor": 8, + "messages": 2, + "nonlinear_witness": { + "a": [ + 1, + 0, + 0, + 0 + ], + "b": [ + 2, + 0, + 0, + 0 + ], + "nonzero_second_difference": 4 + }, + "states": 256, + "widths": [ + 2, + 2, + 2, + 2 + ] + }, + "unequal_width_direct": { + "cost": 4, + "cut_states": 64, + "floor": 4, + "messages": 4, + "states": 16, + "widths": [ + 0, + 1, + 2, + 1 + ] + } + }, + "conditional_budget_examples_b_s_deficit": [ + [ + 1, + 1, + -40 + ], + [ + 1, + 3, + -40 + ], + [ + 1, + 5, + -40 + ], + [ + 1, + 9, + -40 + ], + [ + 1, + 31, + -40 + ], + [ + 2, + 1, + -80 + ], + [ + 2, + 3, + -80 + ], + [ + 2, + 5, + -80 + ], + [ + 2, + 9, + -80 + ], + [ + 2, + 31, + -80 + ], + [ + 7, + 1, + -280 + ], + [ + 7, + 3, + -280 + ], + [ + 7, + 5, + -280 + ], + [ + 7, + 9, + -280 + ], + [ + 7, + 31, + -280 + ] + ], + "geometry": { + "basis_rows": [ + [ + [ + 0, + 0, + 0, + 0, + -2, + -2, + 0, + 0 + ], + [ + 0, + 0, + 0, + 0, + 2, + -2, + 0, + 0 + ], + [ + 0, + 0, + 0, + 0, + 0, + 0, + -2, + 2 + ], + [ + 0, + 0, + 0, + 0, + 0, + 0, + -2, + -2 + ] + ], + [ + [ + -2, + 0, + 0, + 0, + 2, + 0, + 0, + 0 + ], + [ + 0, + -2, + 0, + 0, + 0, + 2, + 0, + 0 + ], + [ + 0, + 0, + -2, + 0, + 0, + 0, + 2, + 0 + ], + [ + 0, + 0, + 0, + -2, + 0, + 0, + 0, + 2 + ] + ], + [ + [ + -2, + 0, + 0, + 0, + 0, + 2, + 0, + 0 + ], + [ + 0, + -2, + 0, + 0, + -2, + 0, + 0, + 0 + ], + [ + 0, + 0, + -2, + 0, + 0, + 0, + 0, + -2 + ], + [ + 0, + 0, + 0, + -2, + 0, + 0, + 2, + 0 + ] + ], + [ + [ + -2, + 0, + 0, + 0, + 0, + 0, + 2, + 0 + ], + [ + 0, + -2, + 0, + 0, + 0, + 0, + 0, + 2 + ], + [ + 0, + 0, + -2, + 0, + -2, + 0, + 0, + 0 + ], + [ + 0, + 0, + 0, + -2, + 0, + -2, + 0, + 0 + ] + ], + [ + [ + -2, + 0, + 0, + 0, + 0, + 0, + 0, + 2 + ], + [ + 0, + -2, + 0, + 0, + 0, + 0, + -2, + 0 + ], + [ + 0, + 0, + -2, + 0, + 0, + 2, + 0, + 0 + ], + [ + 0, + 0, + 0, + -2, + -2, + 0, + 0, + 0 + ] + ], + [ + [ + -2, + 0, + 0, + 0, + 0, + 0, + 0, + -2 + ], + [ + 0, + -2, + 0, + 0, + 0, + 0, + 2, + 0 + ], + [ + 0, + 0, + -2, + 0, + 0, + -2, + 0, + 0 + ], + [ + 0, + 0, + 0, + -2, + 2, + 0, + 0, + 0 + ] + ], + [ + [ + -2, + 0, + 0, + 0, + 0, + 0, + -2, + 0 + ], + [ + 0, + -2, + 0, + 0, + 0, + 0, + 0, + -2 + ], + [ + 0, + 0, + -2, + 0, + 2, + 0, + 0, + 0 + ], + [ + 0, + 0, + 0, + -2, + 0, + 2, + 0, + 0 + ] + ], + [ + [ + -2, + 0, + 0, + 0, + 0, + -2, + 0, + 0 + ], + [ + 0, + -2, + 0, + 0, + 2, + 0, + 0, + 0 + ], + [ + 0, + 0, + -2, + 0, + 0, + 0, + 0, + 2 + ], + [ + 0, + 0, + 0, + -2, + 0, + 0, + -2, + 0 + ] + ], + [ + [ + -2, + 0, + 0, + 0, + -2, + 0, + 0, + 0 + ], + [ + 0, + -2, + 0, + 0, + 0, + -2, + 0, + 0 + ], + [ + 0, + 0, + -2, + 0, + 0, + 0, + -2, + 0 + ], + [ + 0, + 0, + 0, + -2, + 0, + 0, + 0, + -2 + ] + ], + [ + [ + -2, + -2, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + 2, + -2, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + 0, + 0, + -2, + 2, + 0, + 0, + 0, + 0 + ], + [ + 0, + 0, + -2, + -2, + 0, + 0, + 0, + 0 + ] + ] + ], + "line_count": 10, + "mate_pairs": [ + [ + 0, + 9 + ], + [ + 1, + 8 + ], + [ + 2, + 7 + ], + [ + 3, + 6 + ], + [ + 4, + 5 + ] + ], + "root_count": 240, + "roots_per_line": 24, + "singleton_pairing_ranks": [ + [ + 4, + 4, + 4, + 4, + 4, + 4, + 4, + 4, + 4, + 0 + ], + [ + 4, + 4, + 4, + 4, + 4, + 4, + 4, + 4, + 0, + 4 + ], + [ + 4, + 4, + 4, + 4, + 4, + 4, + 4, + 0, + 4, + 4 + ], + [ + 4, + 4, + 4, + 4, + 4, + 4, + 0, + 4, + 4, + 4 + ], + [ + 4, + 4, + 4, + 4, + 4, + 0, + 4, + 4, + 4, + 4 + ], + [ + 4, + 4, + 4, + 4, + 0, + 4, + 4, + 4, + 4, + 4 + ], + [ + 4, + 4, + 4, + 0, + 4, + 4, + 4, + 4, + 4, + 4 + ], + [ + 4, + 4, + 0, + 4, + 4, + 4, + 4, + 4, + 4, + 4 + ], + [ + 4, + 0, + 4, + 4, + 4, + 4, + 4, + 4, + 4, + 4 + ], + [ + 0, + 4, + 4, + 4, + 4, + 4, + 4, + 4, + 4, + 4 + ] + ], + "two_line_spans_checked": 45 + }, + "local_certificate": { + "charge_counts": [ + 2057, + 20350, + 1026169 + ], + "maximum_hits_by_charge": [ + 0, + 16, + 32 + ], + "support_pairs": 1048576, + "transversal_masks": [ + 31, + 47, + 87, + 103, + 155, + 171, + 211, + 227, + 285, + 301, + 341, + 357, + 409, + 425, + 465, + 481, + 542, + 558, + 598, + 614, + 666, + 682, + 722, + 738, + 796, + 812, + 852, + 868, + 920, + 936, + 976, + 992 + ], + "weight": "1/16" + }, + "negative_controls": [ + "duplicate_root", + "wrong_root_norm", + "nonmatching_mates", + "omitted_transversal", + "wrong_weight", + "width_not_charged", + "negative_width", + "missing_source", + "missing_reader", + "truncated_output", + "altered_output", + "extra_side_information_not_granted" + ], + "outside_model_extra_side_information": { + "cost": 2, + "cut_states": 0, + "floor": 10, + "messages": 1, + "states": 1024, + "widths": [ + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ] + }, + "schema": 1, + "scope": "Fixed support, fixed width, zero error, independent inputs, q*c additive pricing; written all-width proof in PROOF.md", + "sources_manifest_sha256": "b81f8a13bc63c41db8c8ae635bff352765e9325fb38ebde3a88a92abf34a9e9b" +} diff --git a/research/hurwitz-nonlinear-copy-floor/SOURCES.json b/research/hurwitz-nonlinear-copy-floor/SOURCES.json new file mode 100644 index 0000000000..685900b32d --- /dev/null +++ b/research/hurwitz-nonlinear-copy-floor/SOURCES.json @@ -0,0 +1,39 @@ +{ + "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "runtime_dependencies": "CPython >=3.10, standard library only; no predecessor code imported", + "selected_kappa_context_only": "51110230636731/31250000000000000", + "predecessors": [ + { + "pr": 703, + "author": "Douglas R. Colkitt / Mister-Meeseeks", + "commit": "358383e2f1b0f292d4d6eb897c06fd8558a4f5e6", + "path": "research/hurwitz-asymmetric-copy-floor/PROOF.md", + "sha256": "7355fcb0eadef64ffd7909e6c3d7717d5a3fb2628449fa3c6c754cb2a5665585", + "role": "Scalar copy floor, exact Hurwitz geometry, charge table and transversal weights; read from the pinned PR, not vendored or imported at runtime" + }, + { + "pr": 620, + "author": "Joel Pulikkan / GamingPuzzled", + "retained_commit": "419c7374c3bf5f2eee28f08b1e50c1d57934081c", + "current_head_at_selection": "e9cf03bbdf7094b5a83f6dbd1d74bfd77a05fb87", + "path": "research/e8-decoder-floors-and-cold14-notes/s1-extension-rings/REPORT.md", + "sha256": "e8de809976a1253087e9058d346dfcc7b098f6481c64f1569aa3072d27345e02", + "role": "Extension-ring geometry and decoder investigation preceding #703; retained source is context only" + }, + { + "author": "DreamingOfClouds", + "commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "path": "research/format-limits-corrected/README.md", + "sha256": "1bcd80c1cd61fddae9f3a7f00fc9d1c796410408251e576600e94c19b16b1e5e", + "role": "Conditional Dfc accounting and #446 pairing-rank premises, not a proof of the nonlinear width-pricing premise" + } + ], + "concurrent_scope_checks": [ + {"pr": 738, "commit": "9671c5d72f3119ba26f3774f40aa7130c67bcf77", "role": "Sagar Thakrar's weighted-clique scalar floor on Gaussian E8; distinct geometry"}, + {"pr": 757, "commit": "e2ec7d7e719031e8f8b8012a4ab5b20faed074ce", "role": "Fixed-label scalar P111 floor; vector totals excluded"}, + {"pr": 761, "commit": "287758702129e6cbca187356b92b311e8a1c843d", "role": "Fixed-label scalar P111 floor; vector totals excluded"} + ], + "license": "Apache-2.0; no predecessor code copied", + "contributor": "Alexander Templeton (@azide0x37)", + "ai_disclosure": "Substantial OpenAI Codex assistance in proof development, implementation, verification and writing" +} diff --git a/research/hurwitz-nonlinear-copy-floor/VALIDATION.md b/research/hurwitz-nonlinear-copy-floor/VALIDATION.md new file mode 100644 index 0000000000..613804eff9 --- /dev/null +++ b/research/hurwitz-nonlinear-copy-floor/VALIDATION.md @@ -0,0 +1,84 @@ +# Validation and handoff + +Validation date: 2026-10-13 UTC. Prepared by Alexander Templeton with +substantial OpenAI Codex assistance. All results below are local execution +receipts, not independent human review or proof-assistant verification. + +## Completed checks + +- CPython 3.10.21 and 3.13.15: the default exact receipt replay and all four + independent test cases pass. +- CPython 3.14.7 with `-O`: the same receipt and four tests pass. All proof + checks in the main verifier use explicit exceptions, not `assert`. +- Exact geometry: 240 distinct E8 roots, ten quaternionic lines of 24 roots, + 100 singleton Gram ranks, and 45 two-line spanning obligations. A separate + Fraction column-basis algorithm agrees with the integer row algorithm on + all 145 rank obligations. +- All 1,048,576 ordered support pairs satisfy the weighted inequality. + There are 2,057 cost-zero, 20,350 cost-one and 1,026,169 cost-two pairs; + maximum transversal incidences are 0, 16 and 32, respectively. +- Three attaining codes pass all 1,296 input assignments and 33,856 + conditional transcript checks. Two use demonstrably nonlinear encoders; + a separate explicit inverse decodes all their 1,280 inputs. The remaining + example includes unequal and zero widths. A zero-cost mate-only message + is also accepted. +- All twelve internal rejection controls pass. Extra nonorthogonal side + information is separately shown to permit cost 2 instead of 10; this is + an explicit counterexample to dropping a premise, not a code in the model. +- The four-port one-bit search exhausts every Boolean truth table, encoded + by integers 0 through 65,535 in increasing order. Four tables let receiver + zero decode, and none lets all four decode. Sources and readers are all + four ports, with independent one-bit inputs and mate-only side information. + This complete finite search has no randomized choices; assignment seed 42 + selected the research scope. The stopping rule was completion of this + exact domain. The all-width theorem comes from PROOF.md, not this search. +- A relocated export containing only `verify.py`, `SOURCES.json` and + `RESULTS.json` passes from an unrelated working directory in isolated, + optimized mode. Mutating the copied receipt or source-manifest bytes + makes the process fail. These two artifact controls are additional to the + twelve mathematical controls. +- `uv run --offline python -B scripts/verify_selected_result.py` passes: + selected record, exact kappa, original source inventory and proof supplements + are unchanged. + +Commands and expected output are in [README.md](README.md). `--write` was used +once to create the committed deterministic receipt; normal validation only +reads and compares it. No solver, floating rank test, numerical optimization +or network service participates in the replay. + +The unchanged full `make verify` and selected supplier cold replay were not +repeated for this isolated research package. No remote CI pass is claimed. +The all-size/physical implementation and nonlinear width-pricing assumptions +remain outside the finite checks. + +## Remote refresh and distinct scope + +At 05:27 UTC, a fresh fetch still gave main at +`66849e1475c930fd7732b1a0067ffee7e1e95f60`. The open queue contained 594 PRs +through #775. #703 still had head +`358383e2f1b0f292d4d6eb897c06fd8558a4f5e6`, with no submitted reviews. +The preceding contribution #740 remained open with no comments or reviews. +There was no pinned sprint coordination issue, so the claim is local. + +The current overlap review inspected #703, #738, #757 and #761 and the +freshly arrived contributions below: + +- #765 (`d8eaa3db32f76111b39db9b930f347ef30118a28`) extends a fixed full-E8 + binary matrix floor to tensor basis mixing; it has different geometry and + factorization restrictions. +- #767 (`96b4b74677d1bef99e8346bfb6a4ed0531e58a62`) gives Gaussian planar and + incidence subclass obstructions. +- #770 (`48d027a664288ea1d4e987de63cb79588b8b936b`) establishes the weighted + maximal-clique method ceiling for Gaussian scalar totals; it explicitly + excludes vector totals. + +All-state searches for nonlinear, transcript and Hurwitz research were also +checked. #288's nonlinear controlled-shift frames and #682's tensor-provider +rate audit use different physical models. None of the inspected claims +establishes the fixed-support nonlinear Hurwitz message result here. This +does not assert novelty beyond the repository or claim priority for the +predecessor's geometry, weights, scalar floor or general counting technique. + +No source from these concurrent PRs is imported. The geometric facts needed +for this proof are rebuilt locally. Historical claims in #620 are credited +as research provenance, not silently promoted to accepted theorems. diff --git a/research/hurwitz-nonlinear-copy-floor/test_verify.py b/research/hurwitz-nonlinear-copy-floor/test_verify.py new file mode 100644 index 0000000000..1c3ad71648 --- /dev/null +++ b/research/hurwitz-nonlinear-copy-floor/test_verify.py @@ -0,0 +1,109 @@ +"""Independent arithmetic/decoder checks and artifact failure controls.""" + +from fractions import Fraction +from itertools import combinations +from pathlib import Path +import shutil +import subprocess +import sys +import tempfile +import unittest + +import verify as v + + +def fraction_rank(matrix): + """Column-space basis insertion, independent of the integer row engine.""" + basis = {} + for column in zip(*matrix): + column = list(map(Fraction, column)) + for pivot in sorted(basis): + factor = column[pivot] + column = [x - factor * y for x, y in zip(column, basis[pivot])] + pivot = next((i for i, value in enumerate(column) if value), None) + if pivot is not None: + factor = column[pivot] + basis[pivot] = [value / factor for value in column] + return len(basis) + + +class IndependentChecks(unittest.TestCase): + def test_fraction_column_engine_checks_all_geometric_obligations(self): + _, data = v.geometry(v.e8_roots()) + bases = data["basis_rows"] + checked = 0 + for a in bases: + for b in bases: + matrix = [[sum(x * y for x, y in zip(row, col)) for col in b] + for row in a] + self.assertEqual(v.rank(matrix), fraction_rank(matrix)) + checked += 1 + for a, b in combinations(bases, 2): + self.assertEqual(fraction_rank(a + b), 8) + checked += 1 + self.assertEqual(checked, 145) + + def test_explicit_inverse_decodes_nonlinear_examples(self): + checked = 0 + for n, width in ((10, 1), (4, 2)): + code = v.broadcast_code(n, width) + for x, transmitted in zip(v.states(code.widths), code.messages[0].outputs): + bits = [(transmitted >> i) & 1 for i in range(n // 2 * width)] + if bits[0] and bits[1]: + bits[2] = 1 - bits[2] + for pair_index, (a, b) in enumerate(code.pairs): + parity = sum(bits[pair_index * width + k] * 2 ** k + for k in range(width)) + self.assertEqual(parity ^ x[b], x[a]) + self.assertEqual(parity ^ x[a], x[b]) + checked += 1 + self.assertEqual(checked, 1280) + + def test_all_four_port_one_bit_encoders_fail(self): + # Exhaust all 2^16 truth tables, including nonlinear encoders, for + # four independent one-bit inputs. Everyone receives the one bit. + # A receiver knows just its mate; its two desired values must have + # disjoint sets of observed outputs at each fixed side-information bit. + masks = {} + for t in range(4): + mate = 3 - t + masks[t] = [[sum(1 << x for x in range(16) + if (x >> t) & 1 == target and (x >> mate) & 1 == side) + for target in range(2)] for side in range(2)] + + def can_decode(table, t): + for zero, one in masks[t]: + a, b = table & zero, table & one + if not ((a == 0 and b == one) or (a == zero and b == 0)): + return False + return True + + first_receiver = [table for table in range(1 << 16) if can_decode(table, 0)] + self.assertEqual(len(first_receiver), 4) + self.assertEqual([table for table in first_receiver + if all(can_decode(table, t) for t in range(4))], []) + + def test_relocated_receipt_and_tamper_rejection_in_optimized_mode(self): + with tempfile.TemporaryDirectory() as tmp: + root = Path(tmp) + for name in ("verify.py", "SOURCES.json", "RESULTS.json"): + shutil.copyfile(v.HERE / name, root / name) + command = [sys.executable, "-I", "-O", "-B", str(root / "verify.py")] + clean = subprocess.run(command, cwd=root.parent, text=True, capture_output=True) + self.assertEqual(clean.returncode, 0, clean.stderr) + self.assertIn("PASS_HURWITZ_NONLINEAR_COPY", clean.stdout) + original = (root / "RESULTS.json").read_bytes() + (root / "RESULTS.json").write_bytes(original.replace(b'"cost": 10', b'"cost": 9', 1)) + bad_receipt = subprocess.run(command, cwd=root.parent, text=True, capture_output=True) + self.assertNotEqual(bad_receipt.returncode, 0) + self.assertIn("committed receipt differs", bad_receipt.stderr) + (root / "RESULTS.json").write_bytes(original) + with (root / "SOURCES.json").open("a") as stream: + stream.write("\n") + bad_sources = subprocess.run(command, cwd=root.parent, text=True, capture_output=True) + self.assertNotEqual(bad_sources.returncode, 0) + self.assertIn("committed receipt differs", bad_sources.stderr) + + +if __name__ == "__main__": + unittest.main() diff --git a/research/hurwitz-nonlinear-copy-floor/verify.py b/research/hurwitz-nonlinear-copy-floor/verify.py new file mode 100644 index 0000000000..f58178c50a --- /dev/null +++ b/research/hurwitz-nonlinear-copy-floor/verify.py @@ -0,0 +1,344 @@ +#!/usr/bin/env python3 +"""Exact, solver-free replay; standard library; checks survive python -O. + +Prepared by Alexander Templeton with substantial OpenAI Codex assistance. +Apache-2.0. See PROOF.md for the all-width argument and pricing premise. +""" + +import argparse +from dataclasses import dataclass, replace +from hashlib import sha256 +from itertools import combinations, product +import json +from math import gcd +from pathlib import Path + + +HERE = Path(__file__).resolve().parent + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def rank(rows): + """Rational rank via integer row operations and primitive row reduction.""" + a = [list(row) for row in rows] + if not a: + return 0 + require(len({len(row) for row in a}) == 1, "ragged matrix") + r = 0 + for col in range(len(a[0])): + pivot = next((i for i in range(r, len(a)) if a[i][col]), None) + if pivot is None: + continue + a[r], a[pivot] = a[pivot], a[r] + for i in range(r + 1, len(a)): + if a[i][col]: + p, f = a[r][col], a[i][col] + a[i] = [p * x - f * y for x, y in zip(a[i], a[r])] + divisor = 0 + for value in a[i]: + divisor = gcd(divisor, value) + if divisor: + a[i] = [value // divisor for value in a[i]] + r += 1 + if r == len(a): + break + return r + + +def dot(x, y): + return sum(a * b for a, b in zip(x, y)) + + +def left_basis(v): + rows = [[], [], [], []] + for start in (0, 4): + a, b, c, d = v[start:start + 4] + for row, block in zip(rows, ((a, b, c, d), (-b, a, -d, c), + (-c, d, a, -b), (-d, -c, b, a))): + row.extend(block) + return tuple(tuple(row) for row in rows) + + +def e8_roots(): + roots = [] + for i, j in combinations(range(8), 2): + for x, y in product((-2, 2), repeat=2): + v = [0] * 8 + v[i], v[j] = x, y + roots.append(tuple(v)) + roots.extend(v for v in product((-1, 1), repeat=8) if v.count(-1) % 2 == 0) + return sorted(roots) + + +def geometry(roots): + require(len(roots) == len(set(roots)) == 240, "root cardinality") + lines = {} + for v in roots: + require(len(v) == 8 and dot(v, v) == 8, "root norm") + basis = left_basis(v) + require([[dot(x, y) for y in basis] for x in basis] == + [[8 * (i == j) for j in range(4)] for i in range(4)], + "quaternion basis Gram") + # The basis has Gram 8I, so this is exactly eight times its projector. + key = tuple(sum(row[i] * row[j] for row in basis) + for i in range(8) for j in range(8)) + lines.setdefault(key, []).append(v) + require(len(lines) == 10, "line count") + require({len(v) for v in lines.values()} == {24}, "line root counts") + bases = [left_basis(min(lines[key])) for key in sorted(lines)] + mates = [] + pairing_ranks = [] + for i, a in enumerate(bases): + ranks = [rank([[dot(x, y) for y in b] for x in a]) for b in bases] + require(ranks[i] == 4 and ranks.count(0) == 1 and ranks.count(4) == 9, + "singleton pairing ranks") + mates.append(ranks.index(0)) + pairing_ranks.append(ranks) + pairs = [(i, j) for i, j in enumerate(mates) if i < j] + check_pairs(10, pairs) + for i, j in combinations(range(10), 2): + require(rank(bases[i] + bases[j]) == 8, "two-line span") + return pairs, { + "root_count": 240, + "line_count": 10, + "roots_per_line": 24, + "basis_rows": bases, + "mate_pairs": pairs, + "singleton_pairing_ranks": pairing_ranks, + "two_line_spans_checked": 45, + } + + +def check_pairs(n, pairs): + require(n > 0 and n % 2 == 0, "positive even port count") + require(sorted(t for pair in pairs for t in pair) == list(range(n)), + "perfect matching") + require(all(len(pair) == 2 and pair[0] != pair[1] for pair in pairs), + "matching pair") + + +def transversals(pairs): + return [sum(1 << t for t in choice) for choice in product(*pairs)] + + +def charge(readers, sources, pairs): + if not readers or not sources: + return 0 + if readers.bit_count() == sources.bit_count() == 1: + if any({readers, sources} == {1 << i, 1 << j} for i, j in pairs): + return 0 + return 1 if min(readers.bit_count(), sources.bit_count()) == 1 else 2 + + +def local_certificate(n, pairs, ts=None, denominator=None): + check_pairs(n, pairs) + expected_ts = transversals(pairs) + ts = expected_ts if ts is None else ts + denominator = 1 << (n // 2 - 1) if denominator is None else denominator + require(sorted(ts) == sorted(expected_ts), "transversal list") + require(all(sum(bool(t & (1 << i)) for t in ts) == denominator + for i in range(n)), "unit vertex coverage") + hit = [sum(1 << i for i, t in enumerate(ts) if mask & t) + for mask in range(1 << n)] + counts = [0, 0, 0] + maximum_hits = [0, 0, 0] + for readers in range(1 << n): + for sources in range(1 << n): + c = charge(readers, sources, pairs) + both = (hit[readers] & hit[sources]).bit_count() + require(both <= denominator * c, "local weighted inequality") + counts[c] += 1 + maximum_hits[c] = max(maximum_hits[c], both) + return {"support_pairs": (1 << n) ** 2, "transversal_masks": ts, + "weight": f"1/{denominator}", "charge_counts": counts, + "maximum_hits_by_charge": maximum_hits} + + +@dataclass(frozen=True) +class Message: + sources: int + readers: int + width: int + outputs: tuple + + +@dataclass(frozen=True) +class Code: + widths: tuple + pairs: tuple + messages: tuple + + +def states(widths): + return list(product(*(range(1 << b) for b in widths))) + + +def selected(state, mask): + return tuple(x for i, x in enumerate(state) if mask & (1 << i)) + + +def single_valued(table, key, value, reason): + require(key not in table or table[key] == value, reason) + table[key] = value + + +def audit_code(code, extra_side_information=False): + n = len(code.widths) + check_pairs(n, code.pairs) + require(all(type(b) is int and b >= 0 for b in code.widths), "input width") + xs = states(code.widths) + all_mask = (1 << n) - 1 + for msg in code.messages: + require(type(msg.width) is int and msg.width >= 0, "message width") + require(0 <= msg.sources <= all_mask and 0 <= msg.readers <= all_mask, + "support domain") + require(len(msg.outputs) == len(xs), "truth table size") + observed = {} + for x, y in zip(xs, msg.outputs): + require(type(y) is int and 0 <= y < (1 << msg.width), + "message alphabet") + single_valued(observed, selected(x, msg.sources), y, + "undeclared source dependency") + mates = {a: b for a, b in code.pairs for a, b in ((a, b), (b, a))} + for t in range(n): + observed = {} + for index, x in enumerate(xs): + side = selected(x, all_mask ^ (1 << t)) if extra_side_information else (x[mates[t]],) + view = side + tuple(msg.outputs[index] for msg in code.messages + if msg.readers & (1 << t)) + single_valued(observed, view, x[t], "decoder collision") + cost = sum(msg.width * charge(msg.readers, msg.sources, code.pairs) + for msg in code.messages) + cut_states = 0 + if not extra_side_information: + for t in transversals(code.pairs): + observed = {} + relevant = [msg for msg in code.messages if msg.readers & t and msg.sources & t] + require(sum(code.widths[i] for i in range(n) if t & (1 << i)) <= + sum(msg.width for msg in relevant), "cut capacity") + for index, x in enumerate(xs): + key = selected(x, all_mask ^ t) + tuple(msg.outputs[index] for msg in relevant) + single_valued(observed, key, selected(x, t), "transcript collision") + cut_states += 1 + require(cost >= sum(code.widths), "copy floor") + return {"widths": list(code.widths), "states": len(xs), "messages": len(code.messages), + "cost": cost, "floor": sum(code.widths), "cut_states": cut_states} + + +def broadcast_code(n, width): + pairs = tuple((i, n - 1 - i) for i in range(n // 2)) + xs = states((width,) * n) + outputs = [] + for x in xs: + z = sum((x[a] ^ x[b]) << (i * width) for i, (a, b) in enumerate(pairs)) + # Toffoli is its own inverse; the third bit changes by the first two's AND. + z ^= ((z & 1) & ((z >> 1) & 1)) << 2 + outputs.append(z) + mask = (1 << n) - 1 + return Code((width,) * n, pairs, (Message(mask, mask, n // 2 * width, tuple(outputs)),)) + + +def nonlinear_witness(code): + lookup = dict(zip(states(code.widths), code.messages[0].outputs)) + zero = (0,) * len(code.widths) + units = [] + for i, b in enumerate(code.widths): + for bit in range(b): + x = [0] * len(code.widths) + x[i] = 1 << bit + units.append(tuple(x)) + for a, b in combinations(units, 2): + ab = tuple(x ^ y for x, y in zip(a, b)) + if lookup[zero] ^ lookup[a] ^ lookup[b] ^ lookup[ab]: + return {"a": a, "b": b, "nonzero_second_difference": + lookup[zero] ^ lookup[a] ^ lookup[b] ^ lookup[ab]} + raise ValueError("expected genuinely nonlinear encoder") + + +def reject(name, action, expected): + try: + action() + except ValueError as error: + require(str(error) == expected, f"{name}: wrong rejection: {error}") + return name + raise ValueError(f"negative control accepted: {name}") + + +def build_receipt(): + roots = e8_roots() + pairs, geo = geometry(roots) + local = local_certificate(10, pairs) + binary = broadcast_code(10, 1) + vector = broadcast_code(4, 2) + # A mate-only transmission has zero charge and cannot help a transversal. + vector_xs = states(vector.widths) + vector = replace(vector, messages=vector.messages + + (Message(1 << 3, 1, 2, tuple(x[3] for x in vector_xs)),)) + widths = (0, 1, 2, 1) + unequal = Code(widths, ((0, 3), (1, 2)), tuple( + Message(1 << t, 1 << t, b, tuple(x[t] for x in states(widths))) + for t, b in enumerate(widths))) + examples = {} + for name, code in (("nonlinear_ten_ports", binary), ("nonlinear_vector_with_free_mate", vector), + ("unequal_width_direct", unequal)): + examples[name] = audit_code(code) + require(examples[name]["cost"] == examples[name]["floor"], "attainment") + if name != "unequal_width_direct": + examples[name]["nonlinear_witness"] = nonlinear_witness(code) + + def changed(**kwargs): + return replace(binary, messages=(replace(binary.messages[0], **kwargs),)) + + controls = [ + reject("duplicate_root", lambda: geometry(roots[:-1] + roots[:1]), "root cardinality"), + reject("wrong_root_norm", lambda: geometry([(1,) + (0,) * 7] + roots[1:]), "root norm"), + reject("nonmatching_mates", lambda: local_certificate(10, pairs[:-1]), "perfect matching"), + reject("omitted_transversal", lambda: local_certificate(10, pairs, transversals(pairs)[:-1]), "transversal list"), + reject("wrong_weight", lambda: local_certificate(10, pairs, denominator=17), "unit vertex coverage"), + reject("width_not_charged", lambda: audit_code(changed(width=1)), "message alphabet"), + reject("negative_width", lambda: audit_code(changed(width=-1)), "message width"), + reject("missing_source", lambda: audit_code(changed(sources=1022)), "undeclared source dependency"), + reject("missing_reader", lambda: audit_code(changed(readers=1022)), "decoder collision"), + reject("truncated_output", lambda: audit_code(changed(width=4, outputs=tuple(y & 15 for y in binary.messages[0].outputs))), "decoder collision"), + reject("altered_output", lambda: audit_code(changed(outputs=(1,) + binary.messages[0].outputs[1:])), "decoder collision"), + ] + # Outside the side-information premise, the claimed floor is false: + # one parity bit, known to all, suffices if every other input is free. + parity = changed(width=1, outputs=tuple(sum(x) % 2 for x in states(binary.widths))) + controls.append(reject("extra_side_information_not_granted", lambda: audit_code(parity), "decoder collision")) + boundary = audit_code(parity, extra_side_information=True) + require(boundary["cost"] == 2 < boundary["floor"] == 10, "boundary counterexample") + budgets = [] + for b, s in product((1, 2, 7), (1, 3, 5, 9, 31)): + deficit = (s - 1) * 40 * b - s * 40 * b + require(deficit == -40 * b, "Dfc identity") + budgets.append([b, s, deficit]) + sources_digest = sha256((HERE / "SOURCES.json").read_bytes()).hexdigest() + return {"schema": 1, "sources_manifest_sha256": sources_digest, + "geometry": geo, "local_certificate": local, "attaining_examples": examples, + "negative_controls": controls, "outside_model_extra_side_information": boundary, + "conditional_budget_examples_b_s_deficit": budgets, + "scope": "Fixed support, fixed width, zero error, independent inputs, q*c additive pricing; written all-width proof in PROOF.md"} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--write", type=Path, help="explicitly write a newly computed receipt") + parser.add_argument("--check", type=Path, default=HERE / "RESULTS.json") + args = parser.parse_args() + result = build_receipt() + encoded = json.dumps(result, indent=2, sort_keys=True) + "\n" + if args.write: + args.write.write_text(encoded) + else: + require(args.check.read_text() == encoded, "committed receipt differs") + print("PASS_HURWITZ_NONLINEAR_COPY: 1048576 support pairs; 3 attaining codes; " + "12 rejection controls; conditional floor 10b") + + +if __name__ == "__main__": + main()