# RUN-020 — Round 17: the D3 quotient is exact and every run rebuilds; the quotient's gain is understated, and the tail window's edge comes from a changed override rule, not from starting at depth 10

**Arm:** 懸衡 (Xuán Héng) / AMRAL Research Lab
**Date:** 2026-09-25
**Subject:** `AMRAL_Lebesgue_Finite_Closure_Round_17_D3_CPG_v0.1.md` (AMRAL-LUC-FC-R17, dated 2026-09-19) and its package, read from the archive:

- `PILOT_SUMMARY.json`, `PRODUCTION_SCHEDULER_SPEC.json`, `VALIDATION.json`, `State_Crystal`;
- the reference directory: its copy of the summary, `pilot_stdout.json`, `tail_window_probe.json`;
- `round17_symmetry_cpg_pilot.py`, `tail_window_probe.py` and `round16_base_pilot.py`, read only after this tree's reconstruction, and never run;
- a compiled `.pyc` of the last, whose header only was read.

**Tools:** [`run020_round17_d3_cpg.py`](../code/run020_round17_d3_cpg.py) — the group and the wedge; ten D3 trees (the official split and the CPG variants, sampled and exact, and one rule changed at a time); RUN-019's pilot routes and its full-root trees
**Logs:** [`run020-round17-d3-cpg.json`](../data/gate-logs/run020-round17-d3-cpg.json)

**Verdict: PASS for the quotient and the pilot's computations; PARTIAL for the tail-window recommendation.**

- **The D3 quotient is exact.**
  - On configurations, the 2π/3 turn `r` and the mirror `s` satisfy `r³ = s² = e` and
    `srs = r⁻¹`, and the exact hull area is invariant under both, to 10⁻¹⁵.
  - Every one of 4,007 configurations (random ones, the wedge's edges and their
    images, and `t₃ = 0`) has an image with `0 ≤ arg t₃ ≤ π/3`. That image lies in
    the D3 root box, and `SYM` does not prune it.
  - The proof needs the a-priori exclusion `|t₅| ≤ t₅(0.8365)`, which the text calls
    radial legality. Take `t₅` at a corner of its square and `arg t₃ = 153°`: the
    representative turns `t₅` to `y₅ = −0.277`, outside the square's `±0.203`. So the
    quotient root inherits that exclusion's capacity, 0.8365.
  - Mishra's `q†` has its representative `sRq†` 3.05×10⁻⁶ inside the wedge's edge. It
    lies in a HARD cell of both D3 trees, as it must.
- **Every run rebuilds — the scheduler runs only with rules the code adds.**
  - The D3 official tree agrees in every count (12,357 nodes, 109 SYM, 3,304 CORE,
    2,766 HARD, 12,248 evaluations). So do the four CPG runs and the tail probe
    (nodes, evaluations, SYM, CORE, HARD, overrides).
  - Three rules are the code's, not the text's:
    - a 10⁻¹⁵ margin on `SYM`. Without it, full CPG at depth 14 has 2,943 nodes, not
      2,975.
    - the windowed CPG overrides on any better key, even when no child is certified.
    - both windows stop at the first axis that certifies both children.
- **The quotient's gain is understated.**
  - The D3 root is 4.6 times smaller by volume, so its depth-16 cells are the full
    root's depth-18 cells: the same `τ = 0.0385532`, and only `y₃` is 13% narrower.
  - At that equal cell size the quotient removes **72.9% of nodes and 73.5% of HARD
    leaves** (73.8% and 74.7% with exact cores). Round 17 compared equal depths and
    reported 47.3% and 32.7%.
- **The tail window's edge is misattributed.**
  - §13 presents the tail window as §10's windowed CPG started at depth 10. The code,
    and the production spec, also change the override rule: an alternate axis wins only
    if it certifies a child.
  - Changing one thing at a time:
    - the rule change cuts overrides from 1,608 to 404 and costs HARD leaves (1,862 →
      2,047);
    - starting at depth 10 rather than at the root makes nodes, evaluations, overrides
      and HARD leaves all worse, under either rule.
  - The pilot supports the certifying rule from the root. It does not support
    `activation_depth = 10`.
  - With exact cores the tail window still beats the official split (8,947 nodes and
    1,909 HARD against 10,967 and 2,339).
- **One stored conclusion contradicts its own data.**
  - The summary says windowing "retained the depth-14 HARD count of full CPG". Its own
    `same_hard_count` is `false`: 863 against 1,210.
  - The sentence is a fixed string in the pilot's code. The text (§11) says it right.
- **The package, otherwise, holds together.**
  - The summary is the pilot's stdout, plus the tail probe's blocks and a seventh
    conclusion added by hand.
  - `round16_base_pilot.py` is Round 16's code, and ships with its CPython 3.13 `.pyc`.
  - The pilot reads its Round 16 baseline from a path outside the package, so it does
    not run as shipped.
  - VALIDATION's digests and key results are right.
- **Reading Round 17 also exposed two blind spots in this tree's status census.**
  - The census v3 correction (commit `749d9ca`) reads both. It adds 18 judgments to the
    registry, 10 of them Round 17's.

Drill: 18 / 18 plants caught by exactly the named checks, 4 / 4 controls undisturbed,
176 / 176 must-stay-green assertions held. Each of the nine checks was blinded in turn,
and each was reported blind in exactly as many cases as plants name it.

---

## What Round 17 claims

1. **Residual symmetry** (§1–2). With the disc at the origin and `B₃`'s orientation
   fixed, the area is invariant under:
   - the 2π/3 turn `t₃ ↦ Rt₃, t₅ ↦ Rt₅, φ₅ ↦ φ₅ + 2π/3 (mod 2π/5)`;
   - the mirror `y ↦ −y, φ₅ ↦ −φ₅`.

   Together they form `G ≅ D₃`.
2. **The canonical wedge** (§3–4, Thm 3.1).
   - Every orbit has a representative with `0 ≤ arg t₃ ≤ π/3`.
   - The enclosing rectangle is `0 ≤ x₃ ≤ t₃⋆`, `0 ≤ y₃ ≤ (√3/2) t₃⋆`.
   - A cell with `y₃⁻ > √3 x₃⁺` is pruned as `SYM`, a quotient leaf, not a
     lower-bound leaf.
3. **A sanity check** (§5). With 120 directions, 20 samples move by at most 6.66×10⁻¹⁶
   under the mirror and 8.88×10⁻¹⁶ under the turn.
4. **The D3 pilot** (§6). At depth 16, 12,357 nodes and 2,766 HARD, against the full
   root's 23,455 and 4,112: 47.32% and 32.73% fewer.
5. **Schedulers** (§7–14).
   - Split choice never affects soundness.
   - CPG: `P(a)` = the children certified, with ties broken by `min(L₋, L₊)`,
     `L₋ + L₊`, the child radius, then the axis.
   - Unrestricted CPG is myopic.
   - A window `L(C) ≥ T − 0.025` when the official split certifies nothing.
   - At depth 16 the window gives 8,625 / 1,862, 1.82 times the evaluations.
   - From depth 10 only, it gives 9,997 / 2,048 with 10.72% overrides and 2.02 times
     the evaluations: "the most balanced production candidate".
6. **Certificate semantics** (§15–17).
   - The official axis is implicit, and sparse overrides take 2 bits.
   - The group, the wedge, `SYM` and child coverage are theorem-critical. The window,
     the activation depth and the codec are performance-only.
7. **Deferred work and Round 18** (§18–21).

## A — sources

**A0.** 49 anchors. Round 17 has no reference list.

## W — rebuilt

| check | Round 17 | rebuilt | result |
| --- | --- | --- | --- |
| W1 | §1–2, §5 | the relations; the area's invariance, exact and sampled | PASS |
| W2 | §3–4 | the wedge on 4,007 configurations; `q†`'s representative | PASS; needs `\|t₅\| ≤ t₅⋆` |
| W3 | §6 | the D3 official tree, sampled and exact; equal cell size | PASS; the gain is ~73% |
| W4 | §8–13 | the CPG runs; one rule changed at a time | PASS as computed; depth 10 is not supported |
| W5 | §11–15 | every stored fraction and factor from its counts | PASS |

**W1 — the group.**

- On 40 random configurations of the full root, `r³`, `s²` and `srs·r` return the
  configuration to 6.7×10⁻¹⁶, with `φ₅` compared round its circle.
- The exact hull area (RUN-009's, through RUN-019) moves by at most 1.0×10⁻¹⁵ under
  either map.
- Sampled hulls:

  | directions | mirror | turn |
  | ---: | ---: | ---: |
  | 120 | 6.7×10⁻¹⁶ | 7.8×10⁻¹⁶ |
  | 40 (the pilot's) | 6.7×10⁻¹⁶ | **1.1×10⁻³** |

- 120 directions, in steps of 3°, are carried to themselves by 120°; 40, in steps of 9°,
  are not. So §5's sanity check is right to change grids.
- It also means the pilot's own bound is not turn-invariant. That does not touch
  soundness: the quotient theorem is about the exact area, and any valid lower bound
  may be used on the canonical domain.

**W2 — the wedge.**

- The six images of a configuration turn `arg t₃` by multiples of 120° and reflect
  it, so one lands in any 60° sector bounded by two mirror lines, such as `[0°, 60°]`.
- 4,000 random configurations, uniform in the discs `|t₃| ≤ t₃⋆` and `|t₅| ≤ t₅⋆`,
  plus the six edge directions and `t₃ = 0`, each have a representative:
  - with `0 ≤ arg t₃ ≤ π/3`;
  - inside the D3 root box, with `φ₅ ∈ [0, 2π/5)`;
  - with `|t₅|` unchanged;
  - on the kept side of `y₃ = √3 x₃`.
- **The box needs the disc.** The representative keeps `|t₅|`, not the square. At
  `t₅ = (t₅⋆, t₅⋆)`, a corner of the full root's square, with `arg t₃ = 153°`, the
  representative is `r²`, and it turns `t₅` to `(0.074, −0.277)`: outside the square.
  Configurations with `|t₅| > t₅⋆` are excluded a priori (area above 0.8365), so the
  quotient root is sound up to 0.8365, and no further, as RUN-018 found for the lift
  roots.
- **`SYM`** prunes a cell whose lowest `y₃` exceeds `√3` times its largest `x₃`. Every
  point of such a cell has `arg t₃ > π/3`.
  - The code's 10⁻¹⁵ margin keeps the dyadic cells whose corner lies exactly on the
    edge.
  - Pruning them would also be sound, since a neighbour covers the corner, but it
    changes the counts (W4).
- **Mishra's seed.** `q†` has `arg t₃ = −π + 3.05×10⁻⁶`, so `r²q†` sits 3.05×10⁻⁶
  *outside* the wedge's upper edge and its mirror `sRq†` 3.05×10⁻⁶ inside. That
  representative's depth-16 cell, `0001110001100111`, is HARD in the sampled and the
  exact D3 tree.

**W3 — the D3 pilot.**

- The sampled tree (RUN-019's route evaluation, `SYM` first) agrees with the summary in
  every count: 12,357 nodes, 12,248 evaluations, 109 SYM, 3,304 CORE and 2,766 HARD.
- With exact cores: 10,967 nodes, 100 SYM, 3,045 CORE and 2,339 HARD.
- **Equal cell size.** The D3 root box has 21.65% of the full root's volume, about 2.2
  bisections less, so the same depth means smaller cells.

  | | `x₃` | `y₃` | `φ₅` | `x₅, y₅` | `τ` |
  | --- | ---: | ---: | ---: | ---: | ---: |
  | D3 root, depth 16 | 0.025128 | 0.021761 | 0.039270 | 0.012664 | 0.0385532 |
  | full root, depth 18 | 0.025128 | 0.025128 | 0.039270 | 0.012664 | 0.0385532 |

  Against RUN-019's full-root trees at depth 18:

  | | full, depth 18 | D3, depth 16 | fewer |
  | --- | ---: | ---: | ---: |
  | nodes, sampled | 45,651 | 12,357 | **72.9%** |
  | HARD, sampled | 10,448 | 2,766 | **73.5%** |
  | nodes, exact cores | 41,899 | 10,967 | 73.8% |
  | HARD, exact cores | 9,234 | 2,339 | 74.7% |

- An ideal quotient would keep one sixth. The rectangle and the cells straddling the
  edge keep a little more than a quarter.
- Round 17's comparison at equal depth, 47.32% and 32.73%, sets the D3 tree's finer
  cells against coarser ones.

**W4 — the schedulers.** Rebuilt from the text alone, the runs do not all agree with the
package. The text settles three things only loosely:

- a cell touching the wedge's edge at a corner;
- what a window does when no alternate axis certifies a child;
- when the search over axes stops.

The code, read after the reconstruction, settles them:

- `SYM` carries a 10⁻¹⁵ margin;
- the windowed CPG replaces the official axis whenever an alternate's key
  `(certified, min L, L₋ + L₊, −τ, −axis)` is larger, certified or not;
- the tail probe replaces it only with an axis that certifies a child, on the key
  `(certified, min L, L₋ + L₊)`;
- both windows stop at the first axis certifying two children.

With these rules every run agrees with the package:

| run | nodes | evaluations | SYM | CORE | HARD | overrides |
| --- | ---: | ---: | ---: | ---: | ---: | ---: |
| official, depth 16 | 12,357 | 12,248 | 109 | 3,304 | 2,766 | 0 |
| full CPG, depth 14 | 2,975 | 14,719 | 76 | 202 | 1,210 | 1,486 |
| windowed, depth 14 | 4,173 | 8,424 | 19 | 1,205 | 863 | 423 |
| windowed, depth 16 | 8,625 | 22,266 | 108 | 2,343 | 1,862 | 1,608 |
| tail window, depth 16 | 9,997 | 24,718 | 69 | 2,882 | 2,048 | 536 |
| *full CPG without the margin* | *2,943* | *14,581* | *70* | *200* | *1,202* | *1,470* |

**One change at a time** (depth 16, the pilot's sampling):

| override rule | from the root | from depth 10 |
| --- | --- | --- |
| any better key (§12's windowed CPG) | 8,625 / 1,862 HARD / 22,266 eval / 1,608 overrides | 9,799 / 1,863 / 24,206 / 1,740 |
| certify a child (§13's tail window) | 8,823 / 2,047 / 22,778 / 404 | 9,997 / 2,048 / 24,718 / 536 |

- Along a row, starting at depth 10 is worse on every count.
- Down a column, the certifying rule costs 185 more HARD leaves and saves 69–75% of the
  overrides.
- §13's comparison moves along the diagonal, and its low override density belongs to
  the rule. The pilot's best balance is the certifying rule from the root: 404
  overrides (9.2% of internal nodes) and 22,778 evaluations (1.86 times official).

With exact cores the tail window keeps its lead over the official split: 8,947 nodes and
1,909 HARD against 10,967 and 2,339, with 465 overrides.

**W5 — the numbers.**

- Every fraction and factor the summary stores is its own counts' arithmetic, to
  10⁻¹⁵:
  - the reductions;
  - the evaluation and wall-time factors;
  - the depth-14 comparisons;
  - the override fractions;
  - the idealized entropy bits, `N + H(f)·internal + 2·overrides`.
- The text rounds them correctly: 47.32, 32.73, 30.20, 32.68, 19.10, 25.96, 42.77,
  42.45 and 10.72%, and 1.82 and 2.02 times.
- Four override axes take `⌈log₂ 4⌉ = 2` bits, as §15 says.

## P — the package

**P1.**

- The summary is the reference directory's copy.
- It is the pilot's stdout plus `tail_window_depth16`, `tail_window_vs_d3_official`
  and a seventh conclusion. The tail probe's file is that block.
- The scheduler spec's `γ = 0.025`, activation depth 10, gate and root semantics are
  the summary's.
- The crystal carries the same numbers.
- The fourth stored conclusion, "Windowing CPG … retained the depth-14 HARD count of
  full CPG", sits beside `"same_hard_count": false` (863 against 1,210).

**P2.**

- `VALIDATION.json` describes the document and the crystal correctly: SHA-256, bytes,
  `$$` 126 and 20, the two flags.
- Its digests of the summary, the spec, the pilot and the tail probe are the archive's,
  and its key results are the summary's.

**The reference code, read after the reconstruction.**

- `round16_base_pilot.py` is byte-identical to Round 16's `global_pilot.py`. Beside it
  sits `__pycache__/round16_base_pilot.cpython-313.pyc`, a compiled copy (magic
  `f30d0d0a`, source size 13,616, which is the shipped file's).
- `round17_symmetry_cpg_pilot.py` loads the Round 16 full-root baseline from an
  absolute path outside the package, so it does not run as shipped.
- Its conclusions are fixed strings. The fourth is the one that contradicts the data
  beside it.

## Round 17, read

| Round 17 | statement | verdict | note |
| --- | --- | --- | --- |
| §1–2 | the residual group is `D₃` | PASS | W1 |
| §3, Thm 3.1 | every orbit meets the 60° wedge | PASS | W2; it rests on `\|t₅\| ≤ t₅⋆`, so the root's capacity is 0.8365 |
| §4 | the rectangle; `SYM` | PASS | W2; the code adds a 10⁻¹⁵ margin (W4) |
| §5 | symmetry sanity | PASS | W1; the pilot's own 40 directions are not turn-invariant |
| §6 | 47.32% / 32.73% fewer at depth 16 | PASS as arithmetic | W3: at equal cell size, 72.9% / 73.5% |
| §7 | split choice is proof-irrelevant | PASS | a cover of the parent by the children is all a verifier needs |
| §8–9 | CPG; unrestricted CPG is myopic | PASS | W4, with the code's margin |
| §10–12 | the window; depth 14 and 16 | PASS | W4; its override rule is not the spec's |
| §13 | tail-only from depth 10 is the best balance | PARTIAL | W4: the gain is the rule's; depth 10 is worse under either rule |
| §14 | emit against replay cost | PASS | as design; the factors are W5's |
| §15 | sparse override, 2 bits | PASS | W5 |
| §16–17 | theorem-critical against performance-only; the stack | PASS | the quotient root's capacity belongs on the theorem-critical side |
| §18–21 | deferred work; Round 18; checklist; handoff | n/a | the checklist is reviewed in the registry |

## The status registry

Round 17's 12 judgments are reviewed, and its 6 first-used phrases defined:
`MISHRA-FIRST-ORDER`, `PILOT-PASS`, `PILOT-PASS / PRODUCTION CANDIDATE`,
`PILOT-RECOMMENDED`, `STILL OPEN / COMPUTE-DEFERRED` and `SYM`.

- Ten of the 12 are found by census v3 only: §0's boxed `D_3` quotient and §20's nine
  checklist lines.
- The two PARTIALs are "TAIL-WINDOW CPG: PILOT-RECOMMENDED" and "Tail-window CPG:
  PILOT-PASS / PRODUCTION CANDIDATE". The runs rebuild, but the case for starting at
  depth 10 does not.

| verdict | judgments |
| --- | ---: |
| PASS | 8 |
| PARTIAL | 2 |
| n/a | 2 |

## The drill

| kind | cases | named checks |
| --- | ---: | --- |
| the document's D3 node count | 1 | A0 |
| a turn that leaves `φ₅` alone; the 40-direction bound called turn-invariant | 2 | W1 |
| the wedge said to need no exclusion; `q†`'s representative said closed | 2 | W2 |
| a D3 node count in the summary | 1 | W3, W5, P1 |
| the exact tree's HARD count; the equal-depth reduction taken for the equal-size one | 2 | W3 |
| an override count in the tail probe | 1 | W4, P1 |
| the margin said immaterial; depth 10 said to help; the tail window said to lose with exact cores | 3 | W4 |
| a stored fraction in the summary | 1 | W5, P1 |
| the spec's `γ`; the stored conclusion said consistent | 2 | P1 |
| the pilot's recorded digest; the pilot said self-contained | 2 | P2 |
| a review dropped | 1 | R1 |

Four controls:

- the unmodified inputs;
- the document with CRLF line endings;
- the turn taken as 8π/3;
- the wedge found with a looser slack.

**18 / 18 plants, 4 / 4 controls, 176 / 176 must-stay-green assertions; no check
without a plant.**

| check blinded | cases reported blind | plants naming it |
| --- | ---: | ---: |
| A0 | 1 | 1 |
| W1 | 2 | 2 |
| W2 | 2 | 2 |
| W3 | 3 | 3 |
| W4 | 4 | 4 |
| W5 | 2 | 2 |
| P1 | 5 | 5 |
| P2 | 2 | 2 |
| R1 | 1 | 1 |

## What this round does not establish

- **Any bound.** The trees are floating-point pilots, as Round 17's are.
- **The schedulers beyond depth 16.** The 2×2 comparison is the pilot's own setting.
  Deeper, or on real tail shards, the activation depth may matter differently. §18
  plans that recalibration; nothing here anticipates it.
- **A quotient by the turn on the grid.** `SYM` quotients by the wedge. The turn maps
  no axis-aligned grid onto itself (RUN-019), so cells are not paired as they are
  under the mirror.