Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-09-14
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Enflo's Walsh-block estimates and symmetry average

Statement

Fix a positive integer n. Let H=Z22n, let Rj(a)=(1)aj, and, for 0m2n, let Wm be the products of m distinct Rj and put Fm=wWmw. If a is the number of nonzero coordinates of a, then

  1. Fm(0)=Fm=(2nm);
  2. if a=1, then Fm(a)=(1m/n)Fm;
  3. if 0<a<2n, then Fn1(a)=Fn+1(a)n1Fn1;
  4. if b is the coordinatewise complement of a, then Fm(a)=(1)mFm(b).

Let G be the finite group of sup-norm isometries generated by coordinate permutations and translations on E=span(Wn1Wn+1). For every linear T:EE there is UG such that, with

f=Fn1/Fn1Fn+1/Fn+1,

Tr~(Wn1,T)Tr~(Wn+1,T)2nTUfUf.

Facts & Assumptions

[L1]

Normalized localized trace means the average of diagonal coefficients in the displayed fixed basis (Enflo finite-expansion and localized-trace system).

Proof

technique · direct

Given: The objects and hypotheses in the Statement.

1.1

Every wWm equals one at zero, and there are [given] (2nm) such products; the triangle inequality proves item 1. If a=1, exactly (2n1m1) summands change sign, so Fm(a)=(2nm)2(2n1m1)=(1m/n)(2nm). This proves item 2.

algebra
2.1

Multiplying the choices coordinatewise gives the generating identity

givenstep 1.1

m=02nzmFm(a)=(1z)a(1+z)2na.

If b is the coordinatewise complement of a, then each Walsh monomial of degree m changes by (1)m, which proves item 4. The same generating polynomial also satisfies

z2nPa(1/z)=(1)aPa(z),Pa(z):=(1z)a(1+z)2na.

Comparing reciprocal coefficients gives

F2nm(a)=(1)aFm(a),

and in particular Fn+1(a)=(1)aFn1(a). [finite product, coefficient comparison]

3.1

Put r=a. Cauchy's coefficient formula on the unit circle gives

givenstep 2.1

Fm(a)=22n2πππ(i)rei(nm)θsinr(θ/2)cos2nr(θ/2)dθ.

The reciprocal identity in step 2.1 gives Fn1(a)=Fn+1(a). Taking absolute values in the integral gives

Fn±1(a)22nπIr,Ir:=0πsinr(θ/2)cos2nr(θ/2)dθ.

Here I2=I2n2 by the substitution θπθ. When n3 and 2<r<2n2, put λ=(2n2r)/(2n4). The integrand defining Ir is

(sin2(θ/2)cos2n2(θ/2))λ(sin2n2(θ/2)cos2(θ/2))1λ,

so weighted Hölder gives IrI2λI2n21λ=I2. For a vector e of weight two, the endpoint calculation in the same Cauchy formula gives (22n/π)I2=Fn(e), and direct coefficient comparison gives

Fn(e)=(2n2n)2(2n2n1)+(2n2n2)=12n1(2nn)1n(2nn1)

for n2. The weights r=1 and r=2n1 follow from item 2 and complementation; r=2 and r=2n2 follow from the endpoint estimate. For n=1, the only intermediate weight is r=1, already covered by item 2. This proves item 3 in every case. [step 2.1, coefficient integral, weighted Hölder, binomial arithmetic]

4.1

Average T over the finite group: T~=G1UGU1TU. Coordinate permutations and translations permute each Walsh layer up to signs, so [L1] gives Tr~(Wn±1,T~)=Tr~(Wn±1,T), and the group average commutes with every element of G.

givenL1step 3.1

Write the matrix of T~ in the Walsh basis. For two distinct Walsh characters v,w, choose a translation Ut for which Utv=v(t)v and Utw=w(t)w have opposite signs. Commutation with Ut forces the (v,w) matrix coefficient of T~ to be its own negative, hence to vanish. Thus T~ is diagonal in the Walsh basis. Coordinate permutations act transitively on each Wn±1, so its diagonal coefficients have constant values λ on Wn1 and λ+ on Wn+1. Consequently

T~f=λFn1Fn1λ+Fn+1Fn+1,

and evaluation at zero gives

Tr~(Wn1,T)Tr~(Wn+1,T)T~f.

[L1, finite group average, Walsh orthogonality]

5.1

The average defining T~f implies that some UG has [given, step 4.1] TUfT~f. Items 1, 3, and 4 give f2/n, while item 2 gives equality at every point of weight one. Hence f=2/n>0. Since U is an isometry, Uf=2/n. Combining these facts with step 4.1 gives the displayed bound.

step 3.14.1algebra

Depends on

Used by

Dependency tree · two levels

2 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources