10.1. QuantumBlockEncoding/ConstructiveHermitePreparation.lean🔗

10 explicit public declarations, in source order.

Definition10.1.1

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “normalized source”. Normalize the formula-derived cores using the local norm, not a full sample sum.

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

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

Technical source note. Normalize the formula-derived cores using the local norm, not a full sample sum.

Declaration kind. def.

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

Lean code for Definition10.1.1●1 definition

defdefined in QuantumBlockEncoding/ConstructiveHermitePreparation.lean

complete

def QuantumBlockEncoding.ConstructiveHermitePreparation.normalizedSource
  (k n : ℕ) (L : ℝ) :
  QuantumBlockEncoding.TensorTrainCanonical.Chain (n + 1) 1 1

def QuantumBlockEncoding.ConstructiveHermitePreparation.normalizedSource
  (k n : ℕ) (L : ℝ) :
  QuantumBlockEncoding.TensorTrainCanonical.Chain
    (n + 1) 1 1

Normalize the formula-derived cores using the local norm, not a full sample sum.

Theorem10.1.2

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “normalized source eq source”; the hypotheses and conclusion in the code panel fix its exact scope.

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. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. theorem.

Source: QuantumBlockEncoding/ConstructiveHermitePreparation.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.1.2●1 theorem

theoremdefined in QuantumBlockEncoding/ConstructiveHermitePreparation.lean

complete

theorem QuantumBlockEncoding.ConstructiveHermitePreparation.normalizedSource_eq_source
  (k n : ℕ) (L : ℝ) (hL : 0 < L) :
  QuantumBlockEncoding.ConstructiveHermitePreparation.normalizedSource k
      n L =
    QuantumBlockEncoding.HermiteFiniteChain.sourceChain k n L

theorem QuantumBlockEncoding.ConstructiveHermitePreparation.normalizedSource_eq_source
  (k n : ℕ) (L : ℝ) (hL : 0 < L) :
  QuantumBlockEncoding.ConstructiveHermitePreparation.normalizedSource
      k n L =
    QuantumBlockEncoding.HermiteFiniteChain.sourceChain
      k n L

Theorem10.1.3

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “normalized source max bond”; the hypotheses and conclusion in the code panel fix its exact scope.

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. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. theorem.

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

Lean code for Theorem10.1.3●1 theorem

theoremdefined in QuantumBlockEncoding/ConstructiveHermitePreparation.lean

complete

theorem QuantumBlockEncoding.ConstructiveHermitePreparation.normalizedSource_maxBond
  (k n : ℕ) (L : ℝ) :
  QuantumBlockEncoding.TensorTrainCanonical.maxBond
      (QuantumBlockEncoding.ConstructiveHermitePreparation.normalizedSource
        k n L) ≤
    2 * k + 6

theorem QuantumBlockEncoding.ConstructiveHermitePreparation.normalizedSource_maxBond
  (k n : ℕ) (L : ℝ) :
  QuantumBlockEncoding.TensorTrainCanonical.maxBond
      (QuantumBlockEncoding.ConstructiveHermitePreparation.normalizedSource
        k n L) ≤
    2 * k + 6

Theorem10.1.4

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “normalized source normalized”; the hypotheses and conclusion in the code panel fix its exact scope.

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. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. theorem.

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

Lean code for Theorem10.1.4●1 theorem

theoremdefined in QuantumBlockEncoding/ConstructiveHermitePreparation.lean

complete

theorem QuantumBlockEncoding.ConstructiveHermitePreparation.normalizedSource_normalized
  (k n : ℕ) (L : ℝ) (hL : 0 < L) :
  ∑ x,
      QuantumBlockEncoding.TensorTrainCanonical.contract
          (QuantumBlockEncoding.ConstructiveHermitePreparation.normalizedSource
            k n L)
          x 0 0 ^
        2 =
    1

theorem QuantumBlockEncoding.ConstructiveHermitePreparation.normalizedSource_normalized
  (k n : ℕ) (L : ℝ) (hL : 0 < L) :
  ∑ x,
      QuantumBlockEncoding.TensorTrainCanonical.contract
          (QuantumBlockEncoding.ConstructiveHermitePreparation.normalizedSource
            k n L)
          x 0 0 ^
        2 =
    1

Theorem10.1.5

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “normalized source contract”; the hypotheses and conclusion in the code panel fix its exact scope.

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. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. theorem.

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

Lean code for Theorem10.1.5●1 theorem

theoremdefined in QuantumBlockEncoding/ConstructiveHermitePreparation.lean

complete

theorem QuantumBlockEncoding.ConstructiveHermitePreparation.normalizedSource_contract
  (k n : ℕ) (L : ℝ) (hL : 0 < L)
  (x : QuantumBlockEncoding.TensorTrainCanonical.Word (n + 1)) :
  QuantumBlockEncoding.TensorTrainCanonical.contract
      (QuantumBlockEncoding.ConstructiveHermitePreparation.normalizedSource
        k n L)
      x 0 0 =
    QuantumBlockEncoding.HermiteStatePreparation.sampledAmplitude k
        (n + 1) L
        ((QuantumBlockEncoding.TensorTrainWord.sampleEquiv (n + 1)) x) /
      QuantumBlockEncoding.HermiteStatePreparation.sampleNorm k (n + 1)
        L

theorem QuantumBlockEncoding.ConstructiveHermitePreparation.normalizedSource_contract
  (k n : ℕ) (L : ℝ) (hL : 0 < L)
  (x :
    QuantumBlockEncoding.TensorTrainCanonical.Word
      (n + 1)) :
  QuantumBlockEncoding.TensorTrainCanonical.contract
      (QuantumBlockEncoding.ConstructiveHermitePreparation.normalizedSource
        k n L)
      x 0 0 =
    QuantumBlockEncoding.HermiteStatePreparation.sampledAmplitude
        k (n + 1) L
        ((QuantumBlockEncoding.TensorTrainWord.sampleEquiv
            (n + 1))
          x) /
      QuantumBlockEncoding.HermiteStatePreparation.sampleNorm
        k (n + 1) L

Definition10.1.6

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “prepare”. The actual finite primitive list; no circuit witness is selected.

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

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

Technical source note. The actual finite primitive list; no circuit witness is selected.

Declaration kind. def.

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

Lean code for Definition10.1.6●1 definition

defdefined in QuantumBlockEncoding/ConstructiveHermitePreparation.lean

complete

def QuantumBlockEncoding.ConstructiveHermitePreparation.prepare (k n : ℕ)
  (L : ℝ) :
  QuantumBlockEncoding.PrimitiveCircuit
    (n + 1 + QuantumBlockEncoding.HermiteFiniteChain.bondQubits k)

def QuantumBlockEncoding.ConstructiveHermitePreparation.prepare
  (k n : ℕ) (L : ℝ) :
  QuantumBlockEncoding.PrimitiveCircuit
    (n + 1 +
      QuantumBlockEncoding.HermiteFiniteChain.bondQubits
        k)

The actual finite primitive list; no circuit witness is selected.

Theorem10.1.7

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “prepare gate count”; the hypotheses and conclusion in the code panel fix its exact scope.

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. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. theorem.

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

Lean code for Theorem10.1.7●1 theorem

theoremdefined in QuantumBlockEncoding/ConstructiveHermitePreparation.lean

complete

theorem QuantumBlockEncoding.ConstructiveHermitePreparation.prepare_gateCount
  (k n : ℕ) (L : ℝ) :
  (QuantumBlockEncoding.ConstructiveHermitePreparation.prepare k n
        L).gateCount ≤
    48 * (n + 1) * (2 * k + 6) ^ 3

theorem QuantumBlockEncoding.ConstructiveHermitePreparation.prepare_gateCount
  (k n : ℕ) (L : ℝ) :
  (QuantumBlockEncoding.ConstructiveHermitePreparation.prepare
        k n L).gateCount ≤
    48 * (n + 1) * (2 * k + 6) ^ 3

Theorem10.1.8

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “prepare depth”; the hypotheses and conclusion in the code panel fix its exact scope.

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. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. theorem.

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

Lean code for Theorem10.1.8●1 theorem

theoremdefined in QuantumBlockEncoding/ConstructiveHermitePreparation.lean

complete

theorem QuantumBlockEncoding.ConstructiveHermitePreparation.prepare_depth
  (k n : ℕ) (L : ℝ) :
  (QuantumBlockEncoding.ConstructiveHermitePreparation.prepare k n
          L).resource.depth ≤
    48 * (n + 1) * (2 * k + 6) ^ 3

theorem QuantumBlockEncoding.ConstructiveHermitePreparation.prepare_depth
  (k n : ℕ) (L : ℝ) :
  (QuantumBlockEncoding.ConstructiveHermitePreparation.prepare
          k n L).resource.depth ≤
    48 * (n + 1) * (2 * k + 6) ^ 3

Theorem10.1.9

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “prepare columns”; the hypotheses and conclusion in the code panel fix its exact scope.

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. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. theorem.

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

Lean code for Theorem10.1.9●1 theorem

theoremdefined in QuantumBlockEncoding/ConstructiveHermitePreparation.lean

complete

theorem QuantumBlockEncoding.ConstructiveHermitePreparation.prepare_columns
  (k n : ℕ) (L : ℝ) (hL : 0 < L)
  (x : QuantumBlockEncoding.PrimitiveBasis (n + 1))
  (b :
    QuantumBlockEncoding.PrimitiveBasis
      (QuantumBlockEncoding.HermiteFiniteChain.bondQubits k)) :
  (QuantumBlockEncoding.evalPrimitiveCircuit
      (QuantumBlockEncoding.ConstructiveHermitePreparation.prepare k n
        L)
      (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.ConstructiveHermitePreparation.prepare_columns
  (k n : ℕ) (L : ℝ) (hL : 0 < L)
  (x :
    QuantumBlockEncoding.PrimitiveBasis
      (n + 1))
  (b :
    QuantumBlockEncoding.PrimitiveBasis
      (QuantumBlockEncoding.HermiteFiniteChain.bondQubits
        k)) :
  (QuantumBlockEncoding.evalPrimitiveCircuit
      (QuantumBlockEncoding.ConstructiveHermitePreparation.prepare
        k n L)
      (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

Theorem10.1.10

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “prepare spec”; the hypotheses and conclusion in the code panel fix its exact scope. Literal source semantics, all clean/non-clean output sectors, full unitary, and gate/depth bounds for this particular constructed circuit.

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. Literal source semantics, all clean/non-clean output sectors, full unitary, and gate/depth bounds for this particular constructed circuit.

Declaration kind. theorem.

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

Lean code for Theorem10.1.10●1 theorem

theoremdefined in QuantumBlockEncoding/ConstructiveHermitePreparation.lean

complete

theorem QuantumBlockEncoding.ConstructiveHermitePreparation.prepare_spec
  (k n : ℕ) (L : ℝ) (hL : 0 < L) :
  (QuantumBlockEncoding.ConstructiveHermitePreparation.prepare k n
          L).gateCount ≤
      48 * (n + 1) * (2 * k + 6) ^ 3 ∧
    (QuantumBlockEncoding.ConstructiveHermitePreparation.prepare k n
              L).resource.depth ≤
        48 * (n + 1) * (2 * k + 6) ^ 3 ∧
      (QuantumBlockEncoding.ConstructiveHermitePreparation.prepare k n
                L).resource.oracleCalls =
          0 ∧
        QuantumBlockEncoding.evalPrimitiveCircuit
              (QuantumBlockEncoding.ConstructiveHermitePreparation.prepare
                k n L) ∈
            Matrix.unitaryGroup
              (QuantumBlockEncoding.PrimitiveBasis
                (n + 1 +
                  QuantumBlockEncoding.HermiteFiniteChain.bondQubits k))
              ℂ ∧
          ∀ (x : QuantumBlockEncoding.PrimitiveBasis (n + 1))
            (b :
              QuantumBlockEncoding.PrimitiveBasis
                (QuantumBlockEncoding.HermiteFiniteChain.bondQubits k)),
            (QuantumBlockEncoding.evalPrimitiveCircuit
                (QuantumBlockEncoding.ConstructiveHermitePreparation.prepare
                  k n L)
                (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.ConstructiveHermitePreparation.prepare_spec
  (k n : ℕ) (L : ℝ) (hL : 0 < L) :
  (QuantumBlockEncoding.ConstructiveHermitePreparation.prepare
          k n L).gateCount ≤
      48 * (n + 1) * (2 * k + 6) ^ 3 ∧
    (QuantumBlockEncoding.ConstructiveHermitePreparation.prepare
              k n L).resource.depth ≤
        48 * (n + 1) * (2 * k + 6) ^ 3 ∧
      (QuantumBlockEncoding.ConstructiveHermitePreparation.prepare
                k n
                L).resource.oracleCalls =
          0 ∧
        QuantumBlockEncoding.evalPrimitiveCircuit
              (QuantumBlockEncoding.ConstructiveHermitePreparation.prepare
                k n L) ∈
            Matrix.unitaryGroup
              (QuantumBlockEncoding.PrimitiveBasis
                (n + 1 +
                  QuantumBlockEncoding.HermiteFiniteChain.bondQubits
                    k))
              ℂ ∧
          ∀
            (x :
              QuantumBlockEncoding.PrimitiveBasis
                (n + 1))
            (b :
              QuantumBlockEncoding.PrimitiveBasis
                (QuantumBlockEncoding.HermiteFiniteChain.bondQubits
                  k)),
            (QuantumBlockEncoding.evalPrimitiveCircuit
                (QuantumBlockEncoding.ConstructiveHermitePreparation.prepare
                  k n L)
                (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

Literal source semantics, all clean/non-clean output sectors, full unitary,
and gate/depth bounds for this particular constructed circuit.