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 assembly

Statement

Assume AC. There is a separable reflexive real Banach space B, a dense linearly independent generator with property A, pairwise disjoint finite subsets Mm of that generator, and constants b>1, K>0 such that

∣Mm+1∣>∣Mm∣b

and every bounded finite-expansion T satisfies

∣Tr⁡~(Mm+1,T)−Tr⁡~(Mm,T)∣≤K∥T∥log⁡∣Mm∣.

Consequently the logarithmic finite-rank lower bound of Enflo's trace lemma holds on B.

Facts & Assumptions

[A1]
[L1]

Enflo's fixed-generator trace criterion converts the two displayed block hypotheses into the logarithmic finite-rank lower bound (Enflo's quantitative localized-trace obstruction).

[L2]

The two adjacent Walsh layers satisfy the exact symmetry trace estimate with factor 2/n (Enflo's Walsh-block estimates and symmetry average).

[L3]

Under AC, the real dominated Hahn--Banach theorem supplies Hahn--Banach; under Hahn--Banach, a closed subspace of a reflexive Banach space is reflexive (Hahn-Banach dominated extension theorem for real vector spaces, Closed subspaces of reflexive spaces are reflexive).

[L4]

Property A and localized traces have their fixed-generator meanings (Enflo finite-expansion and localized-trace system).

Proof

technique · direct

Given: The objects and hypotheses in the Statement.

1.1given

Choose real numbers 1<b<α<γ with α<(2+γ)/(1+γ). Put

nm=⌊αm⌋,tm=(2nmnm−1),km=⌊tmγ⌋.

After deleting finitely many initial indices, all are positive and strictly increasing. Let Km be the disjoint union of km copies Km,j of Z22nm, and let B1=(⨁mC(Km))2. [explicit parameters]

2.1algebra

The dual-coordinate argument identifies [given, step 1.1] B1∗ with (⨁mC(Km)∗)2: finite Hölder gives one inequality, and finite-dimensional compactness supplies norming vectors for each finite partial sum and hence the reverse. Applying the same argument to the bidual, and using finite-dimensional reflexivity of each C(Km), makes the canonical map onto. Thus B1 is reflexive. It is separable because it is the completion of a countable union of finite-dimensional rational spans.

3.1algebra

In C(Km)⊕C(Km+1) choose a set Mm of kmtm vectors so [given, step 2.1] that: (i) each vector has exactly one nonzero Km,j component, an element of Wnm+1; (ii) its components in Km+1,j are zero or elements of Wnm+1−1, and every such Walsh function occurs; and (iii) two distinct vectors never share the same nonzero component. Equivalently Mm is partitioned into Mm,j of size tm and is equipped with subsets Nm,j⊆Mm of size tm+1, with the Mm,j pairwise disjoint and the Nm,j linked to the next layer. No covering assertion is imposed; points outside the selected incidence region have multiplicity zero.

4.1givenL4A1L3step 3.1

Require in addition the three incidence bounds

∣Nm,i∩Nm,j∣≤2tm+1nm+1(i≠j),

∣Nm,j∩Mm,i∣≤min⁡{tm+1nm+1,tmnm},

and, with σ(e)=∣{j:e∈Nm,j}∣,

∑e∈Mm∣1kmtm−σ(e)km+1tm+1∣≤1nm+1.

These are Enflo's conditions 4--6. Let B be the closed span in B1 of ⋃mMm. The unique lowest nonzero block proves independence. To check [L4]'s property A, fix a finite combination x=∑eaee, a participating generator e0, and one component block Kr,i. If e0 vanishes there, the componentwise estimate is trivial. Otherwise the nonzero restrictions of the participating generators are distinct Walsh characters: property (iii) handles characters from the same Mm, and the two possible adjacent layers have different degrees. Walsh orthogonality makes the normalized L2 norm of x∣Kr,i at least ∣ae0∣, so its supremum norm is at least ∣ae0∣ as well. Taking the maximum over i for each C(Kr) coordinate and then the Hilbertian sum over r gives ∥x∥≥∣ae0∣∥e0∥. Thus property A holds with the full generator norm, including both adjacent nonzero coordinates. Countably many generators give separability, and [A1] is used through [L3] to make the closed subspace B reflexive. [A1, L3, L4, steps 2.1, 3.1]

5.1givenL4step 4.1

For a finite-expansion T, condition 6 and property A give

∣Tr⁡~(Mm,T)−1km+1∑j=1km+1Tr⁡~(Nm,j,T)∣≤∥T∥nm+1.

Indeed the left side is the weighted sum of the diagonal coefficients a(e), each bounded by ∥T∥ via property A, and condition 6 is exactly the total weight error. [L4, step 4.1]

6.1givenL2step 5.1

Fix j and put E=[Nm,j∪Mm+1,j]. Delete from each finite expansion of Te the terms outside this generator set, obtaining T′:E→E. The localized traces of T and T′ on the two displayed sets agree, and T′x=Tx on Km+1,j. Restriction to that block identifies E with the two Walsh layers in [L2]. Write

∥ ⁣∣x∣ ⁣∥=max⁡p∈Km+1,j∣x(p)∣.

The vector supplied by [L2] therefore satisfies

∣Tr⁡~(Nm,j,T)−Tr⁡~(Mm+1,j,T)∣≤2nm+1∥ ⁣∣T′x∣ ⁣∥∥ ⁣∣x∣ ⁣∥.

Its values on every other Km+1,i have modulus at most ∣Nm,i∩Nm,j∣/tm+1≤2/nm+1 by condition 4. Its values on Km,i and Km+2,i have modulus at most 1/nm+1 by the two parts of condition 5, while [L2] gives ∥ ⁣∣x∣ ⁣∥≥2/nm+1. Thus the middle block has sup norm ∥ ⁣∣x∣ ⁣∥, each adjacent outer block has sup norm at most half of that, and all other blocks vanish. Since the ambient sum is Hilbertian, ∥x∥≤3/2 ∥ ⁣∣x∣ ⁣∥<2∥ ⁣∣x∣ ⁣∥. Also ∥ ⁣∣T′x∣ ⁣∥≤∥Tx∥≤∥T∥∥x∥. Hence

∣Tr⁡~(Nm,j,T)−Tr⁡~(Mm+1,j,T)∣≤4∥T∥nm+1.

Averaging in j and combining with step 5.1 yields

∣Tr⁡~(Mm+1,T)−Tr⁡~(Mm,T)∣≤5∥T∥nm+1.

[L2, steps 3.1, 4.1, 5.1]

7.1givenstep 6.1

It remains to realize the incidences. Put

Lm=⌊kmtm+1⌋,νm=⌊km+1Lmtm⌋,

and identify each Walsh layer with a cyclic group of the corresponding cardinality. Inside {1,…,Lmtm+1}×Ztm, enumerate

(j,jρ+k),ρ=0,1,2,…,k=0,…,tm−1,j=1,…,Lmtm+1,

first by increasing ρ, then k, then j. Take the first km+1 successive blocks of tm+1 points as Nm,1,…,Nm,km+1. Each such block meets every Mm,i={i}×Ztm in at most one point, so condition 5 holds eventually. [explicit lexicographic construction]

8.1givenstep 7.1

Put Am={1,…,Lmtm+1}×Ztm and qm=km+1/(Lmtm). Every point of Am occurs once at each complete ρ-level, so its multiplicity σ(e) among the selected blocks differs from qm by at most one; points outside Am have multiplicity zero. Since ∣Am∣=Lmtm+1tm,

∑e∈Mm∣1kmtm−σ(e)km+1tm+1∣≤2tm+1km+kmtmkm+1tm+1.

Both terms are o(1/nm+1): their exponential orders are respectively tmα−γ+o(1) and tm(γ+1)(1−α)+o(1). Thus condition 6 holds after discarding finitely many indices. [step 1.1, balanced incidence count]

8.2givenstep 1.1step 7.1

Suppose two distinct selected blocks share a point represented both as (j,jρ1+k1) and (j,jρ2+k2). The injectivity at a fixed ρ-level gives ρ1≠ρ2, and ∣ρ1−ρ2∣≤νm. For any other common point whose first coordinate differs by μ, congruence in Ztm gives

tm∣μ(ρ1−ρ2),μ≥tm∣ρ1−ρ2∣≥tmνm.

Moreover

tmνm∼Lmtm2km+1∼kmtm2tm+1km+1=tmγ+2−α(γ+1)+o(1).

The exponent is positive precisely because α<(2+γ)/(1+γ), so eventually tm/νm>nm+1. The common first coordinates lie in an interval of length less than tm+1 and are more than nm+1 apart. There are therefore at most 1+tm+1/nm+1≤2tm+1/nm+1 of them. This proves condition 4. Together with steps 7.1--8.1, all three incidence conditions hold after a finite reindexing. [step 1.1, finite arithmetic count, Stirling estimate]

9.1L1step 1.16.1algebra∎

Finally [given, L1, step 6.1, step 8.2] log⁡∣Mm∣=log⁡(kmtm)∼(γ+1)(2log⁡2)nm. Therefore ∣Mm+1∣>∣Mm∣b eventually and 5/nm+1≤K/log⁡∣Mm∣ for one constant K. Step 6.1 supplies the trace hypothesis, so [L1] gives the claimed logarithmic finite-rank lower bound.

Depends on

Used by

Dependency tree · two levels

17 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