restricted-franel

• Franel's identity on a digit design: an exact formula for the Fourier and the rank L^2 discrepancy of the denominator-restricted Farey set, written as a gcd-weighted double sum over DILATED Mertens sums.
• The object is the Farey page's THE METER ON A DIGIT DESIGN, denominator convention, written F_Q^d(S_F) here because the Farey page binds F_Q(S_F) to the STRICT set: F_Q^d(S_F) = {a/b reduced, b in S_F, b <= Q, 1 <= a <= b}, with S_F the whole numbers whose every base digit lies in a digit set F.
• Five results: the frequency-m exponential sum (Theorem 1), the identity in both its Fourier and its rank form (Theorem 2), the one-line inequality that carries the restricted Mertens sum back out of it (Theorem 3), the strict convention's divisor-sum identity with the refutation that kills every Mertens-type closed form for it (Theorem 4), and the dilate automaton with the converse it closes (Theorem 5).
• The template is gaussian-franel, which is the same transcription one field up. The enumeration is this study's own: farey-discrepancy is a Rust crate whose Design type and mediant walk are not exported to Python, so the digit test and the design list are rebuilt here in eight lines and the node counts are checked against that study's published table.

THE OBJECT

• Design: base >= 2, digit set F, S_F the whole numbers whose every base digit lies in F, mass exponent alpha = log|F|/log base. The two designs run here are base 3 with F = {0,1} and base 10 with the digit 9 missing, the pair the Farey page meters.
• Denominator set: F_Q^d(S_F) = {a/b : b in S_F, b <= Q, 1 <= a <= b, gcd(a,b) = 1}, of size m_F(Q) = sum_{b in S_F, b <= Q} phi(b).
• Strict set: F_Q^s(S_F) = {a/b : a in S_F, b in S_F, b <= Q, 1 <= a <= b, gcd(a,b) = 1}.
• The dilated Mertens sums. M_F(x; d) = sum_{c <= x, dc in S_F} mu(c), the Mertens function of the dilated design d^{-1} S_F = {c : dc in S_F}. At d = 1 it is the design's own meter M_F(x) = sum_{n in S_F, n <= x} mu(n), the Mobius page's. The dilates are the whole content of the restriction: d^{-1} S_F is not S_F, is not a digit design in general, and carries no digit test, so every d > 1 brings a new function rather than a rescaling of the old one. On the full set every dilate is Z and all of them collapse to M.
• Exponential sums at frequency k: S_F(k, Q) = sum_{r in F_Q^d(S_F)} e(kr) with e(x) = exp(2 pi i x), and S_F^s(k, Q) the same over the strict set.

THEOREM 1, THE EXPONENTIAL SUM

• Ramanujan's sum over a digit design. For every m >= 1 and Q >= 1, S_F(m, Q) = sum_{d | m} d M_F(Q/d; d). Proved.
• Proof. Partition by denominator: S_F(m, Q) = sum_{b in S_F, b <= Q} c_b(m) with c_b(m) = sum_{a mod b, gcd(a,b) = 1} e(ma/b) Ramanujan's sum, which depends on b alone and not on the design. Kluyver's formula is c_b(m) = sum_{d | gcd(m, b)} d mu(b/d). Exchanging the two sums gives S_F(m, Q) = sum_{d | m} d sum_{b in S_F, b <= Q, d | b} mu(b/d), and substituting b = dc turns the inner sum into M_F(Q/d; d).
• At frequency 1 the exponential sum IS the design's Mertens meter. S_F(1, Q) = M_F(Q). Proved, the m = 1 case, only d = 1 surviving. It needs no Ramanujan input: sum_{a mod b, gcd(a,b) = 1} e(a/b) = sum_{d | b} mu(d) sum_{c mod b/d} e(c/(b/d)) = mu(b), the inner complete sum vanishing unless b/d = 1.
• The classical case is S_F = Z, where M_F(Q/d; d) = M(Q/d) for every d and the formula reads sum_{d | m} d M(Q/d), the divisor-shifted Mertens sums.
• Verified. Every denominator b in S_F up to Q = 10^5 at base 3 {0,1}, and up to Q = 10^4 at base 10 without 9 and on the control, has its literal sum of phi(b) roots of unity equal to mu(b): worst deviation 1.09e-11 at b = 86293 on the base 3 design and 1.36e-12 at b = 7247 on base 10 without 9, 0 roundings to the wrong integer at either. The Q = 10^5 rung on base 10 without 9 costs 2.6e9 roots of unity, past the machine budget, so it is not walked and nothing is claimed at it. The aggregated literal sum agrees with the exact integer M_F(Q) to 2.02e-09 at the top rung, floating-point accumulation over 5.4e7 roots of unity and not a mismatch. The frequency-m formula is checked at m = 1, 2, 3, 4, 5, 6, 12 on both designs and the control (verb_denominator).

THEOREM 2, FRANEL ON A DIGIT DESIGN

• The kernel. G_F(Q) = sum_{d, e >= 1} (gcd(d,e)^2/(d e)) M_F(Q/d; d) M_F(Q/e; e), a finite sum of exact rationals, every term with d > Q or e > Q vanishing.
• The Fourier form. sum_{k != 0} |S_F(k, Q)|^2 / k^2 = (pi^2/3) G_F(Q). Proved. Substitute Theorem 1, expand the square and exchange: for fixed d, e the inner sum is sum_{k != 0, lcm(d,e) | k} k^-2 = 2 zeta(2)/lcm(d,e)^2, and d e/lcm(d,e)^2 = gcd(d,e)^2/(d e).
• The rank form. If the node set is closed under r -> 1 - r away from the node 1, then with rho_1 < ... < rho_m the nodes of F_Q^d(S_F) ascending, m = m_F(Q) and delta_j = rho_j - j/m, G_F(Q) - 1 = 12 m sum_j delta_j^2, an identity of exact rationals. Proved. Closure is used only to fix sum_r r = (m+1)/2, so THAT mean-value condition is the surviving hypothesis and closure is one sufficient condition for it; the piecewise integration below needs nothing of the node set beyond a top node of 1. Closure holds for every denominator-restricted set, since a/b reduced with b in S_F gives (b-a)/b reduced with the same b and a = b only at the node 1; it fails for every proper strict set.
• Proof of the rank form. With B1bar the sawtooth and A(v) the counting function of the nodes, sum_r B1bar(u + r) = D(1 - u) + c with D(v) = A(v) - m v and c = sum_r r - m/2, so Parseval gives sum_{k != 0} |S_F(k,Q)|^2/k^2 = 4 pi^2 (int_0^1 D^2 - c^2). Integrating D^2 piecewise between consecutive nodes and telescoping gives int_0^1 D^2 = m sum_j delta_j^2 - (m+1)/2 + sum_r r + 1/3, the two boundary cubes vanishing because rho_m = 1. Under the reflection hypothesis the nodes other than 1 pair into m - 1 values summing to (m-1)/2, so sum_r r = (m+1)/2 and c = 1/2, and the remainder collapses to 1/12.
• The kernel is the gcd matrix gcd(d,e)^2/(d e), the same Smith kernel that carries the moire correlation law on the stack page and the Gaussian identity in gaussian-franel. Digit restriction moves the entries, never the kernel.
• Verified. The rank form is an exact rational identity at base 3 {0,1} Q = 81 and Q = 243, base 10 without 9 Q = 40, and the full-set control Q = 40: True at all four. The Fourier form is checked against the literal Fourier side truncated at |k| <= 200000 with the printed tail bound 2 m^2/K, the gap inside the bound in every row. The control at Q = 40 regenerates Edwards section 12.2, G_F(40) - 1 = 12 m sum delta^2 with m = 490 and sum delta^2 = 0.0104270117, which is the number gaussian-franel prints (verb_identity).

THEOREM 3, WHAT COMES BACK OUT

• The inequality. 2 M_F(Q)^2 <= (pi^2/3) G_F(Q), and by the rank form (pi^2/3) G_F(Q) = 4 pi^2 m_F(Q) sum_j delta_j^2 + pi^2/3. Proved, in one line: k = 1 and k = -1 contribute 2|S_F(1,Q)|^2 = 2 M_F(Q)^2 to a sum of nonnegative terms. The constant is not decorative: the weaker-looking 2 M_F(Q)^2 <= G_F(Q) is FALSE, failing already at the full-set control Q = 5 (2 M(5)^2 = 8 against G(5) = 64/15) and at base 3 {0,1} Q = 37 (18 against G_F(37) = 14.230517).
• So a square-root bound on the denominator-restricted Farey discrepancy forces a square-root bound on the design's Mertens meter. The converse needs the whole k sum and is not claimed here.
• The implication. A_F(Q) = #{n in S_F : n <= Q} << Q^alpha, the block count |F|^level at Q = base^level with a constant depending on the design alone, so m_F(Q) = sum_{b in S_F, b <= Q} phi(b) <= Q A_F(Q) << Q^(1+alpha). Hence the denominator lane's CONJECTURED shape sum_j delta_j^2 = O(Q^(-1+eps)) on the Farey page gives G_F(Q) = O(Q^(alpha+eps)) through the rank form, and the inequality then gives |M_F(Q)| = O(Q^(alpha/2+eps)), which is the square-root ceiling for the design's Mertens meter on the Mobius page. Proved, no unproved input entering, the constant pi^2/3 being absorbed. What yields the ceiling is the conjectured exponent -1 and not the measured one: the lane's measured e_2 sits at -0.959 and -0.899 at the top rungs and S2 Q is still climbing there, and a proof of only the measured shape would give no ceiling. Digit restriction of the denominator is invisible to the SHAPE of the meter, and this is what that invisibility costs.
• The converse is open and is where the road ends. It needs the whole k sum controlled from Mertens bounds, so it needs M_F(x; d) for d > 1, and no bound for a dilated design's Mertens function exists on the tree.
• Verified, at every integer Q rather than at a sample. Both sides step only at Q in S_F, since M_F(Q) and every M_F(Q/d; d) change only when Q itself joins S_F, so scanning S_F covers every integer Q below the bound. The inequality is asserted at 0 violations over Q <= 2187 at base 3 {0,1} (128 jumps) and Q <= 400 at base 10 without 9 (324) and on the control (400). The ratio 2 M_F(Q)^2/((pi^2/3) G_F(Q)) peaks at 0.607927 at the trivial Q = 1 on all three; over Q >= 100 its maximum is 0.340071 at Q = 253 on base 3 {0,1}, 0.137645 at Q = 221 on base 10 without 9 and 0.086385 at Q = 114 on the control (scan_backward).
• That the k = +-1 terms carry a third of the whole functional at Q = 253 on a thin design is worth its own look: if the fraction does not fall with Q, the inequality is near sharp there and the converse is nearer than OBSTRUCTIONS claims. Not measured here.

THEOREM 4, THE STRICT SET

• The divisor-sum identity. S_F^s(1, Q) = sum_{b in S_F, b <= Q} sum_{d | b} mu(d) sum_{a <= b/d, da in S_F} e(a/(b/d)). Proved, Mobius inversion of the coprimality condition followed by a -> da. It is exact and it is where the road stops: the inner sum is a digit-restricted exponential sum over an arithmetic progression, the Type II object the Mobius page has no bound for.
• Verified at every denominator: literal summation over {a in S_F : a <= b, gcd(a,b) = 1} against the divisor route agrees to 6.28e-15 over the 64 denominators of base 3 {0,1} below 729 and to 1.95e-14 over the 162 denominators of base 10 without 9 below 200.
• No Mertens-type sum over S_F equals it. Refuted, two ways, the first exact.
• First, the strict sum is not real. Base 3 {0,1} at Q = 3 gives 1 + e(1/3) = 0.5 + (sqrt 3/2) i, and base 10 without 9 at Q = 10 gives -1.809016994 + 0.587785252 i; every Mertens-type sum over S_F is a real integer or a real rational. The two witnesses carry the whole refutation. Beside them sits an observation and not a mechanism: the strict set also fails the pairing a -> b - a that makes the denominator set's sum real, since a in S_F does not give b - a in S_F. Failure of that pairing is not shown to force a non-real sum, and nothing here rests on it.
• Second, it rides the mass. |S_F^s(1,Q)|/card settles at 0.335693, 0.343837, 0.345905, 0.346338 over Q = 3^5, 3^7, 3^9, 3^11 at base 3 {0,1} and at 0.015138, 0.012250, 0.011561 over Q = 10^2, 10^3, 10^4 at base 10 without 9, so |S_F^s(1,Q)| grows like the node count Q^(2 alpha) while every Mertens-type sum over S_F is bounded by #{n in S_F : n <= Q} = O(Q^alpha). At Q = 3^11 the strict sum has modulus 374203.231 against M_F(Q) = -10.
• The three candidates the refutation names, each killed at the smallest Q printed: M_F(Q), the count-weighted sum_{b in S_F, b <= Q} mu(b) phi_F(b) and the normalised sum_{b in S_F, b <= Q} mu(b) phi_F(b)/phi(b), with phi_F(b) = #{a in S_F : a <= b, gcd(a,b) = 1}. All three are real, so the first refutation kills all three at once, at Q = 3 and Q = 10 respectively.
• This is the Fourier face of the Farey page's reading that the strict lane's S1 and S2 ride the mass: a set whose frequency-1 sum is proportional to its own count has no cancellation at frequency 1 and does not equidistribute.

THEOREM 5, THE DILATE AUTOMATON AND THE CONVERSE

• The dilate is a regular language. d^(-1) S_F is recognised least-significant-digit-first by a deterministic automaton whose d states are the carries of long multiplication by d: from carry r the digit e writes the output digit (de + r) mod base, which must lie in F, and moves to the carry floor((de + r)/base), which stays below d because floor((d(base-1) + d - 1)/base) = d - 1. After level digits dc is the level output digits with the terminal carry r_level written above them, so the run accepts exactly when r_level lies in Acc_d = {0} union (S_F intersect [1, d)), of size A_F(d-1) + 1. Proved for a design carrying the digit 0. The dilated Mertens sums therefore run over regular sets and not over digit designs. Without 0 in F the run tests every one of the level padded output digits, a leading output digit 0 is not a digit of dc, and the automaton recognises the padded set of mobius instead: at base 3 with F = {1,2}, d = 1 and level = 3 it reads 8 where the true count is 14.
• The transfer matrix. T_d(r, r') = #{e < base : (de + r) mod base in F, floor((de + r)/base) = r'} and #{c < base^level : dc in S_F} = e_0 T_d^level 1_(Acc_d). Proved for a design carrying 0, path counting. Over base = 3, 4, 5, every F, every d <= 6 and every level <= 5 the identity holds in all 840 cases carrying 0 and fails in 399 of the 750 without it.
• Every column of T_d sums to |F|, at every base, digit set and d. Proved. The pairs (e, r) in [0, base) x [0, d) are in bijection with v = de + r in [0, d base) by the division algorithm; the column at r' counts the v with v - base r' in F, and [base r', base r' + base) lies inside [0, d base) for every r' < d. So the all-ones vector is a positive left eigenvector and the spectral radius of T_d is |F| for every d: a dilate carries the design's own mass exponent as its Perron root. The rows sum to g times #(F intersect (r + gZ)) with g = gcd(d, base), hence equal |F| when gcd(d, base) = 1, where #{c < base^level : dc in S_F} <= |F|^level with constant 1.
• Base powers are free. If 0 in F then M_F(x; base^j d) = M_F(x; d), since appending zero digits neither enters nor leaves S_F. Proved. At base 3 {0,1} the d = 3 column is the d = 1 column, M_F(3^12; 3) = 56 with peak 61.
• The matrix digit transform. sum of e(ct) over c < base^level with dc in S_F is e_0 M(t) M(base t) ... M(base^(level-1) t) 1_(Acc_d) with M(t)(r, r') = sum of e(et) over the digits e carrying r to r', and M(0) = T_d. Proved. This is the Mobius page's ladder prod_j g_F(base^j t) with the scalar digit symbol replaced by a matrix, and the replacement is the price of the route: an ordered product of non-commuting matrices does not factor, so the sup-over-shift l^1 exponent that carries a Type I estimate for a digit design has no scalar analogue here. The matrix gives the exact count, the exact mass constant and exact evaluation at any t, and no cancellation in mu.
• The mass constant is the accepting set. Conjecture under gcd(d, base Delta_F) = 1, with Delta_F the gcd of the differences of the digits in F. For gcd(d, base) = 1 both sums make T_d/|F| doubly stochastic, so the stationary law is uniform on each closed class, and where the carry chain is irreducible A_d(base^level)/|F|^level converges to #Acc_d/d = (A_F(d-1) + 1)/d = O(d^(alpha-1)), which is exactly the saving a level of distribution for S_F at the modulus d would give. Coprimality to the base alone is not enough: at base 3 with F = {0,2} and Delta_F = 2 the dilate d = 2 has T_2 = [[2,0],[0,2]], carry 1 unreachable from carry 0, counts 2, 4, 8, 16, 32, 64, 128, 256 at level = 1 to 8 and a constant of 1 against #Acc_2/2 = 1/2. Verified to three decimals at level = 24 at every coprime d printed, on both designs, both having Delta_F = 1; and the hypothesis is verified as a split over every base <= 7, every F carrying 0 and every 2 <= d <= 24 coprime to base at level = 400, 1747 agreements and 0 failures at gcd(d, Delta_F) = 1 against 0 agreements and 148 failures at gcd(d, Delta_F) > 1.
• The saving is not uniform in d. Refuted, by the base-power ladder: 0 in F makes (base^j)^(-1) S_F equal to S_F, so the constant at d = base^j is 1 at every j while the ceiling base^(j(alpha-1)) tends to 0, and A_d(x)/(d^(alpha-1) x^alpha) is at least base^(j(1-alpha)), unbounded. Off the ladder the base-smooth dilates are denser than the design in the same way: base 10 without 9 reads 1.1111, 1.1358, 1.1111, 1.1413, 1.0700, 1.0343 at d = 2, 4, 5, 8, 16, 32 against the ceilings 0.968781, 0.938537, 0.929003, 0.909237, 0.880851, 0.853352, and the accepting-set law fails there too. The last digit of an element of S_F is uniform on F and F is unbalanced modulo a prime dividing the base. It costs the converse its first hypothesis and not its conclusion: over the 29 base-smooth d <= 1000 at base 10 without 9 the constant lies in [0.9273, 1.1637] and over every d <= 200 its inflation over the value at the coprime part of d lies in [0.9375, 1.1413], bounded on the metered range and unmeasured past it.
• (U), the d-uniform bound |M_F(x; d)| = O_eps(d^((alpha-1)/2) x^(alpha/2 + eps)), is Refuted. For any design carrying 0 and 1, base powers being free gives M_F(x; base^j) = M_F(x), so (U) at d = base^j demands |M_F(x)| <= C_eps base^(j(alpha-1)/2) x^(alpha/2+eps) at every j, and alpha < 1 drives the right side to 0 at fixed x, forcing M_F identically zero against M_F(1) = 1. At base 3 {0,1} and x = 3^12 the left side is 56 at every j = 0 to 12 while the bound falls 64.0000 to 5.6187 over d = 3^0 to 3^12, the ratio climbing 0.875 to 9.967.
• The converse. Proved from (U'), |M_F(x; d)| = O_eps(d_base^((alpha-1)/2) x^(alpha/2 + eps)) uniform in d >= 1 and x >= 1, with d_base the part of d coprime to base: the same bound with the dilate's true mass constant, whose d = 1 case is exactly the square-root ceiling Theorem 3 delivers. Then G_F(Q) = O_eps(Q^(alpha + eps)) and sum_j delta_j^2 = O_eps(Q^(-1+eps)), the denominator lane's conjecture. Write d = a d_base and e = b e_base with a and b supported on the primes dividing base; the parts have disjoint prime support, so gcd(d,e) = gcd(a,b) gcd(d_base,e_base) and the kernel sum factors. Each term is at most gcd(d,e)^2 (d e)^(-1-alpha/2-eps) (d_base e_base)^((alpha-1)/2) Q^(alpha+2eps); the coprime factor carries exponent -3/2-eps and, with d_base = g u and e_base = g v, gcd(u, v) = 1, is at most zeta(1 + 2eps) zeta(3/2 + eps)^2; the base factor is prod over p | base of sum over i, j >= 0 of p^(2 min(i,j) - (i+j)s) with s = 1 + alpha/2 + eps, equal to prod over p | base of (1 + p^(-s))/((1 - p^(-s))(1 - p^(-alpha-2eps))) and finite because alpha > 0. And m_F(Q) >> Q^(1+alpha)/log log Q, the >> Q^alpha members of S_F in the top block below Q each exceeding Q/base with phi(b) >> b/log log b, so the rank form divides that down.
• The exponent (alpha-1)/2 on d_base is critical. Proved. At (alpha-1)/2 + delta with delta > 0 the coprime g sum becomes sum of g^(-1+2delta), of size Q^(2delta), and the conclusion weakens to G_F(Q) = O(Q^(alpha + 2delta + eps)) with no threshold; at delta = 0 it is the harmonic sum and only the eps closes it. The base factor never sees the exponent, so the refutation above does not touch this.
• It is one implication and not an equivalence. The reverse is unproved and fails by the natural route: the threshold gives |S_F(k, Q)| <= k (pi^2 G_F(Q)/6)^(1/2) termwise, and Mobius inversion of Theorem 1 gives d M_F(Q/d; d) = sum over c | d of mu(d/c) S_F(c, Q), hence only |M_F(Q/d; d)| <= (sigma(d)/d)(pi^2 G_F(Q)/6)^(1/2) << log log d times Q^(alpha/2+eps), which grows in d where (U') asks for d_base^(-1/2-eps) decay.
• The Mobius-free surrogate. Conjecture. M_F(Q/d; d) sums over exactly the m in S_F below Q divisible by d, so square-root cancellation in that mass is |M_F(Q/d; d)| <= N_F(Q; d)^(1/2+eps) with N_F(Q; d) = #{m in S_F : m <= Q, d divides m}, and under that hypothesis the converse reduces to B(Q) = sum over d, e of (gcd(d,e)^2/(d e)) sqrt(N_F(Q; d) N_F(Q; e)) being O(Q^(alpha+eps)), a divisor statement with no mu in it. It stays consistent where (U) does not, reading |M_F(Q/base^j)| <= A_F(Q/base^j)^(1/2+eps) at d = base^j, which is the d = 1 ceiling again. B(Q)/Q^alpha reads 12.5146, 17.8640, 24.7369, 31.5935, 39.0671 at Q = 3^4 to 3^8 with local exponents 0.955, 0.927, 0.854, 0.824 falling toward alpha = 0.630930; no exponent is claimed.
• Verified. The transfer matrix [[1,1],[1,1]] at base 3 {0,1} and d = 2, with both carries accepting, counts 2^level - 1 against literal enumeration of {c : 2c in S_F} at every level <= 12, both reading 4095 at x = 3^12 = 531441. Over d <= 64 on both designs no column of T_d is off |F|; rows are off |F| at 21 and 38 of the 64 and every one of those d shares a factor with the base. The falsification run meters (U') itself, by the ratio of max |M_F(y;d)| over y <= x to d_base^((alpha-1)/2) x^(alpha/2), which (U') asks to stay bounded in d, and it does not fire: at base 3 {0,1} and x = 3^12 the ratio reads 0.9531, 0.7991, 0.9531, 0.6054, 0.9883, 0.3580, 0.5504, 0.8269, 1.0535, 0.4431, 0.5528, 0.3828 at d = 1, 2, 3, 4, 5, 7, 8, 11, 13, 16, 22, 31, and at base 10 without 9 and x = 10^7 it reads 1.1276, 0.9264, 0.5523, 0.6173, 0.8583, 1.2702, 0.4594 at d = 1, 2, 3, 4, 5, 7, 11. Under (U)'s exponent the same ratio reads 1.1673 at d = 3 on base 3 against 1.0535 as the maximum over the coprime d. The raw readings log max |M_F(x;d)| over log x add nothing: 0.311823 at d = 1 and at most 0.292046 over the ten base 3 dilates, the d = 3 row being the d = 1 row rather than an independent reading, and 0.484570 at d = 1 against 0.489199 at d = 7 at base 10 with the x = 10^6 crossing reversing by x = 10^7; the local exponents swing over 0.24 to 0.845, so none of these readings is an exponent (verb_dilate).

WHAT IT PRINTS

• verb_denominator: the frequency-m table at m = 1, 2, 3, 4, 5, 6, 12 for base 3 {0,1} at Q = 2187, base 10 without 9 at Q = 1000 and the control at Q = 300, exact integer against literal sum; then the frequency-1 ladder to Q = 10^5 on base 3, Q = 10^4 on base 10 and on the control, with the per-denominator worst deviation, the denominator it sits at, and the count of denominators rounding to the wrong integer.
• verb_identity: the Fourier form against the truncated Fourier side with its tail bound at four settings; the rank form as an exact rational identity at the same four; the Edwards control at Q = 40; the backward inequality's ratio at six settings.
• verb_dilate: the d = 2 automaton at base 3 {0,1} with its transfer matrix, accepting carries and row and column sums, then the count against brute-force enumeration at every level <= 12; the column-sum law over d <= 64 on both designs with the count of rows off |F| and whether each such d shares a factor with the base; the accept-mass table K_d against #Acc_d/d and d^(alpha-1) at level = 24; the dilated meter at base 3 to 3^12 and base 10 to 10^7 with the mass, the endpoint, the peak, the exponent reading at x and at x/base, the ratio against the refuted bound and against (U), and the local exponents; the d = 1 against d = 2 ladder at base 3; and the Smith reduction B(Q) at Q = 3^4 to 3^8 with its three normalisations and its local exponent.
• verb_converse: the scope of the automaton, automaton against brute force over base = 3, 4, 5, every F, d <= 6, level <= 5, split on whether F carries 0; the mass constant against #Acc_d/d at level = 400 over every base <= 7, every F carrying 0 and every 2 <= d <= 24 coprime to base, split on gcd(d, Delta_F); the refutation table for the d-uniform bound at base 3 {0,1} and x = 3^12 over d = 3^0 to 3^12; and the base-smooth mass constants at base 10 without 9 over d <= 1000 with the inflation ratio over d <= 200.
• verb_strict: the divisor-sum identity's worst deviation at base 3 to 729 and base 10 to 200; the smallest Q with a nonzero imaginary part on each design; and the refutation ladder to Q = 3^11 and Q = 10^4 carrying card, Re, Im, |S_F^s|, |S_F^s|/card and all three candidates.

• The card column is the independent control: 278, 4286, 67561, 1080458 and 1830, 147096, 11890654 are the strict counts farey-discrepancy prints from a Mobius sieve that enumerates no fraction, and this study reaches them by literal enumeration.

RUN

• uv run python research/lab/py/restricted-franel/restricted_franel.py
• From the repository root. One core, 32.4 s summed over the five verbs: denominator 6.7 s, identity 10.8 s, strict 1.6 s, dilate 5.5 s, converse 7.8 s. Append denominator, identity, strict, dilate or converse for one.
• Domain: the frequency-1 identity to Q = 10^5 at base 3 {0,1} and Q = 10^4 at base 10 without 9 and the control; the frequency-m identity at seven frequencies; the Franel identity at Q <= 243; the strict refutation to Q = 3^11 and Q = 10^4; the dilate automaton over d <= 64, the dilated meter to x = 3^12 and x = 10^7, and the Smith reduction to Q = 3^8.
• The wall: the literal frequency-1 check at Q = 10^5 on base 10 without 9 costs 2.6e9 roots of unity, past the machine budget, so that rung is not walked.
• Nothing is written to disk.

WITNESSES

• Theorem 1: ladder_check and mertens_dilated, with literal_denominator as the multi-frequency route.
• Theorem 2: kernel_sum against fourier_side with the printed tail bound, and against farey_delta_square as an exact rational identity.
• Theorem 3: the ratio column of verb_identity.
• Theorem 4: strict_ramanujan_literal against strict_ramanujan_divisor, then strict_literal and strict_weights on the ladder.
• Theorem 5: dilate_matrix and dilate_accept built into automaton_count, against dilate_mask as the literal enumeration, with smith_bilinear over divisor_counts for the surrogate.
• Theorem 5, the hypotheses: brute_dilate against positive_count for the scope, digit_gap for the mass constant's split, and qfree for the coprime part in (U) and in the falsification ratio.
• The node counts: strict_literal's card against the published strict counts of farey-discrepancy.
• The Farey page THE RESTRICTED FRANEL IDENTITY, the objects and the identity: the dilated sums M_F(x; d), the frequency-m formula and its frequency-1 case, with the deviations 1.09e-11 at b = 86293 to Q = 10^5 at base 3 {0,1} and 1.36e-12 at b = 7247 to Q = 10^4 at base 10 without 9 and on the control, the Q = 10^5 rung on base 10 not walked, 0 wrong roundings, and the seven frequencies (Theorem 1).
• The Farey page THE RESTRICTED FRANEL IDENTITY, the two L^2 forms: G_F(Q), the Fourier form inside its tail bound and the rank form as exact rationals at the four settings, with the Edwards control G_F(40) = 62.310829 at m = 490 and sum delta^2 = 0.0104270117 (Theorem 2).
• The Farey page THE RESTRICTED FRANEL IDENTITY, the inequality and the implication: the false display's witnesses Q = 5 and Q = 37, 0 violations at every integer Q <= 2187 and Q <= 400, the peak 0.607927 at Q = 1 and the maxima 0.340071 at Q = 253, 0.137645 at Q = 221 and 0.086385 at Q = 114 (Theorem 3).
• The Farey page THE RESTRICTED FRANEL IDENTITY, the strict set: the divisor identity, the non-real sums at Q = 3 and Q = 10, the three killed candidates, the ratios 0.335693 to 0.346338 and 0.015138 to 0.011561, and the modulus 374203.231 against M_F(3^11) = -10 (Theorem 4).
• The Farey page THE RESTRICTED FRANEL IDENTITY, the dilates: the automaton and its accepting set, the column-sum law and the Perron root |F|, the matrix digit transform, the accept-mass readings, the base-smooth refutation, the converse under (U) with its critical exponent, the surrogate B(Q) and the falsification run (Theorem 5).