# Digit designs and the Euler product - 2026-09-07 [Proved] The indicator of `S_F`, the integers whose base digits all lie in the digit set `F`, is multiplicative exactly at the full digit set. `1 in F` is forced by `f(1) = 1`; if a digit `c >= 2` is missing take the least, and `R_c R_(c+1)` has no carry because its `base^m` coefficient is `min(m+1, c, 2c-m) <= base-1`, so its digit set is exactly `{1..c}` while `gcd(R_c, R_(c+1)) = R_1 = 1`; if only `0` is missing then odd `base` gives the coprime pair `(2, (base^2+1)/2)` with product `base^2 + 1 = 101`, and even `base` gives `(base^2-1, base^2+1)`, coprime and odd, whose product `base^4 - 1` has every digit `base-1` while `base^2+1` does not lie in the set. Over all 8177 sets with `2 <= base <= 12` the constructed witness is asserted at each of the 4083 sets that pass `f(1) = 1` and are not full, and an independent search finds a minimal witness for every one, hardest `base = 12`, `F = {1}`, pair `(5, 377)`. No design outside the full set carries an Euler product over primes; `0` excluded and a single digit both fail. Witness: lab/py/mrly-euler verb wall. - 2026-09-07 [Proved] For every `F` strictly inside `{0..base-1}` the design zeta and the design Mobius series obey a disjunction and not a universal: if `1` is outside `F` the constant coefficient of `zeta_F M_F` is `0`; if a prime `p` of `S_F` has `p^2` outside `S_F` the coefficient at `p^2` is `-1`, since `(p,p)` is the only admissible factorisation; and otherwise `zeta_F M_F = 1` forces the least element `g > 1` of `S_F` to be prime with every power `g^j` in `S_F`, a necessary condition on an escapee and not a contradiction. At the full digit set the two are inverse, `zeta_F = zeta` and `M_F = 1/zeta`. Over 257 sets the least `n > 1` with a nonzero coefficient is at most `50`, first at `n = 4` for base 3 `{0,1}` and `n = 9` for base 10 missing `9`, while the eight full sets have none below `4000`. Witness: lab/py/mrly-euler verb pair. - 2026-09-07 [Proved] The position product. With `G_level(t) = prod_(i= 1) a(n) n^(-s) = int_0^1 G_level(t) A(s,t) dt` for every absolutely convergent Dirichlet series, with `A(s,t) = sum_(n >= 1) a(n) e(-nt) n^(-s)`; `a = 1` is the periodic zeta of DLMF 25.13.1 and `a = mu` the Lerch-Mobius series, so `zeta_F` and `M_F` are pairings of one set-only product against one arithmetic-only kernel. The set enters through the digit positions and never through the primes. Checked to `1.95e-16` and `2.04e-16` at base 10 missing `9`, `level = 3` and `level = 4`, and `2.9e-16` at base 3 `{0,1}`, `level = 3, 4, 5`. Witness: lab/py/mrly-euler verb position. - 2026-09-07 [Proved] The tree's pair route is Holder on the position identity. When `0` is in `F`, at `x = base^level` the identity is finite on both sides, `M_F(base^level) = int_0^1 G_level(t) S_level(t) dt` with `S_level(t) = sum_(n < base^level) mu(n) e(-nt)`, so `abs(M_F(base^level)) <= (int_0^1 abs(G_level)) max_t abs(S_level)` is at most `fill^level base^(level(alpha_1 - 1)) x^b = x^(alpha + alpha_1 - 1 + b)`; when `0` is outside `F` the same upper bound holds after summing the levels, a geometric sum of ratio `base^(alpha + alpha_1 - 1 + b) > 1` by the floor `alpha + alpha_1 >= 1` of mobius.md. It sits under the trivial `x^alpha` exactly when `alpha_1 < 1 - b`, which is the bar of coprime.md and mobius.md derived rather than posited, with `b = 3/4 + eps` under GRH from Baker and Harman 1991. Witness: lab/py/mrly-euler verb position. - 2026-09-07 [Proved] The fibres of the Lerch-Mobius series are inverse Dirichlet L-functions. Splitting `n` by `g = gcd(n,Q)` and expanding on the characters of `(Z/(Q/g))^*` gives `M(s, a/Q) = sum_(g divides Q) mu(g) g^(-s) phi(Q/g)^(-1) sum_(chi mod Q/g) tau_a(chi) L(s,chi)^(-1) prod_(p divides Q not Q/g) (1 - chi(p) p^(-s))^(-1)`, so `M(s, a/Q)` continues to `C` with singularities in `Re s > 0` only at zeros of `L(s,chi)` of modulus dividing `Q`, and `M(s,0) = 1/zeta(s)`. Since `G_level(a/base^j) = fill^(level-j) G_j(a/base^j)` are the largest values the position product takes, the design's major arcs are the `base`-power rationals, and on that family holomorphy in `Re s > 1/2` is exactly GRH for `base`-power modulus. Coefficient identity checked to `2.6e-12` at eleven pairs `(Q,a)` including `Q = 3, 9, 27, 100`, the Euler-factor step to `7.4e-16`. Witness: lab/py/mrly-euler verb fibre. - 2026-09-07 [Proved] The reflection moves the kernel and not the design. Solving Hurwitz's formula DLMF 25.13.3 at `x = t` and `x = 1-t` gives `Z(s,t) = ((2 pi)^s Gamma(1-s)/(2 pi i))(e^(pi i s/2) zeta(1-s,t) - e^(-pi i s/2) zeta(1-s,1-t))` for `s` not a positive integer, the derivation dividing by `2i sin(pi s)`; this is DLMF 25.13.2 recovered, the gain being the range `Re s > 0` in place of `Re s > 1`. The position identity turns it into a dual integral of the same `G_level` against Hurwitz zetas at `1-s`, never a relation between `zeta_F(s)` and `zeta_F(1-s)`; the design's own symmetry is the `base`-adic scaling `G_level(t) = g(t) G_(level-1)(qt)`, whose transfer eigenvalue `fill base^(-s)` is what makes the vertical pole lattice. Formula checked to `2.1e-30` at `s = 3.3`, `2.7 + 1.9i` and `0.6 + 4.1i`. Witness: lab/py/mrly-euler verb dual. - 2026-09-07 [Proved] The design's multiplicative shadow is a Lyndon Euler product with no RH content. On the free monoid over `F` with norm `N(w) = base^(abs(w))`, `sum_w N(w)^(-s) = 1/(1 - fill base^(-s)) = prod_(level>=1) (1 - base^(-level s))^(-c_fill(level))` with `c_fill(level)` the Lyndon count, by Chen-Fox-Lyndon: every word factors uniquely as a non-increasing product of Lyndon words, so the free monoid on `F` is equinumerous by norm with the free abelian monoid on Lyndon words and is not equal to it. The primes are the Lyndon words, the zeta is zero-free, its Mobius is supported on the empty word and the letters so its Mertens is `1 - fill` beyond norm `1`, and its poles are exactly `s = alpha + 2 pi i m / log base`, the design pole lattice. All RH content of `zeta_F` therefore sits in the cofactor `zeta_F(s)(1 - fill base^(-s))`. Expansion verified through `u^16` at `fill = 2, 3, 4, 9, 10`, `c_2(level)` being A001037. Witness: lab/py/mrly-euler verb word, A001037. - 2026-09-07 [Proved] The Beurling system of a design with non-unit digit gcd is finitely generated, on two branches. If `gcd(F) = a > 1` every element of `S_F` is a multiple of `a`; when `a` is prime the primes of the design are `{a}`, `N_F` is the powers of `a` and `M_B(x) = 0` for `x >= a`, and when `a` is composite `S_F` holds no prime at all, `N_F = {1}` and `M_B` is identically `1`, witness `base = 10`, `F = {0,4,8}`. Either way the eight scaled census families of mobius.md are exactly the columns the Beurling route cannot see, while the scaling transfer reads them exactly. Witness: lab/py/mrly-euler verb beurling. - 2026-09-07 [Verified] The Beurling census on the primes of a design, to `x = 10^6`. Base 3 `{0,2}` has the single prime `2` and `M_B` identically zero past `2`; base 3 `{0,1}` has `525` primes, `N_F(920483) = 2198`, running `max abs(M_B) = 98` and exponent `0.3339` against `alpha/2 = 0.3155`; base 10 missing `9` has `35139` primes, `N_F(10^6) = 488864` against `x^alpha = 531441`, `M_B(10^6) = 1860`, running max `1866`, and exponent `log(running max)/log x` reading `0.4203, 0.4882, 0.5452` at `10^4, 10^5, 10^6` against `alpha/2 = 0.4771`, where full base 10 as control reads `0.4084, 0.4241, 0.4276` at the same points against its own `alpha/2 = 0.5`. What the census reads is the level and not a trend: `+0.068` over `alpha/2` for the design against `-0.072` for the control, a running maximum climbing in both. There is cancellation, `0.545` against the trivial `alpha = 0.954`, and it is above `alpha/2`, so the census supports cancellation and does not support the square-root conjecture on `N_F`; `N_F` is not `S_F`. Full base 10 reproduces `-23, -48, 212` at `10^4, 10^5, 10^6`, A084237. Witness: lab/py/mrly-euler verb beurling, A084237. - 2026-09-07 [Proved] The identity that replaces `zeta M = 1` on a design. For every `(base,F)` with `1 in F` the indicator `1_(S_F)` has a Dirichlet inverse `nu_F`, given by `nu_F(1) = 1` and `nu_F(n) = -sum_(d divides n, d > 1, d in S_F) nu_F(n/d)`, so `zeta_F(s) N_F(s) = 1` with `N_F(s) = sum nu_F(n) n^(-s)`; the support of `nu_F` lies inside the multiplicative semigroup generated by `S_F` and strictly inside it, since `9`, `27` and `36` lie in the semigroup with `nu_F = 0` while `16`, `48` and `52` lie in the semigroup and outside `S_F`, so the semigroup is a third set beside `S_F` and the Beurling integers on the primes of the design and the support is a fourth, and `nu_F` is `mu` exactly at the full digit set, where the classical identity is the special case. If `rho` is a zero of `zeta_F` with `Re rho > alpha` then `sigma_c(N_F) >= Re rho`, by the identity theorem on the connected pole-free half plane `Re s > max(sigma_c(N_F), alpha)`, so `sum_(n <= x) nu_F(n)` is not `O(x^(Re rho - eps))` for any `eps > 0`; the converse bound `sigma_c(N_F) <= sup Re rho` is not claimed. Checked against `mu` term for term on the full digit set to `n = 131072` at `base = 2` and `n = 177147` at `base = 3`, and the partial sums of `N_F(sigma)` meet `1/zeta_F(sigma)` to `1.60e-3` at `sigma = Re rho + 0.08 = 0.8008` and `1.96e-4` at `sigma = Re rho + 0.20 = 0.9208` at base 3 `{0,1}`, and to `1.72e-2` at `sigma = 1.0816` and `2.39e-3` at `sigma = 1.2016` at base 10 missing `9`, both offsets sitting above `Re rho`. Witness: lab/py/mrly-pairing verb inverse, lab/py/design-zeta. - 2026-09-07 [Proved] The design's own Mobius has anti-cancellation, and that is what makes the decoupling a blessing. Winding boxes on `zeta_F` by the argument principle certify one zero each and pin `Re rho` to the box edges: winding `1` on `Re in [0.72074, 0.72084]`, `Im in [28.60563, 28.60573]` at base 3 `F = {0,1}` with contour minimum `abs(zeta_F) = 8.298e-4` against the engine bound `6.284e-30`, and winding `1` on `Re in [1.00150, 1.00168]`, `Im in [2.73915, 2.73925]` at base 10 missing `9` with contour minimum `6.865e-4` against `2.798e-23`, while the control rectangle `Re in [0.99900, 1.00050]`, `Im in [2.73810, 2.74030]` there returns winding `0`. Both boxes lie strictly right of `alpha = 0.6309297536` and `0.9542425094`, so `sum_(n <= x) nu_F(n)` is not `O(x^(0.72074 - eps))` and not `O(x^(1.00150 - eps))` respectively: the limsup of the design's own Mertens function exceeds the design's own mass `A_F(x)`, and at base 10 missing `9` exceeds `x` itself, the box lying right of `Re s = 1`. The square-root conjecture in the `alpha/2` shape is therefore false for `nu_F` and can only be carried by `mu` restricted to `S_F`; the sibling's decoupling theorem is what protects it. Pointwise the census is far below both limsups, `max/A_F = 0.0738` at base 3 `level = 16` and `max/x = 0.0847` at base 10 `level = 7`: the running maximum of `sum nu_F(n)` grows by `9.4474, 11.5000, 10.2220, 10.0354` per level at base 10 missing `9`, `level = 4..7`, against `base^(Re rho) = 10.036661` and the trivial `fill = 9`, only the last of the four landing on the predicted rate, with `max/A_F(base^level)` rising `0.1043, 0.1094, 0.1398, 0.1588, 0.1771`; at base 3 `{0,1}` the geometric mean of the four steps `level = 12..16` is `2.059` against `2.207512` and `2` while the arithmetic mean of the five printed level ratios is `1.9972`, below the trivial `2`, a census too short to separate them. Witness: lab/py/mrly-pairing verbs box and inverse, lab/py/design-zeta. - 2026-09-07 [Verified] The pair `zeta_F M_F = 1 + D_F` gains nothing: `D_F` has abscissa exactly `alpha`. Absolute convergence of `zeta_F^2` puts `sigma_a(D_F) <= alpha` and that half is proved; for the other half, if `sigma_c(D_F)` were below `alpha` then `M_F(sigma) = (1 + D_F(sigma))/zeta_F(sigma)` would tend to `0` as `sigma -> alpha+`, since `zeta_F` has nonnegative coefficients and is singular at its abscissa by Landau, so `zeta_F(sigma) -> +infinity`, and there is no circularity in the argument because `M_F` is dominated termwise by `zeta_F` and so converges absolutely at every `sigma > alpha` with no hypothesis on `theta(F)`. That half rests on a measurement, unconditional in shape since `sigma_c(D_F) < alpha` would force `P(x) = o(x^alpha)`: `P(x) = sum_(n <= x) c_F(n)` divided by `x^alpha` is bounded away from `0` and from infinity, reading `0.493767, 0.699235, 0.758519, 0.587055` at four sampling phases at base 3 `{0,1}`, the four phases being needed because `P(x)/x^alpha` is log-periodic and sampling only at `x = base^level` aliases every Fourier mode onto one number. The `M_F(sigma) -> 0` limit test is not a witness here: the tail the generator prints beside it is `base^(-level alpha/2)`, which assumes the square-root conjecture, and against the unconditional tail `(fill-1) base^(-level eps)/(1 - base^(-eps))` from `A_F(base^l) = fill^l` no printed `M_F` value at base 10 missing `9` is distinguishable from `0`. Since `M_F = (1 + D_F) N_F` and `sigma_c(N_F) > alpha`, the glue is not neutral but lossy. Witness: lab/py/mrly-pairing verb glue. - 2026-09-07 [Proved] The position pairing is exact on the grid and its `l^1` mass sits at the top level, which kills the per-denominator split. For `0 in F`, `M_F(base^level) = base^(-level) sum_(a mod base^level) G_level(a/base^level) S_level(a/base^level)` exactly, both factors being trigonometric polynomials of degree below `base^level`; writing `a = base^v a'` with `base` not dividing `a'` and `j = level - v` gives `G_level(a/base^level) = fill^(level-j) G_j(a'/base^j)` and the exact level decomposition `C_level = sum_(j=0)^level fill^(level-j) c_j` of the `l^1` mass, with `C_j = fill C_(j-1) + c_j`. The `l^1` floor `C_j >= base C_(j-1)` forces the top-level share `c_level/C_level >= 1 - fill/base = m/base` at every base and digit set, measured `0.485846, 0.602606, 0.687994, 0.510055` against floors `0.333333, 0.500000, 0.600000, 0.100000`, with levels `j >= level/2` carrying `0.995116, 0.996061, 0.997043, 0.942350`. Since the Baker-Harman Proposition beats the uniform `x^(3/4)` only below `j = level/2`, weighting the Mobius input per denominator saves exactly `log(C_level/c_level)/(level log base)`, a constant factor capped by `base/m`: the numerator is `0.657068` at base 3 `{0,1}`, identical at every `level = 6..14`. The split exponents are `0.988106, 0.912502, 0.905006, 1.012881` uniform and `0.941173, 0.879287, 0.879188, 0.964150` per denominator against `alpha = 0.630930, 0.500000, 0.430677, 0.954243`, while the Cauchy-Schwarz split is `(alpha+1)/2` exactly since `int abs(G_level)^2 = fill^level`; the base 2 and base 3 full-set controls return `0.500000`, the classical RH exponent. Witness: lab/py/mrly-pairing verb split. - 2026-09-07 [Proved] The principal fibre of the grid pairing has exponent `alpha - 1/2` under RH, below the conjectured `alpha/2`, and that is an asymptotic statement only. The `a = 0` term of the grid pairing is `base^(-level) fill^level M(base^level)`, of exponent `alpha - 1/2` under RH, and `alpha - 1/2 < alpha/2` for every `alpha < 1`, so in the limit the classical Mertens function cannot carry the conjectured size of the design meter. At finite depth it carries a great deal: the `a = 0` term reads `-0.31857` of `11`, `0.11133` of `6`, `-0.05924` of `9` and `112.66549` of `276` at base 3 `{0,1}` `level = 14`, base 4 `{0,1}` `level = 11`, base 5 `{0,1}` `level = 9` and base 10 missing `9` `level = 6`, shares `-0.028961, 0.018555, -0.006583, 0.408208`, and exactly all of the meter on the two full-set controls. So at base 10 missing `9` the principal fibre carries `40.8` percent of the meter at the only measured `level`, which refutes any claim that the square-root conjecture lives entirely off the principal fibre at finite depth: the exponent gap there is `0.454243` against `0.477121`, and a factor of `10` between them needs `x = 10^44`. Witness: lab/py/mrly-pairing verb split. - 2026-09-07 [Proved] The one-step constant of the digit transform never exceeds the triangle-split bound, and is strictly below it at every family measured beyond `level = 1`. With `H(t) = sum_(r mod base) abs(g_F((t+r)/base))` and `B_base(F) = sup_t H(t)`, the identity `C_level = sum_(a mod base^(level-1)) abs(G_(level-1)(a/base^(level-1))) H(a/base^level)` gives `C_level <= B_base(F) C_(level-1)`, so `C_level/C_(level-1) <= B_base(F)` at every `level` and every family with no computation at all; the inequality is not strict in general and equality is attained, `C_1/C_0 = 4 = B_base(F)` exactly at base 3 `{0,1}`, so strictness needs `level >= 2`. Verified there: `C_level/C_(level-1)` reads `3.889888518, 5.032783116, 6.410132461, 18.369402635` at base 3 `{0,1}`, base 4 `{0,1}`, base 5 `{0,1}` (all `level = 9`) and base 10 missing `9` (`level = 6`), against `B_base(F) = 4.000000000, 5.226251860, 6.472135955, 19.888543820`, and the ratio agrees between the two consecutive `level` the generator prints to `8.5, 7.4, 10, 5.0` digits by family, so the stability is family by family and two values of `level` are all that is measured. Witness: lab/py/mrly-pairing verb split. - 2026-09-07 [Proved] The design Mobius of the two-digit design is base-free. Let `S*` be the nonzero `0/1` polynomials of `Z[x]`, `M*` the monoid they generate, `nu*` the Dirichlet inverse of `1_(S*)`. For `F = {0,1}` at every `base >= 2`, `nu_F(n) = sum over P in M* with P(base) = n of nu*(P)`. Evaluation is a bijection `S* -> S_F`, a monoid homomorphism, and of finite fibres, since an element of `M*` has nonnegative coefficients so `P(base) = n` caps every coefficient by `n` and `deg P` by `log(n)/log(base)`; the pushforward `g` therefore exists, `g(1) = 1` because `1` is the only element of `M*` of value `1`, and grouping the pairs `(D, Q)` in `S* x M*` with `D(base) Q(base) = n` by `P = DQ` turns `1_(S*) * nu* = delta` into `1_(S_F) * g = delta`, where the Dirichlet inverse is unique. Hence `sum_(n <= x) nu_F(n) = sum over P in M* with P(base) <= x of nu*(P)` at every `x`: the base enters only as the order in which one base-free function is summed, and at `base = 2` the classical `mu` is that pushforward. Checked term for term with 0 mismatches to `n <= 2^15`, `3^10`, `4^8` and `5^7`, where 108978 elements of `M*` collapse onto 32768 integers at base 2. Witness: lab/rs/carry-free-mobius verb lemma. - 2026-09-07 [Proved] The degree-graded mass of the base-free design Mobius is `1 - 2t` exactly. Degree is a monoid homomorphism `M* -> N` with finite fibres because `1` is the only constant in `M*`, which holds for `F = {0,1}` and for no design carrying a digit at least 2, where a constant `c >= 2` makes the degree-zero fibre `{c^k}` infinite; pushing `1_(S*) * nu* = delta` along it with `2^d` polynomials of degree `d` gives `A(t)/(1 - 2t) = 1`, so the graded sums are `1, -2, 0, 0, ...` and `sum over deg P < level of nu*(P) = -1` for every `level >= 2`. The design Mertens function is therefore pinned to `-1` at every level boundary `level >= 2` inside the carry-free window, and reads `0` at `level = 1`. Witness: lab/rs/carry-free-mobius verb sequence. - 2026-09-07 [Proved] The design zeta has an explicit zero free half plane, and it closes the census right of the abscissa. Let `a_min` be the least nonzero digit of `F`, hence the least element of `S_F`, every element of two digits or more exceeding `base`. If a real `sigma > alpha` satisfies `a_min^sigma zeta_F(sigma) < 2` then `zeta_F` has no zero in `Re s >= sigma`: the coefficients are nonnegative and the series converges for `sigma > alpha`, so for `Re s = sigma' >= sigma` one has `abs(a_min^s zeta_F(s) - 1) = abs(sum_(n in S_F, n > a_min) (n/a_min)^(-s)) <= sum_(n > a_min) (n/a_min)^(-sigma) = a_min^sigma zeta_F(sigma) - 1 < 1`. The hypothesis `sigma > alpha` is load bearing and the test is one real evaluation carrying the ladder's own error bound. On the grid `alpha + 0.05 n` the edge `sigma_1` reads `0.5` at base 4 `{1}` to `1.75` at the three full digit sets over twenty-four designs, with `a_min^sigma zeta_F(sigma)` in `[1.8635, 1.9995]` and largest `sigma_1 - alpha` equal to `0.95`, so a census of the zeros right of `alpha` needs no hand chosen right edge and the `alpha + 3.02` strip of the locus sweep is three times wider than the zeros need. Witness: lab/py/transport-census verb census. - 2026-09-07 [Verified] The transport census: every proper design censused carries zeros right of its abscissa, the full digit set alone carries none, and each rightmost is certified by a winding box. On the box `alpha + 1e-6 < Re s < sigma_1`, where the cofactor `Z = zeta_F(s)(1 - fill base^(-s))` is analytic and its zeros right of `alpha` are exactly those of `zeta_F`, the transfer failing only at residue null poles which sit on the line `Re s = alpha`, the argument principle counts `157` zeros right of `alpha` below `Im s = 40` over twenty-three designs, all `157` located, plus `2` at base 50 missing one digit below `Im s = 4`. The count is exact on the box and a lower bound for the half plane, since the sliver `alpha < Re s <= alpha + 1e-6`, the band `0 < Im s < 0.02`, everything above the census height and the conjugate half plane are uncounted. Twenty-one of the twenty-four designs carry such a zero; the three that do not are the base 2, 3 and 4 full digit sets, whose windings read `-1.97e-33`, `1.73e-33` and `1.53e-33`. Every rightmost carries the height it is read below, because the teeth of the level zero comb drift right with the pole index: base 20 missing one digit reads `1.000285484146` at `Im s = 2.0988`, `1.000549674321` at `4.1971` and `1.002685494779` at `14.6920`. Below `Im s = 40` the rightmost real parts run `0.441505537191` at base 5 `{0,1}` to `1.002685494780` at base 20 missing one digit, each certified by a winding `1` box on `zeta_F` of half width `5e-5` in `Re s` and in `Im s` whose sampled contour minimum, `1.2e-4` to `6.1e-3`, beats the engine's error bound by at least eight orders of magnitude and whose distance to the pole lattice `s_(i,j) = alpha - i + 2 pi i j/log base` is at least `0.00517845`, four hundred box half widths. The two published boxes of lab/py/mrly-pairing reproduce at their own edges, winding `1` and `1` with contour minima `8.298e-4` and `6.865e-4`, and its control rectangle returns winding `0`. Witness: lab/py/transport-census verb census. - 2026-09-07 [Proved] A certified zero right of the abscissa refutes every square-root-shaped bound for the design's own Mobius, and the digit `1` is the hypothesis that bites. Let `1 in F`, let `rho` be a zero of `zeta_F` certified by a winding `1` box with left edge `x_0 > alpha` containing no pole, and let `nu_F` be the Dirichlet inverse of `1_(S_F)`. The transport theorem gives `sigma_c(N_F) >= Re rho >= x_0 > alpha`, so `sum_(n <= x) nu_F(n)` is not `O(x^(x_0 - eps))` for any `eps > 0`; since `A_F(x)` has exponent `alpha` the square-root exponent is `alpha/2 <= alpha < x_0`, so the design's own Mobius satisfies no square-root-shaped bound and misses even the trivial `O(x^(alpha - eps))`, the first inequality failing to be strict only at the two designs with `alpha = 0`, where `A_F(x)` grows like `log x`. Nineteen of the twenty-four designs censused meet all three hypotheses and get a bound, and seventeen of the twenty-two the locus and family sweeps censused, the bounds running `theta(nu_F) >= 0.4414555` at base 5 `{0,1}` to `theta(nu_F) >= 1.0026354` at base 20 missing one digit. Four designs have `Re rho > 1`, so their own Mobius outruns the count of all integers below `x`: base 10 missing two digits, base 10 missing the digit `9`, base 20 missing one digit and base 50 missing one digit, at `fill/base = 0.8, 0.9, 0.95, 0.98` and `alpha = 0.9030900, 0.9542425, 0.9828779, 0.9948357`; only the SIGN of `Re rho - 1` is read and never its size, three of the four being censused to `Im s = 40` and base 50 to `Im s = 4`. The `fill/base` reading dies on its control, base 5 `{0,1,2,3}` at the same `fill/base = 0.8` with rightmost `0.989748105861`. Two designs carry a zero right of `alpha` and no bound: base 4 `{2,3}` and base 4 `{0,2,3}` omit the digit `1`, so `1` is outside `S_F`, the indicator vanishes there and `nu_F` does not exist. Witness: lab/py/transport-census verb law. - 2026-09-07 [Refuted] The gain of a design's rightmost zero over its abscissa is not a function of `alpha` and `fill/base`. The refuted functional is new: the locus row already refutes a law for the POSITION of the zeros, this refutes one for the single statistic the transport theorem reads, the rightmost real part less `alpha`. Four equal key families, one base and one digit count each so `alpha` and `fill/base` agree exactly and not to a rounding, read unequal gains: at `alpha = 1/2`, `fill/base = 1/2` the four base 4 two digit designs give `0.0853043873`, `0.4400124317`, `0.2706238545`, `0.3439264581`, a spread of `0.35470804`; base 5 at `alpha = 0.4306766`, `fill/base = 0.4` spreads `0.37474232`; base 3 two digit at `alpha = 0.6309298` spreads `0.17605693`; base 4 three digit at `alpha = 0.7924813` spreads `0.060972003`, which is still six hundred box widths. The two columns disagree in direction: the gain is largest at the sparsest designs, `0.5291214025` and `0.4485242462` at `alpha = 0`, while the rightmost real part itself is smallest there. What rises with `alpha` is the floor, the least rightmost real part at each `alpha` reading `0.4485242462, 0.4415055372, 0.5853043873, 0.7207876015, 0.9126562295, 0.9897481059, 1.0015143877, 1.0015892753, 1.0026854948, 1.0000614750` up ten rungs `alpha = 0, 0.4307, 0.5, 0.6309, 0.7925, 0.8614, 0.9031, 0.9542, 0.9829, 0.9948`, rising at every step but the first and the last, the last being where the census height drops from `40` to `4`; one design per rung above `alpha = 0.86` against six at `alpha = 0.5`, and no fit is taken. Witness: lab/py/transport-census verb law. - 2026-09-11 [Proved] `nu*` vanishes at every polynomial divisible by `x^2`, and `nu*(x b) = -nu*(b)` at every `b` of nonzero constant term. The convolution runs over `Z[x]` divisors and `M*` is not divisor-closed, `1 + x^2 + x^4 = (1 + x + x^2)(1 - x + x^2)`, so the claim lives on `A`, the nonzero polynomials mod units, where `nu*` vanishes off `M*` by induction. `A` splits as `N x R`, `R` the classes of nonzero constant term and divisor-closed; `x^k b` lies in `S*` exactly when `b` lies in `S*_odd`, so `1_(S*)` is the outer product of the all-ones function on `N` with `1_(S*_odd)`, inversion factors, and the inverse of the all-ones function on `N` is `1 - t`. Witness: lab/rs/carry-free-mobius verb ladder. - 2026-09-11 [Proved] Every element of `M*` of degree `d` has its coefficient of `x^i` at most `binomial(d, i)`, so the maximum coefficient at degree `d` is exactly `binomial(d, floor(d/2))`, A001405, attained by `(1+x)^d`. A product of `0/1` polynomials of degrees summing to `d` is dominated coefficientwise by `prod_k (1 + x + ... + x^(d_k))`, each factor by `(1 + x)^(d_k)`, and domination survives products of nonnegative polynomials, so the product is under `(1 + x)^d`, itself in `M*`. This retires the measured clause and the crude cap `2^(L-1)` of the carry-bound row. Checked at every degree to 22, maximum 705432. Witness: lab/rs/carry-free-mobius verb ladder. - 2026-09-11 [Proved] On `R`, the classes of nonzero constant term among the nonzero polynomials up to units, `nu*` is fixed by the reciprocal `b -> x^(deg b) b(1/x)`. There the reciprocal is degree-preserving, multiplicative and involutive, hence a monoid automorphism, and it carries `S*_odd` onto itself by reversing the bitmask, so it preserves `1_(S*_odd)` and its Dirichlet inverse. It is no invariance on all of `Z[x]`: the reciprocal drops the `x` power and `nu*(x) = -1` against `nu*(1) = 1`. Checked with 0 mismatches over the 35121747 classes of degree 1 to 21. Witness: lab/rs/carry-free-mobius verb ladder. - 2026-09-11 [Proved] The carry-free window of a two-digit design is `(base+1)^(level-1) < base^level`. A `0/1` polynomial of degree `d` has `P(base) <= (1+base)^d` and degrees add over a product, so the maximum of `P(base)` over `M*` at degree below `level` is exactly `(base+1)^(level-1)`, attained by `(1+x)^(level-1)`, and the least base holding every such element under `base^level` is the least `base` with `(base+1)^(level-1) < base^level`. Verified by enumeration at `level = 3..14`, reading 3, 3, 4, 4, 4, 5, 5, 6, 6, 6, 7, 7. The windows are 4, 7, 9, 12 and 15 at bases 3 to 7, and `sum_(n <= base^level) nu_F(n)` leaves `-1` at level 5, 8 and 10, one level past the window each time. Witness: lab/rs/carry-free-mobius verb lemma. - 2026-09-11 [Conjecture] The base-free Mertens maximum of the two-digit design gains on the design's mass without reaching it. The running maximum of `sum nu*` over degree below `level` reads 1, 1, 2, 3, 4, 7, 15, 23, 45, 86, 162, 331, 741, 1665, 3173, 7508, 17753, 36147, 79645, 182432, 427806, 858703, 2026147 at `level = 1..23`, and the ratio `max/2^level` bottoms at 0.079102 at `level = 11`, falls for the last time at `level = 15`, and rises at every step from there to 0.241536 at `level = 23`. A turn-down at a deeper level kills the trend and none is seen to 23. Witness: lab/rs/carry-free-mobius verb ladder. - 2026-09-11 [Conjecture] The rate of that maximum exceeds the design's mass rate 2, and its estimate is window-unstable. At depth 23 the geometric mean step reads 2.245836, 2.202419, 2.242075, 2.206405 over the last 4, 6, 8, 10 levels but 2.194975, 2.149760, 2.092480, 2.074545, 1.996559 over the last 12 to 20, a hull of [1.996559, 2.245836] straddling 2, the long windows opening inside the levels where the ratio still fell. Every short-window reading at depths 20 to 23 sits above 2.18 and above its depth-18 value. No constant is claimed; `log_2(max)/level` reaches 0.910883 at `level = 23` unsettled. Witness: lab/rs/carry-free-mobius verb ladder. - 2026-09-19 [Proved] Weil's theorem reaches a design zeta along no evaluation bridge: `P -> P(base)` on polynomials with coefficients in `{0..base-1}` is a bijection onto the nonnegative integers and additive only where no carry occurs, a coefficient of the polynomial product `P R` reaching `(base-1)^2 (min(deg P, deg R) + 1)` against the digit cap `base - 1`, so an integer product's digit string is the carry reduction of the polynomial product and `R_c R_(c+1)` is the shortest coprime pair whose carry-free product shows the missing digit `c`. Witness: lab/py/mrly-euler verb wall. - 2026-09-19 [Proved] Under the hypothesis `alpha < 1` the large sieve does not rescue the per-denominator split on the major arcs: writing `a = base^v a'` with `base` not dividing `a'` and `j = level - v`, the `l^2` mass of the grid pairing over the levels `j <= J` is exactly `fill^(2 level - J) base^J`, and the spacing form of the large sieve on those `base^(-J)` spaced points gives `(base^level + base^J) base^level`, so the levels below `J = u level` cost `x^(alpha + u(1-alpha)/2)`, strictly above `alpha` at every `u > 0` and equal to `alpha` only at `u = 0`. Witness: lab/py/mrly-pairing verb split, Montgomery and Vaughan 1973.