ExampleConstruction: Literature-sourcedVerification: AI-generatedPipeline-generated

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.

Dual adversary certificate for OR_N

Example

For the partial OR problem $D = {0, e_{1}, \dots, e_{N}}$ , define $v_{0, i} = N^{- 1 / 4}$ and $v_{e_{j}, i} = N^{1 / 4} 1 [i = j]$ . This is a balanced dual certificate with $C_{0} = C_{1} = \sqrt{N}$ . The matrix with only the symmetric edges $(0, e_{j})$ has norm $\sqrt{N}$ and each filtered norm 1. Hence ${Adv}^{\pm} ({O R}_{N}) = \sqrt{N} .$

Facts & Assumptions

Given: The partial Boolean function OR_N on the zero string and the N unit vectors.

[F1]

Finite Boolean query problem and error model for adversary bounds: OR_N is the finite Boolean query problem on the declared domain.

[F2]

Input-mismatch masks and entrywise filtering: Δ_i marks exactly the pairs that differ in bit i.

[F3]

General adversary matrix and spectral bound: a real symmetric opposite-output Γ certifies its norm ratio as a lower bound on Adv±.

[F4]

Dual vector formulation of the general adversary bound: a vector certificate of cost C gives Adv±≤C, and the optimum is attained.

Verification

1.1givenF1F2F4construct

Let D={0,e_1,…,e_N}⊂{0,1}^N and f(x)=OR_N(x). For every i set v_{0,i}=N^{-1/4} and v_{e_j,i}=N^{1/4}δ_{ij} in the one-dimensional real space. If x=0,y=e_j, the only mismatch is coordinate j and the corresponding product is 1. If x=e_j,y=e_k with j≠k, the mismatch coordinates are j,k and both products vanish. Reverse pairs give the same real values. Thus all constraints in [F4] hold.

2.1givenF4step 1.1algebra

The cost on the unique 0-input is Σ_iN^{-1/2}=√N. On each 1-input e_j the cost is Σ_iN^{1/2}δ_{ij}=√N. Hence Adv±(OR_N)≤√N by [F4].

3.1givenF2F3step 2.1algebra∎

For the reverse bound, let Γ have Γ_{0,e_j}=Γ_{e_j,0}=1 for every j and all other entries zero. Its nonzero block is the all-ones 1×N matrix, whose singular value is √N, so ||Γ||=√N. For each i, Γ∘Δ_i retains only the two entries joining 0 and e_i and has norm 1. Therefore [F3] gives Adv±(OR_N)≥√N; equality follows.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

18 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

Andrew M. Childs, Lecture Notes on Quantum Algorithms (17 April 2025) (standard reference, not scraped)
Ronald de Wolf, Quantum Computing: Lecture Notes, arXiv:1907.09415v6 (standard reference, not scraped)