# Wallis sieve - 2026-09-06 [Proved] The solid Wallis sieve, which drops the centre cube of every surviving cube cut into `(2k+1)^3` at level `k`, keeps the limit volume `prod_{n odd >= 3} (1 - n^(-3)) = pi^(3/2) / (8 |Gamma(7/4 - i sqrt(3)/4)|^2) = 0.948815486`, by the Weierstrass product for `1/Gamma` after `m^3 - 1 = (m - 1)(m - w)(m - w^2)` turns the `k`-th factor into `k (k + (1 - w)/2)(k + (1 - w^2)/2) / (k + 1/2)^3` with the three shifts summing to `3/2`; the plane sieve's limit area is Wallis's `pi/4`. Witness: `mrlynum::sieve::solid_limit`, evaluated by the log series to one ulp of `0.9488154857196796`, checked against the truncated product to `1e-14` and against the ratio form `cosh(pi sqrt(3)/2) / (3 pi)` over the even product. - 2026-09-06 [Proved] The Wallis sieve is a mixed-radix schedule word: letter `k` is the side-`(2k+1)` tile with its centre cell removed, the word is their Kronecker fold, and the word's fill is the product of the letters' fills exactly, so any odd schedule in any dimension is a sieve with area the product of its letters' survival ratios. Witness: `mrlynum::sieve::ratio`, the raster count against the product at levels 1 to 3 in both schedules. - 2026-09-06 [Proved] A schedule of distinct odd letters buys area and a constant one buys a dimension: with strictly increasing odd sides `sum s_k^(-dim)` converges, the limit area is positive and the odd word's fill exponent `dim + log(ratio_level) / log(side_level)` walks up to `dim` (`1.972027` at plane level 4), while the constant side-`s` word's stands at `log(s^dim - 1) / log s` forever (`log 8 / log 3 = 1.892789` for the carpet); a schedule that merely varies, `3, 5, 3, 5, ...`, loses its area and holds `log 192 / log 15 = 1.941432`. Witness: `mrlynum::sieve::exponent`. - 2026-09-06 [Verified] The plane sieve's truncated product reads `0.785398262` at two million factors against `pi/4 = 0.785398163`, the identity being Wallis's. Witness: `mrlynum::sieve::ratio`, the test that pins its nine-digit rounding.