diff --git a/.github/workflows/design-ceiling.yml b/.github/workflows/design-ceiling.yml new file mode 100644 index 0000000000..a21c3328b0 --- /dev/null +++ b/.github/workflows/design-ceiling.yml @@ -0,0 +1,32 @@ +name: design-ceiling + +on: + pull_request: + paths: + - 'research/design-ceiling/**' + - 'scripts/paired_cube/**' + - 'scripts/paired_cube_producer.py' + - 'certificates/paired-cube-complex-input.json' + - '.github/workflows/design-ceiling.yml' + push: + paths: + - 'research/design-ceiling/**' + - '.github/workflows/design-ceiling.yml' + +jobs: + ceiling: + 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: The ceiling, exact, compared with expected.json + run: python3 research/design-ceiling/ceiling.py --check + - name: Counting lemmas at small p + run: python3 research/design-ceiling/ceiling.py --brute + - name: The lemmas on the certified #144 word + run: python3 research/design-ceiling/model_check.py diff --git a/research/design-ceiling/NOTICE b/research/design-ceiling/NOTICE new file mode 100644 index 0000000000..b74506e03e --- /dev/null +++ b/research/design-ceiling/NOTICE @@ -0,0 +1,9 @@ +A ceiling on kappa for every word on #144's paired-cube design +Copyright 2026 DaysSky. Licensed under the Apache License, Version 2.0. + +Prepared by DaysSky with Anthropic Claude assistance. + +model_check.py imports and runs, unchanged, this repository's paired-cube producer and frame routines +(icekylinx, PR #144 and #130). With --tree it also reads the frame-and-reuse layer and the terminal sinks of a +checkout that has them (eumemic, PR #155 to #168; terminal-sink lemma by jamesyc, PR #166). Their notices and +licenses are retained. diff --git a/research/design-ceiling/PROOF.md b/research/design-ceiling/PROOF.md new file mode 100644 index 0000000000..1ef22fcf32 --- /dev/null +++ b/research/design-ceiling/PROOF.md @@ -0,0 +1,599 @@ +# A ceiling on κ for every word on #144's paired-cube design + +**Claim.** Keep the design of #144 and change anything else about the local word, including `p`. Then the complex +supplier's saving `a` and the certified κ satisfy + + a < 2.5657 × 10⁻³ and κ < a/(1+a) < 2.5592 × 10⁻³. + +The design is fixed by five things: + +- the paired-cube ports; +- the identity `K + H + B = I`; +- the coordinate-star decoder for `B`; +- the `K` step on the source registers; +- the three-stage shared cores. + +The parts that may change are the circuit, the root groups, the gauges, the reuse pairs, the terminal sinks, every +frame and `p`. + +**What it covers.** The claim is about words that obey rules R1–R8 of §3.4. These describe #144's word format, as +checked by `scripts/paired_cube/verify.py`, by the frame-and-reuse layer of #155–#168 (`paired_cube_physical.py`) and +by the terminal-sink gate of #168. It does **not** cover the source-assisted words of #184, #191, #193 and #194. Those +use the original source registers as controls and exact cancellation, which breaks R1 and R2. §11 says more. + +For comparison, the selected construction on main certifies κ = 6.618855 × 10⁻⁴, with complex saving +6.623239 × 10⁻⁴. Its complex word is #181's with #186's frame cuts, reuse pairs and sinks, which are changes of the +kind these rules allow. The ceiling is about 3.87 times that κ. + +This note makes no κ claim. It explains: + +- how κ is certified (§1); +- two facts about the cost function (§2); +- what is fixed and what is free (§3); +- each lemma, with its proof (§4–§8); +- the charging argument that turns the lemmas into a cost floor (§9); +- how the number is computed, and which steps use a computer (§10); +- scope and limits (§11). + +--- + +## 1. How a construction certifies κ + +### 1.1 The ledger + +The repository proves `T(n) = O(n·(log n)^{1−κ})` for integer multiplication; larger κ is better. A construction +feeds the assembly a *supplier*. For this note, a supplier is a ledger with three parts: + +- a number `m` (here `m = 3h`, defined in §3); +- a role count `W`; +- a multiset of **children**: `n_r` children of width `r`, for integers `0 < r < m`. + +The construction's bookkeeping guarantees the rank-mass identity + + Σ_r r·n_r = W·m − D, (1) + +where `D` is the **deficit**, fixed by the design (§3.5). + +### 1.2 Lemma 1: `a < D/C` + +The repository certifies a saving `a` when an exact rational upper bound shows + + Σ_r n_r · r · (m/r)^a < W·m. (2) + +Put `f(r) = r·ln(m/r)` and define the **cost** `C = Σ_r n_r·f(r)`. + +**Lemma 1.** If (2) holds, then `a < D/C`. + +*Proof.* `e^x ≥ 1 + x`, so `(m/r)^a ≥ 1 + a·ln(m/r)` for every child. Multiply by `r·n_r` and sum. Then (2) +gives `W·m > Σ r·n_r + a·C`, and by (1) this equals `W·m − D + a·C`. ∎ + +So the task is to show that **every** word on the design pays at least some cost `C_lo`. Then `a < D/C_lo`. + +### 1.3 From `a` to κ + +Both assemblies on main (`scripts/structured_bulk_assembly.py` and the balanced one in +`research/coordinated-frames-and-entrance-banks/arithmetic/balanced_shared.py`) take a transfer saving `a′` and +require three things: + +- `a′` is below the complex saving `a`; +- `q = a′(1 − 2η)` with a backoff `η > 0`; +- κ is below the margin `ε_A·q`, where `ε_A ≤ (1 − η)/(1 + q)`. + +Hence `κ < q/(1 + q) < a/(1 + a)`. + +--- + +## 2. Two facts about `f` + +`f''(r) = −1/r < 0`, so `f` is strictly concave. Since `f(0⁺) = 0`, it is also strictly subadditive: +`f(x) + f(y) > f(x+y)`. + +**Lemma 2 (chains).** Suppose a register climbs a total of `t` dimensions in steps `r₁, …, r_k`, each a positive +integer. Its cost `Σ f(rᵢ)` is at least + +- `f(t)`; +- `f(1) + f(t−1)` if `k ≥ 2`; +- `2f(1) + f(t−2)` if `k ≥ 3`. + +*Proof.* Merging two steps lowers the cost (subadditivity). So it is enough to treat exactly 1, 2 or 3 steps. The +cost is a concave function of the steps on the simplex `{rᵢ ≥ 1, Σ rᵢ = t}`. A concave function is smallest at a +vertex, and the vertices are the permutations of `(1, t−1)` and of `(1, 1, t−2)`. ∎ + +Three derived quantities appear below: + +| symbol | definition | meaning | +|---|---|---| +| `δ` | `f(1) + f(h−2) − f(h−1)` | extra cost of one intermediate stop in a climb of `h − 1` | +| `ε` | `f(1) + f(h−3) − f(h−2)` | extra cost of one more intermediate stop | +| `g₃` | `min(3f(1), f(3)) = f(3)` | cheapest way to be at a line in all three stages (§3.3) | + +By Lemma 2, a climb of `h − 1` with one intermediate stop costs at least `f(h−1) + δ`, and with two it costs at least +`f(h−1) + δ + ε`. + +--- + +## 3. The fixed design + +### 3.1 Addresses, ports and cubes + +Work in `F₂^h` with `h = 2p`. Group the coordinates into `p` pairs `{2i, 2i+1}`, and call the two coordinates of a +pair *partners*. A **port** `S` picks one coordinate from each of three different pairs, so there are +`v = 8·C(p,3)` ports. Its address `q_S ∈ F₂^h` is the indicator vector of `S`. Two facts follow: + +- `q_S·q_T ≡ |S∩T| (mod 2)`; +- `q_S·q_S = 1`. + +The **cube** of a port is the set of 8 ports on the same three pairs. Every port is both a **source** (input `x_S`, +held in the source register `X_S`) and a **target** (output register `y_T`). + +### 3.2 The identity, and what the auxiliary word must deliver + +The local word must add `x` into `y`. #144 splits the identity as `I = K + H + B`, where +`B_{T,S} = (|T∩S| − 1)/2`: + +- `B` is delivered by the `h` **coordinate stars** (copied centres). Star `i` is the sum of `x_S` over the ports + containing coordinate `i`. +- `K` acts inside each cube. It is implemented on the source registers themselves (§3.4, R7). +- `H = −B` on pairs of ports in **different** cubes, and 0 inside a cube. It is the only part delivered by the + **auxiliary word**. + +For `T` and `S` in different cubes, `H_{T,S} = −(|T∩S| − 1)/2`. That is `½` if `|T∩S| = 0`, `0` if it is 1, and +`−½` if it is 2. Define + + row(T) = { S in another cube : |S∩T| ∈ {0, 2} }, col(S) = { T : S ∈ row(T) }. + +The relation is symmetric, so `row(T) = col(T)` as sets of ports. The auxiliary word must carry each `x_S` to every +`y_T` with `T ∈ col(S)`. Since `|S∩T|` is even exactly when `q_S·q_T = 0`, every `S ∈ row(T)` has `q_S ∈ q_T^⊥`. + +`scripts/paired_cube/verify.py` checks this identity entry by entry (`Signed H mismatch`). + +### 3.3 Frames: what a register pays + +A **register** below always means a physical register. Every register has, at every moment of a stage, a **frame**: +a subspace of `F₂^h`. Within a stage, a register's frames form an ascending chain, each containing the previous +one. Each strict step from dimension `d` to `d′` is one child of width `d′ − d`. A register is *at* `F` when `F` is +its current frame, and its **stops** are the frames of its chain. + +An auxiliary register's chain ends at the full space `F₂^h`. It starts in one of two ways: + +- at `0`, and then every step is paid in each of the three stages; +- at a **gauge** `σ`: the chain starts at `σ`, and one merged child of width `3·dim σ` is paid once for all three + stages. + +So an auxiliary register that is ever at a line (a frame of dimension 1) has paid at least `g₃` to be there: three +steps of width 1 (`3f(1)`), or one merged gauge child (`f(3)`). + +### 3.4 The word: what may vary + +Within the design, the local word is the reversible "transparent" sequence + + z ← z + Vx (inject each source x_S into its own source role) + z ← Mz (operations among auxiliary registers) + y ← y + Jz (reads: deliver root values into targets) + +followed by the inverse cleanup at the full frame. The rules for any word: + +- **R1. Operations.** An operation `a ← a ± b` between auxiliary registers runs with both registers at one common + frame `F`. `F` contains `q_S` for every source `S` in the **conservative support** of the value moved. The + conservative support is every source with a path to that value in the circuit; signed cancellation does not + remove a source. +- **R2. Injection.** `x_S` enters the auxiliary word once: by the injection into its source role, at a frame + containing `q_S`. +- **R3. Root groups.** A root group `G` is a set of targets. Its value is read from an auxiliary register into every + `y_T` with `T ∈ G`, with that register at the read's frame. The frame contains the value's conservative support and + lies inside the group's **cap** + + cap(G) = ( span{ q_T : T ∈ G } )^⊥. + + In the certified words the read frame is the cap itself. +- **R4. Old values.** A role's register holds arbitrary old content when the role begins. That content is cancelled by + a read from the register at the frame it has at that moment: `0` for an ungauged role, the gauge otherwise. The + read goes into every target that the role's content reaches. +- **R5. Reuse pairs.** A recipient role may take over a donor's register after the donor's last operation. The + register's chain is the donor's chain followed by the recipient's. +- **R6. Terminal sinks** (#166, #168). A sink role with group `G` and pivot `p ∈ G` is deleted. Each write into it + becomes a write into `y_p` at the original frame `F_i ⊆ cap(G)`, with the control register and `y_p` at `F_i`. + For every other target `t ∈ G`, `y_t −= y_p` runs at frame 0 before the first write and `y_t += y_p` runs at + `cap(G)` after the last. Groups of different sinks are disjoint. +- **R7. Data registers.** + - `y_T` climbs from `0` to its top, `q_T^⊥`. Every read or write into `y_T` happens with `y_T` at that event's + frame. + - `X_S` is used by the auxiliary word only for the injection. Its itinerary is fixed by the `K` step: it starts at + `span(q_S)`, moves to a 3-dimensional frame, then to a hyperplane, then to the full space. Its steps are + `2, h−4, 1` in every word (`K_source_itinerary_verified` in `verify.py`). +- **R8. Stages.** All three stages run the same local word. + +A **delivery** into `y_T` is an event that adds auxiliary-word content to `y_T`: a root read (R3), an old-value read +(R4), a sink write into a pivot, or the final `y_t += y_p` of a sink (R6). By R7 its frame is a stop of `y_T`, so it +lies in `q_T^⊥`. By R1 and R3 it contains `q_S` for every source it carries. + +Free: `M`, the groups, the gauges, the pairs, the sinks, every frame and `p`. Fixed: the ports, the identity, the +stars and the `K` step. + +### 3.5 The fixed part of the ledger and the deficit + +Every word pays the following, per port and over three stages: + +| part | children | cost | +|---|---|---| +| source registers (R7) | three each of widths `1`, `2`, `h−4` | exactly `3(f(1) + f(2) + f(h−4))` | +| target registers | a climb of `h − 1` per stage | at least `3f(h−1)` | +| endpoints | two of width `2` | exactly `2f(2)` | +| star copies | `3h` of width `h − 2` per vertex | exactly `3h·f(h−2)/v` | + +The stars cost `ℓ = h(h−2)` in rank, and the deficit is + + D = 2v − 3ℓ = (8/3)·p(p−1)(p − 6.5). + +`D ≤ 0` for `p ≤ 6`, so no positive saving is possible there. From here on `p ≥ 7`. + +--- + +## 4. Paths only climb + +A **path** of `x_S` follows the value from its injection to a delivery. Each hop is one of: + +- an operation, where both registers are at the same frame; +- a read or a sink write, where the auxiliary register and the target register are at the same frame; +- the final `y_t += y_p` of a sink, where both target registers are at `cap(G)`. + +Between hops the value stays in one register, whose frames ascend. A recipient continues its donor's register, so a +reuse pair is not a hop. Hence **the frames along a path never decrease.** + +Two consequences are used below. + +- **Supports lie in frames.** A register's conservative support always lies in its current frame. Content arrives by + an injection or an operation at a frame containing it (R1, R2), and the frame only grows afterwards. +- **Deliveries are orthogonal.** If a path of `x_S` ends with a delivery into `y_T` at frame `F`, then every earlier + frame `E` on the path satisfies `E ⊆ F ⊆ q_T^⊥`, so `q_T ⊥ E`. + +For every `T ∈ col(S)` there is a path of `x_S` to `y_T`, because `H_{T,S} ≠ 0`. + +--- + +## 5. Three counting facts + +**Count.** `|col(S)| = 12(p−3) + 12·C(p−3, 2) + 8·C(p−3, 3)`. + +*Proof.* Write `S = {s₀, s₁, s₂}`, let `s̄ᵢ` be the partner of `sᵢ`, and call the other `p − 3` pairs *free*. Sort +`T ∈ col(S)` by how many of `S`'s pairs it uses: + +- none: any port on free pairs, `8·C(p−3,3)` of them; +- one: its coordinate there must be `s̄ᵢ`, giving `3 · 4·C(p−3,2)`; +- two: its coordinates there must be `{sᵢ, sⱼ}` or `{s̄ᵢ, s̄ⱼ}`, giving `3 · 2 · 2(p−3)`; +- three: the same cube, excluded. ∎ + +**Lemma S.** For `p ≥ 7`, the vectors `{q_T : T ∈ col(S)}` span exactly `q_S^⊥`, of dimension `h − 1`. + +*Proof.* Every such `q_T` lies in `q_S^⊥`. For the converse, there are `p − 3 ≥ 4` free pairs. + +1. Ports on free pairs are in `col(S)`. Two of them that differ in one coordinate sum to `e_u + e_{u′}`, where `u` and + `u′` are partners or lie in different free pairs (this needs a fourth free pair). Such vectors give every + even-weight vector on the free coordinates, and a single port adds an odd one. So every `e_x` with `x` free is in + the span. +2. `{s̄ᵢ, y, z}` with `y`, `z` free is in `col(S)`. By step 1, every `e_{s̄ᵢ}` is in the span. +3. `{sᵢ, sⱼ, z}` with `z` free is in `col(S)`. So `e_{sᵢ} + e_{sⱼ}` is in the span. + +These vectors span a space of dimension `2(p−3) + 3 + 2 = h − 1`. ∎ + +**Lemma M.** Let `p ≥ 7` and `w ∉ {0, q_S}`. Then at least `μ = 4(p−3)` targets `T ∈ col(S)` have `w·q_T = 1`. + +*Proof.* Let `N(w)` count those targets. There are three cases. + +- **(a) `w` differs on the two coordinates of some free pair `k`.** Swapping the coordinate that `T` uses in pair `k` + is an involution on the targets of `col(S)` that use `k`, and it flips `w·q_T`. There are `4(p−2)(p−4) + 12` such + targets, so `N ≥ 2(p−2)(p−4) + 6`. +- **(b) `w` is constant on every free pair, equal to 1 on a free pair `k` and 0 on a free pair `k′`.** Moving `T`'s + coordinate from `k` to the same position in `k′` maps the targets that use `k` but not `k′` one-to-one onto those + that use `k′` but not `k`, and flips the parity. So `N ≥ 4(p² − 8p + 18)`. +- **(c) `w` equals one value `c` on every free coordinate.** By the count above, + + N = 8·C(p−3,3)·c + 4·C(p−3,2)·#{i : w_{s̄ᵢ} = 1} + 2(p−3)·#{pairs P : w(P) + c odd}, + + where `P` runs over the six pairs `{sᵢ, sⱼ}` and `{s̄ᵢ, s̄ⱼ}`. + - If `c = 1`, then `N ≥ 8·C(p−3,3)`. + - If `c = 0` and some `w_{s̄ᵢ} = 1`, then `N ≥ 2(p−3)(p−4)`. + - Otherwise `w` lives on `{s₀, s₁, s₂}` with weight 1 or 2. Exactly two pairs `{sᵢ, sⱼ}` then have odd weight, so + `N = 4(p−3)`. + +Every bound is at least `4(p−3)` for `p ≥ 7`. ∎ + +*Consequence.* Let `Φ ∋ q_S` be a subspace of dimension at least 2, and pick `w ∈ Φ` outside `span(q_S)`. Then at +least `μ` targets of `col(S)` are not orthogonal to `Φ`. Also `|col(S)| ≥ 2μ`. + +--- + +## 6. Every source enters at its own line + +**Lemma E.** Let `p ≥ 7`. + +1. The register of the source role of `S` is at exactly `span(q_S)` when `x_S` is injected. +2. For all but at most `n_g = ⌊v/|col|⌋` sources, that register is at frame 0 when the source role begins. It then + steps to the line, which costs `3f(1)` over the three stages. + +*Proof.* + +1. Let `F` be the frame of the injection, so `q_S ∈ F`. Every path of `x_S` starts there. By §4, `q_T ⊥ F` for every + `T ∈ col(S)`. Lemma S gives `F ⊆ (q_S^⊥)^⊥ = span(q_S)`. +2. Before the injection the register's frames lie in the line, so each is `0` or the line. Suppose the register is + already at the line when the source role begins. By R4 the role's old content is read at the line into every + target it reaches. The role's content reaches every `T ∈ col(S)`, since `x_S` does. So every such `y_T` has + `span(q_S)` as a stop. A chain has at most one stop of dimension 1, so the sets `col(S)` of these sources are + pairwise disjoint. There are at most `v/|col|` of them. ∎ + +In the certified words no source role is gauged (`selected_sources_untouched` in `verify.py`), so the exceptional set +is empty there. + +--- + +## 7. Every target has registers at its own hyperplane + +Call an auxiliary register a **T-register** if it is at `q_T^⊥` at some moment. Its next frame is the full space, so +a register is a T-register for at most one target. + +**Lemma T.** Let `p ≥ 7` and let `T` be a target. + +1. `T` has a T-register. +2. If `y_T` has no stop strictly between `0` and `q_T^⊥`, then `T` has two different T-registers. + +*Proof.* + +1. For every `S ∈ row(T)`, some delivery into `y_T` carries `x_S`. Its frame contains `q_S` and is a stop of `y_T`. + Stops are nested, so the largest of these frames, `F*`, contains `q_S` for every `S ∈ row(T)`. Those vectors span + `q_T^⊥` (Lemma S, with `row(T) = col(T)`), and `F* ⊆ q_T^⊥`. So `F* = q_T^⊥`. + + The delivery at `F*` is not the final `y_t += y_p` of a sink. That step runs at `cap(G)` for a group with at least + two targets, of dimension at most `h − 2`. So it is a root read, an old-value read or a sink write, and in each of + those an auxiliary register is at `F*`. +2. Every delivery that carries a source is at a nonzero stop of `y_T`, hence at `q_T^⊥`, and as in part 1 it comes + from an auxiliary register at `q_T^⊥`. If two registers deliver, we are done. Otherwise one register `R` makes + every delivery, so at its last delivery its conservative support contains `row(T)`. + + Look at the last arrival of content into `R` before that delivery, at frame `F`. All earlier arrivals were at + frames inside `F`, so `R`'s support lies in `F` (§4). Hence `q_T^⊥ = span(row(T)) ⊆ F ⊆ q_T^⊥`. An injection + happens at a line (Lemma E), so this arrival is an operation `R ← R ± b`. The register `b` is auxiliary, differs + from `R`, and is at `q_T^⊥`. ∎ + +--- + +## 8. Every source fans out through its units + +### 8.1 Units + +Fix a source `S`. A **unit** of `S` is an auxiliary register that is at `span(q_S)` at some moment. The source role's +register is a unit (Lemma E). A chain has one stop of dimension 1 at most, so units of different sources are +different registers. A unit's **exit** `Φ` is its next frame after the line. Units come in three kinds: + +| kind | exit dimension | targets `T ∈ col(S)` with `q_T ⊥ Φ` | +|---|---|---| +| **big** | `2 … h−2` | misses at least `μ` of them (Lemma M) | +| **small** | `h − 1` | at most one (`Φ^⊥` is a line) | +| **idle** | `h` | none | + +### 8.2 Targets served at the line + +Let `L(S)` be the set of targets `T ∈ col(S)` of one of two kinds: + +- **line targets:** some delivery into `y_T` happens at the frame `span(q_S)`; +- **pivot targets:** `T` is a non-pivot target of a sink group `G` whose pivot register has the stop `span(q_S)`, and + `span(q_S) ⊆ cap(G)`. + +Two facts: + +- **Each `T ∈ L(S)` has an intermediate stop.** A line target has the stop `span(q_S)`. A pivot target has the stop + `cap(G)`, where the sink's final `y_t += y_p` runs. That frame contains `q_S` and has dimension at most `h − 2`. +- **A target is in `L(S)` for at most two sources, and then it has two intermediate stops.** It is a line target for + at most one source, because `y_T` has one stop of dimension 1 at most. It is a pivot target for at most one + source, because it is in at most one sink group and the pivot has one stop of dimension 1 at most. If it is a line + target for `S′` and a pivot target for `S ≠ S′`, the stops `span(q_{S′})` and `cap(G) ∋ q_S` are different. + +### 8.3 Lemma D + +**Lemma D.** Let `p ≥ 7`, and let `S` have `b` big units and `s` small units. Then one of the following holds: + +- `b ≥ 2`; +- `b = 1` and `|L(S)| + s ≥ μ`; +- `b = 0` and `|L(S)| + s ≥ |col(S)|`. + +*Proof.* Take `T ∈ col(S)` outside `L(S)`, and a path of `x_S` to `y_T`. It starts at `span(q_S)` (Lemma E). Let `r` +be the last register on the path that holds the value at the frame `span(q_S)`. + +- `r` is not `y_T`, since `T` is not a line target. +- `r` is not a pivot `y_p`. From `y_p` the value can only continue by the sink's final `y_t += y_p` at `cap(G)`. Frames + ascend, so `span(q_S) ⊆ cap(G)`, and `T` would be a pivot target. +- `r` is no other target register, because only a pivot passes a value on. + +So `r` is an auxiliary register, that is, a unit `u`. A hop at the line would land in another register at the line, +so the value stays in `u` until `u` moves to its exit `Φ_u`. Every later frame on the path contains `Φ_u`, so +`q_T ⊥ Φ_u` (§4). + +Hence every target of `col(S)` outside `L(S)` is orthogonal to the exit of some big or small unit. One big unit +misses at least `μ` targets, and each small unit covers at most one. ∎ + +--- + +## 9. The cost floor + +### 9.1 What registers cost (three stages) + +Put + + U₂ = g₃ + 3f(1) + 3f(h−2), I₀ = g₃ + 3f(h−1). + +By §3.3 and Lemma 2: + +| register | stops after its entrance | cost at least | +|---|---|---| +| idle unit | line, full | `I₀` | +| small unit | line, hyperplane, full | `U₂` | +| big unit | line, exit, full | `U₂` | +| big unit that is a T-register | line, exit, `q_T^⊥`, full | `U₂ + 3ε` | +| T-register that is not a unit | `q_T^⊥`, full | `3f(1)` | + +A small unit whose exit is `q_T^⊥` is a T-register at no extra cost. An idle unit is never a T-register. + +For the source role's register, `g₃` can be replaced by `3f(1)` unless `S` is one of the `n_g` exceptions of +Lemma E. That adds `3f(1) − f(3)` to each of its floors. + +A target register costs at least `3f(h−1)`. It costs `3δ` more with one intermediate stop, and `3δ + 3ε` more with +two (Lemma 2). + +### 9.2 Charging + +Put `ρ = U₂/μ`. Make two kinds of transfer: + +- every T-register pays `3ε` to its target; +- every target `T ∈ L(S)` pays `ρ` to `S`. + +Transfers cancel in the total. So the cost of all target registers and auxiliary registers equals the sum of three +kinds of balance: one per target, one per source, and one per auxiliary register that is no unit. + +**Targets.** The balance of `T` is its extra cost above `3f(h−1)`, plus what it receives, minus what it pays. It is at +least + + τ = min( 6ε, 3δ + 3ε − ρ ). + +- No intermediate stop: `T` is in no `L(S)` (§8.2) and has two T-registers (Lemma T). Balance `≥ 6ε`. +- An intermediate stop, and `T` in at most one `L(S)`: extra cost `≥ 3δ`, one T-register, at most one payment. + Balance `≥ 3δ + 3ε − ρ`. +- `T` in two sets `L(S)`: two intermediate stops (§8.2), so extra cost `≥ 3δ + 3ε`. Balance + `≥ 3δ + 6ε − 2ρ ≥ 3δ + 3ε − ρ`, because `ρ ≤ 3ε`. + +**Registers that are no unit.** A T-register costs `≥ 3f(1)` and pays `3ε ≤ 3f(1)`. Balance `≥ 0`. + +**Sources.** The balance of `S` is the cost of its units, minus their payments, plus `ρ·|L(S)|`. After payments a big +unit keeps at least `U₂`, a small unit at least `U₂ − 3ε ≥ ρ`, and an idle unit at least 0. By Lemma D: + +- `b ≥ 2`: balance `≥ 2U₂`; +- `b = 1`: balance `≥ U₂ + ρ·(s + |L(S)|) ≥ U₂ + ρμ = 2U₂`; +- `b = 0`: balance `≥ ρ·(s + |L(S)|) ≥ ρ·|col| ≥ 2ρμ = 2U₂`. + +In each case the source role's register is one of the units, and its floor is higher by `3f(1) − f(3)` unless `S` is +an exception. So the balance is at least `2U₂ + 3f(1) − f(3)` for all but `n_g` sources. + +The argument uses four side conditions: `ε ≤ f(1)`, `ρ ≤ 3ε`, `U₂ − 3ε ≥ ρ` and `|col| ≥ 2μ`. The last is §5. The +script asserts the others exactly at every `p` it evaluates. + +### 9.3 Theorem + +**Theorem.** For every `p` with `7 ≤ p ≤ 99`, every word on the design satisfies `C ≥ C(p)`, where + + C(p) = v·[ 3(f(1) + f(2) + f(h−4)) + 3f(h−1) + 2f(2) + 2U₂ + τ ] + + (v − n_g)·(3f(1) − f(3)) + 3h·f(h−2). + +*Proof.* Add the fixed part of §3.5 to the balances of §9.2. ∎ + +In words: besides the data registers, every source needs two registers that leave its line and stop again before the +full space, and every target needs two registers at its hyperplane or a stop of its own. + +--- + +## 10. The numbers + +`ceiling.py` computes `D/C(p)` for `7 ≤ p ≤ 99` in exact rational arithmetic. + +- `ln x` reduces to `x ∈ [1, 2)` by halving, then uses `ln x = 2·atanh((x−1)/(x+1))` and `ln 2 = 2·atanh(1/3)`. +- Partial sums of `atanh` are lower bounds, since every term is positive. Adding the geometric tail + `z^{2K+1} / ((2K+1)(1 − z²))` gives upper bounds. +- A lower bound is used wherever `f` enters `C(p)` positively and an upper bound wherever it is subtracted. + +So every printed bound is a true upper bound on `a`. + +| p | 7 | 9 | 11 | 12 | **13** | 14 | 16 | 20 | 30 | 60 | 99 | +|---|---|---|---|---|---|---|---|---|---|---|---| +| `a <` | 7.11e-4 | 2.0837e-3 | 2.4856e-3 | 2.5487e-3 | **2.5657e-3** | 2.5540e-3 | 2.4832e-3 | 2.2753e-3 | 1.7935e-3 | 1.0549e-3 | 6.829e-4 | + +**Tail, `p ≥ 100`.** By Lemma E every source role's register climbs from its line to the full space, which costs at +least `3f(h−1)`. The source and target registers cost at least `3f(h−1)` each (Lemma 2). For `r < h` we have +`m/r > 3`, so `f(r) > r·ln 3`. Hence `C > 9v(h−1)·ln 3`, and with `D < 2v`, + + a < 2 / ((18p − 9)·ln 3) ≤ 1.0165 × 10⁻³ for p ≥ 100. + +The maximum is at `p = 13`: + + a < 2.5657 × 10⁻³ and κ < a/(1+a) < 2.5592 × 10⁻³ for every word on the design, at every p. + +The cost per port at `p = 13` (`h = 26`, `m = 78`, `v = 2288`, `D = 2704`): + +| term | cost per port | +|---|---:| +| source registers `3(f(1) + f(2) + f(h−4))` | 118.59 | +| target registers and endpoints `3f(h−1) + 2f(2)` | 99.99 | +| two units per source `2U₂` | 215.42 | +| target balance `τ` | 22.37 | +| source roles enter from 0 | 3.29 | +| star copies | 0.96 | +| **total** | **460.63** | + +Each ingredient lowers the ceiling: + +| floor | ceiling on `a` | +|---|---:| +| data registers and star copies only | 6.3627e-3 | +| + one unit per source (Lemma E) | 4.2121e-3 | +| + a second non-idle unit per source (Lemma D) | 2.9420e-3 | +| + registers at each target's hyperplane (Lemma T) | 2.7868e-3 | +| + source roles enter from frame 0 (Lemma E) | 2.7653e-3 | +| + the `K` itinerary of the source registers (R7) | 2.5657e-3 | + +If the `K` step were also free, the source registers would only be known to cost `3f(h−1)`, and the ceiling would be +the fifth row. + +--- + +## 11. Scope and limits + +**Assumed.** Rules R1–R8 of §3.4, as properties of #144's word format: + +- each source is injected once, into one source role; +- `H` is produced only through auxiliary root groups and sinks, with conservative supports inside frames; +- every role's old content is cancelled by a read at the frame where the role begins; +- sink groups are disjoint; +- the source registers follow the `K` itinerary, and the three stages run the same word. + +**Not covered.** + +- **Source-assisted words** (#184, #191, #193, #194). They use the original source registers as controls at later + frames and reuse registers after exact cancellation. That breaks R2 and the conservative supports of R1, so + Lemmas E, T and D do not apply. Their best complex saving so far is 7.009184 × 10⁻⁴ (#193). +- **A different decoder, port family or stage structure.** Those change §3. +- **The bit supplier.** The bound is on the complex saving. κ is also below the bit saving, which this note does not + bound. + +**Proved by hand, for all `p ≥ 7`:** Lemmas 1, 2, S, M, E, T, D, the count of `col(S)`, the charging of §9 given its +side conditions, and the tail. + +**Computer, exact arithmetic (`ceiling.py`):** + +- `D/C(p)` for `7 ≤ p ≤ 99`, and the maximum over `p`; +- the side conditions of §9.2 at each of those `p`; +- the tail value at `p = 100`. + +**Computer, sanity only (not used by the proof):** + +- `ceiling.py --brute` enumerates `col(S)`, checks Lemma S, and checks Lemma M: over every `w` at `p = 7, 8`, and over + one `w` from each symmetry orbit for `7 ≤ p ≤ 16`. +- `model_check.py` rebuilds the abstraction of §3–§8 for a real certified word and checks every lemma's conclusion + on it. On #144's word (`p = 12`, on main) and on #168's word (`p = 11`, with frame layer, 2,310 reuse pairs and 47 + sinks) it finds: + - the abstraction lists exactly the certified children; + - every source role enters from frame 0 at its own line; + - every source has three units, all big, and every target of `col(S)` is reached through a unit exit; + - every target has three T-registers (#144) or two (#168); + - every unit, source and target pays at least its floor. + + It was not run on main's selected word (#186), which is stored in its own archive format. + +**Not tight.** On those two words the floor `C(p)` is 19% and 26% of the certified cost. The theorem charges two +registers per source; the certified words use about eight auxiliary registers per port. The extra registers carry +each `x_S` above its line to its roughly `8p³/6` targets, and they are shared between sources. Charging them needs a +lower bound on frame-constrained, cancellation-free circuits for `H`, which this note does not have. + +**Not reviewed.** Nothing here is machine-checked beyond the scripts' exact arithmetic and self-tests, and no one +else has reviewed the proofs. + +## Reproduce + + python3 research/design-ceiling/ceiling.py --check # the ceiling, exact; under a second + python3 research/design-ceiling/ceiling.py --brute # counting lemmas at small p; a few seconds + python3 research/design-ceiling/model_check.py # the lemmas on #144's word; about 15 seconds diff --git a/research/design-ceiling/README.md b/research/design-ceiling/README.md new file mode 100644 index 0000000000..324a60a408 --- /dev/null +++ b/research/design-ceiling/README.md @@ -0,0 +1,99 @@ +# A κ ceiling for #144's paired-cube design + +This package proves that no word on #144's paired-cube design can certify more than + + κ < 2.5592 × 10⁻³ (complex saving a < 2.5657 × 10⁻³), + +whatever its circuit, root groups, gauges, reuse pairs, terminal sinks, frames and `p`. It makes no κ claim and +changes no existing file. + +For comparison, the selected construction on main certifies κ = 6.618855 × 10⁻⁴. The ceiling is about 3.87 times +that. Going beyond it needs a change of design, not a better word. + +## What is fixed, and what is not covered + +The design is the paired-cube ports, the identity `K + H + B = I`, the coordinate-star decoder, the `K` step on the +source registers and the three-stage shared cores. A word must obey the eight rules of [PROOF.md](PROOF.md) §3.4. +They describe #144's word format, as checked by `scripts/paired_cube/verify.py`, the frame-and-reuse layer of +#155–#168 and the terminal-sink gate of #168. + +The ceiling does **not** cover: + +- **source-assisted words** (#184, #191, #193, #194), which use the original source registers as controls and reuse + registers after exact cancellation; +- a different decoder, port family or stage structure; +- the bit supplier. The bound is on the complex saving, and κ is also below the bit saving. + +## The argument + +Write `D = 2v − 3ℓ` for the deficit and `C = Σ n_r·r·ln(m/r)` for the cost of the ledger's children. Every certified +saving satisfies `a < D/C`, and `κ < a/(1+a)`. So it is enough to show that every word pays a cost of at least +`C(p)`. + +The floor `C(p)` comes from one structural fact: along any path of a source value from its injection to a target, +frames never decrease. Three lemmas follow. + +- **Every source enters at its own line.** Its role's register starts at dimension 1 and must climb to the full + space. +- **Every source needs two registers that leave its line and stop again before the full space.** One subspace + larger than the line misses at least `4(p−3)` of the source's targets. +- **Every target needs two registers at its own hyperplane, or an extra stop of its own register.** Each such + register can only go to the full space afterwards. + +A charging argument adds these to the fixed cost of the data registers. Each ingredient lowers the ceiling: + +| Floor | Ceiling on `a` | +|---|---:| +| data registers and star copies only | 6.3627e-3 | +| + one register per source | 4.2121e-3 | +| + a second register per source | 2.9420e-3 | +| + registers at each target's hyperplane | 2.7868e-3 | +| + source roles enter from frame 0 | 2.7653e-3 | +| **+ the `K` itinerary of the source registers** | **2.5657e-3** | + +The maximum over `p` is at `p = 13`. Every `p` from 7 to 99 is evaluated exactly, and a tail bound covers `p ≥ 100`. + +[PROOF.md](PROOF.md) is self-contained: the ledger, the rules, each lemma with its proof, the charging argument and +the numbers. + +## Run + + python3 research/design-ceiling/ceiling.py --check # the ceiling, exact; under a second + python3 research/design-ceiling/ceiling.py --brute # counting lemmas at small p; a few seconds + python3 research/design-ceiling/model_check.py # the lemmas on #144's word; about 15 seconds + +All three use the Python standard library only and refuse `-O`. + +- **`ceiling.py`** evaluates `D/C(p)` in exact rational arithmetic, with every logarithm enclosed between two + rationals, and asserts the side conditions of the charging argument at every `p`. `--check` compares the results + with `expected.json`. +- **`ceiling.py --brute`** enumerates the counting lemmas: over every vector at `p = 7, 8`, and over one vector from + each symmetry orbit for `7 ≤ p ≤ 16`. This is a sanity check; the proofs cover every `p ≥ 7`. +- **`model_check.py`** rebuilds the proof's abstraction for the certified #144 word (`p = 12`) with the repository's + own producer. It checks that the abstraction lists exactly the certified children, and that every lemma's + conclusion holds on that word. `--tree PATH` runs it on another checkout; on #168's word (`p = 11`, with frame + layer, reuse pairs and sinks) it also passes. + +## How far from tight + +On #144's and #168's words the floor is 19% and 26% of the certified cost. The proof charges two registers per +source, and the certified words use about eight auxiliary registers per port. Closing that gap needs a lower bound +on frame-constrained circuits for `H`, which this package does not have. + +## Related + +- #183 (romainhedouin) gives the assembly's acceptance ceiling in closed form. This package bounds the supplier + saving that enters it. +- #192 bounds one fixed word (#168's) over all frame layouts, at 7.010e-4. This package bounds every word, far less + tightly. + +## Credits + +- icekylinx: the paired-cube design, its compiler and independent checker, shared cores and assembly (#144, #130). +- eumemic: the frame-and-reuse layer and terminal-sink gate (#155–#168), used here to state the rules and for the + local check on #168's word. +- jamesyc: the terminal-sink lemma (#166) and birth-read reuse (#124). +- an664: completed-core sharing (#128). +- romainhedouin: the assembly ceiling (#183). + +The lemmas, the charging argument and the scripts were prepared by DaysSky, assisted with Claude. diff --git a/research/design-ceiling/ceiling.py b/research/design-ceiling/ceiling.py new file mode 100644 index 0000000000..cf49661782 --- /dev/null +++ b/research/design-ceiling/ceiling.py @@ -0,0 +1,222 @@ +#!/usr/bin/env python3 +"""Exact evaluation of the design ceiling of PROOF.md (Python stdlib only). + +For every p >= 7, PROOF.md shows that every word on #144's paired-cube design pays at least + + C(p) = v [ 3(f(1) + f(2) + f(h-4)) source data registers (the K itinerary, fixed) + + 3 f(h-1) + 2 f(2) target data registers and endpoint children + + 2 U2 two non-idle units per source + + tau ] registers at each target's hyperplane, or a stop of y_T + + (v - n_g)(3 f(1) - f(3)) source roles enter from frame 0 + + 3h f(h-2) star copies + +with h = 2p, m = 3h, f(r) = r ln(m/r), v = 8 C(p,3) and + + U2 = f(3) + 3 f(1) + 3 f(h-2) + eps = f(1) + f(h-3) - f(h-2), delta = f(1) + f(h-2) - f(h-1) + mu = 4(p-3), tau = min(6 eps, 3 delta + 3 eps - U2/mu), n_g = floor(v / |col|). + +Then a < D / C(p) with D = 2v - 3h(h-2), and kappa < a / (1 + a). + +Arithmetic is exact. Every logarithm is enclosed between two rationals: partial sums of 2 atanh from below, the same +plus a geometric tail from above, both rounded outward to the grid 2^-200. A lower bound is used wherever a term +enters C positively and an upper bound wherever it is subtracted, so every printed ceiling is a true upper bound. +The script also asserts the side conditions of the charging argument at every p, and bounds all p > P_MAX by the tail +of PROOF.md. + +Usage: python3 research/design-ceiling/ceiling.py [--check] [--brute] + --check compare the results with expected.json + --brute brute-force the counting lemmas at small p (sanity only; the proofs in PROOF.md cover every p >= 7) +""" +import argparse +import json +import sys +import time +from fractions import Fraction as Q +from itertools import combinations, product +from math import comb +from pathlib import Path + +if sys.flags.optimize: + raise SystemExit('Assertions must remain enabled: run without -O') + +HERE = Path(__file__).resolve().parent +GRID = 1 << 200 +P_MIN, P_MAX = 7, 99 +T0 = time.time() + + +def log(*a): + print('[%4.0fs]' % (time.time() - T0), *a, flush=True) + + +# ---------------------------------------------------------------------------------------------- enclosed logarithms +def down(x): + return Q((x.numerator * GRID) // x.denominator, GRID) + + +def up(x): + return Q(-((-x.numerator * GRID) // x.denominator), GRID) + + +def atanh(z, upper, terms=45): + """Partial sum of atanh z = sum z^(2j+1)/(2j+1) for 0 <= z < 1: a lower bound; with the tail, an upper bound.""" + s = sum((z ** (2 * j + 1) / (2 * j + 1) for j in range(terms)), Q(0)) + return s + z ** (2 * terms + 1) / ((2 * terms + 1) * (1 - z * z)) if upper else s + + +_LN = {} + + +def ln(x, upper): + """A rational bound on ln x for rational x >= 1: ln x = k ln 2 + ln y with 1 <= y < 2, ln y = 2 atanh((y-1)/(y+1)).""" + key = (x, upper) + if key not in _LN: + assert x >= 1 + y, k = x, 0 + while y >= 2: + y /= 2 + k += 1 + value = 2 * k * atanh(Q(1, 3), upper) + 2 * atanh((y - 1) / (y + 1), upper) + _LN[key] = up(value) if upper else down(value) + return _LN[key] + + +# ---------------------------------------------------------------------------------------------- the floor at one p +def floor_at(p): + h, m = 2 * p, 6 * p + v = 8 * comb(p, 3) + D = 2 * v - 3 * h * (h - 2) + lo = lambda r: r * ln(Q(m, r), False) # f(r) from below + hi = lambda r: r * ln(Q(m, r), True) # f(r) from above + col = 12 * (p - 3) + 12 * comb(p - 3, 2) + 8 * comb(p - 3, 3) + mu = 4 * (p - 3) + eps_lo, eps_hi = lo(1) + lo(h - 3) - hi(h - 2), hi(1) + hi(h - 3) - lo(h - 2) + delta_lo, delta_hi = lo(1) + lo(h - 2) - hi(h - 1), hi(1) + hi(h - 2) - lo(h - 1) + U2_lo, U2_hi = lo(3) + 3 * lo(1) + 3 * lo(h - 2), hi(3) + 3 * hi(1) + 3 * hi(h - 2) + idle = lo(3) + 3 * lo(h - 1) + rho_hi = U2_hi / mu + tau = min(6 * eps_lo, 3 * delta_lo + 3 * eps_lo - rho_hi) + n_g = v // col + # side conditions of PROOF.md, section 9 (each is also proved or explained there) + side = dict( + deficit_positive=D > 0, + widths_in_range=3 * (h - 1) < m and h - 4 >= 1, + gauge_at_a_line_is_cheaper=hi(3) <= 3 * lo(1), # g3 = min(3 f(1), f(3)) = f(3) + eps_below_f1=0 < eps_lo and eps_hi <= lo(1), # a non-unit T-register can pay 3 eps + rho_at_most_3eps=rho_hi <= 3 * eps_lo, # a target that pays rho twice + small_unit_net=U2_lo - 3 * eps_hi >= rho_hi, # one big unit: U2 + mu rho >= 2 U2 + no_big_unit=col >= 2 * mu, # no big unit: |col| rho >= 2 U2 + tau_positive=tau > 0, + ) + assert all(side.values()), (p, {k: ok for k, ok in side.items() if not ok}) + stars = 3 * h * lo(h - 2) + data_only = v * (6 * lo(h - 1) + 2 * lo(2)) + stars + ladder = [data_only] # no auxiliary registers + ladder.append(data_only + v * idle) # + one unit per source (Lemma E) + ladder.append(data_only + v * 2 * U2_lo) # + a second non-idle unit (Lemma D) + ladder.append(ladder[-1] + v * tau) # + T-registers or a stop of y_T (Lemma T) + ladder.append(ladder[-1] + (v - n_g) * (3 * lo(1) - hi(3))) # + source roles enter from 0 (Lemma E) + ladder.append(ladder[-1] + v * (3 * (lo(1) + lo(2) + lo(h - 4)) - 3 * hi(h - 1))) # + K itinerary (fixed) + return dict(p=p, h=h, m=m, v=v, D=D, col=col, mu=mu, n_g=n_g, ladder=ladder, C=ladder[-1], + per_port=dict(source_data=float(3 * (lo(1) + lo(2) + lo(h - 4))), target_data=float(3 * lo(h - 1) + 2 * lo(2)), + units=float(2 * U2_lo), tau=float(tau), source_entry=float((v - n_g) * (3 * lo(1) - hi(3)) / v), + stars=float(stars / v), eps=float(eps_lo), delta=float(delta_lo), U2=float(U2_lo), + rho=float(rho_hi))) + + +def ceil_grid(x, digits=7): + return -((-x.numerator * 10 ** digits) // x.denominator) + + +# ---------------------------------------------------------------------------------------------- counting lemmas +def brute(p, every_w): + """|col(S)|, Lemma S (rank h-1) and Lemma M (min over w of N(w) = 4(p-3)) for one source S, by enumeration. + With every_w, all 2^h - 2 vectors w are tried; otherwise one w from each orbit of the symmetries that fix S and + col(S): permutations of the free pairs and the swap of the two coordinates of a free pair.""" + P = [frozenset(2 * i + b for i, b in zip(I, bits)) for I in combinations(range(p), 3) for bits in product((0, 1), repeat=3)] + q = [sum(1 << c for c in S) for S in P] + cube = [frozenset(c // 2 for c in S) for S in P] + h, S0 = 2 * p, 0 + col = [t for t in range(len(P)) if cube[t] != cube[S0] and len(P[t] & P[S0]) in (0, 2)] + assert len(P) == 8 * comb(p, 3) + assert len(col) == 12 * (p - 3) + 12 * comb(p - 3, 2) + 8 * comb(p - 3, 3) + assert all((q[t] & q[S0]).bit_count() % 2 == 0 for t in col) + pivots = {} + for x in (q[t] for t in col): + while x: + top = x.bit_length() - 1 + if top not in pivots: + pivots[top] = x + break + x ^= pivots[top] + assert len(pivots) == h - 1, 'Lemma S' + qc = [q[t] for t in col] + if every_w: + ws = range(1, 1 << h) + else: + own = [c // 2 for c in sorted(P[S0])] + free = [i for i in range(p) if i not in own] + ws = [] + for bits in range(64): + base = sum(1 << (2 * own[k // 2] + k % 2) for k in range(6) if bits >> k & 1) + for one in range(len(free) + 1): + for both in range(len(free) + 1 - one): + w = base + for j, i in enumerate(free): + if j < one: + w |= 1 << (2 * i) + elif j < one + both: + w |= 3 << (2 * i) + ws.append(w) + least = min(sum((w & x).bit_count() & 1 for x in qc) for w in ws if w not in (0, q[S0])) + assert least == 4 * (p - 3), ('Lemma M', p, least) + return len(col), least + + +# ---------------------------------------------------------------------------------------------- main +def main(): + ap = argparse.ArgumentParser(description=__doc__, formatter_class=argparse.RawDescriptionHelpFormatter) + ap.add_argument('--check', action='store_true') + ap.add_argument('--brute', action='store_true') + a = ap.parse_args() + if a.brute: + for p, every in ((7, True), (8, True)) + tuple((p, False) for p in range(7, 17)): + n, least = brute(p, every) + log('p = %2d: |col| = %4d, span of col = q_S-perp, min N(w) = %d = 4(p-3) over %s w' % ( + p, n, least, 'every' if every else 'one per orbit of')) + log('PASS counting lemmas at small p') + return + rows = [floor_at(p) for p in range(P_MIN, P_MAX + 1)] + names = ('data registers and star copies only', '+ one unit per source', '+ a second non-idle unit per source', + '+ registers at each target hyperplane', '+ source roles enter from frame 0', + '+ K itinerary of the source registers') + ladder = [] + for k, name in enumerate(names): + best = max(rows, key=lambda r: Q(r['D']) / r['ladder'][k]) + ladder.append(dict(floor=name, p=best['p'], ceiling='%d/10^7' % ceil_grid(Q(best['D']) / best['ladder'][k]))) + log('%-40s a < %s (largest at p = %d)' % (name, ladder[-1]['ceiling'], best['p'])) + best = max(rows, key=lambda r: Q(r['D']) / r['C']) + a_max = Q(best['D']) / best['C'] + # tail: for every p >= 7, C > 9 v (h-1) ln 3 and D < 2v (PROOF.md, section 10), so a < 2 / ((18p - 9) ln 3) + tail = 2 / ((18 * (P_MAX + 1) - 9) * ln(Q(3), False)) + assert tail < a_max, 'the tail bound must lie below the maximum over the computed range' + kappa = a_max / (1 + a_max) + out = dict(p_range=[P_MIN, P_MAX], p=best['p'], h=best['h'], v=best['v'], D=best['D'], + ceiling_a='%d/10^7' % ceil_grid(a_max), ceiling_kappa='%d/10^7' % ceil_grid(kappa), + tail='%d/10^7' % ceil_grid(tail), ladder=ladder, + table={str(r['p']): '%d/10^7' % ceil_grid(Q(r['D']) / r['C']) for r in rows + if r['p'] in (7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 20, 30, 40, 60, 99)}) + log('side conditions hold at every p in %d..%d; tail for p >= %d: a < %s' % (P_MIN, P_MAX, P_MAX + 1, out['tail'])) + log('per port at p = %d: %s' % (best['p'], ', '.join('%s %.2f' % kv for kv in best['per_port'].items()))) + log('CEILING: a < %s and kappa < a/(1+a) < %s, for every word on the design at every p' % ( + out['ceiling_a'], out['ceiling_kappa'])) + if a.check: + expected = json.loads((HERE / 'expected.json').read_text()) + assert out == expected, 'results differ from expected.json' + log('PASS results equal expected.json') + print(json.dumps(out, indent=1, sort_keys=True)) + + +if __name__ == '__main__': + main() diff --git a/research/design-ceiling/expected.json b/research/design-ceiling/expected.json new file mode 100644 index 0000000000..4abfd03f6d --- /dev/null +++ b/research/design-ceiling/expected.json @@ -0,0 +1,62 @@ +{ + "D": 2704, + "ceiling_a": "25657/10^7", + "ceiling_kappa": "25592/10^7", + "h": 26, + "ladder": [ + { + "ceiling": "63627/10^7", + "floor": "data registers and star copies only", + "p": 12 + }, + { + "ceiling": "42121/10^7", + "floor": "+ one unit per source", + "p": 12 + }, + { + "ceiling": "29420/10^7", + "floor": "+ a second non-idle unit per source", + "p": 13 + }, + { + "ceiling": "27868/10^7", + "floor": "+ registers at each target hyperplane", + "p": 13 + }, + { + "ceiling": "27653/10^7", + "floor": "+ source roles enter from frame 0", + "p": 13 + }, + { + "ceiling": "25657/10^7", + "floor": "+ K itinerary of the source registers", + "p": 13 + } + ], + "p": 13, + "p_range": [ + 7, + 99 + ], + "table": { + "10": "23474/10^7", + "11": "24856/10^7", + "12": "25487/10^7", + "13": "25657/10^7", + "14": "25540/10^7", + "15": "25242/10^7", + "16": "24832/10^7", + "20": "22753/10^7", + "30": "17935/10^7", + "40": "14587/10^7", + "60": "10549/10^7", + "7": "7110/10^7", + "8": "16006/10^7", + "9": "20837/10^7", + "99": "6829/10^7" + }, + "tail": "10165/10^7", + "v": 2288 +} diff --git a/research/design-ceiling/model_check.py b/research/design-ceiling/model_check.py new file mode 100644 index 0000000000..54a5f65cab --- /dev/null +++ b/research/design-ceiling/model_check.py @@ -0,0 +1,252 @@ +#!/usr/bin/env python3 +"""Check the lemmas of PROOF.md on a certified word (Python stdlib only; sanity, not part of the proof). + +PROOF.md argues about every word on #144's paired-cube design through an abstraction: frame chains of physical +registers, units of a source, registers at a target's hyperplane. This script rebuilds that abstraction for one real +certified word, with the repository's own producer, and checks that + + 1. the abstraction is the word's ledger: the children it lists are the certified child histogram, exactly; + 2. Lemma E: every source role enters at frame 0 and steps to its own line; + 3. Lemma D: every target of col(S) is reached through the exit of a unit of S (or at the line), and every source + has two big units, or enough small units and line targets; + 4. Lemma T: every target has a register at its hyperplane, and two of them unless y_T has an intermediate stop; + 5. every unit, every source and every target pays at least the floor that the charging argument assigns to it, + and the certified cost is above the design floor C(p) of ceiling.py. + +Usage: python3 research/design-ceiling/model_check.py [--tree PATH] + --tree a checkout of this repository (default: the tree containing this script, whose scripts regenerate #144's + word at p = 12). A tree with scripts/paired_cube_physical.py is read with its frame layer, reuse pairs + and, if present, research/terminal-sinks. +""" +import argparse +import importlib +import json +import math +import sys +import tempfile +import time +from collections import Counter, defaultdict +from math import comb +from pathlib import Path + +if sys.flags.optimize: + raise SystemExit('Assertions must remain enabled: run without -O') + +HERE = Path(__file__).resolve().parent +T0 = time.time() + + +def log(*a): + print('[%4.0fs]' % (time.time() - T0), *a, flush=True) + + +def load(tree): + sys.path.insert(0, str(tree / 'scripts')) + cert = lambda name: json.loads((tree / 'certificates' / name).read_text()) + if (tree / 'scripts/paired_cube_physical.py').exists(): + PCP = importlib.import_module('paired_cube_physical') + g, witness, word, record = PCP.regenerated_word() + pairs = [(int(a), int(b)) for a, b, _ in json.loads((PCP.REF / 'pairs.json').read_text())['pairs']] + moved = {int(i): tuple(F) for i, F in json.loads((PCP.REF / 'frames.json').read_text())['frames']} + sink_file = tree / 'research/terminal-sinks/sinks.json' + sinks = {int(s): int(p) for s, p in json.loads(sink_file.read_text())['sinks']} if sink_file.exists() else {} + profile = cert('paired-cube-sinks-input.json' if sinks else 'paired-cube-physical-input.json') + return g, witness, word, record, pairs, moved, sinks, profile + producer = importlib.import_module('paired_cube_producer') + record = cert('paired-cube-complex-input.json') + with tempfile.TemporaryDirectory(prefix='design-ceiling-') as d: + producer.regenerate(record, Path(d)) + g, witness, word = (json.loads((Path(d) / n).read_text()) for n in ('graph.json', 'frames.json', 'selection.json')) + return g, witness, word, record, [], {}, {}, record + + +def main(): + ap = argparse.ArgumentParser(description=__doc__, formatter_class=argparse.RawDescriptionHelpFormatter) + ap.add_argument('--tree', type=Path, default=HERE.parents[1]) + tree = ap.parse_args().tree.resolve() + g, witness, word, record, pairs, moved, sinks, profile = load(tree) + from paired_cube.frames import basis, perp, contained + h, v, R = g['h'], g['v'], record['R'] + m, p = 3 * h, h // 2 + inputs = g['inputs'] + full = perp((), h) + f = lambda r: r * math.log(m / r) if r > 0 else 0.0 + args = [None] + [None if a is None else (a[0] + 1, a[1] + 1) for a in g['args']] + roots = [dict(r, node=r['node'] + 1) for r in g['roots']] + ops = [tuple(o) for o in word['ops']] + span = [()] * len(args) + for x in range(1, len(args)): + span[x] = (inputs[x - 1],) if args[x] is None else basis(span[args[x][0]] + span[args[x][1]]) + frame = [basis(moved[i]) if i in moved else perp(tuple(witness['annihilators'][x]), h) for i, (_, _, x) in enumerate(ops)] + source_of = {s: int(x) - 1 for x, s in word['sources'].items()} + gauge = {z['role']: perp(tuple(z['annihilator']), h) for z in word['selected']} + gauge_targets = {z['role']: z['targets'] for z in word['selected']} + root_frame, root_targets, star_dims = {}, {}, [] + for r, s in zip(roots, word['rootroles']): + if r['kind'] == 'center': + root_frame[s] = span[r['node']] + star_dims.append(len(root_frame[s])) + else: + root_frame[s] = perp(basis(inputs[t] for t in r['targets']), h) + root_targets[s] = list(r['targets']) + role_ops = defaultdict(list) + for i, (a, b, _) in enumerate(ops): + role_ops[a].append(i) + role_ops[b].append(i) + donors = {a for a, _ in pairs} + recipient_of = dict(pairs) + is_recipient = {b for _, b in pairs} + + # ---- physical auxiliary registers: one ascending chain of frames per stage (PROOF.md, section 2.3) + slots, children = {}, Counter() + for s in range(R): + if s in is_recipient or s in sinks: + continue + chain, merged = [()], 0 + for k, u in enumerate([s] + ([recipient_of[s]] if s in donors else [])): + if k == 0 and u in source_of: + chain.append((inputs[source_of[u]],)) # injection at the source line + elif k == 0 and u in gauge: + chain, merged = [gauge[u]], len(gauge[u]) # entrance gauge: one merged child of width 3 dim + elif k > 0: + chain.append(gauge[u]) # hand-off into the recipient's gauge + chain.extend(frame[i] for i in role_ops[u]) + if u in root_frame: + chain.append(root_frame[u]) + chain.append(full) + stops = [chain[0]] + for F in chain[1:]: + assert contained(stops[-1], F), 'a register chain does not ascend' + if len(F) > len(stops[-1]): + stops.append(F) + steps = [len(b) - len(a) for a, b in zip(stops, stops[1:])] + for r in steps: + children[r] += 3 + if merged: + children[3 * merged] += 1 + slots[s] = dict(stops=stops, cost=(f(3 * merged) if merged else 0.0) + 3 * sum(f(r) for r in steps)) + # ---- target registers: the frames at which the auxiliary word uses y_T + y_stops = [set() for _ in range(v)] + sink_groups = [] + for s, targets in gauge_targets.items(): + for t in targets: + y_stops[t].add(gauge[s]) + for s, targets in root_targets.items(): + if s in sinks: + pivot, U = sinks[s], root_frame[s] + for i in role_ops[s]: + assert ops[i][0] == s, 'a sink is written only as a destination' + y_stops[pivot].add(frame[i]) + others = [t for t in targets if t != pivot] + for t in others: + y_stops[t].add(U) + y_stops[pivot].add(U) + sink_groups.append((pivot, U, others)) + else: + for t in targets: + y_stops[t].add(root_frame[s]) + line = [(q,) for q in inputs] + hyper = [perp((q,), h) for q in inputs] + y_cost = [] + for t in range(v): + st = sorted(y_stops[t], key=len) + assert all(contained(a, b) for a, b in zip(st, st[1:])) and all(contained(F, hyper[t]) for F in st) + dims = sorted({0, h - 1} | {len(F) for F in st}) + steps = [b - a for a, b in zip(dims, dims[1:])] + for r in steps: + children[r] += 3 + y_cost.append(3 * sum(f(r) for r in steps)) + for r in (1, 2, h - 4): # source registers: the K itinerary + children[r] += 3 * v + children[2] += 2 * v # endpoint children + for r in star_dims: + children[r] += 3 # star copies + certified = {int(r): n for r, n in profile['child_histogram'].items() if n} + assert dict(children) == certified, 'the abstraction differs from the certified child histogram' + C = sum(n * f(r) for r, n in certified.items()) + log('%s at p = %d: %d physical auxiliary registers, %d reuse pairs, %d sinks' % ( + 'frame-layer word' if moved or pairs else 'gauged word', p, len(slots), len(pairs), len(sinks))) + log('1. the abstraction lists exactly the certified children (C = %.0f)' % C) + + # ---- Lemma E + for s, t in source_of.items(): + stops = slots[s]['stops'] + assert stops[0] == () and stops[1] == line[t], 'a source role does not step from 0 to its own line' + log('2. Lemma E: every source role enters at frame 0 and steps to its own line') + + # ---- units, T-registers, Lemma D + line_index = {line[t]: t for t in range(v)} + hyper_index = {hyper[t]: t for t in range(v)} + units, t_registers = defaultdict(list), defaultdict(list) + for s, d in slots.items(): + for k, F in enumerate(d['stops']): + if len(F) == 1 and F in line_index: + units[line_index[F]].append((s, d['stops'][k + 1])) + if len(F) == h - 1 and F in hyper_index: + t_registers[hyper_index[F]].append(s) + labels = [frozenset(l) for l in g['labels']] + cube = [frozenset(c // 2 for c in l) for l in labels] + mu, ncol = 4 * (p - 3), 12 * (p - 3) + 12 * comb(p - 3, 2) + 8 * comb(p - 3, 3) + orthogonal = lambda F, q: all((x & q).bit_count() % 2 == 0 for x in F) + U2 = f(3) + 3 * f(1) + 3 * f(h - 2) + idle = f(3) + 3 * f(h - 1) + eps, delta = f(1) + f(h - 3) - f(h - 2), f(1) + f(h - 2) - f(h - 1) + rho = U2 / mu + tau = min(6 * eps, 3 * delta + 3 * eps - rho) + at_hyperplane = {s for regs in t_registers.values() for s in regs} + kinds, unit_costs, payers = Counter(), [], defaultdict(set) + for S in range(v): + col = [T for T in range(v) if cube[T] != cube[S] and len(labels[T] & labels[S]) in (0, 2)] + assert len(col) == ncol + at_line = {T for T in col if line[S] in y_stops[T]} # L(S): line targets + for pivot, U, others in sink_groups: # L(S): pivot targets + if line[S] in y_stops[pivot] and contained(line[S], U): + at_line.update(T for T in others if T in col) + for T in at_line: + payers[T].add(S) + big = [F for _, F in units[S] if 2 <= len(F) <= h - 2] + small = [F for _, F in units[S] if len(F) == h - 1] + kinds.update(big=len(big), small=len(small), idle=len(units[S]) - len(big) - len(small)) + reached = set(at_line) + for F in big + small: + reached.update(T for T in col if orthogonal(F, inputs[T])) + assert reached >= set(col), 'a target of col(S) is not reached through a unit exit' + assert len(big) >= 2 or (len(big) == 1 and len(at_line) + len(small) >= mu) or \ + (not big and len(at_line) + len(small) >= ncol), 'Lemma D' + total = 0.0 + for s, F in units[S]: + floor = idle if len(F) == h else U2 + (3 * eps if s in at_hyperplane and len(F) < h - 1 else 0.0) + assert slots[s]['cost'] >= floor - 1e-9, 'a unit costs less than its floor' + total += slots[s]['cost'] + assert total >= 2 * U2 + 3 * math.log(3) - 1e-9, 'a source pays less than two units' + unit_costs.append(total) + log('3. Lemma D: %d units (%s); every target of col(S) is reached through a unit exit; unit cost per source ' + 'min %.1f, mean %.1f, floor %.1f' % (sum(kinds.values()), ', '.join('%d %s' % (n, k) for k, n in sorted(kinds.items())), + min(unit_costs), sum(unit_costs) / v, 2 * U2 + 3 * math.log(3))) + + # ---- Lemma T and the target side of the charging argument + plain = 0 + for T in range(v): + between = [F for F in y_stops[T] if F and F != hyper[T]] + n = len(t_registers[T]) + assert n >= 1 and (n >= 2 or between), 'Lemma T' + plain += not between + assert len(payers[T]) <= 2 + received = y_cost[T] - 3 * f(h - 1) + 3 * eps * min(n, 2) - rho * len(payers[T]) + assert received >= tau - 1e-9, 'a target collects less than tau' + spread = Counter(len(t_registers[T]) for T in range(v)) + log('4. Lemma T: registers at a target hyperplane per target: %s; %d targets without an intermediate stop' % ( + dict(sorted(spread.items())), plain)) + + # ---- the design floor of ceiling.py at this p (floats; ceiling.py has the exact version) + D = 2 * v - 3 * record['loss'] + floor = v * (3 * (f(1) + f(2) + f(h - 4)) + 3 * f(h - 1) + 2 * f(2) + 2 * U2 + tau) \ + + (v - v // ncol) * (3 * f(1) - f(3)) + 3 * h * f(h - 2) + assert D == profile['deficit_per_vertex'] and C >= floor + log('5. certified cost %.0f >= design floor %.0f (%.1f%% of it); D/C = %.4e, D/floor = %.4e' % ( + C, floor, 100 * floor / C, D / C, D / floor)) + log('PASS the lemmas hold on this word') + + +if __name__ == '__main__': + main()