10.14. QuantumBlockEncoding/HermitePolynomialPreparation.lean🔗

1 explicit public declarations, in source order.

Theorem10.14.1

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “exists polynomial preparation”; the hypotheses and conclusion in the code panel fix its exact scope. For 'n+1' data qubits, the additional register has 'ceil(log2(2*k+6))' wires.

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Why it is in this chapter. Paper-facing backend models, source-specific Hermite constructions, and concrete State Preparation / Robin example artifacts.

Technical source note. For 'n+1' data qubits, the additional register has 'ceil(log2(2*k+6))' wires. It is returned completely to zero, without measurement or postselection. Every primitive instruction is counted. For fixed smoothing order the proved gate bound is linear in data width.

Declaration kind. theorem.

Source: QuantumBlockEncoding/HermitePolynomialPreparation.lean:22. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.14.1●1 theorem

theoremdefined in QuantumBlockEncoding/HermitePolynomialPreparation.lean

complete

theorem QuantumBlockEncoding.HermitePolynomialPreparation.exists_polynomial_preparation
  (k n : ℕ) (L : ℝ) (hL : 0 < L) :
  ∃ circuit,
    circuit.gateCount ≤ 48 * (n + 1) * (2 * k + 6) ^ 3 ∧
      circuit.resource.oracleCalls = 0 ∧
        QuantumBlockEncoding.evalPrimitiveCircuit circuit ∈
            Matrix.unitaryGroup
              (QuantumBlockEncoding.PrimitiveBasis
                (n + 1 +
                  QuantumBlockEncoding.HermiteFiniteChain.bondQubits k))
              ℂ ∧
          ∀ (x : QuantumBlockEncoding.PrimitiveBasis (n + 1))
            (b :
              QuantumBlockEncoding.PrimitiveBasis
                (QuantumBlockEncoding.HermiteFiniteChain.bondQubits k)),
            (QuantumBlockEncoding.evalPrimitiveCircuit circuit
                (Fin.append x b) fun x => 0) =
              if b = fun x => 0 then
                QuantumBlockEncoding.HermiteStatePreparation.normalizedAmplitude
                  k (n + 1) L
                  ((QuantumBlockEncoding.primitiveBasisLEEquiv (n + 1))
                    x)
              else 0

theorem QuantumBlockEncoding.HermitePolynomialPreparation.exists_polynomial_preparation
  (k n : ℕ) (L : ℝ) (hL : 0 < L) :
  ∃ circuit,
    circuit.gateCount ≤
        48 * (n + 1) * (2 * k + 6) ^ 3 ∧
      circuit.resource.oracleCalls = 0 ∧
        QuantumBlockEncoding.evalPrimitiveCircuit
              circuit ∈
            Matrix.unitaryGroup
              (QuantumBlockEncoding.PrimitiveBasis
                (n + 1 +
                  QuantumBlockEncoding.HermiteFiniteChain.bondQubits
                    k))
              ℂ ∧
          ∀
            (x :
              QuantumBlockEncoding.PrimitiveBasis
                (n + 1))
            (b :
              QuantumBlockEncoding.PrimitiveBasis
                (QuantumBlockEncoding.HermiteFiniteChain.bondQubits
                  k)),
            (QuantumBlockEncoding.evalPrimitiveCircuit
                circuit (Fin.append x b)
                fun x => 0) =
              if b = fun x => 0 then
                QuantumBlockEncoding.HermiteStatePreparation.normalizedAmplitude
                  k (n + 1) L
                  ((QuantumBlockEncoding.primitiveBasisLEEquiv
                      (n + 1))
                    x)
              else 0

For `n+1` data qubits, the additional register has
`ceil(log2(2*k+6))` wires. It is returned completely to zero, without
measurement or postselection. Every primitive instruction is counted.
For fixed smoothing order the proved gate bound is linear in data width.