Papers · State Preparation · Structured benchmark formalized
Lov Grover, Terry Rudolph · 2002. This is a source-facing partial reproduction page: it separates the paper statement, the finite Lean surface already closed in ASPBE, and the paper-wide work still queued.
Source contract
Source anchors. Eq. (1) Eq. (3) Eq. (5) Eq. (6)
What these source locations say. Eq. (1) is the target probability-amplitude state; Eq. (3) gives the recursive probability refinement; Eq. (5)–(6) turn the coherently computed split angle into a controlled rotation.
Formalized now
An exact two-bit product distribution, a typed generic binary-tree circuit and typed factorized circuit preparing the same target, and a Lean-certified resource improvement from (5,4,0,0) to (2,1,0,0).
These declarations are the proof authority for the finite theorem or resource lemma described above.
QuantumBlockEncoding.StatePreparationBenchmarks.groverRudolphProductTarget_normalizedQuantumBlockEncoding.StatePreparationBenchmarks.groverRudolphFactorized_prepares_targetQuantumBlockEncoding.StatePreparationBenchmarks.groverRudolphTree_prepares_targetQuantumBlockEncoding.StatePreparationBenchmarks.groverRudolphTreeVerified_costQuantumBlockEncoding.StatePreparationBenchmarks.groverRudolphFactorizedVerified_costQuantumBlockEncoding.StatePreparationBenchmarks.groverRudolphFactorized_betterThan_treePaper reproduction boundary
The general efficiently-integrable recursive probability-loading theorem and an end-to-end arithmetic/integration oracle compiler.
Status rule. A finite witness, typed circuit, or resource lemma is not silently promoted to the source paper's arbitrary-width or asymptotic theorem.