diff --git a/.github/workflows/percent-exponent-architecture.yml b/.github/workflows/percent-exponent-architecture.yml new file mode 100644 index 0000000000..b22fdbd4e0 --- /dev/null +++ b/.github/workflows/percent-exponent-architecture.yml @@ -0,0 +1,28 @@ +name: Percent exponent architecture screens + +on: + pull_request: + paths: + - 'research/percent-exponent-architecture/**' + - '.github/workflows/percent-exponent-architecture.yml' + push: + paths: + - 'research/percent-exponent-architecture/**' + - '.github/workflows/percent-exponent-architecture.yml' + workflow_dispatch: + +jobs: + exact-audit: + runs-on: ubuntu-latest + strategy: + matrix: + python-version: ['3.11', '3.14'] + steps: + - uses: actions/checkout@v4 + - uses: actions/setup-python@v5 + with: + python-version: ${{ matrix.python-version }} + - name: Exact arithmetic and complete finite searches + run: python -B -S research/percent-exponent-architecture/verify.py --deep + - name: Verification leaves sources unchanged + run: git diff --exit-code diff --git a/research/percent-exponent-architecture/NOTICE b/research/percent-exponent-architecture/NOTICE new file mode 100644 index 0000000000..617d9e0ac5 --- /dev/null +++ b/research/percent-exponent-architecture/NOTICE @@ -0,0 +1,33 @@ +Architecture screens for a conditional exponent saving of 1/100 +Prepared for huxint with substantial OpenAI Codex assistance, October 2026. +New contributions are licensed under the repository's Apache-2.0 license. + +The paired-cube identity, three-stage cover, shared completed-core compiler, +coordinate-star centers and semantic assembly are inherited from icekylinx +and the contributors credited in the repository NOTICE. Completed-core bank +sharing includes an664's contribution. The complex checkpoint is Avi +Eisenberg/ikeboy's PR193, with its stated Claude assistance, built on +icekylinx, eumemic and the preceding paired-cube work. The bit checkpoint is +Rohan Arun/rohanarun's PR187, retaining its own attribution to the preceding +bit word, source-assisted flow and compiler contributors. These inputs are +not claimed as new constructions here. + +The inequality a < D/C and an exact fixed-word ceiling are also discussed +in DaysSky's PR192. The balanced assembly ceiling is due to romainhedouin's +PR183 and the preceding assembly authors. This package's new scope is the +data-only relaxation, the stated odd-cube family, the rank-minimal center +support lemma, the common-triangular-flag obstruction, and the bounded +Fano stub-reuse/all-permutation investigation. + +The Fano graph, original balanced model and baseline Python +meet-in-the-middle implementation come from the repository's retained +research by Douglas Colkitt and contributors, with its recorded AI +assistance. The original network-coding seed is attributed there to Das and +Rai, Generalized Fano and non-Fano networks (arXiv:1609.05815). +references/SOURCE.json records the original source hashes and the exact +dependency-binding changes to the bundled baseline. Original algorithm +bodies and notices are retained. + +No priority claim is made for standard Walsh projection identities, +triangularization facts, entropy cut arguments or meet-in-the-middle +enumeration. No new all-size integer-multiplication theorem is claimed. diff --git a/research/percent-exponent-architecture/PROOF.md b/research/percent-exponent-architecture/PROOF.md new file mode 100644 index 0000000000..043bc4af5e --- /dev/null +++ b/research/percent-exponent-architecture/PROOF.md @@ -0,0 +1,355 @@ +# Cost barriers for a saving of 1/100 + +This note gives necessary conditions for specified finite interfaces. It does +not prove a new multiplication bound. In particular, it does not rule out +`kappa = 0.01` for a different architecture. + +## 1. A paid-moment inequality + +Let an ordinary finite supplier have ambient width `m`, stock `W`, and `n_r` +children of width `0 < r < m`. Put + +``` +D = m W - sum_r n_r r, +C = sum_r n_r r log(m/r). +``` + +Acceptance at a positive saving `a` requires + +``` +sum_r n_r r (m/r)^a < m W. +``` + +Since `exp(x) >= 1+x`, necessarily `a C < D`. For any retained submultiset +of children, `C_keep <= C`, so `a < D/C_keep`. Dropping all other entropy +costs is a favorable relaxation, not an implementation. Positive wrappers, +fallbacks and scalar tolls cannot improve this upper bound when they leave +this moment and its deficit budget intact. + +The elementary entropy bound was also used in DaysSky's PR #192. The use +here is different: discard the entire auxiliary circuit and bound the data +interface itself. The balanced assembly has `kappa < a/(1+a) < a` for its +limiting ordinary supplier (cf. PR #183). We use the weaker `kappa < a` for +the displayed ceilings. No historical factor-of-five assembly is used. + +## 2. The current data itineraries already exclude 0.01 + +The pinned complex profile is PR #193, whose full commit is recorded +in `inputs/complex-pr193.json`. The bit profile is PR #187, pinned separately +in `inputs/bit-pr187.json`. The input files contain the complete child +histograms and the exact source/target subhistograms, with source-file hashes. +The checker recounts stock, rank, deficit and submultiset inclusion. + +In the three-block shared-core interface, `m=3h` and `D=2v-3 ell`. +The data submultiset consists of three copies of the source and target +itineraries and `2v` rank-two complement children. It is: + +| Profile | h | v | ell | Data children, width: multiplicity | +| --- | ---: | ---: | ---: | --- | +| Complex #193 | 22 | 1320 | 440 | 1:15840, 2:6600, 18:7920 | +| Bit #187 | 24 | 1760 | 528 | 1:18480, 2:6160, 20:5280, 21:2640, 22:2640 | + +These give the following strict upper bounds on `a`, with every auxiliary +entropy cost removed: + +| Profile | Retain the copied-center loss | Grant zero center loss, D <= 2v | +| --- | ---: | ---: | +| Complex #193 | 0.004433342 | 0.008866683 | +| Bit #187 | 0.004893592 | 0.008897440 | + +At `a=0.01` the data alone require deficit greater than `2.28165 v` and +`2.27179 v`, respectively. Both exceed even the favorable `2v` budget. +The required deficit is computed directly from the exponential uplift, not +by treating the first-order approximation as an equality. + +Thus eliminating auxiliary calls or copied-center loss while keeping these +data calls and `D<=2v` cannot reach 0.01. This does not cover a change in +data interfaces, cross-stage fusion, a different deficit identity, or a new +recurrence. A finite-leaf or multitype scheme must be assessed against its +actual recurrence; it cannot be inserted into this theorem by name alone. + +## 3. An odd-dimensional paired-cube extension + +This is a proposed algebraic family and an optimistic cost screen. We do +not supply its complete framed side circuit, bit companion, prime compiler +or all-size assembly. + +Let `d=2t+1 >= 3` and `p>=d+1`. Partition `h=2p` coordinates into pairs. +Each port chooses one coordinate from each of `d` distinct pairs. There are +`v=2^d binom(p,d)` ports. Define the scalar fitting matrix + +``` +B[T,S] = b_d(|T intersection S|), +b_d(z) = product_(j=1..t) (z-(2j-1))/(d-(2j-1)). +``` + +Its diagonal is one, and every off-diagonal odd intersection is a root. +Let `B_block` keep only pairs in the same selector cube, and put +`K=I-B_block`, `H=B_block-B`. Then `K+H+B=I`, and both side terms are +supported on binary-orthogonal source/target pairs. + +### The local K is an involution in every odd dimension + +On a selector cube `F2^d`, let `P` project onto Walsh characters of degree +at most `t`. Exactly half of all characters have that degree, so the +diagonal of `2P` is one. Complementing a character multiplies its value at +a difference `x` by `(-1)^|x|`. At every nonzero even-weight `x`, the sum of +all characters is zero and is twice the low-degree sum. Thus the kernel of +`2P` vanishes there. + +Its radial kernel is a polynomial of degree at most `t` in intersection +size. The `t` prescribed roots and its diagonal value identify it uniquely +as `b_d`. Consequently `B_block=2P` and `(I-B_block)^2=I`. Its nonzero +off-diagonal entries join opposite selector parities. Its entries are +dyadic by the Walsh formula, irrespective of how the product polynomial is +written. + +Each parity class of addresses spans a binary `d`-space: the pair-difference +vectors with even selector parity have dimension `d-1`, and adding one +odd-norm port adds one dimension. The opposite class is orthogonal to it. +The original-source mixing argument therefore has candidate source chain +`[d-1,h-d-1,1]`. A retained lexicographic target flag has chain +`[h-d-1,1,...,1]` with `d` ones. These are compatible endpoint ingredients, +not a complete global word. + +### Copied t-star center budget + +The polynomial `b_d(z)` has degree `t`. Write +`b_d(z)=sum_j b_j binom(z,j)`. For a transversal coordinate t-subset `U`, +use the star `Z_U=sum_(S containing U) x_S`. The identity + +``` +sum_(U subset S, |U|=t) binom(|U intersection T|,j) + = binom(|S intersection T|,j) binom(d-j,t-j) +``` + +expresses the whole center matrix through these stars, using scatter +coefficient `sum_j b_j binom(|U intersection T|,j)/binom(d-j,t-j)`. +There are `2^t binom(p,t)` such stars. + +The span of the ports in a fixed star has dimension `h-2t`. The fixed +partner coordinates vanish; the fixed selected coordinates have one common +coefficient. Differences of outside ports generate the even-parity space +on the other `2(p-t)` coordinates: flips generate each pair difference, and +exchanging selected pairs generates all even pair occupancies. The strict +inequality `p>d` ensures those exchanges exist. One star port supplies the +remaining dimension. Thus the copied-star interface has + +``` +ell = 2^t binom(p,t) (h-2t), +D <= 2v-3 ell, m=3h=6p. +``` + +The inequality is a hypothesis inherited from this copied-center shared +compiler, allowing additional nonmonotone losses. A construction that +changes this center budget is outside the screen. + +### A ceiling even with redesigned local data chains + +Put `f(r)=r log(3h/r)`, with `f(0)=0`. It is increasing on `[0,h]`. +A data chain whose endpoints have distance `h-1` has total jump rank at +least `h-1`. If one jump is at least `h-1`, its entropy is already at least +`f(h-1)`. Otherwise concavity gives +`f(r) >= r f(h-1)/(h-1)` for every jump, and summing proves the same bound. +This permits nonmonotone chains, provided every local jump is at most `h`. + +Six source/target chains per port and the two complement children therefore +give the circuit-independent floor + +``` +C_data/v >= 6(h-1) log(3h/(h-1)) + 4 log(3h/2). +``` + +Together with `D<=2v-3 ell`, every supplier in this stated family satisfies + +``` +a < 0.008094. +``` + +The largest relaxed bound in the finite part occurs at `(p,d)=(13,5)` and +is less than `0.008093706`. Keeping the specific destructive-source and +lexicographic target chains instead gives `a<0.005164`, with the largest +relaxation at `(p,d)=(14,5)`. + +This is an infinite-family screen, not just a finite parameter scan. For +`p>=30`, `D/v<=2`, and the data lower bound is strictly greater than +`(12p-2) log 3`. The resulting ceiling +`2/((12p-2) log 3)` decreases with p and is already below both finite maxima +at p=30. The checker exhausts all odd `3<=d=5`, `h=2p`. Let `A` be +the port-by-coordinate incidence matrix. A nonzero row in its coordinate +star span has values + +``` +f(S) = sum_(i in S) c_i. +``` + +For every such characteristic-zero coefficient vector, the binary span of +the ports where `f(S)` is nonzero has dimension at least `h-2`. + +First suppose the coefficients differ within one coordinate pair i. For +each outside two-coordinate edge from distinct pairs, at least one of its +two extensions by pair i has nonzero f: their values differ by a fixed +nonzero coefficient difference. The projections of these supported ports +onto the outside coordinates therefore contain all edges of the connected +complete multipartite graph on the other p-1 coordinate pairs. Its binary +edge span has dimension `h-3`. Lift the three edges of an outside triangle +using supported ports. Their outside coordinates sum to zero, while their +pair-i coordinates have odd total parity and do not vanish. The projection +kernel has dimension at least one, proving the `h-2` bound. + +Otherwise both coefficients in pair i have one value a_i. A coarse triple +is active when its three a-values sum to a nonzero value; then all its eight +selectors belong to the support. If one pair i is never active, equations +`a_i+a_j+a_k=0` for all other j,k force all outside a_j to be one value b +and `a_i=-2b`. Nonzero f implies b is nonzero. The support is exactly every +triple avoiding pair i. Since p-1>=4, these ports span all `h-2` outside +coordinates over F2. + +If every pair is active, the support contains all p pair-difference +directions. If all a_i agree, the whole port family is supported. Otherwise +choose a_i different from a_j. For each pair k,l outside i,j, at least one +of the coarse triples `{i,k,l}`, `{j,k,l}` is active. Projecting their +coarse incidence vectors outside i,j gives all edges on p-2 vertices, +whose span has dimension p-3. A triangle of such edges lifts to a nonzero +kernel vector on i,j, giving coarse span at least p-2. Quotienting the +full coordinate support by the p pair-difference directions thus proves +dimension at least `p+(p-2)=h-2`. + +Now A has rational rank h. Indeed, a coefficient relation zero on every +port first forces equality within every pair by selector flips, and then +forces all pair coefficients equal by comparing triples; three times that +common coefficient is zero. Also + +``` +B = (AA^T-J)/2 = A (I-J_h/9) A^T / 2. +``` + +The middle matrix is invertible because the even integer h is not 9. +Hence B has rank h and its row space is exactly the coordinate-star span. +In any factorization `B=UV` through exactly h scalar centers, V has h +independent nonzero rows in that same span. The support lemma charges +at least `h-2` copied-center dimensions per row: + +``` +ell >= h(h-2). +``` + +The coordinate stars attain equality. Thus merely rotating, mixing or +rescaling a rank-minimal center basis cannot reduce the selected triple +construction's center loss. For the selected p=11 this lower bound is 440. + +The qualifier **rank-minimal** matters. An overcomplete factor may use +rows outside the star row space whose contributions cancel after scatter; +this proof does not bound such a factor. Sharing the center computation +across stages or replacing copied centers also changes the hypotheses. +At p=4 the support lemma itself fails: a linear form supported on the one +cube avoiding a specified pair has binary support rank 4, below h-2=6. +That is an explicit domain control, not omitted from the checker. + +## 5. A common triangular frame flag precludes any bit rank deficit + +Consider the general finite bit contract: every role has an arbitrary +independent input, the completed scalar circuit is a permutation `rho`, all +incidences of a gate share one rational matrix, and + +``` +M_out(rho(w)) - M_in(w) = I_m. +``` + +If all source, gate and sink matrices are simultaneously upper triangular +over one characteristic-zero extension field, then **s >= Wm**. The matrices +need not commute, be projections, or be diagonalizable. + +To prove this, conjugate them by the common basis; rational matrix ranks do +not change on extending the field. For one diagonal coordinate j, partition +all vertices by their j-th diagonal entry `lambda`. Regard all gates with +the same entry as a single processor and allow it free internal computation. +Its known inputs are exactly the source roles labeled lambda. Every output +at this processor demands an independent original input labeled lambda-1, +by the endpoint equation, so none of those requested inputs is initially +known there. + +Each incoming edge from a different label carries one scalar. The rank of +the requested outside-input transfer, or equivalently its entropy for +uniform independent bits, forces at least one such incoming edge per output +at that processor. Summing over processors gives at least W edges whose +j-th diagonal entries change. This argument permits arbitrary communication +between gates with the same label, so that relaxation can only strengthen +the exclusion. + +An upper triangular matrix has rank at least its number of nonzero diagonal +entries: take the principal minor on those entries. Therefore + +``` +s = sum_edges rank(M_head-M_tail) + >= sum_j number_of_edges_with_changed_diagonal_j + >= Wm. +``` + +In particular, pairwise commuting frames are excluded: a finite commuting +family over an algebraically closed characteristic-zero field is +simultaneously triangularizable, by a common eigenvector and induction on +the quotient. A rational common eigenbasis is not required. + +`triangular_obstruction.py` checks a supplied exact rational common basis, +or pairwise commutation. Failing either sufficient check does not establish +a deficit. This theorem concerns the rational-matrix **bit shear** contract; +it is not a theorem about all binary Lagrangian/Clifford frame families. + +## 6. Locally reused Fano networks + +The graph and balanced 10-role, 14-vertex model come from the retained +`scripts/experiments/fano_completion.py` and `balanced_fano.py`, with their +original attribution. Earlier work excluded the unmodified balanced model +with the three Fano demands fixed. Here an auxiliary output stub may be +connected to a later auxiliary input stub. Each stub is used at most once. +Chronology prevents cycles; no additional decoding circuit is appended. + +There are exactly 87 such choices, including the unchanged graph. Inputs +and outputs after each splice are checked to remain partitions of the +physical roles. Every remaining input is independent. Sixteen choices +preserve the original three-demand routing obstruction. On each of these, +the independent standard-library meet-in-the-middle replay excludes all +`6^14` choices of local `GL(2,F2)` matrices, with the other outputs free. + +The broader C++ check drops even those three terminal obligations. For every +one of the 87 topologies it enumerates **all** completed scalar permutations +and all port-routing permutations. The sets are equal. Hence none of these +scalar completions admits a rational rank deficit in any dimension, by the +retained routing theorem. Keeping only one prefix per key would be +insufficient for this claim; the implementation retains every prefix and +checks every matching suffix/prefix pair. + +Each half has `6^7=279936` assignments. A complete product is a permutation +exactly when the columns of the prefix and inverse suffix agree as +multisets. Both local direction choices and all auxiliary permutations are +included. Routing independently enumerates straight/cross choices at the +14 vertices. Small controls compare this algorithm with direct enumeration +of every complete local word. + +Vector blocks are separate solver experiments. A `sat` result would need an +independent all-column replay, routing analysis and rational-frame witness. +An `unsat` solver report is not upgraded here to a separately checked +impossibility proof; `unknown` and timeout remain unresolved. No vector +experiment is used in the exact ceilings above. + +## Arithmetic and limits + +Logarithms use binary range reduction and +`log x=2 sum_(j>=0) z^(2j+1)/(2j+1)`, `z=(x-1)/(x+1)`, with an explicit +geometric tail. Lower bounds are rounded down on a `10^-24` rational grid. +The exponential uplift uses a finite sum of positive Taylor terms. All +upper ceilings divide by a lower entropy bound, so rounding is favorable +to the hypothetical candidate. No floating-point value is an acceptance +criterion. + +Finite arithmetic and bounded exhaustive search do not formalize the whole +multiplication theorem. The inherited analytic, all-size, weighted compiler, +row restoration, precision and fixed-tape contracts remain separate. The +results above identify assumptions a successful new architecture must change; +they do not assert that any suggested replacement will succeed. diff --git a/research/percent-exponent-architecture/README.md b/research/percent-exponent-architecture/README.md new file mode 100644 index 0000000000..0ede0b55bc --- /dev/null +++ b/research/percent-exponent-architecture/README.md @@ -0,0 +1,95 @@ +# Architecture screens for kappa = 0.01 + +This package identifies structural costs that exclude a saving of 0.01 in +specified continuations of the current construction, and tests a different +small-network route. **It establishes no new multiplication exponent.** + +The target is the saving in `n (log n)^(1-kappa)`, not a measured runtime +improvement. All inherited all-size and analytic assumptions remain in place. + +## Checked results + +| Scope | Result | +| --- | --- | +| Keep PR193's complex data calls; grant every auxiliary call and all center loss for free | `a < 0.008866683` | +| Keep PR187's bit data calls under the same relaxation | `a < 0.008897440` | +| Proposed odd-dimensional paired cubes, copied t-star centers and the retained data flags | `a < 0.005164`, all odd dimensions in the stated domain | +| Same odd-cube family, allowing arbitrary local data chains of the required endpoint distance | `a < 0.008094` | +| Paired triples, p>=5, exactly h independent copied centers | Center loss is at least `h(h-2)`; the current stars attain it | +| General finite bit contract with a common triangular frame flag | `s >= Wm`; no rank deficit | +| All 87 chronological balanced-Fano stub reuses, all local GL(2,F2) gates, any full output permutation | Every completed scalar permutation is routable; no rational-frame deficit in any dimension | + +Here `a` is an ordinary supplier saving; the retained assembly has `kappa=5 时，使用最少的 h 个复制中心，损耗至少为 h(h-2)。现有坐标星已达到这个值。增加中心数量、使用额外行之间的抵消，或跨阶段共享中心，仍不在这个结论的范围内。 +- 检查了 87 种 Fano 网络的辅助输入/输出连接方式，并枚举所有局部可逆二进制运算和最终置换。所有完成的置换都有路由证书对应，因此这批网络不能产生所需的有理矩阵秩节省。 +- 多比特边的后续搜索在 k=2、3、4 时也没有找到候选；这些是求解器记录，未当作独立证明或更大 k 的不可能性结论。 + +下一种构造必须改变已经触及的假设，例如复制中心的实现、跨阶段数据接口或端口几何。仅重新选择 h 个中心的线性组合，或继续替换同类局部模块，不能完成这次目标。 + +一个具体的小网络门槛是：三维、最多 30 个独立输入角色、至少一个单位的秩节省。这在原始均匀 bit 递归中足以超过 1/99，但目前没有构造出满足完整端点条件的网络，还需要足够强的 complex 侧与完整装配。 + +复现： + +```sh +python3 -B -S research/percent-exponent-architecture/verify.py --deep +``` + +完整证明见 [PROOF.md](PROOF.md)。所有界限都针对其中明确列出的接口；它们不排除其他架构达到 10^-2。 diff --git a/research/percent-exponent-architecture/audit.py b/research/percent-exponent-architecture/audit.py new file mode 100644 index 0000000000..9bf9d81573 --- /dev/null +++ b/research/percent-exponent-architecture/audit.py @@ -0,0 +1,296 @@ +#!/usr/bin/env python3 +"""Exact necessary-cost screens for a conditional exponent saving of 1/100. + +These are upper bounds for explicitly specified interfaces, not achieved +suppliers or a lower bound for integer multiplication. Standard library only. +Prepared for huxint with OpenAI Codex assistance. Apache-2.0. +""" +from __future__ import annotations + +import argparse +from collections import Counter +from fractions import Fraction as Q +from functools import lru_cache +from hashlib import sha256 +from itertools import combinations, product +import json +from math import comb +from pathlib import Path +import sys + +HERE = Path(__file__).resolve().parent +GRID = 10**24 +TARGET = Q(1, 100) + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def down(x): + return Q(x.numerator * GRID // x.denominator, GRID) + + +def atanh_log(x, terms=40): + """Rational enclosure, with an explicit geometric tail, for 1<=x<=2.""" + need(Q(1) <= x <= Q(2), "Log series outside its range") + z = (x - 1) / (x + 1) + power = z + total = Q(0) + for j in range(terms): + total += 2 * power / (2 * j + 1) + power *= z * z + tail = 2 * power / ((2 * terms + 1) * (1 - z * z)) + return total, total + tail + + +@lru_cache(None) +def log_interval(x): + x = Q(x) + need(x >= 1, "Only positive-rank child ratios at least one are supported") + power = 0 + while x >= 2: + x /= 2 + power += 1 + lo2, hi2 = atanh_log(Q(2)) + lo, hi = atanh_log(x) + lo += power * lo2 + hi += power * hi2 + return down(lo), Q(-((-hi.numerator * GRID) // hi.denominator), GRID) + + +def cost_floor(m, histogram): + need(all(0 < int(r) < m and int(n) > 0 for r, n in histogram.items()), + "Data children must have positive multiplicities and widths below m") + return sum((Q(int(n) * int(r)) * log_interval(Q(m, int(r)))[0] + for r, n in histogram.items()), Q(0)) + + +def uplift_floor(m, histogram, saving): + """Lower bound on sum n*r*((m/r)^saving-1), using 12 positive terms.""" + result = Q(0) + for r, n in histogram.items(): + x = saving * log_interval(Q(m, int(r)))[0] + term = Q(1) + uplift = Q(0) + for j in range(1, 13): + term = term * x / j + uplift += term + result += int(n) * int(r) * uplift + return down(result) + + +def data_histogram(source, target, v): + result = Counter() + for hist in (source, target): + for r, n in hist.items(): + if int(r) and int(n): + result[int(r)] += 3 * int(n) + result[2] += 2 * v + return result + + +def checkpoint(name): + x = json.loads((HERE / "inputs" / (name + ".json")).read_text()) + p = x["profile"] + m, h, v = p["m"], p["h"], p["v"] + delta, loss = p["deficit"], p["loss"] + children = {int(r): n for r, n in p["child_histogram"].items() if int(r)} + need(m == 3 * h, "Pinned three-block architecture") + need(delta == 2 * v - 3 * loss, "Pinned deficit identity") + need(sum(r * n for r, n in children.items()) == p["rank"], "Full rank recount") + need(m * p["W"] - p["rank"] == delta, "Full stock/deficit recount") + for key in ("source_data_histogram", "target_data_histogram"): + need(sum(int(r) * n for r, n in p[key].items()) == v * (h - 1), + "Complete local data itinerary") + data = data_histogram(p["source_data_histogram"], p["target_data_histogram"], v) + need(all(children.get(r, 0) >= n for r, n in data.items()), "Data is an actual submultiset") + lower = cost_floor(m, data) + full_cost = cost_floor(m, children) + paid_at_target = uplift_floor(m, data, TARGET) + # kappa < a/(1+a) for the retained balanced assembly, so this slightly + # stronger saving is necessary even with its strict backoffs removed. + assembly_required_saving = TARGET / (1 - TARGET) + paid_at_assembly_target = uplift_floor(m, data, assembly_required_saving) + need(Q(2 * v) / lower < Q(9, 1000), "Even free centers stay below 0.009") + need(paid_at_target > 2 * v, "The fixed data alone rejects a=0.01") + return { + "name": name, "provenance": x["provenance"], "h": h, "m": m, "v": v, + "retained_loss": loss, "retained_deficit": delta, + "data_histogram": dict(sorted(data.items())), + "data_entropy_floor": str(lower), "data_entropy_floor_per_port": str(lower / v), + "full_entropy_floor": str(full_cost), + "retained_loss_a_ceiling": str(Q(delta) / lower), + "free_center_a_ceiling": str(Q(2 * v) / lower), + "fixed_data_required_deficit_at_a_001_lower": str(paid_at_target), + "fixed_data_required_deficit_per_port_at_a_001_lower": str(paid_at_target / v), + "assembly_required_saving": str(assembly_required_saving), + "fixed_data_required_deficit_at_assembly_target_lower": str(paid_at_assembly_target), + "available_deficit_even_with_free_centers": 2 * v, + "scope": "The pinned data itinerary and deficit identity; all auxiliary entropy is discarded. Free-center relaxation assumes only D<=2v.", + } + + +def odd_cube_ledger(p, degree): + need(degree >= 3 and degree % 2 == 1 and p >= degree + 1, "Odd-cube family domain") + t = (degree - 1) // 2 + h, m = 2 * p, 6 * p + v = 2**degree * comb(p, degree) + loss = 2**t * comb(p, t) * (h - 2 * t) + delta = 2 * v - 3 * loss + # Histograms normalized per port. Repeated widths must accumulate. + source = Counter([degree - 1, h - degree - 1, 1]) + target = Counter([h - degree - 1] + [1] * degree) + data = data_histogram(source, target, 1) + need(sum(r * n for r, n in data.items()) == 6 * (h - 1) + 4, "Data rank identity") + need(max(data) < h, "All data child logarithms exceed log(3)") + lower = cost_floor(m, data) + relaxed = cost_floor(m, {h - 1: 6, 2: 2}) + return {"p": p, "degree": degree, "h": h, "m": m, "v": v, + "loss": loss, "deficit": delta, "data_histogram_per_port": dict(sorted(data.items())), + "data_entropy_floor_per_port": str(lower), + "a_ceiling": str(Q(delta, v) / lower) if delta > 0 else None, + "arbitrary_local_chains_entropy_floor_per_port": str(relaxed), + "arbitrary_local_chains_a_ceiling": str(Q(delta, v) / relaxed) if delta > 0 else None} + + +def binary_rank(vectors): + pivots = {} + for x in vectors: + while x: + bit = x.bit_length() - 1 + if bit in pivots: + x ^= pivots[bit] + else: + pivots[bit] = x + break + return len(pivots) + + +def b_value(intersection, degree): + result = Q(1) + for j in range(1, (degree - 1) // 2 + 1): + result *= Q(intersection - (2 * j - 1), degree - (2 * j - 1)) + return result + + +def local_identity(degree): + """Independent integer checks of the cube kernel, not a global circuit.""" + size = 1 << degree + denominator = size // 2 + first = [] + for mask in range(size): + value = b_value(degree - mask.bit_count(), degree) * denominator + need(value.denominator == 1, "Local kernel is dyadic") + first.append(int(value)) + eigenvalues = [] + for character in range(size): + eig = sum((-1 if (character & x).bit_count() % 2 else 1) * first[x] + for x in range(size)) + expected = 2 * denominator if character.bit_count() <= (degree - 1) // 2 else 0 + need(eig == expected, "Walsh projector identity") + eigenvalues.append(eig) + k = [-b for b in first] + k[0] += denominator + for shift in range(size): + need(sum(k[x] * k[x ^ shift] for x in range(size)) == + (denominator**2 if shift == 0 else 0), "Exact K squared") + need(not k[shift] or shift.bit_count() % 2 == 1, "K only joins opposite parities") + addresses = [sum(1 << (2 * j + ((mask >> j) & 1)) for j in range(degree)) + for mask in range(size)] + parity_classes = [[addresses[x] for x in range(size) if x.bit_count() % 2 == p] + for p in (0, 1)] + need(all(binary_rank(xs) == degree for xs in parity_classes), "Parity source frame") + need(all((a & b).bit_count() % 2 == 0 for a in parity_classes[0] for b in parity_classes[1]), + "Source/target orthogonality") + return {"degree": degree, "ports_per_cube": size, "B_rank": size // 2, + "K_squared_identity": True, "opposite_parity_source_rank": degree, + "denominator": denominator, "kernel_numerators": first} + + +def star_check(p, degree): + t = (degree - 1) // 2 + fixed = tuple(2 * i for i in range(t)) + vectors = [] + for pairs in combinations(range(t, p), degree - t): + for bits in product((0, 1), repeat=degree - t): + vectors.append(sum(1 << i for i in fixed) + + sum(1 << (2 * i + b) for i, b in zip(pairs, bits))) + observed = binary_rank(vectors) + need(observed == 2 * p - 2 * t, "Copied t-star span") + return {"p": p, "degree": degree, "fixed_coordinates": list(fixed), + "source_count": len(vectors), "rank": observed} + + +def family_screen(): + rows = [odd_cube_ledger(p, d) for p in range(4, 30) for d in range(3, p, 2)] + positive = [r for r in rows if r["a_ceiling"] is not None] + best = max(positive, key=lambda r: Q(r["a_ceiling"])) + best_relaxed = max(positive, key=lambda r: Q(r["arbitrary_local_chains_a_ceiling"])) + claimed_ceiling = Q(5164, 10**6) + relaxed_ceiling = Q(8094, 10**6) + need(Q(best["a_ceiling"]) < claimed_ceiling, "Finite family ceiling") + need(Q(best_relaxed["arbitrary_local_chains_a_ceiling"]) < relaxed_ceiling, + "Arbitrary local data chain ceiling") + # For p>=30, D/v<=2 and each r (12p-2)*ln(3). This bound decreases with p. + tail = Q(2) / ((12 * 30 - 2) * log_interval(Q(3))[0]) + need(tail < Q(best["a_ceiling"]), "Infinite tail below finite maximum") + return {"finite_cases": len(rows), "positive_deficit_cases": len(positive), + "finite_scan_sha256": sha256(json.dumps(rows, sort_keys=True).encode()).hexdigest(), + "best_optimistic_case": best, + "best_arbitrary_local_chains_case": best_relaxed, + "tail_from_p": 30, "all_degrees_tail_a_ceiling": str(tail), + "strict_global_a_ceiling": str(claimed_ceiling), + "strict_arbitrary_local_chains_a_ceiling": str(relaxed_ceiling), + "scope": "Odd d>=3, p>=d+1; copied t-star centers and m=6p. The 0.005164 bound keeps the destructive-parity source/target flag. The 0.008094 bound permits any local source/target chains of endpoint distance h-1 with each jump at most h. Both discard all auxiliary entropy. No global side circuit is claimed.", + "local_identity_checks": [local_identity(d) for d in (3, 5, 7)], + "star_span_checks": [star_check(p, d) for p, d in ((4, 3), (7, 3), (6, 5), (9, 5), (8, 7))]} + + +def small_network_budget(): + result = [] + log3_lo, log3_hi = log_interval(Q(3)) + for stock in (30, 31): + lo, hi = log_interval(Q(3 * stock, 3 * stock - 1)) + lower, upper = lo / log3_hi, hi / log3_lo + if stock == 30: + need(lower > Q(1, 99), "Thirty-role one-deficit budget") + else: + need(upper < Q(1, 99), "Thirty-one-role adverse budget control") + result.append({"m": 3, "W": stock, "rank_deficit": 1, + "uniform_bit_saving_lower": str(lower), + "uniform_bit_saving_upper": str(upper), + "exceeds_assembly_requirement": stock == 30}) + return {"necessary_ordinary_saving_for_kappa_001": "1/99", "cases": result, + "scope": "Conditional search budget for the raw uniform bit recurrence, assuming a complete all-role rational-frame certificate exists. No such circuit or complex companion is supplied."} + + +def certificate(): + need(not sys.flags.optimize, "Run the exact audit without -O") + return {"status": "SCOPED ARCHITECTURE CEILINGS; NO NEW KAPPA", "target_kappa": str(TARGET), + "checkpoints": [checkpoint("complex-pr193"), checkpoint("bit-pr187")], + "odd_cube_extension": family_screen(), + "small_network_target": small_network_budget()} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--write", action="store_true") + args = parser.parse_args() + result = certificate() + output = json.dumps(result, sort_keys=True, indent=2) + "\n" + frozen = HERE / "ceiling-certificate.json" + if args.write: + frozen.write_text(output) + else: + need(frozen.read_text() == output, "Exact ceiling certificate changed") + for row in result["checkpoints"]: + print(f"PASS {row['name']}: even free centers a < {float(Q(row['free_center_a_ceiling'])):.12f}") + print("PASS the specified odd-cube family: a < 0.005164; target 0.01 excluded within this family") + print("PASS even arbitrary local data chains: a < 0.008094 with the same copied centers and three-block architecture") + + +if __name__ == "__main__": + main() diff --git a/research/percent-exponent-architecture/ceiling-certificate.json b/research/percent-exponent-architecture/ceiling-certificate.json new file mode 100644 index 0000000000..43ceb51bf8 --- /dev/null +++ b/research/percent-exponent-architecture/ceiling-certificate.json @@ -0,0 +1,389 @@ +{ + "checkpoints": [ + { + "assembly_required_saving": "1/99", + "available_deficit_even_with_free_centers": 2640, + "data_entropy_floor": "465224708035415792023453377/1562500000000000000000", + "data_entropy_floor_per_port": "14097718425315630061316769/62500000000000000000000", + "data_histogram": { + "1": 15840, + "2": 6600, + "18": 7920 + }, + "fixed_data_required_deficit_at_a_001_lower": "150589276786738347498830173/50000000000000000000000", + "fixed_data_required_deficit_at_assembly_target_lower": "304256163045466013973486521/100000000000000000000000", + "fixed_data_required_deficit_per_port_at_a_001_lower": "150589276786738347498830173/66000000000000000000000000", + "free_center_a_ceiling": "125000000000000000000000/14097718425315630061316769", + "full_entropy_floor": "1881413992825956214088711446887/1000000000000000000000000", + "h": 22, + "m": 66, + "name": "complex-pr193", + "provenance": { + "commit": "187e1010ac8b259af8e9b5166f68b64bc27b4b47", + "path": "research/source-assisted-v4/certificate.json", + "pr": 193, + "source_file_sha256": "d84406d2fcc6990deba2b135509e6d86600e57123d88f9b21f7b7240e1aeb513" + }, + "retained_deficit": 1320, + "retained_loss": 440, + "retained_loss_a_ceiling": "62500000000000000000000/14097718425315630061316769", + "scope": "The pinned data itinerary and deficit identity; all auxiliary entropy is discarded. Free-center relaxation assumes only D<=2v.", + "v": 1320 + }, + { + "assembly_required_saving": "1/99", + "available_deficit_even_with_free_centers": 3520, + "data_entropy_floor": "618155352303523457063780689/1562500000000000000000", + "data_entropy_floor_per_port": "56195941118502132460343699/250000000000000000000000", + "data_histogram": { + "1": 18480, + "2": 6160, + "20": 5280, + "21": 2640, + "22": 2640 + }, + "fixed_data_required_deficit_at_a_001_lower": "3998367945767103076034623033/1000000000000000000000000", + "fixed_data_required_deficit_at_assembly_target_lower": "4039190059375994870834134397/1000000000000000000000000", + "fixed_data_required_deficit_per_port_at_a_001_lower": "3998367945767103076034623033/1760000000000000000000000000", + "free_center_a_ceiling": "500000000000000000000000/56195941118502132460343699", + "full_entropy_floor": "1441589852828214420824154291527/500000000000000000000000", + "h": 24, + "m": 72, + "name": "bit-pr187", + "provenance": { + "commit": "201737a1ec4f936e166e2481fb9e88104cb2ccc7", + "path": "research/source-assisted-bit-bootstrap/emitted-physical.json", + "pr": 187, + "source_file_sha256": "5f1f1d978937b816a14b07fee5ac8fc31f3a9aaf05046a477e8be57bb6d07ce6" + }, + "retained_deficit": 1936, + "retained_loss": 528, + "retained_loss_a_ceiling": "25000000000000000000000/5108721919863830223667609", + "scope": "The pinned data itinerary and deficit identity; all auxiliary entropy is discarded. Free-center relaxation assumes only D<=2v.", + "v": 1760 + } + ], + "odd_cube_extension": { + "all_degrees_tail_a_ceiling": "200000000000000000000000/39330319934318326951949771", + "best_arbitrary_local_chains_case": { + "a_ceiling": "3750000000000000000000/730092913570099349003623", + "arbitrary_local_chains_a_ceiling": "375000000000000000000000/46332299214431808464865457", + "arbitrary_local_chains_entropy_floor_per_port": "46332299214431808464865457/250000000000000000000000", + "data_entropy_floor_per_port": "730092913570099349003623/2500000000000000000000", + "data_histogram_per_port": { + "1": 18, + "2": 2, + "4": 3, + "20": 6 + }, + "deficit": 61776, + "degree": 5, + "h": 26, + "loss": 6864, + "m": 78, + "p": 13, + "v": 41184 + }, + "best_optimistic_case": { + "a_ceiling": "2187500000000000000000000/423623562599894110881194009", + "arbitrary_local_chains_a_ceiling": "4375000000000000000000000/546747925880884664447120863", + "arbitrary_local_chains_entropy_floor_per_port": "49704356898262242222465533/250000000000000000000000", + "data_entropy_floor_per_port": "38511232963626737352835819/125000000000000000000000", + "data_histogram_per_port": { + "1": 18, + "2": 2, + "4": 3, + "22": 6 + }, + "deficit": 101920, + "degree": 5, + "h": 28, + "loss": 8736, + "m": 84, + "p": 14, + "v": 64064 + }, + "finite_cases": 182, + "finite_scan_sha256": "cebf8348bf5dc03f528e809648ed3062340b1d7aaf7b47924e157659f0e374ac", + "local_identity_checks": [ + { + "B_rank": 4, + "K_squared_identity": true, + "degree": 3, + "denominator": 4, + "kernel_numerators": [ + 4, + 2, + 2, + 0, + 2, + 0, + 0, + -2 + ], + "opposite_parity_source_rank": 3, + "ports_per_cube": 8 + }, + { + "B_rank": 16, + "K_squared_identity": true, + "degree": 5, + "denominator": 16, + "kernel_numerators": [ + 16, + 6, + 6, + 0, + 6, + 0, + 0, + -2, + 6, + 0, + 0, + -2, + 0, + -2, + -2, + 0, + 6, + 0, + 0, + -2, + 0, + -2, + -2, + 0, + 0, + -2, + -2, + 0, + -2, + 0, + 0, + 6 + ], + "opposite_parity_source_rank": 5, + "ports_per_cube": 32 + }, + { + "B_rank": 64, + "K_squared_identity": true, + "degree": 7, + "denominator": 64, + "kernel_numerators": [ + 64, + 20, + 20, + 0, + 20, + 0, + 0, + -4, + 20, + 0, + 0, + -4, + 0, + -4, + -4, + 0, + 20, + 0, + 0, + -4, + 0, + -4, + -4, + 0, + 0, + -4, + -4, + 0, + -4, + 0, + 0, + 4, + 20, + 0, + 0, + -4, + 0, + -4, + -4, + 0, + 0, + -4, + -4, + 0, + -4, + 0, + 0, + 4, + 0, + -4, + -4, + 0, + -4, + 0, + 0, + 4, + -4, + 0, + 0, + 4, + 0, + 4, + 4, + 0, + 20, + 0, + 0, + -4, + 0, + -4, + -4, + 0, + 0, + -4, + -4, + 0, + -4, + 0, + 0, + 4, + 0, + -4, + -4, + 0, + -4, + 0, + 0, + 4, + -4, + 0, + 0, + 4, + 0, + 4, + 4, + 0, + 0, + -4, + -4, + 0, + -4, + 0, + 0, + 4, + -4, + 0, + 0, + 4, + 0, + 4, + 4, + 0, + -4, + 0, + 0, + 4, + 0, + 4, + 4, + 0, + 0, + 4, + 4, + 0, + 4, + 0, + 0, + -20 + ], + "opposite_parity_source_rank": 7, + "ports_per_cube": 128 + } + ], + "positive_deficit_cases": 133, + "scope": "Odd d>=3, p>=d+1; copied t-star centers and m=6p. The 0.005164 bound keeps the destructive-parity source/target flag. The 0.008094 bound permits any local source/target chains of endpoint distance h-1 with each jump at most h. Both discard all auxiliary entropy. No global side circuit is claimed.", + "star_span_checks": [ + { + "degree": 3, + "fixed_coordinates": [ + 0 + ], + "p": 4, + "rank": 6, + "source_count": 12 + }, + { + "degree": 3, + "fixed_coordinates": [ + 0 + ], + "p": 7, + "rank": 12, + "source_count": 60 + }, + { + "degree": 5, + "fixed_coordinates": [ + 0, + 2 + ], + "p": 6, + "rank": 8, + "source_count": 32 + }, + { + "degree": 5, + "fixed_coordinates": [ + 0, + 2 + ], + "p": 9, + "rank": 14, + "source_count": 280 + }, + { + "degree": 7, + "fixed_coordinates": [ + 0, + 2, + 4 + ], + "p": 8, + "rank": 10, + "source_count": 80 + } + ], + "strict_arbitrary_local_chains_a_ceiling": "4047/500000", + "strict_global_a_ceiling": "1291/250000", + "tail_from_p": 30 + }, + "small_network_target": { + "cases": [ + { + "W": 30, + "exceeds_assembly_requirement": true, + "m": 3, + "rank_deficit": 1, + "uniform_bit_saving_lower": "5586650299062614245333/549306144334054845697623", + "uniform_bit_saving_upper": "11173300598125228490667/1098612288668109691395245" + }, + { + "W": 31, + "exceeds_assembly_requirement": false, + "m": 3, + "rank_deficit": 1, + "uniform_bit_saving_lower": "5405458052107813841596/549306144334054845697623", + "uniform_bit_saving_upper": "10810916104215627683193/1098612288668109691395245" + } + ], + "necessary_ordinary_saving_for_kappa_001": "1/99", + "scope": "Conditional search budget for the raw uniform bit recurrence, assuming a complete all-role rational-frame certificate exists. No such circuit or complex companion is supplied." + }, + "status": "SCOPED ARCHITECTURE CEILINGS; NO NEW KAPPA", + "target_kappa": "1/100" +} diff --git a/research/percent-exponent-architecture/center-basis-certificate.json b/research/percent-exponent-architecture/center-basis-certificate.json new file mode 100644 index 0000000000..3b57377326 --- /dev/null +++ b/research/percent-exponent-architecture/center-basis-certificate.json @@ -0,0 +1,63 @@ +{ + "excluded_domain_control": { + "p": 4, + "putative_floor": 6, + "support_rank": 4 + }, + "finite_sweep": { + "certified_support_rank_floor": 8, + "coefficient_alphabet": [ + -1, + 0, + 1 + ], + "nonzero_vectors_checked": 59048, + "p": 5, + "scope": "Finite control only; the written lemma handles every characteristic-zero coefficient vector." + }, + "scope": "Exactly h linearly independent copied centers. Overcomplete factors, a different center mechanism, changed port families and global stage fusion remain outside this result.", + "sharp_examples": [ + { + "h": 10, + "incidence_rank_Q": 10, + "omitted_pair_support_rank_F2": 8, + "p": 5, + "rank_minimal_center_loss_floor": 80, + "star_support_rank_F2": 8 + }, + { + "h": 12, + "incidence_rank_Q": 12, + "omitted_pair_support_rank_F2": 10, + "p": 6, + "rank_minimal_center_loss_floor": 120, + "star_support_rank_F2": 10 + }, + { + "h": 22, + "incidence_rank_Q": 22, + "omitted_pair_support_rank_F2": 20, + "p": 11, + "rank_minimal_center_loss_floor": 440, + "star_support_rank_F2": 20 + }, + { + "h": 26, + "incidence_rank_Q": 26, + "omitted_pair_support_rank_F2": 24, + "p": 13, + "rank_minimal_center_loss_floor": 624, + "star_support_rank_F2": 24 + }, + { + "h": 32, + "incidence_rank_Q": 32, + "omitted_pair_support_rank_F2": 30, + "p": 16, + "rank_minimal_center_loss_floor": 960, + "star_support_rank_F2": 30 + } + ], + "status": "SHARP LOWER BOUND FOR RANK-MINIMAL COPIED CENTERS", + "theorem": "For p>=5 and h=2p, every nonzero characteristic-zero linear combination of coordinate stars has binary source-support span at least h-2. Therefore any factorization of B=(AA^T-J)/2 through exactly h copied scalar centers has loss at least h(h-2)." +} diff --git a/research/percent-exponent-architecture/center_basis.py b/research/percent-exponent-architecture/center_basis.py new file mode 100644 index 0000000000..bd95aded50 --- /dev/null +++ b/research/percent-exponent-architecture/center_basis.py @@ -0,0 +1,81 @@ +#!/usr/bin/env python3 +"""Finite controls for the rank-minimal copied-center lower bound. + +The proof for arbitrary characteristic-zero coefficients is in PROOF.md. +The coefficient sweep below is a finite adversarial control, not its proof. +""" +from __future__ import annotations + +from itertools import combinations, product +from math import comb + +from audit import binary_rank, need +from triangular_obstruction import inverse, matrix + + +def ports(p): + labels = [tuple(2 * i + b for i, b in zip(coarse, bits)) + for coarse in combinations(range(p), 3) + for bits in product((0, 1), repeat=3)] + return labels, [sum(1 << j for j in label) for label in labels] + + +def support_rank(p, coefficients): + labels, vectors = ports(p) + return binary_rank(q for label, q in zip(labels, vectors) + if sum(coefficients[j] for j in label)) + + +def sweep(p=5): + labels, vectors = ports(p) + threshold = 2 * p - 2 + checked = 0 + for coefficients in product((-1, 0, 1), repeat=2 * p): + if not any(coefficients): + continue + pivots = {} + for (a, b, c), q in zip(labels, vectors): + if not coefficients[a] + coefficients[b] + coefficients[c]: + continue + while q: + top = q.bit_length() - 1 + if top in pivots: + q ^= pivots[top] + else: + pivots[top] = q + break + if len(pivots) >= threshold: + break + need(len(pivots) >= threshold, "Finite source-support counterexample") + checked += 1 + return {"p": p, "coefficient_alphabet": [-1, 0, 1], "nonzero_vectors_checked": checked, + "certified_support_rank_floor": threshold, + "scope": "Finite control only; the written lemma handles every characteristic-zero coefficient vector."} + + +def certificate(): + sharp = [] + for p in (5, 6, 11, 13, 16): + h = 2 * p + gram = matrix([[4 * comb(p - 1, 2) if i == j else 0 if i // 2 == j // 2 + else 2 * (p - 2) for j in range(h)] for i in range(h)]) + inverse(gram) # Exact full column rank of the port incidence matrix. + center_rank = support_rank(p, [1] + [0] * (h - 1)) + omitted_pair = support_rank(p, [-2, -2] + [1] * (h - 2)) + need(center_rank == omitted_pair == h - 2, "Sharp center-support examples") + sharp.append({"p": p, "h": h, "incidence_rank_Q": h, + "star_support_rank_F2": center_rank, + "omitted_pair_support_rank_F2": omitted_pair, + "rank_minimal_center_loss_floor": h * (h - 2)}) + small = support_rank(4, [-2, -2] + [1] * 6) + need(small == 4 and small < 8 - 2, "The p>=5 domain is necessary") + return {"status": "SHARP LOWER BOUND FOR RANK-MINIMAL COPIED CENTERS", + "theorem": "For p>=5 and h=2p, every nonzero characteristic-zero linear combination of coordinate stars has binary source-support span at least h-2. Therefore any factorization of B=(AA^T-J)/2 through exactly h copied scalar centers has loss at least h(h-2).", + "sharp_examples": sharp, "finite_sweep": sweep(), + "excluded_domain_control": {"p": 4, "support_rank": small, "putative_floor": 6}, + "scope": "Exactly h linearly independent copied centers. Overcomplete factors, a different center mechanism, changed port families and global stage fusion remain outside this result."} + + +if __name__ == "__main__": + import json + print(json.dumps(certificate(), sort_keys=True, indent=2)) diff --git a/research/percent-exponent-architecture/discovery/balanced_search.cpp b/research/percent-exponent-architecture/discovery/balanced_search.cpp new file mode 100644 index 0000000000..34c88f3cc8 --- /dev/null +++ b/research/percent-exponent-architecture/discovery/balanced_search.cpp @@ -0,0 +1,252 @@ +// Exact GL(2,F2) meet-in-the-middle discovery on an explicit balanced graph. +// Every output, including all auxiliary outputs, must be a distinct input. +// Prepared for huxint with OpenAI Codex assistance. Apache-2.0. +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include + +using Rows = std::array; +struct Key { + uint64_t low = 0, high = 0; + bool operator==(const Key& o) const { return low == o.low && high == o.high; } +}; +struct KeyHash { + size_t operator()(const Key& k) const { + uint64_t x = k.low ^ (k.high + 0x9e3779b97f4a7c15ULL + (k.low << 6) + (k.low >> 2)); + x ^= x >> 30; x *= 0xbf58476d1ce4e5b9ULL; + x ^= x >> 27; x *= 0x94d049bb133111ebULL; + return x ^ (x >> 31); + } +}; +constexpr int GL[6][2] = {{1,2},{2,1},{1,3},{3,2},{2,3},{3,1}}; +constexpr int INVERSE[6] = {0,1,2,3,5,4}; + +Rows columns(const Rows& rows, int width) { + Rows result{}; + for (int i = 0; i < width; ++i) + for (int j = 0; j < width; ++j) + result[j] |= ((rows[i] >> j) & 1) << i; + return result; +} + +Key key(const Rows& rows, int width, const std::vector& fixed) { + const auto cols = columns(rows, width); + std::array used{}; + Rows ordered{}; + int n = 0; + for (int j : fixed) { ordered[n++] = cols[j]; used[j] = true; } + for (int j = 0; j < width; ++j) if (!used[j]) ordered[n++] = cols[j]; + std::sort(ordered.begin() + fixed.size(), ordered.begin() + width); + Key k; + for (int j = 0; j < width; ++j) { + k.high = (k.high << width) | (k.low >> (64 - width)); + k.low = (k.low << width) | ordered[j]; + } + return k; +} + +Rows apply(Rows rows, int a, int b, int choice) { + const uint16_t values[4] = {0, rows[a], rows[b], uint16_t(rows[a] ^ rows[b])}; + rows[a] = values[GL[choice][0]]; + rows[b] = values[GL[choice][1]]; + return rows; +} + +uint64_t packed_permutation(const Rows& values, int width) { + uint64_t code = 0; + for (int i = 0; i < width; ++i) code |= uint64_t(values[i]) << (4*i); + return code; +} + +void all_permutations(int id, int width, const std::vector>& pairs) { + const int gates = pairs.size(), split = gates / 2; + Rows tokens{}; + for (int i = 0; i < width; ++i) tokens[i] = i; + std::unordered_set routes{packed_permutation(tokens,width)}; + for (auto [a,b] : pairs) { + auto next = routes; + for (auto code : routes) { + const auto x = (code >> (4*a)) & 15, y = (code >> (4*b)) & 15; + next.insert(code ^ ((x ^ y) << (4*a)) ^ ((x ^ y) << (4*b))); + } + routes.swap(next); + } + int factorial = 1; for (int i = 2; i <= width; ++i) factorial *= i; + if (routes.size() == size_t(factorial)) { + std::cout << "{\"id\":" << id << ",\"W\":" << width + << ",\"routing_permutations\":" << routes.size() + << ",\"all_permutations_routable\":true,\"nonroutable_scalar_permutation\":false}" << std::endl; + return; + } + struct Prefix { Rows cols; uint32_t word; }; + std::unordered_map,KeyHash> prefixes; + prefixes.reserve(300000); + Rows identity{}; + for (int i = 0; i < width; ++i) identity[i] = 1 << i; + uint64_t prefix_count = 0, suffix_count = 0, matches = 0; + std::function forward = [&](int depth, Rows rows, uint32_t word) { + if (depth == split) { + prefixes[key(rows,width,{})].push_back({columns(rows,width),word}); + ++prefix_count; return; + } + auto [a,b] = pairs[depth]; + for (int k = 0; k < 6; ++k) + forward(depth+1,apply(rows,a,b,k),word | (uint32_t(k) << (3*depth))); + }; + forward(0,identity,0); + bool found = false; + uint32_t chosen_prefix = 0, chosen_suffix = 0; + Rows chosen_rho{}; + std::unordered_set scalar_permutations; + std::function backward = [&](int depth, Rows rows, uint32_t word) { + if (found) return; + if (depth == gates-split) { + ++suffix_count; + auto it = prefixes.find(key(rows,width,{})); + if (it == prefixes.end()) return; + auto cols = columns(rows,width); + for (const auto& prefix : it->second) { + ++matches; + Rows output_tokens{}, rho{}; + for (int in = 0; in < width; ++in) { + int out = 0; + while (out < width && cols[out] != prefix.cols[in]) ++out; + if (out == width) throw std::runtime_error("Bad column-key match"); + output_tokens[out] = in; rho[in] = out; + } + auto code = packed_permutation(output_tokens,width); + scalar_permutations.insert(code); + if (!routes.count(code)) { + found = true; chosen_prefix = prefix.word; chosen_suffix = word; + chosen_rho = rho; return; + } + } + return; + } + auto [a,b] = pairs[gates-1-depth]; + for (int k = 0; k < 6 && !found; ++k) + backward(depth+1,apply(rows,a,b,k),word | (uint32_t(k) << (3*depth))); + }; + backward(0,identity,0); + std::cout << "{\"id\":" << id << ",\"W\":" << width + << ",\"routing_permutations\":" << routes.size() + << ",\"prefix_assignments\":" << prefix_count + << ",\"prefix_keys\":" << prefixes.size() + << ",\"suffix_assignments\":" << suffix_count + << ",\"matching_full_words\":" << matches + << ",\"scalar_permutations\":" << scalar_permutations.size() + << ",\"nonroutable_scalar_permutation\":" << (found ? "true" : "false"); + if (found) { + std::cout << ",\"choices\":["; + std::vector choices; + for (int i = 0; i < split; ++i) choices.push_back((chosen_prefix >> (3*i)) & 7); + for (int i = gates-split-1; i >= 0; --i) choices.push_back(INVERSE[(chosen_suffix >> (3*i)) & 7]); + Rows transfer = identity; + for (int i = 0; i < gates; ++i) { + if (i) std::cout << ','; + std::cout << choices[i]; + transfer = apply(transfer,pairs[i].first,pairs[i].second,choices[i]); + } + std::cout << "],\"rho\":["; + for (int i = 0; i < width; ++i) { + if (transfer[chosen_rho[i]] != (1 << i)) throw std::runtime_error("Wrong recovered permutation"); + if (i) std::cout << ','; + std::cout << chosen_rho[i]; + } + std::cout << ']'; + } + std::cout << "}" << std::endl; +} + +int main(int argc, char** argv) { + const bool scan_all = argc == 2 && std::string(argv[1]) == "--all-permutations"; + if (argc != 1 && !scan_all) throw std::runtime_error("Unknown discovery mode"); + int id, width, gates, prescribed; + while (std::cin >> id >> width >> gates >> prescribed) { + if (width < 2 || width > 10 || gates < 0 || gates > 16 || prescribed > width) + throw std::runtime_error("Input outside explicit discovery budget"); + std::vector> pairs(gates); + for (auto& p : pairs) { + std::cin >> p.first >> p.second; + if (p.first < 0 || p.second < 0 || p.first >= width || p.second >= width || p.first == p.second) + throw std::runtime_error("Invalid gate pair"); + } + std::vector input_fixed, output_fixed; + for (int i = 0, a, b; i < prescribed; ++i) { + std::cin >> a >> b; input_fixed.push_back(a); output_fixed.push_back(b); + } + if (scan_all) { all_permutations(id,width,pairs); continue; } + const int split = gates / 2; + Rows identity{}; + for (int j = 0; j < width; ++j) identity[j] = 1 << j; + std::unordered_map prefixes; + prefixes.reserve(300000); + uint64_t prefix_count = 0, suffix_count = 0; + std::function forward = [&](int depth, Rows rows, uint32_t word) { + if (depth == split) { + prefixes.emplace(key(rows, width, input_fixed), word); ++prefix_count; return; + } + auto [a,b] = pairs[depth]; + for (int k = 0; k < 6; ++k) + forward(depth + 1, apply(rows,a,b,k), word | (uint32_t(k) << (3*depth))); + }; + forward(0,identity,0); + bool found = false; + uint32_t chosen_prefix = 0, chosen_inverse_suffix = 0; + Rows matched_inverse{}; + std::function backward = [&](int depth, Rows rows, uint32_t word) { + if (found) return; + if (depth == gates - split) { + ++suffix_count; + auto it = prefixes.find(key(rows, width, output_fixed)); + if (it != prefixes.end()) { + found = true; chosen_prefix = it->second; + chosen_inverse_suffix = word; matched_inverse = rows; + } + return; + } + auto [a,b] = pairs[gates - 1 - depth]; + for (int k = 0; k < 6 && !found; ++k) + backward(depth + 1, apply(rows,a,b,k), word | (uint32_t(k) << (3*depth))); + }; + backward(0,identity,0); + std::cout << "{\"id\":" << id << ",\"W\":" << width + << ",\"prefix_assignments\":" << prefix_count + << ",\"prefix_keys\":" << prefixes.size() + << ",\"suffix_assignments\":" << suffix_count + << ",\"exists\":" << (found ? "true" : "false"); + if (found) { + std::vector choices; + for (int i = 0; i < split; ++i) choices.push_back((chosen_prefix >> (3*i)) & 7); + for (int i = gates-split-1; i >= 0; --i) + choices.push_back(INVERSE[(chosen_inverse_suffix >> (3*i)) & 7]); + Rows transfer = identity; + for (int i = 0; i < gates; ++i) + transfer = apply(transfer,pairs[i].first,pairs[i].second,choices[i]); + std::array rho{}; + std::array occupied{}; + for (int out = 0; out < width; ++out) { + const int row = transfer[out]; + if (!row || (row & (row-1))) throw std::runtime_error("Nonpermutation recovery"); + int in = 0; while ((1 << in) != row) ++in; + if (occupied[in]) throw std::runtime_error("Repeated permutation input"); + occupied[in] = true; rho[in] = out; + } + for (int i = 0; i < prescribed; ++i) + if (rho[input_fixed[i]] != output_fixed[i]) throw std::runtime_error("Wrong fixed terminal"); + std::cout << ",\"choices\":["; + for (int i = 0; i < gates; ++i) { if (i) std::cout << ','; std::cout << choices[i]; } + std::cout << "],\"rho\":["; + for (int i = 0; i < width; ++i) { if (i) std::cout << ','; std::cout << rho[i]; } + std::cout << ']'; + } + std::cout << "}" << std::endl; + } +} diff --git a/research/percent-exponent-architecture/discovery/fano_reuse.py b/research/percent-exponent-architecture/discovery/fano_reuse.py new file mode 100644 index 0000000000..912d4e6cc5 --- /dev/null +++ b/research/percent-exponent-architecture/discovery/fano_reuse.py @@ -0,0 +1,107 @@ +#!/usr/bin/env python3 +"""Enumerate chronological reuse of the balanced Fano network's free stubs. + +This changes the graph before scalar synthesis. It never appends a generic +decoder. A surviving topology must retain the three original routing demands +as an obstruction; every remaining input is still independent. +""" +from __future__ import annotations + +import argparse +from itertools import product +import json +from pathlib import Path +import sys + +PACKAGE = Path(__file__).resolve().parents[1] +sys.path.insert(0, str(PACKAGE / "references")) +from balanced_fano import balanced_fano + + +def partial_routes(width, pairs, prescribed): + """Exact simultaneous routing of the three prescribed source tokens.""" + inputs = tuple(sorted(prescribed)) + states = {inputs} + for a, b in pairs: + states |= {tuple(b if p == a else a if p == b else p for p in s) + for s in states} + destination = tuple(prescribed[p] for p in inputs) + return {"routable": destination in states, + "reachable_token_placements": len(states), + "prescribed_destination": list(destination)} + + +def topologies(): + base = balanced_fano() + time = {name: i for i, name in enumerate(base["gate_vertices"])} + donors = [(name, role) for name, role in base["auxiliary_outputs"] + if any(time[name] < time[rec] for rec, _ in base["auxiliary_inputs"])] + recipients = [(name, role) for name, role in base["auxiliary_inputs"] + if any(time[don] < time[name] for don, _ in donors)] + options = [[None] + [(don, role) for don, role in donors if time[don] < time[rec]] + for rec, _ in recipients] + count = 0 + for choice in product(*options): + chosen = [p for p in choice if p is not None] + if len(chosen) != len(set(chosen)): + continue + parent = list(range(base["W"])) + + def find(i): + while parent[i] != i: + i = parent[i] + return i + + reused = [] + removed_inputs = set() + for (receiver, r), donor in zip(recipients, choice): + if donor is None: + continue + vertex, d = donor + assert time[vertex] < time[receiver] + assert find(r) != find(d) + parent[find(r)] = find(d) + reused.append({"from_vertex": vertex, "from_role": d, + "to_vertex": receiver, "to_role": r}) + removed_inputs.add(r) + independent = [i for i in range(base["W"]) if i not in removed_inputs] + assert len({find(i) for i in independent}) == len(independent) + index = {find(i): k for k, i in enumerate(independent)} + renumber = [index[find(i)] for i in range(base["W"])] + pairs = [[renumber[a], renumber[b]] for a, b in base["pairs"]] + assert all(a != b for a, b in pairs) + prescribed = {renumber[i]: renumber[j] for i, j in base["prescribed"].items()} + width = len(independent) + donated = {d for _, d in chosen} + final_roles = list(base["prescribed"].values()) + [ + r for _, r in base["auxiliary_outputs"] if r not in donated] + assert sorted(renumber[r] for r in final_roles) == list(range(width)) + route = partial_routes(width, pairs, prescribed) + yield {"id": count, "W": width, "pairs": pairs, + "prescribed": prescribed, "reuse": reused, + "independent_original_roles": independent, + "old_to_new_roles": renumber, "routing": route} + count += 1 + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--output", type=Path, required=True) + args = parser.parse_args() + cases = list(topologies()) + args.output.mkdir(parents=True, exist_ok=True) + (args.output / "topologies.json").write_text(json.dumps(cases, indent=2) + "\n") + survivors = [c for c in cases if not c["routing"]["routable"]] + lines = [] + for c in survivors: + nums = [c["id"], c["W"], len(c["pairs"]), len(c["prescribed"])] + nums += [x for pair in c["pairs"] for x in pair] + nums += [x for pair in sorted(c["prescribed"].items()) for x in pair] + lines.append(" ".join(map(str, nums))) + (args.output / "search-input.txt").write_text("\n".join(lines) + "\n") + print(json.dumps({"topologies": len(cases), "routing_obstruction_survivors": len(survivors), + "surviving_widths": sorted({c["W"] for c in survivors})})) + + +if __name__ == "__main__": + main() diff --git a/research/percent-exponent-architecture/discovery/receipts/vector-k2.json b/research/percent-exponent-architecture/discovery/receipts/vector-k2.json new file mode 100644 index 0000000000..87edbf4181 --- /dev/null +++ b/research/percent-exponent-architecture/discovery/receipts/vector-k2.json @@ -0,0 +1,162 @@ +[ + { + "W": 20, + "block": 2, + "case_id": 0, + "elapsed_seconds": 0.08390658199641621, + "scope": "Fixed balanced topology, arbitrary GL(2k,F2) gates and free auxiliary bit permutation; solver discovery only.", + "solver": "5.1.0", + "status": "unsat", + "timeout_ms": 30000 + }, + { + "W": 18, + "block": 2, + "case_id": 3, + "elapsed_seconds": 0.04322447300364729, + "scope": "Fixed balanced topology, arbitrary GL(2k,F2) gates and free auxiliary bit permutation; solver discovery only.", + "solver": "5.1.0", + "status": "unsat", + "timeout_ms": 30000 + }, + { + "W": 18, + "block": 2, + "case_id": 4, + "elapsed_seconds": 0.0316019320016494, + "scope": "Fixed balanced topology, arbitrary GL(2k,F2) gates and free auxiliary bit permutation; solver discovery only.", + "solver": "5.1.0", + "status": "unsat", + "timeout_ms": 30000 + }, + { + "W": 18, + "block": 2, + "case_id": 13, + "elapsed_seconds": 0.03002273699530633, + "scope": "Fixed balanced topology, arbitrary GL(2k,F2) gates and free auxiliary bit permutation; solver discovery only.", + "solver": "5.1.0", + "status": "unsat", + "timeout_ms": 30000 + }, + { + "W": 16, + "block": 2, + "case_id": 16, + "elapsed_seconds": 0.035645643998577725, + "scope": "Fixed balanced topology, arbitrary GL(2k,F2) gates and free auxiliary bit permutation; solver discovery only.", + "solver": "5.1.0", + "status": "unsat", + "timeout_ms": 30000 + }, + { + "W": 18, + "block": 2, + "case_id": 34, + "elapsed_seconds": 0.032037665994721465, + "scope": "Fixed balanced topology, arbitrary GL(2k,F2) gates and free auxiliary bit permutation; solver discovery only.", + "solver": "5.1.0", + "status": "unsat", + "timeout_ms": 30000 + }, + { + "W": 16, + "block": 2, + "case_id": 36, + "elapsed_seconds": 0.0359503660001792, + "scope": "Fixed balanced topology, arbitrary GL(2k,F2) gates and free auxiliary bit permutation; solver discovery only.", + "solver": "5.1.0", + "status": "unsat", + "timeout_ms": 30000 + }, + { + "W": 16, + "block": 2, + "case_id": 37, + "elapsed_seconds": 0.027729383000405505, + "scope": "Fixed balanced topology, arbitrary GL(2k,F2) gates and free auxiliary bit permutation; solver discovery only.", + "solver": "5.1.0", + "status": "unsat", + "timeout_ms": 30000 + }, + { + "W": 16, + "block": 2, + "case_id": 41, + "elapsed_seconds": 0.027134439995279536, + "scope": "Fixed balanced topology, arbitrary GL(2k,F2) gates and free auxiliary bit permutation; solver discovery only.", + "solver": "5.1.0", + "status": "unsat", + "timeout_ms": 30000 + }, + { + "W": 14, + "block": 2, + "case_id": 43, + "elapsed_seconds": 0.6225613789938507, + "scope": "Fixed balanced topology, arbitrary GL(2k,F2) gates and free auxiliary bit permutation; solver discovery only.", + "solver": "5.1.0", + "status": "unsat", + "timeout_ms": 30000 + }, + { + "W": 18, + "block": 2, + "case_id": 47, + "elapsed_seconds": 0.0325405019975733, + "scope": "Fixed balanced topology, arbitrary GL(2k,F2) gates and free auxiliary bit permutation; solver discovery only.", + "solver": "5.1.0", + "status": "unsat", + "timeout_ms": 30000 + }, + { + "W": 16, + "block": 2, + "case_id": 50, + "elapsed_seconds": 0.02946661399619188, + "scope": "Fixed balanced topology, arbitrary GL(2k,F2) gates and free auxiliary bit permutation; solver discovery only.", + "solver": "5.1.0", + "status": "unsat", + "timeout_ms": 30000 + }, + { + "W": 16, + "block": 2, + "case_id": 60, + "elapsed_seconds": 0.029642137000337243, + "scope": "Fixed balanced topology, arbitrary GL(2k,F2) gates and free auxiliary bit permutation; solver discovery only.", + "solver": "5.1.0", + "status": "unsat", + "timeout_ms": 30000 + }, + { + "W": 14, + "block": 2, + "case_id": 62, + "elapsed_seconds": 0.18776335099391872, + "scope": "Fixed balanced topology, arbitrary GL(2k,F2) gates and free auxiliary bit permutation; solver discovery only.", + "solver": "5.1.0", + "status": "unsat", + "timeout_ms": 30000 + }, + { + "W": 18, + "block": 2, + "case_id": 67, + "elapsed_seconds": 0.07445067400112748, + "scope": "Fixed balanced topology, arbitrary GL(2k,F2) gates and free auxiliary bit permutation; solver discovery only.", + "solver": "5.1.0", + "status": "unsat", + "timeout_ms": 30000 + }, + { + "W": 16, + "block": 2, + "case_id": 70, + "elapsed_seconds": 0.4399162910049199, + "scope": "Fixed balanced topology, arbitrary GL(2k,F2) gates and free auxiliary bit permutation; solver discovery only.", + "solver": "5.1.0", + "status": "unsat", + "timeout_ms": 30000 + } +] diff --git a/research/percent-exponent-architecture/discovery/receipts/vector-k3-canonical.json b/research/percent-exponent-architecture/discovery/receipts/vector-k3-canonical.json new file mode 100644 index 0000000000..2d10984da3 --- /dev/null +++ b/research/percent-exponent-architecture/discovery/receipts/vector-k3-canonical.json @@ -0,0 +1,178 @@ +[ + { + "W": 30, + "block": 3, + "canonical_internal_edge_bases": true, + "case_id": 0, + "elapsed_seconds": 0.15675677400577115, + "scope": "Fixed balanced topology, arbitrary GL(2k,F2) gates and free auxiliary bit permutation; solver discovery only.", + "solver": "5.1.0", + "status": "unsat", + "timeout_ms": 30000 + }, + { + "W": 27, + "block": 3, + "canonical_internal_edge_bases": true, + "case_id": 3, + "elapsed_seconds": 0.2439698100060923, + "scope": "Fixed balanced topology, arbitrary GL(2k,F2) gates and free auxiliary bit permutation; solver discovery only.", + "solver": "5.1.0", + "status": "unsat", + "timeout_ms": 30000 + }, + { + "W": 27, + "block": 3, + "canonical_internal_edge_bases": true, + "case_id": 4, + "elapsed_seconds": 0.16877985899918713, + "scope": "Fixed balanced topology, arbitrary GL(2k,F2) gates and free auxiliary bit permutation; solver discovery only.", + "solver": "5.1.0", + "status": "unsat", + "timeout_ms": 30000 + }, + { + "W": 27, + "block": 3, + "canonical_internal_edge_bases": true, + "case_id": 13, + "elapsed_seconds": 0.15741428400360746, + "scope": "Fixed balanced topology, arbitrary GL(2k,F2) gates and free auxiliary bit permutation; solver discovery only.", + "solver": "5.1.0", + "status": "unsat", + "timeout_ms": 30000 + }, + { + "W": 24, + "block": 3, + "canonical_internal_edge_bases": true, + "case_id": 16, + "elapsed_seconds": 0.6926457559966366, + "scope": "Fixed balanced topology, arbitrary GL(2k,F2) gates and free auxiliary bit permutation; solver discovery only.", + "solver": "5.1.0", + "status": "unsat", + "timeout_ms": 30000 + }, + { + "W": 27, + "block": 3, + "canonical_internal_edge_bases": true, + "case_id": 34, + "elapsed_seconds": 0.1434111650014529, + "scope": "Fixed balanced topology, arbitrary GL(2k,F2) gates and free auxiliary bit permutation; solver discovery only.", + "solver": "5.1.0", + "status": "unsat", + "timeout_ms": 30000 + }, + { + "W": 24, + "block": 3, + "canonical_internal_edge_bases": true, + "case_id": 36, + "elapsed_seconds": 0.14983427499828395, + "scope": "Fixed balanced topology, arbitrary GL(2k,F2) gates and free auxiliary bit permutation; solver discovery only.", + "solver": "5.1.0", + "status": "unsat", + "timeout_ms": 30000 + }, + { + "W": 24, + "block": 3, + "canonical_internal_edge_bases": true, + "case_id": 37, + "elapsed_seconds": 0.3101165990010486, + "scope": "Fixed balanced topology, arbitrary GL(2k,F2) gates and free auxiliary bit permutation; solver discovery only.", + "solver": "5.1.0", + "status": "unsat", + "timeout_ms": 30000 + }, + { + "W": 24, + "block": 3, + "canonical_internal_edge_bases": true, + "case_id": 41, + "elapsed_seconds": 0.13760596999782138, + "scope": "Fixed balanced topology, arbitrary GL(2k,F2) gates and free auxiliary bit permutation; solver discovery only.", + "solver": "5.1.0", + "status": "unsat", + "timeout_ms": 30000 + }, + { + "W": 21, + "block": 3, + "canonical_internal_edge_bases": true, + "case_id": 43, + "elapsed_seconds": 1.192008750003879, + "scope": "Fixed balanced topology, arbitrary GL(2k,F2) gates and free auxiliary bit permutation; solver discovery only.", + "solver": "5.1.0", + "status": "unsat", + "timeout_ms": 30000 + }, + { + "W": 27, + "block": 3, + "canonical_internal_edge_bases": true, + "case_id": 47, + "elapsed_seconds": 0.15285538799798815, + "scope": "Fixed balanced topology, arbitrary GL(2k,F2) gates and free auxiliary bit permutation; solver discovery only.", + "solver": "5.1.0", + "status": "unsat", + "timeout_ms": 30000 + }, + { + "W": 24, + "block": 3, + "canonical_internal_edge_bases": true, + "case_id": 50, + "elapsed_seconds": 0.20848940200085053, + "scope": "Fixed balanced topology, arbitrary GL(2k,F2) gates and free auxiliary bit permutation; solver discovery only.", + "solver": "5.1.0", + "status": "unsat", + "timeout_ms": 30000 + }, + { + "W": 24, + "block": 3, + "canonical_internal_edge_bases": true, + "case_id": 60, + "elapsed_seconds": 0.14178073199582286, + "scope": "Fixed balanced topology, arbitrary GL(2k,F2) gates and free auxiliary bit permutation; solver discovery only.", + "solver": "5.1.0", + "status": "unsat", + "timeout_ms": 30000 + }, + { + "W": 21, + "block": 3, + "canonical_internal_edge_bases": true, + "case_id": 62, + "elapsed_seconds": 0.22376338899630355, + "scope": "Fixed balanced topology, arbitrary GL(2k,F2) gates and free auxiliary bit permutation; solver discovery only.", + "solver": "5.1.0", + "status": "unsat", + "timeout_ms": 30000 + }, + { + "W": 27, + "block": 3, + "canonical_internal_edge_bases": true, + "case_id": 67, + "elapsed_seconds": 0.14402453799993964, + "scope": "Fixed balanced topology, arbitrary GL(2k,F2) gates and free auxiliary bit permutation; solver discovery only.", + "solver": "5.1.0", + "status": "unsat", + "timeout_ms": 30000 + }, + { + "W": 24, + "block": 3, + "canonical_internal_edge_bases": true, + "case_id": 70, + "elapsed_seconds": 0.24018301400064956, + "scope": "Fixed balanced topology, arbitrary GL(2k,F2) gates and free auxiliary bit permutation; solver discovery only.", + "solver": "5.1.0", + "status": "unsat", + "timeout_ms": 30000 + } +] diff --git a/research/percent-exponent-architecture/discovery/receipts/vector-k3.json b/research/percent-exponent-architecture/discovery/receipts/vector-k3.json new file mode 100644 index 0000000000..d468c63360 --- /dev/null +++ b/research/percent-exponent-architecture/discovery/receipts/vector-k3.json @@ -0,0 +1,165 @@ +[ + { + "W": 30, + "block": 3, + "case_id": 0, + "elapsed_seconds": 0.301878983998904, + "scope": "Fixed balanced topology, arbitrary GL(2k,F2) gates and free auxiliary bit permutation; solver discovery only.", + "solver": "5.1.0", + "status": "unsat", + "timeout_ms": 30000 + }, + { + "W": 27, + "block": 3, + "case_id": 3, + "elapsed_seconds": 0.5156547680016956, + "scope": "Fixed balanced topology, arbitrary GL(2k,F2) gates and free auxiliary bit permutation; solver discovery only.", + "solver": "5.1.0", + "status": "unsat", + "timeout_ms": 30000 + }, + { + "W": 27, + "block": 3, + "case_id": 4, + "elapsed_seconds": 1.0573794480005745, + "scope": "Fixed balanced topology, arbitrary GL(2k,F2) gates and free auxiliary bit permutation; solver discovery only.", + "solver": "5.1.0", + "status": "unsat", + "timeout_ms": 30000 + }, + { + "W": 27, + "block": 3, + "case_id": 13, + "elapsed_seconds": 0.1497653759943205, + "scope": "Fixed balanced topology, arbitrary GL(2k,F2) gates and free auxiliary bit permutation; solver discovery only.", + "solver": "5.1.0", + "status": "unsat", + "timeout_ms": 30000 + }, + { + "W": 24, + "block": 3, + "case_id": 16, + "elapsed_seconds": 1.3012972610013094, + "scope": "Fixed balanced topology, arbitrary GL(2k,F2) gates and free auxiliary bit permutation; solver discovery only.", + "solver": "5.1.0", + "status": "unsat", + "timeout_ms": 30000 + }, + { + "W": 27, + "block": 3, + "case_id": 34, + "elapsed_seconds": 2.0745798500065575, + "scope": "Fixed balanced topology, arbitrary GL(2k,F2) gates and free auxiliary bit permutation; solver discovery only.", + "solver": "5.1.0", + "status": "unsat", + "timeout_ms": 30000 + }, + { + "W": 24, + "block": 3, + "case_id": 36, + "elapsed_seconds": 2.4167229930026224, + "scope": "Fixed balanced topology, arbitrary GL(2k,F2) gates and free auxiliary bit permutation; solver discovery only.", + "solver": "5.1.0", + "status": "unsat", + "timeout_ms": 30000 + }, + { + "W": 24, + "block": 3, + "case_id": 37, + "elapsed_seconds": 1.3961161529950914, + "scope": "Fixed balanced topology, arbitrary GL(2k,F2) gates and free auxiliary bit permutation; solver discovery only.", + "solver": "5.1.0", + "status": "unsat", + "timeout_ms": 30000 + }, + { + "W": 24, + "block": 3, + "case_id": 41, + "elapsed_seconds": 0.25829674000124214, + "scope": "Fixed balanced topology, arbitrary GL(2k,F2) gates and free auxiliary bit permutation; solver discovery only.", + "solver": "5.1.0", + "status": "unsat", + "timeout_ms": 30000 + }, + { + "W": 21, + "block": 3, + "case_id": 43, + "elapsed_seconds": 30.004746368998894, + "reason": "timeout", + "scope": "Fixed balanced topology, arbitrary GL(2k,F2) gates and free auxiliary bit permutation; solver discovery only.", + "solver": "5.1.0", + "status": "unknown", + "timeout_ms": 30000 + }, + { + "W": 27, + "block": 3, + "case_id": 47, + "elapsed_seconds": 4.603576653003984, + "scope": "Fixed balanced topology, arbitrary GL(2k,F2) gates and free auxiliary bit permutation; solver discovery only.", + "solver": "5.1.0", + "status": "unsat", + "timeout_ms": 30000 + }, + { + "W": 24, + "block": 3, + "case_id": 50, + "elapsed_seconds": 5.056007115003013, + "scope": "Fixed balanced topology, arbitrary GL(2k,F2) gates and free auxiliary bit permutation; solver discovery only.", + "solver": "5.1.0", + "status": "unsat", + "timeout_ms": 30000 + }, + { + "W": 24, + "block": 3, + "case_id": 60, + "elapsed_seconds": 1.6813189849999617, + "scope": "Fixed balanced topology, arbitrary GL(2k,F2) gates and free auxiliary bit permutation; solver discovery only.", + "solver": "5.1.0", + "status": "unsat", + "timeout_ms": 30000 + }, + { + "W": 21, + "block": 3, + "case_id": 62, + "elapsed_seconds": 30.004507912999543, + "reason": "timeout", + "scope": "Fixed balanced topology, arbitrary GL(2k,F2) gates and free auxiliary bit permutation; solver discovery only.", + "solver": "5.1.0", + "status": "unknown", + "timeout_ms": 30000 + }, + { + "W": 27, + "block": 3, + "case_id": 67, + "elapsed_seconds": 3.4740445950010326, + "scope": "Fixed balanced topology, arbitrary GL(2k,F2) gates and free auxiliary bit permutation; solver discovery only.", + "solver": "5.1.0", + "status": "unsat", + "timeout_ms": 30000 + }, + { + "W": 24, + "block": 3, + "case_id": 70, + "elapsed_seconds": 30.003693307000503, + "reason": "timeout", + "scope": "Fixed balanced topology, arbitrary GL(2k,F2) gates and free auxiliary bit permutation; solver discovery only.", + "solver": "5.1.0", + "status": "unknown", + "timeout_ms": 30000 + } +] diff --git a/research/percent-exponent-architecture/discovery/receipts/vector-k4-canonical.json b/research/percent-exponent-architecture/discovery/receipts/vector-k4-canonical.json new file mode 100644 index 0000000000..8398d44516 --- /dev/null +++ b/research/percent-exponent-architecture/discovery/receipts/vector-k4-canonical.json @@ -0,0 +1,178 @@ +[ + { + "W": 40, + "block": 4, + "canonical_internal_edge_bases": true, + "case_id": 0, + "elapsed_seconds": 0.3884478109976044, + "scope": "Fixed balanced topology, arbitrary GL(2k,F2) gates and free auxiliary bit permutation; solver discovery only.", + "solver": "5.1.0", + "status": "unsat", + "timeout_ms": 30000 + }, + { + "W": 36, + "block": 4, + "canonical_internal_edge_bases": true, + "case_id": 3, + "elapsed_seconds": 1.2231093989976216, + "scope": "Fixed balanced topology, arbitrary GL(2k,F2) gates and free auxiliary bit permutation; solver discovery only.", + "solver": "5.1.0", + "status": "unsat", + "timeout_ms": 30000 + }, + { + "W": 36, + "block": 4, + "canonical_internal_edge_bases": true, + "case_id": 4, + "elapsed_seconds": 0.7701890269963769, + "scope": "Fixed balanced topology, arbitrary GL(2k,F2) gates and free auxiliary bit permutation; solver discovery only.", + "solver": "5.1.0", + "status": "unsat", + "timeout_ms": 30000 + }, + { + "W": 36, + "block": 4, + "canonical_internal_edge_bases": true, + "case_id": 13, + "elapsed_seconds": 0.35572365400003036, + "scope": "Fixed balanced topology, arbitrary GL(2k,F2) gates and free auxiliary bit permutation; solver discovery only.", + "solver": "5.1.0", + "status": "unsat", + "timeout_ms": 30000 + }, + { + "W": 32, + "block": 4, + "canonical_internal_edge_bases": true, + "case_id": 16, + "elapsed_seconds": 1.5544145349995233, + "scope": "Fixed balanced topology, arbitrary GL(2k,F2) gates and free auxiliary bit permutation; solver discovery only.", + "solver": "5.1.0", + "status": "unsat", + "timeout_ms": 30000 + }, + { + "W": 36, + "block": 4, + "canonical_internal_edge_bases": true, + "case_id": 34, + "elapsed_seconds": 0.35808689599798527, + "scope": "Fixed balanced topology, arbitrary GL(2k,F2) gates and free auxiliary bit permutation; solver discovery only.", + "solver": "5.1.0", + "status": "unsat", + "timeout_ms": 30000 + }, + { + "W": 32, + "block": 4, + "canonical_internal_edge_bases": true, + "case_id": 36, + "elapsed_seconds": 1.314940808006213, + "scope": "Fixed balanced topology, arbitrary GL(2k,F2) gates and free auxiliary bit permutation; solver discovery only.", + "solver": "5.1.0", + "status": "unsat", + "timeout_ms": 30000 + }, + { + "W": 32, + "block": 4, + "canonical_internal_edge_bases": true, + "case_id": 37, + "elapsed_seconds": 1.4739143309998326, + "scope": "Fixed balanced topology, arbitrary GL(2k,F2) gates and free auxiliary bit permutation; solver discovery only.", + "solver": "5.1.0", + "status": "unsat", + "timeout_ms": 30000 + }, + { + "W": 32, + "block": 4, + "canonical_internal_edge_bases": true, + "case_id": 41, + "elapsed_seconds": 0.3120910979996552, + "scope": "Fixed balanced topology, arbitrary GL(2k,F2) gates and free auxiliary bit permutation; solver discovery only.", + "solver": "5.1.0", + "status": "unsat", + "timeout_ms": 30000 + }, + { + "W": 28, + "block": 4, + "canonical_internal_edge_bases": true, + "case_id": 43, + "elapsed_seconds": 3.597975317003147, + "scope": "Fixed balanced topology, arbitrary GL(2k,F2) gates and free auxiliary bit permutation; solver discovery only.", + "solver": "5.1.0", + "status": "unsat", + "timeout_ms": 30000 + }, + { + "W": 36, + "block": 4, + "canonical_internal_edge_bases": true, + "case_id": 47, + "elapsed_seconds": 0.3852785830022185, + "scope": "Fixed balanced topology, arbitrary GL(2k,F2) gates and free auxiliary bit permutation; solver discovery only.", + "solver": "5.1.0", + "status": "unsat", + "timeout_ms": 30000 + }, + { + "W": 32, + "block": 4, + "canonical_internal_edge_bases": true, + "case_id": 50, + "elapsed_seconds": 1.1258174190006685, + "scope": "Fixed balanced topology, arbitrary GL(2k,F2) gates and free auxiliary bit permutation; solver discovery only.", + "solver": "5.1.0", + "status": "unsat", + "timeout_ms": 30000 + }, + { + "W": 32, + "block": 4, + "canonical_internal_edge_bases": true, + "case_id": 60, + "elapsed_seconds": 0.33207599100569496, + "scope": "Fixed balanced topology, arbitrary GL(2k,F2) gates and free auxiliary bit permutation; solver discovery only.", + "solver": "5.1.0", + "status": "unsat", + "timeout_ms": 30000 + }, + { + "W": 28, + "block": 4, + "canonical_internal_edge_bases": true, + "case_id": 62, + "elapsed_seconds": 1.3429372629980207, + "scope": "Fixed balanced topology, arbitrary GL(2k,F2) gates and free auxiliary bit permutation; solver discovery only.", + "solver": "5.1.0", + "status": "unsat", + "timeout_ms": 30000 + }, + { + "W": 36, + "block": 4, + "canonical_internal_edge_bases": true, + "case_id": 67, + "elapsed_seconds": 0.3690150699985679, + "scope": "Fixed balanced topology, arbitrary GL(2k,F2) gates and free auxiliary bit permutation; solver discovery only.", + "solver": "5.1.0", + "status": "unsat", + "timeout_ms": 30000 + }, + { + "W": 32, + "block": 4, + "canonical_internal_edge_bases": true, + "case_id": 70, + "elapsed_seconds": 2.5139326170028653, + "scope": "Fixed balanced topology, arbitrary GL(2k,F2) gates and free auxiliary bit permutation; solver discovery only.", + "solver": "5.1.0", + "status": "unsat", + "timeout_ms": 30000 + } +] diff --git a/research/percent-exponent-architecture/discovery/receipts/vector-k4.json b/research/percent-exponent-architecture/discovery/receipts/vector-k4.json new file mode 100644 index 0000000000..d6599d688d --- /dev/null +++ b/research/percent-exponent-architecture/discovery/receipts/vector-k4.json @@ -0,0 +1,173 @@ +[ + { + "W": 40, + "block": 4, + "case_id": 0, + "elapsed_seconds": 17.614681708000717, + "scope": "Fixed balanced topology, arbitrary GL(2k,F2) gates and free auxiliary bit permutation; solver discovery only.", + "solver": "5.1.0", + "status": "unsat", + "timeout_ms": 30000 + }, + { + "W": 36, + "block": 4, + "case_id": 3, + "elapsed_seconds": 30.122233105001214, + "reason": "timeout", + "scope": "Fixed balanced topology, arbitrary GL(2k,F2) gates and free auxiliary bit permutation; solver discovery only.", + "solver": "5.1.0", + "status": "unknown", + "timeout_ms": 30000 + }, + { + "W": 36, + "block": 4, + "case_id": 4, + "elapsed_seconds": 30.009896276998916, + "reason": "timeout", + "scope": "Fixed balanced topology, arbitrary GL(2k,F2) gates and free auxiliary bit permutation; solver discovery only.", + "solver": "5.1.0", + "status": "unknown", + "timeout_ms": 30000 + }, + { + "W": 36, + "block": 4, + "case_id": 13, + "elapsed_seconds": 30.007519078004407, + "reason": "timeout", + "scope": "Fixed balanced topology, arbitrary GL(2k,F2) gates and free auxiliary bit permutation; solver discovery only.", + "solver": "5.1.0", + "status": "unknown", + "timeout_ms": 30000 + }, + { + "W": 32, + "block": 4, + "case_id": 16, + "elapsed_seconds": 30.00722944700101, + "reason": "timeout", + "scope": "Fixed balanced topology, arbitrary GL(2k,F2) gates and free auxiliary bit permutation; solver discovery only.", + "solver": "5.1.0", + "status": "unknown", + "timeout_ms": 30000 + }, + { + "W": 36, + "block": 4, + "case_id": 34, + "elapsed_seconds": 17.11180779699498, + "scope": "Fixed balanced topology, arbitrary GL(2k,F2) gates and free auxiliary bit permutation; solver discovery only.", + "solver": "5.1.0", + "status": "unsat", + "timeout_ms": 30000 + }, + { + "W": 32, + "block": 4, + "case_id": 36, + "elapsed_seconds": 30.006529671001772, + "reason": "timeout", + "scope": "Fixed balanced topology, arbitrary GL(2k,F2) gates and free auxiliary bit permutation; solver discovery only.", + "solver": "5.1.0", + "status": "unknown", + "timeout_ms": 30000 + }, + { + "W": 32, + "block": 4, + "case_id": 37, + "elapsed_seconds": 30.020238129000063, + "reason": "timeout", + "scope": "Fixed balanced topology, arbitrary GL(2k,F2) gates and free auxiliary bit permutation; solver discovery only.", + "solver": "5.1.0", + "status": "unknown", + "timeout_ms": 30000 + }, + { + "W": 32, + "block": 4, + "case_id": 41, + "elapsed_seconds": 30.006549896999786, + "reason": "timeout", + "scope": "Fixed balanced topology, arbitrary GL(2k,F2) gates and free auxiliary bit permutation; solver discovery only.", + "solver": "5.1.0", + "status": "unknown", + "timeout_ms": 30000 + }, + { + "W": 28, + "block": 4, + "case_id": 43, + "elapsed_seconds": 30.097369429000537, + "reason": "timeout", + "scope": "Fixed balanced topology, arbitrary GL(2k,F2) gates and free auxiliary bit permutation; solver discovery only.", + "solver": "5.1.0", + "status": "unknown", + "timeout_ms": 30000 + }, + { + "W": 36, + "block": 4, + "case_id": 47, + "elapsed_seconds": 8.83743350199802, + "scope": "Fixed balanced topology, arbitrary GL(2k,F2) gates and free auxiliary bit permutation; solver discovery only.", + "solver": "5.1.0", + "status": "unsat", + "timeout_ms": 30000 + }, + { + "W": 32, + "block": 4, + "case_id": 50, + "elapsed_seconds": 30.10296854400076, + "reason": "timeout", + "scope": "Fixed balanced topology, arbitrary GL(2k,F2) gates and free auxiliary bit permutation; solver discovery only.", + "solver": "5.1.0", + "status": "unknown", + "timeout_ms": 30000 + }, + { + "W": 32, + "block": 4, + "case_id": 60, + "elapsed_seconds": 12.264251690001402, + "scope": "Fixed balanced topology, arbitrary GL(2k,F2) gates and free auxiliary bit permutation; solver discovery only.", + "solver": "5.1.0", + "status": "unsat", + "timeout_ms": 30000 + }, + { + "W": 28, + "block": 4, + "case_id": 62, + "elapsed_seconds": 30.00668929299718, + "reason": "timeout", + "scope": "Fixed balanced topology, arbitrary GL(2k,F2) gates and free auxiliary bit permutation; solver discovery only.", + "solver": "5.1.0", + "status": "unknown", + "timeout_ms": 30000 + }, + { + "W": 36, + "block": 4, + "case_id": 67, + "elapsed_seconds": 10.24407730299572, + "scope": "Fixed balanced topology, arbitrary GL(2k,F2) gates and free auxiliary bit permutation; solver discovery only.", + "solver": "5.1.0", + "status": "unsat", + "timeout_ms": 30000 + }, + { + "W": 32, + "block": 4, + "case_id": 70, + "elapsed_seconds": 30.007083201002388, + "reason": "timeout", + "scope": "Fixed balanced topology, arbitrary GL(2k,F2) gates and free auxiliary bit permutation; solver discovery only.", + "solver": "5.1.0", + "status": "unknown", + "timeout_ms": 30000 + } +] diff --git a/research/percent-exponent-architecture/discovery/vector_fano.py b/research/percent-exponent-architecture/discovery/vector_fano.py new file mode 100644 index 0000000000..3511bed01e --- /dev/null +++ b/research/percent-exponent-architecture/discovery/vector_fano.py @@ -0,0 +1,116 @@ +#!/usr/bin/env python3 +"""Search vector-linear, all-input completions on a fixed Fano topology. + +Each former edge holds k independent bits. Every vertex may apply any binary +linear map on all 2k incident bits. Requiring the final map to be a complete +permutation forces every local square map to be invertible. There are no +zero-initialized bits and no appended decoder. A solver UNSAT/timeout is only +a discovery receipt, not an independently checked impossibility certificate. +""" +from __future__ import annotations + +import argparse +import json +from pathlib import Path +import time + +import z3 +from fano_reuse import topologies + + +def synthesize(case, block, timeout_ms, canonical_edges=False): + width = case["W"] * block + solver = z3.SolverFor("QF_BV") + solver.set(timeout=timeout_ms, random_seed=0) + last = [z3.BitVecVal(1 << r, width) for r in range(width)] + symbolic_gates = [] + for index, (a, b) in enumerate(case["pairs"]): + roles = [block * r + j for r in (a, b) for j in range(block)] + old = [last[r] for r in roles] + coefficients = [] + for out, r in enumerate(roles): + row = [z3.Bool(f"c_{index}_{out}_{j}") for j in range(len(roles))] + coefficients.append(row) + value = z3.BitVecVal(0, width) + for coeff, operand in zip(row, old): + value = value ^ z3.If(coeff, operand, z3.BitVecVal(0, width)) + current = z3.BitVec(f"g_{index}_{out}", width) + solver.add(current == value) + last[r] = current + symbolic_gates.append((roles, coefficients)) + if canonical_edges: + # Independent basis changes on each internal block are absorbed + # into its adjacent GL(2k) vertices. A final free auxiliary block + # can sort its unit vectors; the prescribed blocks are already + # sorted. Thus row-reduced internal edge bases lose no existence + # cases in this scalar model. + for start in (0, block): + values = [last[r] for r in roles[start:start + block]] + pivots = [x & -x for x in values] + for x in values: + solver.add(x != 0) + for i in range(block - 1): + solver.add(z3.ULT(pivots[i], pivots[i + 1])) + for i in range(block): + for j in range(block): + if i != j: + solver.add(values[i] & pivots[j] == 0) + for row in last: + solver.add(row != 0, row & (row - 1) == 0) + solver.add(z3.Distinct(*last)) + for source, target in case["prescribed"].items(): + for j in range(block): + solver.add(last[block * target + j] == 1 << (block * source + j)) + start = time.monotonic() + status = solver.check() + result = {"case_id": case["id"], "block": block, "W": width, + "status": str(status), "elapsed_seconds": time.monotonic() - start, + "solver": z3.get_version_string(), "timeout_ms": timeout_ms, + "canonical_internal_edge_bases": canonical_edges, + "scope": "Fixed balanced topology, arbitrary GL(2k,F2) gates and free auxiliary bit permutation; solver discovery only."} + if status == z3.unknown: + result["reason"] = solver.reason_unknown() + if status != z3.sat: + return result + model = solver.model() + rows = [1 << r for r in range(width)] + gates = [] + for roles, coefficients in symbolic_gates: + matrix = [[int(z3.is_true(model.eval(c, model_completion=True))) for c in row] + for row in coefficients] + old = [rows[r] for r in roles] + new = [] + for row in matrix: + value = 0 + for c, operand in zip(row, old): + if c: + value ^= operand + new.append(value) + for r, value in zip(roles, new): + rows[r] = value + gates.append({"roles": roles, "matrix": matrix}) + assert sorted(rows) == [1 << r for r in range(width)] + rho = [rows.index(1 << r) for r in range(width)] + assert all(rho[block * source + j] == block * target + j + for source, target in case["prescribed"].items() for j in range(block)) + result.update(gates=gates, rho=rho, independently_replayed_all_columns=True) + return result + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--block", type=int, default=2) + parser.add_argument("--timeout-ms", type=int, default=30000) + parser.add_argument("--case", type=int, action="append") + parser.add_argument("--canonical-edges", action="store_true") + args = parser.parse_args() + assert 1 <= args.block <= 4 + cases = [c for c in topologies() if not c["routing"]["routable"]] + if args.case is not None: + cases = [c for c in cases if c["id"] in args.case] + for case in cases: + print(json.dumps(synthesize(case, args.block, args.timeout_ms, args.canonical_edges)), flush=True) + + +if __name__ == "__main__": + main() diff --git a/research/percent-exponent-architecture/enumeration-controls.json b/research/percent-exponent-architecture/enumeration-controls.json new file mode 100644 index 0000000000..d3ddb3265d --- /dev/null +++ b/research/percent-exponent-architecture/enumeration-controls.json @@ -0,0 +1,4 @@ +{ + "all_passed": true, + "direct_full_word_controls": 8 +} diff --git a/research/percent-exponent-architecture/fano-all-permutations.json b/research/percent-exponent-architecture/fano-all-permutations.json new file mode 100644 index 0000000000..f78b1e737f --- /dev/null +++ b/research/percent-exponent-architecture/fano-all-permutations.json @@ -0,0 +1,972 @@ +{ + "results": [ + { + "W": 10, + "id": 0, + "matching_full_words": 26112, + "nonroutable_scalar_permutation": false, + "prefix_assignments": 279936, + "prefix_keys": 28611, + "routing_permutations": 14064, + "scalar_permutations": 14064, + "suffix_assignments": 279936 + }, + { + "W": 9, + "id": 1, + "matching_full_words": 44544, + "nonroutable_scalar_permutation": false, + "prefix_assignments": 279936, + "prefix_keys": 28611, + "routing_permutations": 11120, + "scalar_permutations": 11120, + "suffix_assignments": 279936 + }, + { + "W": 9, + "id": 2, + "matching_full_words": 57728, + "nonroutable_scalar_permutation": false, + "prefix_assignments": 279936, + "prefix_keys": 28611, + "routing_permutations": 9152, + "scalar_permutations": 9152, + "suffix_assignments": 279936 + }, + { + "W": 9, + "id": 3, + "matching_full_words": 72448, + "nonroutable_scalar_permutation": false, + "prefix_assignments": 279936, + "prefix_keys": 28611, + "routing_permutations": 7952, + "scalar_permutations": 7952, + "suffix_assignments": 279936 + }, + { + "W": 9, + "id": 4, + "matching_full_words": 101376, + "nonroutable_scalar_permutation": false, + "prefix_assignments": 279936, + "prefix_keys": 28611, + "routing_permutations": 6448, + "scalar_permutations": 6448, + "suffix_assignments": 279936 + }, + { + "W": 9, + "id": 5, + "matching_full_words": 68096, + "nonroutable_scalar_permutation": false, + "prefix_assignments": 279936, + "prefix_keys": 28611, + "routing_permutations": 9904, + "scalar_permutations": 9904, + "suffix_assignments": 279936 + }, + { + "W": 8, + "id": 6, + "matching_full_words": 163456, + "nonroutable_scalar_permutation": false, + "prefix_assignments": 279936, + "prefix_keys": 28611, + "routing_permutations": 6024, + "scalar_permutations": 6024, + "suffix_assignments": 279936 + }, + { + "W": 8, + "id": 7, + "matching_full_words": 205184, + "nonroutable_scalar_permutation": false, + "prefix_assignments": 279936, + "prefix_keys": 28611, + "routing_permutations": 5312, + "scalar_permutations": 5312, + "suffix_assignments": 279936 + }, + { + "W": 8, + "id": 8, + "matching_full_words": 279552, + "nonroutable_scalar_permutation": false, + "prefix_assignments": 279936, + "prefix_keys": 28611, + "routing_permutations": 4320, + "scalar_permutations": 4320, + "suffix_assignments": 279936 + }, + { + "W": 9, + "id": 9, + "matching_full_words": 44544, + "nonroutable_scalar_permutation": false, + "prefix_assignments": 279936, + "prefix_keys": 28611, + "routing_permutations": 11120, + "scalar_permutations": 11120, + "suffix_assignments": 279936 + }, + { + "W": 8, + "id": 10, + "matching_full_words": 80128, + "nonroutable_scalar_permutation": false, + "prefix_assignments": 279936, + "prefix_keys": 28611, + "routing_permutations": 8032, + "scalar_permutations": 8032, + "suffix_assignments": 279936 + }, + { + "W": 8, + "id": 11, + "matching_full_words": 123648, + "nonroutable_scalar_permutation": false, + "prefix_assignments": 279936, + "prefix_keys": 28611, + "routing_permutations": 5408, + "scalar_permutations": 5408, + "suffix_assignments": 279936 + }, + { + "W": 8, + "id": 12, + "matching_full_words": 185856, + "nonroutable_scalar_permutation": false, + "prefix_assignments": 279936, + "prefix_keys": 28611, + "routing_permutations": 4656, + "scalar_permutations": 4656, + "suffix_assignments": 279936 + }, + { + "W": 9, + "id": 13, + "matching_full_words": 95232, + "nonroutable_scalar_permutation": false, + "prefix_assignments": 279936, + "prefix_keys": 28611, + "routing_permutations": 6464, + "scalar_permutations": 6464, + "suffix_assignments": 279936 + }, + { + "W": 8, + "id": 14, + "matching_full_words": 172032, + "nonroutable_scalar_permutation": false, + "prefix_assignments": 279936, + "prefix_keys": 28611, + "routing_permutations": 4768, + "scalar_permutations": 4768, + "suffix_assignments": 279936 + }, + { + "W": 8, + "id": 15, + "matching_full_words": 223488, + "nonroutable_scalar_permutation": false, + "prefix_assignments": 279936, + "prefix_keys": 28611, + "routing_permutations": 3856, + "scalar_permutations": 3856, + "suffix_assignments": 279936 + }, + { + "W": 8, + "id": 16, + "matching_full_words": 405504, + "nonroutable_scalar_permutation": false, + "prefix_assignments": 279936, + "prefix_keys": 28611, + "routing_permutations": 2816, + "scalar_permutations": 2816, + "suffix_assignments": 279936 + }, + { + "W": 9, + "id": 17, + "matching_full_words": 62464, + "nonroutable_scalar_permutation": false, + "prefix_assignments": 279936, + "prefix_keys": 28611, + "routing_permutations": 9424, + "scalar_permutations": 9424, + "suffix_assignments": 279936 + }, + { + "W": 8, + "id": 18, + "matching_full_words": 102144, + "nonroutable_scalar_permutation": false, + "prefix_assignments": 279936, + "prefix_keys": 28611, + "routing_permutations": 6592, + "scalar_permutations": 6592, + "suffix_assignments": 279936 + }, + { + "W": 8, + "id": 19, + "matching_full_words": 151680, + "nonroutable_scalar_permutation": false, + "prefix_assignments": 279936, + "prefix_keys": 28611, + "routing_permutations": 5264, + "scalar_permutations": 5264, + "suffix_assignments": 279936 + }, + { + "W": 8, + "id": 20, + "matching_full_words": 177664, + "nonroutable_scalar_permutation": false, + "prefix_assignments": 279936, + "prefix_keys": 28611, + "routing_permutations": 3680, + "scalar_permutations": 3680, + "suffix_assignments": 279936 + }, + { + "W": 9, + "id": 21, + "matching_full_words": 62464, + "nonroutable_scalar_permutation": false, + "prefix_assignments": 279936, + "prefix_keys": 25011, + "routing_permutations": 9424, + "scalar_permutations": 9424, + "suffix_assignments": 279936 + }, + { + "W": 8, + "id": 22, + "matching_full_words": 151680, + "nonroutable_scalar_permutation": false, + "prefix_assignments": 279936, + "prefix_keys": 25011, + "routing_permutations": 5264, + "scalar_permutations": 5264, + "suffix_assignments": 279936 + }, + { + "W": 8, + "id": 23, + "matching_full_words": 187648, + "nonroutable_scalar_permutation": false, + "prefix_assignments": 279936, + "prefix_keys": 25011, + "routing_permutations": 4608, + "scalar_permutations": 4608, + "suffix_assignments": 279936 + }, + { + "W": 8, + "id": 24, + "matching_full_words": 245760, + "nonroutable_scalar_permutation": false, + "prefix_assignments": 279936, + "prefix_keys": 25011, + "routing_permutations": 3728, + "scalar_permutations": 3728, + "suffix_assignments": 279936 + }, + { + "W": 8, + "id": 25, + "matching_full_words": 102144, + "nonroutable_scalar_permutation": false, + "prefix_assignments": 279936, + "prefix_keys": 25011, + "routing_permutations": 6592, + "scalar_permutations": 6592, + "suffix_assignments": 279936 + }, + { + "W": 7, + "id": 26, + "matching_full_words": 320000, + "nonroutable_scalar_permutation": false, + "prefix_assignments": 279936, + "prefix_keys": 25011, + "routing_permutations": 2544, + "scalar_permutations": 2544, + "suffix_assignments": 279936 + }, + { + "W": 7, + "id": 27, + "matching_full_words": 465408, + "nonroutable_scalar_permutation": false, + "prefix_assignments": 279936, + "prefix_keys": 25011, + "routing_permutations": 2224, + "scalar_permutations": 2224, + "suffix_assignments": 279936 + }, + { + "W": 8, + "id": 28, + "matching_full_words": 253440, + "nonroutable_scalar_permutation": false, + "prefix_assignments": 279936, + "prefix_keys": 25011, + "routing_permutations": 4128, + "scalar_permutations": 4128, + "suffix_assignments": 279936 + }, + { + "W": 7, + "id": 29, + "matching_full_words": 698112, + "nonroutable_scalar_permutation": false, + "prefix_assignments": 279936, + "prefix_keys": 25011, + "routing_permutations": 2016, + "scalar_permutations": 2016, + "suffix_assignments": 279936 + }, + { + "W": 7, + "id": 30, + "matching_full_words": 1133568, + "nonroutable_scalar_permutation": false, + "prefix_assignments": 279936, + "prefix_keys": 25011, + "routing_permutations": 1392, + "scalar_permutations": 1392, + "suffix_assignments": 279936 + }, + { + "W": 8, + "id": 31, + "matching_full_words": 145920, + "nonroutable_scalar_permutation": false, + "prefix_assignments": 279936, + "prefix_keys": 25011, + "routing_permutations": 4896, + "scalar_permutations": 4896, + "suffix_assignments": 279936 + }, + { + "W": 7, + "id": 32, + "matching_full_words": 416128, + "nonroutable_scalar_permutation": false, + "prefix_assignments": 279936, + "prefix_keys": 25011, + "routing_permutations": 2336, + "scalar_permutations": 2336, + "suffix_assignments": 279936 + }, + { + "W": 7, + "id": 33, + "matching_full_words": 434176, + "nonroutable_scalar_permutation": false, + "prefix_assignments": 279936, + "prefix_keys": 25011, + "routing_permutations": 1648, + "scalar_permutations": 1648, + "suffix_assignments": 279936 + }, + { + "W": 9, + "id": 34, + "matching_full_words": 101376, + "nonroutable_scalar_permutation": false, + "prefix_assignments": 279936, + "prefix_keys": 4995, + "routing_permutations": 6448, + "scalar_permutations": 6448, + "suffix_assignments": 279936 + }, + { + "W": 8, + "id": 35, + "matching_full_words": 185856, + "nonroutable_scalar_permutation": false, + "prefix_assignments": 279936, + "prefix_keys": 4995, + "routing_permutations": 4656, + "scalar_permutations": 4656, + "suffix_assignments": 279936 + }, + { + "W": 8, + "id": 36, + "matching_full_words": 288768, + "nonroutable_scalar_permutation": false, + "prefix_assignments": 279936, + "prefix_keys": 4995, + "routing_permutations": 3216, + "scalar_permutations": 3216, + "suffix_assignments": 279936 + }, + { + "W": 8, + "id": 37, + "matching_full_words": 470016, + "nonroutable_scalar_permutation": false, + "prefix_assignments": 279936, + "prefix_keys": 4995, + "routing_permutations": 2704, + "scalar_permutations": 2704, + "suffix_assignments": 279936 + }, + { + "W": 8, + "id": 38, + "matching_full_words": 279552, + "nonroutable_scalar_permutation": false, + "prefix_assignments": 279936, + "prefix_keys": 4995, + "routing_permutations": 4320, + "scalar_permutations": 4320, + "suffix_assignments": 279936 + }, + { + "W": 7, + "id": 39, + "matching_full_words": 903936, + "nonroutable_scalar_permutation": false, + "prefix_assignments": 279936, + "prefix_keys": 4995, + "routing_permutations": 1984, + "scalar_permutations": 1984, + "suffix_assignments": 279936 + }, + { + "W": 7, + "id": 40, + "matching_full_words": 1410048, + "nonroutable_scalar_permutation": false, + "prefix_assignments": 279936, + "prefix_keys": 4995, + "routing_permutations": 1696, + "scalar_permutations": 1696, + "suffix_assignments": 279936 + }, + { + "W": 8, + "id": 41, + "matching_full_words": 368640, + "nonroutable_scalar_permutation": false, + "prefix_assignments": 279936, + "prefix_keys": 4995, + "routing_permutations": 2912, + "scalar_permutations": 2912, + "suffix_assignments": 279936 + }, + { + "W": 7, + "id": 42, + "matching_full_words": 783360, + "nonroutable_scalar_permutation": false, + "prefix_assignments": 279936, + "prefix_keys": 4995, + "routing_permutations": 1872, + "scalar_permutations": 1872, + "suffix_assignments": 279936 + }, + { + "W": 7, + "id": 43, + "matching_full_words": 1935360, + "nonroutable_scalar_permutation": false, + "prefix_assignments": 279936, + "prefix_keys": 4995, + "routing_permutations": 1088, + "scalar_permutations": 1088, + "suffix_assignments": 279936 + }, + { + "W": 8, + "id": 44, + "matching_full_words": 245760, + "nonroutable_scalar_permutation": false, + "prefix_assignments": 279936, + "prefix_keys": 4995, + "routing_permutations": 3728, + "scalar_permutations": 3728, + "suffix_assignments": 279936 + }, + { + "W": 7, + "id": 45, + "matching_full_words": 465408, + "nonroutable_scalar_permutation": false, + "prefix_assignments": 279936, + "prefix_keys": 4995, + "routing_permutations": 2224, + "scalar_permutations": 2224, + "suffix_assignments": 279936 + }, + { + "W": 7, + "id": 46, + "matching_full_words": 768000, + "nonroutable_scalar_permutation": false, + "prefix_assignments": 279936, + "prefix_keys": 4995, + "routing_permutations": 1248, + "scalar_permutations": 1248, + "suffix_assignments": 279936 + }, + { + "W": 9, + "id": 47, + "matching_full_words": 95232, + "nonroutable_scalar_permutation": false, + "prefix_assignments": 279936, + "prefix_keys": 4995, + "routing_permutations": 6464, + "scalar_permutations": 6464, + "suffix_assignments": 279936 + }, + { + "W": 8, + "id": 48, + "matching_full_words": 223488, + "nonroutable_scalar_permutation": false, + "prefix_assignments": 279936, + "prefix_keys": 4995, + "routing_permutations": 3856, + "scalar_permutations": 3856, + "suffix_assignments": 279936 + }, + { + "W": 8, + "id": 49, + "matching_full_words": 268800, + "nonroutable_scalar_permutation": false, + "prefix_assignments": 279936, + "prefix_keys": 4995, + "routing_permutations": 3520, + "scalar_permutations": 3520, + "suffix_assignments": 279936 + }, + { + "W": 8, + "id": 50, + "matching_full_words": 368640, + "nonroutable_scalar_permutation": false, + "prefix_assignments": 279936, + "prefix_keys": 4995, + "routing_permutations": 2912, + "scalar_permutations": 2912, + "suffix_assignments": 279936 + }, + { + "W": 8, + "id": 51, + "matching_full_words": 172032, + "nonroutable_scalar_permutation": false, + "prefix_assignments": 279936, + "prefix_keys": 4995, + "routing_permutations": 4768, + "scalar_permutations": 4768, + "suffix_assignments": 279936 + }, + { + "W": 7, + "id": 52, + "matching_full_words": 502272, + "nonroutable_scalar_permutation": false, + "prefix_assignments": 279936, + "prefix_keys": 4995, + "routing_permutations": 2144, + "scalar_permutations": 2144, + "suffix_assignments": 279936 + }, + { + "W": 7, + "id": 53, + "matching_full_words": 783360, + "nonroutable_scalar_permutation": false, + "prefix_assignments": 279936, + "prefix_keys": 4995, + "routing_permutations": 1872, + "scalar_permutations": 1872, + "suffix_assignments": 279936 + }, + { + "W": 8, + "id": 54, + "matching_full_words": 377856, + "nonroutable_scalar_permutation": false, + "prefix_assignments": 279936, + "prefix_keys": 4995, + "routing_permutations": 2848, + "scalar_permutations": 2848, + "suffix_assignments": 279936 + }, + { + "W": 7, + "id": 55, + "matching_full_words": 953856, + "nonroutable_scalar_permutation": false, + "prefix_assignments": 279936, + "prefix_keys": 4995, + "routing_permutations": 1520, + "scalar_permutations": 1520, + "suffix_assignments": 279936 + }, + { + "W": 7, + "id": 56, + "matching_full_words": 1603584, + "nonroutable_scalar_permutation": false, + "prefix_assignments": 279936, + "prefix_keys": 4995, + "routing_permutations": 1216, + "scalar_permutations": 1216, + "suffix_assignments": 279936 + }, + { + "W": 8, + "id": 57, + "matching_full_words": 253440, + "nonroutable_scalar_permutation": false, + "prefix_assignments": 279936, + "prefix_keys": 4995, + "routing_permutations": 4128, + "scalar_permutations": 4128, + "suffix_assignments": 279936 + }, + { + "W": 7, + "id": 58, + "matching_full_words": 698112, + "nonroutable_scalar_permutation": false, + "prefix_assignments": 279936, + "prefix_keys": 4995, + "routing_permutations": 2016, + "scalar_permutations": 2016, + "suffix_assignments": 279936 + }, + { + "W": 7, + "id": 59, + "matching_full_words": 732672, + "nonroutable_scalar_permutation": false, + "prefix_assignments": 279936, + "prefix_keys": 4995, + "routing_permutations": 1536, + "scalar_permutations": 1536, + "suffix_assignments": 279936 + }, + { + "W": 8, + "id": 60, + "matching_full_words": 405504, + "nonroutable_scalar_permutation": false, + "prefix_assignments": 279936, + "prefix_keys": 873, + "routing_permutations": 2816, + "scalar_permutations": 2816, + "suffix_assignments": 279936 + }, + { + "W": 7, + "id": 61, + "matching_full_words": 1179648, + "nonroutable_scalar_permutation": false, + "prefix_assignments": 279936, + "prefix_keys": 873, + "routing_permutations": 1280, + "scalar_permutations": 1280, + "suffix_assignments": 279936 + }, + { + "W": 7, + "id": 62, + "matching_full_words": 1935360, + "nonroutable_scalar_permutation": false, + "prefix_assignments": 279936, + "prefix_keys": 873, + "routing_permutations": 1088, + "scalar_permutations": 1088, + "suffix_assignments": 279936 + }, + { + "W": 7, + "id": 63, + "matching_full_words": 1603584, + "nonroutable_scalar_permutation": false, + "prefix_assignments": 279936, + "prefix_keys": 873, + "routing_permutations": 1216, + "scalar_permutations": 1216, + "suffix_assignments": 279936 + }, + { + "W": 6, + "id": 64, + "matching_full_words": 9953280, + "nonroutable_scalar_permutation": false, + "prefix_assignments": 279936, + "prefix_keys": 873, + "routing_permutations": 400, + "scalar_permutations": 400, + "suffix_assignments": 279936 + }, + { + "W": 7, + "id": 65, + "matching_full_words": 1133568, + "nonroutable_scalar_permutation": false, + "prefix_assignments": 279936, + "prefix_keys": 873, + "routing_permutations": 1392, + "scalar_permutations": 1392, + "suffix_assignments": 279936 + }, + { + "W": 6, + "id": 66, + "matching_full_words": 3732480, + "nonroutable_scalar_permutation": false, + "prefix_assignments": 279936, + "prefix_keys": 873, + "routing_permutations": 432, + "scalar_permutations": 432, + "suffix_assignments": 279936 + }, + { + "W": 9, + "id": 67, + "matching_full_words": 72448, + "nonroutable_scalar_permutation": false, + "prefix_assignments": 279936, + "prefix_keys": 25011, + "routing_permutations": 7952, + "scalar_permutations": 7952, + "suffix_assignments": 279936 + }, + { + "W": 8, + "id": 68, + "matching_full_words": 123648, + "nonroutable_scalar_permutation": false, + "prefix_assignments": 279936, + "prefix_keys": 25011, + "routing_permutations": 5408, + "scalar_permutations": 5408, + "suffix_assignments": 279936 + }, + { + "W": 8, + "id": 69, + "matching_full_words": 227968, + "nonroutable_scalar_permutation": false, + "prefix_assignments": 279936, + "prefix_keys": 25011, + "routing_permutations": 3248, + "scalar_permutations": 3248, + "suffix_assignments": 279936 + }, + { + "W": 8, + "id": 70, + "matching_full_words": 288768, + "nonroutable_scalar_permutation": false, + "prefix_assignments": 279936, + "prefix_keys": 25011, + "routing_permutations": 3216, + "scalar_permutations": 3216, + "suffix_assignments": 279936 + }, + { + "W": 8, + "id": 71, + "matching_full_words": 205184, + "nonroutable_scalar_permutation": false, + "prefix_assignments": 279936, + "prefix_keys": 25011, + "routing_permutations": 5312, + "scalar_permutations": 5312, + "suffix_assignments": 279936 + }, + { + "W": 7, + "id": 72, + "matching_full_words": 726400, + "nonroutable_scalar_permutation": false, + "prefix_assignments": 279936, + "prefix_keys": 25011, + "routing_permutations": 2000, + "scalar_permutations": 2000, + "suffix_assignments": 279936 + }, + { + "W": 7, + "id": 73, + "matching_full_words": 903936, + "nonroutable_scalar_permutation": false, + "prefix_assignments": 279936, + "prefix_keys": 25011, + "routing_permutations": 1984, + "scalar_permutations": 1984, + "suffix_assignments": 279936 + }, + { + "W": 8, + "id": 74, + "matching_full_words": 268800, + "nonroutable_scalar_permutation": false, + "prefix_assignments": 279936, + "prefix_keys": 25011, + "routing_permutations": 3520, + "scalar_permutations": 3520, + "suffix_assignments": 279936 + }, + { + "W": 7, + "id": 75, + "matching_full_words": 502272, + "nonroutable_scalar_permutation": false, + "prefix_assignments": 279936, + "prefix_keys": 25011, + "routing_permutations": 2144, + "scalar_permutations": 2144, + "suffix_assignments": 279936 + }, + { + "W": 7, + "id": 76, + "matching_full_words": 1179648, + "nonroutable_scalar_permutation": false, + "prefix_assignments": 279936, + "prefix_keys": 25011, + "routing_permutations": 1280, + "scalar_permutations": 1280, + "suffix_assignments": 279936 + }, + { + "W": 8, + "id": 77, + "matching_full_words": 187648, + "nonroutable_scalar_permutation": false, + "prefix_assignments": 279936, + "prefix_keys": 25011, + "routing_permutations": 4608, + "scalar_permutations": 4608, + "suffix_assignments": 279936 + }, + { + "W": 7, + "id": 78, + "matching_full_words": 320000, + "nonroutable_scalar_permutation": false, + "prefix_assignments": 279936, + "prefix_keys": 25011, + "routing_permutations": 2544, + "scalar_permutations": 2544, + "suffix_assignments": 279936 + }, + { + "W": 7, + "id": 79, + "matching_full_words": 602112, + "nonroutable_scalar_permutation": false, + "prefix_assignments": 279936, + "prefix_keys": 25011, + "routing_permutations": 1344, + "scalar_permutations": 1344, + "suffix_assignments": 279936 + }, + { + "W": 8, + "id": 80, + "matching_full_words": 177664, + "nonroutable_scalar_permutation": false, + "prefix_assignments": 279936, + "prefix_keys": 20493, + "routing_permutations": 3680, + "scalar_permutations": 3680, + "suffix_assignments": 279936 + }, + { + "W": 7, + "id": 81, + "matching_full_words": 602112, + "nonroutable_scalar_permutation": false, + "prefix_assignments": 279936, + "prefix_keys": 20493, + "routing_permutations": 1344, + "scalar_permutations": 1344, + "suffix_assignments": 279936 + }, + { + "W": 7, + "id": 82, + "matching_full_words": 768000, + "nonroutable_scalar_permutation": false, + "prefix_assignments": 279936, + "prefix_keys": 20493, + "routing_permutations": 1248, + "scalar_permutations": 1248, + "suffix_assignments": 279936 + }, + { + "W": 7, + "id": 83, + "matching_full_words": 732672, + "nonroutable_scalar_permutation": false, + "prefix_assignments": 279936, + "prefix_keys": 20493, + "routing_permutations": 1536, + "scalar_permutations": 1536, + "suffix_assignments": 279936 + }, + { + "W": 6, + "id": 84, + "matching_full_words": 3732480, + "nonroutable_scalar_permutation": false, + "prefix_assignments": 279936, + "prefix_keys": 20493, + "routing_permutations": 432, + "scalar_permutations": 432, + "suffix_assignments": 279936 + }, + { + "W": 7, + "id": 85, + "matching_full_words": 434176, + "nonroutable_scalar_permutation": false, + "prefix_assignments": 279936, + "prefix_keys": 20493, + "routing_permutations": 1648, + "scalar_permutations": 1648, + "suffix_assignments": 279936 + }, + { + "W": 6, + "id": 86, + "matching_full_words": 1544704, + "nonroutable_scalar_permutation": false, + "prefix_assignments": 279936, + "prefix_keys": 20493, + "routing_permutations": 432, + "scalar_permutations": 432, + "suffix_assignments": 279936 + } + ], + "scope": "All 87 chronological balanced-Fano stub reuses; all local GL(2,F2) gates; every full output permutation, including arbitrary auxiliary/data exchanges. This does not cover vector gates or other graphs.", + "status": "ALL COMPLETED SCALAR PERMUTATIONS ARE ROUTABLE IN THIS FINITE FAMILY", + "topologies": 87, + "topology_specification_sha256": "c423c71fd035fbb6b0428163b87680939eb3a6596962082e39d0823f3e3183b2", + "width_counts": { + "6": 4, + "7": 32, + "8": 38, + "9": 12, + "10": 1 + } +} diff --git a/research/percent-exponent-architecture/fano-reuse-certificate.json b/research/percent-exponent-architecture/fano-reuse-certificate.json new file mode 100644 index 0000000000..fac670e9bf --- /dev/null +++ b/research/percent-exponent-architecture/fano-reuse-certificate.json @@ -0,0 +1,2128 @@ +{ + "cases": [ + { + "scalar_exhaustion": { + "W": 10, + "exhaustive_negative": true, + "exists": false, + "full_assignment_count": 78364164096, + "gates": 14, + "prefix_assignments": 279936, + "prefix_keys": 258156, + "prefix_sha256": "b34379c5feeb67216fb7531294f13da5f67ce4a22f92b94ff8ea2b26f3aa21ec", + "prescribed": { + "0": 7, + "1": 0, + "2": 3 + }, + "scope": "Existence with a free permutation of unprescribed roles; not an enumeration of every matching circuit.", + "split": 7, + "suffix_assignments": 279936, + "suffix_sha256": "a19c1f14c463451e7bdd0900a2aeae701d98bcee790e9145d70e05c316555c38", + "witness": null + }, + "topology": { + "W": 10, + "id": 0, + "independent_original_roles": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 8, + 9 + ], + "old_to_new_roles": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 8, + 9 + ], + "pairs": [ + [ + 0, + 3 + ], + [ + 1, + 4 + ], + [ + 2, + 5 + ], + [ + 0, + 1 + ], + [ + 4, + 2 + ], + [ + 0, + 6 + ], + [ + 4, + 7 + ], + [ + 0, + 4 + ], + [ + 5, + 6 + ], + [ + 0, + 8 + ], + [ + 5, + 9 + ], + [ + 0, + 5 + ], + [ + 7, + 9 + ], + [ + 3, + 8 + ] + ], + "prescribed": { + "0": 7, + "1": 0, + "2": 3 + }, + "reuse": [], + "routing": { + "prescribed_destination": [ + 7, + 0, + 3 + ], + "reachable_token_placements": 413, + "routable": false + } + } + }, + { + "scalar_exhaustion": { + "W": 9, + "exhaustive_negative": true, + "exists": false, + "full_assignment_count": 78364164096, + "gates": 14, + "prefix_assignments": 279936, + "prefix_keys": 258156, + "prefix_sha256": "efc6209f40f81fbe06965bd6ec20901497e07ac7d3c3e01c3c8ac75a33e939c9", + "prescribed": { + "0": 7, + "1": 0, + "2": 3 + }, + "scope": "Existence with a free permutation of unprescribed roles; not an enumeration of every matching circuit.", + "split": 7, + "suffix_assignments": 279936, + "suffix_sha256": "55886af3abe760674a3d538ef43559a247469f162c10718676a8792bbfa9ec88", + "witness": null + }, + "topology": { + "W": 9, + "id": 3, + "independent_original_roles": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 8 + ], + "old_to_new_roles": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 8, + 4 + ], + "pairs": [ + [ + 0, + 3 + ], + [ + 1, + 4 + ], + [ + 2, + 5 + ], + [ + 0, + 1 + ], + [ + 4, + 2 + ], + [ + 0, + 6 + ], + [ + 4, + 7 + ], + [ + 0, + 4 + ], + [ + 5, + 6 + ], + [ + 0, + 8 + ], + [ + 5, + 4 + ], + [ + 0, + 5 + ], + [ + 7, + 4 + ], + [ + 3, + 8 + ] + ], + "prescribed": { + "0": 7, + "1": 0, + "2": 3 + }, + "reuse": [ + { + "from_role": 4, + "from_vertex": "u5", + "to_role": 9, + "to_vertex": "u8" + } + ], + "routing": { + "prescribed_destination": [ + 7, + 0, + 3 + ], + "reachable_token_placements": 319, + "routable": false + } + } + }, + { + "scalar_exhaustion": { + "W": 9, + "exhaustive_negative": true, + "exists": false, + "full_assignment_count": 78364164096, + "gates": 14, + "prefix_assignments": 279936, + "prefix_keys": 258156, + "prefix_sha256": "efc6209f40f81fbe06965bd6ec20901497e07ac7d3c3e01c3c8ac75a33e939c9", + "prescribed": { + "0": 7, + "1": 0, + "2": 3 + }, + "scope": "Existence with a free permutation of unprescribed roles; not an enumeration of every matching circuit.", + "split": 7, + "suffix_assignments": 279936, + "suffix_sha256": "8ab1597800673b81fef726004e7fb56e4261228f07bee6ce19cbcf6d16e53414", + "witness": null + }, + "topology": { + "W": 9, + "id": 4, + "independent_original_roles": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 8 + ], + "old_to_new_roles": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 8, + 6 + ], + "pairs": [ + [ + 0, + 3 + ], + [ + 1, + 4 + ], + [ + 2, + 5 + ], + [ + 0, + 1 + ], + [ + 4, + 2 + ], + [ + 0, + 6 + ], + [ + 4, + 7 + ], + [ + 0, + 4 + ], + [ + 5, + 6 + ], + [ + 0, + 8 + ], + [ + 5, + 6 + ], + [ + 0, + 5 + ], + [ + 7, + 6 + ], + [ + 3, + 8 + ] + ], + "prescribed": { + "0": 7, + "1": 0, + "2": 3 + }, + "reuse": [ + { + "from_role": 6, + "from_vertex": "u6", + "to_role": 9, + "to_vertex": "u8" + } + ], + "routing": { + "prescribed_destination": [ + 7, + 0, + 3 + ], + "reachable_token_placements": 313, + "routable": false + } + } + }, + { + "scalar_exhaustion": { + "W": 9, + "exhaustive_negative": true, + "exists": false, + "full_assignment_count": 78364164096, + "gates": 14, + "prefix_assignments": 279936, + "prefix_keys": 258156, + "prefix_sha256": "efc6209f40f81fbe06965bd6ec20901497e07ac7d3c3e01c3c8ac75a33e939c9", + "prescribed": { + "0": 7, + "1": 0, + "2": 3 + }, + "scope": "Existence with a free permutation of unprescribed roles; not an enumeration of every matching circuit.", + "split": 7, + "suffix_assignments": 279936, + "suffix_sha256": "f7f40358230ec476f2d199c3f0eb9a100006afdb131c0836ce895850b4a1bf7b", + "witness": null + }, + "topology": { + "W": 9, + "id": 13, + "independent_original_roles": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 9 + ], + "old_to_new_roles": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 4, + 8 + ], + "pairs": [ + [ + 0, + 3 + ], + [ + 1, + 4 + ], + [ + 2, + 5 + ], + [ + 0, + 1 + ], + [ + 4, + 2 + ], + [ + 0, + 6 + ], + [ + 4, + 7 + ], + [ + 0, + 4 + ], + [ + 5, + 6 + ], + [ + 0, + 4 + ], + [ + 5, + 8 + ], + [ + 0, + 5 + ], + [ + 7, + 8 + ], + [ + 3, + 4 + ] + ], + "prescribed": { + "0": 7, + "1": 0, + "2": 3 + }, + "reuse": [ + { + "from_role": 4, + "from_vertex": "u5", + "to_role": 8, + "to_vertex": "u7" + } + ], + "routing": { + "prescribed_destination": [ + 7, + 0, + 3 + ], + "reachable_token_placements": 303, + "routable": false + } + } + }, + { + "scalar_exhaustion": { + "W": 8, + "exhaustive_negative": true, + "exists": false, + "full_assignment_count": 78364164096, + "gates": 14, + "prefix_assignments": 279936, + "prefix_keys": 258156, + "prefix_sha256": "c0abd91329d32175dca935c243ad0f996e723da4076554dc37278ea897efb902", + "prescribed": { + "0": 7, + "1": 0, + "2": 3 + }, + "scope": "Existence with a free permutation of unprescribed roles; not an enumeration of every matching circuit.", + "split": 7, + "suffix_assignments": 279936, + "suffix_sha256": "eb023aa402f0722c242d41989828b5e027b2a272654a61832ef17a48f38c04cc", + "witness": null + }, + "topology": { + "W": 8, + "id": 16, + "independent_original_roles": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 7 + ], + "old_to_new_roles": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 4, + 6 + ], + "pairs": [ + [ + 0, + 3 + ], + [ + 1, + 4 + ], + [ + 2, + 5 + ], + [ + 0, + 1 + ], + [ + 4, + 2 + ], + [ + 0, + 6 + ], + [ + 4, + 7 + ], + [ + 0, + 4 + ], + [ + 5, + 6 + ], + [ + 0, + 4 + ], + [ + 5, + 6 + ], + [ + 0, + 5 + ], + [ + 7, + 6 + ], + [ + 3, + 4 + ] + ], + "prescribed": { + "0": 7, + "1": 0, + "2": 3 + }, + "reuse": [ + { + "from_role": 4, + "from_vertex": "u5", + "to_role": 8, + "to_vertex": "u7" + }, + { + "from_role": 6, + "from_vertex": "u6", + "to_role": 9, + "to_vertex": "u8" + } + ], + "routing": { + "prescribed_destination": [ + 7, + 0, + 3 + ], + "reachable_token_placements": 216, + "routable": false + } + } + }, + { + "scalar_exhaustion": { + "W": 9, + "exhaustive_negative": true, + "exists": false, + "full_assignment_count": 78364164096, + "gates": 14, + "prefix_assignments": 279936, + "prefix_keys": 44181, + "prefix_sha256": "d4030c203902fbc56a370dc8bd278611633e7081d38ed94613a7e52bcb352232", + "prescribed": { + "0": 2, + "1": 0, + "2": 3 + }, + "scope": "Existence with a free permutation of unprescribed roles; not an enumeration of every matching circuit.", + "split": 7, + "suffix_assignments": 279936, + "suffix_sha256": "22f4b7126d689e11fca1614ea3b2ee85019bdee86c0f37fcdbd6283d80b92b98", + "witness": null + }, + "topology": { + "W": 9, + "id": 34, + "independent_original_roles": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 8, + 9 + ], + "old_to_new_roles": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 2, + 7, + 8 + ], + "pairs": [ + [ + 0, + 3 + ], + [ + 1, + 4 + ], + [ + 2, + 5 + ], + [ + 0, + 1 + ], + [ + 4, + 2 + ], + [ + 0, + 6 + ], + [ + 4, + 2 + ], + [ + 0, + 4 + ], + [ + 5, + 6 + ], + [ + 0, + 7 + ], + [ + 5, + 8 + ], + [ + 0, + 5 + ], + [ + 2, + 8 + ], + [ + 3, + 7 + ] + ], + "prescribed": { + "0": 2, + "1": 0, + "2": 3 + }, + "reuse": [ + { + "from_role": 2, + "from_vertex": "u2", + "to_role": 7, + "to_vertex": "u4" + } + ], + "routing": { + "prescribed_destination": [ + 2, + 0, + 3 + ], + "reachable_token_placements": 336, + "routable": false + } + } + }, + { + "scalar_exhaustion": { + "W": 8, + "exhaustive_negative": true, + "exists": false, + "full_assignment_count": 78364164096, + "gates": 14, + "prefix_assignments": 279936, + "prefix_keys": 44181, + "prefix_sha256": "531b7872b128b783a283c729a8b50d242e2c2a382b2e456f1f3d00fdd00c1622", + "prescribed": { + "0": 2, + "1": 0, + "2": 3 + }, + "scope": "Existence with a free permutation of unprescribed roles; not an enumeration of every matching circuit.", + "split": 7, + "suffix_assignments": 279936, + "suffix_sha256": "9b1dd257806b8f2d8cfd9b12d6d34f3e86477f9a57b361a26c1ab534347f88c4", + "witness": null + }, + "topology": { + "W": 8, + "id": 36, + "independent_original_roles": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 8 + ], + "old_to_new_roles": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 2, + 7, + 4 + ], + "pairs": [ + [ + 0, + 3 + ], + [ + 1, + 4 + ], + [ + 2, + 5 + ], + [ + 0, + 1 + ], + [ + 4, + 2 + ], + [ + 0, + 6 + ], + [ + 4, + 2 + ], + [ + 0, + 4 + ], + [ + 5, + 6 + ], + [ + 0, + 7 + ], + [ + 5, + 4 + ], + [ + 0, + 5 + ], + [ + 2, + 4 + ], + [ + 3, + 7 + ] + ], + "prescribed": { + "0": 2, + "1": 0, + "2": 3 + }, + "reuse": [ + { + "from_role": 2, + "from_vertex": "u2", + "to_role": 7, + "to_vertex": "u4" + }, + { + "from_role": 4, + "from_vertex": "u5", + "to_role": 9, + "to_vertex": "u8" + } + ], + "routing": { + "prescribed_destination": [ + 2, + 0, + 3 + ], + "reachable_token_placements": 242, + "routable": false + } + } + }, + { + "scalar_exhaustion": { + "W": 8, + "exhaustive_negative": true, + "exists": false, + "full_assignment_count": 78364164096, + "gates": 14, + "prefix_assignments": 279936, + "prefix_keys": 44181, + "prefix_sha256": "531b7872b128b783a283c729a8b50d242e2c2a382b2e456f1f3d00fdd00c1622", + "prescribed": { + "0": 2, + "1": 0, + "2": 3 + }, + "scope": "Existence with a free permutation of unprescribed roles; not an enumeration of every matching circuit.", + "split": 7, + "suffix_assignments": 279936, + "suffix_sha256": "d1a4d6590ce080244d93ed469bebc3321784d635a3ec470efcc943673984f0d0", + "witness": null + }, + "topology": { + "W": 8, + "id": 37, + "independent_original_roles": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 8 + ], + "old_to_new_roles": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 2, + 7, + 6 + ], + "pairs": [ + [ + 0, + 3 + ], + [ + 1, + 4 + ], + [ + 2, + 5 + ], + [ + 0, + 1 + ], + [ + 4, + 2 + ], + [ + 0, + 6 + ], + [ + 4, + 2 + ], + [ + 0, + 4 + ], + [ + 5, + 6 + ], + [ + 0, + 7 + ], + [ + 5, + 6 + ], + [ + 0, + 5 + ], + [ + 2, + 6 + ], + [ + 3, + 7 + ] + ], + "prescribed": { + "0": 2, + "1": 0, + "2": 3 + }, + "reuse": [ + { + "from_role": 2, + "from_vertex": "u2", + "to_role": 7, + "to_vertex": "u4" + }, + { + "from_role": 6, + "from_vertex": "u6", + "to_role": 9, + "to_vertex": "u8" + } + ], + "routing": { + "prescribed_destination": [ + 2, + 0, + 3 + ], + "reachable_token_placements": 240, + "routable": false + } + } + }, + { + "scalar_exhaustion": { + "W": 8, + "exhaustive_negative": true, + "exists": false, + "full_assignment_count": 78364164096, + "gates": 14, + "prefix_assignments": 279936, + "prefix_keys": 44181, + "prefix_sha256": "531b7872b128b783a283c729a8b50d242e2c2a382b2e456f1f3d00fdd00c1622", + "prescribed": { + "0": 2, + "1": 0, + "2": 3 + }, + "scope": "Existence with a free permutation of unprescribed roles; not an enumeration of every matching circuit.", + "split": 7, + "suffix_assignments": 279936, + "suffix_sha256": "6ae7f0465a498692a8577d442031b761a2ba9eb670b2637eb08a15b528f50faa", + "witness": null + }, + "topology": { + "W": 8, + "id": 41, + "independent_original_roles": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 9 + ], + "old_to_new_roles": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 2, + 4, + 7 + ], + "pairs": [ + [ + 0, + 3 + ], + [ + 1, + 4 + ], + [ + 2, + 5 + ], + [ + 0, + 1 + ], + [ + 4, + 2 + ], + [ + 0, + 6 + ], + [ + 4, + 2 + ], + [ + 0, + 4 + ], + [ + 5, + 6 + ], + [ + 0, + 4 + ], + [ + 5, + 7 + ], + [ + 0, + 5 + ], + [ + 2, + 7 + ], + [ + 3, + 4 + ] + ], + "prescribed": { + "0": 2, + "1": 0, + "2": 3 + }, + "reuse": [ + { + "from_role": 2, + "from_vertex": "u2", + "to_role": 7, + "to_vertex": "u4" + }, + { + "from_role": 4, + "from_vertex": "u5", + "to_role": 8, + "to_vertex": "u7" + } + ], + "routing": { + "prescribed_destination": [ + 2, + 0, + 3 + ], + "reachable_token_placements": 234, + "routable": false + } + } + }, + { + "scalar_exhaustion": { + "W": 7, + "exhaustive_negative": true, + "exists": false, + "full_assignment_count": 78364164096, + "gates": 14, + "prefix_assignments": 279936, + "prefix_keys": 44181, + "prefix_sha256": "bdf51bb6d89a9be2ef6735a8204f5e84eb11c986c4af6b94af0d212449bfcff2", + "prescribed": { + "0": 2, + "1": 0, + "2": 3 + }, + "scope": "Existence with a free permutation of unprescribed roles; not an enumeration of every matching circuit.", + "split": 7, + "suffix_assignments": 279936, + "suffix_sha256": "ee0efcd60581fed7fe9497278b1dab0d99a3c397554632be89c0846d1b99d575", + "witness": null + }, + "topology": { + "W": 7, + "id": 43, + "independent_original_roles": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6 + ], + "old_to_new_roles": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 2, + 4, + 6 + ], + "pairs": [ + [ + 0, + 3 + ], + [ + 1, + 4 + ], + [ + 2, + 5 + ], + [ + 0, + 1 + ], + [ + 4, + 2 + ], + [ + 0, + 6 + ], + [ + 4, + 2 + ], + [ + 0, + 4 + ], + [ + 5, + 6 + ], + [ + 0, + 4 + ], + [ + 5, + 6 + ], + [ + 0, + 5 + ], + [ + 2, + 6 + ], + [ + 3, + 4 + ] + ], + "prescribed": { + "0": 2, + "1": 0, + "2": 3 + }, + "reuse": [ + { + "from_role": 2, + "from_vertex": "u2", + "to_role": 7, + "to_vertex": "u4" + }, + { + "from_role": 4, + "from_vertex": "u5", + "to_role": 8, + "to_vertex": "u7" + }, + { + "from_role": 6, + "from_vertex": "u6", + "to_role": 9, + "to_vertex": "u8" + } + ], + "routing": { + "prescribed_destination": [ + 2, + 0, + 3 + ], + "reachable_token_placements": 158, + "routable": false + } + } + }, + { + "scalar_exhaustion": { + "W": 9, + "exhaustive_negative": true, + "exists": false, + "full_assignment_count": 78364164096, + "gates": 14, + "prefix_assignments": 279936, + "prefix_keys": 44181, + "prefix_sha256": "f1f86b3b3682911d1644451e40c162d286eb8b265133087cca5c2d9b78adbcb8", + "prescribed": { + "0": 6, + "1": 0, + "2": 3 + }, + "scope": "Existence with a free permutation of unprescribed roles; not an enumeration of every matching circuit.", + "split": 7, + "suffix_assignments": 279936, + "suffix_sha256": "eda055fb37dcfd685f5b43f6698f2b2c1d2f193b1f9ca8f09d96444daff97a74", + "witness": null + }, + "topology": { + "W": 9, + "id": 47, + "independent_original_roles": [ + 0, + 1, + 2, + 3, + 4, + 5, + 7, + 8, + 9 + ], + "old_to_new_roles": [ + 0, + 1, + 2, + 3, + 4, + 5, + 1, + 6, + 7, + 8 + ], + "pairs": [ + [ + 0, + 3 + ], + [ + 1, + 4 + ], + [ + 2, + 5 + ], + [ + 0, + 1 + ], + [ + 4, + 2 + ], + [ + 0, + 1 + ], + [ + 4, + 6 + ], + [ + 0, + 4 + ], + [ + 5, + 1 + ], + [ + 0, + 7 + ], + [ + 5, + 8 + ], + [ + 0, + 5 + ], + [ + 6, + 8 + ], + [ + 3, + 7 + ] + ], + "prescribed": { + "0": 6, + "1": 0, + "2": 3 + }, + "reuse": [ + { + "from_role": 1, + "from_vertex": "u1", + "to_role": 6, + "to_vertex": "u3" + } + ], + "routing": { + "prescribed_destination": [ + 6, + 0, + 3 + ], + "reachable_token_placements": 362, + "routable": false + } + } + }, + { + "scalar_exhaustion": { + "W": 8, + "exhaustive_negative": true, + "exists": false, + "full_assignment_count": 78364164096, + "gates": 14, + "prefix_assignments": 279936, + "prefix_keys": 44181, + "prefix_sha256": "b27cfb99491a9f1090d01efed26f15b5af9f5cd0d505fa2eba9e7d228de40fcf", + "prescribed": { + "0": 6, + "1": 0, + "2": 3 + }, + "scope": "Existence with a free permutation of unprescribed roles; not an enumeration of every matching circuit.", + "split": 7, + "suffix_assignments": 279936, + "suffix_sha256": "d1c1ea4b57f47d4dbbf57168ab560dd1e8fa29ba16d7b0ad4ac7b4d0abaea77d", + "witness": null + }, + "topology": { + "W": 8, + "id": 50, + "independent_original_roles": [ + 0, + 1, + 2, + 3, + 4, + 5, + 7, + 8 + ], + "old_to_new_roles": [ + 0, + 1, + 2, + 3, + 4, + 5, + 1, + 6, + 7, + 1 + ], + "pairs": [ + [ + 0, + 3 + ], + [ + 1, + 4 + ], + [ + 2, + 5 + ], + [ + 0, + 1 + ], + [ + 4, + 2 + ], + [ + 0, + 1 + ], + [ + 4, + 6 + ], + [ + 0, + 4 + ], + [ + 5, + 1 + ], + [ + 0, + 7 + ], + [ + 5, + 1 + ], + [ + 0, + 5 + ], + [ + 6, + 1 + ], + [ + 3, + 7 + ] + ], + "prescribed": { + "0": 6, + "1": 0, + "2": 3 + }, + "reuse": [ + { + "from_role": 1, + "from_vertex": "u1", + "to_role": 6, + "to_vertex": "u3" + }, + { + "from_role": 6, + "from_vertex": "u6", + "to_role": 9, + "to_vertex": "u8" + } + ], + "routing": { + "prescribed_destination": [ + 6, + 0, + 3 + ], + "reachable_token_placements": 254, + "routable": false + } + } + }, + { + "scalar_exhaustion": { + "W": 8, + "exhaustive_negative": true, + "exists": false, + "full_assignment_count": 78364164096, + "gates": 14, + "prefix_assignments": 279936, + "prefix_keys": 7560, + "prefix_sha256": "b6eeb5263b08f093f8022d161ab0062bbb71dd7c61baff81496cbb8c9a7c4b1c", + "prescribed": { + "0": 2, + "1": 0, + "2": 3 + }, + "scope": "Existence with a free permutation of unprescribed roles; not an enumeration of every matching circuit.", + "split": 7, + "suffix_assignments": 279936, + "suffix_sha256": "0a6dc4127dbd3baafed8411d99bb0228f1e646d5676f3b7ab967d647c0658d89", + "witness": null + }, + "topology": { + "W": 8, + "id": 60, + "independent_original_roles": [ + 0, + 1, + 2, + 3, + 4, + 5, + 8, + 9 + ], + "old_to_new_roles": [ + 0, + 1, + 2, + 3, + 4, + 5, + 1, + 2, + 6, + 7 + ], + "pairs": [ + [ + 0, + 3 + ], + [ + 1, + 4 + ], + [ + 2, + 5 + ], + [ + 0, + 1 + ], + [ + 4, + 2 + ], + [ + 0, + 1 + ], + [ + 4, + 2 + ], + [ + 0, + 4 + ], + [ + 5, + 1 + ], + [ + 0, + 6 + ], + [ + 5, + 7 + ], + [ + 0, + 5 + ], + [ + 2, + 7 + ], + [ + 3, + 6 + ] + ], + "prescribed": { + "0": 2, + "1": 0, + "2": 3 + }, + "reuse": [ + { + "from_role": 1, + "from_vertex": "u1", + "to_role": 6, + "to_vertex": "u3" + }, + { + "from_role": 2, + "from_vertex": "u2", + "to_role": 7, + "to_vertex": "u4" + } + ], + "routing": { + "prescribed_destination": [ + 2, + 0, + 3 + ], + "reachable_token_placements": 276, + "routable": false + } + } + }, + { + "scalar_exhaustion": { + "W": 7, + "exhaustive_negative": true, + "exists": false, + "full_assignment_count": 78364164096, + "gates": 14, + "prefix_assignments": 279936, + "prefix_keys": 7560, + "prefix_sha256": "45a9842f5becb39c9b4485389003ec502eba980337aafdb8460af1cd4b8c7391", + "prescribed": { + "0": 2, + "1": 0, + "2": 3 + }, + "scope": "Existence with a free permutation of unprescribed roles; not an enumeration of every matching circuit.", + "split": 7, + "suffix_assignments": 279936, + "suffix_sha256": "902181daa3f0d66b663bbb340ed4ce8b20ec59837ab51ce98549ca5906cbf404", + "witness": null + }, + "topology": { + "W": 7, + "id": 62, + "independent_original_roles": [ + 0, + 1, + 2, + 3, + 4, + 5, + 8 + ], + "old_to_new_roles": [ + 0, + 1, + 2, + 3, + 4, + 5, + 1, + 2, + 6, + 1 + ], + "pairs": [ + [ + 0, + 3 + ], + [ + 1, + 4 + ], + [ + 2, + 5 + ], + [ + 0, + 1 + ], + [ + 4, + 2 + ], + [ + 0, + 1 + ], + [ + 4, + 2 + ], + [ + 0, + 4 + ], + [ + 5, + 1 + ], + [ + 0, + 6 + ], + [ + 5, + 1 + ], + [ + 0, + 5 + ], + [ + 2, + 1 + ], + [ + 3, + 6 + ] + ], + "prescribed": { + "0": 2, + "1": 0, + "2": 3 + }, + "reuse": [ + { + "from_role": 1, + "from_vertex": "u1", + "to_role": 6, + "to_vertex": "u3" + }, + { + "from_role": 2, + "from_vertex": "u2", + "to_role": 7, + "to_vertex": "u4" + }, + { + "from_role": 6, + "from_vertex": "u6", + "to_role": 9, + "to_vertex": "u8" + } + ], + "routing": { + "prescribed_destination": [ + 2, + 0, + 3 + ], + "reachable_token_placements": 184, + "routable": false + } + } + }, + { + "scalar_exhaustion": { + "W": 9, + "exhaustive_negative": true, + "exists": false, + "full_assignment_count": 78364164096, + "gates": 14, + "prefix_assignments": 279936, + "prefix_keys": 231939, + "prefix_sha256": "7458afe3e4843fb4b5fb4ade9b2eeef9f7141e1193db11b908fc526dcbd7b098", + "prescribed": { + "0": 6, + "1": 0, + "2": 3 + }, + "scope": "Existence with a free permutation of unprescribed roles; not an enumeration of every matching circuit.", + "split": 7, + "suffix_assignments": 279936, + "suffix_sha256": "1b2dc695600aede6e6c31cc71f48b9cab3b5240048523826f54e4a98dbf65051", + "witness": null + }, + "topology": { + "W": 9, + "id": 67, + "independent_original_roles": [ + 0, + 1, + 2, + 3, + 4, + 5, + 7, + 8, + 9 + ], + "old_to_new_roles": [ + 0, + 1, + 2, + 3, + 4, + 5, + 2, + 6, + 7, + 8 + ], + "pairs": [ + [ + 0, + 3 + ], + [ + 1, + 4 + ], + [ + 2, + 5 + ], + [ + 0, + 1 + ], + [ + 4, + 2 + ], + [ + 0, + 2 + ], + [ + 4, + 6 + ], + [ + 0, + 4 + ], + [ + 5, + 2 + ], + [ + 0, + 7 + ], + [ + 5, + 8 + ], + [ + 0, + 5 + ], + [ + 6, + 8 + ], + [ + 3, + 7 + ] + ], + "prescribed": { + "0": 6, + "1": 0, + "2": 3 + }, + "reuse": [ + { + "from_role": 2, + "from_vertex": "u2", + "to_role": 6, + "to_vertex": "u3" + } + ], + "routing": { + "prescribed_destination": [ + 6, + 0, + 3 + ], + "reachable_token_placements": 386, + "routable": false + } + } + }, + { + "scalar_exhaustion": { + "W": 8, + "exhaustive_negative": true, + "exists": false, + "full_assignment_count": 78364164096, + "gates": 14, + "prefix_assignments": 279936, + "prefix_keys": 231939, + "prefix_sha256": "8551d47c14617a0c1b544f9a48d8c778f491ef0cfd3982b3c55bcd30f9f866d2", + "prescribed": { + "0": 6, + "1": 0, + "2": 3 + }, + "scope": "Existence with a free permutation of unprescribed roles; not an enumeration of every matching circuit.", + "split": 7, + "suffix_assignments": 279936, + "suffix_sha256": "89dd511fb3101845a6774c19ba777383117d8fdc72cc5cfebbde6bc2ff5f1ee4", + "witness": null + }, + "topology": { + "W": 8, + "id": 70, + "independent_original_roles": [ + 0, + 1, + 2, + 3, + 4, + 5, + 7, + 8 + ], + "old_to_new_roles": [ + 0, + 1, + 2, + 3, + 4, + 5, + 2, + 6, + 7, + 2 + ], + "pairs": [ + [ + 0, + 3 + ], + [ + 1, + 4 + ], + [ + 2, + 5 + ], + [ + 0, + 1 + ], + [ + 4, + 2 + ], + [ + 0, + 2 + ], + [ + 4, + 6 + ], + [ + 0, + 4 + ], + [ + 5, + 2 + ], + [ + 0, + 7 + ], + [ + 5, + 2 + ], + [ + 0, + 5 + ], + [ + 6, + 2 + ], + [ + 3, + 7 + ] + ], + "prescribed": { + "0": 6, + "1": 0, + "2": 3 + }, + "reuse": [ + { + "from_role": 2, + "from_vertex": "u2", + "to_role": 6, + "to_vertex": "u3" + }, + { + "from_role": 6, + "from_vertex": "u6", + "to_role": 9, + "to_vertex": "u8" + } + ], + "routing": { + "prescribed_destination": [ + 6, + 0, + 3 + ], + "reachable_token_placements": 266, + "routable": false + } + } + } + ], + "obstruction_preserving_topologies": 16, + "other_topologies": 71, + "scope": "Chronological pairings of distinct auxiliary output/input stubs of the balanced Fano DAG, retaining the original three-demand obstruction; GL(2,F2) at each of 14 vertices; all other inputs independent with a free output permutation. Other topologies, larger local blocks and different coding graphs are not excluded.", + "status": "NO SCALAR COMPLETION IN THE SPECIFIED OBSTRUCTION-PRESERVING REUSE FAMILY", + "topologies_enumerated": 87, + "width_counts": { + "7": 2, + "8": 7, + "9": 6, + "10": 1 + } +} diff --git a/research/percent-exponent-architecture/fano_reuse_verify.py b/research/percent-exponent-architecture/fano_reuse_verify.py new file mode 100644 index 0000000000..8e0208ca88 --- /dev/null +++ b/research/percent-exponent-architecture/fano_reuse_verify.py @@ -0,0 +1,59 @@ +#!/usr/bin/env python3 +"""Replay the whole finite stub-reuse screen without a solver or C++. + +The complete negative statements below apply only to reuse topologies that +preserve the original three-demand routing obstruction. The other topologies +are recorded as outside this particular selection, not proved impossible. +""" +from __future__ import annotations + +import argparse +from collections import Counter +import json +from pathlib import Path +import sys + +HERE = Path(__file__).resolve().parent +sys.path.insert(0, str(HERE / "discovery")) +from fano_reuse import topologies +from balanced_fano import existence + + +def verify(): + if sys.flags.optimize: + raise ValueError("Run without -O") + cases = list(topologies()) + accepted = [c for c in cases if not c["routing"]["routable"]] + if len(cases) != 87 or len(accepted) != 16: + raise ValueError("The exhaustively specified topology family changed") + certificates = [] + for i, c in enumerate(accepted): + result = existence(c["W"], c["pairs"], c["prescribed"]) + if result["exists"] or not result["exhaustive_negative"]: + raise ValueError("A scalar completion needs further investigation") + if result["prefix_assignments"] != 6**7 or result["suffix_assignments"] != 6**7: + raise ValueError("The complete halves were not enumerated") + certificates.append({"topology": c, "scalar_exhaustion": result}) + print(f"PASS {i+1}/{len(accepted)}: case {c['id']}, W={c['W']}, all 6^14 assignments excluded", flush=True) + return {"status": "NO SCALAR COMPLETION IN THE SPECIFIED OBSTRUCTION-PRESERVING REUSE FAMILY", + "topologies_enumerated": len(cases), "obstruction_preserving_topologies": len(accepted), + "other_topologies": len(cases) - len(accepted), + "width_counts": dict(sorted(Counter(c["W"] for c in accepted).items())), + "cases": certificates, + "scope": "Chronological pairings of distinct auxiliary output/input stubs of the balanced Fano DAG, retaining the original three-demand obstruction; GL(2,F2) at each of 14 vertices; all other inputs independent with a free output permutation. Other topologies, larger local blocks and different coding graphs are not excluded."} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--write", action="store_true") + args = parser.parse_args() + output = json.dumps(verify(), sort_keys=True, indent=2) + "\n" + path = HERE / "fano-reuse-certificate.json" + if args.write: + path.write_text(output) + elif path.read_text() != output: + raise ValueError("Exact Fano reuse certificate changed") + + +if __name__ == "__main__": + main() diff --git a/research/percent-exponent-architecture/inputs/bit-pr187.json b/research/percent-exponent-architecture/inputs/bit-pr187.json new file mode 100644 index 0000000000..1a00656788 --- /dev/null +++ b/research/percent-exponent-architecture/inputs/bit-pr187.json @@ -0,0 +1,53 @@ +{ + "profile": { + "W": 21108, + "child_histogram": { + "1": 120168, + "10": 2508, + "11": 1158, + "12": 4320, + "13": 1590, + "14": 3234, + "15": 1230, + "16": 3216, + "17": 1164, + "18": 1332, + "19": 918, + "2": 64228, + "20": 5280, + "21": 11160, + "22": 11952, + "3": 29616, + "4": 8970, + "5": 7800, + "6": 3660, + "60": 2200, + "7": 3312, + "8": 2802, + "9": 1812 + }, + "deficit": 1936, + "h": 24, + "loss": 528, + "m": 72, + "rank": 1517840, + "source_data_histogram": { + "1": 1760, + "2": 880, + "20": 880, + "22": 880 + }, + "target_data_histogram": { + "1": 4400, + "20": 880, + "21": 880 + }, + "v": 1760 + }, + "provenance": { + "commit": "201737a1ec4f936e166e2481fb9e88104cb2ccc7", + "path": "research/source-assisted-bit-bootstrap/emitted-physical.json", + "pr": 187, + "source_file_sha256": "5f1f1d978937b816a14b07fee5ac8fc31f3a9aaf05046a477e8be57bb6d07ce6" + } +} diff --git a/research/percent-exponent-architecture/inputs/complex-pr193.json b/research/percent-exponent-architecture/inputs/complex-pr193.json new file mode 100644 index 0000000000..550d0ca928 --- /dev/null +++ b/research/percent-exponent-architecture/inputs/complex-pr193.json @@ -0,0 +1,49 @@ +{ + "profile": { + "W": 12052, + "child_histogram": { + "1": 87534, + "10": 2790, + "11": 1062, + "12": 3591, + "13": 381, + "14": 2226, + "15": 5637, + "16": 264, + "17": 243, + "18": 7959, + "19": 501, + "2": 39834, + "20": 66, + "3": 29769, + "4": 12627, + "5": 5850, + "6": 4815, + "7": 2118, + "8": 4593, + "9": 1287 + }, + "deficit": 1320, + "h": 22, + "loss": 440, + "m": 66, + "rank": 794112, + "source_data_histogram": { + "1": 1320, + "18": 1320, + "2": 1320 + }, + "target_data_histogram": { + "0": 6270, + "1": 3960, + "18": 1320 + }, + "v": 1320 + }, + "provenance": { + "commit": "187e1010ac8b259af8e9b5166f68b64bc27b4b47", + "path": "research/source-assisted-v4/certificate.json", + "pr": 193, + "source_file_sha256": "d84406d2fcc6990deba2b135509e6d86600e57123d88f9b21f7b7240e1aeb513" + } +} diff --git a/research/percent-exponent-architecture/references/SOURCE.json b/research/percent-exponent-architecture/references/SOURCE.json new file mode 100644 index 0000000000..f0df4a2be3 --- /dev/null +++ b/research/percent-exponent-architecture/references/SOURCE.json @@ -0,0 +1,8 @@ +{ + "changes": "Added source/attribution header; replaced two imports by the identical require predicate and FANO_EDGES tuple. Algorithm bodies are unchanged.", + "commit": "187e1010ac8b259af8e9b5166f68b64bc27b4b47", + "files": { + "scripts/experiments/balanced_fano.py": "1586fb1db4f40e79e97bae59f47192675663403bbcacbf5f4e0b702edfd22b0a", + "scripts/experiments/fano_completion.py": "6cade2a36b910bf7e68a872dc4fd3560837935cffe80f9526cd012a28b247738" + } +} diff --git a/research/percent-exponent-architecture/references/balanced_fano.py b/research/percent-exponent-architecture/references/balanced_fano.py new file mode 100644 index 0000000000..d7369878e2 --- /dev/null +++ b/research/percent-exponent-architecture/references/balanced_fano.py @@ -0,0 +1,130 @@ +# Derived from CrocSwap/integer-mult-bounds scripts/experiments/balanced_fano.py. +# Apache-2.0; original repository attribution retained in ../NOTICE. +# Only dependency bindings are adapted: require and the original edge tuple are local. +"""Balance the Fano DAG, then exhaust the local reversible binary model. + +The meet-in-the-middle algorithm tests existence with a free permutation of +unprescribed roles. Keeping one prefix per key is sufficient for existence, +but not for enumerating all possible complete words or output permutations. +""" +from hashlib import sha256 + +def require(condition, message): + if not condition: + raise ValueError(message) + + +FANO_EDGES = (('a', 'u1'), ('a', 'tc'), ('b', 'u1'), ('b', 'u2'), ('c', 'u2'), ('c', 'u6'), ('u1', 'u3'), ('u2', 'u4'), ('u3', 'u5'), ('u3', 'u6'), ('u4', 'u5'), ('u4', 'ta'), ('u5', 'u7'), ('u6', 'u8'), ('u7', 'u9'), ('u7', 'tc'), ('u8', 'u9'), ('u8', 'ta'), ('u9', 'u10'), ('u10', 'tb')) + + +GL2 = ((1, 2), (2, 1), (1, 3), (3, 2), (2, 3), (3, 1)) + + +def balanced_fano(): + order = ('a', 'b', 'c', 'u1', 'u2', 'u3', 'u4', 'u5', 'u6', 'u7', 'u8', 'u9', 'u10', 'ta', 'tb', 'tc') + source = {'a': 0, 'b': 1, 'c': 2} + edge_roles = {}; next_role = 3; pairs = []; gates_at = [] + auxiliary_inputs = []; auxiliary_outputs = []; targets = {} + for vertex in order: + incoming = [i for i, (u, v) in enumerate(FANO_EDGES) if v == vertex] + outgoing = [i for i, (u, v) in enumerate(FANO_EDGES) if u == vertex] + roles = [edge_roles[i] for i in incoming] + if vertex in source: roles.append(source[vertex]) + output_count = len(outgoing)+int(vertex in ('ta', 'tb', 'tc')) + width = max(len(roles), output_count) + require(width in (1, 2), 'Unexpected local width') + while len(roles) < width: + auxiliary_inputs.append((vertex, next_role)) + roles.append(next_role); next_role += 1 + if width == 2: + pairs.append(tuple(roles)); gates_at.append(vertex) + for edge, role in zip(outgoing, roles): edge_roles[edge] = role + occupied = len(outgoing) + if vertex in ('ta', 'tb', 'tc'): + targets[vertex] = roles[occupied]; occupied += 1 + auxiliary_outputs.extend((vertex, r) for r in roles[occupied:]) + require(next_role == 10 and len(pairs) == 14, 'Wrong balanced model size') + outputs = list(targets.values())+[r for v, r in auxiliary_outputs] + require(sorted(outputs) == list(range(next_role)), 'Output roles are not a partition') + return dict(W=next_role, pairs=pairs, gate_vertices=gates_at, + prescribed={0: targets['ta'], 1: targets['tb'], 2: targets['tc']}, + auxiliary_inputs=auxiliary_inputs, auxiliary_outputs=auxiliary_outputs, + edge_roles=[edge_roles[i] for i in range(len(FANO_EDGES))]) + + +def execute(W, pairs, choices): + require(len(pairs) == len(choices), 'One choice per gate required') + rows = [1 << i for i in range(W)] + for (a, b), k in zip(pairs, choices): + values = (0, rows[a], rows[b], rows[a]^rows[b]) + x, y = GL2[k] + rows[a], rows[b] = values[x], values[y] + return tuple(rows) + + +def columns(rows): + W = len(rows) + return tuple(sum(((row >> j) & 1) << i for i, row in enumerate(rows)) for j in range(W)) + + +def assignments(W, pairs): + pairs = tuple(pairs) + def descend(depth, rows, word): + if depth == len(pairs): + yield rows, word + return + a, b = pairs[depth]; x, y = rows[a], rows[b] + values = (0, x, y, x^y) + for k, (s, t) in enumerate(GL2): + new = list(rows); new[a] = values[s]; new[b] = values[t] + yield from descend(depth+1, tuple(new), word+(k,)) + yield from descend(0, tuple(1 << i for i in range(W)), ()) + + +def inverse_choice(k): + for j in range(6): + if execute(2, [(0, 1), (0, 1)], [k, j]) == (1, 2): return j + raise ValueError('GL2 inverse missing') + + +def existence(W, pairs, prescribed=None, half_budget=300000): + """Exact complete search, not a heuristic or solver-unsat certificate.""" + prescribed = dict(prescribed or {}) + require(W >= 2 and all(0 <= i < W and 0 <= j < W for i, j in prescribed.items()), 'Invalid fixed terminals') + require(len(set(prescribed.values())) == len(prescribed), 'Fixed terminal outputs repeat') + require(all(len(p) == 2 and p[0] != p[1] and all(0 <= i < W for i in p) for p in pairs), 'Invalid ports') + split = len(pairs)//2 + require(max(6**split, 6**(len(pairs)-split)) <= half_budget, 'Half-enumeration budget exceeded') + source_fixed = tuple(sorted(prescribed)) + output_fixed = tuple(prescribed[i] for i in source_fixed) + def key(cols, fixed): + return tuple(cols[i] for i in fixed)+tuple(sorted(cols[i] for i in range(W) if i not in fixed)) + width = (W+7)//8 + def packed(key): return b''.join(v.to_bytes(width, 'big') for v in key) + seen = {}; prefix_hash = sha256(); suffix_hash = sha256(); prefix_count = suffix_count = 0 + for rows, word in assignments(W, pairs[:split]): + k = key(columns(rows), source_fixed) + seen.setdefault(k, (rows, word)) + prefix_hash.update(packed(k)); prefix_count += 1 + found = None + for rows, word in assignments(W, list(reversed(pairs[split:]))): + # These are inverse-suffix words. Inversion is a bijection on GL2, + # so this enumeration covers every possible suffix exactly once. + cols = columns(rows); k = key(cols, output_fixed) + suffix_hash.update(packed(k)); suffix_count += 1 + if k not in seen: continue + A, prefix_word = seen[k] + rho = tuple(cols.index(c) for c in columns(A)) + suffix_word = tuple(inverse_choice(j) for j in reversed(word)) + full_word = prefix_word+suffix_word + transfer = execute(W, pairs, full_word) + require(all(transfer[rho[i]] == 1 << i for i in range(W)), 'Recovered scalar permutation is wrong') + require(all(rho[i] == j for i, j in prescribed.items()), 'Recovered terminals are wrong') + found = dict(choices=full_word, rho=rho) + break + return dict(W=W, gates=len(pairs), split=split, prescribed=prescribed, + prefix_assignments=prefix_count, prefix_keys=len(seen), suffix_assignments=suffix_count, + prefix_sha256=prefix_hash.hexdigest(), suffix_sha256=suffix_hash.hexdigest(), + full_assignment_count=6**len(pairs), exists=found is not None, + exhaustive_negative=found is None, witness=found, + scope='Existence with a free permutation of unprescribed roles; not an enumeration of every matching circuit.') diff --git a/research/percent-exponent-architecture/test_audit.py b/research/percent-exponent-architecture/test_audit.py new file mode 100644 index 0000000000..49a8f9839b --- /dev/null +++ b/research/percent-exponent-architecture/test_audit.py @@ -0,0 +1,76 @@ +#!/usr/bin/env python3 +"""Adverse controls for exact arithmetic, independent inputs and frame screens.""" +from fractions import Fraction as Q +import json +from pathlib import Path +import tempfile +import unittest +from unittest.mock import patch + +import audit +from triangular_obstruction import inverse, matrix, multiply, rejection + + +class ExactAuditTests(unittest.TestCase): + def test_log_enclosures_against_longer_series(self): + for x in (Q(1), Q(6, 5), Q(2), Q(3), Q(66), Q(72, 22)): + lo, hi = audit.log_interval(x) + y, power = x, 0 + while y >= 2: + y /= 2 + power += 1 + l, u = audit.atanh_log(y, terms=65) + l2, u2 = audit.atanh_log(Q(2), terms=65) + self.assertLessEqual(lo, l + power * l2) + self.assertGreaterEqual(hi, u + power * u2) + self.assertLessEqual(hi - lo, Q(2, audit.GRID)) + + def test_checkpoint_corruption_rejected(self): + original = json.loads((audit.HERE / "inputs/complex-pr193.json").read_text()) + for field in ("rank", "loss"): + changed = json.loads(json.dumps(original)) + changed["profile"][field] -= 1 + with tempfile.TemporaryDirectory() as directory: + root = Path(directory) + (root / "inputs").mkdir() + (root / "inputs/complex-pr193.json").write_text(json.dumps(changed)) + with patch.object(audit, "HERE", root), self.assertRaises(ValueError): + audit.checkpoint("complex-pr193") + + def test_cube_kernel_beyond_frozen_controls(self): + result = audit.local_identity(9) + self.assertEqual(result["B_rank"], 256) + self.assertEqual(result["opposite_parity_source_rank"], 9) + + def test_infinite_tail_excludes_target(self): + result = audit.family_screen() + self.assertLess(Q(result["strict_arbitrary_local_chains_a_ceiling"]), Q(1, 100)) + self.assertEqual(result["best_arbitrary_local_chains_case"]["p"], 13) + self.assertEqual(result["best_arbitrary_local_chains_case"]["degree"], 5) + + def test_common_flag_need_not_commute(self): + upper = [matrix([[1, 1], [0, 0]]), matrix([[0, 2], [0, 1]])] + basis = matrix([[1, 1], [1, 2]]) + inv = inverse(basis) + frames = [multiply(multiply(basis, a), inv) for a in upper] + self.assertFalse(rejection(frames)["rejected"]) + self.assertTrue(rejection(frames, basis)["rejected"]) + with self.assertRaises(ValueError): + rejection(frames, [[1, 0], [0, 1]]) + + def test_commuting_without_rational_eigenbasis(self): + rotation = [[0, -1], [1, 0]] + translated = [[1, -1], [1, 1]] + self.assertTrue(rejection([rotation, translated])["rejected"]) + with self.assertRaises(ValueError): + rejection([rotation], [[1, 0], [0, 1]]) + + def test_nontriangular_family_is_only_inconclusive(self): + frames = [[[1, 0], [0, 0]], [[Q(1, 2), Q(1, 2)], [Q(1, 2), Q(1, 2)]]] + self.assertFalse(rejection(frames)["rejected"]) + with self.assertRaises(ValueError): + rejection(frames, [[1, 0], [0, 1]]) + + +if __name__ == "__main__": + unittest.main() diff --git a/research/percent-exponent-architecture/triangular_obstruction.py b/research/percent-exponent-architecture/triangular_obstruction.py new file mode 100644 index 0000000000..a4eb402499 --- /dev/null +++ b/research/percent-exponent-architecture/triangular_obstruction.py @@ -0,0 +1,66 @@ +#!/usr/bin/env python3 +"""Exact sufficient rejection checks for a common triangular frame flag. + +The written theorem applies over any characteristic-zero splitting field. +The explicit-basis check uses rational arithmetic; commuting rational frames +are covered even when their common triangularizing basis is not rational. +""" +from __future__ import annotations + +from fractions import Fraction as Q +from itertools import combinations + + +def matrix(a): + n = len(a) + if not n or any(len(row) != n for row in a): + raise ValueError("Square nonempty matrices required") + if any(isinstance(v, float) for row in a for v in row): + raise ValueError("Use exact entries") + return tuple(tuple(Q(v) for v in row) for row in a) + + +def multiply(a, b): + if len(a) != len(b): + raise ValueError("Dimensions differ") + n = len(a) + return tuple(tuple(sum((a[i][k] * b[k][j] for k in range(n)), Q(0)) + for j in range(n)) for i in range(n)) + + +def inverse(a): + n = len(a) + rows = [list(a[i]) + [Q(i == j) for j in range(n)] for i in range(n)] + for j in range(n): + pivot = next((i for i in range(j, n) if rows[i][j]), None) + if pivot is None: + raise ValueError("Singular common basis") + rows[j], rows[pivot] = rows[pivot], rows[j] + scale = rows[j][j] + rows[j] = [v / scale for v in rows[j]] + for i in range(n): + if i != j and rows[i][j]: + scale = rows[i][j] + rows[i] = [x - scale * y for x, y in zip(rows[i], rows[j])] + return tuple(tuple(row[n:]) for row in rows) + + +def rejection(frames, basis=None): + frames = tuple(dict.fromkeys(matrix(a) for a in frames)) + if not frames or any(len(a) != len(frames[0]) for a in frames): + raise ValueError("Nonempty common-dimensional frame family required") + n = len(frames[0]) + if basis is not None: + basis = matrix(basis) + if len(basis) != n: + raise ValueError("Wrong common basis dimension") + inv = inverse(basis) + changed = [multiply(multiply(inv, a), basis) for a in frames] + if any(a[i][j] for a in changed for i in range(n) for j in range(i)): + raise ValueError("The supplied common basis does not triangularize every frame") + return {"rejected": True, "reason": "Exact common triangularizing basis", + "unique_frames": len(frames), "rank_lower_bound": "W*m"} + commuting = all(multiply(a, b) == multiply(b, a) for a, b in combinations(frames, 2)) + return {"rejected": commuting, + "reason": "Pairwise commuting frames" if commuting else "This sufficient screen is inconclusive", + "unique_frames": len(frames), "rank_lower_bound": "W*m" if commuting else None} diff --git a/research/percent-exponent-architecture/verify.py b/research/percent-exponent-architecture/verify.py new file mode 100644 index 0000000000..af85ad7f72 --- /dev/null +++ b/research/percent-exponent-architecture/verify.py @@ -0,0 +1,162 @@ +#!/usr/bin/env python3 +"""Reproduce the exact architecture screens using Python's stdlib and C++17. + +No optimizer, network access, supplier checkout or vector-code solver runs. +--deep adds the independent Python replay of the 16 prescribed-terminal +negative cases; the default already exhausts all permutations on all 87 +topologies in C++ and checks its matching method against direct enumeration. +""" +from __future__ import annotations + +import argparse +from collections import Counter +from hashlib import sha256 +from itertools import product +import json +import os +from pathlib import Path +import subprocess +import sys +import tempfile + +import audit +import center_basis + +HERE = Path(__file__).resolve().parent +sys.path.insert(0, str(HERE / "discovery")) +from fano_reuse import topologies +from balanced_fano import execute + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def manifest(): + paths = [p for p in HERE.rglob("*") if p.is_file() and p.name != "SOURCE.json" + and "__pycache__" not in p.parts and p.suffix in (".py", ".cpp", ".md", ".json")] + # The reference provenance itself is an input, not this manifest. + paths.append(HERE / "references/SOURCE.json") + paths.append(HERE / "NOTICE") + return {"files": {p.relative_to(HERE).as_posix(): sha256(p.read_bytes()).hexdigest() + for p in sorted(set(paths))}, + "scope": "This self-contained package only; inherited whole-algorithm interfaces are not discharged."} + + +def line(identifier, width, pairs): + values = [identifier, width, len(pairs), 0] + [v for pair in pairs for v in pair] + return " ".join(map(str, values)) + + +def run_binary(binary, cases): + text = "\n".join(line(c["id"], c["W"], c["pairs"]) for c in cases) + "\n" + done = subprocess.run([str(binary), "--all-permutations"], input=text, + text=True, capture_output=True, check=True) + rows = [json.loads(s) for s in done.stdout.splitlines()] + need([r["id"] for r in rows] == [c["id"] for c in cases], "Missing, duplicate or reordered search case") + return rows + + +def brute_control(case): + width, pairs = case["W"], case["pairs"] + routes = {tuple(range(width))} + for a, b in pairs: + next_routes = set(routes) + for permutation in routes: + new = list(permutation) + new[a], new[b] = new[b], new[a] + next_routes.add(tuple(new)) + routes = next_routes + actual = set() + words = 0 + for choices in product(range(6), repeat=len(pairs)): + rows = execute(width, pairs, choices) + if sorted(rows) != [1 << j for j in range(width)]: + continue + words += 1 + actual.add(tuple(row.bit_length() - 1 for row in rows)) + return {"routes": len(routes), "scalar_permutations": len(actual), + "matching_full_words": words, "outside_routing": bool(actual - routes)} + + +def controls(binary): + specs = [(3, []), (3, [(0, 1)]), (4, [(0, 1), (2, 3)]), + (4, [(0, 1), (1, 2), (2, 3)]), + (4, [(0, 1), (1, 2), (0, 2), (2, 3)]), + (4, [(0, 1), (1, 2), (2, 3), (0, 3), (1, 3)]), + (5, [(0, 1), (2, 3), (1, 4), (0, 2), (3, 4)]), + (5, [(0, 4), (1, 4), (2, 4), (3, 4), (0, 4)])] + cases = [{"id": 1000 + i, "W": w, "pairs": pairs} for i, (w, pairs) in enumerate(specs)] + results = run_binary(binary, cases) + for case, observed in zip(cases, results): + expected = brute_control(case) + need(observed["routing_permutations"] == expected["routes"], "Routing disagrees with direct enumeration") + need(observed["nonroutable_scalar_permutation"] == expected["outside_routing"], "Incorrect routing comparison") + if not observed.get("all_permutations_routable"): + need(observed["scalar_permutations"] == expected["scalar_permutations"], "Lost scalar permutations") + need(observed["matching_full_words"] == expected["matching_full_words"], "Lost matching complete words") + return {"direct_full_word_controls": len(cases), "all_passed": True} + + +def all_fano(binary): + cases = list(topologies()) + need(len(cases) == 87, "The finite topology family changed") + results = run_binary(binary, cases) + for result in results: + need(not result["nonroutable_scalar_permutation"], "A nonroutable scalar candidate needs a frame investigation") + if not result.get("all_permutations_routable"): + need(result["prefix_assignments"] == result["suffix_assignments"] == 6**7, + "An enumeration half is incomplete") + need(result["scalar_permutations"] == result["routing_permutations"], "Unexpected permutation-set count") + return {"status": "ALL COMPLETED SCALAR PERMUTATIONS ARE ROUTABLE IN THIS FINITE FAMILY", + "topologies": len(cases), "width_counts": dict(sorted(Counter(c["W"] for c in cases).items())), + "topology_specification_sha256": sha256(json.dumps(cases, sort_keys=True).encode()).hexdigest(), + "results": results, + "scope": "All 87 chronological balanced-Fano stub reuses; all local GL(2,F2) gates; every full output permutation, including arbitrary auxiliary/data exchanges. This does not cover vector gates or other graphs."} + + +def compare(name, value, writing): + content = json.dumps(value, sort_keys=True, indent=2) + "\n" + path = HERE / name + if writing: + path.write_text(content) + else: + need(path.read_text() == content, "Regenerated certificate differs: " + name) + + +def main(): + need(not sys.flags.optimize, "Run without -O") + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--write", action="store_true") + parser.add_argument("--deep", action="store_true") + args = parser.parse_args() + before = manifest() + if not args.write: + need(before == json.loads((HERE / "SOURCE.json").read_text()), "Package source closure changed") + compare("ceiling-certificate.json", audit.certificate(), args.write) + compare("center-basis-certificate.json", center_basis.certificate(), args.write) + print("PASS exact data/family ceilings and the sharp rank-minimal center controls", flush=True) + env = dict(os.environ, PYTHONDONTWRITEBYTECODE="1") + subprocess.run([sys.executable, "-B", str(HERE / "test_audit.py")], check=True, env=env) + with tempfile.TemporaryDirectory(prefix="percent-exponent-check-") as directory: + binary = Path(directory) / "balanced-search" + subprocess.run([os.environ.get("CXX", "c++"), "-std=c++17", "-O3", "-Wall", "-Wextra", "-Werror", + str(HERE / "discovery/balanced_search.cpp"), "-o", str(binary)], check=True) + compare("enumeration-controls.json", controls(binary), args.write) + compare("fano-all-permutations.json", all_fano(binary), args.write) + print("PASS all 87 topologies and all scalar permutations; independent full-word controls", flush=True) + if args.deep: + command = [sys.executable, "-B", str(HERE / "fano_reuse_verify.py")] + if args.write: + command.append("--write") + subprocess.run(command, check=True, env=env) + if args.write: + (HERE / "SOURCE.json").write_text(json.dumps(manifest(), sort_keys=True, indent=2) + "\n") + else: + need(manifest() == before, "Verification changed package inputs") + print("PASS conditional architecture audit; no new multiplication exponent", flush=True) + + +if __name__ == "__main__": + main()