6.10. QuantumBlockEncoding/GrayGivensCompiler.lean🔗

26 explicit public declarations, in source order.

Theorem6.10.1

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.10.1●1 theorem

theoremdefined in QuantumBlockEncoding/GrayGivensCompiler.lean

complete

theorem QuantumBlockEncoding.GrayGivensCompiler.bit_eq_or_flip (a b : Fin 2) :
  a = b ∨ a = QuantumBlockEncoding.flipBit b

theorem QuantumBlockEncoding.GrayGivensCompiler.bit_eq_or_flip
  (a b : Fin 2) :
  a = b ∨
    a = QuantumBlockEncoding.flipBit b

Theorem6.10.2

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.10.2●1 theorem

theoremdefined in QuantumBlockEncoding/GrayGivensCompiler.lean

complete

theorem QuantumBlockEncoding.GrayGivensCompiler.x_context {n : ℕ}
  (target : Fin n) (bits : QuantumBlockEncoding.PrimitiveBasis n) :
  ((QuantumBlockEncoding.splitPrimitiveWire target)
        (QuantumBlockEncoding.xBasisAction target bits)).2 =
    ((QuantumBlockEncoding.splitPrimitiveWire target) bits).2

theorem QuantumBlockEncoding.GrayGivensCompiler.x_context
  {n : ℕ} (target : Fin n)
  (bits :
    QuantumBlockEncoding.PrimitiveBasis
      n) :
  ((QuantumBlockEncoding.splitPrimitiveWire
          target)
        (QuantumBlockEncoding.xBasisAction
          target bits)).2 =
    ((QuantumBlockEncoding.splitPrimitiveWire
          target)
        bits).2

Theorem6.10.3

uses 0used by 0✓L∃∀N

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

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

Lean code for Theorem6.10.3●1 theorem

theoremdefined in QuantumBlockEncoding/GrayGivensCompiler.lean

complete

theorem QuantumBlockEncoding.GrayGivensCompiler.same_context_iff {n : ℕ}
  (target : Fin n) (a b : QuantumBlockEncoding.PrimitiveBasis n) :
  ((QuantumBlockEncoding.splitPrimitiveWire target) a).2 =
      ((QuantumBlockEncoding.splitPrimitiveWire target) b).2 ↔
    a = b ∨ a = QuantumBlockEncoding.xBasisAction target b

theorem QuantumBlockEncoding.GrayGivensCompiler.same_context_iff
  {n : ℕ} (target : Fin n)
  (a b :
    QuantumBlockEncoding.PrimitiveBasis
      n) :
  ((QuantumBlockEncoding.splitPrimitiveWire
            target)
          a).2 =
      ((QuantumBlockEncoding.splitPrimitiveWire
            target)
          b).2 ↔
    a = b ∨
      a =
        QuantumBlockEncoding.xBasisAction
          target b

Definition6.10.4

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “controls equiv”.

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

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

Lean code for Definition6.10.4●1 definition

defdefined in QuantumBlockEncoding/GrayGivensCompiler.lean

complete

def QuantumBlockEncoding.GrayGivensCompiler.controlsEquiv {q : ℕ}
  (target : Fin (q + 1)) :
  Fin q ≃ QuantumBlockEncoding.OtherPrimitiveWires target

def QuantumBlockEncoding.GrayGivensCompiler.controlsEquiv
  {q : ℕ} (target : Fin (q + 1)) :
  Fin q ≃
    QuantumBlockEncoding.OtherPrimitiveWires
      target

Definition6.10.5

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “real transport”.

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

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

Lean code for Definition6.10.5●1 definition

defdefined in QuantumBlockEncoding/GrayGivensCompiler.lean

complete

def QuantumBlockEncoding.GrayGivensCompiler.realTransport {N n : ℕ}
  (basis : Fin N ≃ QuantumBlockEncoding.PrimitiveBasis n) :
  Matrix (Fin N) (Fin N) ℝ ≃ₐ[ℝ]
    Matrix (QuantumBlockEncoding.PrimitiveBasis n)
      (QuantumBlockEncoding.PrimitiveBasis n) ℝ

def QuantumBlockEncoding.GrayGivensCompiler.realTransport
  {N n : ℕ}
  (basis :
    Fin N ≃
      QuantumBlockEncoding.PrimitiveBasis
        n) :
  Matrix (Fin N) (Fin N) ℝ ≃ₐ[ℝ]
    Matrix
      (QuantumBlockEncoding.PrimitiveBasis
        n)
      (QuantumBlockEncoding.PrimitiveBasis
        n)
      ℝ

Definition6.10.6

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “transport”.

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

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

Lean code for Definition6.10.6●1 definition

defdefined in QuantumBlockEncoding/GrayGivensCompiler.lean

complete

def QuantumBlockEncoding.GrayGivensCompiler.transport {N n : ℕ}
  (basis : Fin N ≃ QuantumBlockEncoding.PrimitiveBasis n) :
  Matrix (Fin N) (Fin N) ℝ →+*
    Matrix (QuantumBlockEncoding.PrimitiveBasis n)
      (QuantumBlockEncoding.PrimitiveBasis n) ℂ

def QuantumBlockEncoding.GrayGivensCompiler.transport
  {N n : ℕ}
  (basis :
    Fin N ≃
      QuantumBlockEncoding.PrimitiveBasis
        n) :
  Matrix (Fin N) (Fin N) ℝ →+*
    Matrix
      (QuantumBlockEncoding.PrimitiveBasis
        n)
      (QuantumBlockEncoding.PrimitiveBasis
        n)
      ℂ

Theorem6.10.7

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.10.7●1 theorem

theoremdefined in QuantumBlockEncoding/GrayGivensCompiler.lean

complete

theorem QuantumBlockEncoding.GrayGivensCompiler.edge_plane_transport {N n : ℕ}
  (basis : Fin N ≃ QuantumBlockEncoding.PrimitiveBasis n)
  (first second : Fin N) (distinct : first ≠ second) (target : Fin n)
  (action :
    basis second =
      QuantumBlockEncoding.xBasisAction target (basis first))
  (theta : ℝ) :
  (QuantumBlockEncoding.GrayGivensCompiler.realTransport basis)
      (QuantumBlockEncoding.AdjacentGivens.planeMatrix first second
        theta) =
    QuantumBlockEncoding.selectedRyPlaneMatrix target
      ((QuantumBlockEncoding.splitPrimitiveWire target) (basis first)).2
      (if basis first target = 0 then theta else -theta)

theorem QuantumBlockEncoding.GrayGivensCompiler.edge_plane_transport
  {N n : ℕ}
  (basis :
    Fin N ≃
      QuantumBlockEncoding.PrimitiveBasis
        n)
  (first second : Fin N)
  (distinct : first ≠ second)
  (target : Fin n)
  (action :
    basis second =
      QuantumBlockEncoding.xBasisAction
        target (basis first))
  (theta : ℝ) :
  (QuantumBlockEncoding.GrayGivensCompiler.realTransport
        basis)
      (QuantumBlockEncoding.AdjacentGivens.planeMatrix
        first second theta) =
    QuantumBlockEncoding.selectedRyPlaneMatrix
      target
      ((QuantumBlockEncoding.splitPrimitiveWire
            target)
          (basis first)).2
      (if basis first target = 0 then
        theta
      else -theta)

Definition6.10.8

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “step target”.

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

Source: QuantumBlockEncoding/GrayGivensCompiler.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.10.8●1 definition

defdefined in QuantumBlockEncoding/GrayGivensCompiler.lean

complete

def QuantumBlockEncoding.GrayGivensCompiler.stepTarget {q : ℕ}
  (step : QuantumBlockEncoding.AdjacentGivens.Step (2 ^ (q + 1))) :
  Fin (q + 1)

def QuantumBlockEncoding.GrayGivensCompiler.stepTarget
  {q : ℕ}
  (step :
    QuantumBlockEncoding.AdjacentGivens.Step
      (2 ^ (q + 1))) :
  Fin (q + 1)

Theorem6.10.9

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “step target action”; 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/GrayGivensCompiler.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.10.9●1 theorem

theoremdefined in QuantumBlockEncoding/GrayGivensCompiler.lean

complete

theorem QuantumBlockEncoding.GrayGivensCompiler.stepTarget_action {q : ℕ}
  (step : QuantumBlockEncoding.AdjacentGivens.Step (2 ^ (q + 1))) :
  (QuantumBlockEncoding.GrayBasis.equiv (q + 1)) step.second =
    QuantumBlockEncoding.xBasisAction
      (QuantumBlockEncoding.GrayGivensCompiler.stepTarget step)
      ((QuantumBlockEncoding.GrayBasis.equiv (q + 1)) step.first)

theorem QuantumBlockEncoding.GrayGivensCompiler.stepTarget_action
  {q : ℕ}
  (step :
    QuantumBlockEncoding.AdjacentGivens.Step
      (2 ^ (q + 1))) :
  (QuantumBlockEncoding.GrayBasis.equiv
        (q + 1))
      step.second =
    QuantumBlockEncoding.xBasisAction
      (QuantumBlockEncoding.GrayGivensCompiler.stepTarget
        step)
      ((QuantumBlockEncoding.GrayBasis.equiv
          (q + 1))
        step.first)

Definition6.10.10

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “selected step”. One actual selected-rotation instruction.

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. One actual selected-rotation instruction. Reversed target-bit order negates the RY angle, while every non-target wire is an explicit control.

Declaration kind. def.

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

Lean code for Definition6.10.10●1 definition

defdefined in QuantumBlockEncoding/GrayGivensCompiler.lean

complete

def QuantumBlockEncoding.GrayGivensCompiler.selectedStep {q : ℕ}
  (step : QuantumBlockEncoding.AdjacentGivens.Step (2 ^ (q + 1))) :
  QuantumBlockEncoding.SelectedRyStep (q + 1) q

def QuantumBlockEncoding.GrayGivensCompiler.selectedStep
  {q : ℕ}
  (step :
    QuantumBlockEncoding.AdjacentGivens.Step
      (2 ^ (q + 1))) :
  QuantumBlockEncoding.SelectedRyStep
    (q + 1) q

One actual selected-rotation instruction. Reversed target-bit order negates
the RY angle, while every non-target wire is an explicit control.

Theorem6.10.11

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.10.11●1 theorem

theoremdefined in QuantumBlockEncoding/GrayGivensCompiler.lean

complete

theorem QuantumBlockEncoding.GrayGivensCompiler.selectedStep_matrix {q : ℕ}
  (step : QuantumBlockEncoding.AdjacentGivens.Step (2 ^ (q + 1))) :
  (QuantumBlockEncoding.GrayGivensCompiler.selectedStep step).matrix =
    (QuantumBlockEncoding.GrayGivensCompiler.transport
        (QuantumBlockEncoding.GrayBasis.equiv (q + 1)))
      step.matrix

theorem QuantumBlockEncoding.GrayGivensCompiler.selectedStep_matrix
  {q : ℕ}
  (step :
    QuantumBlockEncoding.AdjacentGivens.Step
      (2 ^ (q + 1))) :
  (QuantumBlockEncoding.GrayGivensCompiler.selectedStep
        step).matrix =
    (QuantumBlockEncoding.GrayGivensCompiler.transport
        (QuantumBlockEncoding.GrayBasis.equiv
          (q + 1)))
      step.matrix

Definition6.10.12

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “compile steps”.

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

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

Lean code for Definition6.10.12●1 definition

defdefined in QuantumBlockEncoding/GrayGivensCompiler.lean

complete

def QuantumBlockEncoding.GrayGivensCompiler.compileSteps {q : ℕ}
  (steps :
    List (QuantumBlockEncoding.AdjacentGivens.Step (2 ^ (q + 1)))) :
  QuantumBlockEncoding.PrimitiveCircuit (q + 1)

def QuantumBlockEncoding.GrayGivensCompiler.compileSteps
  {q : ℕ}
  (steps :
    List
      (QuantumBlockEncoding.AdjacentGivens.Step
        (2 ^ (q + 1)))) :
  QuantumBlockEncoding.PrimitiveCircuit
    (q + 1)

Theorem6.10.13

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.10.13●1 theorem

theoremdefined in QuantumBlockEncoding/GrayGivensCompiler.lean

complete

theorem QuantumBlockEncoding.GrayGivensCompiler.compileSteps_eval {q : ℕ}
  (steps :
    List (QuantumBlockEncoding.AdjacentGivens.Step (2 ^ (q + 1)))) :
  QuantumBlockEncoding.evalPrimitiveCircuit
      (QuantumBlockEncoding.GrayGivensCompiler.compileSteps steps) =
    (QuantumBlockEncoding.GrayGivensCompiler.transport
        (QuantumBlockEncoding.GrayBasis.equiv (q + 1)))
      (QuantumBlockEncoding.AdjacentGivens.stepsMatrix steps)

theorem QuantumBlockEncoding.GrayGivensCompiler.compileSteps_eval
  {q : ℕ}
  (steps :
    List
      (QuantumBlockEncoding.AdjacentGivens.Step
        (2 ^ (q + 1)))) :
  QuantumBlockEncoding.evalPrimitiveCircuit
      (QuantumBlockEncoding.GrayGivensCompiler.compileSteps
        steps) =
    (QuantumBlockEncoding.GrayGivensCompiler.transport
        (QuantumBlockEncoding.GrayBasis.equiv
          (q + 1)))
      (QuantumBlockEncoding.AdjacentGivens.stepsMatrix
        steps)

Theorem6.10.14

uses 0used by 0✓L∃∀N

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

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

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

Lean code for Theorem6.10.14●1 theorem

theoremdefined in QuantumBlockEncoding/GrayGivensCompiler.lean

complete

theorem QuantumBlockEncoding.GrayGivensCompiler.compileSteps_gateCount {q : ℕ}
  (steps :
    List (QuantumBlockEncoding.AdjacentGivens.Step (2 ^ (q + 1)))) :
  (QuantumBlockEncoding.GrayGivensCompiler.compileSteps
        steps).gateCount =
    steps.length * (2 ^ q + 2 * (2 ^ q - 1))

theorem QuantumBlockEncoding.GrayGivensCompiler.compileSteps_gateCount
  {q : ℕ}
  (steps :
    List
      (QuantumBlockEncoding.AdjacentGivens.Step
        (2 ^ (q + 1)))) :
  (QuantumBlockEncoding.GrayGivensCompiler.compileSteps
        steps).gateCount =
    steps.length *
      (2 ^ q + 2 * (2 ^ q - 1))

Definition6.10.15

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “compile so gray”. Input coordinates here are Gray-ordered natural indices.

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. Input coordinates here are Gray-ordered natural indices.

Declaration kind. def.

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

Lean code for Definition6.10.15●1 definition

defdefined in QuantumBlockEncoding/GrayGivensCompiler.lean

complete

def QuantumBlockEncoding.GrayGivensCompiler.compileSOGray {q : ℕ}
  (A : Matrix (Fin (2 ^ (q + 1))) (Fin (2 ^ (q + 1))) ℝ) :
  QuantumBlockEncoding.PrimitiveCircuit (q + 1)

def QuantumBlockEncoding.GrayGivensCompiler.compileSOGray
  {q : ℕ}
  (A :
    Matrix (Fin (2 ^ (q + 1)))
      (Fin (2 ^ (q + 1))) ℝ) :
  QuantumBlockEncoding.PrimitiveCircuit
    (q + 1)

Input coordinates here are Gray-ordered natural indices.

Theorem6.10.16

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.10.16●1 theorem

theoremdefined in QuantumBlockEncoding/GrayGivensCompiler.lean

complete

theorem QuantumBlockEncoding.GrayGivensCompiler.compileSOGray_eval {q : ℕ}
  (A : Matrix (Fin (2 ^ (q + 1))) (Fin (2 ^ (q + 1))) ℝ)
  (orthogonal : A.transpose * A = 1) (determinant : A.det = 1) :
  QuantumBlockEncoding.evalPrimitiveCircuit
      (QuantumBlockEncoding.GrayGivensCompiler.compileSOGray A) =
    (QuantumBlockEncoding.GrayGivensCompiler.transport
        (QuantumBlockEncoding.GrayBasis.equiv (q + 1)))
      A

theorem QuantumBlockEncoding.GrayGivensCompiler.compileSOGray_eval
  {q : ℕ}
  (A :
    Matrix (Fin (2 ^ (q + 1)))
      (Fin (2 ^ (q + 1))) ℝ)
  (orthogonal : A.transpose * A = 1)
  (determinant : A.det = 1) :
  QuantumBlockEncoding.evalPrimitiveCircuit
      (QuantumBlockEncoding.GrayGivensCompiler.compileSOGray
        A) =
    (QuantumBlockEncoding.GrayGivensCompiler.transport
        (QuantumBlockEncoding.GrayBasis.equiv
          (q + 1)))
      A

Theorem6.10.17

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “compile so gray cubic bound”; 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/GrayGivensCompiler.lean:151. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.10.17●1 theorem

theoremdefined in QuantumBlockEncoding/GrayGivensCompiler.lean

complete

theorem QuantumBlockEncoding.GrayGivensCompiler.compileSOGray_cubic_bound
  {q : ℕ} (A : Matrix (Fin (2 ^ (q + 1))) (Fin (2 ^ (q + 1))) ℝ) :
  (QuantumBlockEncoding.GrayGivensCompiler.compileSOGray A).gateCount ≤
      6 * (2 ^ q) ^ 3 ∧
    (QuantumBlockEncoding.GrayGivensCompiler.compileSOGray
            A).resource.oracleCalls =
      0

theorem QuantumBlockEncoding.GrayGivensCompiler.compileSOGray_cubic_bound
  {q : ℕ}
  (A :
    Matrix (Fin (2 ^ (q + 1)))
      (Fin (2 ^ (q + 1))) ℝ) :
  (QuantumBlockEncoding.GrayGivensCompiler.compileSOGray
          A).gateCount ≤
      6 * (2 ^ q) ^ 3 ∧
    (QuantumBlockEncoding.GrayGivensCompiler.compileSOGray
            A).resource.oracleCalls =
      0

Definition6.10.18

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “gray coordinates”.

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

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

Lean code for Definition6.10.18●1 definition

defdefined in QuantumBlockEncoding/GrayGivensCompiler.lean

complete

def QuantumBlockEncoding.GrayGivensCompiler.grayCoordinates {q : ℕ}
  (A :
    Matrix (QuantumBlockEncoding.PrimitiveBasis (q + 1))
      (QuantumBlockEncoding.PrimitiveBasis (q + 1)) ℝ) :
  Matrix (Fin (2 ^ (q + 1))) (Fin (2 ^ (q + 1))) ℝ

def QuantumBlockEncoding.GrayGivensCompiler.grayCoordinates
  {q : ℕ}
  (A :
    Matrix
      (QuantumBlockEncoding.PrimitiveBasis
        (q + 1))
      (QuantumBlockEncoding.PrimitiveBasis
        (q + 1))
      ℝ) :
  Matrix (Fin (2 ^ (q + 1)))
    (Fin (2 ^ (q + 1))) ℝ

Definition6.10.19

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “compile so”. A circuit on the original named wires; Gray order is internal only.

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 circuit on the original named wires; Gray order is internal only.

Declaration kind. def.

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

Lean code for Definition6.10.19●1 definition

defdefined in QuantumBlockEncoding/GrayGivensCompiler.lean

complete

def QuantumBlockEncoding.GrayGivensCompiler.compileSO {q : ℕ}
  (A :
    Matrix (QuantumBlockEncoding.PrimitiveBasis (q + 1))
      (QuantumBlockEncoding.PrimitiveBasis (q + 1)) ℝ) :
  QuantumBlockEncoding.PrimitiveCircuit (q + 1)

def QuantumBlockEncoding.GrayGivensCompiler.compileSO
  {q : ℕ}
  (A :
    Matrix
      (QuantumBlockEncoding.PrimitiveBasis
        (q + 1))
      (QuantumBlockEncoding.PrimitiveBasis
        (q + 1))
      ℝ) :
  QuantumBlockEncoding.PrimitiveCircuit
    (q + 1)

A circuit on the original named wires; Gray order is internal only.

Theorem6.10.20

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.10.20●1 theorem

theoremdefined in QuantumBlockEncoding/GrayGivensCompiler.lean

complete

theorem QuantumBlockEncoding.GrayGivensCompiler.grayCoordinates_orthogonal
  {q : ℕ}
  (A :
    Matrix (QuantumBlockEncoding.PrimitiveBasis (q + 1))
      (QuantumBlockEncoding.PrimitiveBasis (q + 1)) ℝ)
  (orthogonal : A.transpose * A = 1) :
  (QuantumBlockEncoding.GrayGivensCompiler.grayCoordinates
          A).transpose *
      QuantumBlockEncoding.GrayGivensCompiler.grayCoordinates A =
    1

theorem QuantumBlockEncoding.GrayGivensCompiler.grayCoordinates_orthogonal
  {q : ℕ}
  (A :
    Matrix
      (QuantumBlockEncoding.PrimitiveBasis
        (q + 1))
      (QuantumBlockEncoding.PrimitiveBasis
        (q + 1))
      ℝ)
  (orthogonal : A.transpose * A = 1) :
  (QuantumBlockEncoding.GrayGivensCompiler.grayCoordinates
          A).transpose *
      QuantumBlockEncoding.GrayGivensCompiler.grayCoordinates
        A =
    1

Theorem6.10.21

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.10.21●1 theorem

theoremdefined in QuantumBlockEncoding/GrayGivensCompiler.lean

complete

theorem QuantumBlockEncoding.GrayGivensCompiler.grayCoordinates_det {q : ℕ}
  (A :
    Matrix (QuantumBlockEncoding.PrimitiveBasis (q + 1))
      (QuantumBlockEncoding.PrimitiveBasis (q + 1)) ℝ) :
  (QuantumBlockEncoding.GrayGivensCompiler.grayCoordinates A).det =
    A.det

theorem QuantumBlockEncoding.GrayGivensCompiler.grayCoordinates_det
  {q : ℕ}
  (A :
    Matrix
      (QuantumBlockEncoding.PrimitiveBasis
        (q + 1))
      (QuantumBlockEncoding.PrimitiveBasis
        (q + 1))
      ℝ) :
  (QuantumBlockEncoding.GrayGivensCompiler.grayCoordinates
        A).det =
    A.det

Theorem6.10.22

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “compile so eval”; the hypotheses and conclusion in the code panel fix its exact scope. No assumed plane realization or Gray adjacency: the actual finite primitive list realizes the original real SO matrix embedded in complex amplitudes.

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

Technical source note. No assumed plane realization or Gray adjacency: the actual finite primitive list realizes the original real SO matrix embedded in complex amplitudes.

Declaration kind. theorem.

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

Lean code for Theorem6.10.22●1 theorem

theoremdefined in QuantumBlockEncoding/GrayGivensCompiler.lean

complete

theorem QuantumBlockEncoding.GrayGivensCompiler.compileSO_eval {q : ℕ}
  (A :
    Matrix (QuantumBlockEncoding.PrimitiveBasis (q + 1))
      (QuantumBlockEncoding.PrimitiveBasis (q + 1)) ℝ)
  (orthogonal : A.transpose * A = 1) (determinant : A.det = 1) :
  QuantumBlockEncoding.evalPrimitiveCircuit
      (QuantumBlockEncoding.GrayGivensCompiler.compileSO A) =
    A.map Complex.ofReal

theorem QuantumBlockEncoding.GrayGivensCompiler.compileSO_eval
  {q : ℕ}
  (A :
    Matrix
      (QuantumBlockEncoding.PrimitiveBasis
        (q + 1))
      (QuantumBlockEncoding.PrimitiveBasis
        (q + 1))
      ℝ)
  (orthogonal : A.transpose * A = 1)
  (determinant : A.det = 1) :
  QuantumBlockEncoding.evalPrimitiveCircuit
      (QuantumBlockEncoding.GrayGivensCompiler.compileSO
        A) =
    A.map Complex.ofReal

No assumed plane realization or Gray adjacency: the actual finite primitive
list realizes the original real SO matrix embedded in complex amplitudes.

Theorem6.10.23

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “compile so cubic bound”; the hypotheses and conclusion in the code panel fix its exact scope. With 'S=2^q', the exact recursive selected-RY backend needs at most '6*S^3' primitive gates and no oracle calls, on the existing 'q+1' wires.

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

Technical source note. With 'S=2^q', the exact recursive selected-RY backend needs at most '6*S^3' primitive gates and no oracle calls, on the existing 'q+1' wires.

Declaration kind. theorem.

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

Lean code for Theorem6.10.23●1 theorem

theoremdefined in QuantumBlockEncoding/GrayGivensCompiler.lean

complete

theorem QuantumBlockEncoding.GrayGivensCompiler.compileSO_cubic_bound {q : ℕ}
  (A :
    Matrix (QuantumBlockEncoding.PrimitiveBasis (q + 1))
      (QuantumBlockEncoding.PrimitiveBasis (q + 1)) ℝ) :
  (QuantumBlockEncoding.GrayGivensCompiler.compileSO A).gateCount ≤
      6 * (2 ^ q) ^ 3 ∧
    (QuantumBlockEncoding.GrayGivensCompiler.compileSO
            A).resource.oracleCalls =
      0

theorem QuantumBlockEncoding.GrayGivensCompiler.compileSO_cubic_bound
  {q : ℕ}
  (A :
    Matrix
      (QuantumBlockEncoding.PrimitiveBasis
        (q + 1))
      (QuantumBlockEncoding.PrimitiveBasis
        (q + 1))
      ℝ) :
  (QuantumBlockEncoding.GrayGivensCompiler.compileSO
          A).gateCount ≤
      6 * (2 ^ q) ^ 3 ∧
    (QuantumBlockEncoding.GrayGivensCompiler.compileSO
            A).resource.oracleCalls =
      0

With `S=2^q`, the exact recursive selected-RY backend needs at most `6*S^3`
primitive gates and no oracle calls, on the existing `q+1` wires.

Theorem6.10.24

uses 0used by 0✓L∃∀N

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

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

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

Lean code for Theorem6.10.24●1 theorem

theoremdefined in QuantumBlockEncoding/GrayGivensCompiler.lean

complete

theorem QuantumBlockEncoding.GrayGivensCompiler.compileSO_gateCount {q : ℕ}
  (A :
    Matrix (QuantumBlockEncoding.PrimitiveBasis (q + 1))
      (QuantumBlockEncoding.PrimitiveBasis (q + 1)) ℝ) :
  (QuantumBlockEncoding.GrayGivensCompiler.compileSO A).gateCount =
    2 ^ (q + 1) * (2 ^ (q + 1) - 1) / 2 * (2 ^ q + 2 * (2 ^ q - 1))

theorem QuantumBlockEncoding.GrayGivensCompiler.compileSO_gateCount
  {q : ℕ}
  (A :
    Matrix
      (QuantumBlockEncoding.PrimitiveBasis
        (q + 1))
      (QuantumBlockEncoding.PrimitiveBasis
        (q + 1))
      ℝ) :
  (QuantumBlockEncoding.GrayGivensCompiler.compileSO
        A).gateCount =
    2 ^ (q + 1) * (2 ^ (q + 1) - 1) / 2 *
      (2 ^ q + 2 * (2 ^ q - 1))

Theorem6.10.25

uses 0used by 0✓L∃∀N

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

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

Lean code for Theorem6.10.25●1 theorem

theoremdefined in QuantumBlockEncoding/GrayGivensCompiler.lean

complete

theorem QuantumBlockEncoding.GrayGivensCompiler.compileSO_ryCount {q : ℕ}
  (A :
    Matrix (QuantumBlockEncoding.PrimitiveBasis (q + 1))
      (QuantumBlockEncoding.PrimitiveBasis (q + 1)) ℝ) :
  (QuantumBlockEncoding.GrayGivensCompiler.compileSO A).ryCount =
    2 ^ (q + 1) * (2 ^ (q + 1) - 1) / 2 * 2 ^ q

theorem QuantumBlockEncoding.GrayGivensCompiler.compileSO_ryCount
  {q : ℕ}
  (A :
    Matrix
      (QuantumBlockEncoding.PrimitiveBasis
        (q + 1))
      (QuantumBlockEncoding.PrimitiveBasis
        (q + 1))
      ℝ) :
  (QuantumBlockEncoding.GrayGivensCompiler.compileSO
        A).ryCount =
    2 ^ (q + 1) * (2 ^ (q + 1) - 1) / 2 *
      2 ^ q

Theorem6.10.26

uses 0used by 0✓L∃∀N

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

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

Lean code for Theorem6.10.26●1 theorem

theoremdefined in QuantumBlockEncoding/GrayGivensCompiler.lean

complete

theorem QuantumBlockEncoding.GrayGivensCompiler.compileSO_cxCount {q : ℕ}
  (A :
    Matrix (QuantumBlockEncoding.PrimitiveBasis (q + 1))
      (QuantumBlockEncoding.PrimitiveBasis (q + 1)) ℝ) :
  (QuantumBlockEncoding.GrayGivensCompiler.compileSO A).cxCount =
    2 ^ (q + 1) * (2 ^ (q + 1) - 1) / 2 * (2 * (2 ^ q - 1))

theorem QuantumBlockEncoding.GrayGivensCompiler.compileSO_cxCount
  {q : ℕ}
  (A :
    Matrix
      (QuantumBlockEncoding.PrimitiveBasis
        (q + 1))
      (QuantumBlockEncoding.PrimitiveBasis
        (q + 1))
      ℝ) :
  (QuantumBlockEncoding.GrayGivensCompiler.compileSO
        A).cxCount =
    2 ^ (q + 1) * (2 ^ (q + 1) - 1) / 2 *
      (2 * (2 ^ q - 1))