ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedprecheck pass

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.

Small Johnson-walk spectra and marked fractions

Example

For $N = 5, r = 2$ and $N = 6, r = 3$ , compute the lazy Johnson spectrum, its gap, and the marked fraction from one fixed colliding pair. Also compute the marked fraction for two disjoint colliding pairs in the $N = 6, r = 3$ case. In the one-pair cases assume that the named pair is the only collision pair; in the two-pair case assume that the named disjoint pairs are the only collision pairs, so their common values are distinct and all remaining values are distinct from each other and from those common values.

Facts & Assumptions

Given: The lazy Johnson transition and formulas in Element-distinctness Johnson walk and value access and Spectrum of the lazy Johnson walk.

[F1]

Spectrum of the lazy Johnson walk: $λ_{j} = 1 - j (N + 1 - j) / (2 r (N - r))$ with multiplicity $(\binom{N}{j}) - (\binom{N}{j - 1})$ , for $0 \leq j \leq r$ .

[F2]

Element-distinctness O(N^{2/3}) query bound: one fixed collision pair marks a fraction at least $r (r - 1) / [N (N - 1)]$ of all $r$ -subsets.

[F3]

Element-distinctness Johnson walk and value access: the state space consists of all $r$ -subsets and marked states contain at least one collision pair.

Proof

1.1F1F2F3algebra

For $N = 5, r = 2$ , the denominator in [F1] is $2 r (N - r) = 12$ . At $j = 0, 1, 2$ , the eigenvalues are $1$ , $1 - 5 / 12 = 7 / 12$ , and $1 - 8 / 12 = 1 / 3$ . Their multiplicities are $1$ , $(\binom{5}{1}) - (\binom{5}{0}) = 4$ , and $(\binom{5}{2}) - (\binom{5}{1}) = 5$ , totaling $10 = (\binom{5}{2})$ . Thus the nonconstant top eigenvalue is $7 / 12$ and the gap is $5 / 12$ . An independent finite check enumerates the ten $2$ -subsets lexicographically and forms the integer matrix $B_{S T} = 12 P (S, T)$ : its diagonal is $6$ , and its off-diagonal entry is $1$ exactly when $∣ S \cap T ∣ = 1$ . Exact determinant expansion gives $\det (x I - B) = (x - 12) (x - 7)^{4} (x - 4)^{5}$ , confirming the scaled spectrum. A fixed colliding pair lies in $(\binom{3}{0}) = 1$ of the $10$ subsets, so its marked fraction is $1 / 10$ .

1.2F1F2F3algebra

For $N = 6, r = 3$ , the denominator is $18$ . Formula [F1] gives eigenvalues $1, 2 / 3, 4 / 9, 1 / 3$ for $j = 0, 1, 2, 3$ . Their multiplicities are $1, 5, 9, 5$ , totaling $20 = (\binom{6}{3})$ . The independent exact check enumerates the $20$ triples and forms $B_{S T} = 18 P (S, T)$ with diagonal $9$ and off-diagonal $1$ exactly when $∣ S \cap T ∣ = 2$ ; fraction-free determinant expansion gives $\det (x I - B) = (x - 18) (x - 12)^{5} (x - 8)^{9} (x - 6)^{5}$ , confirming those eigenvalues and multiplicities. The gap is $1 - 2 / 3 = 1 / 3$ . A fixed pair belongs to $(\binom{4}{1}) = 4$ of the $20$ subsets, hence has marked fraction $1 / 5$ .

2.1F2F3step 1.2algebra∎

Under the stated assumption that the only collision pairs are the two named disjoint pairs, each pair is contained in four $3$ -subsets, and no $3$ -subset contains both pairs because their union has four elements. The two marked families are therefore disjoint and their union has $4 + 4 = 8$ subsets, a fraction $8 / 20 = 2 / 5$ . The value exceeds the one-pair lower bound $1 / 5$ , as required by the “at least” in [F2]. Without the exclusivity assumptions, the counted families still give lower bounds for the marked fraction, but extra collisions can increase it.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

16 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

Andris Ambainis, Quantum walk algorithm for element distinctness, §§3–4 (standard reference, not scraped)
Andrew M. Childs, Lecture Notes on Quantum Algorithms, Chapter 20, §20.2 (standard reference, not scraped)