6.15. QuantumBlockEncoding/PrimitiveCircuitPerturbation.lean🔗

12 explicit public declarations, in source order.

Definition6.15.1

uses 0used by 0✓L∃∀N

Plain-English reading. This type lists the allowed alternatives for “gate aligned”; its constructors are the cases that downstream code must handle.

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. Circuit and register semantics, reusable tensor-train and matrix constructions, and explicit exact-real storage-cost refinements. Each declaration's hypotheses and conclusion fix its certified scope.

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. inductive.

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

Lean code for Definition6.15.1●1 definition

inductive(2 constructors, Prop, 4 parameters)defined in QuantumBlockEncoding/PrimitiveCircuitPerturbation.lean

complete

inductive QuantumBlockEncoding.PrimitiveCircuitPerturbation.GateAligned
  {qubits : ℕ} (δ : ℝ) :
  QuantumBlockEncoding.PrimitiveGate qubits →
    QuantumBlockEncoding.PrimitiveGate qubits → Prop

inductive QuantumBlockEncoding.PrimitiveCircuitPerturbation.GateAligned
  {qubits : ℕ} (δ : ℝ) :
  QuantumBlockEncoding.PrimitiveGate
      qubits →
    QuantumBlockEncoding.PrimitiveGate
        qubits →
      Prop

Constructors

unchanged {qubits : ℕ} {δ : ℝ}
  (gate : QuantumBlockEncoding.PrimitiveGate qubits) :
  QuantumBlockEncoding.PrimitiveCircuitPerturbation.GateAligned
    δ gate gate

ry {qubits : ℕ} {δ : ℝ} (target : Fin qubits)
  (a b : QuantumBlockEncoding.ExactAngle)
  (error : |a.eval - b.eval| ≤ δ) :
  QuantumBlockEncoding.PrimitiveCircuitPerturbation.GateAligned
    δ (QuantumBlockEncoding.PrimitiveGate.ry target a)
    (QuantumBlockEncoding.PrimitiveGate.ry target b)

Definition6.15.2

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “aligned”. A Forall₂ witness preserves every position, physical label and list length.

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

Technical source note. A Forall₂ witness preserves every position, physical label and list length.

Declaration kind. def.

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

Lean code for Definition6.15.2●1 definition

defdefined in QuantumBlockEncoding/PrimitiveCircuitPerturbation.lean

complete

def QuantumBlockEncoding.PrimitiveCircuitPerturbation.Aligned {qubits : ℕ}
  (δ : ℝ)
  (exact approximate : QuantumBlockEncoding.PrimitiveCircuit qubits) :
  Prop

def QuantumBlockEncoding.PrimitiveCircuitPerturbation.Aligned
  {qubits : ℕ} (δ : ℝ)
  (exact approximate :
    QuantumBlockEncoding.PrimitiveCircuit
      qubits) :
  Prop

A Forall₂ witness preserves every position, physical label and list length.

Theorem6.15.3

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “touched eq”; 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.

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/PrimitiveCircuitPerturbation.lean:25. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.15.3●1 theorem

theoremdefined in QuantumBlockEncoding/PrimitiveCircuitPerturbation.lean

complete

theorem QuantumBlockEncoding.PrimitiveCircuitPerturbation.GateAligned.touched_eq
  {qubits : ℕ} {δ : ℝ} {a b : QuantumBlockEncoding.PrimitiveGate qubits}
  (h :
    QuantumBlockEncoding.PrimitiveCircuitPerturbation.GateAligned δ a
      b) :
  a.touched = b.touched

theorem QuantumBlockEncoding.PrimitiveCircuitPerturbation.GateAligned.touched_eq
  {qubits : ℕ} {δ : ℝ}
  {a b :
    QuantumBlockEncoding.PrimitiveGate
      qubits}
  (h :
    QuantumBlockEncoding.PrimitiveCircuitPerturbation.GateAligned
      δ a b) :
  a.touched = b.touched

Theorem6.15.4

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “length eq”; 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.

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/PrimitiveCircuitPerturbation.lean:29. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.15.4●1 theorem

theoremdefined in QuantumBlockEncoding/PrimitiveCircuitPerturbation.lean

complete

theorem QuantumBlockEncoding.PrimitiveCircuitPerturbation.Aligned.length_eq
  {qubits : ℕ} {δ : ℝ}
  {exact approximate : QuantumBlockEncoding.PrimitiveCircuit qubits}
  (h :
    QuantumBlockEncoding.PrimitiveCircuitPerturbation.Aligned δ exact
      approximate) :
  List.length exact = List.length approximate

theorem QuantumBlockEncoding.PrimitiveCircuitPerturbation.Aligned.length_eq
  {qubits : ℕ} {δ : ℝ}
  {exact approximate :
    QuantumBlockEncoding.PrimitiveCircuit
      qubits}
  (h :
    QuantumBlockEncoding.PrimitiveCircuitPerturbation.Aligned
      δ exact approximate) :
  List.length exact =
    List.length approximate

Theorem6.15.5

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “refl”; 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.

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/PrimitiveCircuitPerturbation.lean:33. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.15.5●1 theorem

theoremdefined in QuantumBlockEncoding/PrimitiveCircuitPerturbation.lean

complete

theorem QuantumBlockEncoding.PrimitiveCircuitPerturbation.Aligned.refl
  {qubits : ℕ} (δ : ℝ)
  (circuit : QuantumBlockEncoding.PrimitiveCircuit qubits) :
  QuantumBlockEncoding.PrimitiveCircuitPerturbation.Aligned δ circuit
    circuit

theorem QuantumBlockEncoding.PrimitiveCircuitPerturbation.Aligned.refl
  {qubits : ℕ} (δ : ℝ)
  (circuit :
    QuantumBlockEncoding.PrimitiveCircuit
      qubits) :
  QuantumBlockEncoding.PrimitiveCircuitPerturbation.Aligned
    δ circuit circuit

Theorem6.15.6

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “distance 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.

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/PrimitiveCircuitPerturbation.lean:39. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.15.6●1 theorem

theoremdefined in QuantumBlockEncoding/PrimitiveCircuitPerturbation.lean

complete

theorem QuantumBlockEncoding.PrimitiveCircuitPerturbation.GateAligned.distance_le
  {qubits : ℕ} {δ : ℝ} (hδ : 0 ≤ δ)
  {exact approximate : QuantumBlockEncoding.PrimitiveGate qubits}
  (h :
    QuantumBlockEncoding.PrimitiveCircuitPerturbation.GateAligned δ
      exact approximate) :
  ‖QuantumBlockEncoding.evalPrimitiveGate approximate -
        QuantumBlockEncoding.evalPrimitiveGate exact‖ ≤
    δ / 2

theorem QuantumBlockEncoding.PrimitiveCircuitPerturbation.GateAligned.distance_le
  {qubits : ℕ} {δ : ℝ} (hδ : 0 ≤ δ)
  {exact approximate :
    QuantumBlockEncoding.PrimitiveGate
      qubits}
  (h :
    QuantumBlockEncoding.PrimitiveCircuitPerturbation.GateAligned
      δ exact approximate) :
  ‖QuantumBlockEncoding.evalPrimitiveGate
          approximate -
        QuantumBlockEncoding.evalPrimitiveGate
          exact‖ ≤
    δ / 2

Theorem6.15.7

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “aligned eval distance le”; the hypotheses and conclusion in the code panel fix its exact scope. No gate order is commuted: each induction step matches the actual evaluator.

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

Technical source note. No gate order is commuted: each induction step matches the actual evaluator.

Declaration kind. theorem.

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

Lean code for Theorem6.15.7●1 theorem

theoremdefined in QuantumBlockEncoding/PrimitiveCircuitPerturbation.lean

complete

theorem QuantumBlockEncoding.PrimitiveCircuitPerturbation.aligned_eval_distance_le
  {qubits : ℕ} {δ : ℝ} (hδ : 0 ≤ δ)
  {exact approximate : QuantumBlockEncoding.PrimitiveCircuit qubits}
  (aligned :
    QuantumBlockEncoding.PrimitiveCircuitPerturbation.Aligned δ exact
      approximate) :
  ‖QuantumBlockEncoding.evalPrimitiveCircuit approximate -
        QuantumBlockEncoding.evalPrimitiveCircuit exact‖ ≤
    ↑(List.length exact) * δ / 2

theorem QuantumBlockEncoding.PrimitiveCircuitPerturbation.aligned_eval_distance_le
  {qubits : ℕ} {δ : ℝ} (hδ : 0 ≤ δ)
  {exact approximate :
    QuantumBlockEncoding.PrimitiveCircuit
      qubits}
  (aligned :
    QuantumBlockEncoding.PrimitiveCircuitPerturbation.Aligned
      δ exact approximate) :
  ‖QuantumBlockEncoding.evalPrimitiveCircuit
          approximate -
        QuantumBlockEncoding.evalPrimitiveCircuit
          exact‖ ≤
    ↑(List.length exact) * δ / 2

No gate order is commuted: each induction step matches the actual evaluator.

Theorem6.15.8

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “aligned eval clm distance le”; the hypotheses and conclusion in the code panel fix its exact scope. Explicit Euclidean CLM formulation prevents accidental entrywise-norm use.

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

Technical source note. Explicit Euclidean CLM formulation prevents accidental entrywise-norm use.

Declaration kind. theorem.

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

Lean code for Theorem6.15.8●1 theorem

theoremdefined in QuantumBlockEncoding/PrimitiveCircuitPerturbation.lean

complete

theorem QuantumBlockEncoding.PrimitiveCircuitPerturbation.aligned_eval_clm_distance_le
  {qubits : ℕ} {δ : ℝ} (hδ : 0 ≤ δ)
  {exact approximate : QuantumBlockEncoding.PrimitiveCircuit qubits}
  (aligned :
    QuantumBlockEncoding.PrimitiveCircuitPerturbation.Aligned δ exact
      approximate) :
  ‖Matrix.toEuclideanCLM
        (QuantumBlockEncoding.evalPrimitiveCircuit approximate -
          QuantumBlockEncoding.evalPrimitiveCircuit exact)‖ ≤
    ↑(List.length exact) * δ / 2

theorem QuantumBlockEncoding.PrimitiveCircuitPerturbation.aligned_eval_clm_distance_le
  {qubits : ℕ} {δ : ℝ} (hδ : 0 ≤ δ)
  {exact approximate :
    QuantumBlockEncoding.PrimitiveCircuit
      qubits}
  (aligned :
    QuantumBlockEncoding.PrimitiveCircuitPerturbation.Aligned
      δ exact approximate) :
  ‖Matrix.toEuclideanCLM
        (QuantumBlockEncoding.evalPrimitiveCircuit
            approximate -
          QuantumBlockEncoding.evalPrimitiveCircuit
            exact)‖ ≤
    ↑(List.length exact) * δ / 2

Explicit Euclidean CLM formulation prevents accidental entrywise-norm use.

Definition6.15.9

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “hermite angle budget”. Sufficient uniform RY-angle budget for the existing actual prepare list.

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

Technical source note. Sufficient uniform RY-angle budget for the existing actual prepare list.

Declaration kind. def.

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

Lean code for Definition6.15.9●1 definition

defdefined in QuantumBlockEncoding/PrimitiveCircuitPerturbation.lean

complete

def QuantumBlockEncoding.PrimitiveCircuitPerturbation.hermiteAngleBudget
  (k n : ℕ) (ε : ℝ) : ℝ

def QuantumBlockEncoding.PrimitiveCircuitPerturbation.hermiteAngleBudget
  (k n : ℕ) (ε : ℝ) : ℝ

Sufficient uniform RY-angle budget for the existing actual prepare list.

Theorem6.15.10

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “hermite angle budget 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.

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/PrimitiveCircuitPerturbation.lean:91. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.15.10●1 theorem

theoremdefined in QuantumBlockEncoding/PrimitiveCircuitPerturbation.lean

complete

theorem QuantumBlockEncoding.PrimitiveCircuitPerturbation.hermiteAngleBudget_nonneg
  (k n : ℕ) {ε : ℝ} (hε : 0 ≤ ε) :
  0 ≤
    QuantumBlockEncoding.PrimitiveCircuitPerturbation.hermiteAngleBudget
      k n ε

theorem QuantumBlockEncoding.PrimitiveCircuitPerturbation.hermiteAngleBudget_nonneg
  (k n : ℕ) {ε : ℝ} (hε : 0 ≤ ε) :
  0 ≤
    QuantumBlockEncoding.PrimitiveCircuitPerturbation.hermiteAngleBudget
      k n ε

Theorem6.15.11

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “prepare conditional distance le”; the hypotheses and conclusion in the code panel fix its exact scope. A conditional consumer of the actual constructed Hermite circuit and its existing gate-count theorem.

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

Technical source note. A conditional consumer of the actual constructed Hermite circuit and its existing gate-count theorem. The alignment witness remains an input.

Declaration kind. theorem.

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

Lean code for Theorem6.15.11●1 theorem

theoremdefined in QuantumBlockEncoding/PrimitiveCircuitPerturbation.lean

complete

theorem QuantumBlockEncoding.PrimitiveCircuitPerturbation.prepare_conditional_distance_le
  (k n : ℕ) (L : ℝ) {ε : ℝ} (hε : 0 ≤ ε)
  (approximate :
    QuantumBlockEncoding.PrimitiveCircuit
      (n + 1 + QuantumBlockEncoding.HermiteFiniteChain.bondQubits k))
  (aligned :
    QuantumBlockEncoding.PrimitiveCircuitPerturbation.Aligned
      (QuantumBlockEncoding.PrimitiveCircuitPerturbation.hermiteAngleBudget
        k n ε)
      (QuantumBlockEncoding.ConstructiveHermitePreparation.prepare k n
        L)
      approximate) :
  ‖QuantumBlockEncoding.evalPrimitiveCircuit approximate -
        QuantumBlockEncoding.evalPrimitiveCircuit
          (QuantumBlockEncoding.ConstructiveHermitePreparation.prepare k
            n L)‖ ≤
    ε

theorem QuantumBlockEncoding.PrimitiveCircuitPerturbation.prepare_conditional_distance_le
  (k n : ℕ) (L : ℝ) {ε : ℝ} (hε : 0 ≤ ε)
  (approximate :
    QuantumBlockEncoding.PrimitiveCircuit
      (n + 1 +
        QuantumBlockEncoding.HermiteFiniteChain.bondQubits
          k))
  (aligned :
    QuantumBlockEncoding.PrimitiveCircuitPerturbation.Aligned
      (QuantumBlockEncoding.PrimitiveCircuitPerturbation.hermiteAngleBudget
        k n ε)
      (QuantumBlockEncoding.ConstructiveHermitePreparation.prepare
        k n L)
      approximate) :
  ‖QuantumBlockEncoding.evalPrimitiveCircuit
          approximate -
        QuantumBlockEncoding.evalPrimitiveCircuit
          (QuantumBlockEncoding.ConstructiveHermitePreparation.prepare
            k n L)‖ ≤
    ε

A conditional consumer of the actual constructed Hermite circuit and
its existing gate-count theorem. The alignment witness remains an input.

Theorem6.15.12

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “prepare conditional clm distance 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.

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/PrimitiveCircuitPerturbation.lean:121. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.15.12●1 theorem

theoremdefined in QuantumBlockEncoding/PrimitiveCircuitPerturbation.lean

complete

theorem QuantumBlockEncoding.PrimitiveCircuitPerturbation.prepare_conditional_clm_distance_le
  (k n : ℕ) (L : ℝ) {ε : ℝ} (hε : 0 ≤ ε)
  (approximate :
    QuantumBlockEncoding.PrimitiveCircuit
      (n + 1 + QuantumBlockEncoding.HermiteFiniteChain.bondQubits k))
  (aligned :
    QuantumBlockEncoding.PrimitiveCircuitPerturbation.Aligned
      (QuantumBlockEncoding.PrimitiveCircuitPerturbation.hermiteAngleBudget
        k n ε)
      (QuantumBlockEncoding.ConstructiveHermitePreparation.prepare k n
        L)
      approximate) :
  ‖Matrix.toEuclideanCLM
        (QuantumBlockEncoding.evalPrimitiveCircuit approximate -
          QuantumBlockEncoding.evalPrimitiveCircuit
            (QuantumBlockEncoding.ConstructiveHermitePreparation.prepare
              k n L))‖ ≤
    ε

theorem QuantumBlockEncoding.PrimitiveCircuitPerturbation.prepare_conditional_clm_distance_le
  (k n : ℕ) (L : ℝ) {ε : ℝ} (hε : 0 ≤ ε)
  (approximate :
    QuantumBlockEncoding.PrimitiveCircuit
      (n + 1 +
        QuantumBlockEncoding.HermiteFiniteChain.bondQubits
          k))
  (aligned :
    QuantumBlockEncoding.PrimitiveCircuitPerturbation.Aligned
      (QuantumBlockEncoding.PrimitiveCircuitPerturbation.hermiteAngleBudget
        k n ε)
      (QuantumBlockEncoding.ConstructiveHermitePreparation.prepare
        k n L)
      approximate) :
  ‖Matrix.toEuclideanCLM
        (QuantumBlockEncoding.evalPrimitiveCircuit
            approximate -
          QuantumBlockEncoding.evalPrimitiveCircuit
            (QuantumBlockEncoding.ConstructiveHermitePreparation.prepare
              k n L))‖ ≤
    ε