6.19. QuantumBlockEncoding/PrimitiveRyPerturbation.lean🔗

10 explicit public declarations, in source order.

Theorem6.19.1

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “standard ry centered difference”; 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. 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. theorem.

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

Lean code for Theorem6.19.1●1 theorem

theoremdefined in QuantumBlockEncoding/PrimitiveRyPerturbation.lean

complete

theorem QuantumBlockEncoding.PrimitiveRyPerturbation.standardRy_centered_difference
  (u v : ℝ) :
  QuantumBlockEncoding.standardRyMatrix (u + v) -
      QuantumBlockEncoding.standardRyMatrix (u - v) =
    ↑(2 * Real.sin (v / 2)) •
      QuantumBlockEncoding.standardRyMatrix (u + Real.pi)

theorem QuantumBlockEncoding.PrimitiveRyPerturbation.standardRy_centered_difference
  (u v : ℝ) :
  QuantumBlockEncoding.standardRyMatrix
        (u + v) -
      QuantumBlockEncoding.standardRyMatrix
        (u - v) =
    ↑(2 * Real.sin (v / 2)) •
      QuantumBlockEncoding.standardRyMatrix
        (u + Real.pi)

Theorem6.19.2

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “standard ry difference factor”; the hypotheses and conclusion in the code panel fix its exact scope. The scalar sign is retained; this is equality, not equality up to phase.

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

Technical source note. The scalar sign is retained; this is equality, not equality up to phase.

Declaration kind. theorem.

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

theoremdefined in QuantumBlockEncoding/PrimitiveRyPerturbation.lean

complete

theorem QuantumBlockEncoding.PrimitiveRyPerturbation.standardRy_difference_factor
  (a b : ℝ) :
  QuantumBlockEncoding.standardRyMatrix a -
      QuantumBlockEncoding.standardRyMatrix b =
    ↑(2 * Real.sin ((a - b) / 4)) •
      QuantumBlockEncoding.standardRyMatrix ((a + b) / 2 + Real.pi)

theorem QuantumBlockEncoding.PrimitiveRyPerturbation.standardRy_difference_factor
  (a b : ℝ) :
  QuantumBlockEncoding.standardRyMatrix
        a -
      QuantumBlockEncoding.standardRyMatrix
        b =
    ↑(2 * Real.sin ((a - b) / 4)) •
      QuantumBlockEncoding.standardRyMatrix
        ((a + b) / 2 + Real.pi)

The scalar sign is retained; this is equality, not equality up to phase.

Theorem6.19.3

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “lift sub”; 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/PrimitiveRyPerturbation.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.19.3●1 theorem

theoremdefined in QuantumBlockEncoding/PrimitiveRyPerturbation.lean

complete

theorem QuantumBlockEncoding.PrimitiveRyPerturbation.lift_sub {qubits : ℕ}
  (target : Fin qubits) (A B : Matrix (Fin 2) (Fin 2) ℂ) :
  QuantumBlockEncoding.liftPrimitiveOneQubit target (A - B) =
    QuantumBlockEncoding.liftPrimitiveOneQubit target A -
      QuantumBlockEncoding.liftPrimitiveOneQubit target B

theorem QuantumBlockEncoding.PrimitiveRyPerturbation.lift_sub
  {qubits : ℕ} (target : Fin qubits)
  (A B : Matrix (Fin 2) (Fin 2) ℂ) :
  QuantumBlockEncoding.liftPrimitiveOneQubit
      target (A - B) =
    QuantumBlockEncoding.liftPrimitiveOneQubit
        target A -
      QuantumBlockEncoding.liftPrimitiveOneQubit
        target B

Theorem6.19.4

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.19.4●1 theorem

theoremdefined in QuantumBlockEncoding/PrimitiveRyPerturbation.lean

complete

theorem QuantumBlockEncoding.PrimitiveRyPerturbation.lift_smul {qubits : ℕ}
  (target : Fin qubits) (c : ℂ) (A : Matrix (Fin 2) (Fin 2) ℂ) :
  QuantumBlockEncoding.liftPrimitiveOneQubit target (c • A) =
    c • QuantumBlockEncoding.liftPrimitiveOneQubit target A

theorem QuantumBlockEncoding.PrimitiveRyPerturbation.lift_smul
  {qubits : ℕ} (target : Fin qubits)
  (c : ℂ) (A : Matrix (Fin 2) (Fin 2) ℂ) :
  QuantumBlockEncoding.liftPrimitiveOneQubit
      target (c • A) =
    c •
      QuantumBlockEncoding.liftPrimitiveOneQubit
        target A

Theorem6.19.5

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.19.5●1 theorem

theoremdefined in QuantumBlockEncoding/PrimitiveRyPerturbation.lean

complete

theorem QuantumBlockEncoding.PrimitiveRyPerturbation.liftedRy_difference_factor
  {qubits : ℕ} (target : Fin qubits) (a b : ℝ) :
  QuantumBlockEncoding.liftPrimitiveOneQubit target
        (QuantumBlockEncoding.standardRyMatrix a) -
      QuantumBlockEncoding.liftPrimitiveOneQubit target
        (QuantumBlockEncoding.standardRyMatrix b) =
    ↑(2 * Real.sin ((a - b) / 4)) •
      QuantumBlockEncoding.liftPrimitiveOneQubit target
        (QuantumBlockEncoding.standardRyMatrix ((a + b) / 2 + Real.pi))

theorem QuantumBlockEncoding.PrimitiveRyPerturbation.liftedRy_difference_factor
  {qubits : ℕ} (target : Fin qubits)
  (a b : ℝ) :
  QuantumBlockEncoding.liftPrimitiveOneQubit
        target
        (QuantumBlockEncoding.standardRyMatrix
          a) -
      QuantumBlockEncoding.liftPrimitiveOneQubit
        target
        (QuantumBlockEncoding.standardRyMatrix
          b) =
    ↑(2 * Real.sin ((a - b) / 4)) •
      QuantumBlockEncoding.liftPrimitiveOneQubit
        target
        (QuantumBlockEncoding.standardRyMatrix
          ((a + b) / 2 + Real.pi))

Theorem6.19.6

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “lifted ry distance”; the hypotheses and conclusion in the code panel fix its exact scope. Exact L2 norm for every physical target and every number of spectators.

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

Technical source note. Exact L2 norm for every physical target and every number of spectators.

Declaration kind. theorem.

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

Lean code for Theorem6.19.6●1 theorem

theoremdefined in QuantumBlockEncoding/PrimitiveRyPerturbation.lean

complete

theorem QuantumBlockEncoding.PrimitiveRyPerturbation.liftedRy_distance
  {qubits : ℕ} (target : Fin qubits) (a b : ℝ) :
  ‖QuantumBlockEncoding.liftPrimitiveOneQubit target
          (QuantumBlockEncoding.standardRyMatrix a) -
        QuantumBlockEncoding.liftPrimitiveOneQubit target
          (QuantumBlockEncoding.standardRyMatrix b)‖ =
    2 * |Real.sin ((a - b) / 4)|

theorem QuantumBlockEncoding.PrimitiveRyPerturbation.liftedRy_distance
  {qubits : ℕ} (target : Fin qubits)
  (a b : ℝ) :
  ‖QuantumBlockEncoding.liftPrimitiveOneQubit
          target
          (QuantumBlockEncoding.standardRyMatrix
            a) -
        QuantumBlockEncoding.liftPrimitiveOneQubit
          target
          (QuantumBlockEncoding.standardRyMatrix
            b)‖ =
    2 * |Real.sin ((a - b) / 4)|

Exact L2 norm for every physical target and every number of spectators.

Theorem6.19.7

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.19.7●1 theorem

theoremdefined in QuantumBlockEncoding/PrimitiveRyPerturbation.lean

complete

theorem QuantumBlockEncoding.PrimitiveRyPerturbation.liftedRy_distance_le
  {qubits : ℕ} (target : Fin qubits) (a b : ℝ) :
  ‖QuantumBlockEncoding.liftPrimitiveOneQubit target
          (QuantumBlockEncoding.standardRyMatrix a) -
        QuantumBlockEncoding.liftPrimitiveOneQubit target
          (QuantumBlockEncoding.standardRyMatrix b)‖ ≤
    |a - b| / 2

theorem QuantumBlockEncoding.PrimitiveRyPerturbation.liftedRy_distance_le
  {qubits : ℕ} (target : Fin qubits)
  (a b : ℝ) :
  ‖QuantumBlockEncoding.liftPrimitiveOneQubit
          target
          (QuantumBlockEncoding.standardRyMatrix
            a) -
        QuantumBlockEncoding.liftPrimitiveOneQubit
          target
          (QuantumBlockEncoding.standardRyMatrix
            b)‖ ≤
    |a - b| / 2

Theorem6.19.8

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “eval ry distance”; the hypotheses and conclusion in the code panel fix its exact scope. This names the existing actual RY gate, not an abstract error assumption.

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

Technical source note. This names the existing actual RY gate, not an abstract error assumption.

Declaration kind. theorem.

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

Lean code for Theorem6.19.8●1 theorem

theoremdefined in QuantumBlockEncoding/PrimitiveRyPerturbation.lean

complete

theorem QuantumBlockEncoding.PrimitiveRyPerturbation.eval_ry_distance
  {qubits : ℕ} (target : Fin qubits)
  (a b : QuantumBlockEncoding.ExactAngle) :
  ‖QuantumBlockEncoding.evalPrimitiveGate
          (QuantumBlockEncoding.PrimitiveGate.ry target a) -
        QuantumBlockEncoding.evalPrimitiveGate
          (QuantumBlockEncoding.PrimitiveGate.ry target b)‖ =
    2 * |Real.sin ((a.eval - b.eval) / 4)|

theorem QuantumBlockEncoding.PrimitiveRyPerturbation.eval_ry_distance
  {qubits : ℕ} (target : Fin qubits)
  (a b :
    QuantumBlockEncoding.ExactAngle) :
  ‖QuantumBlockEncoding.evalPrimitiveGate
          (QuantumBlockEncoding.PrimitiveGate.ry
            target a) -
        QuantumBlockEncoding.evalPrimitiveGate
          (QuantumBlockEncoding.PrimitiveGate.ry
            target b)‖ =
    2 * |Real.sin ((a.eval - b.eval) / 4)|

This names the existing actual RY gate, not an abstract error assumption.

Theorem6.19.9

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.19.9●1 theorem

theoremdefined in QuantumBlockEncoding/PrimitiveRyPerturbation.lean

complete

theorem QuantumBlockEncoding.PrimitiveRyPerturbation.eval_ry_distance_le
  {qubits : ℕ} (target : Fin qubits)
  (a b : QuantumBlockEncoding.ExactAngle) :
  ‖QuantumBlockEncoding.evalPrimitiveGate
          (QuantumBlockEncoding.PrimitiveGate.ry target a) -
        QuantumBlockEncoding.evalPrimitiveGate
          (QuantumBlockEncoding.PrimitiveGate.ry target b)‖ ≤
    |a.eval - b.eval| / 2

theorem QuantumBlockEncoding.PrimitiveRyPerturbation.eval_ry_distance_le
  {qubits : ℕ} (target : Fin qubits)
  (a b :
    QuantumBlockEncoding.ExactAngle) :
  ‖QuantumBlockEncoding.evalPrimitiveGate
          (QuantumBlockEncoding.PrimitiveGate.ry
            target a) -
        QuantumBlockEncoding.evalPrimitiveGate
          (QuantumBlockEncoding.PrimitiveGate.ry
            target b)‖ ≤
    |a.eval - b.eval| / 2

Theorem6.19.10

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “eval ry clm distance le”; the hypotheses and conclusion in the code panel fix its exact scope. Explicit Euclidean continuous-linear-map form removes all norm-scope ambiguity.

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

Technical source note. Explicit Euclidean continuous-linear-map form removes all norm-scope ambiguity.

Declaration kind. theorem.

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

Lean code for Theorem6.19.10●1 theorem

theoremdefined in QuantumBlockEncoding/PrimitiveRyPerturbation.lean

complete

theorem QuantumBlockEncoding.PrimitiveRyPerturbation.eval_ry_clm_distance_le
  {qubits : ℕ} (target : Fin qubits)
  (a b : QuantumBlockEncoding.ExactAngle) :
  ‖Matrix.toEuclideanCLM
        (QuantumBlockEncoding.evalPrimitiveGate
            (QuantumBlockEncoding.PrimitiveGate.ry target a) -
          QuantumBlockEncoding.evalPrimitiveGate
            (QuantumBlockEncoding.PrimitiveGate.ry target b))‖ ≤
    |a.eval - b.eval| / 2

theorem QuantumBlockEncoding.PrimitiveRyPerturbation.eval_ry_clm_distance_le
  {qubits : ℕ} (target : Fin qubits)
  (a b :
    QuantumBlockEncoding.ExactAngle) :
  ‖Matrix.toEuclideanCLM
        (QuantumBlockEncoding.evalPrimitiveGate
            (QuantumBlockEncoding.PrimitiveGate.ry
              target a) -
          QuantumBlockEncoding.evalPrimitiveGate
            (QuantumBlockEncoding.PrimitiveGate.ry
              target b))‖ ≤
    |a.eval - b.eval| / 2

Explicit Euclidean continuous-linear-map form removes all norm-scope ambiguity.