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 0000000000..df8b16392d Binary files /dev/null and b/research/c5-dyadic-decoder-gate/inputs/DATA-PHASES.json.gz differ 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()