6.33. QuantumBlockEncoding/StoredIsometryCompletion.lean🔗

59 explicit public declarations, in source order.

Definition6.33.1

uses 0used by 0✓L∃∀N

Plain-English reading. This record groups the data and proof fields needed for “positions”. A proposition-valued field is a requirement until a constructor supplies it.

Formal status. Data contract in the default import surface; proposition-valued fields are obligations, not automatically established facts.

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

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

Lean code for Definition6.33.1●1 definition

structure(2 fields)defined in QuantumBlockEncoding/StoredIsometryCompletion.lean

complete

structure QuantumBlockEncoding.StoredIsometryCompletion.Positions (N r : ℕ) : Type

structure QuantumBlockEncoding.StoredIsometryCompletion.Positions
  (N r : ℕ) : Type

Fields

values : Vector (Fin N) r

injective : Function.Injective fun i => self.values[↑i]

Definition6.33.2

uses 0used by 0✓L∃∀N

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

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

Lean code for Definition6.33.2●1 definition

defdefined in QuantumBlockEncoding/StoredIsometryCompletion.lean

complete

def QuantumBlockEncoding.StoredIsometryCompletion.Positions.embedding
  {N r : ℕ}
  (e : QuantumBlockEncoding.StoredIsometryCompletion.Positions N r) :
  Fin r ↪ Fin N

def QuantumBlockEncoding.StoredIsometryCompletion.Positions.embedding
  {N r : ℕ}
  (e :
    QuantumBlockEncoding.StoredIsometryCompletion.Positions
      N r) :
  Fin r ↪ Fin N

Definition6.33.3

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “materialize”. Materialize a counted physical-label generator.

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. Materialize a counted physical-label generator. Injectivity is an input contract, not a charged search for a proof or a freely evaluated embedding.

Declaration kind. def.

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

Lean code for Definition6.33.3●1 definition

defdefined in QuantumBlockEncoding/StoredIsometryCompletion.lean

complete

def QuantumBlockEncoding.StoredIsometryCompletion.Positions.materialize
  {N r : ℕ} (f : Fin r → QuantumBlockEncoding.StoredGivens.Run (Fin N))
  (injective : Function.Injective fun i => (f i).value) :
  QuantumBlockEncoding.StoredGivens.Run
    (QuantumBlockEncoding.StoredIsometryCompletion.Positions N r)

def QuantumBlockEncoding.StoredIsometryCompletion.Positions.materialize
  {N r : ℕ}
  (f :
    Fin r →
      QuantumBlockEncoding.StoredGivens.Run
        (Fin N))
  (injective :
    Function.Injective fun i =>
      (f i).value) :
  QuantumBlockEncoding.StoredGivens.Run
    (QuantumBlockEncoding.StoredIsometryCompletion.Positions
      N r)

Materialize a counted physical-label generator. Injectivity is an input
contract, not a charged search for a proof or a freely evaluated embedding.

Theorem6.33.4

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.33.4●1 theorem

theoremdefined in QuantumBlockEncoding/StoredIsometryCompletion.lean

complete

theorem QuantumBlockEncoding.StoredIsometryCompletion.Positions.materialize_value
  {N r : ℕ} (f : Fin r → QuantumBlockEncoding.StoredGivens.Run (Fin N))
  (injective : Function.Injective fun i => (f i).value) (i : Fin r) :
  (QuantumBlockEncoding.StoredIsometryCompletion.Positions.materialize f
            injective).value.embedding
      i =
    (f i).value

theorem QuantumBlockEncoding.StoredIsometryCompletion.Positions.materialize_value
  {N r : ℕ}
  (f :
    Fin r →
      QuantumBlockEncoding.StoredGivens.Run
        (Fin N))
  (injective :
    Function.Injective fun i =>
      (f i).value)
  (i : Fin r) :
  (QuantumBlockEncoding.StoredIsometryCompletion.Positions.materialize
            f injective).value.embedding
      i =
    (f i).value

Theorem6.33.5

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.33.5●1 theorem

theoremdefined in QuantumBlockEncoding/StoredIsometryCompletion.lean

complete

theorem QuantumBlockEncoding.StoredIsometryCompletion.Positions.materialize_cost
  {N r : ℕ} (f : Fin r → QuantumBlockEncoding.StoredGivens.Run (Fin N))
  (injective : Function.Injective fun i => (f i).value)
  (op : QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredIsometryCompletion.Positions.materialize f
          injective).cost
      op =
    ∑ i, (f i).cost op +
      r *
        (2 *
            QuantumBlockEncoding.StoredGivens.tick
              QuantumBlockEncoding.StoredGivens.Op.read op +
          2 *
            QuantumBlockEncoding.StoredGivens.tick
              QuantumBlockEncoding.StoredGivens.Op.write op)

theorem QuantumBlockEncoding.StoredIsometryCompletion.Positions.materialize_cost
  {N r : ℕ}
  (f :
    Fin r →
      QuantumBlockEncoding.StoredGivens.Run
        (Fin N))
  (injective :
    Function.Injective fun i =>
      (f i).value)
  (op :
    QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredIsometryCompletion.Positions.materialize
          f injective).cost
      op =
    ∑ i, (f i).cost op +
      r *
        (2 *
            QuantumBlockEncoding.StoredGivens.tick
              QuantumBlockEncoding.StoredGivens.Op.read
              op +
          2 *
            QuantumBlockEncoding.StoredGivens.tick
              QuantumBlockEncoding.StoredGivens.Op.write
              op)

Definition6.33.6

uses 0used by 0✓L∃∀N

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

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

Lean code for Definition6.33.6●1 definition

defdefined in QuantumBlockEncoding/StoredIsometryCompletion.lean

complete

def QuantumBlockEncoding.StoredIsometryCompletion.transpose {N M : ℕ}
  (A : QuantumBlockEncoding.StoredGivens.StoredMatrix N M) :
  QuantumBlockEncoding.StoredGivens.Run
    (QuantumBlockEncoding.StoredGivens.StoredMatrix M N)

def QuantumBlockEncoding.StoredIsometryCompletion.transpose
  {N M : ℕ}
  (A :
    QuantumBlockEncoding.StoredGivens.StoredMatrix
      N M) :
  QuantumBlockEncoding.StoredGivens.Run
    (QuantumBlockEncoding.StoredGivens.StoredMatrix
      M N)

Theorem6.33.7

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.33.7●1 theorem

theoremdefined in QuantumBlockEncoding/StoredIsometryCompletion.lean

complete

theorem QuantumBlockEncoding.StoredIsometryCompletion.transpose_value {N M : ℕ}
  (A : QuantumBlockEncoding.StoredGivens.StoredMatrix N M) :
  QuantumBlockEncoding.StoredGivens.denote
      (QuantumBlockEncoding.StoredIsometryCompletion.transpose
          A).value =
    (QuantumBlockEncoding.StoredGivens.denote A).transpose

theorem QuantumBlockEncoding.StoredIsometryCompletion.transpose_value
  {N M : ℕ}
  (A :
    QuantumBlockEncoding.StoredGivens.StoredMatrix
      N M) :
  QuantumBlockEncoding.StoredGivens.denote
      (QuantumBlockEncoding.StoredIsometryCompletion.transpose
          A).value =
    (QuantumBlockEncoding.StoredGivens.denote
        A).transpose

Definition6.33.8

uses 0used by 0✓L∃∀N

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

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

Lean code for Definition6.33.8●1 definition

defdefined in QuantumBlockEncoding/StoredIsometryCompletion.lean

complete

def QuantumBlockEncoding.StoredIsometryCompletion.transposeBudget
  (N M : ℕ) : QuantumBlockEncoding.StoredGivens.Cost

def QuantumBlockEncoding.StoredIsometryCompletion.transposeBudget
  (N M : ℕ) :
  QuantumBlockEncoding.StoredGivens.Cost

Theorem6.33.9

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “transpose cost”; 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/StoredIsometryCompletion.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.33.9●1 theorem

theoremdefined in QuantumBlockEncoding/StoredIsometryCompletion.lean

complete

theorem QuantumBlockEncoding.StoredIsometryCompletion.transpose_cost {N M : ℕ}
  (A : QuantumBlockEncoding.StoredGivens.StoredMatrix N M)
  (op : QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredIsometryCompletion.transpose A).cost op =
    QuantumBlockEncoding.StoredIsometryCompletion.transposeBudget N M op

theorem QuantumBlockEncoding.StoredIsometryCompletion.transpose_cost
  {N M : ℕ}
  (A :
    QuantumBlockEncoding.StoredGivens.StoredMatrix
      N M)
  (op :
    QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredIsometryCompletion.transpose
          A).cost
      op =
    QuantumBlockEncoding.StoredIsometryCompletion.transposeBudget
      N M op

Definition6.33.10

uses 0used by 0✓L∃∀N

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

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

Lean code for Definition6.33.10●1 definition

defdefined in QuantumBlockEncoding/StoredIsometryCompletion.lean

complete

def QuantumBlockEncoding.StoredIsometryCompletion.prefixCompletion {N r : ℕ}
  (V : QuantumBlockEncoding.StoredGivens.StoredMatrix N r) :
  QuantumBlockEncoding.StoredGivens.Run
    (QuantumBlockEncoding.StoredGivens.StoredMatrix N N)

def QuantumBlockEncoding.StoredIsometryCompletion.prefixCompletion
  {N r : ℕ}
  (V :
    QuantumBlockEncoding.StoredGivens.StoredMatrix
      N r) :
  QuantumBlockEncoding.StoredGivens.Run
    (QuantumBlockEncoding.StoredGivens.StoredMatrix
      N N)

Theorem6.33.11

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “prefix completion value”; 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/StoredIsometryCompletion.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.33.11●1 theorem

theoremdefined in QuantumBlockEncoding/StoredIsometryCompletion.lean

complete

theorem QuantumBlockEncoding.StoredIsometryCompletion.prefixCompletion_value
  {N r : ℕ} (V : QuantumBlockEncoding.StoredGivens.StoredMatrix N r) :
  QuantumBlockEncoding.StoredGivens.denote
      (QuantumBlockEncoding.StoredIsometryCompletion.prefixCompletion
          V).value =
    QuantumBlockEncoding.ConstructiveIsometryCompletion.prefixCompletion
      (QuantumBlockEncoding.StoredGivens.denote V)

theorem QuantumBlockEncoding.StoredIsometryCompletion.prefixCompletion_value
  {N r : ℕ}
  (V :
    QuantumBlockEncoding.StoredGivens.StoredMatrix
      N r) :
  QuantumBlockEncoding.StoredGivens.denote
      (QuantumBlockEncoding.StoredIsometryCompletion.prefixCompletion
          V).value =
    QuantumBlockEncoding.ConstructiveIsometryCompletion.prefixCompletion
      (QuantumBlockEncoding.StoredGivens.denote
        V)

Definition6.33.12

uses 0used by 0✓L∃∀N

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

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

Lean code for Definition6.33.12●1 definition

defdefined in QuantumBlockEncoding/StoredIsometryCompletion.lean

complete

def QuantumBlockEncoding.StoredIsometryCompletion.prefixBudget (N r : ℕ) :
  QuantumBlockEncoding.StoredGivens.Cost

def QuantumBlockEncoding.StoredIsometryCompletion.prefixBudget
  (N r : ℕ) :
  QuantumBlockEncoding.StoredGivens.Cost

Theorem6.33.13

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “prefix completion cost 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/StoredIsometryCompletion.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.33.13●1 theorem

theoremdefined in QuantumBlockEncoding/StoredIsometryCompletion.lean

complete

theorem QuantumBlockEncoding.StoredIsometryCompletion.prefixCompletion_cost_le
  {N r : ℕ} (V : QuantumBlockEncoding.StoredGivens.StoredMatrix N r)
  (op : QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredIsometryCompletion.prefixCompletion
          V).cost
      op ≤
    QuantumBlockEncoding.StoredIsometryCompletion.prefixBudget N r op

theorem QuantumBlockEncoding.StoredIsometryCompletion.prefixCompletion_cost_le
  {N r : ℕ}
  (V :
    QuantumBlockEncoding.StoredGivens.StoredMatrix
      N r)
  (op :
    QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredIsometryCompletion.prefixCompletion
          V).cost
      op ≤
    QuantumBlockEncoding.StoredIsometryCompletion.prefixBudget
      N r op

Definition6.33.14

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “swap index”. Both equality decisions are actual charged operations; the second is skipped if the first comparison succeeds.

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. Both equality decisions are actual charged operations; the second is skipped if the first comparison succeeds.

Declaration kind. def.

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

Lean code for Definition6.33.14●1 definition

defdefined in QuantumBlockEncoding/StoredIsometryCompletion.lean

complete

def QuantumBlockEncoding.StoredIsometryCompletion.swapIndex {N : ℕ}
  (x y z : Fin N) : QuantumBlockEncoding.StoredGivens.Run (Fin N)

def QuantumBlockEncoding.StoredIsometryCompletion.swapIndex
  {N : ℕ} (x y z : Fin N) :
  QuantumBlockEncoding.StoredGivens.Run
    (Fin N)

Both equality decisions are actual charged operations; the second is
skipped if the first comparison succeeds.

Theorem6.33.15

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.33.15●1 theorem

theoremdefined in QuantumBlockEncoding/StoredIsometryCompletion.lean

complete

theorem QuantumBlockEncoding.StoredIsometryCompletion.swapIndex_value {N : ℕ}
  (x y z : Fin N) :
  (QuantumBlockEncoding.StoredIsometryCompletion.swapIndex x y
        z).value =
    (Equiv.swap x y) z

theorem QuantumBlockEncoding.StoredIsometryCompletion.swapIndex_value
  {N : ℕ} (x y z : Fin N) :
  (QuantumBlockEncoding.StoredIsometryCompletion.swapIndex
        x y z).value =
    (Equiv.swap x y) z

Theorem6.33.16

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.33.16●1 theorem

theoremdefined in QuantumBlockEncoding/StoredIsometryCompletion.lean

complete

theorem QuantumBlockEncoding.StoredIsometryCompletion.swapIndex_cost_le {N : ℕ}
  (x y z : Fin N) (op : QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredIsometryCompletion.swapIndex x y z).cost
      op ≤
    2 *
      QuantumBlockEncoding.StoredGivens.tick
        QuantumBlockEncoding.StoredGivens.Op.compare op

theorem QuantumBlockEncoding.StoredIsometryCompletion.swapIndex_cost_le
  {N : ℕ} (x y z : Fin N)
  (op :
    QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredIsometryCompletion.swapIndex
          x y z).cost
      op ≤
    2 *
      QuantumBlockEncoding.StoredGivens.tick
        QuantumBlockEncoding.StoredGivens.Op.compare
        op

Definition6.33.17

uses 0used by 0✓L∃∀N

Plain-English reading. This record groups the data and proof fields needed for “permutation table”. A proposition-valued field is a requirement until a constructor supplies it.

Formal status. Data contract in the default import surface; proposition-valued fields are obligations, not automatically established facts.

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

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

Lean code for Definition6.33.17●1 definition

structure(3 fields)defined in QuantumBlockEncoding/StoredIsometryCompletion.lean

complete

structure QuantumBlockEncoding.StoredIsometryCompletion.PermutationTable (N : ℕ) :
  Type

structure QuantumBlockEncoding.StoredIsometryCompletion.PermutationTable
  (N : ℕ) : Type

Fields

forward : Vector (Fin N) N

inverse : Vector (Fin N) N

polarity : ℝ

Definition6.33.18

uses 0used by 0✓L∃∀N

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

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

Lean code for Definition6.33.18●1 definition

defdefined in QuantumBlockEncoding/StoredIsometryCompletion.lean

complete

def QuantumBlockEncoding.StoredIsometryCompletion.identityPermutation
  (N : ℕ) :
  QuantumBlockEncoding.StoredGivens.Run
    (QuantumBlockEncoding.StoredIsometryCompletion.PermutationTable N)

def QuantumBlockEncoding.StoredIsometryCompletion.identityPermutation
  (N : ℕ) :
  QuantumBlockEncoding.StoredGivens.Run
    (QuantumBlockEncoding.StoredIsometryCompletion.PermutationTable
      N)

Definition6.33.19

uses 0used by 0✓L∃∀N

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

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

Lean code for Definition6.33.19●1 definition

defdefined in QuantumBlockEncoding/StoredIsometryCompletion.lean

complete

def QuantumBlockEncoding.StoredIsometryCompletion.swapPermutation {N : ℕ}
  (p : QuantumBlockEncoding.StoredIsometryCompletion.PermutationTable N)
  (x y : Fin N) :
  QuantumBlockEncoding.StoredGivens.Run
    (QuantumBlockEncoding.StoredIsometryCompletion.PermutationTable N)

def QuantumBlockEncoding.StoredIsometryCompletion.swapPermutation
  {N : ℕ}
  (p :
    QuantumBlockEncoding.StoredIsometryCompletion.PermutationTable
      N)
  (x y : Fin N) :
  QuantumBlockEncoding.StoredGivens.Run
    (QuantumBlockEncoding.StoredIsometryCompletion.PermutationTable
      N)

Theorem6.33.20

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.33.20●1 theorem

theoremdefined in QuantumBlockEncoding/StoredIsometryCompletion.lean

complete

theorem QuantumBlockEncoding.StoredIsometryCompletion.swapPermutation_forward
  {N : ℕ}
  (p : QuantumBlockEncoding.StoredIsometryCompletion.PermutationTable N)
  (x y i : Fin N) :
  (QuantumBlockEncoding.StoredIsometryCompletion.swapPermutation p x
            y).value.forward[↑i] =
    (Equiv.swap x y) p.forward[↑i]

theorem QuantumBlockEncoding.StoredIsometryCompletion.swapPermutation_forward
  {N : ℕ}
  (p :
    QuantumBlockEncoding.StoredIsometryCompletion.PermutationTable
      N)
  (x y i : Fin N) :
  (QuantumBlockEncoding.StoredIsometryCompletion.swapPermutation
            p x y).value.forward[↑i] =
    (Equiv.swap x y) p.forward[↑i]

Theorem6.33.21

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.33.21●1 theorem

theoremdefined in QuantumBlockEncoding/StoredIsometryCompletion.lean

complete

theorem QuantumBlockEncoding.StoredIsometryCompletion.swapPermutation_inverse
  {N : ℕ}
  (p : QuantumBlockEncoding.StoredIsometryCompletion.PermutationTable N)
  (x y i : Fin N) :
  (QuantumBlockEncoding.StoredIsometryCompletion.swapPermutation p x
            y).value.inverse[↑i] =
    p.inverse[↑((Equiv.swap x y) i)]

theorem QuantumBlockEncoding.StoredIsometryCompletion.swapPermutation_inverse
  {N : ℕ}
  (p :
    QuantumBlockEncoding.StoredIsometryCompletion.PermutationTable
      N)
  (x y i : Fin N) :
  (QuantumBlockEncoding.StoredIsometryCompletion.swapPermutation
            p x y).value.inverse[↑i] =
    p.inverse[↑((Equiv.swap x y) i)]

Theorem6.33.22

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.33.22●1 theorem

theoremdefined in QuantumBlockEncoding/StoredIsometryCompletion.lean

complete

theorem QuantumBlockEncoding.StoredIsometryCompletion.swapPermutation_polarity
  {N : ℕ}
  (p : QuantumBlockEncoding.StoredIsometryCompletion.PermutationTable N)
  (x y : Fin N) :
  (QuantumBlockEncoding.StoredIsometryCompletion.swapPermutation p x
          y).value.polarity =
    if x = y then p.polarity else -p.polarity

theorem QuantumBlockEncoding.StoredIsometryCompletion.swapPermutation_polarity
  {N : ℕ}
  (p :
    QuantumBlockEncoding.StoredIsometryCompletion.PermutationTable
      N)
  (x y : Fin N) :
  (QuantumBlockEncoding.StoredIsometryCompletion.swapPermutation
          p x y).value.polarity =
    if x = y then p.polarity
    else -p.polarity

Definition6.33.23

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “real sign”. A proof-only interpretation of permutation orientation.

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 proof-only interpretation of permutation orientation.

Declaration kind. def.

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

Lean code for Definition6.33.23●1 definition

defdefined in QuantumBlockEncoding/StoredIsometryCompletion.lean

complete

def QuantumBlockEncoding.StoredIsometryCompletion.realSign {N : ℕ}
  (p : Equiv.Perm (Fin N)) : ℝ

def QuantumBlockEncoding.StoredIsometryCompletion.realSign
  {N : ℕ} (p : Equiv.Perm (Fin N)) : ℝ

A proof-only interpretation of permutation orientation.

Theorem6.33.24

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.33.24●1 theorem

theoremdefined in QuantumBlockEncoding/StoredIsometryCompletion.lean

complete

theorem QuantumBlockEncoding.StoredIsometryCompletion.realSign_swap_trans
  {N : ℕ} (p : Equiv.Perm (Fin N)) (x y : Fin N) :
  QuantumBlockEncoding.StoredIsometryCompletion.realSign
      (Equiv.trans p (Equiv.swap x y)) =
    if x = y then
      QuantumBlockEncoding.StoredIsometryCompletion.realSign p
    else -QuantumBlockEncoding.StoredIsometryCompletion.realSign p

theorem QuantumBlockEncoding.StoredIsometryCompletion.realSign_swap_trans
  {N : ℕ} (p : Equiv.Perm (Fin N))
  (x y : Fin N) :
  QuantumBlockEncoding.StoredIsometryCompletion.realSign
      (Equiv.trans p (Equiv.swap x y)) =
    if x = y then
      QuantumBlockEncoding.StoredIsometryCompletion.realSign
        p
    else
      -QuantumBlockEncoding.StoredIsometryCompletion.realSign
          p

Theorem6.33.25

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.33.25●1 theorem

theoremdefined in QuantumBlockEncoding/StoredIsometryCompletion.lean

complete

theorem QuantumBlockEncoding.StoredIsometryCompletion.realSign_one_iff {N : ℕ}
  (p : Equiv.Perm (Fin N)) :
  QuantumBlockEncoding.StoredIsometryCompletion.realSign p = 1 ↔
    Equiv.Perm.sign p = 1

theorem QuantumBlockEncoding.StoredIsometryCompletion.realSign_one_iff
  {N : ℕ} (p : Equiv.Perm (Fin N)) :
  QuantumBlockEncoding.StoredIsometryCompletion.realSign
        p =
      1 ↔
    Equiv.Perm.sign p = 1

Definition6.33.26

uses 0used by 0✓L∃∀N

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

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/StoredIsometryCompletion.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.33.26●1 definition

defdefined in QuantumBlockEncoding/StoredIsometryCompletion.lean

complete

def QuantumBlockEncoding.StoredIsometryCompletion.permutation {N r : ℕ}
  (hr : r ≤ N)
  (e : QuantumBlockEncoding.StoredIsometryCompletion.Positions N r)
  (k : ℕ) :
  k ≤ r →
    QuantumBlockEncoding.StoredGivens.Run
      (QuantumBlockEncoding.StoredIsometryCompletion.PermutationTable N)

def QuantumBlockEncoding.StoredIsometryCompletion.permutation
  {N r : ℕ} (hr : r ≤ N)
  (e :
    QuantumBlockEncoding.StoredIsometryCompletion.Positions
      N r)
  (k : ℕ) :
  k ≤ r →
    QuantumBlockEncoding.StoredGivens.Run
      (QuantumBlockEncoding.StoredIsometryCompletion.PermutationTable
        N)

Theorem6.33.27

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.33.27●1 theorem

theoremdefined in QuantumBlockEncoding/StoredIsometryCompletion.lean

complete

theorem QuantumBlockEncoding.StoredIsometryCompletion.permutation_forward
  {N r : ℕ} (hr : r ≤ N)
  (e : QuantumBlockEncoding.StoredIsometryCompletion.Positions N r)
  (k : ℕ) (hk : k ≤ r) (i : Fin N) :
  (QuantumBlockEncoding.StoredIsometryCompletion.permutation hr e k
            hk).value.forward[↑i] =
    (QuantumBlockEncoding.ConstructiveIsometryCompletion.extendPrefix hr
        e.embedding k hk)
      i

theorem QuantumBlockEncoding.StoredIsometryCompletion.permutation_forward
  {N r : ℕ} (hr : r ≤ N)
  (e :
    QuantumBlockEncoding.StoredIsometryCompletion.Positions
      N r)
  (k : ℕ) (hk : k ≤ r) (i : Fin N) :
  (QuantumBlockEncoding.StoredIsometryCompletion.permutation
            hr e k hk).value.forward[↑i] =
    (QuantumBlockEncoding.ConstructiveIsometryCompletion.extendPrefix
        hr e.embedding k hk)
      i

Theorem6.33.28

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.33.28●1 theorem

theoremdefined in QuantumBlockEncoding/StoredIsometryCompletion.lean

complete

theorem QuantumBlockEncoding.StoredIsometryCompletion.permutation_inverse
  {N r : ℕ} (hr : r ≤ N)
  (e : QuantumBlockEncoding.StoredIsometryCompletion.Positions N r)
  (k : ℕ) (hk : k ≤ r) (i : Fin N) :
  (QuantumBlockEncoding.StoredIsometryCompletion.permutation hr e k
            hk).value.inverse[↑i] =
    (Equiv.symm
        (QuantumBlockEncoding.ConstructiveIsometryCompletion.extendPrefix
          hr e.embedding k hk))
      i

theorem QuantumBlockEncoding.StoredIsometryCompletion.permutation_inverse
  {N r : ℕ} (hr : r ≤ N)
  (e :
    QuantumBlockEncoding.StoredIsometryCompletion.Positions
      N r)
  (k : ℕ) (hk : k ≤ r) (i : Fin N) :
  (QuantumBlockEncoding.StoredIsometryCompletion.permutation
            hr e k hk).value.inverse[↑i] =
    (Equiv.symm
        (QuantumBlockEncoding.ConstructiveIsometryCompletion.extendPrefix
          hr e.embedding k hk))
      i

Theorem6.33.29

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.33.29●1 theorem

theoremdefined in QuantumBlockEncoding/StoredIsometryCompletion.lean

complete

theorem QuantumBlockEncoding.StoredIsometryCompletion.permutation_polarity
  {N r : ℕ} (hr : r ≤ N)
  (e : QuantumBlockEncoding.StoredIsometryCompletion.Positions N r)
  (k : ℕ) (hk : k ≤ r) :
  (QuantumBlockEncoding.StoredIsometryCompletion.permutation hr e k
          hk).value.polarity =
    QuantumBlockEncoding.StoredIsometryCompletion.realSign
      (QuantumBlockEncoding.ConstructiveIsometryCompletion.extendPrefix
        hr e.embedding k hk)

theorem QuantumBlockEncoding.StoredIsometryCompletion.permutation_polarity
  {N r : ℕ} (hr : r ≤ N)
  (e :
    QuantumBlockEncoding.StoredIsometryCompletion.Positions
      N r)
  (k : ℕ) (hk : k ≤ r) :
  (QuantumBlockEncoding.StoredIsometryCompletion.permutation
          hr e k hk).value.polarity =
    QuantumBlockEncoding.StoredIsometryCompletion.realSign
      (QuantumBlockEncoding.ConstructiveIsometryCompletion.extendPrefix
        hr e.embedding k hk)

Theorem6.33.30

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “collect cost 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/StoredIsometryCompletion.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.33.30●1 theorem

theoremdefined in QuantumBlockEncoding/StoredIsometryCompletion.lean

complete

theorem QuantumBlockEncoding.StoredIsometryCompletion.collect_cost_le {α : Type}
  {n : ℕ} (f : Fin n → QuantumBlockEncoding.StoredGivens.Run α)
  (op : QuantumBlockEncoding.StoredGivens.Op) (cap : ℕ)
  (bounded : ∀ (i : Fin n), (f i).cost op ≤ cap) :
  (QuantumBlockEncoding.StoredGivens.collect f).cost op ≤
    n *
      (cap +
          2 *
            QuantumBlockEncoding.StoredGivens.tick
              QuantumBlockEncoding.StoredGivens.Op.read op +
        2 *
          QuantumBlockEncoding.StoredGivens.tick
            QuantumBlockEncoding.StoredGivens.Op.write op)

theorem QuantumBlockEncoding.StoredIsometryCompletion.collect_cost_le
  {α : Type} {n : ℕ}
  (f :
    Fin n →
      QuantumBlockEncoding.StoredGivens.Run
        α)
  (op :
    QuantumBlockEncoding.StoredGivens.Op)
  (cap : ℕ)
  (bounded :
    ∀ (i : Fin n), (f i).cost op ≤ cap) :
  (QuantumBlockEncoding.StoredGivens.collect
          f).cost
      op ≤
    n *
      (cap +
          2 *
            QuantumBlockEncoding.StoredGivens.tick
              QuantumBlockEncoding.StoredGivens.Op.read
              op +
        2 *
          QuantumBlockEncoding.StoredGivens.tick
            QuantumBlockEncoding.StoredGivens.Op.write
            op)

Definition6.33.31

uses 0used by 0✓L∃∀N

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

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

Lean code for Definition6.33.31●1 definition

defdefined in QuantumBlockEncoding/StoredIsometryCompletion.lean

complete

def QuantumBlockEncoding.StoredIsometryCompletion.swapBudget (N : ℕ) :
  QuantumBlockEncoding.StoredGivens.Cost

def QuantumBlockEncoding.StoredIsometryCompletion.swapBudget
  (N : ℕ) :
  QuantumBlockEncoding.StoredGivens.Cost

Theorem6.33.32

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.33.32●1 theorem

theoremdefined in QuantumBlockEncoding/StoredIsometryCompletion.lean

complete

theorem QuantumBlockEncoding.StoredIsometryCompletion.swapPermutation_cost_le
  {N : ℕ}
  (p : QuantumBlockEncoding.StoredIsometryCompletion.PermutationTable N)
  (x y : Fin N) (op : QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredIsometryCompletion.swapPermutation p x
          y).cost
      op ≤
    QuantumBlockEncoding.StoredIsometryCompletion.swapBudget N op

theorem QuantumBlockEncoding.StoredIsometryCompletion.swapPermutation_cost_le
  {N : ℕ}
  (p :
    QuantumBlockEncoding.StoredIsometryCompletion.PermutationTable
      N)
  (x y : Fin N)
  (op :
    QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredIsometryCompletion.swapPermutation
          p x y).cost
      op ≤
    QuantumBlockEncoding.StoredIsometryCompletion.swapBudget
      N op

Definition6.33.33

uses 0used by 0✓L∃∀N

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

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

Lean code for Definition6.33.33●1 definition

defdefined in QuantumBlockEncoding/StoredIsometryCompletion.lean

complete

def QuantumBlockEncoding.StoredIsometryCompletion.permutationBudget
  (N k : ℕ) : QuantumBlockEncoding.StoredGivens.Cost

def QuantumBlockEncoding.StoredIsometryCompletion.permutationBudget
  (N k : ℕ) :
  QuantumBlockEncoding.StoredGivens.Cost

Theorem6.33.34

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.33.34●1 theorem

theoremdefined in QuantumBlockEncoding/StoredIsometryCompletion.lean

complete

theorem QuantumBlockEncoding.StoredIsometryCompletion.identityPermutation_cost
  (N : ℕ) (op : QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredIsometryCompletion.identityPermutation
          N).cost
      op =
    4 * N *
      (QuantumBlockEncoding.StoredGivens.tick
          QuantumBlockEncoding.StoredGivens.Op.read op +
        QuantumBlockEncoding.StoredGivens.tick
          QuantumBlockEncoding.StoredGivens.Op.write op)

theorem QuantumBlockEncoding.StoredIsometryCompletion.identityPermutation_cost
  (N : ℕ)
  (op :
    QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredIsometryCompletion.identityPermutation
          N).cost
      op =
    4 * N *
      (QuantumBlockEncoding.StoredGivens.tick
          QuantumBlockEncoding.StoredGivens.Op.read
          op +
        QuantumBlockEncoding.StoredGivens.tick
          QuantumBlockEncoding.StoredGivens.Op.write
          op)

Theorem6.33.35

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.33.35●1 theorem

theoremdefined in QuantumBlockEncoding/StoredIsometryCompletion.lean

complete

theorem QuantumBlockEncoding.StoredIsometryCompletion.permutation_cost_le
  {N r : ℕ} (hr : r ≤ N)
  (e : QuantumBlockEncoding.StoredIsometryCompletion.Positions N r)
  (k : ℕ) (hk : k ≤ r) (op : QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredIsometryCompletion.permutation hr e k
          hk).cost
      op ≤
    QuantumBlockEncoding.StoredIsometryCompletion.permutationBudget N k
      op

theorem QuantumBlockEncoding.StoredIsometryCompletion.permutation_cost_le
  {N r : ℕ} (hr : r ≤ N)
  (e :
    QuantumBlockEncoding.StoredIsometryCompletion.Positions
      N r)
  (k : ℕ) (hk : k ≤ r)
  (op :
    QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredIsometryCompletion.permutation
          hr e k hk).cost
      op ≤
    QuantumBlockEncoding.StoredIsometryCompletion.permutationBudget
      N k op

Definition6.33.36

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “permute columns”. Every matrix entry reads its old column from the stored inverse table.

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. Every matrix entry reads its old column from the stored inverse table.

Declaration kind. def.

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

Lean code for Definition6.33.36●1 definition

defdefined in QuantumBlockEncoding/StoredIsometryCompletion.lean

complete

def QuantumBlockEncoding.StoredIsometryCompletion.permuteColumns {N : ℕ}
  (U : QuantumBlockEncoding.StoredGivens.StoredMatrix N N)
  (inverse : Vector (Fin N) N) :
  QuantumBlockEncoding.StoredGivens.Run
    (QuantumBlockEncoding.StoredGivens.StoredMatrix N N)

def QuantumBlockEncoding.StoredIsometryCompletion.permuteColumns
  {N : ℕ}
  (U :
    QuantumBlockEncoding.StoredGivens.StoredMatrix
      N N)
  (inverse : Vector (Fin N) N) :
  QuantumBlockEncoding.StoredGivens.Run
    (QuantumBlockEncoding.StoredGivens.StoredMatrix
      N N)

Every matrix entry reads its old column from the stored inverse table.

Theorem6.33.37

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.33.37●1 theorem

theoremdefined in QuantumBlockEncoding/StoredIsometryCompletion.lean

complete

theorem QuantumBlockEncoding.StoredIsometryCompletion.permuteColumns_value
  {N : ℕ} (U : QuantumBlockEncoding.StoredGivens.StoredMatrix N N)
  (inverse : Vector (Fin N) N) (row col : Fin N) :
  QuantumBlockEncoding.StoredGivens.denote
      (QuantumBlockEncoding.StoredIsometryCompletion.permuteColumns U
          inverse).value
      row col =
    QuantumBlockEncoding.StoredGivens.denote U row inverse[↑col]

theorem QuantumBlockEncoding.StoredIsometryCompletion.permuteColumns_value
  {N : ℕ}
  (U :
    QuantumBlockEncoding.StoredGivens.StoredMatrix
      N N)
  (inverse : Vector (Fin N) N)
  (row col : Fin N) :
  QuantumBlockEncoding.StoredGivens.denote
      (QuantumBlockEncoding.StoredIsometryCompletion.permuteColumns
          U inverse).value
      row col =
    QuantumBlockEncoding.StoredGivens.denote
      U row inverse[↑col]

Definition6.33.38

uses 0used by 0✓L∃∀N

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

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

Lean code for Definition6.33.38●1 definition

defdefined in QuantumBlockEncoding/StoredIsometryCompletion.lean

complete

def QuantumBlockEncoding.StoredIsometryCompletion.permuteBudget (N : ℕ) :
  QuantumBlockEncoding.StoredGivens.Cost

def QuantumBlockEncoding.StoredIsometryCompletion.permuteBudget
  (N : ℕ) :
  QuantumBlockEncoding.StoredGivens.Cost

Theorem6.33.39

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.33.39●1 theorem

theoremdefined in QuantumBlockEncoding/StoredIsometryCompletion.lean

complete

theorem QuantumBlockEncoding.StoredIsometryCompletion.permuteColumns_cost
  {N : ℕ} (U : QuantumBlockEncoding.StoredGivens.StoredMatrix N N)
  (inverse : Vector (Fin N) N)
  (op : QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredIsometryCompletion.permuteColumns U
          inverse).cost
      op =
    QuantumBlockEncoding.StoredIsometryCompletion.permuteBudget N op

theorem QuantumBlockEncoding.StoredIsometryCompletion.permuteColumns_cost
  {N : ℕ}
  (U :
    QuantumBlockEncoding.StoredGivens.StoredMatrix
      N N)
  (inverse : Vector (Fin N) N)
  (op :
    QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredIsometryCompletion.permuteColumns
          U inverse).cost
      op =
    QuantumBlockEncoding.StoredIsometryCompletion.permuteBudget
      N op

Definition6.33.40

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “sign column”. Negate exactly the spare entry of each stored row.

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. Negate exactly the spare entry of each stored row. Full row copies are charged, including the untouched entries, so no in-place storage is assumed.

Declaration kind. def.

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

Lean code for Definition6.33.40●1 definition

defdefined in QuantumBlockEncoding/StoredIsometryCompletion.lean

complete

def QuantumBlockEncoding.StoredIsometryCompletion.signColumn {N : ℕ}
  (U : QuantumBlockEncoding.StoredGivens.StoredMatrix N N)
  (spare : Fin N) :
  QuantumBlockEncoding.StoredGivens.Run
    (QuantumBlockEncoding.StoredGivens.StoredMatrix N N)

def QuantumBlockEncoding.StoredIsometryCompletion.signColumn
  {N : ℕ}
  (U :
    QuantumBlockEncoding.StoredGivens.StoredMatrix
      N N)
  (spare : Fin N) :
  QuantumBlockEncoding.StoredGivens.Run
    (QuantumBlockEncoding.StoredGivens.StoredMatrix
      N N)

Negate exactly the spare entry of each stored row. Full row copies are
charged, including the untouched entries, so no in-place storage is assumed.

Theorem6.33.41

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.33.41●1 theorem

theoremdefined in QuantumBlockEncoding/StoredIsometryCompletion.lean

complete

theorem QuantumBlockEncoding.StoredIsometryCompletion.signColumn_value {N : ℕ}
  (U : QuantumBlockEncoding.StoredGivens.StoredMatrix N N)
  (spare : Fin N) :
  QuantumBlockEncoding.StoredGivens.denote
      (QuantumBlockEncoding.StoredIsometryCompletion.signColumn U
          spare).value =
    QuantumBlockEncoding.StoredGivens.denote U *
      QuantumBlockEncoding.RealIsometryCompletion.signFlip spare

theorem QuantumBlockEncoding.StoredIsometryCompletion.signColumn_value
  {N : ℕ}
  (U :
    QuantumBlockEncoding.StoredGivens.StoredMatrix
      N N)
  (spare : Fin N) :
  QuantumBlockEncoding.StoredGivens.denote
      (QuantumBlockEncoding.StoredIsometryCompletion.signColumn
          U spare).value =
    QuantumBlockEncoding.StoredGivens.denote
        U *
      QuantumBlockEncoding.RealIsometryCompletion.signFlip
        spare

Definition6.33.42

uses 0used by 0✓L∃∀N

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

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

Lean code for Definition6.33.42●1 definition

defdefined in QuantumBlockEncoding/StoredIsometryCompletion.lean

complete

def QuantumBlockEncoding.StoredIsometryCompletion.signBudget (N : ℕ) :
  QuantumBlockEncoding.StoredGivens.Cost

def QuantumBlockEncoding.StoredIsometryCompletion.signBudget
  (N : ℕ) :
  QuantumBlockEncoding.StoredGivens.Cost

Theorem6.33.43

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.33.43●1 theorem

theoremdefined in QuantumBlockEncoding/StoredIsometryCompletion.lean

complete

theorem QuantumBlockEncoding.StoredIsometryCompletion.signColumn_cost {N : ℕ}
  (U : QuantumBlockEncoding.StoredGivens.StoredMatrix N N)
  (spare : Fin N) (op : QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredIsometryCompletion.signColumn U
          spare).cost
      op =
    QuantumBlockEncoding.StoredIsometryCompletion.signBudget N op

theorem QuantumBlockEncoding.StoredIsometryCompletion.signColumn_cost
  {N : ℕ}
  (U :
    QuantumBlockEncoding.StoredGivens.StoredMatrix
      N N)
  (spare : Fin N)
  (op :
    QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredIsometryCompletion.signColumn
          U spare).cost
      op =
    QuantumBlockEncoding.StoredIsometryCompletion.signBudget
      N op

Definition6.33.44

uses 0used by 0✓L∃∀N

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

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

Lean code for Definition6.33.44●1 definition

defdefined in QuantumBlockEncoding/StoredIsometryCompletion.lean

complete

def QuantumBlockEncoding.StoredIsometryCompletion.placeColumns {N r : ℕ}
  (hr : r < N)
  (e : QuantumBlockEncoding.StoredIsometryCompletion.Positions N r)
  (U : QuantumBlockEncoding.StoredGivens.StoredMatrix N N) :
  QuantumBlockEncoding.StoredGivens.Run
    (QuantumBlockEncoding.StoredGivens.StoredMatrix N N)

def QuantumBlockEncoding.StoredIsometryCompletion.placeColumns
  {N r : ℕ} (hr : r < N)
  (e :
    QuantumBlockEncoding.StoredIsometryCompletion.Positions
      N r)
  (U :
    QuantumBlockEncoding.StoredGivens.StoredMatrix
      N N) :
  QuantumBlockEncoding.StoredGivens.Run
    (QuantumBlockEncoding.StoredGivens.StoredMatrix
      N N)

Theorem6.33.45

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.33.45●1 theorem

theoremdefined in QuantumBlockEncoding/StoredIsometryCompletion.lean

complete

theorem QuantumBlockEncoding.StoredIsometryCompletion.placeColumns_value
  {N r : ℕ} (hr : r < N)
  (e : QuantumBlockEncoding.StoredIsometryCompletion.Positions N r)
  (U : QuantumBlockEncoding.StoredGivens.StoredMatrix N N) :
  QuantumBlockEncoding.StoredGivens.denote
      (QuantumBlockEncoding.StoredIsometryCompletion.placeColumns hr e
          U).value =
    QuantumBlockEncoding.ConstructiveIsometryCompletion.placeColumns hr
      e.embedding (QuantumBlockEncoding.StoredGivens.denote U)

theorem QuantumBlockEncoding.StoredIsometryCompletion.placeColumns_value
  {N r : ℕ} (hr : r < N)
  (e :
    QuantumBlockEncoding.StoredIsometryCompletion.Positions
      N r)
  (U :
    QuantumBlockEncoding.StoredGivens.StoredMatrix
      N N) :
  QuantumBlockEncoding.StoredGivens.denote
      (QuantumBlockEncoding.StoredIsometryCompletion.placeColumns
          hr e U).value =
    QuantumBlockEncoding.ConstructiveIsometryCompletion.placeColumns
      hr e.embedding
      (QuantumBlockEncoding.StoredGivens.denote
        U)

Definition6.33.46

uses 0used by 0✓L∃∀N

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

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

Lean code for Definition6.33.46●1 definition

defdefined in QuantumBlockEncoding/StoredIsometryCompletion.lean

complete

def QuantumBlockEncoding.StoredIsometryCompletion.placeBudget (N r : ℕ) :
  QuantumBlockEncoding.StoredGivens.Cost

def QuantumBlockEncoding.StoredIsometryCompletion.placeBudget
  (N r : ℕ) :
  QuantumBlockEncoding.StoredGivens.Cost

Theorem6.33.47

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.33.47●1 theorem

theoremdefined in QuantumBlockEncoding/StoredIsometryCompletion.lean

complete

theorem QuantumBlockEncoding.StoredIsometryCompletion.placeColumns_cost_le
  {N r : ℕ} (hr : r < N)
  (e : QuantumBlockEncoding.StoredIsometryCompletion.Positions N r)
  (U : QuantumBlockEncoding.StoredGivens.StoredMatrix N N)
  (op : QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredIsometryCompletion.placeColumns hr e
          U).cost
      op ≤
    QuantumBlockEncoding.StoredIsometryCompletion.placeBudget N r op

theorem QuantumBlockEncoding.StoredIsometryCompletion.placeColumns_cost_le
  {N r : ℕ} (hr : r < N)
  (e :
    QuantumBlockEncoding.StoredIsometryCompletion.Positions
      N r)
  (U :
    QuantumBlockEncoding.StoredGivens.StoredMatrix
      N N)
  (op :
    QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredIsometryCompletion.placeColumns
          hr e U).cost
      op ≤
    QuantumBlockEncoding.StoredIsometryCompletion.placeBudget
      N r op

Definition6.33.48

uses 0used by 0✓L∃∀N

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

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

Lean code for Definition6.33.48●1 definition

defdefined in QuantumBlockEncoding/StoredIsometryCompletion.lean

complete

def QuantumBlockEncoding.StoredIsometryCompletion.complete {N r : ℕ}
  (hr : r < N) (V : QuantumBlockEncoding.StoredGivens.StoredMatrix N r)
  (e : QuantumBlockEncoding.StoredIsometryCompletion.Positions N r) :
  QuantumBlockEncoding.StoredGivens.Run
    (QuantumBlockEncoding.StoredGivens.StoredMatrix N N)

def QuantumBlockEncoding.StoredIsometryCompletion.complete
  {N r : ℕ} (hr : r < N)
  (V :
    QuantumBlockEncoding.StoredGivens.StoredMatrix
      N r)
  (e :
    QuantumBlockEncoding.StoredIsometryCompletion.Positions
      N r) :
  QuantumBlockEncoding.StoredGivens.Run
    (QuantumBlockEncoding.StoredGivens.StoredMatrix
      N N)

Theorem6.33.49

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.33.49●1 theorem

theoremdefined in QuantumBlockEncoding/StoredIsometryCompletion.lean

complete

theorem QuantumBlockEncoding.StoredIsometryCompletion.complete_value {N r : ℕ}
  (hr : r < N) (V : QuantumBlockEncoding.StoredGivens.StoredMatrix N r)
  (e : QuantumBlockEncoding.StoredIsometryCompletion.Positions N r) :
  QuantumBlockEncoding.StoredGivens.denote
      (QuantumBlockEncoding.StoredIsometryCompletion.complete hr V
          e).value =
    QuantumBlockEncoding.ConstructiveIsometryCompletion.complete hr
      (QuantumBlockEncoding.StoredGivens.denote V) e.embedding

theorem QuantumBlockEncoding.StoredIsometryCompletion.complete_value
  {N r : ℕ} (hr : r < N)
  (V :
    QuantumBlockEncoding.StoredGivens.StoredMatrix
      N r)
  (e :
    QuantumBlockEncoding.StoredIsometryCompletion.Positions
      N r) :
  QuantumBlockEncoding.StoredGivens.denote
      (QuantumBlockEncoding.StoredIsometryCompletion.complete
          hr V e).value =
    QuantumBlockEncoding.ConstructiveIsometryCompletion.complete
      hr
      (QuantumBlockEncoding.StoredGivens.denote
        V)
      e.embedding

Definition6.33.50

uses 0used by 0✓L∃∀N

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

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

Lean code for Definition6.33.50●1 definition

defdefined in QuantumBlockEncoding/StoredIsometryCompletion.lean

complete

def QuantumBlockEncoding.StoredIsometryCompletion.completeBudget (N r : ℕ) :
  QuantumBlockEncoding.StoredGivens.Cost

def QuantumBlockEncoding.StoredIsometryCompletion.completeBudget
  (N r : ℕ) :
  QuantumBlockEncoding.StoredGivens.Cost

Theorem6.33.51

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.33.51●1 theorem

theoremdefined in QuantumBlockEncoding/StoredIsometryCompletion.lean

complete

theorem QuantumBlockEncoding.StoredIsometryCompletion.complete_cost_le {N r : ℕ}
  (hr : r < N) (V : QuantumBlockEncoding.StoredGivens.StoredMatrix N r)
  (e : QuantumBlockEncoding.StoredIsometryCompletion.Positions N r)
  (op : QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredIsometryCompletion.complete hr V e).cost
      op ≤
    QuantumBlockEncoding.StoredIsometryCompletion.completeBudget N r op

theorem QuantumBlockEncoding.StoredIsometryCompletion.complete_cost_le
  {N r : ℕ} (hr : r < N)
  (V :
    QuantumBlockEncoding.StoredGivens.StoredMatrix
      N r)
  (e :
    QuantumBlockEncoding.StoredIsometryCompletion.Positions
      N r)
  (op :
    QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredIsometryCompletion.complete
          hr V e).cost
      op ≤
    QuantumBlockEncoding.StoredIsometryCompletion.completeBudget
      N r op

Theorem6.33.52

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.33.52●1 theorem

theoremdefined in QuantumBlockEncoding/StoredIsometryCompletion.lean

complete

theorem QuantumBlockEncoding.StoredIsometryCompletion.complete_spec {N r : ℕ}
  (hr : r < N) (V : QuantumBlockEncoding.StoredGivens.StoredMatrix N r)
  (e : QuantumBlockEncoding.StoredIsometryCompletion.Positions N r)
  (hV :
    (QuantumBlockEncoding.StoredGivens.denote V).transpose *
        QuantumBlockEncoding.StoredGivens.denote V =
      1) :
  (QuantumBlockEncoding.StoredGivens.denote
            (QuantumBlockEncoding.StoredIsometryCompletion.complete hr V
                e).value).transpose *
        QuantumBlockEncoding.StoredGivens.denote
          (QuantumBlockEncoding.StoredIsometryCompletion.complete hr V
              e).value =
      1 ∧
    (QuantumBlockEncoding.StoredGivens.denote
            (QuantumBlockEncoding.StoredIsometryCompletion.complete hr V
                e).value).det =
        1 ∧
      ∀ (row : Fin N) (a : Fin r),
        QuantumBlockEncoding.StoredGivens.denote
            (QuantumBlockEncoding.StoredIsometryCompletion.complete hr V
                e).value
            row (e.embedding a) =
          QuantumBlockEncoding.StoredGivens.denote V row a

theorem QuantumBlockEncoding.StoredIsometryCompletion.complete_spec
  {N r : ℕ} (hr : r < N)
  (V :
    QuantumBlockEncoding.StoredGivens.StoredMatrix
      N r)
  (e :
    QuantumBlockEncoding.StoredIsometryCompletion.Positions
      N r)
  (hV :
    (QuantumBlockEncoding.StoredGivens.denote
            V).transpose *
        QuantumBlockEncoding.StoredGivens.denote
          V =
      1) :
  (QuantumBlockEncoding.StoredGivens.denote
            (QuantumBlockEncoding.StoredIsometryCompletion.complete
                hr V e).value).transpose *
        QuantumBlockEncoding.StoredGivens.denote
          (QuantumBlockEncoding.StoredIsometryCompletion.complete
              hr V e).value =
      1 ∧
    (QuantumBlockEncoding.StoredGivens.denote
            (QuantumBlockEncoding.StoredIsometryCompletion.complete
                hr V e).value).det =
        1 ∧
      ∀ (row : Fin N) (a : Fin r),
        QuantumBlockEncoding.StoredGivens.denote
            (QuantumBlockEncoding.StoredIsometryCompletion.complete
                hr V e).value
            row (e.embedding a) =
          QuantumBlockEncoding.StoredGivens.denote
            V row a

Definition6.33.53

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “polynomial budget”. Expanded bound including the stored prefix matrix, both permutation tables, orientation tracking, column placement, and spare-column correction.

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. Expanded bound including the stored prefix matrix, both permutation tables, orientation tracking, column placement, and spare-column correction.

Declaration kind. def.

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

Lean code for Definition6.33.53●1 definition

defdefined in QuantumBlockEncoding/StoredIsometryCompletion.lean

complete

def QuantumBlockEncoding.StoredIsometryCompletion.polynomialBudget
  (N r : ℕ) : QuantumBlockEncoding.StoredGivens.Cost

def QuantumBlockEncoding.StoredIsometryCompletion.polynomialBudget
  (N r : ℕ) :
  QuantumBlockEncoding.StoredGivens.Cost

Expanded bound including the stored prefix matrix, both permutation
tables, orientation tracking, column placement, and spare-column correction.

Theorem6.33.54

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.33.54●1 theorem

theoremdefined in QuantumBlockEncoding/StoredIsometryCompletion.lean

complete

theorem QuantumBlockEncoding.StoredIsometryCompletion.completeBudget_eq
  (N r : ℕ) :
  QuantumBlockEncoding.StoredIsometryCompletion.completeBudget N r =
    QuantumBlockEncoding.StoredIsometryCompletion.polynomialBudget N r

theorem QuantumBlockEncoding.StoredIsometryCompletion.completeBudget_eq
  (N r : ℕ) :
  QuantumBlockEncoding.StoredIsometryCompletion.completeBudget
      N r =
    QuantumBlockEncoding.StoredIsometryCompletion.polynomialBudget
      N r

Theorem6.33.55

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.33.55●1 theorem

theoremdefined in QuantumBlockEncoding/StoredIsometryCompletion.lean

complete

theorem QuantumBlockEncoding.StoredIsometryCompletion.complete_polynomial_cost_le
  {N r : ℕ} (hr : r < N)
  (V : QuantumBlockEncoding.StoredGivens.StoredMatrix N r)
  (e : QuantumBlockEncoding.StoredIsometryCompletion.Positions N r)
  (op : QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredIsometryCompletion.complete hr V e).cost
      op ≤
    QuantumBlockEncoding.StoredIsometryCompletion.polynomialBudget N r
      op

theorem QuantumBlockEncoding.StoredIsometryCompletion.complete_polynomial_cost_le
  {N r : ℕ} (hr : r < N)
  (V :
    QuantumBlockEncoding.StoredGivens.StoredMatrix
      N r)
  (e :
    QuantumBlockEncoding.StoredIsometryCompletion.Positions
      N r)
  (op :
    QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredIsometryCompletion.complete
          hr V e).cost
      op ≤
    QuantumBlockEncoding.StoredIsometryCompletion.polynomialBudget
      N r op

Theorem6.33.56

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.33.56●1 theorem

theoremdefined in QuantumBlockEncoding/StoredIsometryCompletion.lean

complete

theorem QuantumBlockEncoding.StoredIsometryCompletion.complete_total_cost_le
  {N r : ℕ} (hr : r < N)
  (V : QuantumBlockEncoding.StoredGivens.StoredMatrix N r)
  (e : QuantumBlockEncoding.StoredIsometryCompletion.Positions N r) :
  QuantumBlockEncoding.StoredRectangularGivens.total
      (QuantumBlockEncoding.StoredIsometryCompletion.complete hr V
          e).cost ≤
    N * r * (22 * r + 30 * N + 43) + 20 * N * N + 27 * N + 5 * r + 3

theorem QuantumBlockEncoding.StoredIsometryCompletion.complete_total_cost_le
  {N r : ℕ} (hr : r < N)
  (V :
    QuantumBlockEncoding.StoredGivens.StoredMatrix
      N r)
  (e :
    QuantumBlockEncoding.StoredIsometryCompletion.Positions
      N r) :
  QuantumBlockEncoding.StoredRectangularGivens.total
      (QuantumBlockEncoding.StoredIsometryCompletion.complete
          hr V e).cost ≤
    N * r * (22 * r + 30 * N + 43) +
            20 * N * N +
          27 * N +
        5 * r +
      3

Definition6.33.57

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “complete from”. Source construction is composed as counted input producers, never an unpriced callback hidden inside the completion.

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. Source construction is composed as counted input producers, never an unpriced callback hidden inside the completion.

Declaration kind. def.

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

Lean code for Definition6.33.57●1 definition

defdefined in QuantumBlockEncoding/StoredIsometryCompletion.lean

complete

def QuantumBlockEncoding.StoredIsometryCompletion.completeFrom {N r : ℕ}
  (hr : r < N)
  (active :
    QuantumBlockEncoding.StoredGivens.Run
      (QuantumBlockEncoding.StoredGivens.StoredMatrix N r))
  (positions :
    QuantumBlockEncoding.StoredGivens.Run
      (QuantumBlockEncoding.StoredIsometryCompletion.Positions N r)) :
  QuantumBlockEncoding.StoredGivens.Run
    (QuantumBlockEncoding.StoredGivens.StoredMatrix N N)

def QuantumBlockEncoding.StoredIsometryCompletion.completeFrom
  {N r : ℕ} (hr : r < N)
  (active :
    QuantumBlockEncoding.StoredGivens.Run
      (QuantumBlockEncoding.StoredGivens.StoredMatrix
        N r))
  (positions :
    QuantumBlockEncoding.StoredGivens.Run
      (QuantumBlockEncoding.StoredIsometryCompletion.Positions
        N r)) :
  QuantumBlockEncoding.StoredGivens.Run
    (QuantumBlockEncoding.StoredGivens.StoredMatrix
      N N)

Source construction is composed as counted input producers, never an
unpriced callback hidden inside the completion.

Theorem6.33.58

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.33.58●1 theorem

theoremdefined in QuantumBlockEncoding/StoredIsometryCompletion.lean

complete

theorem QuantumBlockEncoding.StoredIsometryCompletion.completeFrom_value
  {N r : ℕ} (hr : r < N)
  (active :
    QuantumBlockEncoding.StoredGivens.Run
      (QuantumBlockEncoding.StoredGivens.StoredMatrix N r))
  (positions :
    QuantumBlockEncoding.StoredGivens.Run
      (QuantumBlockEncoding.StoredIsometryCompletion.Positions N r)) :
  QuantumBlockEncoding.StoredGivens.denote
      (QuantumBlockEncoding.StoredIsometryCompletion.completeFrom hr
          active positions).value =
    QuantumBlockEncoding.ConstructiveIsometryCompletion.complete hr
      (QuantumBlockEncoding.StoredGivens.denote active.value)
      positions.value.embedding

theorem QuantumBlockEncoding.StoredIsometryCompletion.completeFrom_value
  {N r : ℕ} (hr : r < N)
  (active :
    QuantumBlockEncoding.StoredGivens.Run
      (QuantumBlockEncoding.StoredGivens.StoredMatrix
        N r))
  (positions :
    QuantumBlockEncoding.StoredGivens.Run
      (QuantumBlockEncoding.StoredIsometryCompletion.Positions
        N r)) :
  QuantumBlockEncoding.StoredGivens.denote
      (QuantumBlockEncoding.StoredIsometryCompletion.completeFrom
          hr active positions).value =
    QuantumBlockEncoding.ConstructiveIsometryCompletion.complete
      hr
      (QuantumBlockEncoding.StoredGivens.denote
        active.value)
      positions.value.embedding

Theorem6.33.59

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.33.59●1 theorem

theoremdefined in QuantumBlockEncoding/StoredIsometryCompletion.lean

complete

theorem QuantumBlockEncoding.StoredIsometryCompletion.completeFrom_cost_le
  {N r : ℕ} (hr : r < N)
  (active :
    QuantumBlockEncoding.StoredGivens.Run
      (QuantumBlockEncoding.StoredGivens.StoredMatrix N r))
  (positions :
    QuantumBlockEncoding.StoredGivens.Run
      (QuantumBlockEncoding.StoredIsometryCompletion.Positions N r))
  (op : QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredIsometryCompletion.completeFrom hr active
          positions).cost
      op ≤
    active.cost op + positions.cost op +
      QuantumBlockEncoding.StoredIsometryCompletion.polynomialBudget N r
        op

theorem QuantumBlockEncoding.StoredIsometryCompletion.completeFrom_cost_le
  {N r : ℕ} (hr : r < N)
  (active :
    QuantumBlockEncoding.StoredGivens.Run
      (QuantumBlockEncoding.StoredGivens.StoredMatrix
        N r))
  (positions :
    QuantumBlockEncoding.StoredGivens.Run
      (QuantumBlockEncoding.StoredIsometryCompletion.Positions
        N r))
  (op :
    QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredIsometryCompletion.completeFrom
          hr active positions).cost
      op ≤
    active.cost op + positions.cost op +
      QuantumBlockEncoding.StoredIsometryCompletion.polynomialBudget
        N r op