A SUNTF_R(2, 5, 3) exists

W. J. Brinkley, M. Fickus, J. Jasper and D. G. Mixon, Incoherent filter banks, arXiv:2610.05302v1, Section 4, Example 4.4, asks whether a SUNTF_R(2, 5, 3) exists. The last paragraph states:

We do not yet know whether a SUNTF_R(2, 5, 3) exists, and we leave this for future research.

Definition 3.2 requires each of the R layers to be a unit norm tight frame in dimension D and requires the averaged squared inner products between every two distinct columns to be constant.

The present result settles the concrete real instance by an explicit exact construction.

Example 4.4 records the SUNTF_R(2, 5, 3) case as open. The formalization uses the real field and the definitions in the paper, including repeated vectors within a layer.

Set u = √(3/8) and v = √(5/8). The three layers have columns (1,0), (u, s_{r,1}v), (u, s_{r,2}v), (u, s_{r,3}v), (u, s_{r,4}v), with sign words (+,−,−,+), (+,−,+,−), and (+,+,−,−). Each layer is unit norm and tight with frame bound 5/2. Across the three layers, the sign words of the four non-anchor columns, namely (+,+,+), (−,−,+), (−,+,−), (+,−,−) (each of length three), agree pairwise in exactly one position, so the averaged squared inner products are 3/8 for every pair of distinct columns.

The construction would fail if a layer were not unit norm tight or if any ordered pair of distinct columns had an averaged squared inner product other than 3/8. The Lean proof checks all finite cases exactly.

Lean source: D5/S3/QuantumBounds/Designs/StratifiedTightFrameTwoFiveThree.lean. The theorem result : ¬ claim is equivalent to the existence statement in the encoded claim. Its proof uses only pinned Mathlib declarations and has no additional axioms beyond the standard Lean environment.

theorem; settlement Proved.

What the settlement shows

• Proved (Lean): a SUNTF_R(2,5,3) exists.
• Proved (mathematical consequence): with the paper's SUNTF_R(2,5,2), SUNTF_R(2,5,5) and stacking (Theorem 4.1(d)), SUNTF_R(2,5,R) exists exactly for R ≥ 2. R = 1 is an ETF_R(2,5), excluded by Gerzon's bound. Thus the threshold of Problem 4.3 for (R,2,5) is 2, not 4.
• Computed: across the three layers, the four non-anchor columns have sign words (+,+,+), (−,−,+), (−,+,−), (+,−,−), each of length three. These agree pairwise in exactly one position, a code with constant distance 2. This makes the layer averages flat.
• Open: Problem 4.3 in general for other D and N over R is not settled by this result.

The general classification beyond the stated (D,N)=(2,5) instance is not claimed here. The interpretation of the stacking result and Gerzon's bound is the mathematical consequence recorded above; only the concrete existence statement is kernel-checked in this module.