# Sponge Tube

- The Menger sponge through Kombrink, Pearse and Winter 2016, Corollary 3.2, with the open unit cube as the feasible open set: `p(eps) = eps^(D-3) (20/27 + sum_(l >= 0) (27/20)^l T(eps/3^l))` for `eps in (sqrt(2)/18, 1/6]`, where `T(delta)` is the volume of the sponge's `delta`-neighbourhood inside the plus of seven removed cubes and `D = log 20 / log 3`.
- `T(delta)` on `(0, 1/6]` in closed form: the centre cube's edge tube `pi delta^2 - 8 sqrt(2) delta^3`, and per arm four wall carpets, `T = pi delta^2 - 8 sqrt(2) delta^3 + 8 delta^2 + 48 (V1 - A1) - 24 Deep`, with `V1` half the wall's integral of `sqrt(delta^2 - d^2)` over the carpet's holes, `A1` the same integral over the strip within `delta` of the wall's edge, both hole sums of arcsine closed forms with a proved geometric tail, and `Deep` the volume of the set deep in holes of two perpendicular walls at once, bounded above by an enumeration of hole pairs to level 7 and a counting bound beyond.
- Every printed interval is an enclosure: the closed forms run in mpmath interval arithmetic at 133 bits (`sqrt`, `pi`, `atan2` for the arcsine, `exp` and `log` for the power), the truncation tails of the level sums, the `Deep` bound and the tail of the criterion's series over levels above 40 are exact rationals added to the endpoints, and the script asserts the hard bounds `V1 <= delta/18` and `A1 <= delta^2/3` at every radius; the raster is a float check only. mpmath's interval `+ - * / sqrt` and integer powers are exactly directed, while `pi`, `atan2`, `exp` and `log` are guard-bit approximations rounded outward, a drift below `1e-30` absorbed by the printed rounding of at least `5.6e-9`.
- A raster check: distances from the wall carpets and the centre edges on `120^3` cells per cube, bracketed by the half diagonal, contain the closed form at `delta = 1/8` and `1/12`.
- `checks.py` is the second verb: four independent checks of the lemmas and the certificate, none part of it, each printing its own numbers: `oracle` (exact distances to the level-4 prefractal through a KD-tree with a completeness test, against the 24 level-4 wall carpets and against the own-walls or centre-edges reduction), `montecarlo` (seeded Monte Carlo of `T` at three radii through the reduced distance, a lemma-free bracket of `T` from the prefractal, and `V2` at `1/12`), `seeded` (Monte Carlo of `Deep` on its confinement box and of `V2` at `1/6` and `1/8`, seed 20260921), `recompute` (the tube, the `Deep` bound and the three bands from the closed forms of the paper at 60 digits with their own column recursion, hole integrals checked against quadrature, plus `V1` and `A1` at `1/12` at 200 digits with the naive `a1` and on a `3000^2` midpoint grid).

## RUN

- `uv run python mrlyprod/research/lab/py/sponge-tube/sponge_tube.py`
- About 46 to 50 seconds; prints only, writes nothing, asserts the raster brackets and the positive gap.
- `uv run python mrlyprod/research/lab/py/sponge-tube/checks.py` runs the four checks, about 125 seconds in all: `oracle` 4 s, `montecarlo` 82 s, `seeded` 29 s, `recompute` 9 s; append one name for one check. Needs numpy, scipy and mpmath; prints only, writes nothing.

## WITNESSES

- dimensions.md, section "The sponge, through the criterion without pluriphase": `T(1/8)` in `[0.234186414, 0.234701259]` and `T(1/12)` in `[0.180947086, 0.180947093]`, raster bands `[0.23229, 0.23708]` and `[0.17665, 0.18531]`; `T(1/6) = (pi + 8)/36 - sqrt(2)/27 - 24 Deep` in `[0.256188319, 0.257110405]`.
- The same section: `p(1/12)` in `[2.122718, 2.122723]`, `p(1/8)` in `[2.134668, 2.135742]`, `p(1/6)` in `[2.135019, 2.136794]`, `p(1/6) - p(1/12) >= 0.012296`, relative swing at least `0.5792 %`, the `Deep` bound `3.84e-5` at `delta = 1/6`, `2.15e-5` at `delta = 1/8` and `2.42e-10` at `delta = 1/12`.
- The paper `papers/sponge-measurability.md`, Fact 4.4 and Fact 5.3: the same bands; its Section 6, every number: `checks.py oracle` prints `160000` cubes, `12288` wall faces, `22844` points with `2844` near a face, the differences `0.0` and `2.8e-17`, and the centre distance to `8.3e-17`; `checks.py montecarlo` prints the brackets `[0.23190, 0.23467]` and `[0.17601, 0.18090]` at `1e6` points, `T(1/12) = 0.180952 +- 0.000056`, `T(1/8) = 0.234691 +- 0.000036`, `T(1/6) = 0.257060 +- 0.000011` at `4e7` points, and `V2(1/12) = 0.00231180 +- 5.6e-8` against `0.00231178`; `checks.py seeded` prints `Deep = 1.8882e-6 +- 1.4e-8` against the bound `3.8420e-5` at `1/6` and `4.7432e-8 +- 2.9e-9` against `2.1452e-5` at `1/8`, with `V2` at both radii against `2 A1 - delta^2/3 + Deep`; `checks.py recompute` prints the column counts validated to level 6, the hole integrals against quadrature to `1e-24` or better, `V1`, `A1`, the `Deep` bound and `T` at the three radii, the three bands to twelve digits, the series tails, and `V1(1/12)`, `A1(1/12)` at 200 digits with the naive `a1` and on the grid.