ExampleConstruction: AI-adaptedVerification: AI-generatedPipeline-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.

Simon decision for n equals two

Example

Take $n = 2$ , so $V_{2} = F_{2}^{2}$ , and consider a NO function with mask $s = 01$ . Then $s^{⊥} = {00, 10}$ , so every Simon sample lies in this one-dimensional subspace and the rank test rejects. On a YES permutation, the algorithm takes $m = n + 2 = 4$ independent uniform samples. Its exact probability of failing to span is $23 / 128$ , and the general union bound is $3 / 16$ .

Facts & Assumptions

Given: The algorithm and its output law from Simon promise decision by sampled rank and Simon rank test correctness and linear query cost; $s = 01$ ; and four independent uniform samples in $V_{2}$ in the YES case.

[F1]

Simon rank test correctness and linear query cost: every NO sample is orthogonal to $s$ , every YES sample is uniform on $V_{n}$ , and the YES rank-failure bound for $n = 2, m = 4$ is $(2^{2} - 1) 2^{- 4} = 3 / 16$ .

[F2]

Finite probability spaces, outcome weights, events, and event probabilities: a finite probability space assigns nonnegative weights summing to one to its outcomes; an event's probability is the sum of its outcome weights.

Verification

1.1givenF1algebra

The dot product with $s = 01$ is the second coordinate, so $s^{⊥} = {00, 10}$ . Its span is itself and has rank one. Hence four NO samples cannot have rank two, and the algorithm rejects with probability one.

1.2givenconstructalgebra

In $V_{2}$ , the three one-dimensional subspaces are ${00, 10}$ , ${00, 01}$ , and ${00, 11}$ . Four vectors fail to span exactly when all four lie in one of these three subspaces. Each corresponding set of four-tuples has $2^{4} = 16$ elements; every pairwise intersection and the triple intersection consist only of $(00, 00, 00, 00)$ . Inclusion-exclusion therefore gives $3 \cdot 16 - 3 \cdot 1 + 1 = 46$ failing tuples out of $4^{4} = 256$ .

2.1givenF1F2step 1.2algebra∎

By the independent runs in the given algorithm and the uniform YES law in [F1], each ordered four-tuple has weight $(1 / 4)^{4} = 1 / 256$ . Summing these weights by [F2], the exact failure probability is $46 / 256 = 23 / 128$ . The union bound is $3 \cdot 16 / 256 = 3 / 16$ , agreeing with [F1] and strictly below $1 / 4$ . There are exactly four oracle runs by the algorithm's definition.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

19 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

Ronald de Wolf, Quantum Computing: Lecture Notes, Chapter 3, Section 3.2 (standard reference, not scraped)