From 002a9983079a3244c10221b4e16d0cff7e70da40 Mon Sep 17 00:00:00 2001 From: Tekalign <152792726+tekuuu@users.noreply.github.com> Date: Fri, 16 Oct 2026 00:48:42 +0300 Subject: [PATCH] Prove a positive half-integral Gram tariff barrier and exhaust paired-plane C5 menu --- .../c5-dyadic-decoder-gate/.gitattributes | 1 + research/c5-dyadic-decoder-gate/PROOF.md | 100 ++ research/c5-dyadic-decoder-gate/README.md | 135 ++ research/c5-dyadic-decoder-gate/RESULT.json | 1439 +++++++++++++++++ research/c5-dyadic-decoder-gate/SEARCH.md | 54 + research/c5-dyadic-decoder-gate/SOURCES.json | 60 + research/c5-dyadic-decoder-gate/TASK.json | 118 ++ research/c5-dyadic-decoder-gate/VERIFY.json | 30 + research/c5-dyadic-decoder-gate/algebra.py | 157 ++ .../c5-dyadic-decoder-gate/independent.cpp | 70 + .../c5-dyadic-decoder-gate/independent.py | 60 + .../inputs/DATA-PHASES.json.gz | Bin 0 -> 24910 bytes .../inputs/MATCHING.json | 539 ++++++ research/c5-dyadic-decoder-gate/search.py | 69 + .../c5-dyadic-decoder-gate/test_package.py | 98 ++ research/c5-dyadic-decoder-gate/verify.py | 151 ++ 16 files changed, 3081 insertions(+) create mode 100644 research/c5-dyadic-decoder-gate/.gitattributes create mode 100644 research/c5-dyadic-decoder-gate/PROOF.md create mode 100644 research/c5-dyadic-decoder-gate/README.md create mode 100644 research/c5-dyadic-decoder-gate/RESULT.json create mode 100644 research/c5-dyadic-decoder-gate/SEARCH.md create mode 100644 research/c5-dyadic-decoder-gate/SOURCES.json create mode 100644 research/c5-dyadic-decoder-gate/TASK.json create mode 100644 research/c5-dyadic-decoder-gate/VERIFY.json create mode 100644 research/c5-dyadic-decoder-gate/algebra.py create mode 100644 research/c5-dyadic-decoder-gate/independent.cpp create mode 100644 research/c5-dyadic-decoder-gate/independent.py create mode 100644 research/c5-dyadic-decoder-gate/inputs/DATA-PHASES.json.gz create mode 100644 research/c5-dyadic-decoder-gate/inputs/MATCHING.json create mode 100644 research/c5-dyadic-decoder-gate/search.py create mode 100644 research/c5-dyadic-decoder-gate/test_package.py create mode 100644 research/c5-dyadic-decoder-gate/verify.py diff --git a/research/c5-dyadic-decoder-gate/.gitattributes b/research/c5-dyadic-decoder-gate/.gitattributes new file mode 100644 index 0000000000..f1c360bc66 --- /dev/null +++ b/research/c5-dyadic-decoder-gate/.gitattributes @@ -0,0 +1 @@ +inputs/*.gz binary diff --git a/research/c5-dyadic-decoder-gate/PROOF.md b/research/c5-dyadic-decoder-gate/PROOF.md new file mode 100644 index 0000000000..a742ad5b18 --- /dev/null +++ b/research/c5-dyadic-decoder-gate/PROOF.md @@ -0,0 +1,100 @@ +# Positive half-integral Gram decoders cannot save port-space cost + +## Statement + +Let each scalar port i carry a nondegenerate subspace E_i of a finite binary +space with a symmetric bilinear form. Write d_i = dim E_i. The ambient form may +be degenerate. A scalar fitting matrix K has diagonal one and K_ij = 0 whenever +i != j and E_i is not orthogonal to E_j. + +Suppose + + K = sum_t c_t v_t v_t^T, + +where the factor vectors are integral and every coefficient is a positive +multiple of 1/2. Discard zero terms. Charge term t the binary pairing rank of +S_t against itself, where S_t is the sum of the **complete** E_i for which +v_it is nonzero. There is no bound on the number of terms or support size. + +**Theorem.** The total charge is at least sum_i d_i. Unit-weight singleton +factors attain equality. The statement is normalized to K_ii = 1; rescaling an +unnormalized diagonal also rescales its coefficient alphabet. + +## 1. The diagonal forces a sparse incidence structure + +Positivity and K_ii = 1 imply that every active coefficient is 1/2 or 1, and +that every nonzero factor entry is +1 or -1. Each row therefore occurs either +in exactly one unit-weight column, or in exactly two half-weight columns. +The two kinds of rows never share columns. + +Within one unit-weight column, every pair of distinct rows has nonzero scalar +inner product. The fitting condition forces their complete port spaces to be +pairwise orthogonal. Those spaces are nondegenerate, so the column's charge is +exactly the sum of their dimensions. + +## 2. Half-weight rows form edges + +Identify each half-weight row with the unordered pair of factor columns in +which it occurs: an edge of a multigraph on column indices. Rows on distinct +edges sharing a vertex have exactly one common column and scalar inner product ++1/2 or -1/2. Consequently their complete port spaces are orthogonal. + +On a fixed edge, divide its rows into the two sign classes proportional to +(1,1) and (1,-1). Two rows in the same class have scalar inner product +1 or -1. +Their port spaces are pairwise orthogonal and span a nondegenerate space. +Let A_e and B_e be the dimensions of the two class spaces, equal to the sums of +the individual row dimensions in each class. An empty class has dimension zero. + +Let H_e be the sum of the two class spaces, and let r_e be its restricted +binary pairing rank. It contains each nondegenerate class space, so + + r_e >= max(A_e, B_e) >= (A_e + B_e)/2. + +## 3. The complete tariff adds at each column + +At a column vertex, the H_e of its incident edges are pairwise orthogonal by +section 2. The rank of their sum is the sum of their restricted ranks, **even +if degenerate summands intersect**. To see this, pull the form back along the +surjection from the external direct sum of those spaces. The pullback matrix +is block diagonal. Pullback along a surjection preserves bilinear rank: choose +lifts of a basis in the range and then a basis of the kernel. + +Every edge has two endpoints. Summing the column invoices therefore gives + + half-column charge = 2 sum_e r_e + >= sum_e (A_e + B_e). + +The right side is the sum of d_i over all half-weight rows. Add the unit-column +bill from section 1 to prove the theorem. + +## Consequence and limits + +Under the retained favorable s-stage coverage law, the available deficit is +proportional to `(s-1)/s * tau - C`, where tau = sum_i d_i and C is the decoder +charge. The theorem gives an upper bound `-tau/s`, strictly negative for +positive tau and finite s. Further native, routing, restoration or hosting +charges cannot repair that unfavorable budget. This application retains the +stated coverage law; it is not an all-architecture multiplication lower bound. + +Positivity and the coefficient lattice are essential. The exact E8 fixtures +in algebra.py give cost 72 on 120 line ports with positive quarter weights, +and cost 81 with eight positive and one negative half weight. Both use integral +factors, diagonal one and the same type of full-space tariff. Their binary +pairings have rank nine; quotienting by the radical produces a nine-dimensional +nondegenerate ambient model without changing any charge. They are algebraic +controls, not new native suppliers. + +Asymmetric factors, other coefficients, changed endpoint masks and alternative +physical tariffs remain open. The separate finite C5 census covers only its +explicit 120-root menu. Neither a finite replay nor this handwritten proof is +a formal verification of the full multiplication theorem. + +## Credit + +New proof by Tekalign (`tekuuu`) with substantial OpenAI Codex assistance. +The strict masked endpoint, complete-port-space tariff and 2-integral benchmark +are credited to Adam Gall, Jeremy Diviney, Philippe Van Velzen and their cited +predecessors. This proof addresses a positive half-integral Gram class outside +the 2-integral coefficient hypothesis, with additional symmetry and positivity +restrictions. Known E8 geometry supplies the escape controls. See README and +SOURCES for exact pins and retained construction credit. Apache-2.0. diff --git a/research/c5-dyadic-decoder-gate/README.md b/research/c5-dyadic-decoder-gate/README.md new file mode 100644 index 0000000000..9e761f3018 --- /dev/null +++ b/research/c5-dyadic-decoder-gate/README.md @@ -0,0 +1,135 @@ +# A denominator barrier for positive Gram port decoders + +**Scoped proof and finite negative result; no new κ.** Positive half-integral +weights with integral Gram factors cannot save full port-space cost. Quarter +weights and signed weights genuinely escape that theorem. On the actual 23 +induced C5s of PR1825's paired-plane matching, the specified quarter-integral +E8 menu nevertheless has minimum cost **20**, exactly the direct baseline. + +This stops this particular expansion into a supplier. It does not establish a +barrier for arbitrary rational decoders, other matchings or changed physical +interfaces. The selected frontier remains unchanged. + +## Written theorem + +Normalize the strict scalar endpoint to diagonal one. Let every port carry a +nondegenerate binary space E_i of dimension d_i. A rank-one Gram term costs the +binary pairing rank of the sum of its **complete port spaces** against itself. +For any finite number of terms, positive weights in `(1/2) Z`, and integral +factor entries, + + total cost >= sum_i d_i. + +[PROOF.md](PROOF.md) gives the argument for arbitrary term counts, supports and +port dimensions. The diagonal equation forces either one unit-weight occurrence +or two half-weight occurrences per row. The latter form edges of a graph on +columns; orthogonality of distinct incident edge bundles makes their ranks add. +The two sign classes on each edge give the required lower bound. + +Under the retained favorable s-stage coverage law, the available deficit is +proportional to `(s-1)/s * sum_i d_i - cost`, hence is strictly negative in this +class even before further costs. This inference is conditional on that coverage +law; it is not a universal lower bound for multiplication. + +The restrictions are material. Exact generated E8 controls have 120 line ports +and binary quotient dimension nine: + +| Integral-coordinate representation | Weights | Cost | +|---|---|---:| +| Positive scaled E8 chart | eight `+1/4` | 72 | +| Lorentzian E8 chart | eight `+1/2`, one `-1/2` | 81 | + +Both fit their strict scalar masks. These are algebraic controls using known E8 +geometry, not new suppliers or new κ. They show that quarter is the first +positive dyadic weight scale permitting a saving in this integral-coordinate +model, and that removing positivity also changes the answer. + +## Complete finite experiment + +PR2484's core `(13,23,35,16,34)` motivated the experiment. We then enumerated +**all 23 induced C5s** in the same 56-plane matching; two different cycle censuses +agree. Each has ten scalar ports. The finite decoder menu is eight coordinate +Gram terms with coefficient 1/4, with each row chosen from these 120 unoriented +norm-four integral E8 roots: + +- eight vectors `2 e_i`; +- the 112 signed weight-four vectors supported on affine hyperplanes of F2^3, + identified up to whole-row sign. + +Every nonorthogonal-plane cross entry must vanish; both ports of the same plane +remain independent. The cost uses all dimensions of every touched plane. +There are 16 distinct tariff tables up to cycle rotations and reversal. Exact +integer backtracking exhausts both first-root symmetry classes at cost at most +19 for every table. Each cycle has an explicit five-axis cost-20 witness. Thus +**20 is the minimum inside this finite menu**, not the minimum among all +rational decoders. + +The search proof, symmetry justification and stopping rule are in +[SEARCH.md](SEARCH.md). [RESULT.json](RESULT.json) records every cycle, its +class, exact tariff table, anchor and completed node/prune counts. A separately +written C++ implementation derives adjacency from the physical labels and +checks all 46 cycle/anchor cases, without the class reduction. OR-Tools 9.14 +also reported infeasibility on the original core, but is not a replay dependency +or the basis of the certificate. + +The initial signed half-weight, support-at-most-four MILP ran for 120 seconds, +found cost 20, and retained lower bound 13. That run was **inconclusive**. It is +not included in the completed exclusion. The evidence-driven pivot was to the +quarter-integral E8 menu, with an exact exhaustive implementation. + +## Reproduce + +Python 3.12, standard library only, typically about one minute: + +```sh +python3.12 -I -B research/c5-dyadic-decoder-gate/verify.py +``` + +Expected: `PASS_C5_DYADIC_DECODER_GATE`, 23 cycles, minimum 20, E8 controls 72/81, +and `no_new_kappa`. Default replay is read-only. The optional independent check +requires g++ with C++20 support: + +```sh +python3.12 -I -B research/c5-dyadic-decoder-gate/independent.py +``` + +It prints `PASS_INDEPENDENT_C5_SEARCH ... minimum=20`. This is exact finite +search corroboration and a written proof, not proof-assistant verification. + +## Sources, scope and credit + +Scientific base: `31452ecd309f32a97e2e84214719b21297a59018`, priority revision 5, seed **24**. +Pre-submission canonical main: `6ca6f217708b075814de409ad693fea9a2aaa760`; +guidance, selected record and the consumed frozen inputs are unchanged. +The selected #1094 certificate and all 1,579 manifest inputs were authenticated; +its actual construction/review were followed. The reviewed κ was +`0.001672660197076918`; the pending #2766/#2767 claims were approximately +`0.001717256973467002`. No pending claim was treated as admitted. + +The small `inputs/` directory preserves the exact PR1825 matching and compressed +bytes of the selected archive's DATA-PHASES member. Authentication checks the +uncompressed original SHA256 before parsing. [SOURCES.json](SOURCES.json) binds +provenance, archive/member identities, source heads and attribution. + +Credit Cinna Davis (PR1825/2126), Adam Gall (PR1889 strict mask), ywz65 (PR2471), +Sagar Thakrar (PR2484 C5 core/minrank), Jeremy Diviney (PR2203 full payload bill), +Philippe Van Velzen (full-space tariff, 2-integral and coverage-law work), and +flyingviper (PR2757's different triad-mask rational floors). The selected E8 +geometry, compiler and supplier lineage retain their credit. This theorem is +about positive half-integral **Gram** factors; it neither repeats nor extends +Philippe's all-decoder 2-integral theorem without those additional hypotheses. + +New proof, searches and checks: Tekalign (`tekuuu`), with substantial OpenAI Codex +assistance. No independent human review is claimed. Apache-2.0; upstream and +frozen predecessor packages are unchanged. + +## Open next questions + +1. Can signed half-weight or asymmetric factors beat 20 on these physical C5s? + The theorem excludes neither. Start with one exact full-cost identity and + retain every cancellation term; the earlier MILP is unresolved. +2. Can a different quarter-integral menu or changed matching improve the cost? + This census closes only the specified 120-root menu on this matching. +3. A favorable scalar fit would still need the complete native gather/copy/ + scatter/restoration, hosting, precision and other-supplier budget. None is + supplied here; the failed gate justifies stopping before that expansion. diff --git a/research/c5-dyadic-decoder-gate/RESULT.json b/research/c5-dyadic-decoder-gate/RESULT.json new file mode 100644 index 0000000000..45207e5643 --- /dev/null +++ b/research/c5-dyadic-decoder-gate/RESULT.json @@ -0,0 +1,1439 @@ +{ + "coefficient": "1/4", + "completed_anchor_searches": 32, + "controls": [ + "forbidden_cross_entry", + "missing_diagonal_payload", + "wrong_common_normalization", + "support_only_half_invoice", + "underpricing_search_sensitivity" + ], + "core_ports": [ + 21, + 16, + 41, + 29, + 69, + 57, + 35, + 22, + 64, + 54 + ], + "cost_classes": [ + { + "members": [ + { + "index": 13, + "order": [ + 23, + 54, + 26, + 6, + 13 + ] + } + ], + "prices": [ + 0, + 2, + 2, + 4, + 2, + 3, + 4, + 5, + 2, + 3, + 3, + 6, + 4, + 6, + 5, + 8, + 2, + 4, + 3, + 5, + 4, + 6, + 6, + 7, + 4, + 5, + 6, + 8, + 6, + 7, + 7, + 8 + ], + "searches": [ + { + "anchor": 0, + "cap": 19, + "found": false, + "nodes": 159950, + "prunes": 112613, + "witness": null + }, + { + "anchor": 8, + "cap": 19, + "found": false, + "nodes": 4825, + "prunes": 2291, + "witness": null + } + ] + }, + { + "members": [ + { + "index": 0, + "order": [ + 6, + 4, + 10, + 3, + 13 + ] + }, + { + "index": 22, + "order": [ + 55, + 14, + 24, + 47, + 18 + ] + } + ], + "prices": [ + 0, + 2, + 2, + 4, + 2, + 3, + 4, + 5, + 2, + 3, + 3, + 6, + 4, + 6, + 5, + 8, + 2, + 4, + 4, + 6, + 4, + 5, + 5, + 8, + 4, + 5, + 6, + 7, + 6, + 8, + 8, + 9 + ], + "searches": [ + { + "anchor": 0, + "cap": 19, + "found": false, + "nodes": 159950, + "prunes": 112613, + "witness": null + }, + { + "anchor": 8, + "cap": 19, + "found": false, + "nodes": 4825, + "prunes": 2291, + "witness": null + } + ] + }, + { + "members": [ + { + "index": 3, + "order": [ + 23, + 12, + 10, + 3, + 13 + ] + } + ], + "prices": [ + 0, + 2, + 2, + 4, + 2, + 3, + 4, + 5, + 2, + 3, + 3, + 6, + 4, + 6, + 5, + 8, + 2, + 4, + 4, + 6, + 4, + 5, + 6, + 7, + 4, + 5, + 6, + 7, + 6, + 8, + 7, + 8 + ], + "searches": [ + { + "anchor": 0, + "cap": 19, + "found": false, + "nodes": 159950, + "prunes": 112613, + "witness": null + }, + { + "anchor": 8, + "cap": 19, + "found": false, + "nodes": 4825, + "prunes": 2291, + "witness": null + } + ] + }, + { + "members": [ + { + "index": 14, + "order": [ + 6, + 13, + 34, + 54, + 26 + ] + }, + { + "index": 20, + "order": [ + 34, + 13, + 23, + 35, + 16 + ] + } + ], + "prices": [ + 0, + 2, + 2, + 4, + 2, + 3, + 4, + 5, + 2, + 3, + 3, + 6, + 4, + 6, + 5, + 8, + 2, + 4, + 4, + 6, + 4, + 6, + 4, + 7, + 4, + 5, + 6, + 7, + 6, + 7, + 7, + 8 + ], + "searches": [ + { + "anchor": 0, + "cap": 19, + "found": false, + "nodes": 159950, + "prunes": 112613, + "witness": null + }, + { + "anchor": 8, + "cap": 19, + "found": false, + "nodes": 4825, + "prunes": 2291, + "witness": null + } + ] + }, + { + "members": [ + { + "index": 1, + "order": [ + 6, + 13, + 3, + 10, + 7 + ] + }, + { + "index": 8, + "order": [ + 18, + 3, + 13, + 22, + 55 + ] + } + ], + "prices": [ + 0, + 2, + 2, + 4, + 2, + 3, + 4, + 5, + 2, + 3, + 4, + 5, + 4, + 6, + 6, + 8, + 2, + 4, + 4, + 6, + 4, + 6, + 6, + 7, + 4, + 5, + 5, + 8, + 6, + 7, + 7, + 8 + ], + "searches": [ + { + "anchor": 0, + "cap": 19, + "found": false, + "nodes": 159950, + "prunes": 112613, + "witness": null + }, + { + "anchor": 8, + "cap": 19, + "found": false, + "nodes": 4825, + "prunes": 2291, + "witness": null + } + ] + }, + { + "members": [ + { + "index": 9, + "order": [ + 6, + 13, + 23, + 12, + 4 + ] + } + ], + "prices": [ + 0, + 2, + 2, + 4, + 2, + 3, + 4, + 5, + 2, + 3, + 4, + 6, + 4, + 6, + 6, + 7, + 2, + 4, + 4, + 6, + 4, + 6, + 4, + 7, + 4, + 5, + 6, + 7, + 6, + 7, + 6, + 7 + ], + "searches": [ + { + "anchor": 0, + "cap": 19, + "found": false, + "nodes": 159950, + "prunes": 112613, + "witness": null + }, + { + "anchor": 8, + "cap": 19, + "found": false, + "nodes": 4825, + "prunes": 2291, + "witness": null + } + ] + }, + { + "members": [ + { + "index": 15, + "order": [ + 10, + 12, + 21, + 44, + 7 + ] + } + ], + "prices": [ + 0, + 2, + 2, + 4, + 2, + 3, + 4, + 5, + 2, + 4, + 3, + 5, + 4, + 5, + 5, + 8, + 2, + 4, + 4, + 6, + 4, + 5, + 4, + 7, + 4, + 6, + 5, + 7, + 6, + 7, + 7, + 9 + ], + "searches": [ + { + "anchor": 0, + "cap": 19, + "found": false, + "nodes": 157022, + "prunes": 110717, + "witness": null + }, + { + "anchor": 8, + "cap": 19, + "found": false, + "nodes": 2101, + "prunes": 1301, + "witness": null + } + ] + }, + { + "members": [ + { + "index": 11, + "order": [ + 6, + 7, + 49, + 22, + 13 + ] + }, + { + "index": 12, + "order": [ + 6, + 26, + 49, + 22, + 13 + ] + } + ], + "prices": [ + 0, + 2, + 2, + 4, + 2, + 3, + 4, + 5, + 2, + 4, + 4, + 4, + 4, + 5, + 6, + 7, + 2, + 4, + 4, + 6, + 4, + 5, + 4, + 7, + 4, + 6, + 4, + 8, + 6, + 7, + 8, + 9 + ], + "searches": [ + { + "anchor": 0, + "cap": 19, + "found": false, + "nodes": 157022, + "prunes": 110717, + "witness": null + }, + { + "anchor": 8, + "cap": 19, + "found": false, + "nodes": 2101, + "prunes": 1301, + "witness": null + } + ] + }, + { + "members": [ + { + "index": 21, + "order": [ + 30, + 24, + 14, + 33, + 28 + ] + } + ], + "prices": [ + 0, + 2, + 2, + 4, + 2, + 3, + 4, + 5, + 2, + 4, + 4, + 4, + 4, + 5, + 6, + 7, + 2, + 4, + 4, + 6, + 4, + 5, + 6, + 7, + 4, + 6, + 5, + 7, + 6, + 7, + 7, + 7 + ], + "searches": [ + { + "anchor": 0, + "cap": 19, + "found": false, + "nodes": 157022, + "prunes": 110717, + "witness": null + }, + { + "anchor": 8, + "cap": 19, + "found": false, + "nodes": 2101, + "prunes": 1301, + "witness": null + } + ] + }, + { + "members": [ + { + "index": 10, + "order": [ + 12, + 21, + 44, + 7, + 4 + ] + } + ], + "prices": [ + 0, + 2, + 2, + 4, + 2, + 3, + 4, + 5, + 2, + 4, + 4, + 4, + 4, + 5, + 6, + 7, + 2, + 4, + 4, + 6, + 4, + 5, + 6, + 8, + 4, + 6, + 4, + 8, + 6, + 7, + 6, + 9 + ], + "searches": [ + { + "anchor": 0, + "cap": 19, + "found": false, + "nodes": 157022, + "prunes": 110717, + "witness": null + }, + { + "anchor": 8, + "cap": 19, + "found": false, + "nodes": 2101, + "prunes": 1301, + "witness": null + } + ] + }, + { + "members": [ + { + "index": 16, + "order": [ + 24, + 47, + 43, + 7, + 10 + ] + }, + { + "index": 17, + "order": [ + 10, + 12, + 23, + 35, + 16 + ] + } + ], + "prices": [ + 0, + 2, + 2, + 4, + 2, + 3, + 4, + 5, + 2, + 4, + 4, + 6, + 4, + 5, + 6, + 7, + 2, + 4, + 4, + 6, + 4, + 5, + 6, + 7, + 4, + 6, + 6, + 8, + 6, + 7, + 8, + 9 + ], + "searches": [ + { + "anchor": 0, + "cap": 19, + "found": false, + "nodes": 157022, + "prunes": 110717, + "witness": null + }, + { + "anchor": 8, + "cap": 19, + "found": false, + "nodes": 2101, + "prunes": 1301, + "witness": null + } + ] + }, + { + "members": [ + { + "index": 18, + "order": [ + 23, + 12, + 10, + 16, + 54 + ] + }, + { + "index": 19, + "order": [ + 39, + 31, + 28, + 10, + 14 + ] + } + ], + "prices": [ + 0, + 2, + 2, + 4, + 2, + 3, + 4, + 5, + 2, + 4, + 4, + 6, + 4, + 5, + 6, + 7, + 2, + 4, + 4, + 6, + 4, + 5, + 6, + 8, + 4, + 6, + 5, + 7, + 6, + 7, + 7, + 9 + ], + "searches": [ + { + "anchor": 0, + "cap": 19, + "found": false, + "nodes": 157022, + "prunes": 110717, + "witness": null + }, + { + "anchor": 8, + "cap": 19, + "found": false, + "nodes": 2101, + "prunes": 1301, + "witness": null + } + ] + }, + { + "members": [ + { + "index": 4, + "order": [ + 14, + 10, + 3, + 18, + 55 + ] + } + ], + "prices": [ + 0, + 2, + 2, + 4, + 2, + 4, + 4, + 6, + 2, + 4, + 4, + 4, + 4, + 5, + 6, + 7, + 2, + 4, + 4, + 6, + 4, + 6, + 5, + 7, + 4, + 6, + 6, + 6, + 6, + 7, + 7, + 7 + ], + "searches": [ + { + "anchor": 0, + "cap": 19, + "found": false, + "nodes": 152806, + "prunes": 108773, + "witness": null + }, + { + "anchor": 8, + "cap": 19, + "found": false, + "nodes": 1381, + "prunes": 932, + "witness": null + } + ] + }, + { + "members": [ + { + "index": 5, + "order": [ + 3, + 13, + 34, + 16, + 10 + ] + } + ], + "prices": [ + 0, + 2, + 2, + 4, + 2, + 4, + 4, + 6, + 2, + 4, + 4, + 4, + 4, + 5, + 6, + 7, + 2, + 4, + 4, + 6, + 4, + 6, + 6, + 8, + 4, + 6, + 5, + 7, + 6, + 7, + 7, + 9 + ], + "searches": [ + { + "anchor": 0, + "cap": 19, + "found": false, + "nodes": 152806, + "prunes": 108773, + "witness": null + }, + { + "anchor": 8, + "cap": 19, + "found": false, + "nodes": 1381, + "prunes": 932, + "witness": null + } + ] + }, + { + "members": [ + { + "index": 2, + "order": [ + 7, + 10, + 3, + 38, + 44 + ] + } + ], + "prices": [ + 0, + 2, + 2, + 4, + 2, + 4, + 4, + 6, + 2, + 4, + 4, + 5, + 4, + 6, + 6, + 7, + 2, + 4, + 4, + 6, + 4, + 5, + 6, + 7, + 4, + 6, + 6, + 7, + 6, + 7, + 7, + 7 + ], + "searches": [ + { + "anchor": 0, + "cap": 19, + "found": false, + "nodes": 152806, + "prunes": 108773, + "witness": null + }, + { + "anchor": 8, + "cap": 19, + "found": false, + "nodes": 1381, + "prunes": 932, + "witness": null + } + ] + }, + { + "members": [ + { + "index": 6, + "order": [ + 10, + 24, + 47, + 18, + 3 + ] + }, + { + "index": 7, + "order": [ + 10, + 30, + 34, + 13, + 3 + ] + } + ], + "prices": [ + 0, + 2, + 2, + 4, + 2, + 4, + 4, + 6, + 2, + 4, + 4, + 5, + 4, + 6, + 6, + 7, + 2, + 4, + 4, + 6, + 4, + 6, + 6, + 8, + 4, + 6, + 6, + 7, + 6, + 8, + 8, + 9 + ], + "searches": [ + { + "anchor": 0, + "cap": 19, + "found": false, + "nodes": 152806, + "prunes": 108773, + "witness": null + }, + { + "anchor": 8, + "cap": 19, + "found": false, + "nodes": 1381, + "prunes": 932, + "witness": null + } + ] + } + ], + "cycles": [ + [ + 3, + 10, + 4, + 6, + 13 + ], + [ + 3, + 10, + 7, + 6, + 13 + ], + [ + 3, + 10, + 7, + 44, + 38 + ], + [ + 3, + 10, + 12, + 23, + 13 + ], + [ + 3, + 10, + 14, + 55, + 18 + ], + [ + 3, + 10, + 16, + 34, + 13 + ], + [ + 3, + 10, + 24, + 47, + 18 + ], + [ + 3, + 10, + 30, + 34, + 13 + ], + [ + 3, + 13, + 22, + 55, + 18 + ], + [ + 4, + 6, + 13, + 23, + 12 + ], + [ + 4, + 7, + 44, + 21, + 12 + ], + [ + 6, + 7, + 49, + 22, + 13 + ], + [ + 6, + 13, + 22, + 49, + 26 + ], + [ + 6, + 13, + 23, + 54, + 26 + ], + [ + 6, + 13, + 34, + 54, + 26 + ], + [ + 7, + 10, + 12, + 21, + 44 + ], + [ + 7, + 10, + 24, + 47, + 43 + ], + [ + 10, + 12, + 23, + 35, + 16 + ], + [ + 10, + 12, + 23, + 54, + 16 + ], + [ + 10, + 14, + 39, + 31, + 28 + ], + [ + 13, + 23, + 35, + 16, + 34 + ], + [ + 14, + 24, + 30, + 28, + 33 + ], + [ + 14, + 24, + 47, + 18, + 55 + ] + ], + "escape_controls": { + "binary_quotient_dimension": 9, + "line_ports": 120, + "quarter_positive_cost": 72, + "signed_half_cost": 81 + }, + "minimum_cost_each_cycle": 20, + "pins": { + "DATA-PHASES.json.gz": "c5916ff312678f12aba403847643fbbc29f643acec60bdf836fa56cd3e8251fa", + "MATCHING.json": "4fd648f7b5178bff5441bf364d58234b7bc1a43b924bc6da03013c948f1473b1" + }, + "port_count_per_cycle": 10, + "positive_half_fixtures": [ + [ + 2, + 2, + 1, + 2 + ], + [ + 2, + 2, + 2, + 4 + ], + [ + 2, + 2, + 3, + 6 + ], + [ + 3, + 6, + 1, + 6 + ], + [ + 3, + 6, + 2, + 12 + ], + [ + 3, + 6, + 3, + 18 + ], + [ + 4, + 12, + 1, + 12 + ], + [ + 4, + 12, + 2, + 24 + ], + [ + 4, + 12, + 3, + 36 + ], + [ + 5, + 20, + 1, + 20 + ], + [ + 5, + 20, + 2, + 40 + ], + [ + 5, + 20, + 3, + 60 + ], + [ + 6, + 30, + 1, + 30 + ], + [ + 6, + 30, + 2, + 60 + ], + [ + 6, + 30, + 3, + 90 + ], + [ + 7, + 42, + 1, + 42 + ], + [ + 7, + 42, + 2, + 84 + ], + [ + 7, + 42, + 3, + 126 + ] + ], + "root_count": 120, + "schema_version": 1, + "status": "SCOPED_NEGATIVE_RESULT_NO_NEW_KAPPA" +} diff --git a/research/c5-dyadic-decoder-gate/SEARCH.md b/research/c5-dyadic-decoder-gate/SEARCH.md new file mode 100644 index 0000000000..894926096e --- /dev/null +++ b/research/c5-dyadic-decoder-gate/SEARCH.md @@ -0,0 +1,54 @@ +# Exact finite-search scope and completeness + +The scientific source pins and row menu are fixed in README/RESULT. Enumerating +all 56-choose-5 subsets whose induced degrees are two recovers 23 C5s. On five +vertices, a simple graph with every degree two must be a single five-cycle. +A separately implemented path enumeration gives the identical sets and orders. + +For each cycle, all 32 plane-subset tariffs are computed by binary elimination +on the complete two-vector bases. Rotations and reversal preserve the scalar +cycle mask. Cases are grouped only when one such permutation makes their entire +tariff tables identical. All 23 cases are represented by 16 tables; the C++ +checker skips this reduction and checks all 23 directly. + +The E8 row domain has two coordinate-symmetry orbits: axes and affine +hyperplane-supported rows. Affine permutations of F2^3 are transitive on points +and hyperplanes. Coordinate sign changes realize all sign choices, and whole-row +sign changes preserve the forced zeros, diagonals and supports. These operations +permute or sign the eight coordinate factors, leaving their summed tariff +unchanged. Therefore the first port can be anchored to root 0 (an axis) or root +8 (the first signed hyperplane root). + +The two scalar ports within each plane can also be interchanged: the required +mask and complete plane tariff are unchanged. We enforce increasing root indices +within a plane. To justify this with the anchor reduction, choose an axis port +first when the first plane contains one; this maps to root 0. If both are +hyperplane roots, either can be mapped to root 8, the lowest index of that orbit. +Other planes can then be sorted freely. Equal roots on one plane cannot fit its +zero off-diagonal, so no equality case is omitted. + +A state contains exact bitsets of still-possible roots and the current set of +planes using each coordinate. Adding a root enlarges each relevant binary +space. Pairing rank on a subspace cannot decrease when the subspace grows, +because its Gram matrix is a submatrix of the larger Gram matrix (or a pulled +back restriction in redundant bases). Hence the current price is a lower bound +on every completion. The search removes a root only if that lower bound exceeds +19, an already assigned forced scalar inner product is nonzero, or the proved +within-plane ordering is violated. It branches over every remaining root of a +chosen unassigned port. Empty domains reject; complete assignments are checked +as witnesses. There is no floating point, random stopping, timeout or heuristic +exclusion in this replay. Seed24 selected the initial object; the final census +is deterministic and exhaustive in its declared finite domain. + +All branches finish without a cost-19 witness. Five axis columns always give a +cost-20 fitting matrix: assign the two ports of plane i to axes i-1 and i modulo +five. Every axis touches two orthogonal planes and costs four. The fitting rank +is five, crediting the predecessor's C5 construction rather than claiming a new +minrank. The exact complete cost is 20. + +The generic replay uses only the Python search. The optional independent C++ +search is separately written and derives each constrained pair from the ten +actual binary labels, whereas the Python search uses the verified abstract C5 +mask. Both retain every plane dimension and agree on exclusion and a cost-20 +positive control. Neither establishes an impossibility for arbitrary rational +factors, changed row menus or other matchings. diff --git a/research/c5-dyadic-decoder-gate/SOURCES.json b/research/c5-dyadic-decoder-gate/SOURCES.json new file mode 100644 index 0000000000..d8169efd25 --- /dev/null +++ b/research/c5-dyadic-decoder-gate/SOURCES.json @@ -0,0 +1,60 @@ +{ + "schema_version": 1, + "base_commit": "31452ecd309f32a97e2e84214719b21297a59018", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "889b95d936746df124872133ae1e7cc339adcb92", + "sha256": "7d185cd8c2af35988d638d969748ad7b670f902606444dbfc748e4402c340df6" + }, + { + "path": "research/paired-plane-scalar-mask-obstruction/PR1825-CERTIFICATE.json", + "usage": "provenance", + "git_blob": "7ca668d7d50c7276e89b0f6f9575e1b9f1ad9ef6", + "sha256": "4fd648f7b5178bff5441bf364d58234b7bc1a43b924bc6da03013c948f1473b1" + }, + { + "path": "research/community-frontier1094-audit/selected-replay.tar.gz", + "usage": "provenance", + "git_blob": "c24daf067f9c543421d89ca2eeaa4eb78a57fb6f", + "sha256": "f1da80610bf33c58527f18ad63b4350d0b864e1d4486141ee17ac9bed4d529d6" + } + ], + "vendored_members": [ + { + "path": "inputs/DATA-PHASES.json.gz", + "source_archive": "research/community-frontier1094-audit/selected-replay.tar.gz", + "archive_member": "candidate/strict/global/base/work/complex-nine-native/DATA-PHASES.json", + "uncompressed_sha256": "c5916ff312678f12aba403847643fbbc29f643acec60bdf836fa56cd3e8251fa" + }, + { + "path": "inputs/MATCHING.json", + "source_path": "research/paired-plane-scalar-mask-obstruction/PR1825-CERTIFICATE.json", + "sha256": "4fd648f7b5178bff5441bf364d58234b7bc1a43b924bc6da03013c948f1473b1" + } + ], + "read_predecessors": [ + { + "pr": 2484, + "head": "4823273c8163e4c72472bdf7d42202e2c12d2e46", + "scope": "C5 core and minrank proof; no code imported" + }, + { + "pr": 2757, + "head": "1c7bdd4575137b3334adb185ec8f7efb63584b9e", + "scope": "different triad-mask rational floors; no code imported" + }, + { + "pr": 2203, + "head": "c3c85ea8c226640334b1d2246071f230d81cc137", + "scope": "full two-payload price and retained physical obligations" + } + ] +} diff --git a/research/c5-dyadic-decoder-gate/TASK.json b/research/c5-dyadic-decoder-gate/TASK.json new file mode 100644 index 0000000000..07709a56b4 --- /dev/null +++ b/research/c5-dyadic-decoder-gate/TASK.json @@ -0,0 +1,118 @@ +{ + "schema_version": 1, + "task_id": "complex-new-helper-inventory", + "priority_revision": 5, + "base_commit": "31452ecd309f32a97e2e84214719b21297a59018", + "original_card": { + "id": "complex-new-helper-inventory", + "question": "Can a new local cost interface change the deficit-to-recursive-cost ratio beyond current packing?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/complex-local-word-ceiling/README.md", + "research/heterogeneous-owner-assembly/README.md", + "certificates/selected-result.json", + "research/selected-k8-unrestricted-ends/README.md" + ], + "methods": [ + "Propose a changed helper inventory and derive an optimistic exact moment.", + "Design a small completed instance and independently verify its endpoint and rank bill." + ], + "acceptance_gate": "A new physically realizable contract outside the frozen catalogue whose per-call profile, screened with ceiling.ceiling(), beats the selected word's packing ceiling; a lower cap does not establish identical circuitry or order attainable optima, and is insufficient to pass the stronger-budget target under this model. 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.", + "bottleneck_link": "Packing of the selected word is capped at +0.87% (ceiling model); only a lower local excess spend or a changed coverage law raises the cap.", + "allowed_variations": [ + "Narrow to one changed boundary or helper type with explicit counts.", + "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": [ + "Mixing only providers already inside the pinned catalogue.", + "Only changing helper terminal subspaces and monotone frames within the fixed scalar word, entrances and cleanup contract already covered by #1995/#2013.", + "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": [ + "helper inventory", + "heterogeneous-owner", + "mutable leaver" + ] + }, + "scope_status": "changed", + "actual_scope": "Prove a general positive half-integral Gram tariff floor, and test quarter-integral E8 cancellation on all 23 C5s of the pinned matching.", + "scope_change_reason": "The supplier-design attempt stopped at an unfavorable complete local cost gate. The contribution is a structural theorem and exact finite exclusion, not an admitted changed supplier.", + "bottleneck_link": "A coverage-law improvement needs a decoder costing less than the unpaid port dimensions. The theorem rejects an entire positive half-integral Gram class even before native overhead; the quarter escape prevents overgeneralization.", + "budget_minutes": 60, + "stop_rule": "One 120-second signed half-weight MILP, then one evidence-driven pivot to the finite E8 quarter menu. Complete all branches at cap 19; stop supplier expansion when every minimum remains 20.", + "outcome": "negative-result", + "evidence": "PROOF.md and RESULT.json; independent C++ search; source/mask/tariff controls; no full supplier replay or new kappa.", + "author": "Tekalign (tekuuu), with substantial OpenAI Codex assistance", + "ai_assistance": "Substantial OpenAI Codex assistance in investigation, proof, implementation and checks; no subagents or human review claimed.", + "open_questions": [ + { + "question": "Can signed half-weight or asymmetric factors beat the full C5 cost 20?", + "why_it_matters": "These hypotheses evade the general proof and could change coverage budgets.", + "first_step": "Give one exact local fit with every full port-space tariff; the initial MILP was inconclusive.", + "blocked_by": "No favorable exact identity; native implementation would remain additional." + }, + { + "question": "Can another row menu or matching improve the quarter-weight cost?", + "why_it_matters": "The finite exclusion is specific to 120 roots and one matching.", + "first_step": "State a changed menu or physical plane arrangement before new search.", + "blocked_by": "No general rational-decoder impossibility theorem is established." + } + ], + "assignment_seed": 24, + "catalogue_nonce": "1a50b3cc9f973470a2360b5027f8045a", + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1587#discussioncomment-18958959", + "initial_search": { + "coefficient_twice_values": [ + -2, + -1, + 1, + 2 + ], + "max_support": 4, + "vectors": 2260, + "time_limit_seconds": 120, + "solver": "SciPy 1.18.1 / HiGHS", + "best_exact_cost": 20, + "reported_dual_bound": 13, + "result": "time limit, inconclusive" + }, + "family_expansion_decision": { + "boundary": "strict scalar mask on actual paired planes, arbitrary scalar inputs, all complete port spaces included in each rank tariff", + "proved_cost": "minimum 20 in finite quarter E8 menu; at least sum dimensions in general positive-half Gram class", + "unknown_costs": [ + "native frame route", + "source access and copied payloads", + "restoration", + "hosting and idle work", + "precision and recursive children", + "other supplier improvements" + ], + "decision": "stop this expansion; no complete supplier or kappa claimed" + }, + "freshness": { + "canonical_main": "6ca6f217708b075814de409ad693fea9a2aaa760", + "checked_utc": "2026-10-15T21:46:00Z", + "priority_revision": 5, + "guidance_selected_record_unchanged": true, + "new_review": "community-efficient1300-review; 71 merged scoped contributions; selected exponent unchanged", + "open_pr_snapshot_count": 717, + "open_pr_snapshot_max_number": 2779, + "discussion_scope": "Fresh Discussion1587 comments; earlier complete cached helper snapshot was stale after a network timeout; no novelty guarantee", + "decision": "Retain immutable scientific base and source fixtures; add-only package compatible with refreshed main" + }, + "baseline_checks": [ + "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "PASS_COMPLEX_LOCAL_WORD_CEILING" + ] +} diff --git a/research/c5-dyadic-decoder-gate/VERIFY.json b/research/c5-dyadic-decoder-gate/VERIFY.json new file mode 100644 index 0000000000..7d1405f65a --- /dev/null +++ b/research/c5-dyadic-decoder-gate/VERIFY.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 300, + "checks": "Exact source authentication, 23-cycle census, complete integer C5 searches, sharp positive controls and explicit quarter/signed-half escapes." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/test_package.py" + ], + "timeout_seconds": 60, + "checks": "Source corruption before parsing, valid recompression, both full plane dimensions, endpoint/sign controls and receipt type controls." + } + ] +} diff --git a/research/c5-dyadic-decoder-gate/algebra.py b/research/c5-dyadic-decoder-gate/algebra.py new file mode 100644 index 0000000000..88f99999c4 --- /dev/null +++ b/research/c5-dyadic-decoder-gate/algebra.py @@ -0,0 +1,157 @@ +"""Exact algebra for the scoped decoder gate. Tekalign; Apache-2.0; AI-assisted.""" +from itertools import combinations, product + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def rank(rows): + pivots = {} + for value in rows: + while value: + pivot = value.bit_length() - 1 + if pivot in pivots: + value ^= pivots[pivot] + else: + pivots[pivot] = value + break + return len(pivots) + + +def dot(a, b): + return (a & b).bit_count() % 2 + + +def pairing(left, right): + return rank([sum(dot(x, y) << j for j, y in enumerate(right)) for x in left]) + + +def costs_for(planes): + result = [] + for mask in range(32): + basis = [x for i, plane in enumerate(planes) if mask >> i & 1 for x in plane] + result.append(pairing(basis, basis)) + return result + + +def roots_e8(): + """120 unoriented integral norm-four E8 roots in a scaled coordinate chart.""" + roots = [] + for i in range(8): + row = [0] * 8 + row[i] = 2 + roots.append(row) + quads = sorted({tuple(x for x in range(8) if dot(x, a) == b) + for a in range(1, 8) for b in (0, 1)}) + for quad in quads: + for signs in product((-1, 1), repeat=3): + row = [0] * 8 + for i, sign in zip(quad, (1,) + signs): + row[i] = sign + roots.append(row) + need(len(roots) == 120 and len({tuple(r) for r in roots}) == 120, 'root menu') + need(all(sum(x*x for x in row) == 4 for row in roots), 'norm-four menu') + return roots + + +def scalar_gram(rows, signs=None): + signs = signs if signs is not None else [1] * len(rows[0]) + return [[sum(s*x*y for s, x, y in zip(signs, u, v)) for v in rows] for u in rows] + + +def check_fit(rows, planes, denominator=4): + matrix = scalar_gram(rows) + for i in range(len(rows)): + for j in range(len(rows)): + if i == j or any(dot(a, b) for a in planes[i//2] for b in planes[j//2]): + need(matrix[i][j] == (denominator if i == j else 0), 'scalar mask') + prices = costs_for(planes) + charges = [prices[sum(1 << g for g in range(5) + if rows[2*g][k] or rows[2*g+1][k])] + for k in range(len(rows[0]))] + return charges + + +def baseline(planes): + rows = [] + for i in range(5): + for k in ((i-1) % 5, i): + row = [0] * 8 + row[k] = 2 + rows.append(row) + need(sum(check_fit(rows, planes)) == 20, 'five-axis positive control') + return rows + + +def tariff_from_matrix(rows, binary): + charges = [] + for k in range(len(rows[0])): + indices = [i for i, row in enumerate(rows) if row[k]] + charges.append(rank([sum(binary[i][j] << t for t, j in enumerate(indices)) + for i in indices])) + return charges + + +def escape_controls(): + # These are inherited E8 geometry, independently generated controls, not new suppliers. + roots = roots_e8() + gram = scalar_gram(roots) + need(all(x % 2 == 0 for row in gram for x in row), 'even E8 products') + binary = [[1 ^ ((x // 2) % 2) for x in row] for row in gram] + need(all(gram[i][i] == 4 and binary[i][i] == 1 for i in range(120)), 'quarter diagonal') + need(all(gram[i][j] == 0 for i in range(120) for j in range(120) + if i != j and binary[i][j]), 'quarter mask') + quarter = tariff_from_matrix(roots, binary) + need(quarter == [9] * 8, 'quarter escape tariff') + # E8 roots in the orthogonal complement of (-3,1,...,1) in I_(8,1). + lorentz = [] + for i, j in combinations(range(8), 2): + row = [0] * 9 + row[i], row[j] = 1, -1 + lorentz.append(row) + for count, height in ((3, 1), (6, 2)): + for indices in combinations(range(8), count): + row = [0] * 9 + row[8] = height + for i in indices: + row[i] = 1 + lorentz.append(row) + for i in range(8): + row = [1] * 9 + row[i], row[8] = 2, 3 + lorentz.append(row) + gram_l = scalar_gram(lorentz, [1] * 8 + [-1]) + binary_l = [[1 ^ (x % 2) for x in row] for row in gram_l] + need(len(lorentz) == 120 and all(gram_l[i][i] == 2 for i in range(120)), 'signed-half diagonal') + need(all(gram_l[i][j] == 0 for i in range(120) for j in range(120) + if i != j and binary_l[i][j]), 'signed-half mask') + signed = tariff_from_matrix(lorentz, binary_l) + need(signed == [9] * 9, 'signed-half escape tariff') + need(rank([sum(x << j for j, x in enumerate(r)) for r in binary]) == 9, 'quarter ambient rank') + need(rank([sum(x << j for j, x in enumerate(r)) for r in binary_l]) == 9, 'signed ambient rank') + return {'quarter_positive_cost': sum(quarter), 'signed_half_cost': sum(signed), + 'line_ports': 120, 'binary_quotient_dimension': 9} + + +def half_fixtures(): + records = [] + for n in range(2, 8): + rows = [] + for i, j in combinations(range(n), 2): + for sign in (-1, 1): + row = [0] * n + row[i], row[j] = 1, sign + rows.append(row) + gram = scalar_gram(rows) + binary = [[int(i == j or gram[i][j] == 0) for j in range(len(rows))] + for i in range(len(rows))] + need(all(gram[i][i] == 2 for i in range(len(rows))), 'half norm') + prices = tariff_from_matrix(rows, binary) + for dim in (1, 2, 3): + # Tensoring the pairing by I_dim multiplies every rank by dim. + cost = dim * sum(prices) + need(cost == dim * len(rows), 'sharp positive-half fixture') + records.append([n, len(rows), dim, cost]) + return records diff --git a/research/c5-dyadic-decoder-gate/independent.cpp b/research/c5-dyadic-decoder-gate/independent.cpp new file mode 100644 index 0000000000..2c1d43c879 --- /dev/null +++ b/research/c5-dyadic-decoder-gate/independent.cpp @@ -0,0 +1,70 @@ +// Tekalign (tekuuu), with substantial OpenAI Codex assistance. Apache-2.0. +// Separately written exact search; input file supplies the ten physical labels. +#include +#include +#include +#include +#include +#include +#include +#include +using namespace std; +using Mask=__uint128_t; +array,120> roots; +array support; +array ortho; +array costs; +array neighbors; +array chosen; +uint64_t nodes=0,leaves=0,prunes=0; +int cap=19; +int indexbit(Mask m){uint64_t lo=(uint64_t)m;return lo?countr_zero(lo):64+countr_zero((uint64_t)(m>>64));} +int pop(Mask m){return popcount((uint64_t)m)+popcount((uint64_t)(m>>64));} +int rankbin(vector rows){arrayb={};int r=0;for(unsigned x:rows){while(x){int k=31-countl_zero(x);if(b[k])x^=b[k];else{b[k]=x;r++;break;}}}return r;} +int price(const array& masks){int s=0;for(auto m:masks)s+=costs[m];return s;} +bool dfs(array domains,array masks,unsigned todo){ + nodes++; if(!todo){leaves++;cout<<"WITNESS cost="<>i&1){ + Mask keep=0,d=domains[i]; + while(d){int r=indexbit(d);d&=d-1;auto nm=masks;for(int k=0;k<8;k++)if(support[r]>>k&1)nm[k]|=1u<<(i/2); + if(price(nm)<=cap)keep|=Mask(1)<>k&1)ms[k]|=1u<<(slot/2); + bool ok=true;unsigned rem=todo&~(1u<>j&1){ + if(neighbors[slot]>>j&1)ds[j]&=ortho[r]; + // Within-plane port interchange leaves this mask and tariff unchanged. + if(j== (slot^1)){ + if(slot%2==0) ds[j]&=~((Mask(1)<<(r+1))-1); + else ds[j]&=(Mask(1)<1?stoi(argv[1]):0; + if(argc>2)cap=stoi(argv[2]); + int n=0;for(int i=0;i<8;i++){roots[n][i]=2;support[n++]=1u<> quads; + for(int a=1;a<8;a++)for(int b=0;b<2;b++){array q={};int j=0;for(int x=0;x<8;x++)if((popcount((unsigned)(a&x))%2)==b)q[j++]=x;quads.push_back(q);} + sort(quads.begin(),quads.end()); + for(auto q:quads)for(int s=0;s<8;s++){roots[n][q[0]]=1;for(int j=1;j<4;j++)roots[n][q[j]]=(s>>(3-j)&1)?1:-1;for(int j:q)support[n]|=1u<,5> planes={{{289,49},{194,134},{304,56},{50,193},{200,196}}}; + if(argc>3){ifstream f(argv[3]);int row=stoi(argv[4]);for(int z=0;z<=row;z++)for(auto &p:planes)for(auto &v:p)if(!(f>>v))return 3;} + for(int m=0;m<32;m++){vector vec;for(int i=0;i<5;i++)if(m>>i&1)for(auto x:planes[i])vec.push_back(x);vector rows;for(auto x:vec){unsigned r=0;for(int j=0;j<(int)vec.size();j++)r|=(popcount(x&vec[j])%2)< ds;ds.fill((Mask(1)<<120)-1);ds[0]=Mask(1)< ms={};chosen.fill(-1); + auto begin=chrono::steady_clock::now();bool found=dfs(ds,ms,1023); + cout<<"RESULT anchor="<> i & 1] + require(bool(options), 'cycle reconstruction') + order.append(min(options)) + cycles.append(order) + require(len(cycles) == 23, 'all 5-subsets cycle count') + total_nodes = 0 + with tempfile.TemporaryDirectory(prefix='c5-independent-') as tmp: + directory = Path(tmp) + binary = directory/'search' + subprocess.run(['g++', '-std=c++20', '-O3', '-Wall', '-Wextra', str(HERE/'independent.cpp'), '-o', str(binary)], check=True, timeout=60) + inputs = directory/'planes.txt' + inputs.write_text(''.join(' '.join(str(x) for i in c for x in planes[i])+'\n' for c in cycles)) + for i in range(23): + for anchor in (0, 8): + completed = subprocess.run([str(binary), str(anchor), '19', str(inputs), str(i)], check=True, + capture_output=True, text=True, timeout=30) + require('found=0' in completed.stdout and 'WITNESS' not in completed.stdout, 'independent exclusion') + total_nodes += int(completed.stdout.split(' nodes=')[1].split()[0]) + positive = subprocess.run([str(binary), '0', '20', str(inputs), '0'], check=True, + capture_output=True, text=True, timeout=30) + require('found=1' in positive.stdout and 'WITNESS cost=20' in positive.stdout, 'exact native search positive control') + print(f'PASS_INDEPENDENT_C5_SEARCH cycles=23 anchors=46 nodes={total_nodes} minimum=20') + + +if __name__ == '__main__': + main() diff --git a/research/c5-dyadic-decoder-gate/inputs/DATA-PHASES.json.gz b/research/c5-dyadic-decoder-gate/inputs/DATA-PHASES.json.gz new file mode 100644 index 0000000000000000000000000000000000000000..df8b16392df722c4f1d47c6bc5b18926cdb62556 GIT binary patch literal 24910 zcmb@uWmuNo8a5~*E!{|$lz=oyhk!_jbV`SGNasUHr*wBbq=a;LH%f|hN+ZsFgL`K0 zFW&vl9OI$C{Nv?X>%7joAqzu%1pa#bXTSMFB(b#p=GC2`gl`3PCI|lAvQ9@cLFuOL z<8x;?X_v7*!^A?`k|sC9SOIExj%L4>8v#5;4fAxu&s7ZYIg}2hB)h?o9mO zyzQ&K-Oo1H$qt2@y-trO3vRgezI)yt?Nt0hH5U4Pdv`bZdv{dmTeJ6{>(z`~*FT$j zg00uPf9^h197Qhem!Ojg-B#Sllj(W?LAe`lUGl!R{iA#4@6Ef^a(%fy7)j=RdAWM< zdpF~t#pC0}Ch3oZ6Z~!OeS`exq?&GZdb#y( zbyKK02;SyM@6Txkv99q)74N+}d6y3@U;mtObN@NB(>`pu{dl^0(3x^`k?~P~C+ovMT|OKNtxNoIJpBRuoAd;~#?secQRVNg z7c76hzF2%G^!3jrN&e1HvO~e;)|Q)Joh(A%yf6J+Zb)7qGwS|C=XU*_a&x@>y9xcm zCBx?6d&_Uf$ktQ#yAc+>gZC#tSXK^)Zo^ZSSI>Ih-Ch1x7ed?GZ0%0@bGpuw@!gtyl1wn(jeeV^9_G5w|}}!}rZN(IDqzxj%lb86WhDX5Bq6 z1WLo#sBPFT62B?jmW_Vzc1`j4RlCO0ll-QK%(|P#`QD*AUH?o9bblT>UYc#b~}$%@QcZeL-qS$O=DH5e+FHNNG?v zMAi5{`en}k*jfm6>xAAxPucoK7qu8uc};RktnV6}CekG%fz1m7iGE{Z$B?W#ob0D0 z6^d`3*~cOUm*uLEz%xvaY1%Wpe@ej14rJ~W{lfT`^UmJVA6;-0Q;-unIJ{)7?buEX7po6u%A#u^_N0hmz&9qb8LFjR&#m8-7@1)gMTfcO@Ho za$V>jYgdpZu_a2&gHCG1;$QLt5@g=PiXB7-QAlQap^zQ7<@6>F`6c6qGkbnd%Ilx3 z34C!XFQwUBYOj5~qZM^i8QJ`4dOvwn{1}JOod%D>(NY__#cZGd1Q{CcNYSln^Arxmq)oipWYCZSMGS-83x z*0wPV>Eho;(Pao$6b$cS8w&47l7d5h|I9Bua;K2x%UQe~4<1#3u6ka2mMprH-RzOSk6a2k*QI@-OSpJ8dC_|2vDI=l@gbblcFl^ zN9ycDa?nV^#w#HDg#M~7@X$(yUxw8B1r<|_<09no`Z8{1$J{qEZ>H)qm@^YICA16` zmd2?Wd0*o9&nMm&7oNt>3Mi`h9L)(0D3ee(-Za4MmNFIs&k~&&$-(^BqYSd6SG&8k&MH2!Ei!k zD-*W0Z2ESRL|r4y)n}$+aq#Y>oqHQk6f?vIaD%G!?OVTQ?RgRJ$G&zqZ#X&WrWwo$ zF{6x0o}TFb!8mLt6|R(%8zN504^J(dyF2Ez#kawuLSas+Dus*nKALs{v1Fo)V?sOw zPu?P_iOEId`8uPHVC(Vtg4+2bvBb6y?+o{07$39Iqv`atcz(VTfC}~#1u?quN$9<^ z+8+#qtWL?;u*0XZ9cOkdWH8n64saosq?ddwk1QTqFI!8mvgpuSxf*uiN-E-9%z;mx zGzbf#;BzGtq|T}yw))MRkN7g>1Kry03N>D`V3_v#$oHV~Jv->E$JPGYLCd&k4Ti?B zCU1rdt=*x$dc|XHi&d5DN zHB-uzLVb(iEdEgr-Qv?Bm;Nd#n=TbxX}bF184Bq;B2&^;`Pf@TVd^Pbukc!JErasw z+aF@5-^5(4o8m2zmxEKUP``Drt5;meEq3de=lGhDpCme!JLqhOi!sC@(@;=vu8fl+ z{k>Z$z}-Rw@0M+70C2aWF%q_0RwvqJJY8Df>acV+3#PqB2a&61!ZG`6QQHg=JONP^ z^^Rj;6M)8ZqAGpx_KKc`qFO9b$V7cyPo8BI!aD8PYv~a}j9!Xv!Nn4sm6Fa7m=d6^ z*j=$3MfWTj4(6HO)KAPXp1kQm?}D*C--HifkzGKpo;GE{PF{}<3SFjF)~-I0t=BM1 zSv4WvJ)bDXltt6fNO;(uww$A z;wqPKJg?3RO0H(d#DfE$sju(74&vZO^@iP^;Z|EDxoQ%4I%{6w4xd%Naysw z#jenJ?6orow;^wp{~wTRu@C8Vq6j5S8MOz}yWtOoj_?OdY7HWWQGYwnYP)oiC}nlN z=p`Gp@)T~4d9CojK`wZ>0jIB&P1FKkI~lYhZMB#n_554x=WkEgh0l1E%{}BJ_tS6r zq|oRoSI?@3b`#Uegd|a_1;h-ZtP9=w9lE%)m{Mz4tmrJsB;BV8k2<>Z+Q4@%`gvNZ zEs#-G8GPr|kS;R*6Dr<^6M4_2LeYPJBAU^}z&no-YuMqWWzgnVHrR>*kjn_2Z!F{i zxhQp~8y=8r28|leif?tLWoQ9q=4l`Ot5WM?G98P3B%-Ht--Yef-JBZR{gF?X{0u@R z)kLbQE)-8a)Q$JC`Pro>VYK*Md1@-KUz5H|w#G#95^5`0wKQ(qiQo@T(=pi{{rR%y zIor@>YF<7%T?+PDU9DC97#HWjR2;UrT04o)=g56sq_`%| zhM5kF^?U*VE=LkS;^HWtXn^fVR|R962RPYfr&JMbc25#*GLP!aY+t@f9RJ`^Qx`AW zHkNm^7_aW$7UQEGDwbINLC?esok^i8cvUG~ZekW!>*i$5kmo$+=99>CS^h%k`Ey3= zh${4ss-MN_yEzP}t|gZROewbb^nD`KYs7D{JF`5AE(CItIo z)r+91N~MCUo?4?TgrlR8XFQVUC9^DcPLHIb1HGAqKb>1m?Jo?C9kWFheM_ByfxrkO zK|I3cuW0rO8xHd9szqgFeJvas$PNdeO~7|zl?J`?wOFP8;bTRrGXJsb1P#B)EcgeB zR%yhC5fviSR(<~7T&{9I#@ypXoy4@)uEf?6n11R-Cgv?4j?{ z-XBhM7*7D$Yd&P5v02WpMh##u7D3F%quj{0hXs!@tq}Mm2*h4B34H*2QJ!`pJ{_DG ze;bBosNr}!vJi+xLT3HKsM}N*g6>JjdZ&{_PtmWB&-SZwXhzaD&rc~~27;sty!ZFG zC{^}`)l-2c`vcaV2JI4PBEe%zNBjNAK${56IA;@n}V6t^1!b;1DNC=iswAz zQ950u80nOrW?Dlt8U8^ubL#s{!B9Rd_{J<`Bn%LQ_d*{n zmG*liEw#+3S76Iej%DFy&PlT*n)hH;@b4G=Rc3@bh0=5+bL}~G1WsmZ(n};+CuaqN z^hG|KDqCZ8Io@2Gbo7!Thlm^wD=3k(9R=D^tIZv_-=l^zp`un8G^xd%lG)XRR==-2 zg1ghvU#?Rt+0#3HjD;o6K+Ozl8lQz63-|bDiy7i z8xTrO#g9s@^6>7vcvUE}!2KR$ipem6xGUQID+>4Ji*(#dN4KNUflzgbnyQ+(TTNZ} zt&tsrs;NZkn^FN`83nB{>9a}}_Ew1hW45?QiaUwp-7_tjz3N@;M9>W7W)c^|duF&%^Y>S_1^HgpHKFj?zJ2C1s~iP2E~`mF$a$hjSkhvy zkENod03tc&6l_~4>L*?t#X#LjDV2+<1{dNs0GY$v4DJUPi&4@zpDT$0PGnueI%bs3 zje@@AZ(Fq7MIpTTk8>Xs9G?RuGV*)KR{FL5y4Crv1$Q+>wMRoxo2rRWsJ!NkZ+)h5 z8DQ>L7%8~8YC@#kk9FQ~<<;>EmKd;Kf)WG^lpr$MpadZ|A;E9}BnX-zC_xINzWSSb zhzCAMkSIWc0I*afs>F~DNDx&O_17xu-#QAR@YDJpu0ui~qm` zt?e0k#Nfl5Gt%;f5#YRO^`Y>6F9@8-XFQ9_GPvqFn4Q&$#im3woEq!|VWC7D5&8vH zIL;34>c*)*x!Pt0Zl9G1E+p8DL^6h-MxF|U^oQy_zARU$G{d;ju&HnV)f0-2EGd&6&MEpB>gMvFxK7eEvBx@O=@%z7q*_vOYVSwSrE=7c() zx9CL@E;M)lJ=}&_2FHSoOofZZ$(Iz}NZRZWL`${77cOr+6Vo3>6Xm@|!jYD6#gfYW zd!6hHMITFm*J+SaAs2H7F4TI!TfJlA3SDM`@UW*q$E!u;Zgk*+_X^jgZ_{=L;smAmYR23gz6|#=9a4;r|%ajJ^ zrR;VBo8&lhRU1~#A(yg?^4Y6rLsOdWa$;Ds<(GwRS{sIiEDKzxXQroQ3HmL0Ndr%POn&;njzsnWMN1QiSwEd6?OO?hR7k|RF`|Z)-EFpgkI2Nw-YgZzv!oOoV z6pD)8k2OlE0*nXl?eznMpsx@If9EITN&oEyd`yme`29rojK^0=ai3(XAaS1YQZ z1&D?xQ}sFJ)2i2{)H;2tIu@jgMRIDg!MSIv?{1J!_wuJK!Zfm@47c}8uAu|B5j=t@ z!Gg$toU58;bhKx{(;|Xb_drg%5jhAonME)Mh>N@Y%M{p*Ypy*ssvj|(ou~-JQp_$6 z6%G4KOY8Ti)${~BEq9~{;Ix7*)tX?Pfz$Gm2Tv;mr(ePqPb&9eEJR=|%KNc~DV2b+ zBtmT(3)B}UE^tyNxhH!Hz6tQXO@HU|6F94xRrW}dpjnrVd@M_J%xGS_&&<1m=f;~C zM=K7PJHEwdgIk7{dQxA4ts@Er+f7wIAmGm2?bKJcGe5mU5ZEP+EH3pl)PbDpZ$l8c z>Qi>DSl?Oh6Iu#-5Yagg=_7fB%KII-x7_UsbT15D;Akz8NUoi})U~HWSzfYSL_!!C z*S(;rcQ%ja1YcI0N%JfHeLh$j@MUFD_9M!}BH=!~EIVNH7lJQqLn9y*cv%YL@)tOZ z6YcVLJei02oFrZ~#w5HB0E=;|H-vm>MEiQBV7O1whphPCT=CaI<alm-Xzn3=XM zw(`%kmpZWXB*b^hS|)YiKqhFO$VNq-QVkpA+{Cuz4FvBy-H+?rf* zsvq1ohpe}yt2hn4}b{+~6g1(Hk0 znUUf?*{Zr~+*33(2GJptLPU;6p@^&N z+BV~^nMvjp{@aN)D!i0asLapHGJHWq6)yj33$8>Jt`WR}Vw%ve7A=gG=TVia!u2Y2 z5e2{JdkVNC;?3XT(ckh#&tgdR~x2|uW2j2{4V3k8{5fmi5 zaV|NSNiJ$ooaQAOOQn}PQ^rQUm(UWYCNeeUM(gTwn0_$lw7k1e0F*OjATyLlVj99w zbM}}acri@93i{e)T2ap?Rgy_l!&&+g-74f)D(Mu#GU^2$;{hvQ2y^JCU^)5ow|RD( z*u*kka6Y$1o*0L95x7#0>U4d~4$thXHiTL4hI$cA#_VuXQ=b2UoK(KEu{QE&b(Q4k$8~e*1mg%ceyZ z#bQr_$Lp!oyafyb_c5wW>e=ZDz2Qv!v);fTPqE@q+$8FxKe|Fx>qu9>sH59?j+t5| zZ@BpEIOI=Urjywx#w*3JCL?4J3QaoDbED&ziF=2N@{m2E)oT`OKfG{;&31H9VvSrIa7zreOxT( za-pDaeOT$tBc=3{cqviCy*(L**BDYOdzJ%&vp>w@GbuF2iV+@HKo4lKzCD(5jlH1! zz&Q$0oe^wjkL4hN=J`X!Zum?$?DFREDpxLGJ&0P=;7bpr0_Wz9>+Y-=I`v15lSoEL zQUrtJWS$zgKk;@GBfR5TcpiQ}aq{Cwm`su+Kn=t>OY%MqzDu5t0(U5Ozql(JpfB$U zG$O!w*6s;(KcyT%pu0m1l1>2CjQwnrc~WNv>FQ15sMS}FBUZ{GnZ!vno)El*XqkQ$fZk# zC}nqryr<+xpq6`h_)h?FV|OoZ-eW!o9{!s6g%5UOeu%_+PPV$CoJ5v5|NMe4p&un~ zIA-r-tzCjH*Lt2p%r&v-<3q8MId}a$^J^LvKs-m1$RbsB4b(~Hi0RnuqWF{r%~4}8 zlpk)p36#E!!2IANL5RY4uF+>l(0C0;81k zUNPB*d8NzlD%WQ*Wx)08IPo`YHKd77KMsWa6z*tbo474$+d$1Z4;}q zeHJ?YwYteJRlSlx*VHveRxu!LN)1KSb0I!oG*^mV>9M#HM*1x#`GX~s{j50Z5opQumm^{T zmJE!cYhR!`{%GJ_BeAQj9S;+XEDR5z69Qi!t*VugfjXfh)X=WPf5%YIWFL-^YzmWc zuk3m}ZzjDf`f(h#ojdxt5U#>5f^u$xa`E!|2 z21@0E1H~I45XhM_R_rj}@Y{yr#u<$5^jx!LVV?co9oUn5ubw$$hjq*!DT8K!3N_)X zIeFG!8Z!cz0k|NI;SW;)Xbd4k4+JAWte16IM{2M%C+YF>Hf#O~z@o2u*Hju6@|8ns z5zLS*I(4K-UY}MD-IAgq_bK=VD?vC^|4ltd9JnbM?90~)9CbY!7cEpAJyVQ#`x+%g z{?muXNqg0RO<)h?FYluzW5h0p9B(^_>Y)u*-b8GHW66V_zNR%K)(zK-{{>tw7R#$)VhKIQar~hFCx1> zae)rV%_L(L?vcksxy(u70PMb?=*eqIKL=sgZkrjeOL2PkmUOVRS%12{Dv+~(ch|3R zY9V$Ik%i9!Z?~+49su5b7DG#aRSqNbF6V+RH-I{}Qhk5l)-7t)$0~`*oR10+{W|!T zC#3jXl{%fz;Vy(Kb6paE%k*r9Bl(bYErp#_;tdA}E^^rmg3apO{eY_n$r+aD28ftv zEU^!g69vx=5HY0VasLOB(-_%Ib8P}fR%U{NskcC zsf80}wP(euY`M=%QAw@cw3hSugKz7qQKmJ!o;O#fd5BseV!$ii4}Ejch^+Ahw3GP- z6LRoseOU&tmd5}4tF?=WrKOWZRhJKhd`*L9=7qA~1Y!ZNocPB?h6U)&>{l@M+K5k~|O8CF}*W>;?|To(d`;|zdgl25fbA)LcDE<1ED$B$Io`q!&` z1s&$(G65A`Y-Ez2e7oN>lna>V_MfLkU#BZA=Rr900FSvt3=1Ru8k6(^&Ued7)=CoM3DFEIFaYmp|yil9^-1odC z4gLHXtMDKgybRG!N~U(>>dTxe(EDi1pHG2Jd0Zn%{Q8Yb4J68pCrX=n%G6;I>8yWT z(7YxQkMk6eGTaulV3s*sipOyRXc+-0J?EQnEc%$RBc>>+zi_ar5Ga1n{*xtg0XPW7 zS!adgvhJMll}(w<0xsh>C+@fD%J@tFx1ydD;Vb|ZwTJ?yC;R_GQNsu(JV`}G63hY2 z59s;3-f&cBgCn6WjSE*5AQ#x>OGS_o;)k|>(>C>Q(6k&?KV6*^uAFOHHS(ircCPze zA@ppn26fXt^u=BT)$tVp3vXQDhlASv4fGAOiW@BLrWzFw4oq2b{p#-|Q0KJITZM`i zaSGAz0}6ZtLLbaG9tZ>AeS$oiNmPQ!z_@TL-#yfN+bV>Ic+6!odF0((m0T^ipync< zc4h2`#!XiMv?1h-PZF@wHf+HqgiqByFt@+;D+quN>$ z`YFS?!pD3d(yS)cG%pw4nOjk92%5h?E!0oU>&fPR%bZc)+E;~Yje(rwyRy}$c1Zgx zCj$CJ;*B6!G-`Z*t4juJ_$s>^`Dgoq$HlR+ts1%#0B!5yELlyC-Dz^v76bAd@z4!Q zeiUk@zZwUiI??x3#{`oe@Np?6geWDVpn=hpds&)qO2h^ zMfZ`%SAa(AjlwDRqp~5*g>rx&}J=oIP zj_PRD(^VuxJ@=RJb*Y@}opT5-cn9Z7;jQF~4kvt3!7IoR^XZ5qO5yJn{HYKaaDN5U zB?`gl0JrlAuB9#!!%X(eiOU*)U8tsFrVMGBwLmW1V990^aQO(e-~wb&B>;Q+|4dE8 z&gIX>dTN`dy9JO1`ggjIb&@w8mV!t~$jsH3uSnUu<`A0#p-@={%(qIz;my=g9^WoB zj90x7Sm}lhsF|?Ba$W5EDF5cQzT|>UucrBHFwUtrsnvFx{VW%al_&m>uA&-TsNF!m zI=+1Vobl-7FFNkwQ2Xjy2drCr1zB*#N@A|*O9QP9wmZ)T$Sk~6?M|Ws5QTI+3K_U& z=v6E(Xj$S(jA~8XS1dx+q7bM+;Ha>f zH*y!0g#*SqgQY>nas!8J;}jBaqOnM0e2%6fkN!qfi@-gDfJTRnge!Q@&`%N3k3Dsh zNC8W<$ zlxZbiyqBP2ih#S>(5;zZd>Zg4DlI1cCt&ivqI5It77%{a;uEjxg|da8R>Y}A)qc1k z`M9Hy>)2gm_Z}A%B@nNWL}XyJJe_x#u*l$3C7JR2*gpU*1;|bAs;;K?kcY4DOLMA) z;4YKev8XGH&P1hL9QsPidBjoJkiYh!FJK>*-ZLf5F2Fu4Ru^Y(NN^Q{B^7+Xnj zf}sO$yFK6@b{EH1N{+o0Cj)qdI1^rr!Lv;N&w>e`mtjdC?O*!*c-#7kx$YdU*2Ky( zlZELW-%}72T4SKEI&4=2Fuh8Cg8rc{tK4&I1mbLoq*CXH21oxWydC4$RGHu}L_r`X zm{O%~J`dn2JHXTGqlHArsF`nPW;n@+2=UHXcB`J9WSdR^r6=BDqSSm{OGjm}0U3Q`IeY(8K)X~ zl7P#q_=RzuAk?dm0&6NeCwK=i4p1{I2iEXK@n6-jaF0B9emi%p|2b$t2?!hu2WE^& zS#fxjV(0Sw*v?W%Rfv9)J!2Ku2y9;|Q-@S4Go`%%Q2V&!I_^=yrLxnfFs^U9Z4K)k zFhXA(*&}nBcltgjx^#yFG*8M{4dt0zSt3Reu!OdvZv9QY#32t$Xbf;b`0f)R#%wXb z0dbro6-}Ax7E7sP&dh6cf~VS+F z>kruS7=RGb9b-?_)++F~l1o`d1z>#U5v&TQq{bO+@3WkesC{0x>!V!vp{pYN={y(i zG|OxX*t&EEJ}A70i(~MYNFTSEfOJ~0W*hr}Ec<4W@3r_MM6A~q;k0l;tY8)U_=|GvPf#*vZ4y9Ch z+le!UL#xSCXim@f>BnUaN@Iw;m!j`Ib4~D3@VmD^G1zkvS9zyQ@4PA`fCx_J%OH+L8d?iJa>0g}i7kVIu_OTusa;6gIquBI{Z{m2O-v<2j=?Zx`EOLM`$bp9y!?Y$2IB%(2`8Oe*&|km1+PAgL z*C!9uGzTIhTfG5}M-u7dxC?n~dGn1o>Hw6i#;qdbzqgc5Z?@8;E|dUDXLA!+n*yMK zWrk!}?txSO1phf<>p{LgV6E?W8MunpPwwUWONGP-9X>&$N({7gli`KsU9hB8y*g1k zdMG?-7Sifjri+87x*Rq3DlfU+-`CLxnCjTz>!1$f0bU30^J}E%n|aDKjinBo4XKV& zBl)MW5r8V1WBsHyxn#{ydA@@3G{ZnRP5B5&3Q%TS!rhz?bm_aMO%7jcxW?KPiN7Mjw8ue9%1*2$L)WPr1gY93r*C_I<0mq-HO_|7 zAYMIhJo?S&?-hOpBfKJg{idb{qF@g4&?janTF5X1;|aUr`Jf^qmIW0N5bGe*f{KXj z2vkJ>9P5aO8X&ud9{%Wnk=GidVD2p-iSQTkTeAg(Hi|OrTtlY6wH!dQ4Xtq(;ew?r z>w4Kv-SyLa(V)oPnR>5*umD+CG*UE+XYP&c8IZj1R~TaU=1aO#s~zNmIJWToJ2jdp z+A4*5{ju5tyhH6wx^f%WOUiskehz(uph#8gl&kA%82J?M4uNjGe1P2u_Q;@Fuco+L z%ecV-XVvm#mYGF@?19)gA(ZM^;z@vq^^ev8E?7`eRMe?l88(RrbnCQWGhzb5VtF>O3wMtt=+gf3Q2D+r zM5`OueU5!=FThtOJ847|xt`u`ewJ_yh5J&<* zfF1+^bG&E(1Q?XwQYm$jUpa1 z?ot9jRI3jGS#XPUTLFKr3$EGul5PtO|+b>w|QFSVNfgN4@704y|Umqx9C)_brk z6x8HaYLB@Jrd+NR?o;4@j7tMT-TXpX7dsR%d2MiB6Ja!|jVC@6#DJu6*TO8G#okGUC^FUl?sz&;y{J5;*?`RA|hqQ8=0yfl} z3Q(7cdmeiAxcAYkPq<;u@SIL*xF!~50_$z%J}8MWazPpR>bb`m#fQKRRIgNfrS|Cy zRNpZ;p>D9d#*BZgCeJpLc(-<~*wIaq(;RT&b4^f{V#_(V=s~B4CI)i!G>YyouU-SB z-M!NjDiH_ponWlNV64drO!-(e`_GMApLL*$E;y#Y-Vb8ZHZT*L@P@wlSan9%Aeg@e z_MmT-U14z+12Lxo9=gKc{qtqG0X{FdOKF!zpU>mcFpcOy$8rEmQ5_i@Ps=xnR3^7{ zCDa;dL@qlZ!sHJ$@a;9Myf|{Q4!yc|sA2t4(AKeYWKBSoo%aJ~A^%_l=nfBLGap$z z1N*Q2;d=wHq@32-*xrm0HFNvH!eAfoIdqTshW&wXRtEw8vb zAYHmNv;6$NcFg4)DZrx*tUOMXU9zn809RC>JDMCZRiQ}N5v)eB;%XREMU?+S9V%bq z$siExOb#-j{wmG=1&k3Kg4N?nSdh|_>{1j)uYhFgj-B{fO8aAc7-M2vttl7K7KNZ> zIDZ+V$Y*qhG?|&2YXog7&Ebfzn^oXR19_+{J3W|(#%lx)0C^~`j~IvseAItdK9i0A zt#;M`(0yMUo(kOps-2i5b(kar(fw6>7!cUv?q4-jwzUnJV<`apTnj_5h9fz0WP;Z9 zc5w9(VfmqbYy^CS7>cAQXp;ViY}kwg01;NTk!8}}Uw00q_`NpQ0Ti68QlL<0?W|;zMK~N>IK1V|<8!bISTyA}S@& zm$KyunCn;4DYK9u@I?WThay!yb36r54x$)o-ApGfjv!N0 z!~RF`n+vcnrFU!1(v+{1vKRGBn@mmP<`+D`&Y8epIPeWc%tX%U`b=$4|AKT2o1TeVVxDKtviXm*#Q}HteHE|NBz#b>pvwi0 zA5?Gun2^kLhS)S_1Q+RDdaXtMDyum*hvc(i{i4UC0X8kUev$a}bynMgE{B$Xsd*@1 ze`vV-l4em;6Edj+sn75s)k6FJD=DQX1-iu*tfMayDlwqb(c$PEML(~gz$(JCV9G%q zhDOJ*7Ja-kWf(R}EYo(b3LEU3CRmveGfkYouKt1zxy-dKP-uO|9d2I%1Bo8&sQp@& z>Px(T7E|mILVpRmsf8vaDzO#Z^7lvdJSOCb7^p_x_o6X26au^MfgnaA6$Aq8-vQV_ zg%ztHH7JsRz9iQz=P6Dg3Zw{mw5D5hBZygX6-2iL(o~!)W{Fj>`Z*EF zPHrGu~Lw8LsszIR2O?8(qBrhf_46#=u&g!1PGczA~b ztQ)w4_`DG0KB=u=_l*#B>l~{TDC%RIhl-mRgVYlwYuCt6zY`|GlG{Eu<@wR59~`mh zC}BiSV_He=dFoNTPwOS(mlA)LzEgr4>&@L!cz)|E=?k1_IAuXPudf^A{YeR58zAb? z#l{A}1AkFT#QgGK^a0i?Xm>aptn2<`ZI4m3n@6PE;Ft*r;wvwlT# zw{`D{G`$EtFuLcXEFd4Xl>Zi5@(S!9*|f$vvwNx=r=R7>iUNZi_S-wXKjuQJO$@By))o@igp z5&^ZrCCLi#|Naw7cCdA*69M zk5bsQJ4hs}1R$k!Y|doCPMXK(A6Y@N z(-l2KE*LaDS)1t~>x{eU;_m}X^ptYV54LjbM+Sc(`zU{%Ih#DE*!+>~-b&3qEx;#( zt|7RZS|8DRNJ4#4_~d_R|JH!c-72>kHcRl&?AVB~1C^?57!k6#2EwtPN?jU&#GR!8 zBn|^rT;+6Faaej^2SzSev`C>t91Ao3F&6D#TN^kw*87~U5)r6QPwN{J8c?=;LFw#5 zy4cs;TU|!X?U3xKr&-QPa*4^y2uVz|rA0hb zJ9A5*U+`#I22CqxGm5p6%3czPw2xs3)?8)BI*pD{$4-Tm&1c$uZsXhfd@ANRJ3iQr zsw^6}+!2cge98#IIHqsEpy)4yPnBREoX+Qnf3{{pyyqlZtnAQgCnW)-r@0)<=@Y3~ z%c{2GZ{o22*)~9-o=o<{yxNw2Txu?=Z2 zx@V=(L^CwXHl-XOdECSl@lq$vnhM2c5`eaJ@HeSTXm$MI)^`ZpPe|Ve?H$8ITDI3x zbJ|L62AbfDvK&21PxZ8^R}U4SB(50v052hAx;xs@6_WvvEnqmkc0*+vZC?WOGkQ?s zj(DQyk_f>)jezws>mr70W^DS*X8{RA~|$zIKKZ*b_) zw?G@dlvG`R>K@;MXG5k@Ey;*;QH#I$BU^ggstNAVt5))hWzBQN}?K7n%)F!-VP z&#eKEzFOeu%%`*eu>j81ypN}WDG)#pOE$uVH4+uOSM3mjT?y?;a?Lgs)=(J3-2#<#%_5?Xa&L=q9j6iw6|= z1pIXq2mm+XE$AlLGj#xN!i%J>{H73tZQ%lC)`{LlGZDBiII$(_2_PgUkZPAqwo8EJ zOQqLuItiMRvOzI%IU6%zYg>*&vjBXV;K%>|mA~hkBb_JX;Ca;-(qq1>+z*vvo9jju z0D5n)@Jt|_g6)CXt{Q*SJtOm;NFRg36B(FR7U<0+7^=8)zvO>8W!`qCG+*7bEsVuY zj7Mc_6OxEMTO6FOGDCcy)!?5#aRz z!HU9*`~s5D&X=R>r-v@1Gc%J7kv6RW(nA+hw!pknaqkP&H+{#-+6tSr>HDVJzW&vo z?tQ~e^7})x?KE|Hrv<=o3JJvPkX5-;0#?-J1TCKlV=ABPG8&u>{R;M^{MMl*j~a{@ z;<~5%M$*@oBln$cA+$AMzKQ;r#KMM|yFv?u|)sUwNCmK;GA@?$FRnF6c?QNWoIVq+#jV93uRbtqq zDkS5VK5?dlU$asCqx9JhTsPqqk3AqKhd2C{Wtm1_QM$qHN3O+X*f66uDMUq;@cB zpI03Vfo(!Qy{*gQxD+SpLek=%1?&X3-gMcoQ>ciRd>cNf33csn%W6#nUU!d%`?y4_ zm-0*vUdCr$rvp*l0moIrx;Vz$kOW$U7`OHSKXgoE?$>iXbGs<{+XLMl44T1slqFYn zmDD;7_No74eJA+d$^t&%0n9f{@BPV#4u`V9g(6M- zbA9^}41W|55#vkv_5ohXk1U0nxJk}bz)tE6v@5a^Io{>kzEv*K~fs1&i57Jv#A<+cAl0wS3-h-Df`nWSKE6TtSe5q(~v_9)HDyTo) zcQPTzs?z#+f)v5sscmO!Nw4EKH#knkRsPq_xXbdNLEtBd{~o7OD1omY>?Z?_S8|}A ztR@`lCK`I8Wvr1)kOD8YK1p>X8ZePhk;t#5D9dfNh_a+iB9JYc)MOBBBGT~51%Wh)y}R|TA?sKfmq2MytQB) zn$~nLC$$Ob%U7Q|j(zMxC!l6JeF4-%a|udF=xGB=W&7rWo1%`s+dspk;!=5{AcIm> z$6*yxYu7jW>?Dw)G!}1;wIe&t?D<6MwE2iMk}kh(t^&P^p=1?yIzHB`2j1|QtT<}! zp6-1OCNU2&*7%0I!bV z?%+DMc_jjPR5can4dn2;^--;OZhUNwly&9;lt<5E} zit*Ba!U&U*|)?8Lp# za_7iU)dRG)9%g$KLfXVt-|piy-DzBVPhq()BYL+<+bFXO*AgEAU&g0hU7ya4YgMij zxXUt&uBc#*5VDi{cOvAsbuRi5qG~NX4Omag5ZaWH!F3&Yl0u`&frBcMd&=f^DrbJw z5seoACJ#$6Ci7@2>gcb&y#Y+3NYErYkhqkh`ufD9v@>qCvOABRzb^OmDqQ~N)?Zz@ zG1cF-t}ZA`hKbYsk_Q;GunMsY@n(nEuL;<=y5$;%uP}XI#0Etc15CX`TAe6ShQ<6T zuE!oDFy)Gjs@w<>^Pldll>HpO)1mbU>R+F3<1yXKc%EiecYyfl8!|UXG4TSPL5P}Y ztZ)bTG{7pT7jO7TF-B1O30DJ}uW~0j(kp|zW5ffj@ z@~>ZrWS)scb|35NdQ=5U5%~z$Km|VoXZvNwSm?foIDIh=5HBwHIYS# zLW3wL+z4~AE7&2V|MdhBJ$_+(e3CJB?^^YFEvxvG(y@w(j+jeOORMuEsmUY~9++b4 zlZZBU5;>xEd46`osSknt@jXUJ`vs1NyGTBdZ)tJFm9}}5*>P*5-nxpcz7_y`J@o*a zk7(8j&=%?UzO697c)-n|(?`$OPIfL+D5&a+FB@AD`Q8BozILeVee@{uhxgk@G#Ar%3qD6~QWU%ABAc(y7Ce+3$p#d6It&1C19(c7otukk&XaNX91DCMbykoPOP zI!ir~erVl#17EI4f!`VZru56j)O{ingeel#=(yRd;FR9FZH{k&Ei~YyDFo1Xi36eA zy4ikAkQHL!*N7tO9Q1nvFY&p7OqP5u@6yzBZzz3$5#fbRht3pf%+$$6u9|#`m=z|M=5EKosNse``73oEspBD-+WEM z#O48s!V%`;5zR8DeL#!XH*f#nQ&x zru@4pUYx7b;=29iSQZ#o<-eJ>hcvd49q#O`9Eu+>8; z;Cm^AKJ?*3syn(@nHEBvDTm!)lCjHiUMUsgFjP{_BaNbjko@gjqN_^n-8TtzyCOI` zuIF9~=}Ug$aehkjej-cQvwO*Mj}BOX>Vi<_xWdz?U;szXo%+O$K=$7j1^*0sIEiXy zEsI$rjT9a}rZH?@rO`Ws^i{-gNwNvF-vqiF7IkZH0K_s+yjXSJlF z+ViEASEL2*kHTQRd{;F6P8ax2&wf_sR2xbz{Z9S6DID4kNx3)uW1_6WMC#}2u$|+K zyzY`%KAEL)w3~$Bp-PBhZhu9b;4NxLk>mqF^v(ZO%aw*h+4lV`71^RtlCg|CBur9F z7)vsyERm#b3ejdy_8Ccpn4tyPl00Q8q%09)7=@5*MGPWY8Wb~Td(Lad{oc>>zQ^(0 zU*6}_bsfGq&pFTQ|6BeG4ISCwVBTQK%U{m`SH~FQ(p9n)l?19Xwe&U>fzhhBps0wi zKN>$ZC28EC<=ki)yowZ;|3r!dZU#rWNFQ{nOtatSz}eO!O0Guv(mfxk`_12^Tw)M{%cP=nHyq&V!RRNWamJjAPklb9I*YAG7X_H9(jmrnNo4XC*C z?@)1I+%{7YLc-|ZhHd}Yq{*#&n{K$Q}*e?G@DEnhg~ zfg^eQ_qc?7zWJF%@XPGA1x0bbrjm8D0e;+AN?QADqghI*A8>)2torT0Z@MTRu+sP( z@R?tY5uQ@zrpM0*G=ONjSe-DZ_I0PO?$uaz!gQN1Avyx@b5^rX`bgXB&G(>mcqwiy z(L*M%!SnFUz^N%e#}9qk0z_h&w8`jl!?TnvS9~%2s-^won5Yb^5W2Ev(HrR;jn#Ca7Gq z^Xeg@<}F1TG`CbHT4hh%Or_ zk109**#gPqZE1%?W|7`WNAizqP*j9B*oq0mc$iTNFoVWzUOf{<*wYYSPo}PcrHEI? zHS%Rril?gm6|POa*a!eoPxLgAUEI2Nm3S*oj&z=v9=zuqIxo(UyRt*MB+teqA4p!+ zjHo={s;J|Sc!0=Pd-U6Q5#@x6OZ^X?h{rtgkfo&cKM_M)=0AffIGv$zDjd7Ll-f9) z{_x0J7;s)2E&W>@!`w&80$#83?u%_gs-^??1$^^7*OPqPIusW35YHU`=-29glygB% zIaAgY`D9Pf6g3HxXD;30wDronw(NtJiEN6-TKSWa`N#{n&+0r@4r6@-?6$`g*T?*rKLi|O&@4H14 z5JRH^y3ObAOmFnli0wG&~yFEH=w1%9OnEZ5+R>(g6x$5^RrFry{!0&dM8mBI>7${xlE z1$#!5d^@qa-$fcv?C>mcF0we(Wj~J8CI#5UQ9puNdzgGF)8t(03{fbVmjPviQV1fX z5LYY&tyF4+BHL6VMbA&Q5on&z0W+<(OQ#)q-o5e;Sh9W`O2r$S#7baZMpQnOHv8^p z3l-z&3!mH&uH2qugYO5#Ee^M(#JT~Dwkom-0v#o|imvTVq37MBwGiKYGlM6(Hc}niq3!g7fAR>&uv|vLu1{W??B*o>LTk%SoeEmGsC#0TRIa^(h4z z8A=i=TCPiJFbM#O*~#Arl>FgKCw#YK38O?G%ULMGWsJ+St&)LcLMkLlDeYrqc6APGEuSGc_Ow>&-$gZ@O@jMb1)kx_Avpre>X+Np%BN z?T0_-@ze$3o^i|fkBU|*rN;vS|JFPCc(hM&LNv5C;#Pq$XaBWc0E;59c-Dj~DF?ng zdsIdDObik5n!U{#c9oi?{|~W-pV}qXcmUS;(F*2^eCXUwd+F+W%R8=PJ}V{xNDZBA za>K*VKOwEJw4i^CU(4Yw8rIsDTkmMdlqk|BA7k)B&h>RJde+Y{I7?}tm&H1D+hlxb z{Jr{o*E`E`Z*!4=#Mw6+$S*nc*Sy8TLkepnLQa9g|E~gB$44R;a{1n=P%c4I!(+-- z=SjGzG+%$c8KTQoac`9bLgCP;uF}>V8FOD^pSzv>dY0aeTAk+sAJ?USJMnV!E{l>y zv$K*a|n@AR+Nik%x^_02|j?fx!+WtQ&DpL#qyY-|m)(&ZDin(M)|O zkS{r1(r&-L#|!A;-?X_gaxJ%3HlpRBGzNW!*V@o2=z+PYX1@KZ6b6`YJ6F!t8w)cO zHOqWEr__LJU!A~Kn*%h?&1irO1eK*Z(?3Y3cQ|fabUx3M(j2M$me!Ol#oorKl6n~c z3KJyJEdvOi2+--NvS;4Ai2i%waYpm*51_4#VB>V4hrZ19IsdB$uQ@k_a;t4MoT2I!?uK_S_c7mhxHa3q=xrD*F~6hY(LR<{Q)P!lh_mdKwy@I|(5?Bj$NsNNmmU3UOB z?GN7RGlbv4;5{Ea2f#B8Ja>Y>mw|Vu^Y|i;=@L0)FT+*K_5*uM>)kCsIy5Ae*SBXx zZu_8)1`tj{9?q}0uw;q3XRmr4evs0oBn;=7*bFciQ4un+squoz2al(iOsF$dTpXUI zu@K^?m&p2tyBMwt;$^4_N-!G-IvjoadcB*~V&O;`(LhTd4Q%kuzc&)sYp{HyUsTA?aRkA10?JnwW8caZ6r;xShInps3E zRLZ_pC%2$GRt(K|3BfUYKCIJyh24aI1x*SapcNV$GSE^*YeS$(oi*HsgNayYZpUv z4{e{~>Ch!HH0&R(lK5jOdMyEi}+vJB}|^!)z$k@Uu)>J z?v9^7>jsCzUgH<%CK>5qJUWg}ogi0Bpa$#SRB^h~8DQ#p4P$|RFl>BcD5hc=zmlG= zje3vb_$|)~u-iKVO&(zFIP5+N7(OI$nLW`?SoUUrTNGoD4+Z`l4rk9#unAx?{2O{0 zhs|!6o%$_NS6^DoTuFDLmhFS#YsuBjB^G1ek@_fm-uCO)@TzM1+?Y1(>(?Ar_PZz5 z+Avgj?HfsANSQ!>#lGru!_38L)Zk!vP^kYhn}vOYU$$hX6KJ_K4!)t%t-r2{UM)fE zTk!sA9KI}m=hswU-3qfcFdJVRdIKN6Oc{#_^tPk3=c>UF`+4uVC%z-+jfY)t2V&=j zZM~WEDYo8oSldP%i%#AzKj5-vcuaJO!IWYAW=`x6o3E3gZ5*9WT}b~GesOrXn&OGu zPpZ%gm;G839O|?X80fQfb@{ZGcTBa@*uKeDZJPU=6~-`o3{}e>LUEQ*tnO)!43;zN z&6%nw=1}U`D9*3yKKyb8haOmrXJFY&zfr6?82e`(L%WXEQOsd;R%TJ`IT%)*uYO%N lDn4^KEUMYKmcs-G%GqaA6E@1M<9KsW?FU+J8(k4y^G{6J?@<5% literal 0 HcmV?d00001 diff --git a/research/c5-dyadic-decoder-gate/inputs/MATCHING.json b/research/c5-dyadic-decoder-gate/inputs/MATCHING.json new file mode 100644 index 0000000000..7ca668d7d5 --- /dev/null +++ b/research/c5-dyadic-decoder-gate/inputs/MATCHING.json @@ -0,0 +1,539 @@ +{ + "schema_version": 1, + "selected_archive_sha256": "f1da80610bf33c58527f18ad63b4350d0b864e1d4486141ee17ac9bed4d529d6", + "selected_payload_sha256": "c5916ff312678f12aba403847643fbbc29f643acec60bdf836fa56cd3e8251fa", + "port_count": 112, + "label_space_dimension": 9, + "edge_rule": "i != j and parity(q_i dot q_j)=0", + "matching": [ + [ + 0, + 1 + ], + [ + 2, + 3 + ], + [ + 4, + 5 + ], + [ + 78, + 12 + ], + [ + 80, + 6 + ], + [ + 82, + 7 + ], + [ + 83, + 8 + ], + [ + 84, + 9 + ], + [ + 79, + 10 + ], + [ + 81, + 11 + ], + [ + 77, + 13 + ], + [ + 85, + 31 + ], + [ + 36, + 15 + ], + [ + 21, + 16 + ], + [ + 23, + 17 + ], + [ + 33, + 14 + ], + [ + 35, + 22 + ], + [ + 53, + 18 + ], + [ + 55, + 20 + ], + [ + 47, + 25 + ], + [ + 24, + 19 + ], + [ + 91, + 26 + ], + [ + 32, + 28 + ], + [ + 41, + 29 + ], + [ + 39, + 27 + ], + [ + 50, + 30 + ], + [ + 96, + 43 + ], + [ + 56, + 38 + ], + [ + 86, + 37 + ], + [ + 88, + 34 + ], + [ + 89, + 40 + ], + [ + 90, + 42 + ], + [ + 87, + 44 + ], + [ + 45, + 46 + ], + [ + 64, + 54 + ], + [ + 69, + 57 + ], + [ + 102, + 58 + ], + [ + 59, + 49 + ], + [ + 92, + 48 + ], + [ + 62, + 52 + ], + [ + 93, + 51 + ], + [ + 94, + 61 + ], + [ + 95, + 65 + ], + [ + 97, + 60 + ], + [ + 63, + 66 + ], + [ + 111, + 67 + ], + [ + 106, + 68 + ], + [ + 109, + 71 + ], + [ + 98, + 70 + ], + [ + 72, + 75 + ], + [ + 99, + 73 + ], + [ + 101, + 76 + ], + [ + 100, + 74 + ], + [ + 103, + 104 + ], + [ + 105, + 108 + ], + [ + 107, + 110 + ] + ], + "plane_translation_labels": [ + 24, + 96, + 384, + 467, + 483, + 427, + 347, + 187, + 371, + 219, + 437, + 483, + 411, + 272, + 272, + 3, + 243, + 437, + 485, + 258, + 144, + 235, + 12, + 68, + 132, + 18, + 249, + 486, + 231, + 215, + 159, + 63, + 497, + 160, + 12, + 264, + 175, + 12, + 423, + 12, + 399, + 435, + 243, + 483, + 160, + 207, + 95, + 399, + 311, + 48, + 311, + 183, + 215, + 96, + 48, + 160 + ], + "matching_degree": 52, + "plane_matrices_2bit_rows": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 8, + 0, + 0, + 0, + 8, + 6, + 14, + 1, + 0, + 0, + 0, + 0, + 0, + 6, + 8, + 0, + 0, + 0, + 0, + 0, + 8, + 0, + 1, + 8, + 14, + 6, + 8, + 1, + 9, + 9, + 0 + ], + "plane_matrix_rank_histogram": { + "0": 40, + "1": 9, + "2": 7 + }, + "active_query_terms": [ + { + "pair_index": 25, + "ports": [ + 50, + 30 + ], + "M_bits": 8, + "matrix_rank": 1, + "support_pairing_rank": 7 + }, + { + "pair_index": 29, + "ports": [ + 88, + 34 + ], + "M_bits": 8, + "matrix_rank": 1, + "support_pairing_rank": 7 + }, + { + "pair_index": 30, + "ports": [ + 89, + 40 + ], + "M_bits": 6, + "matrix_rank": 2, + "support_pairing_rank": 9 + }, + { + "pair_index": 31, + "ports": [ + 90, + 42 + ], + "M_bits": 14, + "matrix_rank": 2, + "support_pairing_rank": 9 + }, + { + "pair_index": 32, + "ports": [ + 87, + 44 + ], + "M_bits": 1, + "matrix_rank": 1, + "support_pairing_rank": 7 + }, + { + "pair_index": 38, + "ports": [ + 92, + 48 + ], + "M_bits": 6, + "matrix_rank": 2, + "support_pairing_rank": 9 + }, + { + "pair_index": 39, + "ports": [ + 62, + 52 + ], + "M_bits": 8, + "matrix_rank": 1, + "support_pairing_rank": 7 + }, + { + "pair_index": 45, + "ports": [ + 111, + 67 + ], + "M_bits": 8, + "matrix_rank": 1, + "support_pairing_rank": 7 + }, + { + "pair_index": 47, + "ports": [ + 109, + 71 + ], + "M_bits": 1, + "matrix_rank": 1, + "support_pairing_rank": 7 + }, + { + "pair_index": 48, + "ports": [ + 98, + 70 + ], + "M_bits": 8, + "matrix_rank": 1, + "support_pairing_rank": 7 + }, + { + "pair_index": 49, + "ports": [ + 72, + 75 + ], + "M_bits": 14, + "matrix_rank": 2, + "support_pairing_rank": 9 + }, + { + "pair_index": 50, + "ports": [ + 99, + 73 + ], + "M_bits": 6, + "matrix_rank": 2, + "support_pairing_rank": 9 + }, + { + "pair_index": 51, + "ports": [ + 101, + 76 + ], + "M_bits": 8, + "matrix_rank": 1, + "support_pairing_rank": 7 + }, + { + "pair_index": 52, + "ports": [ + 100, + 74 + ], + "M_bits": 1, + "matrix_rank": 1, + "support_pairing_rank": 7 + }, + { + "pair_index": 53, + "ports": [ + 103, + 104 + ], + "M_bits": 9, + "matrix_rank": 2, + "support_pairing_rank": 9 + }, + { + "pair_index": 54, + "ports": [ + 105, + 108 + ], + "M_bits": 9, + "matrix_rank": 2, + "support_pairing_rank": 9 + } + ], + "copy_charge": 126, + "copy_rank_histogram": { + "7": 9, + "9": 7 + }, + "exact_dirty_basis_states_checked": 28672, + "negative_controls_rejected": 4, + "ceiling_screen": { + "a_lo": "6894407/2000000000", + "a_hi": "3447203501/1000000000000", + "kappa_planning_cap_exact": "3447203501/1003447203501", + "kappa_planning_cap_decimal_12": "0.003435361112", + "model": { + "m": 73, + "families": 896, + "stages": 9, + "unpaid": 2, + "centre": 126, + "idle_rank_cap": 51 + } + } +} diff --git a/research/c5-dyadic-decoder-gate/search.py b/research/c5-dyadic-decoder-gate/search.py new file mode 100644 index 0000000000..e3e7cbd604 --- /dev/null +++ b/research/c5-dyadic-decoder-gate/search.py @@ -0,0 +1,69 @@ +"""Complete integer search in one finite E8 menu; not a theorem about all decoders.""" +from algebra import roots_e8 + + +def exclude(costs, anchor, cap=19): + roots = roots_e8() + supports = [tuple(i for i, x in enumerate(r) if x) for r in roots] + orthogonal = [sum(1 << j for j, v in enumerate(roots) + if sum(x*y for x, y in zip(u, v)) == 0) for u in roots] + # Plane orthogonality is exactly the cycle edges; same-plane ports are constrained. + neighbors = [sum(1 << j for j in range(10) if i != j and + ((i//2 - j//2) % 5 not in (1, 4))) for i in range(10)] + nodes = prunes = 0 + + def visit(domains, masks, todo, current_cost): + nonlocal nodes, prunes + nodes += 1 + if not todo: + return [] + best, slot = 121, -1 + domains = list(domains) + for i in range(10): + if not (todo >> i & 1): + continue + keep, domain, plane = 0, domains[i], 1 << (i//2) + while domain: + bit = domain & -domain + r = bit.bit_length() - 1 + domain -= bit + delta = sum(costs[masks[k] | plane] - costs[masks[k]] for k in supports[r]) + if current_cost + delta <= cap: + keep |= bit + domains[i] = keep + count = keep.bit_count() + if not count: + prunes += 1 + return None + if count < best: + slot, best = i, count + domain, plane = domains[slot], 1 << (slot//2) + while domain: + bit = domain & -domain + r = bit.bit_length() - 1 + domain -= bit + child, new_masks = list(domains), list(masks) + for k in supports[r]: + new_masks[k] |= plane + remaining, ok = todo & ~(1 << slot), True + for j in range(10): + if not (remaining >> j & 1): + continue + if neighbors[slot] >> j & 1: + child[j] &= orthogonal[r] + if j == (slot ^ 1): + child[j] &= (~((1 << (r+1))-1) if slot % 2 == 0 else (1 << r)-1) + if not child[j]: + ok = False + break + if ok: + witness = visit(child, new_masks, remaining, sum(costs[m] for m in new_masks)) + if witness is not None: + return [(slot, r)] + witness + return None + + domains = [(1 << 120)-1] * 10 + domains[0] = 1 << anchor + witness = visit(domains, [0]*8, 1023, 0) + return {'anchor': anchor, 'cap': cap, 'found': witness is not None, + 'nodes': nodes, 'prunes': prunes, 'witness': witness} diff --git a/research/c5-dyadic-decoder-gate/test_package.py b/research/c5-dyadic-decoder-gate/test_package.py new file mode 100644 index 0000000000..8c99730cee --- /dev/null +++ b/research/c5-dyadic-decoder-gate/test_package.py @@ -0,0 +1,98 @@ +#!/usr/bin/env python3 +"""Behavior and mathematical boundary controls; no expensive search repetition.""" +import gzip +import json +from pathlib import Path +import shutil +import sys +import tempfile +import unittest + +sys.path.insert(0, str(Path(__file__).resolve().parent)) +import verify +from algebra import (baseline, check_fit, dot, escape_controls, pairing, + rank, roots_e8, scalar_gram) + + +class Controls(unittest.TestCase): + def test_authenticate_before_parsing_both_inputs(self): + original = verify.HERE + for name in verify.PINS: + with self.subTest(name=name), tempfile.TemporaryDirectory() as tmp: + copied = Path(tmp) + shutil.copytree(original/'inputs', copied/'inputs') + raw = b'{invalid JSON' + (copied/'inputs'/name).write_bytes(gzip.compress(raw) if name.endswith('.gz') else raw) + verify.HERE = copied + try: + with self.assertRaisesRegex(ValueError, 'source authentication'): + verify.sources() + finally: + verify.HERE = original + + def test_recompression_preserves_the_scientific_source(self): + original = verify.HERE + expected = verify.sources() + with tempfile.TemporaryDirectory() as tmp: + copied = Path(tmp) + shutil.copytree(original/'inputs', copied/'inputs') + path = copied/'inputs/DATA-PHASES.json.gz' + path.write_bytes(gzip.compress(gzip.decompress(path.read_bytes()), compresslevel=1, mtime=1234)) + verify.HERE = copied + try: + self.assertEqual(verify.sources(), expected) + finally: + verify.HERE = original + + def test_both_plane_dimensions_and_scalar_mask(self): + _, all_planes = verify.sources() + planes = [all_planes[i] for i in (13, 23, 35, 16, 34)] + rows = baseline(planes) + self.assertEqual(sum(check_fit(rows, planes)), 20) + bad = [r[:] for r in rows] + bad[4] = bad[0][:] + with self.assertRaisesRegex(ValueError, 'scalar mask'): + check_fit(bad, planes) + # Each axis touches two orthogonal full planes, with pairing rank four. + self.assertEqual(pairing(planes[0]+planes[1], planes[0]+planes[1]), 4) + self.assertEqual(pairing([planes[0][0], planes[1][0]], [planes[0][0], planes[1][0]]), 2) + + def test_quarter_and_signed_half_are_actual_escapes(self): + self.assertEqual(escape_controls(), {'quarter_positive_cost': 72, + 'signed_half_cost': 81, 'line_ports': 120, + 'binary_quotient_dimension': 9}) + roots = roots_e8() + gram = scalar_gram(roots) + binary = [[1 ^ ((x//2) % 2) for x in row] for row in gram] + bad = [r[:] for r in roots] + bad[8][1] *= -1 + modified = scalar_gram(bad) + self.assertTrue(any(modified[i][j] != 0 for i in range(120) for j in range(120) + if i != j and binary[i][j])) + + def test_orthogonal_degenerate_sums_share_a_radical(self): + # B=diag(1,1,0); H1=, H2= are orthogonal, + # intersect nontrivially, yet their bilinear ranks add. + def gram_rank(vectors): + return rank([sum(dot(x & 3, y & 3) << j for j, y in enumerate(vectors)) for x in vectors]) + self.assertEqual(gram_rank([1, 4]), 1) + self.assertEqual(gram_rank([2, 4]), 1) + self.assertEqual(gram_rank([1, 4, 2, 4]), 2) + self.assertEqual(rank([1, 4, 2, 4]), 3) + + def test_frozen_receipt_has_typed_complete_coverage(self): + result = json.loads((verify.HERE/'RESULT.json').read_text()) + self.assertIs(type(result['minimum_cost_each_cycle']), int) + self.assertEqual(result['minimum_cost_each_cycle'], 20) + self.assertEqual(len(result['cycles']), 23) + self.assertEqual(len(result['cost_classes']), 16) + self.assertEqual(sum(len(c['members']) for c in result['cost_classes']), 23) + self.assertTrue(all(type(s['found']) is bool and not s['found'] and s['witness'] is None + for c in result['cost_classes'] for s in c['searches'])) + original = json.dumps(result, sort_keys=True) + result['minimum_cost_each_cycle'] = '20' + self.assertNotEqual(original, json.dumps(result, sort_keys=True)) + + +if __name__ == '__main__': + unittest.main() diff --git a/research/c5-dyadic-decoder-gate/verify.py b/research/c5-dyadic-decoder-gate/verify.py new file mode 100644 index 0000000000..819a9de307 --- /dev/null +++ b/research/c5-dyadic-decoder-gate/verify.py @@ -0,0 +1,151 @@ +#!/usr/bin/env python3 +"""Source-bound C5 gate and explicit hypothesis controls. Tekalign; AI-assisted.""" +import argparse +import gzip +import hashlib +import itertools +import json +from pathlib import Path +import sys + +sys.path.insert(0, str(Path(__file__).resolve().parent)) + +from algebra import (baseline, check_fit, costs_for, dot, escape_controls, + half_fixtures, need, roots_e8) +from search import exclude + +HERE = Path(__file__).resolve().parent +PINS = {'DATA-PHASES.json.gz': 'c5916ff312678f12aba403847643fbbc29f643acec60bdf836fa56cd3e8251fa', + 'MATCHING.json': '4fd648f7b5178bff5441bf364d58234b7bc1a43b924bc6da03013c948f1473b1'} + + +def sources(): + bound = {} + for name, pin in PINS.items(): + raw = (HERE / 'inputs' / name).read_bytes() + if name.endswith('.gz'): + raw = gzip.decompress(raw) + need(hashlib.sha256(raw).hexdigest() == pin, 'source authentication: ' + name) + bound[name] = raw + # Parse only after authenticating every input. + recipes = json.loads(bound['DATA-PHASES.json.gz'])['recipes'] + labels = {r['port']: r['q'] for r in recipes} + need(len(labels) == len(recipes) == 112 and sorted(labels) == list(range(112)), 'source ports') + matching = json.loads(bound['MATCHING.json'])['matching'] + need(len(matching) == 56 and sorted(p for pair in matching for p in pair) == list(range(112)), 'matching partition') + planes = [[labels[p] for p in pair] for pair in matching] + need(all([[dot(a, b) for b in plane] for a in plane] == [[1, 0], [0, 1]] for plane in planes), 'nondegenerate planes') + return matching, planes + + +def cycles_and_classes(planes): + neighbors = [{j for j, q in enumerate(planes) if all(dot(a, b) == 0 for a in p for b in q)} + for p in planes] + cycles = [] + for a in range(56): + for b in sorted(neighbors[a]): + if b <= a: + continue + for c in sorted(neighbors[b] - neighbors[a] - {a}): + if c <= a: + continue + for d in sorted(neighbors[c] - neighbors[b] - neighbors[a] - {a, b}): + if d <= a: + continue + for e in sorted((neighbors[d] & neighbors[a]) - neighbors[b] - neighbors[c] - {b, c}): + if e > a and e > b: + cycles.append([a, b, c, d, e]) + # A different exhaustive census: all 56 choose 5 vertex sets, degree two. + neighbor_bits = [sum(1 << j for j in row) for row in neighbors] + subsets = set() + for group in itertools.combinations(range(56), 5): + bits = sum(1 << i for i in group) + if all((neighbor_bits[i] & bits).bit_count() == 2 for i in group): + subsets.add(group) + need(subsets == {tuple(sorted(c)) for c in cycles}, 'independent cycle census') + need(len(cycles) == 23, 'cycle count') + classes = {} + for i, cycle in enumerate(cycles): + variants = [] + for direction in (cycle, cycle[::-1]): + for offset in range(5): + order = direction[offset:] + direction[:offset] + variants.append((costs_for([planes[j] for j in order]), order)) + prices, order = min(variants) + classes.setdefault(tuple(prices), []).append({'index': i, 'order': order}) + need(len(classes) == 16, 'cost class count') + return cycles, classes + + +def controls(planes): + rows = baseline(planes) + names = [] + def rejects(name, fn): + try: + fn() + except ValueError: + names.append(name) + else: + raise ValueError('control did not reject: ' + name) + bad = [r[:] for r in rows] + bad[4] = bad[0][:] # nonadjacent planes now share a forbidden scalar entry. + rejects('forbidden_cross_entry', lambda: check_fit(bad, planes)) + bad = [r[:] for r in rows] + bad[0] = [0] * 8 + rejects('missing_diagonal_payload', lambda: check_fit(bad, planes)) + rejects('wrong_common_normalization', lambda: check_fit(rows, planes, 2)) + actual = sum(check_fit(rows, planes)) + rejects('support_only_half_invoice', lambda: need(actual == 10, 'both plane dimensions are paid')) + prices = costs_for(planes) + # This sensitivity probe weakens the tariff, rather than the scalar endpoint. + weak = [c//2 for c in prices] + result = exclude(weak, 0, 19) + need(result['found'], 'underpriced search must admit a witness') + decoded = [None] * 10 + roots = roots_e8() + for slot, r in result['witness']: + decoded[slot] = roots[r] + true_cost = sum(check_fit(decoded, planes)) + need(true_cost >= 20, 'underpriced witness true invoice') + names.append('underpricing_search_sensitivity') + return names + + +def compute(): + matching, planes = sources() + cycles, classes = cycles_and_classes(planes) + searches = [] + for prices, members in sorted(classes.items()): + results = [exclude(list(prices), anchor, 19) for anchor in (0, 8)] + need(all(not r['found'] for r in results), 'improving finite-domain decoder found') + searches.append({'prices': list(prices), 'members': members, 'searches': results}) + for cycle in cycles: + baseline([planes[i] for i in cycle]) + core = [13, 23, 35, 16, 34] + need(tuple(sorted(core)) in {tuple(sorted(c)) for c in cycles}, 'PR2484 core included') + return {'schema_version': 1, 'status': 'SCOPED_NEGATIVE_RESULT_NO_NEW_KAPPA', + 'pins': PINS, 'cycles': cycles, 'cost_classes': searches, + 'completed_anchor_searches': 2*len(classes), 'minimum_cost_each_cycle': 20, + 'root_count': 120, 'port_count_per_cycle': 10, 'coefficient': '1/4', + 'positive_half_fixtures': half_fixtures(), 'escape_controls': escape_controls(), + 'controls': controls([planes[i] for i in core]), + 'core_ports': [p for i in core for p in matching[i]]} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--write', type=Path, help='exclusive creation of a new receipt') + args = parser.parse_args() + result = compute() + if args.write: + with args.write.open('x', encoding='utf-8') as handle: + json.dump(result, handle, indent=2, sort_keys=True) + handle.write('\n') + else: + expected = json.loads((HERE / 'RESULT.json').read_text()) + need(json.dumps(result, sort_keys=True) == json.dumps(expected, sort_keys=True), 'exact typed receipt changed') + print('PASS_C5_DYADIC_DECODER_GATE cycles=23 classes=16 minimum=20 half_gram_floor=proved quarter_escape=72 signed_half_escape=81 no_new_kappa') + + +if __name__ == '__main__': + main()