QuantumBlockEncoding/HermitePolynomialResources.lean

Lean checks the proposition indexed as “exists polynomial resources”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem exists_polynomial_resources (k n : Nat) (L : ℝ) (hL : 0 < L) :
    ∃ circuit : PrimitiveCircuit ((n + 1) + bondQubits k),
      circuit.gateCount ≤ 48 * (n + 1) * (2 * k + 6) ^ 3 ∧
      circuit.resource.depth ≤ 48 * (n + 1) * (2 * k + 6) ^ 3 ∧
      circuit.resource.oracleCalls = 0 ∧
      evalPrimitiveCircuit circuit ∈
        _root_.Matrix.unitaryGroup (PrimitiveBasis ((n + 1) + bondQubits k)) ℂ ∧
      ∀ (x : PrimitiveBasis (n + 1)) (b : PrimitiveBasis (bondQubits k)),
        evalPrimitiveCircuit circuit (Fin.append x b) (fun _ => 0) =
          if b = (fun _ => 0) then
            HermiteStatePreparation.normalizedAmplitude k (n + 1) L

commit-pinned source · Verso Blueprint panel