ASPBE Lean Blueprint

10.20. QuantumBlockEncoding/RealAmplitudePreparation.lean🔗

41 explicit public declarations, in source order.

Definition10.20.1
uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “last basis equiv”. Adjoin a most-significant bit; existing wire numbers do not change.

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. Adjoin a most-significant bit; existing wire numbers do not change.

Declaration kind. def.

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

Lean code for Definition10.20.1●1 definition
  • defdefined in QuantumBlockEncoding/RealAmplitudePreparation.lean
    complete
    def QuantumBlockEncoding.RealAmplitudePreparation.lastBasisEquiv (n : ℕ) :
  QuantumBlockEncoding.PrimitiveBasis (n + 1) ≃
    QuantumBlockEncoding.PrimitiveBasis n × Fin 2
    def QuantumBlockEncoding.RealAmplitudePreparation.lastBasisEquiv
  (n : ℕ) :
  QuantumBlockEncoding.PrimitiveBasis
      (n + 1) ≃
    QuantumBlockEncoding.PrimitiveBasis
        n ×
      Fin 2
    Adjoin a most-significant bit; existing wire numbers do not change.
Theorem10.20.2
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “last basis equiv apply”; 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/RealAmplitudePreparation.lean:23. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.20.2●1 theorem
  • theoremdefined in QuantumBlockEncoding/RealAmplitudePreparation.lean
    complete
    theorem QuantumBlockEncoding.RealAmplitudePreparation.lastBasisEquiv_apply
  {n : ℕ} (b : QuantumBlockEncoding.PrimitiveBasis (n + 1)) :
  (QuantumBlockEncoding.RealAmplitudePreparation.lastBasisEquiv n) b =
    (Fin.init b, b (Fin.last n))
    theorem QuantumBlockEncoding.RealAmplitudePreparation.lastBasisEquiv_apply
  {n : ℕ}
  (b :
    QuantumBlockEncoding.PrimitiveBasis
      (n + 1)) :
  (QuantumBlockEncoding.RealAmplitudePreparation.lastBasisEquiv
        n)
      b =
    (Fin.init b, b (Fin.last n))
Theorem10.20.3
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “last basis equiv symm apply”; 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/RealAmplitudePreparation.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.20.3●1 theorem
  • theoremdefined in QuantumBlockEncoding/RealAmplitudePreparation.lean
    complete
    theorem QuantumBlockEncoding.RealAmplitudePreparation.lastBasisEquiv_symm_apply
  {n : ℕ} (b : QuantumBlockEncoding.PrimitiveBasis n) (v : Fin 2) :
  (QuantumBlockEncoding.RealAmplitudePreparation.lastBasisEquiv n).symm
      (b, v) =
    Fin.snoc b v
    theorem QuantumBlockEncoding.RealAmplitudePreparation.lastBasisEquiv_symm_apply
  {n : ℕ}
  (b :
    QuantumBlockEncoding.PrimitiveBasis n)
  (v : Fin 2) :
  (QuantumBlockEncoding.RealAmplitudePreparation.lastBasisEquiv
          n).symm
      (b, v) =
    Fin.snoc b v
Theorem10.20.4
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “basis eq iff”; 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/RealAmplitudePreparation.lean:29. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.20.4●1 theorem
  • theoremdefined in QuantumBlockEncoding/RealAmplitudePreparation.lean
    complete
    theorem QuantumBlockEncoding.RealAmplitudePreparation.basis_eq_iff {n : ℕ}
  (a b : QuantumBlockEncoding.PrimitiveBasis (n + 1)) :
  a = b ↔ Fin.init a = Fin.init b ∧ a (Fin.last n) = b (Fin.last n)
    theorem QuantumBlockEncoding.RealAmplitudePreparation.basis_eq_iff
  {n : ℕ}
  (a b :
    QuantumBlockEncoding.PrimitiveBasis
      (n + 1)) :
  a = b ↔
    Fin.init a = Fin.init b ∧
      a (Fin.last n) = b (Fin.last n)
Definition10.20.5
uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “lift last matrix”. Tensor a circuit matrix with an untouched highest wire.

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. Tensor a circuit matrix with an untouched highest wire.

Declaration kind. def.

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

Lean code for Definition10.20.5●1 definition
  • defdefined in QuantumBlockEncoding/RealAmplitudePreparation.lean
    complete
    def QuantumBlockEncoding.RealAmplitudePreparation.liftLastMatrix {n : ℕ}
  (M :
    Matrix (QuantumBlockEncoding.PrimitiveBasis n)
      (QuantumBlockEncoding.PrimitiveBasis n) ℂ) :
  Matrix (QuantumBlockEncoding.PrimitiveBasis (n + 1))
    (QuantumBlockEncoding.PrimitiveBasis (n + 1)) ℂ
    def QuantumBlockEncoding.RealAmplitudePreparation.liftLastMatrix
  {n : ℕ}
  (M :
    Matrix
      (QuantumBlockEncoding.PrimitiveBasis
        n)
      (QuantumBlockEncoding.PrimitiveBasis
        n)
      ℂ) :
  Matrix
    (QuantumBlockEncoding.PrimitiveBasis
      (n + 1))
    (QuantumBlockEncoding.PrimitiveBasis
      (n + 1))
    ℂ
    Tensor a circuit matrix with an untouched highest wire.
Theorem10.20.6
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “lift last matrix apply”; 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/RealAmplitudePreparation.lean:41. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.20.6●1 theorem
  • theoremdefined in QuantumBlockEncoding/RealAmplitudePreparation.lean
    complete
    theorem QuantumBlockEncoding.RealAmplitudePreparation.liftLastMatrix_apply
  {n : ℕ}
  (M :
    Matrix (QuantumBlockEncoding.PrimitiveBasis n)
      (QuantumBlockEncoding.PrimitiveBasis n) ℂ)
  (a b : QuantumBlockEncoding.PrimitiveBasis (n + 1)) :
  QuantumBlockEncoding.RealAmplitudePreparation.liftLastMatrix M a b =
    if a (Fin.last n) = b (Fin.last n) then M (Fin.init a) (Fin.init b)
    else 0
    theorem QuantumBlockEncoding.RealAmplitudePreparation.liftLastMatrix_apply
  {n : ℕ}
  (M :
    Matrix
      (QuantumBlockEncoding.PrimitiveBasis
        n)
      (QuantumBlockEncoding.PrimitiveBasis
        n)
      ℂ)
  (a b :
    QuantumBlockEncoding.PrimitiveBasis
      (n + 1)) :
  QuantumBlockEncoding.RealAmplitudePreparation.liftLastMatrix
      M a b =
    if
        a (Fin.last n) =
          b (Fin.last n) then
      M (Fin.init a) (Fin.init b)
    else 0
Theorem10.20.7
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “lift last matrix one”; 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/RealAmplitudePreparation.lean:50. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.20.7●1 theorem
  • theoremdefined in QuantumBlockEncoding/RealAmplitudePreparation.lean
    complete
    theorem QuantumBlockEncoding.RealAmplitudePreparation.liftLastMatrix_one
  (n : ℕ) :
  QuantumBlockEncoding.RealAmplitudePreparation.liftLastMatrix 1 = 1
    theorem QuantumBlockEncoding.RealAmplitudePreparation.liftLastMatrix_one
  (n : ℕ) :
  QuantumBlockEncoding.RealAmplitudePreparation.liftLastMatrix
      1 =
    1
Theorem10.20.8
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “lift last matrix mul”; 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/RealAmplitudePreparation.lean:54. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.20.8●1 theorem
  • theoremdefined in QuantumBlockEncoding/RealAmplitudePreparation.lean
    complete
    theorem QuantumBlockEncoding.RealAmplitudePreparation.liftLastMatrix_mul {n : ℕ}
  (M N :
    Matrix (QuantumBlockEncoding.PrimitiveBasis n)
      (QuantumBlockEncoding.PrimitiveBasis n) ℂ) :
  QuantumBlockEncoding.RealAmplitudePreparation.liftLastMatrix (M * N) =
    QuantumBlockEncoding.RealAmplitudePreparation.liftLastMatrix M *
      QuantumBlockEncoding.RealAmplitudePreparation.liftLastMatrix N
    theorem QuantumBlockEncoding.RealAmplitudePreparation.liftLastMatrix_mul
  {n : ℕ}
  (M N :
    Matrix
      (QuantumBlockEncoding.PrimitiveBasis
        n)
      (QuantumBlockEncoding.PrimitiveBasis
        n)
      ℂ) :
  QuantumBlockEncoding.RealAmplitudePreparation.liftLastMatrix
      (M * N) =
    QuantumBlockEncoding.RealAmplitudePreparation.liftLastMatrix
        M *
      QuantumBlockEncoding.RealAmplitudePreparation.liftLastMatrix
        N
Definition10.20.9
uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “lift gate”. Embed every instruction without changing its original wire number.

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. Embed every instruction without changing its original wire number.

Declaration kind. def.

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

Lean code for Definition10.20.9●1 definition
  • defdefined in QuantumBlockEncoding/RealAmplitudePreparation.lean
    complete
    def QuantumBlockEncoding.RealAmplitudePreparation.liftGate {n : ℕ} :
  QuantumBlockEncoding.PrimitiveGate n →
    QuantumBlockEncoding.PrimitiveGate (n + 1)
    def QuantumBlockEncoding.RealAmplitudePreparation.liftGate
  {n : ℕ} :
  QuantumBlockEncoding.PrimitiveGate n →
    QuantumBlockEncoding.PrimitiveGate
      (n + 1)
    Embed every instruction without changing its original wire number.
Theorem10.20.10
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “lift one qubit”; 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/RealAmplitudePreparation.lean:87. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.20.10●1 theorem
  • theoremdefined in QuantumBlockEncoding/RealAmplitudePreparation.lean
    complete
    theorem QuantumBlockEncoding.RealAmplitudePreparation.lift_oneQubit {n : ℕ}
  (t : Fin n) (M : Matrix (Fin 2) (Fin 2) ℂ) :
  QuantumBlockEncoding.liftPrimitiveOneQubit t.castSucc M =
    QuantumBlockEncoding.RealAmplitudePreparation.liftLastMatrix
      (QuantumBlockEncoding.liftPrimitiveOneQubit t M)
    theorem QuantumBlockEncoding.RealAmplitudePreparation.lift_oneQubit
  {n : ℕ} (t : Fin n)
  (M : Matrix (Fin 2) (Fin 2) ℂ) :
  QuantumBlockEncoding.liftPrimitiveOneQubit
      t.castSucc M =
    QuantumBlockEncoding.RealAmplitudePreparation.liftLastMatrix
      (QuantumBlockEncoding.liftPrimitiveOneQubit
        t M)
Theorem10.20.11
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “eval lift gate”; 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/RealAmplitudePreparation.lean:108. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.20.11●1 theorem
  • theoremdefined in QuantumBlockEncoding/RealAmplitudePreparation.lean
    complete
    theorem QuantumBlockEncoding.RealAmplitudePreparation.eval_liftGate {n : ℕ}
  (g : QuantumBlockEncoding.PrimitiveGate n) :
  QuantumBlockEncoding.evalPrimitiveGate
      (QuantumBlockEncoding.RealAmplitudePreparation.liftGate g) =
    QuantumBlockEncoding.RealAmplitudePreparation.liftLastMatrix
      (QuantumBlockEncoding.evalPrimitiveGate g)
    theorem QuantumBlockEncoding.RealAmplitudePreparation.eval_liftGate
  {n : ℕ}
  (g :
    QuantumBlockEncoding.PrimitiveGate
      n) :
  QuantumBlockEncoding.evalPrimitiveGate
      (QuantumBlockEncoding.RealAmplitudePreparation.liftGate
        g) =
    QuantumBlockEncoding.RealAmplitudePreparation.liftLastMatrix
      (QuantumBlockEncoding.evalPrimitiveGate
        g)
Theorem10.20.12
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “eval lift circuit”; 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/RealAmplitudePreparation.lean:135. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.20.12●1 theorem
  • theoremdefined in QuantumBlockEncoding/RealAmplitudePreparation.lean
    complete
    theorem QuantumBlockEncoding.RealAmplitudePreparation.eval_liftCircuit {n : ℕ}
  (c : QuantumBlockEncoding.PrimitiveCircuit n) :
  QuantumBlockEncoding.evalPrimitiveCircuit
      (List.map QuantumBlockEncoding.RealAmplitudePreparation.liftGate
        c) =
    QuantumBlockEncoding.RealAmplitudePreparation.liftLastMatrix
      (QuantumBlockEncoding.evalPrimitiveCircuit c)
    theorem QuantumBlockEncoding.RealAmplitudePreparation.eval_liftCircuit
  {n : ℕ}
  (c :
    QuantumBlockEncoding.PrimitiveCircuit
      n) :
  QuantumBlockEncoding.evalPrimitiveCircuit
      (List.map
        QuantumBlockEncoding.RealAmplitudePreparation.liftGate
        c) =
    QuantumBlockEncoding.RealAmplitudePreparation.liftLastMatrix
      (QuantumBlockEncoding.evalPrimitiveCircuit
        c)
Definition10.20.13
uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “pair norm”. Euclidean mass at one binary split.

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. Euclidean mass at one binary split.

Declaration kind. def.

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

Lean code for Definition10.20.13●1 definition
  • defdefined in QuantumBlockEncoding/RealAmplitudePreparation.lean
    complete
    def QuantumBlockEncoding.RealAmplitudePreparation.pairNorm (a b : ℝ) : ℝ
    def QuantumBlockEncoding.RealAmplitudePreparation.pairNorm
  (a b : ℝ) : ℝ
    Euclidean mass at one binary split.
Theorem10.20.14
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “pair norm nonneg”; 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/RealAmplitudePreparation.lean:145. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.20.14●1 theorem
  • theoremdefined in QuantumBlockEncoding/RealAmplitudePreparation.lean
    complete
    theorem QuantumBlockEncoding.RealAmplitudePreparation.pairNorm_nonneg
  (a b : ℝ) :
  0 ≤ QuantumBlockEncoding.RealAmplitudePreparation.pairNorm a b
    theorem QuantumBlockEncoding.RealAmplitudePreparation.pairNorm_nonneg
  (a b : ℝ) :
  0 ≤
    QuantumBlockEncoding.RealAmplitudePreparation.pairNorm
      a b
Theorem10.20.15
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “pair norm sq”; 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/RealAmplitudePreparation.lean:147. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.20.15●1 theorem
  • theoremdefined in QuantumBlockEncoding/RealAmplitudePreparation.lean
    complete
    theorem QuantumBlockEncoding.RealAmplitudePreparation.pairNorm_sq (a b : ℝ) :
  QuantumBlockEncoding.RealAmplitudePreparation.pairNorm a b ^ 2 =
    a ^ 2 + b ^ 2
    theorem QuantumBlockEncoding.RealAmplitudePreparation.pairNorm_sq
  (a b : ℝ) :
  QuantumBlockEncoding.RealAmplitudePreparation.pairNorm
        a b ^
      2 =
    a ^ 2 + b ^ 2
Definition10.20.16
uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “split angle”. Twice the signed polar angle, with the zero subtree assigned angle zero.

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. Twice the signed polar angle, with the zero subtree assigned angle zero. The arccos formula avoids an unverified numerical 'atan2' primitive.

Declaration kind. def.

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

Lean code for Definition10.20.16●1 definition
  • defdefined in QuantumBlockEncoding/RealAmplitudePreparation.lean
    complete
    def QuantumBlockEncoding.RealAmplitudePreparation.splitAngle (a b : ℝ) :
  QuantumBlockEncoding.ExactAngle
    def QuantumBlockEncoding.RealAmplitudePreparation.splitAngle
  (a b : ℝ) :
  QuantumBlockEncoding.ExactAngle
    Twice the signed polar angle, with the zero subtree assigned angle zero.
The arccos formula avoids an unverified numerical `atan2` primitive.
Theorem10.20.17
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “split angle first column”; 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/RealAmplitudePreparation.lean:157. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.20.17●1 theorem
  • theoremdefined in QuantumBlockEncoding/RealAmplitudePreparation.lean
    complete
    theorem QuantumBlockEncoding.RealAmplitudePreparation.splitAngle_firstColumn
  (a b : ℝ) (v : Fin 2) :
  QuantumBlockEncoding.standardRyMatrix
        (QuantumBlockEncoding.RealAmplitudePreparation.splitAngle a
            b).eval
        v 0 *
      ↑(QuantumBlockEncoding.RealAmplitudePreparation.pairNorm a b) =
    if v = 0 then ↑a else ↑b
    theorem QuantumBlockEncoding.RealAmplitudePreparation.splitAngle_firstColumn
  (a b : ℝ) (v : Fin 2) :
  QuantumBlockEncoding.standardRyMatrix
        (QuantumBlockEncoding.RealAmplitudePreparation.splitAngle
            a b).eval
        v 0 *
      ↑(QuantumBlockEncoding.RealAmplitudePreparation.pairNorm
          a b) =
    if v = 0 then ↑a else ↑b
Definition10.20.18
uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “marginal”. Marginal amplitudes on all but the highest wire.

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. Marginal amplitudes on all but the highest wire.

Declaration kind. def.

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

Lean code for Definition10.20.18●1 definition
  • defdefined in QuantumBlockEncoding/RealAmplitudePreparation.lean
    complete
    def QuantumBlockEncoding.RealAmplitudePreparation.marginal {n : ℕ}
  (f : QuantumBlockEncoding.PrimitiveBasis (n + 1) → ℝ) :
  QuantumBlockEncoding.PrimitiveBasis n → ℝ
    def QuantumBlockEncoding.RealAmplitudePreparation.marginal
  {n : ℕ}
  (f :
    QuantumBlockEncoding.PrimitiveBasis
        (n + 1) →
      ℝ) :
  QuantumBlockEncoding.PrimitiveBasis n →
    ℝ
    Marginal amplitudes on all but the highest wire.
Theorem10.20.19
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “marginal nonneg”; 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/RealAmplitudePreparation.lean:207. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.20.19●1 theorem
  • theoremdefined in QuantumBlockEncoding/RealAmplitudePreparation.lean
    complete
    theorem QuantumBlockEncoding.RealAmplitudePreparation.marginal_nonneg {n : ℕ}
  (f : QuantumBlockEncoding.PrimitiveBasis (n + 1) → ℝ)
  (b : QuantumBlockEncoding.PrimitiveBasis n) :
  0 ≤ QuantumBlockEncoding.RealAmplitudePreparation.marginal f b
    theorem QuantumBlockEncoding.RealAmplitudePreparation.marginal_nonneg
  {n : ℕ}
  (f :
    QuantumBlockEncoding.PrimitiveBasis
        (n + 1) →
      ℝ)
  (b :
    QuantumBlockEncoding.PrimitiveBasis
      n) :
  0 ≤
    QuantumBlockEncoding.RealAmplitudePreparation.marginal
      f b
Definition10.20.20
uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “norm sq”. True squared Euclidean norm of the complete amplitude table.

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. True squared Euclidean norm of the complete amplitude table.

Declaration kind. def.

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

Lean code for Definition10.20.20●1 definition
  • defdefined in QuantumBlockEncoding/RealAmplitudePreparation.lean
    complete
    def QuantumBlockEncoding.RealAmplitudePreparation.normSq {n : ℕ}
  (f : QuantumBlockEncoding.PrimitiveBasis n → ℝ) : ℝ
    def QuantumBlockEncoding.RealAmplitudePreparation.normSq
  {n : ℕ}
  (f :
    QuantumBlockEncoding.PrimitiveBasis
        n →
      ℝ) :
  ℝ
    True squared Euclidean norm of the complete amplitude table.
Theorem10.20.21
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “norm sq nonneg”; 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/RealAmplitudePreparation.lean:213. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.20.21●1 theorem
  • theoremdefined in QuantumBlockEncoding/RealAmplitudePreparation.lean
    complete
    theorem QuantumBlockEncoding.RealAmplitudePreparation.normSq_nonneg {n : ℕ}
  (f : QuantumBlockEncoding.PrimitiveBasis n → ℝ) :
  0 ≤ QuantumBlockEncoding.RealAmplitudePreparation.normSq f
    theorem QuantumBlockEncoding.RealAmplitudePreparation.normSq_nonneg
  {n : ℕ}
  (f :
    QuantumBlockEncoding.PrimitiveBasis
        n →
      ℝ) :
  0 ≤
    QuantumBlockEncoding.RealAmplitudePreparation.normSq
      f
Theorem10.20.22
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “norm sq marginal”; 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/RealAmplitudePreparation.lean:216. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.20.22●1 theorem
  • theoremdefined in QuantumBlockEncoding/RealAmplitudePreparation.lean
    complete
    theorem QuantumBlockEncoding.RealAmplitudePreparation.normSq_marginal {n : ℕ}
  (f : QuantumBlockEncoding.PrimitiveBasis (n + 1) → ℝ) :
  QuantumBlockEncoding.RealAmplitudePreparation.normSq
      (QuantumBlockEncoding.RealAmplitudePreparation.marginal f) =
    QuantumBlockEncoding.RealAmplitudePreparation.normSq f
    theorem QuantumBlockEncoding.RealAmplitudePreparation.normSq_marginal
  {n : ℕ}
  (f :
    QuantumBlockEncoding.PrimitiveBasis
        (n + 1) →
      ℝ) :
  QuantumBlockEncoding.RealAmplitudePreparation.normSq
      (QuantumBlockEncoding.RealAmplitudePreparation.marginal
        f) =
    QuantumBlockEncoding.RealAmplitudePreparation.normSq
      f
Definition10.20.23
uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “prepare circuit”. Chronological low-bit-first binary tree, compiled entirely to RY and CX.

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. Chronological low-bit-first binary tree, compiled entirely to RY and CX.

Declaration kind. def.

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

Lean code for Definition10.20.23●1 definition
  • defdefined in QuantumBlockEncoding/RealAmplitudePreparation.lean
    complete
    def QuantumBlockEncoding.RealAmplitudePreparation.prepareCircuit (n : ℕ) :
  (QuantumBlockEncoding.PrimitiveBasis n → ℝ) →
    QuantumBlockEncoding.PrimitiveCircuit n
    def QuantumBlockEncoding.RealAmplitudePreparation.prepareCircuit
  (n : ℕ) :
  (QuantumBlockEncoding.PrimitiveBasis n →
      ℝ) →
    QuantumBlockEncoding.PrimitiveCircuit
      n
    Chronological low-bit-first binary tree, compiled entirely to RY and CX.
Theorem10.20.24
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “prepare circuit unitary”; 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/RealAmplitudePreparation.lean:231. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.20.24●1 theorem
  • theoremdefined in QuantumBlockEncoding/RealAmplitudePreparation.lean
    complete
    theorem QuantumBlockEncoding.RealAmplitudePreparation.prepareCircuit_unitary
  {n : ℕ} (f : QuantumBlockEncoding.PrimitiveBasis n → ℝ) :
  QuantumBlockEncoding.evalPrimitiveCircuit
      (QuantumBlockEncoding.RealAmplitudePreparation.prepareCircuit n
        f) ∈
    Matrix.unitaryGroup (QuantumBlockEncoding.PrimitiveBasis n) ℂ
    theorem QuantumBlockEncoding.RealAmplitudePreparation.prepareCircuit_unitary
  {n : ℕ}
  (f :
    QuantumBlockEncoding.PrimitiveBasis
        n →
      ℝ) :
  QuantumBlockEncoding.evalPrimitiveCircuit
      (QuantumBlockEncoding.RealAmplitudePreparation.prepareCircuit
        n f) ∈
    Matrix.unitaryGroup
      (QuantumBlockEncoding.PrimitiveBasis
        n)
      ℂ
Theorem10.20.25
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “controlled last apply”; 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/RealAmplitudePreparation.lean:252. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.20.25●1 theorem
  • theoremdefined in QuantumBlockEncoding/RealAmplitudePreparation.lean
    complete
    theorem QuantumBlockEncoding.RealAmplitudePreparation.controlledLast_apply
  {n : ℕ}
  (angles :
    QuantumBlockEncoding.PrimitiveBasis n →
      QuantumBlockEncoding.ExactAngle)
  (a b : QuantumBlockEncoding.PrimitiveBasis (n + 1)) :
  QuantumBlockEncoding.controlledRyBlockMatrix Fin.castSucc (Fin.last n)
      ⋯ angles a b =
    if Fin.init a = Fin.init b then
      QuantumBlockEncoding.standardRyMatrix (angles (Fin.init a)).eval
        (a (Fin.last n)) (b (Fin.last n))
    else 0
    theorem QuantumBlockEncoding.RealAmplitudePreparation.controlledLast_apply
  {n : ℕ}
  (angles :
    QuantumBlockEncoding.PrimitiveBasis
        n →
      QuantumBlockEncoding.ExactAngle)
  (a b :
    QuantumBlockEncoding.PrimitiveBasis
      (n + 1)) :
  QuantumBlockEncoding.controlledRyBlockMatrix
      Fin.castSucc (Fin.last n) ⋯ angles a
      b =
    if Fin.init a = Fin.init b then
      QuantumBlockEncoding.standardRyMatrix
        (angles (Fin.init a)).eval
        (a (Fin.last n)) (b (Fin.last n))
    else 0
Theorem10.20.26
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “controlled last mul lift”; 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/RealAmplitudePreparation.lean:261. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.20.26●1 theorem
  • theoremdefined in QuantumBlockEncoding/RealAmplitudePreparation.lean
    complete
    theorem QuantumBlockEncoding.RealAmplitudePreparation.controlledLast_mul_lift
  {n : ℕ}
  (angles :
    QuantumBlockEncoding.PrimitiveBasis n →
      QuantumBlockEncoding.ExactAngle)
  (M :
    Matrix (QuantumBlockEncoding.PrimitiveBasis n)
      (QuantumBlockEncoding.PrimitiveBasis n) ℂ)
  (a : QuantumBlockEncoding.PrimitiveBasis (n + 1)) :
  ((QuantumBlockEncoding.controlledRyBlockMatrix Fin.castSucc
          (Fin.last n) ⋯ angles *
        QuantumBlockEncoding.RealAmplitudePreparation.liftLastMatrix M)
      a fun x => 0) =
    QuantumBlockEncoding.standardRyMatrix (angles (Fin.init a)).eval
        (a (Fin.last n)) 0 *
      M (Fin.init a) fun x => 0
    theorem QuantumBlockEncoding.RealAmplitudePreparation.controlledLast_mul_lift
  {n : ℕ}
  (angles :
    QuantumBlockEncoding.PrimitiveBasis
        n →
      QuantumBlockEncoding.ExactAngle)
  (M :
    Matrix
      (QuantumBlockEncoding.PrimitiveBasis
        n)
      (QuantumBlockEncoding.PrimitiveBasis
        n)
      ℂ)
  (a :
    QuantumBlockEncoding.PrimitiveBasis
      (n + 1)) :
  ((QuantumBlockEncoding.controlledRyBlockMatrix
          Fin.castSucc (Fin.last n) ⋯
          angles *
        QuantumBlockEncoding.RealAmplitudePreparation.liftLastMatrix
          M)
      a fun x => 0) =
    QuantumBlockEncoding.standardRyMatrix
        (angles (Fin.init a)).eval
        (a (Fin.last n)) 0 *
      M (Fin.init a) fun x => 0
Theorem10.20.27
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “prepare circuit first column”; the hypotheses and conclusion in the code panel fix its exact scope. The compiled first column is the normalized input table.

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 compiled first column is the normalized input table. This version also covers the zero-qubit register, whose sole amplitude must be nonnegative.

Declaration kind. theorem.

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

Lean code for Theorem10.20.27●1 theorem
  • theoremdefined in QuantumBlockEncoding/RealAmplitudePreparation.lean
    complete
    theorem QuantumBlockEncoding.RealAmplitudePreparation.prepareCircuit_firstColumn
  {n : ℕ} (f : QuantumBlockEncoding.PrimitiveBasis n → ℝ)
  (nonneg : ∀ (b : QuantumBlockEncoding.PrimitiveBasis n), 0 ≤ f b)
  (positive :
    0 < QuantumBlockEncoding.RealAmplitudePreparation.normSq f)
  (b : QuantumBlockEncoding.PrimitiveBasis n) :
  (QuantumBlockEncoding.evalPrimitiveCircuit
      (QuantumBlockEncoding.RealAmplitudePreparation.prepareCircuit n f)
      b fun x => 0) =
    ↑(f b / √(QuantumBlockEncoding.RealAmplitudePreparation.normSq f))
    theorem QuantumBlockEncoding.RealAmplitudePreparation.prepareCircuit_firstColumn
  {n : ℕ}
  (f :
    QuantumBlockEncoding.PrimitiveBasis
        n →
      ℝ)
  (nonneg :
    ∀
      (b :
        QuantumBlockEncoding.PrimitiveBasis
          n),
      0 ≤ f b)
  (positive :
    0 <
      QuantumBlockEncoding.RealAmplitudePreparation.normSq
        f)
  (b :
    QuantumBlockEncoding.PrimitiveBasis
      n) :
  (QuantumBlockEncoding.evalPrimitiveCircuit
      (QuantumBlockEncoding.RealAmplitudePreparation.prepareCircuit
        n f)
      b fun x => 0) =
    ↑(f b /
        √(QuantumBlockEncoding.RealAmplitudePreparation.normSq
            f))
    The compiled first column is the normalized input table. This version
also covers the zero-qubit register, whose sole amplitude must be nonnegative.
Theorem10.20.28
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “normalized sum sq”; the hypotheses and conclusion in the code panel fix its exact scope. Normalization is the actual sum of squared amplitudes, not a certificate flag.

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. Normalization is the actual sum of squared amplitudes, not a certificate flag.

Declaration kind. theorem.

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

Lean code for Theorem10.20.28●1 theorem
  • theoremdefined in QuantumBlockEncoding/RealAmplitudePreparation.lean
    complete
    theorem QuantumBlockEncoding.RealAmplitudePreparation.normalized_sum_sq {n : ℕ}
  (f : QuantumBlockEncoding.PrimitiveBasis n → ℝ)
  (positive :
    0 < QuantumBlockEncoding.RealAmplitudePreparation.normSq f) :
  ∑ b,
      (f b /
          √(QuantumBlockEncoding.RealAmplitudePreparation.normSq f)) ^
        2 =
    1
    theorem QuantumBlockEncoding.RealAmplitudePreparation.normalized_sum_sq
  {n : ℕ}
  (f :
    QuantumBlockEncoding.PrimitiveBasis
        n →
      ℝ)
  (positive :
    0 <
      QuantumBlockEncoding.RealAmplitudePreparation.normSq
        f) :
  ∑ b,
      (f b /
          √(QuantumBlockEncoding.RealAmplitudePreparation.normSq
              f)) ^
        2 =
    1
    Normalization is the actual sum of squared amplitudes, not a certificate flag.
Theorem10.20.29
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “norm sq pos of positive”; 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/RealAmplitudePreparation.lean:319. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.20.29●1 theorem
  • theoremdefined in QuantumBlockEncoding/RealAmplitudePreparation.lean
    complete
    theorem QuantumBlockEncoding.RealAmplitudePreparation.normSq_pos_of_positive
  {n : ℕ} (f : QuantumBlockEncoding.PrimitiveBasis n → ℝ)
  (positive : ∀ (b : QuantumBlockEncoding.PrimitiveBasis n), 0 < f b) :
  0 < QuantumBlockEncoding.RealAmplitudePreparation.normSq f
    theorem QuantumBlockEncoding.RealAmplitudePreparation.normSq_pos_of_positive
  {n : ℕ}
  (f :
    QuantumBlockEncoding.PrimitiveBasis
        n →
      ℝ)
  (positive :
    ∀
      (b :
        QuantumBlockEncoding.PrimitiveBasis
          n),
      0 < f b) :
  0 <
    QuantumBlockEncoding.RealAmplitudePreparation.normSq
      f
Theorem10.20.30
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “lift circuit ry 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/RealAmplitudePreparation.lean:325. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.20.30●1 theorem
  • theoremdefined in QuantumBlockEncoding/RealAmplitudePreparation.lean
    complete
    theorem QuantumBlockEncoding.RealAmplitudePreparation.liftCircuit_ryCount
  {n : ℕ} (c : QuantumBlockEncoding.PrimitiveCircuit n) :
  QuantumBlockEncoding.PrimitiveCircuit.ryCount
      (List.map QuantumBlockEncoding.RealAmplitudePreparation.liftGate
        c) =
    c.ryCount
    theorem QuantumBlockEncoding.RealAmplitudePreparation.liftCircuit_ryCount
  {n : ℕ}
  (c :
    QuantumBlockEncoding.PrimitiveCircuit
      n) :
  QuantumBlockEncoding.PrimitiveCircuit.ryCount
      (List.map
        QuantumBlockEncoding.RealAmplitudePreparation.liftGate
        c) =
    c.ryCount
Theorem10.20.31
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “lift circuit cx 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/RealAmplitudePreparation.lean:332. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.20.31●1 theorem
  • theoremdefined in QuantumBlockEncoding/RealAmplitudePreparation.lean
    complete
    theorem QuantumBlockEncoding.RealAmplitudePreparation.liftCircuit_cxCount
  {n : ℕ} (c : QuantumBlockEncoding.PrimitiveCircuit n) :
  QuantumBlockEncoding.PrimitiveCircuit.cxCount
      (List.map QuantumBlockEncoding.RealAmplitudePreparation.liftGate
        c) =
    c.cxCount
    theorem QuantumBlockEncoding.RealAmplitudePreparation.liftCircuit_cxCount
  {n : ℕ}
  (c :
    QuantumBlockEncoding.PrimitiveCircuit
      n) :
  QuantumBlockEncoding.PrimitiveCircuit.cxCount
      (List.map
        QuantumBlockEncoding.RealAmplitudePreparation.liftGate
        c) =
    c.cxCount
Theorem10.20.32
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “prepare circuit ry count”; the hypotheses and conclusion in the code panel fix its exact scope. The unoptimized reference tree uses exactly one RY per internal tree node.

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 unoptimized reference tree uses exactly one RY per internal tree node.

Declaration kind. theorem.

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

Lean code for Theorem10.20.32●1 theorem
  • theoremdefined in QuantumBlockEncoding/RealAmplitudePreparation.lean
    complete
    theorem QuantumBlockEncoding.RealAmplitudePreparation.prepareCircuit_ryCount
  {n : ℕ} (f : QuantumBlockEncoding.PrimitiveBasis n → ℝ) :
  (QuantumBlockEncoding.RealAmplitudePreparation.prepareCircuit n
        f).ryCount =
    2 ^ n - 1
    theorem QuantumBlockEncoding.RealAmplitudePreparation.prepareCircuit_ryCount
  {n : ℕ}
  (f :
    QuantumBlockEncoding.PrimitiveBasis
        n →
      ℝ) :
  (QuantumBlockEncoding.RealAmplitudePreparation.prepareCircuit
        n f).ryCount =
    2 ^ n - 1
    The unoptimized reference tree uses exactly one RY per internal tree node.
Theorem10.20.33
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “prepare circuit cx count”; the hypotheses and conclusion in the code panel fix its exact scope. CX count for the recursive reference multiplexor, without Gray-code optimization.

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. CX count for the recursive reference multiplexor, without Gray-code optimization.

Declaration kind. theorem.

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

Lean code for Theorem10.20.33●1 theorem
  • theoremdefined in QuantumBlockEncoding/RealAmplitudePreparation.lean
    complete
    theorem QuantumBlockEncoding.RealAmplitudePreparation.prepareCircuit_cxCount
  {n : ℕ} (f : QuantumBlockEncoding.PrimitiveBasis n → ℝ) :
  (QuantumBlockEncoding.RealAmplitudePreparation.prepareCircuit n
        f).cxCount =
    2 * (2 ^ n - 1 - n)
    theorem QuantumBlockEncoding.RealAmplitudePreparation.prepareCircuit_cxCount
  {n : ℕ}
  (f :
    QuantumBlockEncoding.PrimitiveBasis
        n →
      ℝ) :
  (QuantumBlockEncoding.RealAmplitudePreparation.prepareCircuit
        n f).cxCount =
    2 * (2 ^ n - 1 - n)
    CX count for the recursive reference multiplexor, without Gray-code optimization.
Theorem10.20.34
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “prepare circuit oracle calls”; 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/RealAmplitudePreparation.lean:361. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.20.34●1 theorem
  • theoremdefined in QuantumBlockEncoding/RealAmplitudePreparation.lean
    complete
    theorem QuantumBlockEncoding.RealAmplitudePreparation.prepareCircuit_oracleCalls
  {n : ℕ} (f : QuantumBlockEncoding.PrimitiveBasis n → ℝ) :
  (QuantumBlockEncoding.RealAmplitudePreparation.prepareCircuit n
          f).resource.oracleCalls =
    0
    theorem QuantumBlockEncoding.RealAmplitudePreparation.prepareCircuit_oracleCalls
  {n : ℕ}
  (f :
    QuantumBlockEncoding.PrimitiveBasis
        n →
      ℝ) :
  (QuantumBlockEncoding.RealAmplitudePreparation.prepareCircuit
          n f).resource.oracleCalls =
    0
Theorem10.20.35
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “primitive basis le zero”; 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/RealAmplitudePreparation.lean:365. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.20.35●1 theorem
  • theoremdefined in QuantumBlockEncoding/RealAmplitudePreparation.lean
    complete
    theorem QuantumBlockEncoding.RealAmplitudePreparation.primitiveBasisLE_zero
  (n : ℕ) :
  ((QuantumBlockEncoding.primitiveBasisLEEquiv n) fun x => 0) =
    QuantumBlockEncoding.zeroBasisIndex n
    theorem QuantumBlockEncoding.RealAmplitudePreparation.primitiveBasisLE_zero
  (n : ℕ) :
  ((QuantumBlockEncoding.primitiveBasisLEEquiv
        n)
      fun x => 0) =
    QuantumBlockEncoding.zeroBasisIndex n
Theorem10.20.36
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “primitive basis le zero symm”; 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/RealAmplitudePreparation.lean:374. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.20.36●1 theorem
  • theoremdefined in QuantumBlockEncoding/RealAmplitudePreparation.lean
    complete
    theorem QuantumBlockEncoding.RealAmplitudePreparation.primitiveBasisLE_zero_symm
  (n : ℕ) :
  (QuantumBlockEncoding.primitiveBasisLEEquiv n).symm
      (QuantumBlockEncoding.zeroBasisIndex n) =
    fun x => 0
    theorem QuantumBlockEncoding.RealAmplitudePreparation.primitiveBasisLE_zero_symm
  (n : ℕ) :
  (QuantumBlockEncoding.primitiveBasisLEEquiv
          n).symm
      (QuantumBlockEncoding.zeroBasisIndex
        n) =
    fun x => 0
Definition10.20.37
uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “prepare matrix le”. The same circuit matrix on flat little-endian integer indices.

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 same circuit matrix on flat little-endian integer indices.

Declaration kind. def.

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

Lean code for Definition10.20.37●1 definition
  • defdefined in QuantumBlockEncoding/RealAmplitudePreparation.lean
    complete
    def QuantumBlockEncoding.RealAmplitudePreparation.prepareMatrixLE {n : ℕ}
  (f : Fin (QuantumBlockEncoding.gridSize n) → ℝ) :
  Matrix (Fin (QuantumBlockEncoding.gridSize n))
    (Fin (QuantumBlockEncoding.gridSize n)) ℂ
    def QuantumBlockEncoding.RealAmplitudePreparation.prepareMatrixLE
  {n : ℕ}
  (f :
    Fin
        (QuantumBlockEncoding.gridSize
          n) →
      ℝ) :
  Matrix
    (Fin
      (QuantumBlockEncoding.gridSize n))
    (Fin
      (QuantumBlockEncoding.gridSize n))
    ℂ
    The same circuit matrix on flat little-endian integer indices.
Theorem10.20.38
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “prepare matrix le unitary”; 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/RealAmplitudePreparation.lean:385. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.20.38●1 theorem
  • theoremdefined in QuantumBlockEncoding/RealAmplitudePreparation.lean
    complete
    theorem QuantumBlockEncoding.RealAmplitudePreparation.prepareMatrixLE_unitary
  {n : ℕ} (f : Fin (QuantumBlockEncoding.gridSize n) → ℝ) :
  QuantumBlockEncoding.RealAmplitudePreparation.prepareMatrixLE f ∈
    Matrix.unitaryGroup (Fin (QuantumBlockEncoding.gridSize n)) ℂ
    theorem QuantumBlockEncoding.RealAmplitudePreparation.prepareMatrixLE_unitary
  {n : ℕ}
  (f :
    Fin
        (QuantumBlockEncoding.gridSize
          n) →
      ℝ) :
  QuantumBlockEncoding.RealAmplitudePreparation.prepareMatrixLE
      f ∈
    Matrix.unitaryGroup
      (Fin
        (QuantumBlockEncoding.gridSize n))
      ℂ
Theorem10.20.39
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “norm sq reindex”; 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/RealAmplitudePreparation.lean:389. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.20.39●1 theorem
  • theoremdefined in QuantumBlockEncoding/RealAmplitudePreparation.lean
    complete
    theorem QuantumBlockEncoding.RealAmplitudePreparation.normSq_reindex {n : ℕ}
  (f : Fin (QuantumBlockEncoding.gridSize n) → ℝ) :
  (QuantumBlockEncoding.RealAmplitudePreparation.normSq fun b =>
      f ((QuantumBlockEncoding.primitiveBasisLEEquiv n) b)) =
    ∑ j, f j ^ 2
    theorem QuantumBlockEncoding.RealAmplitudePreparation.normSq_reindex
  {n : ℕ}
  (f :
    Fin
        (QuantumBlockEncoding.gridSize
          n) →
      ℝ) :
  (QuantumBlockEncoding.RealAmplitudePreparation.normSq
      fun b =>
      f
        ((QuantumBlockEncoding.primitiveBasisLEEquiv
            n)
          b)) =
    ∑ j, f j ^ 2
Theorem10.20.40
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “prepare matrix le first column”; 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/RealAmplitudePreparation.lean:393. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.20.40●1 theorem
  • theoremdefined in QuantumBlockEncoding/RealAmplitudePreparation.lean
    complete
    theorem QuantumBlockEncoding.RealAmplitudePreparation.prepareMatrixLE_firstColumn
  {n : ℕ} (f : Fin (QuantumBlockEncoding.gridSize n) → ℝ)
  (positive : ∀ (j : Fin (QuantumBlockEncoding.gridSize n)), 0 < f j)
  (j : Fin (QuantumBlockEncoding.gridSize n)) :
  QuantumBlockEncoding.RealAmplitudePreparation.prepareMatrixLE f j
      (QuantumBlockEncoding.zeroBasisIndex n) =
    ↑(f j / √(∑ i, f i ^ 2))
    theorem QuantumBlockEncoding.RealAmplitudePreparation.prepareMatrixLE_firstColumn
  {n : ℕ}
  (f :
    Fin
        (QuantumBlockEncoding.gridSize
          n) →
      ℝ)
  (positive :
    ∀
      (j :
        Fin
          (QuantumBlockEncoding.gridSize
            n)),
      0 < f j)
  (j :
    Fin
      (QuantumBlockEncoding.gridSize n)) :
  QuantumBlockEncoding.RealAmplitudePreparation.prepareMatrixLE
      f j
      (QuantumBlockEncoding.zeroBasisIndex
        n) =
    ↑(f j / √(∑ i, f i ^ 2))
Theorem10.20.41
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “normalized sum sq le”; 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/RealAmplitudePreparation.lean:404. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.20.41●1 theorem
  • theoremdefined in QuantumBlockEncoding/RealAmplitudePreparation.lean
    complete
    theorem QuantumBlockEncoding.RealAmplitudePreparation.normalized_sum_sq_LE
  {n : ℕ} (f : Fin (QuantumBlockEncoding.gridSize n) → ℝ)
  (positive : ∀ (j : Fin (QuantumBlockEncoding.gridSize n)), 0 < f j) :
  ∑ j, (f j / √(∑ i, f i ^ 2)) ^ 2 = 1
    theorem QuantumBlockEncoding.RealAmplitudePreparation.normalized_sum_sq_LE
  {n : ℕ}
  (f :
    Fin
        (QuantumBlockEncoding.gridSize
          n) →
      ℝ)
  (positive :
    ∀
      (j :
        Fin
          (QuantumBlockEncoding.gridSize
            n)),
      0 < f j) :
  ∑ j, (f j / √(∑ i, f i ^ 2)) ^ 2 = 1