From d3d44a83a9c455c376cfa528baf243865343dca9 Mon Sep 17 00:00:00 2001 From: Cinna Davis <1337isnot1337@users.noreply.github.com> Date: Wed, 14 Oct 2026 11:20:57 -0500 Subject: [PATCH] Add exact local P112 gauge rank floors --- .../PROOF.md | 19 + .../README.md | 38 + .../RESULT.json | 2076 +++++++++++++++++ .../SOURCES.json | 72 + .../TASK.json | 74 + .../VERIFY.json | 26 + .../verify.py | 162 ++ 7 files changed, 2467 insertions(+) create mode 100644 research/coord-root-p112-local-tetrad-gauge-seed8232/PROOF.md create mode 100644 research/coord-root-p112-local-tetrad-gauge-seed8232/README.md create mode 100644 research/coord-root-p112-local-tetrad-gauge-seed8232/RESULT.json create mode 100644 research/coord-root-p112-local-tetrad-gauge-seed8232/SOURCES.json create mode 100644 research/coord-root-p112-local-tetrad-gauge-seed8232/TASK.json create mode 100644 research/coord-root-p112-local-tetrad-gauge-seed8232/VERIFY.json create mode 100644 research/coord-root-p112-local-tetrad-gauge-seed8232/verify.py diff --git a/research/coord-root-p112-local-tetrad-gauge-seed8232/PROOF.md b/research/coord-root-p112-local-tetrad-gauge-seed8232/PROOF.md new file mode 100644 index 0000000000..9491419dac --- /dev/null +++ b/research/coord-root-p112-local-tetrad-gauge-seed8232/PROOF.md @@ -0,0 +1,19 @@ +# Exact exterior-rank floor + +Let `b_0,...,b_8` be the coordinate-frame-plus-root normals on the pinned P112 puncture. The exact dependency is + +```text +sum_k z_k b_k = 0, z=(-1,-1,-1,-1,0,0,0,0,2). +``` + +For every live root line `r_i`, the predecessor solver gives an exact base row `c_i` with `sum_k c_ik b_k=2r_i`. Any rational gauge `t_i` produces another exact row `c_i+t_i z`. Thus arbitrary rational gauges on a selected set of rows preserve the identity, including all 112 squared live pairs. + +For term `k`, let `X_k` be the binary pairing rows from the nonzero coefficients and `Y_k` the fixed normal support. If a proposed local edit changes only rows in a selected block union `B`, the untouched exterior rows give a submatrix of the full pairing matrix. Adding rows cannot lower binary rank, so + +```text +sum_k rank_F2(X_k,Y_k) >= sum_k rank_F2(X_k restricted to i outside B,Y_k). +``` + +The verifier constructs a deterministic partition of the 112 live E8 lines: repeatedly take the smallest remaining index and append the smallest remaining lines orthogonal to all already chosen until an eight-line block forms. It certifies 14 disjoint orthogonal blocks covering P112. For each of the 14 individual blocks and 91 unordered block pairs, it computes the exact exterior-row rank vector using the canonical per-root sparsest gauges outside the selected union. + +The singleton floor histogram is `67:2, 68:12`. The pair floor histogram is `64:1, 67:24, 68:66`; the unique 64 case has fixed ranks `(8,8,8,8,8,8,8,8,0)`. Hence no decoder in this scoped family can beat copied-information cost 64, even with arbitrary rational gauge choices on the changed rows. The argument does not permit coordinated changes on three or more blocks, changes to exterior rows, a different frame, or a different puncture. diff --git a/research/coord-root-p112-local-tetrad-gauge-seed8232/README.md b/research/coord-root-p112-local-tetrad-gauge-seed8232/README.md new file mode 100644 index 0000000000..bbfa90b220 --- /dev/null +++ b/research/coord-root-p112-local-tetrad-gauge-seed8232/README.md @@ -0,0 +1,38 @@ +# Two-block local gauge edits cannot beat the P112 copy cost + +**Scoped exact negative result; no new κ.** On one fixed P112 nine-normal decoder, allow arbitrary rational per-root coefficient gauges on any one or two blocks of a fixed 14-block orthogonal partition, while keeping all exterior rows at their canonical sparsest gauges. The exact optimistic cost floor is at least **64** for every one of the 14 singleton blocks and 91 block pairs. The existing P112 decoder already costs 64, so this local support-change mechanism has no copy-cost headroom before frame or realization expenses. + +Cycle 16 seed: `8232e87e36b7bc2bd06a84ddf3384413`; track `complex-mechanisms`; refined task `complex-rank-shape-decoder`; priority revision 3. The exact base is `ecc75c79c22d909fd42aa68437eb77c4c1361835`, and the selected-record SHA256 is `10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32`. Selected κ remains `836330098538459/500000000000000000`. Source and predecessor pins are in [SOURCES.json](SOURCES.json). + +## Object and result + +The frame consists of the eight coordinate-frame normals removed for P112 plus the first four-contact extra root (line index 1). Its dependency is `(-1,-1,-1,-1,0,0,0,0,2)`. Each live-root coefficient row is `c_i+t_i z`; this retains the exact identity for every rational `t_i`. + +The 112 live lines are greedily partitioned by increasing canonical line index into 14 disjoint orthogonal eight-line blocks. For any chosen block or block pair, freeze every exterior row at `Frame.sparsest(i)`. The sum of the nine F2 ranks from those exterior rows is an exact lower bound on every local gauge completion, because adding pairing rows cannot reduce rank. + +| Changed blocks | Cases | Exact exterior floors | +|---|---:|---| +| One | 14 | 67 twice; 68 twelve times | +| Two | 91 | 64 once; 67 twenty-four times; 68 sixty-six times | + +The unique pair floor 64 is attained by retaining ranks `(8,8,8,8,8,8,8,8,0)` from the exterior rows. This does not show that the completed decoder reaches 64; it shows only that this favorable local-edit model cannot go below it. + +## Relation to nearby work + +Merged PR #1224 supplies the nine-normal frame and per-root dependency gauge. Cycle 15’s PR #1962 studies one shared ternary shift vector; this package instead permits independent rational shifts on any one or two tetrad blocks and proves a monotone exterior-rank floor. Open PR #1909 proves a different tetrad-local masked-decoder bound and lists two-tetrad support escape as a next question. Here the exact construction family is fixed to the coordinate-plus-root frame and fixed exterior sparse gauges. No arbitrary masked supports or general frame excess theorem is claimed. + +## Reproduce + +```sh +python3 -I -B research/coord-root-p112-local-tetrad-gauge-seed8232/verify.py +python3 scripts/research_package.py --package research/coord-root-p112-local-tetrad-gauge-seed8232 --check-only +``` + +The exact verifier writes `RESULT.json`, checks the baseline decoder on all `112^2` live pairs, tests three nontrivial rational gauge completions, and rejects a one-coefficient mutation. The registered replay targets Python 3.12; the local environment provides Python 3.14.7. + +## Open next questions + +- Can coordinated gauge changes on three or more of these 14 blocks produce a copy floor below 64? First compute the exterior-rank floor for every three-block union, then continue only if it leaves headroom. +- Can another nine-normal frame on this same puncture make a sparse local gauge edit favorable? This changes the frame hypothesis and needs a separate optimistic screen. + +Prepared with substantial OpenAI Codex assistance in the exact census, proof checks and writing. No independent human review, full supplier realization or κ change is claimed. diff --git a/research/coord-root-p112-local-tetrad-gauge-seed8232/RESULT.json b/research/coord-root-p112-local-tetrad-gauge-seed8232/RESULT.json new file mode 100644 index 0000000000..369ec761c0 --- /dev/null +++ b/research/coord-root-p112-local-tetrad-gauge-seed8232/RESULT.json @@ -0,0 +1,2076 @@ +{ + "schema_version": 1, + "seed": "8232e87e36b7bc2bd06a84ddf3384413", + "base_commit": "ecc75c79c22d909fd42aa68437eb77c4c1361835", + "selected_record_sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32", + "puncture_indices": [ + 0, + 13, + 90, + 99, + 108, + 113, + 118, + 119 + ], + "extra_root_index": 1, + "dependency": [ + -1, + -1, + -1, + -1, + 0, + 0, + 0, + 0, + 2 + ], + "live_roots": 112, + "baseline_sparsest_cost": 68, + "baseline_term_ranks": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 4 + ], + "baseline_exact_pairs": 12544, + "tetrads": [ + [ + 1, + 12, + 79, + 88, + 109, + 112, + 115, + 116 + ], + [ + 2, + 11, + 78, + 89, + 110, + 111, + 114, + 117 + ], + [ + 3, + 10, + 81, + 86, + 93, + 96, + 103, + 104 + ], + [ + 4, + 9, + 80, + 87, + 94, + 95, + 102, + 105 + ], + [ + 5, + 8, + 83, + 84, + 91, + 98, + 101, + 106 + ], + [ + 6, + 7, + 82, + 85, + 92, + 97, + 100, + 107 + ], + [ + 14, + 21, + 39, + 44, + 56, + 59, + 65, + 66 + ], + [ + 15, + 20, + 38, + 45, + 57, + 58, + 64, + 67 + ], + [ + 16, + 19, + 41, + 42, + 54, + 61, + 63, + 68 + ], + [ + 17, + 18, + 40, + 43, + 55, + 60, + 62, + 69 + ], + [ + 22, + 29, + 31, + 36, + 48, + 51, + 73, + 74 + ], + [ + 23, + 28, + 30, + 37, + 49, + 50, + 72, + 75 + ], + [ + 24, + 27, + 33, + 34, + 46, + 53, + 71, + 76 + ], + [ + 25, + 26, + 32, + 35, + 47, + 52, + 70, + 77 + ] + ], + "single_block_floors": [ + { + "blocks": [ + 0 + ], + "fixed_ranks": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 3 + ], + "floor": 67 + }, + { + "blocks": [ + 1 + ], + "fixed_ranks": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 3 + ], + "floor": 67 + }, + { + "blocks": [ + 2 + ], + "fixed_ranks": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 4 + ], + "floor": 68 + }, + { + "blocks": [ + 3 + ], + "fixed_ranks": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 4 + ], + "floor": 68 + }, + { + "blocks": [ + 4 + ], + "fixed_ranks": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 4 + ], + "floor": 68 + }, + { + "blocks": [ + 5 + ], + "fixed_ranks": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 4 + ], + "floor": 68 + }, + { + "blocks": [ + 6 + ], + "fixed_ranks": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 4 + ], + "floor": 68 + }, + { + "blocks": [ + 7 + ], + "fixed_ranks": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 4 + ], + "floor": 68 + }, + { + "blocks": [ + 8 + ], + "fixed_ranks": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 4 + ], + "floor": 68 + }, + { + "blocks": [ + 9 + ], + "fixed_ranks": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 4 + ], + "floor": 68 + }, + { + "blocks": [ + 10 + ], + "fixed_ranks": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 4 + ], + "floor": 68 + }, + { + "blocks": [ + 11 + ], + "fixed_ranks": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 4 + ], + "floor": 68 + }, + { + "blocks": [ + 12 + ], + "fixed_ranks": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 4 + ], + "floor": 68 + }, + { + "blocks": [ + 13 + ], + "fixed_ranks": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 4 + ], + "floor": 68 + } + ], + "pair_block_floors": [ + { + "blocks": [ + 0, + 1 + ], + "fixed_ranks": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 0 + ], + "floor": 64 + }, + { + "blocks": [ + 0, + 2 + ], + "fixed_ranks": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 3 + ], + "floor": 67 + }, + { + "blocks": [ + 0, + 3 + ], + "fixed_ranks": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 3 + ], + "floor": 67 + }, + { + "blocks": [ + 0, + 4 + ], + "fixed_ranks": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 3 + ], + "floor": 67 + }, + { + "blocks": [ + 0, + 5 + ], + "fixed_ranks": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 3 + ], + "floor": 67 + }, + { + "blocks": [ + 0, + 6 + ], + "fixed_ranks": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 3 + ], + "floor": 67 + }, + { + "blocks": [ + 0, + 7 + ], + "fixed_ranks": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 3 + ], + "floor": 67 + }, + { + "blocks": [ + 0, + 8 + ], + "fixed_ranks": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 3 + ], + "floor": 67 + }, + { + "blocks": [ + 0, + 9 + ], + "fixed_ranks": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 3 + ], + "floor": 67 + }, + { + "blocks": [ + 0, + 10 + ], + "fixed_ranks": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 3 + ], + "floor": 67 + }, + { + "blocks": [ + 0, + 11 + ], + "fixed_ranks": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 3 + ], + "floor": 67 + }, + { + "blocks": [ + 0, + 12 + ], + "fixed_ranks": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 3 + ], + "floor": 67 + }, + { + "blocks": [ + 0, + 13 + ], + "fixed_ranks": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 3 + ], + "floor": 67 + }, + { + "blocks": [ + 1, + 2 + ], + "fixed_ranks": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 3 + ], + "floor": 67 + }, + { + "blocks": [ + 1, + 3 + ], + "fixed_ranks": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 3 + ], + "floor": 67 + }, + { + "blocks": [ + 1, + 4 + ], + "fixed_ranks": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 3 + ], + "floor": 67 + }, + { + "blocks": [ + 1, + 5 + ], + "fixed_ranks": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 3 + ], + "floor": 67 + }, + { + "blocks": [ + 1, + 6 + ], + "fixed_ranks": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 3 + ], + "floor": 67 + }, + { + "blocks": [ + 1, + 7 + ], + "fixed_ranks": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 3 + ], + "floor": 67 + }, + { + "blocks": [ + 1, + 8 + ], + "fixed_ranks": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 3 + ], + "floor": 67 + }, + { + "blocks": [ + 1, + 9 + ], + "fixed_ranks": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 3 + ], + "floor": 67 + }, + { + "blocks": [ + 1, + 10 + ], + "fixed_ranks": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 3 + ], + "floor": 67 + }, + { + "blocks": [ + 1, + 11 + ], + "fixed_ranks": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 3 + ], + "floor": 67 + }, + { + "blocks": [ + 1, + 12 + ], + "fixed_ranks": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 3 + ], + "floor": 67 + }, + { + "blocks": [ + 1, + 13 + ], + "fixed_ranks": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 3 + ], + "floor": 67 + }, + { + "blocks": [ + 2, + 3 + ], + "fixed_ranks": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 4 + ], + "floor": 68 + }, + { + "blocks": [ + 2, + 4 + ], + "fixed_ranks": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 4 + ], + "floor": 68 + }, + { + "blocks": [ + 2, + 5 + ], + "fixed_ranks": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 4 + ], + "floor": 68 + }, + { + "blocks": [ + 2, + 6 + ], + "fixed_ranks": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 4 + ], + "floor": 68 + }, + { + "blocks": [ + 2, + 7 + ], + "fixed_ranks": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 4 + ], + "floor": 68 + }, + { + "blocks": [ + 2, + 8 + ], + "fixed_ranks": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 4 + ], + "floor": 68 + }, + { + "blocks": [ + 2, + 9 + ], + "fixed_ranks": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 4 + ], + "floor": 68 + }, + { + "blocks": [ + 2, + 10 + ], + "fixed_ranks": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 4 + ], + "floor": 68 + }, + { + "blocks": [ + 2, + 11 + ], + "fixed_ranks": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 4 + ], + "floor": 68 + }, + { + "blocks": [ + 2, + 12 + ], + "fixed_ranks": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 4 + ], + "floor": 68 + }, + { + "blocks": [ + 2, + 13 + ], + "fixed_ranks": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 4 + ], + "floor": 68 + }, + { + "blocks": [ + 3, + 4 + ], + "fixed_ranks": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 4 + ], + "floor": 68 + }, + { + "blocks": [ + 3, + 5 + ], + "fixed_ranks": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 4 + ], + "floor": 68 + }, + { + "blocks": [ + 3, + 6 + ], + "fixed_ranks": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 4 + ], + "floor": 68 + }, + { + "blocks": [ + 3, + 7 + ], + "fixed_ranks": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 4 + ], + "floor": 68 + }, + { + "blocks": [ + 3, + 8 + ], + "fixed_ranks": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 4 + ], + "floor": 68 + }, + { + "blocks": [ + 3, + 9 + ], + "fixed_ranks": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 4 + ], + "floor": 68 + }, + { + "blocks": [ + 3, + 10 + ], + "fixed_ranks": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 4 + ], + "floor": 68 + }, + { + "blocks": [ + 3, + 11 + ], + "fixed_ranks": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 4 + ], + "floor": 68 + }, + { + "blocks": [ + 3, + 12 + ], + "fixed_ranks": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 4 + ], + "floor": 68 + }, + { + "blocks": [ + 3, + 13 + ], + "fixed_ranks": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 4 + ], + "floor": 68 + }, + { + "blocks": [ + 4, + 5 + ], + "fixed_ranks": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 4 + ], + "floor": 68 + }, + { + "blocks": [ + 4, + 6 + ], + "fixed_ranks": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 4 + ], + "floor": 68 + }, + { + "blocks": [ + 4, + 7 + ], + "fixed_ranks": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 4 + ], + "floor": 68 + }, + { + "blocks": [ + 4, + 8 + ], + "fixed_ranks": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 4 + ], + "floor": 68 + }, + { + "blocks": [ + 4, + 9 + ], + "fixed_ranks": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 4 + ], + "floor": 68 + }, + { + "blocks": [ + 4, + 10 + ], + "fixed_ranks": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 4 + ], + "floor": 68 + }, + { + "blocks": [ + 4, + 11 + ], + "fixed_ranks": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 4 + ], + "floor": 68 + }, + { + "blocks": [ + 4, + 12 + ], + "fixed_ranks": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 4 + ], + "floor": 68 + }, + { + "blocks": [ + 4, + 13 + ], + "fixed_ranks": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 4 + ], + "floor": 68 + }, + { + "blocks": [ + 5, + 6 + ], + "fixed_ranks": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 4 + ], + "floor": 68 + }, + { + "blocks": [ + 5, + 7 + ], + "fixed_ranks": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 4 + ], + "floor": 68 + }, + { + "blocks": [ + 5, + 8 + ], + "fixed_ranks": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 4 + ], + "floor": 68 + }, + { + "blocks": [ + 5, + 9 + ], + "fixed_ranks": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 4 + ], + "floor": 68 + }, + { + "blocks": [ + 5, + 10 + ], + "fixed_ranks": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 4 + ], + "floor": 68 + }, + { + "blocks": [ + 5, + 11 + ], + "fixed_ranks": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 4 + ], + "floor": 68 + }, + { + "blocks": [ + 5, + 12 + ], + "fixed_ranks": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 4 + ], + "floor": 68 + }, + { + "blocks": [ + 5, + 13 + ], + "fixed_ranks": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 4 + ], + "floor": 68 + }, + { + "blocks": [ + 6, + 7 + ], + "fixed_ranks": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 4 + ], + "floor": 68 + }, + { + "blocks": [ + 6, + 8 + ], + "fixed_ranks": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 4 + ], + "floor": 68 + }, + { + "blocks": [ + 6, + 9 + ], + "fixed_ranks": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 4 + ], + "floor": 68 + }, + { + "blocks": [ + 6, + 10 + ], + "fixed_ranks": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 4 + ], + "floor": 68 + }, + { + "blocks": [ + 6, + 11 + ], + "fixed_ranks": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 4 + ], + "floor": 68 + }, + { + "blocks": [ + 6, + 12 + ], + "fixed_ranks": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 4 + ], + "floor": 68 + }, + { + "blocks": [ + 6, + 13 + ], + "fixed_ranks": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 4 + ], + "floor": 68 + }, + { + "blocks": [ + 7, + 8 + ], + "fixed_ranks": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 4 + ], + "floor": 68 + }, + { + "blocks": [ + 7, + 9 + ], + "fixed_ranks": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 4 + ], + "floor": 68 + }, + { + "blocks": [ + 7, + 10 + ], + "fixed_ranks": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 4 + ], + "floor": 68 + }, + { + "blocks": [ + 7, + 11 + ], + "fixed_ranks": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 4 + ], + "floor": 68 + }, + { + "blocks": [ + 7, + 12 + ], + "fixed_ranks": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 4 + ], + "floor": 68 + }, + { + "blocks": [ + 7, + 13 + ], + "fixed_ranks": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 4 + ], + "floor": 68 + }, + { + "blocks": [ + 8, + 9 + ], + "fixed_ranks": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 4 + ], + "floor": 68 + }, + { + "blocks": [ + 8, + 10 + ], + "fixed_ranks": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 4 + ], + "floor": 68 + }, + { + "blocks": [ + 8, + 11 + ], + "fixed_ranks": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 4 + ], + "floor": 68 + }, + { + "blocks": [ + 8, + 12 + ], + "fixed_ranks": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 4 + ], + "floor": 68 + }, + { + "blocks": [ + 8, + 13 + ], + "fixed_ranks": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 4 + ], + "floor": 68 + }, + { + "blocks": [ + 9, + 10 + ], + "fixed_ranks": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 4 + ], + "floor": 68 + }, + { + "blocks": [ + 9, + 11 + ], + "fixed_ranks": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 4 + ], + "floor": 68 + }, + { + "blocks": [ + 9, + 12 + ], + "fixed_ranks": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 4 + ], + "floor": 68 + }, + { + "blocks": [ + 9, + 13 + ], + "fixed_ranks": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 4 + ], + "floor": 68 + }, + { + "blocks": [ + 10, + 11 + ], + "fixed_ranks": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 4 + ], + "floor": 68 + }, + { + "blocks": [ + 10, + 12 + ], + "fixed_ranks": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 4 + ], + "floor": 68 + }, + { + "blocks": [ + 10, + 13 + ], + "fixed_ranks": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 4 + ], + "floor": 68 + }, + { + "blocks": [ + 11, + 12 + ], + "fixed_ranks": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 4 + ], + "floor": 68 + }, + { + "blocks": [ + 11, + 13 + ], + "fixed_ranks": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 4 + ], + "floor": 68 + }, + { + "blocks": [ + 12, + 13 + ], + "fixed_ranks": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 4 + ], + "floor": 68 + } + ], + "single_floor_histogram": { + "67": 2, + "68": 12 + }, + "pair_floor_histogram": { + "64": 1, + "67": 24, + "68": 66 + }, + "gauge_identity_controls": 3, + "mutation_rejected": true, + "scope_limit": "Exterior rows remain at the canonical sparsest gauges; only one or two blocks of this fixed partition may change. No result is claimed for three or more blocks or another frame or puncture." +} diff --git a/research/coord-root-p112-local-tetrad-gauge-seed8232/SOURCES.json b/research/coord-root-p112-local-tetrad-gauge-seed8232/SOURCES.json new file mode 100644 index 0000000000..a79baa0cfe --- /dev/null +++ b/research/coord-root-p112-local-tetrad-gauge-seed8232/SOURCES.json @@ -0,0 +1,72 @@ +{ + "schema_version": 1, + "base_commit": "ecc75c79c22d909fd42aa68437eb77c4c1361835", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "input", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "06c96f5579bb67ed1b86d334e78fbed7da6945f1", + "sha256": "6686ad58f1fbdbc87134a78901b60fd53a20d3984355e91defbbebc9e9fa8075" + }, + { + "path": "docs/research/community-batch1099-review.md", + "usage": "input", + "git_blob": "6cb6ec061a071a06a2d18cd4dc3e9a2b05d28099", + "sha256": "7e76d2c38e5fce30587835b7251df1430488ae4dd372611ef69a3f03f476b6cb" + }, + { + "path": "research/community-frontier1094-audit/SELECTED-SOURCE.json", + "usage": "input", + "git_blob": "6a75493790b4eff9c4a98051ef8b01d6aad0d5a8", + "sha256": "79b3de5db3dbcb9829789ba58e9e45758926031e2a7d80667a08429d369be53b" + }, + { + "path": "research/community-frontier1094-audit/ASSEMBLY.json", + "usage": "input", + "git_blob": "5fd676df060f3b450782fdf5ff5f6beb63a5eeb0", + "sha256": "1122cb3a575f8c788345fc1bf4c108ac7c3250fb81a5988671f5eb04b3ab3045" + }, + { + "path": "research/nine-term-decoder-normal-form-seed42/e8lab.py", + "usage": "input", + "git_blob": "6aef95fc972f56e600b7c9699238e3a1ce7f7413", + "sha256": "772349edc9dff45fa3cac89fdbbe8bf1bab734e9776a245fcac8e8bd60d94634" + }, + { + "path": "research/nine-term-decoder-normal-form-seed42/verify.py", + "usage": "input", + "git_blob": "994e429042f292084546c8d1efe287dfb5930fd9", + "sha256": "248763cf5ff85f073766aa8a85187a1d314fcf3a716b2586ca8fc1197d4c6c4e" + }, + { + "path": "research/nine-term-decoder-normal-form-seed42/README.md", + "usage": "provenance", + "git_blob": "9cf8ecd3eda302b57ab14302c429b00c255f2dba", + "sha256": "d272081da47d6ea6a2404fddff211418dd6e7c236babf7eb4560737e818c1677" + }, + { + "path": "research/nine-term-decoder-normal-form-seed42/CLAIM.md", + "usage": "provenance", + "git_blob": "ce6c5b94ce1e061c4ea9c8ff39037f81dfd44370", + "sha256": "55eaaa473a2491727bf6efa5cbf48bd28134a6cc16c5b1eb62894a01362bb91d" + }, + { + "path": "research/nine-term-decoder-normal-form-seed42/SOURCES.json", + "usage": "provenance", + "git_blob": "a36ca6604aafcd5ba9a1d13b6be4c5a1eeedd98d", + "sha256": "a4bd91641f598799619a163d0ae30b49fce87903f3517e6cdc8d88889ac51eac" + }, + { + "path": "scripts/choose_research_task.py", + "usage": "provenance", + "git_blob": "695639622a283190948c4187bdbb41997e6e43d7", + "sha256": "f1af1e70858ab1d033ce20ee1968201bc592eb9e3fd05ab8ad78c842c0b028d1" + } + ] +} diff --git a/research/coord-root-p112-local-tetrad-gauge-seed8232/TASK.json b/research/coord-root-p112-local-tetrad-gauge-seed8232/TASK.json new file mode 100644 index 0000000000..47555d2122 --- /dev/null +++ b/research/coord-root-p112-local-tetrad-gauge-seed8232/TASK.json @@ -0,0 +1,74 @@ +{ + "schema_version": 1, + "task_id": "complex-rank-shape-decoder", + "priority_revision": 3, + "seed": "8232e87e36b7bc2bd06a84ddf3384413", + "base_commit": "ecc75c79c22d909fd42aa68437eb77c4c1361835", + "selected_record_sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32", + "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": [ + "research/complex-local-word-ceiling/README.md", + "research/complex-decoder-field-extension-seed44/README.md", + "research/complex-frame-pair-decoders/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.", + "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." + ], + "overlap_terms": [ + "rank shape", + "block climb", + "masked decoder", + "overcomplete", + "effective rank" + ] + }, + "scope_status": "refined", + "scope_change_reason": "The assigned block-decoder route is crowded by open P112 masked-decoder work. This package isolates a different exact support-change mechanism: independent rational null-dependency gauges on at most two orthogonal blocks of the merged coordinate-frame-plus-root P112 decoder, with every exterior row fixed to its canonical sparsest gauge. It supplies an exact monotone exterior-rank lower bound rather than repeating Cycle 15's shared ternary shift search.", + "actual_scope": "For the coordinate-frame-plus-root nine-normal decoder on the fixed P112 puncture, partition the 112 live E8 lines by the stated increasing-index greedy rule into 14 disjoint orthogonal eight-line blocks. For each of the 14 blocks and 91 unordered block pairs, vary arbitrary rational coefficient gauges only on the selected block union and pin every exterior row to Frame.sparsest(i). Compute the exact F2 copied-information rank of the exterior rows as a lower bound for every completion.", + "bottleneck_link": "A decoder with copied-information cost below 64 could improve the P112 local invoice before frame and realization charges. The exact exterior-row relaxation floors this entire one/two-block family at 64 or more, so no favorable completed budget exists in this scope.", + "budget_minutes": 60, + "stop_rule": "Compute the exact exterior-row rank floor for all 14 singleton blocks and all 91 block pairs. Stop if every floor is at least the existing cost 64; do not extend to three blocks, different gauges outside the selected union, another frame or another puncture.", + "outcome": "negative-result", + "evidence": "The exact census gives one-block floors 67 twice and 68 twelve times; pair floors 64 once, 67 twenty-four times and 68 sixty-six times. The coordinate-root baseline costs 68 and is exact on all 112^2 live pairs. Three arbitrary rational dependency-gauge completions pass the exact identity; a coefficient mutation fails. No floor is a new decoder cost or kappa.", + "author": "Cinna Davis", + "ai_assistance": "Substantial OpenAI Codex assistance in scope selection, exact enumeration, proof checks and writing. No independent human review or proof-assistant formalization is claimed.", + "open_questions": [ + { + "question": "Can coordinated gauge changes on three or more blocks lower the exterior-row floor below 64?", + "why_it_matters": "This is the next size of local support change that could leave copy-cost headroom.", + "first_step": "Compute exact fixed-exterior ranks for all three-block unions before enumerating any gauge choices.", + "blocked_by": "No three-block floor has been computed; the current result is intentionally limited to one or two blocks." + }, + { + "question": "Can a different nine-normal frame on this puncture make one- or two-block edits favorable?", + "why_it_matters": "That would change the fixed-frame restriction behind this local obstruction.", + "first_step": "Select a specific alternate frame and derive the same exterior-rank lower bound before any coefficient search.", + "blocked_by": "No alternate frame has been selected or cost-screened." + } + ] +} diff --git a/research/coord-root-p112-local-tetrad-gauge-seed8232/VERIFY.json b/research/coord-root-p112-local-tetrad-gauge-seed8232/VERIFY.json new file mode 100644 index 0000000000..6b3022e90e --- /dev/null +++ b/research/coord-root-p112-local-tetrad-gauge-seed8232/VERIFY.json @@ -0,0 +1,26 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "certificates/selected-result.json", + "docs/research/community-batch1099-review.md", + "research/community-frontier1094-audit/SELECTED-SOURCE.json", + "research/community-frontier1094-audit/ASSEMBLY.json", + "research/nine-term-decoder-normal-form-seed42/e8lab.py", + "research/nine-term-decoder-normal-form-seed42/verify.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 180, + "checks": "Pin predecessor sources; rebuild the exact P112 frame and 14-block partition; check the baseline on all 12,544 live pairs; recompute all 14 singleton and 91 pair exterior-rank floors; test three rational gauge identities and reject a coefficient mutation." + } + ] +} diff --git a/research/coord-root-p112-local-tetrad-gauge-seed8232/verify.py b/research/coord-root-p112-local-tetrad-gauge-seed8232/verify.py new file mode 100644 index 0000000000..07e97156bc --- /dev/null +++ b/research/coord-root-p112-local-tetrad-gauge-seed8232/verify.py @@ -0,0 +1,162 @@ +#!/usr/bin/env python3 +"""Exact fixed-row rank floors for local gauges of one P112 nine-normal decoder.""" +from collections import Counter +from fractions import Fraction +import hashlib +import itertools +import json +from pathlib import Path +import sys + +ROOT = Path(__file__).resolve().parents[2] +HERE = Path(__file__).resolve().parent +PREDECESSOR = ROOT / "research/nine-term-decoder-normal-form-seed42" +PINNED = { + "e8lab.py": "772349edc9dff45fa3cac89fdbbe8bf1bab734e9776a245fcac8e8bd60d94634", + "verify.py": "248763cf5ff85f073766aa8a85187a1d314fcf3a716b2586ca8fc1197d4c6c4e", +} + + +def need(ok, message): + if not ok: + raise AssertionError(message) + + +for name, expected in PINNED.items(): + need(hashlib.sha256((PREDECESSOR / name).read_bytes()).hexdigest() == expected, + "predecessor source drift: " + name) +sys.path.insert(0, str(PREDECESSOR)) +import e8lab as E # noqa: E402 +import verify as V # noqa: E402 + + +def masks_and_cost(rows, normals, live): + X = [0] * 9 + for i, row in rows.items(): + for k, coefficient in enumerate(row): + if coefficient: + X[k] |= 1 << i + Y = [E.support(b, live) for b in normals] + ranks = tuple(E.pairing_rank(X[k], Y[k]) for k in range(9)) + return ranks, X, Y + + +def exact_tetrads(roots): + remaining = set(roots) + blocks = [] + while remaining: + first = min(remaining) + block = [first] + for i in sorted(remaining - {first}): + if all(E.G[i][j] == 0 for j in block): + block.append(i) + if len(block) == 8: + break + need(len(block) == 8, "greedy orthogonal block did not have size 8") + blocks.append(block) + remaining.difference_update(block) + need(len(blocks) == 14 and sum(map(len, blocks)) == 112, "P112 partition changed") + need(len(set(i for block in blocks for i in block)) == 112, "blocks are not disjoint") + need(all(all(E.G[i][j] == 0 for i, j in itertools.combinations(block, 2)) + for block in blocks), "a block is not orthogonal") + return blocks + + +def fixed_row_floor(roots, base_rows, normals, live, changed): + """Cost from exterior rows only; any added row preserves or raises F2 rank.""" + X = [0] * 9 + changed = set(changed) + for i in roots: + if i in changed: + continue + for k, coefficient in enumerate(base_rows[i]): + if coefficient: + X[k] |= 1 << i + Y = [E.support(b, live) for b in normals] + ranks = tuple(E.pairing_rank(X[k], Y[k]) for k in range(9)) + return ranks + + +def run(): + puncture = V.coordinate_frame() + need(puncture == [0, 13, 90, 99, 108, 113, 118, 119], "P112 puncture changed") + extra = next(i for i in range(E.N) if i not in puncture and + sum(E.G[i][f] != 0 for f in puncture) == 4) + need(extra == 1, "extra normal changed") + frame = V.Frame("coordinate frame + root", [E.LINES[f] for f in puncture] + [E.LINES[extra]]) + need(frame.z == [Fraction(-1), Fraction(-1), Fraction(-1), Fraction(-1), + Fraction(0), Fraction(0), Fraction(0), Fraction(0), Fraction(2)], + "nine-normal dependency changed") + live = E.FULL ^ sum(1 << i for i in puncture) + roots = list(E.bits(live)) + need(len(roots) == 112, "live set is not P112") + tetrads = exact_tetrads(roots) + base = {i: frame.sparsest(i) for i in roots} + base_ranks, _, _ = masks_and_cost(base, frame.F, live) + need(sum(base_ranks) == 68, "canonical sparse P112 cost changed") + exact, pairs = V.exact_on_pairs(base, frame.F, live) + need(exact and pairs == 112 ** 2, "baseline decoder identity failed") + + one = [] + two = [] + for a, block in enumerate(tetrads): + ranks = fixed_row_floor(roots, base, frame.F, live, block) + one.append({"blocks": [a], "fixed_ranks": list(ranks), "floor": sum(ranks)}) + for a, b in itertools.combinations(range(14), 2): + changed = tetrads[a] + tetrads[b] + ranks = fixed_row_floor(roots, base, frame.F, live, changed) + two.append({"blocks": [a, b], "fixed_ranks": list(ranks), "floor": sum(ranks)}) + need(Counter(x["floor"] for x in one) == Counter({67: 2, 68: 12}), "single-block census changed") + need(Counter(x["floor"] for x in two) == Counter({64: 1, 67: 24, 68: 66}), "pair census changed") + need([x for x in two if x["floor"] == 64] == [ + {"blocks": [0, 1], "fixed_ranks": [8, 8, 8, 8, 8, 8, 8, 8, 0], "floor": 64} + ], "unique optimistic equality case changed") + + # Nontrivial rational gauges on the changed rows preserve the exact decoder identity. + for block_ids in ([0], [0, 1], [12, 13]): + changed = set().union(*(set(tetrads[j]) for j in block_ids)) + rows = {i: list(row) for i, row in base.items()} + for i in changed: + t = Fraction((i % 7) - 3, 5) + rows[i] = [base[i][k] + t * frame.z[k] for k in range(9)] + ok, count = V.exact_on_pairs(rows, frame.F, live) + need(ok and count == 112 ** 2, "dependency gauge failed exact all-pairs identity") + + bad = {i: list(row) for i, row in base.items()} + bad[roots[0]][0] += 1 + need(V.exact_on_pairs(bad, frame.F, live)[0] is False, "coefficient mutation escaped control") + + result = { + "schema_version": 1, + "seed": "8232e87e36b7bc2bd06a84ddf3384413", + "base_commit": "ecc75c79c22d909fd42aa68437eb77c4c1361835", + "selected_record_sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32", + "puncture_indices": puncture, + "extra_root_index": extra, + "dependency": [int(x) for x in frame.z], + "live_roots": len(roots), + "baseline_sparsest_cost": sum(base_ranks), + "baseline_term_ranks": list(base_ranks), + "baseline_exact_pairs": pairs, + "tetrads": tetrads, + "single_block_floors": one, + "pair_block_floors": two, + "single_floor_histogram": {str(k): v for k, v in sorted(Counter(x["floor"] for x in one).items())}, + "pair_floor_histogram": {str(k): v for k, v in sorted(Counter(x["floor"] for x in two).items())}, + "gauge_identity_controls": 3, + "mutation_rejected": True, + "scope_limit": "Exterior rows remain at the canonical sparsest gauges; only one or two blocks of this fixed partition may change. No result is claimed for three or more blocks or another frame or puncture.", + } + (HERE / "RESULT.json").write_text(json.dumps(result, indent=2) + "\n", encoding="utf-8") + print("PASS_COORD_ROOT_P112_LOCAL_TETRAD_GAUGE", json.dumps({ + "baseline_cost": result["baseline_sparsest_cost"], + "single_floor_histogram": result["single_floor_histogram"], + "pair_floor_histogram": result["pair_floor_histogram"], + "exact_pairs": pairs, + "gauge_controls": 3, + "mutation_rejected": True, + }, sort_keys=True)) + + +if __name__ == "__main__": + run()