diff --git a/research/a7-a1-nonlinear-copy-floor/README.md b/research/a7-a1-nonlinear-copy-floor/README.md new file mode 100644 index 0000000000..d462318589 --- /dev/null +++ b/research/a7-a1-nonlinear-copy-floor/README.md @@ -0,0 +1,110 @@ +# Nonlinear messages keep the A7+A1 nine-term COPY floor at 72 + +**Scoped negative result; no new κ.** The selected record and frontier are unchanged. + +[a7-a1-decoder-floor](../a7-a1-decoder-floor/README.md) proves that the A7+A1 nine-normal decoder of +[PR1224](https://github.com/CrocSwap/integer-mult-bounds/pull/1224) has separate-term COPY cost at least 72 +for every complex row shift. Its scope list says that arbitrary nonlinear decoder architectures are +outside that theorem. This package closes the nearest such case. It keeps the nine fixed term supports +and lets every term send an **arbitrary deterministic zero-error message**, for example one built with +AND gates. Each message is priced by its width in bits, the explicit pricing premise of +[gaussian-nonlinear-copy-floor](../gaussian-nonlinear-copy-floor/README.md) (#888) and #785/#814. + +| Setting | Lower bound on the nine-term bill | Scope | +|---|---:|---| +| no reader side information | **72** (in general `sum rho_k`) | every complex shift (written lemma) | +| readers know all orthogonal inputs | **72** | both pinned sharp witnesses (finite certificates) | + +Both bounds equal the linear invoice. So nonlinear coding cannot undercut it, and on the two sharp +witnesses free orthogonal side information cannot either. For d-bit blocks every bound scales to `72d`. + +## Model + +The model is inherited from a7-a1-decoder-floor without change. There are 120 E8 root lines with +`B_ij = 1` exactly when lines i and j are orthogonal or equal. The reader supports are +`Y_k = {j : T_jk != 0}` and the row supports are `X_k = {i : D_ik != 0}`. Term k is billed +`rho_k = rank_F2 B[X_k, Y_k]`. A nonlinear term k is a map `m_k = f_k(x restricted to X_k)` with finite +range. Every reader `j` in `Y_k` must recover its term value `sum_{i in X_k} B_ij x_i` from `m_k` and +from its own side information. The cost is `log2 |range f_k|`. + +## Proofs + +**Lemma 1 (no side information, every shift).** Choose `rho_k` rows S of X_k and `rho_k` readers R of Y_k +with `B[S,R]` invertible over F2. Set all inputs outside S to zero. The `2^rho_k` assignments on S then +give pairwise different value vectors on R. Each of these vectors is a function of `m_k`, so `m_k` takes +at least `2^rho_k` values. Summing over the terms gives `sum_k rho_k >= 72` for every shift, by the +predecessor's theorem. ∎ + +**Lemma 2 (orthogonal side information).** Suppose reader j knows `x_i` for every line i orthogonal to j. +Then a reader outside `X_k` already knows its term value. A reader j inside `X_k ∩ Y_k` needs exactly `x_j`. +Fix the inputs outside `X_k` to zero. Term k is then an index-coding instance on the induced orthogonality +graph `G[X_k ∩ Y_k]`. An induced subgraph only lowers the zero-error rate, and two lower bounds apply: + +- *Petersen plus m isolated lines* gives `5d + md`. Petersen's broadcast rate is 5 + ([Blasiak, Kleinberg and Lubetzky, Fact 5.6(1)](https://www.cs.cornell.edu/~ablasiak/papers/bkl-beta.pdf); + [p112-characteristic-two-minrank](../p112-characteristic-two-minrank/README.md) certifies the m=4 case, + which gives 9d). Each isolated receiver v adds d: `H(M) = I(M; x_v) + H(M | x_v) >= d + H(M | x_v)`, + and for each value of `x_v` the message is still a valid code for the rest. Induction on m finishes it. +- *A set of r pairwise non-orthogonal lines* gives `rd`: its receivers have no side information about + one another. + +The checker finds a certificate equal to `rho_k` in every term of both pinned witnesses: + +| Witness (predecessor RESULT.json) | Invoice | Certificates | +|---|---|---| +| eight-active, `t_i = -x_i0` | `0,9,9,9,9,9,9,9,9` | 8 × (Petersen + 4) | +| nine-active (one row changed) | `1,8,9,9,9,9,9,9,9` | 1 non-orthogonal line, Petersen + 3, 7 × (Petersen + 4) | + +The demand graphs have 50–57 lines. Both totals are 72. ∎ + +## What this does and does not cover + +It covers nonlinear and AND-containing message codes on the predecessor's fixed nine-term supports, +for the separate-term bill and for the strongest natural side information at the two sharp witnesses. + +It does **not** cover: + +- other decoder architectures, changed normals, punctures, masked exactness or shared COPY billing; +- receivers that combine several terms nonlinearly instead of using separate-term values; +- the side-information bound for *every* complex shift (see the open question below). + +With side information even a linear code can fall below `rho_k` on a small demand graph. A shift that +undercuts 72 under side information would therefore change the copy contract; it would not be a +nonlinear effect. No supplier, physical circuit or κ is claimed. The selected κ is unchanged. + +## Reproduce + +From the repository root, Python 3.12 and the standard library: + +```sh +python3.12 -I -B research/a7-a1-nonlinear-copy-floor/verify.py +python3.12 -I -B research/a7-a1-nonlinear-copy-floor/test_verify.py +python3.12 -B scripts/research_package.py --package research/a7-a1-nonlinear-copy-floor +``` + +Expected markers: + +```text +PASS_A7_A1_NONLINEAR_COPY_FLOOR roots=120 witnesses=2 no_side_info=72 orthogonal_side_info=72 petersen_terms=16 certificate=09a3e17032f727cb no_new_kappa +PASS_A7_A1_NONLINEAR_COPY_FLOOR_CONTROLS rejected=9 +``` + +`verify.py` checks the SHA256 of the pinned predecessor `RESULT.json` before reading it. It rebuilds the +120-line model and both shift witnesses and checks the all-pairs identity and the invoices against the +predecessor. It then rebuilds every fooling block and side-information witness, compares the result with +the stored [RESULT.json](RESULT.json), and re-checks the stored certificate exactly as given. +`--write` regenerates the file explicitly. The default run is read-only. `test_verify.py` runs nine +rejecting controls: a singular or misplaced fooling block, a broken Petersen edge, a non-isolated or +duplicated witness line, a clique too small for its rank, a changed shift, a tampered certificate and a +drifted predecessor input. + +## Open next questions + +- Does the orthogonal-side-information floor stay at 72 for **every** complex row shift? A first step is + to list each line's few support-reducing shifts (`t_i` in `{0, -x_ik}`) and find, per term, the largest + demand graph that lacks a Petersen + (rank − 5) witness. +- The same two lemmas apply verbatim to the A8 simplex nine-term floor + ([a8-simplex-decoder-floor](../a8-simplex-decoder-floor/README.md), #1248). Lemma 1 transfers at once; + Lemma 2 needs its own witness search. + +Prepared by Mark (Matarener) with substantial Claude Code (Claude) assistance. diff --git a/research/a7-a1-nonlinear-copy-floor/RESULT.json b/research/a7-a1-nonlinear-copy-floor/RESULT.json new file mode 100644 index 0000000000..fc3a594a50 --- /dev/null +++ b/research/a7-a1-nonlinear-copy-floor/RESULT.json @@ -0,0 +1,852 @@ +{ + "orthogonal_pairs": 3780, + "petersen_terms": 16, + "root_lines": 120, + "schema_version": 1, + "witnesses": { + "eight_active": { + "costs": [ + 0, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9 + ], + "no_side_info_floor": 72, + "orthogonal_side_info_floor": 72, + "terms": [ + { + "demand_lines": 0, + "fooling_readers": [], + "fooling_sources": [], + "rank": 0, + "sideinfo": { + "kind": "empty" + }, + "sources": 0, + "term": 0 + }, + { + "demand_lines": 51, + "fooling_readers": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 13, + 15 + ], + "fooling_sources": [ + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 13, + 46 + ], + "rank": 9, + "sideinfo": { + "isolated": [ + 13, + 47, + 48, + 49 + ], + "kind": "petersen+isolated", + "petersen": [ + 1, + 2, + 3, + 46, + 53, + 57, + 89, + 65, + 88, + 87 + ] + }, + "sources": 57, + "term": 1 + }, + { + "demand_lines": 51, + "fooling_readers": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 12, + 15 + ], + "fooling_sources": [ + 0, + 2, + 3, + 4, + 5, + 6, + 7, + 12, + 30 + ], + "rank": 9, + "sideinfo": { + "isolated": [ + 12, + 31, + 32, + 33 + ], + "kind": "petersen+isolated", + "petersen": [ + 0, + 2, + 3, + 30, + 37, + 41, + 89, + 65, + 99, + 98 + ] + }, + "sources": 57, + "term": 2 + }, + { + "demand_lines": 51, + "fooling_readers": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 11, + 15 + ], + "fooling_sources": [ + 0, + 1, + 3, + 4, + 5, + 6, + 7, + 11, + 22 + ], + "rank": 9, + "sideinfo": { + "isolated": [ + 11, + 23, + 24, + 25 + ], + "kind": "petersen+isolated", + "petersen": [ + 0, + 1, + 3, + 22, + 29, + 41, + 88, + 57, + 99, + 107 + ] + }, + "sources": 57, + "term": 3 + }, + { + "demand_lines": 51, + "fooling_readers": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 10, + 15 + ], + "fooling_sources": [ + 0, + 1, + 2, + 4, + 5, + 6, + 7, + 10, + 18 + ], + "rank": 9, + "sideinfo": { + "isolated": [ + 10, + 19, + 20, + 21 + ], + "kind": "petersen+isolated", + "petersen": [ + 0, + 1, + 2, + 18, + 29, + 37, + 87, + 53, + 98, + 107 + ] + }, + "sources": 57, + "term": 4 + }, + { + "demand_lines": 51, + "fooling_readers": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 9, + 15 + ], + "fooling_sources": [ + 0, + 1, + 2, + 3, + 5, + 6, + 7, + 9, + 16 + ], + "rank": 9, + "sideinfo": { + "isolated": [ + 9, + 17, + 20, + 21 + ], + "kind": "petersen+isolated", + "petersen": [ + 0, + 1, + 2, + 16, + 29, + 37, + 86, + 53, + 97, + 106 + ] + }, + "sources": 57, + "term": 5 + }, + { + "demand_lines": 51, + "fooling_readers": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 8, + 15 + ], + "fooling_sources": [ + 0, + 1, + 2, + 3, + 4, + 6, + 7, + 8, + 15 + ], + "rank": 9, + "sideinfo": { + "isolated": [ + 8, + 17, + 19, + 21 + ], + "kind": "petersen+isolated", + "petersen": [ + 0, + 1, + 2, + 15, + 29, + 37, + 85, + 53, + 96, + 105 + ] + }, + "sources": 57, + "term": 6 + }, + { + "demand_lines": 51, + "fooling_readers": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 15 + ], + "fooling_sources": [ + 0, + 1, + 2, + 3, + 4, + 5, + 7, + 8, + 15 + ], + "rank": 9, + "sideinfo": { + "isolated": [ + 7, + 16, + 18, + 21 + ], + "kind": "petersen+isolated", + "petersen": [ + 0, + 1, + 2, + 15, + 28, + 36, + 84, + 52, + 95, + 104 + ] + }, + "sources": 57, + "term": 7 + }, + { + "demand_lines": 57, + "fooling_readers": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 14, + 15 + ], + "fooling_sources": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 14, + 15 + ], + "rank": 9, + "sideinfo": { + "isolated": [ + 4, + 5, + 6, + 14 + ], + "kind": "petersen+isolated", + "petersen": [ + 0, + 1, + 2, + 3, + 26, + 34, + 38, + 50, + 54, + 62 + ] + }, + "sources": 57, + "term": 8 + } + ] + }, + "nine_active": { + "costs": [ + 1, + 8, + 9, + 9, + 9, + 9, + 9, + 9, + 9 + ], + "no_side_info_floor": 72, + "orthogonal_side_info_floor": 72, + "terms": [ + { + "demand_lines": 1, + "fooling_readers": [ + 0 + ], + "fooling_sources": [ + 13 + ], + "rank": 1, + "sideinfo": { + "kind": "independent", + "lines": [ + 13 + ] + }, + "sources": 1, + "term": 0 + }, + { + "demand_lines": 50, + "fooling_readers": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 15 + ], + "fooling_sources": [ + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 46 + ], + "rank": 8, + "sideinfo": { + "isolated": [ + 47, + 48, + 49 + ], + "kind": "petersen+isolated", + "petersen": [ + 1, + 2, + 3, + 46, + 53, + 57, + 89, + 65, + 88, + 87 + ] + }, + "sources": 56, + "term": 1 + }, + { + "demand_lines": 51, + "fooling_readers": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 12, + 15 + ], + "fooling_sources": [ + 0, + 2, + 3, + 4, + 5, + 6, + 7, + 12, + 30 + ], + "rank": 9, + "sideinfo": { + "isolated": [ + 12, + 31, + 32, + 33 + ], + "kind": "petersen+isolated", + "petersen": [ + 0, + 2, + 3, + 30, + 37, + 41, + 89, + 65, + 99, + 98 + ] + }, + "sources": 57, + "term": 2 + }, + { + "demand_lines": 51, + "fooling_readers": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 11, + 15 + ], + "fooling_sources": [ + 0, + 1, + 3, + 4, + 5, + 6, + 7, + 11, + 22 + ], + "rank": 9, + "sideinfo": { + "isolated": [ + 11, + 23, + 24, + 25 + ], + "kind": "petersen+isolated", + "petersen": [ + 0, + 1, + 3, + 22, + 29, + 41, + 88, + 57, + 99, + 107 + ] + }, + "sources": 57, + "term": 3 + }, + { + "demand_lines": 51, + "fooling_readers": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 10, + 15 + ], + "fooling_sources": [ + 0, + 1, + 2, + 4, + 5, + 6, + 7, + 10, + 18 + ], + "rank": 9, + "sideinfo": { + "isolated": [ + 10, + 19, + 20, + 21 + ], + "kind": "petersen+isolated", + "petersen": [ + 0, + 1, + 2, + 18, + 29, + 37, + 87, + 53, + 98, + 107 + ] + }, + "sources": 57, + "term": 4 + }, + { + "demand_lines": 51, + "fooling_readers": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 9, + 15 + ], + "fooling_sources": [ + 0, + 1, + 2, + 3, + 5, + 6, + 7, + 9, + 16 + ], + "rank": 9, + "sideinfo": { + "isolated": [ + 9, + 17, + 20, + 21 + ], + "kind": "petersen+isolated", + "petersen": [ + 0, + 1, + 2, + 16, + 29, + 37, + 86, + 53, + 97, + 106 + ] + }, + "sources": 57, + "term": 5 + }, + { + "demand_lines": 51, + "fooling_readers": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 8, + 15 + ], + "fooling_sources": [ + 0, + 1, + 2, + 3, + 4, + 6, + 7, + 8, + 15 + ], + "rank": 9, + "sideinfo": { + "isolated": [ + 8, + 17, + 19, + 21 + ], + "kind": "petersen+isolated", + "petersen": [ + 0, + 1, + 2, + 15, + 29, + 37, + 85, + 53, + 96, + 105 + ] + }, + "sources": 57, + "term": 6 + }, + { + "demand_lines": 51, + "fooling_readers": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 15 + ], + "fooling_sources": [ + 0, + 1, + 2, + 3, + 4, + 5, + 7, + 8, + 15 + ], + "rank": 9, + "sideinfo": { + "isolated": [ + 7, + 16, + 18, + 21 + ], + "kind": "petersen+isolated", + "petersen": [ + 0, + 1, + 2, + 15, + 28, + 36, + 84, + 52, + 95, + 104 + ] + }, + "sources": 57, + "term": 7 + }, + { + "demand_lines": 57, + "fooling_readers": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 14, + 15 + ], + "fooling_sources": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 14, + 15 + ], + "rank": 9, + "sideinfo": { + "isolated": [ + 4, + 5, + 6, + 14 + ], + "kind": "petersen+isolated", + "petersen": [ + 0, + 1, + 2, + 3, + 26, + 34, + 38, + 50, + 54, + 62 + ] + }, + "sources": 57, + "term": 8 + } + ] + } + } +} diff --git a/research/a7-a1-nonlinear-copy-floor/SOURCES.json b/research/a7-a1-nonlinear-copy-floor/SOURCES.json new file mode 100644 index 0000000000..a1be615238 --- /dev/null +++ b/research/a7-a1-nonlinear-copy-floor/SOURCES.json @@ -0,0 +1,42 @@ +{ + "schema_version": 1, + "base_commit": "ff3cc58e370d0f678e529246f8c73e8094e18fcf", + "files": [ + { + "path": "research/a7-a1-decoder-floor/RESULT.json", + "usage": "input", + "git_blob": "709bdea7ddb37c17330c5b48a5ff2e813d949fe8", + "sha256": "db01b040fa361bba0eb8878d8528ba958c6502e66a44498adacb6a704a486b40" + }, + { + "path": "research/a7-a1-decoder-floor/verify.py", + "usage": "provenance", + "git_blob": "cc7d686671cd94fc476ecbcb341ce011dc91ba49", + "sha256": "29158aeb3aa79ce2bd0fe02addf95207b6005c446d1aa3d400dd949ea445ca46" + }, + { + "path": "research/a7-a1-decoder-floor/README.md", + "usage": "provenance", + "git_blob": "c6f3649af2bb2d91f10127b89eabb3a3c007f166", + "sha256": "b05e08146efb393415aad940a7cb4566fa63a9e37138e06ff8e9ea06e04cd476" + }, + { + "path": "research/p112-characteristic-two-minrank/README.md", + "usage": "provenance", + "git_blob": "387df8b87d0ec68bba74b3d5f2f8854a36db2f06", + "sha256": "dcc2081314205d42ac29c022bf7f83be06449eb756feab1ccdc96dfbcf395510" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395", + "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375" + } + ] +} diff --git a/research/a7-a1-nonlinear-copy-floor/TASK.json b/research/a7-a1-nonlinear-copy-floor/TASK.json new file mode 100644 index 0000000000..14d67a582d --- /dev/null +++ b/research/a7-a1-nonlinear-copy-floor/TASK.json @@ -0,0 +1,72 @@ +{ + "schema_version": 1, + "task_id": "complex-rank-shape-decoder", + "priority_revision": 7, + "base_commit": "ff3cc58e370d0f678e529246f8c73e8094e18fcf", + "original_card": { + "id": "complex-rank-shape-decoder", + "question": "Can a decoder deliver the local paid mass in fewer, larger-rank children (block frame climbs instead of rank-1 to rank-3 steps)?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/complex-local-word-ceiling/README.md", + "research/complex-decoder-field-extension-seed44/README.md", + "research/complex-frame-pair-decoders/README.md", + "research/selected-k8-unrestricted-ends/README.md", + "research/eisenstein-reduction-copy-floor/README.md" + ], + "methods": [ + "Find one exact small decoding identity whose frame path climbs in blocks, and price its complete per-call profile.", + "Bound the best effective child rank achievable for one fixed support alphabet, including copies, frames and restoration." + ], + "acceptance_gate": "A per-call local profile, with all copied information, frames and restoration counted, whose ceiling exceeds the selected word's by at least 5%; masked or overcomplete supports must change an assumption of the eight-term all-pairs bound. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "research/complex-local-word-ceiling/verify.py" + ], + "expected": "PASS_COMPLEX_LOCAL_WORD_CEILING", + "inspect": "Read the selected word's per-call local profile, its packing ceiling and the lever table; run levers.py for the ideal budget of the lever you target.", + "scope": "Positive control and planning budget only; this is not a new construction or full cold replay." + }, + "first_experiment": "Before any synthesis, write the candidate per-call local profile (and centre charge / unpaid coordinates if changed) and screen it with ceiling.ceiling(); reject it if even the ideal ceiling does not beat the selected word's by your stated margin. Ideal budget: rank-16 delivery is 2.31x (levers.py).", + "bottleneck_link": "Rank-1 children are about half of recursive cost; the selected word's effective child rank is about 3.9. Larger-rank delivery lowers recursive cost per unit of paid mass.", + "allowed_variations": [ + "One masked, overcomplete or block decoder family with exact labels and supports.", + "A scoped lower bound on effective rank for one alphabet.", + "If the coverage law, template or guard changes, derive an applicable fully charged replacement bound instead of applying the incumbent ceiling outside its scope." + ], + "scope_change_triggers": [ + "Repacking idle remainders of an unchanged word (covered by the packing ceiling).", + "Repeating the eight-term all-pairs search inside its proved scope.", + "Only changing helper terminal subspaces and monotone frames within the fixed scalar word, entrances and cleanup contract already covered by #1995/#2013.", + "Searching below C=40 in the #2017 Eisenstein binary scalar-rectangle or fixed-support block-linear additive pairing model; specify a changed premise instead. This bound does not cover every complex decoder.", + "Continuing a partial cost improvement while leaving the same unpriced consumer, restoration or central-readout obligation unresolved; refresh the family expansion decision first. Local product-retiming evidence has a narrow scope and is not a ban on changed graphs or contracts." + ], + "overlap_terms": [ + "rank shape", + "block climb", + "masked decoder", + "overcomplete", + "effective rank" + ] + }, + "scope_status": "changed", + "actual_scope": "Does the sharp A7+A1 nine-term COPY floor 72 of research/a7-a1-decoder-floor (linear separate-term messages) survive arbitrary nonlinear zero-error messages with the same fixed supports, without and with free orthogonal side information at the readers?", + "scope_change_reason": "The predecessor lists arbitrary nonlinear decoder architectures as outside its theorem. This package keeps its fixed nine-term supports and asks only whether nonlinear (AND-containing) message codes, priced by message width, can undercut the linear invoice; it does not synthesize a new decoder or profile.", + "bottleneck_link": "Side result: no new kappa. Removes nonlinear message coding of fixed-support frame decoders as a route to cheaper COPY on this family.", + "budget_minutes": 120, + "stop_rule": "Stop after the written fibre lemma for every complex shift and finite side-information certificates on both pinned sharp witnesses; do not search all shift assignments under side information.", + "outcome": "negative-result", + "evidence": "verify.py rebuilds the model, binds both pinned sharp shift witnesses to the predecessor RESULT.json, and certifies per term an invertible fooling block of size rho_k and an induced Petersen+(rho_k-5) or rho_k-line non-orthogonal witness, totals 72 each; test_verify.py has nine rejecting controls.", + "author": "Mark (Matarener)", + "ai_assistance": "Prepared with substantial Claude Code (Claude) assistance.", + "open_questions": [ + { + "question": "Does the orthogonal-side-information floor stay at 72 for every complex row shift, not only the two sharp witnesses?", + "why_it_matters": "With free orthogonal side information even a linear code can fall below a term's pairing rank when its demand graph is small; a shift with small supports could then undercut 72, which would be a change of the copy contract rather than a nonlinear effect.", + "blocked_by": "Needs a deficiency argument for broadcast rates of induced orthogonality subgraphs over the row-shift family, analogous to the predecessor's 43,435-plane label census.", + "first_step": "For each line list its few support-reducing shifts (t_i in {0, -x_ik}) and compute, per term, the largest demand subgraph lacking a Petersen+(rank-5) witness." + } + ] +} diff --git a/research/a7-a1-nonlinear-copy-floor/VERIFY.json b/research/a7-a1-nonlinear-copy-floor/VERIFY.json new file mode 100644 index 0000000000..25f7d9e1c8 --- /dev/null +++ b/research/a7-a1-nonlinear-copy-floor/VERIFY.json @@ -0,0 +1,21 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/a7-a1-decoder-floor/RESULT.json" + ], + "commands": [ + { + "argv": ["{python}", "-I", "-B", "{package}/verify.py"], + "timeout_seconds": 120, + "checks": "Pinned predecessor input hash; rebuilt 120-line A7+A1 model; both pinned sharp shift witnesses satisfy the all-pairs identity and reproduce invoices (0,9^8) and (1,8,9^7); per term an invertible fooling block of size rho_k (no side information) and an induced Petersen+(rho_k-5) witness or rho_k-line non-orthogonal set (orthogonal side information); both totals 72; stored RESULT.json equals the rebuild and is re-checked as given." + }, + { + "argv": ["{python}", "-I", "-B", "{package}/test_verify.py"], + "timeout_seconds": 180, + "checks": "Rejecting controls: singular fooling block, fooling line outside the term, Petersen non-edge swapped, isolated line orthogonal to the witness, duplicated witness line, clique too small for its rank, invoice mismatch after a changed shift, tampered stored certificate, drifted predecessor input." + } + ] +} diff --git a/research/a7-a1-nonlinear-copy-floor/test_verify.py b/research/a7-a1-nonlinear-copy-floor/test_verify.py new file mode 100644 index 0000000000..3f7a999a85 --- /dev/null +++ b/research/a7-a1-nonlinear-copy-floor/test_verify.py @@ -0,0 +1,122 @@ +"""Rejecting controls for verify.py. Each mutation must raise SystemExit.""" +import copy +import json +import sys +from pathlib import Path + +HERE = Path(__file__).resolve().parent +sys.path.insert(0, str(HERE)) +import verify as V # noqa: E402 + +rr, pairing, orth, t16, readers = V.model() +shifts = V.source_shifts() +stored = json.loads((HERE / "RESULT.json").read_text(encoding="utf-8")) +eight, _ = shifts["eight_active"] +sources, costs = V.invoice(V.decoder(rr, eight), pairing, readers) +rows = stored["witnesses"]["eight_active"]["terms"] + + +def rejects(name, fn): + try: + fn() + except SystemExit as exc: + if not str(exc).startswith("FAIL"): + raise + return name + raise AssertionError("control accepted: " + name) + + +def mutated(edit): + r = copy.deepcopy(rows) + edit(r) + return lambda: V.check_terms(pairing, orth, sources, readers, costs, r) + + +def singular(r): + t = r[1] + t["fooling_sources"][1] = next(i for i in sorted(sources[1]) + if i not in t["fooling_sources"] + and pairing[i] == pairing[t["fooling_sources"][0]]) \ + if any(pairing[i] == pairing[t["fooling_sources"][0]] and i not in t["fooling_sources"] + for i in sources[1]) else t["fooling_sources"][0] + + +def outside(r): + r[1]["fooling_sources"][0] = next(i for i in range(120) if i not in sources[1]) + + +def nonedge(r): + p = r[2]["sideinfo"]["petersen"] + p[0], p[1] = p[1], p[0] # vertices 01 and 02 swap roles: edge pattern breaks + + +def isolated(r): + info = r[3]["sideinfo"] + demand = sources[3] & readers[3] + info["isolated"][0] = next(c for c in sorted(demand) + if c not in info["petersen"] + info["isolated"] + and any(orth[c][x] for x in info["petersen"])) + + +def duplicate(r): + info = r[4]["sideinfo"] + info["isolated"][1] = info["isolated"][0] + + +nine, _ = shifts["nine_active"] +n_sources, n_costs = V.invoice(V.decoder(rr, nine), pairing, readers) +n_rows = stored["witnesses"]["nine_active"]["terms"] + + +def bad_clique(): + r = copy.deepcopy(n_rows) + r[0]["sideinfo"]["lines"] = [next(iter(sorted(n_sources[0] & readers[0])))] * 1 + r[0]["rank"] = 2 + V.check_terms(pairing, orth, n_sources, readers, n_costs, r) + + +def changed_shift(): + s = list(eight) + s[5] += 3 + d4 = V.decoder(rr, s) + V.require(V.exact(d4, t16, rr), "identity") + src, cst = V.invoice(d4, pairing, readers) + V.require(cst == [0] + [9] * 8, "changed shift invoice equals pinned predecessor") + + +def tampered(): + t = copy.deepcopy(stored) + t["witnesses"]["eight_active"]["costs"][1] = 8 + V.require(t == json.loads(json.dumps(V.result())), "stored certificate mismatch") + + +def drifted(): + original = V.ROOT + try: + fake = HERE / "_drift" + target = fake / "research" / "a7-a1-decoder-floor" + target.mkdir(parents=True, exist_ok=True) + (target / "RESULT.json").write_text("{}", encoding="utf-8") + V.ROOT = fake + V.pinned_inputs() + finally: + V.ROOT = original + for p in sorted((HERE / "_drift").rglob("*"), reverse=True): + p.unlink() if p.is_file() else p.rmdir() + (HERE / "_drift").rmdir() + + +# Every stored row must pass before the controls mean anything. +V.check_terms(pairing, orth, sources, readers, costs, rows) +done = [ + rejects("singular fooling block", mutated(singular)), + rejects("fooling line outside the term", mutated(outside)), + rejects("Petersen non-edge swapped", mutated(nonedge)), + rejects("isolated line orthogonal to the witness", mutated(isolated)), + rejects("duplicated witness line", mutated(duplicate)), + rejects("clique too small for its rank", bad_clique), + rejects("changed shift breaks exactness or invoice", changed_shift), + rejects("tampered stored certificate", tampered), + rejects("drifted predecessor input", drifted), +] +print("PASS_A7_A1_NONLINEAR_COPY_FLOOR_CONTROLS rejected=%d" % len(done)) diff --git a/research/a7-a1-nonlinear-copy-floor/verify.py b/research/a7-a1-nonlinear-copy-floor/verify.py new file mode 100644 index 0000000000..e9ba80be42 --- /dev/null +++ b/research/a7-a1-nonlinear-copy-floor/verify.py @@ -0,0 +1,299 @@ +"""Nonlinear zero-error messages keep the A7+A1 nine-term COPY floor at 72. + +Standard library only. Rebuilds the 120 E8 root lines, A7+A1 readers and the +two pinned sharp shift witnesses of research/a7-a1-decoder-floor, then checks +two finite certificates per term: + + fooling rho_k source lines S and reader lines R inside the term with + B[S,R] invertible over F2 (any message, linear or not, needs + 2^rho_k values: no side information); + sideinfo readers know every orthogonal input: either an induced + "Petersen + (rho_k - 5) isolated" subgraph of the orthogonality + graph (broadcast rate rho_k; the rho=9 case is the 14-vertex + witness of p112-characteristic-two-minrank) or a pairwise + non-orthogonal set of size rho_k (independence bound). + +The stored RESULT.json must equal the rebuilt certificate. +""" +import argparse +import hashlib +import itertools +import json +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parent.parent +PRED = ROOT / "research" / "a7-a1-decoder-floor" + + +def pinned_inputs(): + """Every usage=input file must match its SOURCES.json SHA256 before use.""" + rows = json.loads((HERE / "SOURCES.json").read_text(encoding="utf-8"))["files"] + for row in rows: + if row["usage"] == "input": + data = (ROOT / row["path"]).read_bytes() + require(hashlib.sha256(data).hexdigest() == row["sha256"], "input drift: " + row["path"]) + + +def require(condition, message): + if not condition: + raise SystemExit("FAIL: " + message) + + +def canonical(vector): + first = next(x for x in vector if x) + return tuple(vector) if first > 0 else tuple(-x for x in vector) + + +def roots(): + # Same enumeration and ordering as research/a7-a1-decoder-floor/verify.py. + values = set() + for i, j in itertools.combinations(range(8), 2): + for a, b in itertools.product((-2, 2), repeat=2): + row = [0] * 8 + row[i], row[j] = a, b + values.add(canonical(row)) + for row in itertools.product((-1, 1), repeat=8): + if sum(x < 0 for x in row) % 2 == 0: + values.add(canonical(row)) + return sorted(values, reverse=True) + + +def dot(a, b): + return sum(x * y for x, y in zip(a, b)) + + +def f2_rank(rows): + pivots = {} + for value in rows: + while value: + top = value.bit_length() - 1 + if top in pivots: + value ^= pivots[top] + else: + pivots[top] = value + break + return len(pivots) + + +def model(): + rr = roots() + require(len(rr) == 120 and all(dot(x, x) == 8 for x in rr), "E8 root model") + # B_ij = 1 iff the true inner product is even: orthogonal or the same line. + pairing = [[(dot(x, y) // 4 + 1) % 2 for y in rr] for x in rr] + orth = [[i != j and dot(rr[i], rr[j]) == 0 for j in range(120)] for i in range(120)] + t16 = [[8 * r[k] - sum(r) for k in range(8)] + [4 * sum(r)] for r in rr] + readers = [frozenset(i for i in range(120) if t16[i][k]) for k in range(9)] + return rr, pairing, orth, t16, readers + + +def decoder(rr, shifts): + return [[4 * (r[k] + shifts[i]) for k in range(8)] + [sum(r)] for i, r in enumerate(rr)] + + +def exact(d4, t16, rr): + return all(dot(d4[i], t16[j]) == 32 * dot(rr[i], rr[j]) for i in range(120) for j in range(120)) + + +def invoice(d4, pairing, readers): + sources = [frozenset(i for i in range(120) if d4[i][k]) for k in range(9)] + costs = [] + for k in range(9): + rows = [sum(pairing[i][j] << j for j in readers[k]) for i in sorted(sources[k])] + costs.append(f2_rank(rows)) + return sources, costs + + +def fooling(pairing, src, rdr, rho): + """Greedy rho x rho invertible submatrix B[S,R]; returns sorted (S, R).""" + if rho == 0: + return [], [] + S, basis_rows = [], [] + for i in sorted(src): + row = sum(pairing[i][j] << j for j in rdr) + if f2_rank(basis_rows + [row]) > len(basis_rows): + S.append(i) + basis_rows.append(row) + require(len(S) == rho, "fooling sources reach the rank") + R = [] + for j in sorted(rdr): + cand = R + [j] + cols = [sum(pairing[i][c] << t for t, c in enumerate(cand)) for i in S] + if f2_rank(cols) == len(cand): + R = cand + require(len(R) == rho, "fooling readers reach the rank") + return S, R + + +def check_fooling(pairing, src, rdr, S, R): + """Distinct inputs on S give distinct reader vectors on R.""" + require(set(S) <= src and set(R) <= rdr and len(S) == len(R), "fooling support") + require(len(set(S)) == len(S) and len(set(R)) == len(R), "fooling repeats") + rows = [sum(pairing[i][j] << t for t, j in enumerate(R)) for i in S] + require(f2_rank(rows) == len(S), "fooling block invertible") + return len(S) + + +KNESER = list(itertools.combinations(range(5), 2)) + + +def petersen_witness(orth, S, extra=4): + """Induced Petersen (edges = orthogonal pairs) plus `extra` lines that are + pairwise non-orthogonal and non-orthogonal to all ten, inside S.""" + S = sorted(S) + assign = [] + + def bt(t): + if t == 10: + cand = [c for c in S if c not in assign and not any(orth[c][p] for p in assign)] + for quad in itertools.combinations(cand, extra): + if not any(orth[a][b] for a, b in itertools.combinations(quad, 2)): + return list(assign), list(quad) + return None + v = KNESER[t] + for line in S: + if line in assign: + continue + if all(orth[line][assign[u]] == (not set(KNESER[u]) & set(v)) for u in range(t)): + assign.append(line) + found = bt(t + 1) + if found: + return found + assign.pop() + return None + return bt(0) + + +def check_petersen(orth, S, petersen, isolated): + lines = petersen + isolated + require(len(petersen) == 10 and len(isolated) <= 4, "witness shape") + require(len(set(lines)) == len(lines) and set(lines) <= S, "witness inside the term") + for a, b in itertools.combinations(range(10), 2): + require(orth[petersen[a]][petersen[b]] == (not set(KNESER[a]) & set(KNESER[b])), + "Petersen adjacency") + for c in isolated: + require(not any(orth[c][x] for x in lines if x != c), "isolated vertex") + # Broadcast rate of Petersen is 5; isolated receivers add one each. + return 5 + len(isolated) + + +def clique(orth, S, size): + """Pairwise non-orthogonal set of the requested size inside S.""" + S = sorted(S) + + def bt(chosen, start): + if len(chosen) == size: + return list(chosen) + for t in range(start, len(S)): + c = S[t] + if not any(orth[c][x] for x in chosen): + found = bt(chosen + [c], t + 1) + if found: + return found + return None + return bt([], 0) + + +def check_clique(orth, S, lines, rho): + require(len(lines) == rho and len(set(lines)) == rho and set(lines) <= S, "clique support") + require(not any(orth[a][b] for a, b in itertools.combinations(lines, 2)), "clique non-orthogonal") + return rho + + +def term_certificates(pairing, orth, sources, readers, costs): + out = [] + for k in range(9): + src, rdr, rho = sources[k], readers[k], costs[k] + S, R = fooling(pairing, src, rdr, rho) + demand = src & rdr + row = {"term": k, "rank": rho, "sources": len(src), "demand_lines": len(demand), + "fooling_sources": S, "fooling_readers": R} + if rho >= 5: + found = petersen_witness(orth, demand, rho - 5) + require(found is not None, "Petersen witness in term %d" % k) + row["sideinfo"] = {"kind": "petersen+isolated", "petersen": found[0], "isolated": found[1]} + elif rho > 0: + found = clique(orth, demand, rho) + require(found is not None, "independent set in term %d" % k) + row["sideinfo"] = {"kind": "independent", "lines": found} + else: + row["sideinfo"] = {"kind": "empty"} + out.append(row) + return out + + +def check_terms(pairing, orth, sources, readers, costs, rows): + fool, side = [], [] + for k, row in enumerate(rows): + require(row["term"] == k and row["rank"] == costs[k], "term row binding") + fool.append(check_fooling(pairing, sources[k], readers[k], + row["fooling_sources"], row["fooling_readers"])) + demand = sources[k] & readers[k] + info = row["sideinfo"] + if info["kind"] == "petersen+isolated": + side.append(check_petersen(orth, demand, info["petersen"], info["isolated"])) + elif info["kind"] == "independent": + side.append(check_clique(orth, demand, info["lines"], costs[k])) + else: + require(info["kind"] == "empty" and costs[k] == 0, "empty term") + side.append(0) + require(fool == costs, "no-side-information bounds equal the linear invoice") + require(side == costs, "side-information bounds equal the linear invoice") + return sum(fool), sum(side) + + +def source_shifts(): + pinned_inputs() + data = json.loads((PRED / "RESULT.json").read_text(encoding="utf-8")) + w = data["witness"] + nine = list(w["row_shifts"]) + rr = roots() + eight = [-r[0] for r in rr] + idx = w["changed_root_index"] + require(rr[idx] == tuple(w["changed_root"]), "pinned changed root") + require(nine[:idx] + nine[idx + 1:] == eight[:idx] + eight[idx + 1:], "pinned shifts differ only at one row") + return {"eight_active": (eight, w["eight_active_costs"]), "nine_active": (nine, w["nine_active_costs"])} + + +def result(): + rr, pairing, orth, t16, readers = model() + out = {"schema_version": 1, "root_lines": 120, "petersen_terms": 0, + "orthogonal_pairs": sum(orth[i][j] for i in range(120) for j in range(i)), + "witnesses": {}} + for name, (shifts, pinned_costs) in source_shifts().items(): + d4 = decoder(rr, shifts) + require(exact(d4, t16, rr), name + " all-pairs identity") + sources, costs = invoice(d4, pairing, readers) + require(costs == pinned_costs, name + " invoice equals pinned predecessor") + rows = term_certificates(pairing, orth, sources, readers, costs) + fool, side = check_terms(pairing, orth, sources, readers, costs, rows) + require(fool == side == 72, name + " totals") + out["petersen_terms"] += sum(r["sideinfo"]["kind"] == "petersen+isolated" for r in rows) + out["witnesses"][name] = {"costs": costs, "no_side_info_floor": fool, + "orthogonal_side_info_floor": side, "terms": rows} + return out + + +def main(): + ap = argparse.ArgumentParser(description=__doc__) + ap.add_argument("--write", action="store_true", help="explicitly regenerate RESULT.json") + args = ap.parse_args() + evidence = result() + path = HERE / "RESULT.json" + if args.write: + path.write_text(json.dumps(evidence, indent=1, sort_keys=True) + "\n", encoding="utf-8") + else: + stored = json.loads(path.read_text(encoding="utf-8")) + require(stored == json.loads(json.dumps(evidence)), "stored certificate mismatch") + # Re-check the stored certificate itself, not only its regeneration. + rr, pairing, orth, t16, readers = model() + for name, (shifts, _) in source_shifts().items(): + sources, costs = invoice(decoder(rr, shifts), pairing, readers) + check_terms(pairing, orth, sources, readers, costs, stored["witnesses"][name]["terms"]) + digest = hashlib.sha256(json.dumps(evidence, sort_keys=True).encode()).hexdigest()[:16] + print("PASS_A7_A1_NONLINEAR_COPY_FLOOR roots=120 witnesses=2 no_side_info=72 " + "orthogonal_side_info=72 petersen_terms=%d certificate=" % evidence["petersen_terms"] + digest + " no_new_kappa") + + +if __name__ == "__main__": + main()