From e374f75c9bfb625695a14c4e4daa621adb8008bd Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Tue, 27 Oct 2026 15:39:07 +0000 Subject: [PATCH] feat(research): certify A8 simplex COPY floor under side information Answer the second open question of #5299: on both #1248 sharp A8 simplex witnesses, every term has an induced Petersen plus (rank - 5) isolated lines or a rank-sized non-orthogonal set, so free orthogonal side information keeps the nine-term bill at 72. The exact independence bound alone gives 64, so the Petersen step is needed. No new kappa. --- .../README.md | 126 ++ .../RESULT.json | 1018 +++++++++++++++++ .../SOURCES.json | 60 + .../TASK.json | 81 ++ .../VERIFY.json | 21 + .../test_verify.py | 115 ++ .../verify.py | 330 ++++++ 7 files changed, 1751 insertions(+) create mode 100644 research/a8-simplex-side-information-floor/README.md create mode 100644 research/a8-simplex-side-information-floor/RESULT.json create mode 100644 research/a8-simplex-side-information-floor/SOURCES.json create mode 100644 research/a8-simplex-side-information-floor/TASK.json create mode 100644 research/a8-simplex-side-information-floor/VERIFY.json create mode 100644 research/a8-simplex-side-information-floor/test_verify.py create mode 100644 research/a8-simplex-side-information-floor/verify.py diff --git a/research/a8-simplex-side-information-floor/README.md b/research/a8-simplex-side-information-floor/README.md new file mode 100644 index 0000000000..c7d70700a6 --- /dev/null +++ b/research/a8-simplex-side-information-floor/README.md @@ -0,0 +1,126 @@ +# Orthogonal side information keeps the A8 simplex nine-term COPY floor at 72 + +**Finite certificate on two pinned witnesses; no new κ.** The selected record and frontier are unchanged. + +[a8-simplex-decoder-floor](../a8-simplex-decoder-floor/README.md) (#1248) proves that the A8 simplex +nine-term decoder on P120 has separate-term COPY cost at least 72 for every complex row shift, with two +explicit sharp witnesses. [a7-a1-nonlinear-copy-floor](../a7-a1-nonlinear-copy-floor/README.md) (#5299) +showed that two lemmas keep the A7+A1 floor at 72 against nonlinear messages, with and without free +orthogonal side information. Its second Open next question asks for the A8 case: Lemma 1 transfers at +once, and Lemma 2 needs its own witness search. This package runs that search. + +| Setting | Lower bound on the nine-term bill | Scope | +|---|---:|---| +| no reader side information | **72** | every complex shift (#5299 Lemma 1 with #1248's theorem) | +| readers know all orthogonal inputs | **72** | both #1248 sharp witnesses (finite certificate, this package) | +| same, independence bound only | 64 | both witnesses (exact maximum, a control) | + +Both certified bounds equal the linear invoice. On these two witnesses, nonlinear coding does not +undercut the linear invoice, and free orthogonal side information does not either. For d-bit blocks +each bound scales to `72d`. + +## Model + +The model is #1248's, unchanged. There are 120 E8 root lines in the A8 frame (36 pair roots +`e_a - e_b`, 84 triple roots `1_S - 1/3`). The binary pairing is `B_ij = 1` exactly when lines i and j are +orthogonal or equal. The readers are `Y_k = {j : r_jk != 0}`, and the decoder rows are +`D_i = 2(r_i - r_i,anchor)`. The anchor is coordinate 0, except that the active witness anchors row 0 at +coordinate 1. Term k reads rows `X_k = {i : D_ik != 0}` and is billed `rho_k = rank_F2 B[X_k, Y_k]`. The +nonlinear message model is #5299's. Term k sends `m_k = f_k(x restricted to X_k)`. Every reader `j` in +`Y_k` must recover `sum_{i in X_k} B_ij x_i` from `m_k` and its own side information. The cost is +`log2 |range f_k|`. + +## What is checked + +The lemmas are #5299's. They are used here as written premises, not re-proved: + +- **Lemma 1 (no side information).** An invertible `rho_k x rho_k` block `B[S,R]` with `S` in `X_k` and + `R` in `Y_k` forces `2^rho_k` message values. Summed over terms this is `sum_k rho_k`, at least 72 + for every shift by #1248. +- **Lemma 2 (orthogonal side information).** If reader j knows every input orthogonal to j, then only + readers in `X_k ∩ Y_k` need anything, and each needs exactly `x_j`. Term k becomes an index-coding + instance on the induced orthogonality graph of its demand lines `X_k ∩ Y_k`. Two certificates bound + its rate: an induced Petersen graph with m isolated lines has rate `5 + m` (Blasiak, Kleinberg and + Lubetzky, Fact 5.6(1), with #5299's isolated-receiver induction), and a set of r pairwise + non-orthogonal lines has rate r. + +[verify.py](verify.py) checks the SHA256 of the pinned predecessor `CERTIFICATE.json` and rebuilds the +model from coordinates. It does not import predecessor code. For both witnesses it checks all 14,400 +entries of `D T^t = 2G`, recomputes the invoices `0,9,9,9,9,9,9,9,9` and `1,8,9,9,9,9,9,9,9` from `B`, +and requires them to equal the pinned ones. Per term it then finds and checks: + +| Witness | Demand lines per term | Side-information certificates | Largest non-orthogonal set | +|---|---|---|---| +| dropped, `0,9^8` | 0, then 50 × 8 | 8 × (Petersen + 4) | 0, then 8 × 8 | +| nine-active, `1,8,9^7` | 1, 49, then 50 × 7 | 1 single line, Petersen + 3, 7 × (Petersen + 4) | 1, 7, then 7 × 8 | + +Each term also has an invertible fooling block of size `rho_k`. Both totals are 72 in both settings. + +The largest pairwise non-orthogonal set is computed exactly by branch and bound. Every rank-9 term has +one of size 8 only, and the rank-8 term one of size 7. The independence bound by itself therefore +certifies 64 on each witness. The Petersen step supplies the missing unit in every one of the 16 +nonempty high-rank terms. + +## What this does and does not cover + +It covers nonlinear and AND-containing message codes on #1248's fixed nine-term supports, for the +separate-term bill, and for the strongest natural side information at #1248's two sharp witnesses. + +It does **not** cover: + +- the side-information bound for *every* complex shift (Open next question 1); +- other A8 frames, punctures, masked exactness or shared COPY billing; +- receivers that combine several terms nonlinearly. + +The two rate lemmas are inherited written premises. The Petersen rate 5 is a cited published fact. No +independent human proof review or formal proof-kernel check is claimed. No supplier, physical circuit or +κ is claimed. The selected κ is unchanged. + +## Reproduce + +From the repository root, with Python 3.12 and the standard library: + +```sh +python3.12 -I -B research/a8-simplex-side-information-floor/verify.py +python3.12 -I -B research/a8-simplex-side-information-floor/test_verify.py +python3.12 -B scripts/research_package.py --package research/a8-simplex-side-information-floor +``` + +Expected markers (each script runs in well under a second): + +```text +PASS_A8_SIMPLEX_SIDE_INFORMATION_FLOOR roots=120 witnesses=2 no_side_info=72 orthogonal_side_info=72 independence_only=64 petersen_terms=16 certificate=e1b19301ed2e402d no_new_kappa +PASS_A8_SIMPLEX_SIDE_INFORMATION_CONTROLS rejected=12 +``` + +The default run is read-only. It compares the rebuild with the stored [RESULT.json](RESULT.json) and +re-checks the stored certificate exactly as given. `--write` regenerates the file explicitly. +`test_verify.py` runs twelve rejecting controls: + +- a singular fooling block, and a fooling line outside the term; +- swapped Petersen labels, an isolated line orthogonal to the witness, and a duplicated line; +- Petersen + 3 against rank 9, a non-independent set, and an independence-only claim on a rank-9 term; +- an invoice mismatch, a broken all-pairs identity, a tampered stored certificate, and a drifted + predecessor input. + +## Open next questions + +1. Does the orthogonal-side-information floor stay at 72 for **every** complex row shift of the A8 + simplex decoder? A first step is to list each line's support-reducing shifts and find, per term, the + largest demand set with neither a Petersen + (rank − 5) witness nor a rank-sized non-orthogonal set. + #5299 poses the same question for A7+A1. +2. Is the Petersen step forced, or would a different induced subgraph whose broadcast rate exceeds its + independence number also close the one-unit gap in each rank-9 term? A first step is to compare + fractional or LP index-coding bounds with the independence number on one 50-line demand graph. + +## Credit and provenance + +This package was produced by Nick Petalas. It answers the second Open next question of Mark (Matarener)'s +#5299 and reuses its two lemmas and certificate format. Philipp / mightyOil's #1248 supplies the A8 +simplex model, the every-shift floor 72 and both sharp witnesses. joaqcoo's #1224 supplies the +one-sided nine-term normal form. The Petersen broadcast rate is Blasiak, Kleinberg and Lubetzky's +published result, with the m=4 case certified in +[p112-characteristic-two-minrank](../p112-characteristic-two-minrank/README.md). The width pricing +premise is that of #888 and #785/#814. [SOURCES.json](SOURCES.json) pins every predecessor file at +the base commit. Only `CERTIFICATE.json` is a replay input. The new checker is separately written. +Apache-2.0. diff --git a/research/a8-simplex-side-information-floor/RESULT.json b/research/a8-simplex-side-information-floor/RESULT.json new file mode 100644 index 0000000000..9bc358311f --- /dev/null +++ b/research/a8-simplex-side-information-floor/RESULT.json @@ -0,0 +1,1018 @@ +{ + "orthogonal_pairs": 3780, + "petersen_terms": 16, + "root_lines": 120, + "schema_version": 1, + "witnesses": { + "dropped": { + "costs": [ + 0, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9 + ], + "independence_only_floor": 64, + "no_side_info_floor": 72, + "orthogonal_side_info_floor": 72, + "terms": [ + { + "demand_lines": 0, + "fooling_readers": [], + "fooling_sources": [], + "max_independent": [], + "rank": 0, + "sideinfo": { + "kind": "independent", + "lines": [] + }, + "sources": 0, + "term": 0 + }, + { + "demand_lines": 50, + "fooling_readers": [ + 0, + 8, + 9, + 10, + 11, + 12, + 13, + 14, + 36 + ], + "fooling_sources": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 8 + ], + "max_independent": [ + 0, + 8, + 9, + 10, + 11, + 12, + 13, + 14 + ], + "rank": 9, + "sideinfo": { + "isolated": [ + 0, + 8, + 9, + 10 + ], + "kind": "petersen+isolated", + "petersen": [ + 11, + 12, + 13, + 14, + 84, + 83, + 82, + 81, + 80, + 79 + ] + }, + "sources": 57, + "term": 1 + }, + { + "demand_lines": 50, + "fooling_readers": [ + 1, + 8, + 15, + 16, + 17, + 18, + 19, + 20, + 36 + ], + "fooling_sources": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 8 + ], + "max_independent": [ + 1, + 8, + 15, + 16, + 17, + 18, + 19, + 20 + ], + "rank": 9, + "sideinfo": { + "isolated": [ + 1, + 8, + 15, + 16 + ], + "kind": "petersen+isolated", + "petersen": [ + 17, + 18, + 19, + 20, + 99, + 98, + 97, + 96, + 95, + 94 + ] + }, + "sources": 57, + "term": 2 + }, + { + "demand_lines": 50, + "fooling_readers": [ + 2, + 9, + 15, + 21, + 22, + 23, + 24, + 25, + 37 + ], + "fooling_sources": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 9 + ], + "max_independent": [ + 2, + 9, + 15, + 21, + 22, + 23, + 24, + 25 + ], + "rank": 9, + "sideinfo": { + "isolated": [ + 2, + 9, + 15, + 21 + ], + "kind": "petersen+isolated", + "petersen": [ + 22, + 23, + 24, + 25, + 109, + 108, + 107, + 106, + 105, + 104 + ] + }, + "sources": 57, + "term": 3 + }, + { + "demand_lines": 50, + "fooling_readers": [ + 3, + 10, + 16, + 21, + 26, + 27, + 28, + 29, + 38 + ], + "fooling_sources": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 10 + ], + "max_independent": [ + 3, + 10, + 16, + 21, + 26, + 27, + 28, + 29 + ], + "rank": 9, + "sideinfo": { + "isolated": [ + 3, + 10, + 16, + 21 + ], + "kind": "petersen+isolated", + "petersen": [ + 26, + 27, + 28, + 29, + 115, + 114, + 113, + 112, + 111, + 110 + ] + }, + "sources": 57, + "term": 4 + }, + { + "demand_lines": 50, + "fooling_readers": [ + 4, + 11, + 17, + 22, + 26, + 30, + 31, + 32, + 39 + ], + "fooling_sources": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 11 + ], + "max_independent": [ + 4, + 11, + 17, + 22, + 26, + 30, + 31, + 32 + ], + "rank": 9, + "sideinfo": { + "isolated": [ + 4, + 11, + 17, + 22 + ], + "kind": "petersen+isolated", + "petersen": [ + 26, + 30, + 31, + 32, + 118, + 117, + 116, + 112, + 111, + 110 + ] + }, + "sources": 57, + "term": 5 + }, + { + "demand_lines": 50, + "fooling_readers": [ + 5, + 12, + 18, + 23, + 27, + 30, + 33, + 34, + 40 + ], + "fooling_sources": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 12 + ], + "max_independent": [ + 5, + 12, + 18, + 23, + 27, + 30, + 33, + 34 + ], + "rank": 9, + "sideinfo": { + "isolated": [ + 5, + 12, + 18, + 23 + ], + "kind": "petersen+isolated", + "petersen": [ + 27, + 30, + 33, + 34, + 119, + 117, + 116, + 114, + 113, + 110 + ] + }, + "sources": 57, + "term": 6 + }, + { + "demand_lines": 50, + "fooling_readers": [ + 6, + 13, + 19, + 24, + 28, + 31, + 33, + 35, + 41 + ], + "fooling_sources": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 13 + ], + "max_independent": [ + 6, + 13, + 19, + 24, + 28, + 31, + 33, + 35 + ], + "rank": 9, + "sideinfo": { + "isolated": [ + 6, + 13, + 19, + 24 + ], + "kind": "petersen+isolated", + "petersen": [ + 28, + 31, + 33, + 35, + 119, + 118, + 116, + 115, + 113, + 111 + ] + }, + "sources": 57, + "term": 7 + }, + { + "demand_lines": 50, + "fooling_readers": [ + 7, + 14, + 20, + 25, + 29, + 32, + 34, + 35, + 42 + ], + "fooling_sources": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 14 + ], + "max_independent": [ + 7, + 14, + 20, + 25, + 29, + 32, + 34, + 35 + ], + "rank": 9, + "sideinfo": { + "isolated": [ + 7, + 14, + 20, + 25 + ], + "kind": "petersen+isolated", + "petersen": [ + 29, + 32, + 34, + 35, + 119, + 118, + 117, + 115, + 114, + 112 + ] + }, + "sources": 57, + "term": 8 + } + ] + }, + "nine_active": { + "costs": [ + 1, + 8, + 9, + 9, + 9, + 9, + 9, + 9, + 9 + ], + "independence_only_floor": 64, + "no_side_info_floor": 72, + "orthogonal_side_info_floor": 72, + "terms": [ + { + "demand_lines": 1, + "fooling_readers": [ + 0 + ], + "fooling_sources": [ + 0 + ], + "max_independent": [ + 0 + ], + "rank": 1, + "sideinfo": { + "kind": "independent", + "lines": [ + 0 + ] + }, + "sources": 1, + "term": 0 + }, + { + "demand_lines": 49, + "fooling_readers": [ + 8, + 9, + 10, + 11, + 12, + 13, + 14, + 36 + ], + "fooling_sources": [ + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 8 + ], + "max_independent": [ + 8, + 9, + 10, + 11, + 12, + 13, + 14 + ], + "rank": 8, + "sideinfo": { + "isolated": [ + 8, + 9, + 10 + ], + "kind": "petersen+isolated", + "petersen": [ + 11, + 12, + 13, + 14, + 84, + 83, + 82, + 81, + 80, + 79 + ] + }, + "sources": 56, + "term": 1 + }, + { + "demand_lines": 50, + "fooling_readers": [ + 1, + 8, + 15, + 16, + 17, + 18, + 19, + 20, + 36 + ], + "fooling_sources": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 8 + ], + "max_independent": [ + 1, + 8, + 15, + 16, + 17, + 18, + 19, + 20 + ], + "rank": 9, + "sideinfo": { + "isolated": [ + 1, + 8, + 15, + 16 + ], + "kind": "petersen+isolated", + "petersen": [ + 17, + 18, + 19, + 20, + 99, + 98, + 97, + 96, + 95, + 94 + ] + }, + "sources": 57, + "term": 2 + }, + { + "demand_lines": 50, + "fooling_readers": [ + 2, + 9, + 15, + 21, + 22, + 23, + 24, + 25, + 37 + ], + "fooling_sources": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 9 + ], + "max_independent": [ + 2, + 9, + 15, + 21, + 22, + 23, + 24, + 25 + ], + "rank": 9, + "sideinfo": { + "isolated": [ + 2, + 9, + 15, + 21 + ], + "kind": "petersen+isolated", + "petersen": [ + 22, + 23, + 24, + 25, + 109, + 108, + 107, + 106, + 105, + 104 + ] + }, + "sources": 57, + "term": 3 + }, + { + "demand_lines": 50, + "fooling_readers": [ + 3, + 10, + 16, + 21, + 26, + 27, + 28, + 29, + 38 + ], + "fooling_sources": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 10 + ], + "max_independent": [ + 3, + 10, + 16, + 21, + 26, + 27, + 28, + 29 + ], + "rank": 9, + "sideinfo": { + "isolated": [ + 3, + 10, + 16, + 21 + ], + "kind": "petersen+isolated", + "petersen": [ + 26, + 27, + 28, + 29, + 115, + 114, + 113, + 112, + 111, + 110 + ] + }, + "sources": 57, + "term": 4 + }, + { + "demand_lines": 50, + "fooling_readers": [ + 4, + 11, + 17, + 22, + 26, + 30, + 31, + 32, + 39 + ], + "fooling_sources": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 11 + ], + "max_independent": [ + 4, + 11, + 17, + 22, + 26, + 30, + 31, + 32 + ], + "rank": 9, + "sideinfo": { + "isolated": [ + 4, + 11, + 17, + 22 + ], + "kind": "petersen+isolated", + "petersen": [ + 26, + 30, + 31, + 32, + 118, + 117, + 116, + 112, + 111, + 110 + ] + }, + "sources": 57, + "term": 5 + }, + { + "demand_lines": 50, + "fooling_readers": [ + 5, + 12, + 18, + 23, + 27, + 30, + 33, + 34, + 40 + ], + "fooling_sources": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 12 + ], + "max_independent": [ + 5, + 12, + 18, + 23, + 27, + 30, + 33, + 34 + ], + "rank": 9, + "sideinfo": { + "isolated": [ + 5, + 12, + 18, + 23 + ], + "kind": "petersen+isolated", + "petersen": [ + 27, + 30, + 33, + 34, + 119, + 117, + 116, + 114, + 113, + 110 + ] + }, + "sources": 57, + "term": 6 + }, + { + "demand_lines": 50, + "fooling_readers": [ + 6, + 13, + 19, + 24, + 28, + 31, + 33, + 35, + 41 + ], + "fooling_sources": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 13 + ], + "max_independent": [ + 6, + 13, + 19, + 24, + 28, + 31, + 33, + 35 + ], + "rank": 9, + "sideinfo": { + "isolated": [ + 6, + 13, + 19, + 24 + ], + "kind": "petersen+isolated", + "petersen": [ + 28, + 31, + 33, + 35, + 119, + 118, + 116, + 115, + 113, + 111 + ] + }, + "sources": 57, + "term": 7 + }, + { + "demand_lines": 50, + "fooling_readers": [ + 7, + 14, + 20, + 25, + 29, + 32, + 34, + 35, + 42 + ], + "fooling_sources": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 14 + ], + "max_independent": [ + 7, + 14, + 20, + 25, + 29, + 32, + 34, + 35 + ], + "rank": 9, + "sideinfo": { + "isolated": [ + 7, + 14, + 20, + 25 + ], + "kind": "petersen+isolated", + "petersen": [ + 29, + 32, + 34, + 35, + 119, + 118, + 117, + 115, + 114, + 112 + ] + }, + "sources": 57, + "term": 8 + } + ] + } + } +} diff --git a/research/a8-simplex-side-information-floor/SOURCES.json b/research/a8-simplex-side-information-floor/SOURCES.json new file mode 100644 index 0000000000..103601b6ba --- /dev/null +++ b/research/a8-simplex-side-information-floor/SOURCES.json @@ -0,0 +1,60 @@ +{ + "schema_version": 1, + "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "files": [ + { + "path": "research/a8-simplex-decoder-floor/CERTIFICATE.json", + "usage": "input", + "git_blob": "ec2719c2eb185e3cef404e7ba05e6e09c0e62fda", + "sha256": "2ccf0a99b19fd977f473f63bbb46fc9bb35afb3284b1d11ae3e4633971374e3e" + }, + { + "path": "research/a8-simplex-decoder-floor/verify.py", + "usage": "provenance", + "git_blob": "4284e401804cfeb62402782f20467d4290a19a11", + "sha256": "57cb0895aacab5bb0acf951fb6b1a80fd876ee069f1249bac2bcb5076876b56e" + }, + { + "path": "research/a8-simplex-decoder-floor/PROOF.md", + "usage": "provenance", + "git_blob": "4d1d3bcd8799c833dfbb63ed5319af5fe863fa1a", + "sha256": "7e3a5407fc535fd9cc7f25f06aab787b0216f09121e571938cccedb383aab3c4" + }, + { + "path": "research/a8-simplex-decoder-floor/README.md", + "usage": "provenance", + "git_blob": "cc814ae890f18da884b70ae6e471f31a75bade5f", + "sha256": "4f279ea113cea46593609cdcd580099c24ec8aa02428aae0c5bae54baa0e4557" + }, + { + "path": "research/a7-a1-nonlinear-copy-floor/README.md", + "usage": "provenance", + "git_blob": "d4623185896227e4248e2623578848ad90ad7ec6", + "sha256": "516d38653c1a8f08aa99dd024d00276d4abdd7cbd5934d158296e9cf88606729" + }, + { + "path": "research/a7-a1-nonlinear-copy-floor/verify.py", + "usage": "provenance", + "git_blob": "e9ba80be421861aec873c45dbd7eee0d6db10d3e", + "sha256": "a1245bb0548c76c3ce3c5018ec872b88767a3074abfd28eebf13db7a8d145d57" + }, + { + "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": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8", + "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + } + ] +} diff --git a/research/a8-simplex-side-information-floor/TASK.json b/research/a8-simplex-side-information-floor/TASK.json new file mode 100644 index 0000000000..895db42781 --- /dev/null +++ b/research/a8-simplex-side-information-floor/TASK.json @@ -0,0 +1,81 @@ +{ + "schema_version": 1, + "task_id": "complex-rank-shape-decoder", + "priority_revision": 8, + "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "original_card": { + "id": "complex-rank-shape-decoder", + "question": "Can a legal decoder or coframe change improve the full signed moment, including changed helper targets?", + "starting_points": [ + "docs/research/current-priorities.md", + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "docs/research/recursive-invoice-preflight.md" + ], + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "acceptance_gate": "A source-bound arbitrary-input identity and legal producer/consumer boundary with the complete paid and productive target invoice, including restoration, ownership, native alignment and extra charges. Price under the actual current model; historical ceiling.py assumptions must be established before use. A favorable optimistic relaxation keeps a route open but is not a completed supplier. A scoped local result remains useful; expansion requires the family-level budget gate.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "first_experiment": "Price one complete changed itinerary with both paid and productive histograms. Check #5693/#5698 for overlap and their exact hypotheses before another coframe search. Use the signed invoice preflight where its boundary contract agrees; an inconclusive concave comparison is not a power crossing. Stop if an optimistic complete budget fails at the chosen target or native delivery remains unspecified.", + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "allowed_variations": [ + "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes." + ], + "scope_change_triggers": [ + "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.", + "Treating an archived proposal or local numerical pass as complete supplier admission." + ], + "overlap_terms": [ + "coframe", + "signed moment", + "5693", + "5698" + ], + "existing_checks": [ + { + "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "status": "reviewed", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Does the sharp A8 simplex nine-term COPY floor 72 of research/a8-simplex-decoder-floor (#1248) survive arbitrary nonlinear zero-error messages with the same fixed supports, without and with free orthogonal side information at the readers, on #1248's two pinned sharp witnesses?", + "scope_change_reason": "PR #5299 (research/a7-a1-nonlinear-copy-floor) poses this as its second Open next question: its no-side-information lemma transfers at once and its side-information lemma needs a separate A8 witness search. This package supplies that search; it does not synthesize a decoder or profile.", + "bottleneck_link": "Side result: no new kappa. Removes nonlinear message coding and free orthogonal side information as routes to cheaper COPY on the two sharp A8 simplex witnesses.", + "budget_minutes": 60, + "stop_rule": "Stop after 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 A8 model, binds both pinned sharp witnesses to the predecessor CERTIFICATE.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; the exact independence bound alone totals 64; test_verify.py has twelve rejecting controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Does the orthogonal-side-information floor stay at 72 for every complex row shift of the A8 simplex decoder, not only the two sharp witnesses?", + "why_it_matters": "With free orthogonal side information a small demand graph can let even a linear code fall below its term's pairing rank; a shift with small supports would then change the copy contract.", + "blocked_by": "Needs a deficiency argument for broadcast rates of induced orthogonality subgraphs over the full shift family, analogous to #1248's 43,435-plane census.", + "first_step": "For each line list its support-reducing shifts and compute, per term, the largest demand set with no Petersen+(rank-5) witness and no rank-sized non-orthogonal set." + }, + { + "question": "Is the Petersen step forced for every rank-9 term, or would a different small induced subgraph with broadcast rate above its independence number also serve?", + "why_it_matters": "Each 50-line rank-9 demand graph has largest non-orthogonal set 8, so the plain independence bound loses one unit per term; a catalogue of rate-above-independence subgraphs would make side-information certificates portable to other frames.", + "blocked_by": "No such catalogue for the E8 orthogonality graph is checked here.", + "first_step": "Enumerate induced subgraphs of one 50-line demand graph up to symmetry and compare fractional-clique-cover or LP bounds with the independence number." + } + ] +} diff --git a/research/a8-simplex-side-information-floor/VERIFY.json b/research/a8-simplex-side-information-floor/VERIFY.json new file mode 100644 index 0000000000..46ed49d647 --- /dev/null +++ b/research/a8-simplex-side-information-floor/VERIFY.json @@ -0,0 +1,21 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/a8-simplex-decoder-floor/CERTIFICATE.json" + ], + "commands": [ + { + "argv": ["{python}", "-I", "-B", "{package}/verify.py"], + "timeout_seconds": 120, + "checks": "Pinned predecessor CERTIFICATE.json hash; rebuilt 120-line A8 simplex model; both #1248 sharp witnesses satisfy D T^t = 2G and reproduce invoices (0,9^8) and (1,8,9^7); per term an invertible fooling block of size rho_k (no side information), an induced Petersen+(rho_k-5) witness or rho_k-line non-orthogonal set (orthogonal side information), and the exact largest non-orthogonal set; totals 72, 72 and 64 on each witness; stored RESULT.json equals the rebuild and is re-checked as given." + }, + { + "argv": ["{python}", "-I", "-B", "{package}/test_verify.py"], + "timeout_seconds": 120, + "checks": "Twelve rejecting controls: singular fooling block, fooling line outside the term, Petersen labels swapped, isolated line orthogonal to the witness, duplicated witness line, Petersen+3 against rank 9, non-independent set, independence-only claim on a rank-9 term, invoice mismatch, broken all-pairs identity, tampered stored certificate, drifted predecessor input." + } + ] +} diff --git a/research/a8-simplex-side-information-floor/test_verify.py b/research/a8-simplex-side-information-floor/test_verify.py new file mode 100644 index 0000000000..ca9fc40852 --- /dev/null +++ b/research/a8-simplex-side-information-floor/test_verify.py @@ -0,0 +1,115 @@ +"""Rejecting controls for the A8 simplex side-information certificate.""" +import copy +import hashlib +import json +import sys +from pathlib import Path + +HERE = Path(__file__).resolve().parent +sys.path.insert(0, str(HERE)) +import verify # noqa: E402 + + +def rejected(call): + try: + call() + except SystemExit as exc: + if str(exc).startswith("FAIL: "): + return + raise + raise AssertionError("control unexpectedly accepted") + + +def main(): + rr, gram, pairing, orth, readers = verify.model() + stored = json.loads((HERE / "RESULT.json").read_text(encoding="utf-8")) + d3 = verify.decoder(rr, True) + sources, costs = verify.invoice(d3, pairing, readers) + rows = stored["witnesses"]["nine_active"]["terms"] + k = 2 + demand = sources[k] & readers[k] + + def check(bad_rows, bad_costs=costs): + return lambda: verify.check_terms(pairing, orth, sources, readers, bad_costs, bad_rows) + + controls = 0 + verify.check_terms(pairing, orth, sources, readers, costs, rows) # positive control + + # 1. Singular fooling block: replace one source by a line in the span of the others. + bad = copy.deepcopy(rows) + S, R = bad[k]["fooling_sources"], bad[k]["fooling_readers"] + block = [sum(pairing[i][j] << t for t, j in enumerate(R)) for i in S[:-1]] + swap = next(i for i in sorted(sources[k]) if i not in S + and verify.f2_rank(block + [sum(pairing[i][j] << t for t, j in enumerate(R))]) < len(S)) + S[-1] = swap + rejected(check(bad)); controls += 1 + + # 2. Fooling source outside the term. + bad = copy.deepcopy(rows) + bad[k]["fooling_sources"][0] = next(i for i in range(verify.N) if i not in sources[k]) + rejected(check(bad)); controls += 1 + + # 3. Petersen labels swapped across an edge and a non-edge. + bad = copy.deepcopy(rows) + pet = bad[k]["sideinfo"]["petersen"] + pet[0], pet[2] = pet[2], pet[0] + rejected(check(bad)); controls += 1 + + # 4. Isolated line orthogonal to a Petersen vertex. + bad = copy.deepcopy(rows) + info = bad[k]["sideinfo"] + info["isolated"][0] = next(c for c in sorted(demand) + if c not in info["petersen"] + info["isolated"] + and orth[c][info["petersen"][0]]) + rejected(check(bad)); controls += 1 + + # 5. Duplicated witness line. + bad = copy.deepcopy(rows) + info = bad[k]["sideinfo"] + info["isolated"][1] = info["isolated"][0] + rejected(check(bad)); controls += 1 + + # 6. Too few isolated lines for the rank (Petersen + 3 against rank 9). + bad = copy.deepcopy(rows) + bad[k]["sideinfo"]["isolated"].pop() + rejected(check(bad)); controls += 1 + + # 7. "Independent" set containing an orthogonal pair. + bad = copy.deepcopy(rows) + lines = bad[k]["max_independent"] + lines[0] = next(c for c in sorted(demand) if c not in lines and orth[c][lines[1]]) + rejected(check(bad)); controls += 1 + + # 8. Independence alone cannot certify a rank-9 term: claiming it is rejected. + bad = copy.deepcopy(rows) + alpha = bad[k]["max_independent"] + bad[k]["sideinfo"] = {"kind": "independent", "lines": alpha + [alpha[0]]} + rejected(check(bad)); controls += 1 + + # 9. Wrong invoice: a raised cost on one term is not bound to its row. + bad_costs = list(costs) + bad_costs[0] += 1 + rejected(check(copy.deepcopy(rows), bad_costs)); controls += 1 + + # 10. A non-constant change to one decoder row breaks the all-pairs identity. + broken = list(d3) + broken[0] = tuple(x + (1 if t == 0 else 0) for t, x in enumerate(broken[0])) + rejected(lambda: verify.require(verify.exact(broken, rr, gram), "identity")); controls += 1 + + # 11. Tampered stored certificate is caught by the stored re-check. + bad = copy.deepcopy(stored) + bad["witnesses"]["dropped"]["terms"][3]["sideinfo"]["petersen"].reverse() + rejected(lambda: verify.recheck(bad)); controls += 1 + + # 12. Drifted predecessor input bytes fail the pinned SHA256. + entry = next(r for r in json.loads((HERE / "SOURCES.json").read_text(encoding="utf-8"))["files"] + if r["usage"] == "input") + real = (verify.ROOT / entry["path"]).read_bytes() + rejected(lambda: verify.require(hashlib.sha256(real + b" ").hexdigest() == entry["sha256"], + "input drift")); controls += 1 + + print("PASS_A8_SIMPLEX_SIDE_INFORMATION_CONTROLS rejected=%d" % controls) + + +if __name__ == "__main__": + main() diff --git a/research/a8-simplex-side-information-floor/verify.py b/research/a8-simplex-side-information-floor/verify.py new file mode 100644 index 0000000000..8b434f128a --- /dev/null +++ b/research/a8-simplex-side-information-floor/verify.py @@ -0,0 +1,330 @@ +"""Orthogonal side information keeps the A8 simplex nine-term COPY floor at 72. + +Standard library only. Rebuilds the 120 E8 root lines in the A8 simplex +frame of research/a8-simplex-decoder-floor (#1248), its two pinned sharp +shift witnesses, and 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: an induced + "Petersen + (rho_k - 5) isolated" subgraph of the orthogonality + graph on the term's demand lines (broadcast rate rho_k), or a + pairwise non-orthogonal set of size rho_k (independence bound). + +It also computes, by exact branch and bound, the largest pairwise +non-orthogonal set in every demand graph. That independence bound alone +certifies only 64 on each witness, so the Petersen step is needed. + +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" / "a8-simplex-decoder-floor" +N = 120 + + +def require(condition, message): + if not condition: + raise SystemExit("FAIL: " + message) + + +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 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 roots(): + """A8 realization, scaled by 3: 36 pair roots e_a-e_b, 84 triple roots 1_S-1/3.""" + rows = [] + for a, b in itertools.combinations(range(9), 2): + rows.append(tuple(3 if k == a else -3 if k == b else 0 for k in range(9))) + for subset in itertools.combinations(range(9), 3): + rows.append(tuple(2 if k in subset else -1 for k in range(9))) + return rows + + +def model(): + rr = roots() + require(len(rr) == N and all(sum(r) == 0 and dot(r, r) == 18 for r in rr), "A8 root model") + gram = [[dot(x, y) for y in rr] for x in rr] + require(all(g % 9 == 0 for row in gram for g in row), "integral Gram") + # B_ij = 1 iff the true inner product is even: orthogonal or the same line. + pairing = [[(g // 9 + 1) % 2 for g in row] for row in gram] + orth = [[i != j and gram[i][j] == 0 for j in range(N)] for i in range(N)] + readers = [frozenset(j for j in range(N) if rr[j][k]) for k in range(9)] + return rr, gram, pairing, orth, readers + + +def decoder(rr, active): + """#1248 witness: D_i = 2(r_i - r_i[anchor]) (scaled by 3); row 0 anchors at 1 when active.""" + return [tuple(2 * (x - r[1 if active and i == 0 else 0]) for x in r) for i, r in enumerate(rr)] + + +def exact(d3, rr, gram): + # D T^t = 2G with D = d3/3 and T = r/3. + return all(dot(d3[i], rr[j]) == 2 * gram[i][j] for i in range(N) for j in range(N)) + + +def invoice(d3, pairing, readers): + sources = [frozenset(i for i in range(N) if d3[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).""" + 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) + + +def masks(orth): + full = (1 << N) - 1 + on = [sum(1 << j for j in range(N) if orth[i][j]) for i in range(N)] + off = [full ^ on[i] ^ (1 << i) for i in range(N)] + return on, off + + +def members(mask): + while mask: + low = mask & -mask + yield low.bit_length() - 1 + mask ^= low + + +def to_mask(lines): + return sum(1 << i for i in lines) + + +KNESER = list(itertools.combinations(range(5), 2)) +ADJ = [[not set(KNESER[a]) & set(KNESER[b]) for b in range(10)] for a in range(10)] + + +def petersen_in(on, off, pool): + """Induced Petersen (edges = orthogonal pairs) inside the bitmask pool, or None.""" + assign = [] + + def bt(t, rest): + if t == 10: + return list(assign) + allowed = rest + for u in range(t): + allowed &= on[assign[u]] if ADJ[u][t] else off[assign[u]] + for line in members(allowed): + assign.append(line) + found = bt(t + 1, rest & ~(1 << line)) + if found: + return found + assign.pop() + return None + return bt(0, pool) + + +def petersen_witness(on, off, demand, extra): + """`extra` pairwise non-orthogonal lines, then an induced Petersen among the + demand lines non-orthogonal to all of them. Returns (petersen, isolated).""" + def bt(isolated, cand, common): + if len(isolated) == extra: + found = petersen_in(on, off, common) + return (found, isolated) if found else None + for line in members(cand): + cand &= ~(1 << line) + found = bt(isolated + [line], cand & off[line], common & off[line] & ~(1 << line)) + if found: + return found + return None + pool = to_mask(demand) + return bt([], pool, pool) + + +def max_independent(off, demand): + """Exact largest pairwise non-orthogonal set inside demand (branch and bound).""" + best = [] + + def bt(chosen, cand): + nonlocal best + if len(chosen) + cand.bit_count() <= len(best): + return + if not cand: + best = list(chosen) + return + for line in list(members(cand)): + if len(chosen) + cand.bit_count() <= len(best): + return + bt(chosen + [line], cand & off[line]) + cand &= ~(1 << line) + bt([], to_mask(demand)) + return sorted(best) + + +def check_petersen(orth, demand, petersen, isolated): + lines = petersen + isolated + require(len(petersen) == 10 and len(isolated) <= 4, "witness shape") + require(len(set(lines)) == len(lines) and set(lines) <= demand, "witness inside the term") + for a, b in itertools.combinations(range(10), 2): + require(orth[petersen[a]][petersen[b]] == ADJ[a][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 check_independent(orth, demand, lines, rho): + require(len(lines) == rho and len(set(lines)) == rho and set(lines) <= demand, "independent support") + require(not any(orth[a][b] for a, b in itertools.combinations(lines, 2)), "independent non-orthogonal") + return rho + + +def term_certificates(pairing, orth, sources, readers, costs): + on, off = masks(orth) + 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 + alpha = max_independent(off, demand) + row = {"term": k, "rank": rho, "sources": len(src), "demand_lines": len(demand), + "fooling_sources": S, "fooling_readers": R, "max_independent": alpha} + if len(alpha) >= rho: + row["sideinfo"] = {"kind": "independent", "lines": alpha[:rho]} + else: + require(rho >= 5, "term %d needs a Petersen witness" % k) + found = petersen_witness(on, off, 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]} + out.append(row) + return out + + +def check_terms(pairing, orth, sources, readers, costs, rows): + fool, side, indep = [], [], [] + 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] + indep.append(check_independent(orth, demand, row["max_independent"], len(row["max_independent"]))) + info = row["sideinfo"] + if info["kind"] == "petersen+isolated": + side.append(check_petersen(orth, demand, info["petersen"], info["isolated"])) + else: + require(info["kind"] == "independent", "certificate kind") + side.append(check_independent(orth, demand, info["lines"], costs[k])) + 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), sum(indep) + + +def source_witnesses(): + pinned_inputs() + data = json.loads((PRED / "CERTIFICATE.json").read_text(encoding="utf-8")) + require(data["sharp_cost"] == 72, "pinned sharp cost") + return {"dropped": (False, data["dropped_witness_costs"]), + "nine_active": (True, data["active_witness_costs"])} + + +def result(): + rr, gram, pairing, orth, readers = model() + require(all(f2_rank(sum(pairing[i][j] << j for j in readers[k]) for i in range(N)) == 9 + for k in range(9)), "reader supports have full pairing rank") + out = {"schema_version": 1, "root_lines": N, "petersen_terms": 0, + "orthogonal_pairs": sum(orth[i][j] for i in range(N) for j in range(i)), + "witnesses": {}} + for name, (active, pinned_costs) in source_witnesses().items(): + d3 = decoder(rr, active) + require(exact(d3, rr, gram), name + " all-pairs identity") + sources, costs = invoice(d3, pairing, readers) + require(costs == pinned_costs, name + " invoice equals pinned predecessor") + rows = term_certificates(pairing, orth, sources, readers, costs) + fool, side, indep = check_terms(pairing, orth, sources, readers, costs, rows) + require(fool == side == 72, name + " totals") + require(indep == 64, name + " independence bound alone gives 64") + 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, + "independence_only_floor": indep, "terms": rows} + return out + + +def recheck(stored): + """Re-check the stored certificate itself, not only its regeneration.""" + rr, gram, pairing, orth, readers = model() + for name, (active, _) in source_witnesses().items(): + sources, costs = invoice(decoder(rr, active), pairing, readers) + fool, side, indep = check_terms(pairing, orth, sources, readers, costs, + stored["witnesses"][name]["terms"]) + require(fool == side == 72 and indep == 64, name + " stored totals") + + +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") + recheck(stored) + digest = hashlib.sha256(json.dumps(evidence, sort_keys=True).encode()).hexdigest()[:16] + print("PASS_A8_SIMPLEX_SIDE_INFORMATION_FLOOR roots=120 witnesses=2 no_side_info=72 " + "orthogonal_side_info=72 independence_only=64 petersen_terms=%d certificate=%s no_new_kappa" + % (evidence["petersen_terms"], digest)) + + +if __name__ == "__main__": + main()