6.13. QuantumBlockEncoding/PrimitiveBasisLE.lean🔗

33 explicit public declarations, in source order.

Definition6.13.1

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “primitive basis le equiv”. Convert named primitive bits to a flat little-endian matrix index.

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

Why it is in this chapter. Circuit and register semantics, reusable tensor-train and matrix constructions, and explicit exact-real storage-cost refinements. Each declaration's hypotheses and conclusion fix its certified scope.

Technical source note. Convert named primitive bits to a flat little-endian matrix index.

Declaration kind. def.

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

Lean code for Definition6.13.1●1 definition

defdefined in QuantumBlockEncoding/PrimitiveBasisLE.lean

complete

def QuantumBlockEncoding.primitiveBasisLEEquiv (q : ℕ) :
  QuantumBlockEncoding.PrimitiveBasis q ≃
    Fin (QuantumBlockEncoding.gridSize q)

def QuantumBlockEncoding.primitiveBasisLEEquiv
  (q : ℕ) :
  QuantumBlockEncoding.PrimitiveBasis q ≃
    Fin (QuantumBlockEncoding.gridSize q)

Convert named primitive bits to a flat little-endian matrix index.

Theorem6.13.2

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “primitive basis le equiv zero apply”; the hypotheses and conclusion in the code panel fix its exact scope.

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

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

Lean code for Theorem6.13.2●1 theorem

theoremdefined in QuantumBlockEncoding/PrimitiveBasisLE.lean

complete

theorem QuantumBlockEncoding.primitiveBasisLEEquiv_zero_apply
  (bits : QuantumBlockEncoding.PrimitiveBasis 0) :
  ↑((QuantumBlockEncoding.primitiveBasisLEEquiv 0) bits) = 0

theorem QuantumBlockEncoding.primitiveBasisLEEquiv_zero_apply
  (bits :
    QuantumBlockEncoding.PrimitiveBasis
      0) :
  ↑((QuantumBlockEncoding.primitiveBasisLEEquiv
          0)
        bits) =
    0

Theorem6.13.3

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “primitive basis le equiv succ value”; the hypotheses and conclusion in the code panel fix its exact scope. The recursive equation makes the little-endian convention inspectable.

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

Technical source note. The recursive equation makes the little-endian convention inspectable.

Declaration kind. theorem.

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

Lean code for Theorem6.13.3●1 theorem

theoremdefined in QuantumBlockEncoding/PrimitiveBasisLE.lean

complete

theorem QuantumBlockEncoding.primitiveBasisLEEquiv_succ_value (q : ℕ)
  (bits : QuantumBlockEncoding.PrimitiveBasis (q + 1)) :
  ↑((QuantumBlockEncoding.primitiveBasisLEEquiv (q + 1)) bits) =
    ↑(bits 0) +
      2 *
        ↑((QuantumBlockEncoding.primitiveBasisLEEquiv q) fun wire =>
            bits wire.succ)

theorem QuantumBlockEncoding.primitiveBasisLEEquiv_succ_value
  (q : ℕ)
  (bits :
    QuantumBlockEncoding.PrimitiveBasis
      (q + 1)) :
  ↑((QuantumBlockEncoding.primitiveBasisLEEquiv
          (q + 1))
        bits) =
    ↑(bits 0) +
      2 *
        ↑((QuantumBlockEncoding.primitiveBasisLEEquiv
              q)
            fun wire => bits wire.succ)

The recursive equation makes the little-endian convention inspectable.

Theorem6.13.4

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “primitive basis le equiv six value”; the hypotheses and conclusion in the code panel fix its exact scope. Six-wire expansion used by the fixed Robin executable benchmark.

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

Technical source note. Six-wire expansion used by the fixed Robin executable benchmark.

Declaration kind. theorem.

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

Lean code for Theorem6.13.4●1 theorem

theoremdefined in QuantumBlockEncoding/PrimitiveBasisLE.lean

complete

theorem QuantumBlockEncoding.primitiveBasisLEEquiv_six_value
  (bits : QuantumBlockEncoding.PrimitiveBasis 6) :
  ↑((QuantumBlockEncoding.primitiveBasisLEEquiv 6) bits) =
    ↑(bits 0) + 2 * ↑(bits 1) + 4 * ↑(bits 2) + 8 * ↑(bits 3) +
        16 * ↑(bits 4) +
      32 * ↑(bits 5)

theorem QuantumBlockEncoding.primitiveBasisLEEquiv_six_value
  (bits :
    QuantumBlockEncoding.PrimitiveBasis
      6) :
  ↑((QuantumBlockEncoding.primitiveBasisLEEquiv
          6)
        bits) =
    ↑(bits 0) + 2 * ↑(bits 1) +
            4 * ↑(bits 2) +
          8 * ↑(bits 3) +
        16 * ↑(bits 4) +
      32 * ↑(bits 5)

Six-wire expansion used by the fixed Robin executable benchmark.

Definition6.13.5

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “primitive bits 2 le”. Explicit inverse used by finite two-wire state-preparation proofs.

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. Explicit inverse used by finite two-wire state-preparation proofs.

Declaration kind. def.

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

defdefined in QuantumBlockEncoding/PrimitiveBasisLE.lean

complete

def QuantumBlockEncoding.primitiveBits2LE (index : Fin 4) :
  QuantumBlockEncoding.PrimitiveBasis 2

def QuantumBlockEncoding.primitiveBits2LE
  (index : Fin 4) :
  QuantumBlockEncoding.PrimitiveBasis 2

Explicit inverse used by finite two-wire state-preparation proofs.

Theorem6.13.6

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “primitive basis le equiv two symm”; the hypotheses and conclusion in the code panel fix its exact scope.

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

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

Lean code for Theorem6.13.6●1 theorem

theoremdefined in QuantumBlockEncoding/PrimitiveBasisLE.lean

complete

theorem QuantumBlockEncoding.primitiveBasisLEEquiv_two_symm (index : Fin 4) :
  (QuantumBlockEncoding.primitiveBasisLEEquiv 2).symm index =
    QuantumBlockEncoding.primitiveBits2LE index

theorem QuantumBlockEncoding.primitiveBasisLEEquiv_two_symm
  (index : Fin 4) :
  (QuantumBlockEncoding.primitiveBasisLEEquiv
          2).symm
      index =
    QuantumBlockEncoding.primitiveBits2LE
      index

Theorem6.13.7

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “primitive basis le equiv two symm wire zero”; the hypotheses and conclusion in the code panel fix its exact scope. Fixed-width coordinate reductions whose domain exactly matches the 'gridSize'-indexed finite matrix backend.

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

Technical source note. Fixed-width coordinate reductions whose domain exactly matches the 'gridSize'-indexed finite matrix backend.

Declaration kind. theorem.

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

Lean code for Theorem6.13.7●1 theorem

theoremdefined in QuantumBlockEncoding/PrimitiveBasisLE.lean

complete

theorem QuantumBlockEncoding.primitiveBasisLEEquiv_two_symm_wire_zero
  (index : Fin (QuantumBlockEncoding.gridSize 2)) :
  (QuantumBlockEncoding.primitiveBasisLEEquiv 2).symm index 0 =
    ⟨↑index % 2, ⋯⟩

theorem QuantumBlockEncoding.primitiveBasisLEEquiv_two_symm_wire_zero
  (index :
    Fin
      (QuantumBlockEncoding.gridSize 2)) :
  (QuantumBlockEncoding.primitiveBasisLEEquiv
          2).symm
      index 0 =
    ⟨↑index % 2, ⋯⟩

Fixed-width coordinate reductions whose domain exactly matches the
`gridSize`-indexed finite matrix backend.

Theorem6.13.8

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “primitive basis le equiv two symm wire one”; the hypotheses and conclusion in the code panel fix its exact scope.

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

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

Lean code for Theorem6.13.8●1 theorem

theoremdefined in QuantumBlockEncoding/PrimitiveBasisLE.lean

complete

theorem QuantumBlockEncoding.primitiveBasisLEEquiv_two_symm_wire_one
  (index : Fin (QuantumBlockEncoding.gridSize 2)) :
  (QuantumBlockEncoding.primitiveBasisLEEquiv 2).symm index 1 =
    ⟨↑index / 2 % 2, ⋯⟩

theorem QuantumBlockEncoding.primitiveBasisLEEquiv_two_symm_wire_one
  (index :
    Fin
      (QuantumBlockEncoding.gridSize 2)) :
  (QuantumBlockEncoding.primitiveBasisLEEquiv
          2).symm
      index 1 =
    ⟨↑index / 2 % 2, ⋯⟩

Theorem6.13.9

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “primitive basis le equiv two symm 0”; the hypotheses and conclusion in the code panel fix its exact scope. Concrete inverse images used after 'fin_cases'; these avoid relying on type normalization between 'Fin (gridSize 2)' and 'Fin 4'.

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

Technical source note. Concrete inverse images used after 'fin_cases'; these avoid relying on type normalization between 'Fin (gridSize 2)' and 'Fin 4'.

Declaration kind. theorem.

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

theoremdefined in QuantumBlockEncoding/PrimitiveBasisLE.lean

complete

theorem QuantumBlockEncoding.primitiveBasisLEEquiv_two_symm_0 :
  (QuantumBlockEncoding.primitiveBasisLEEquiv 2).symm ⟨0, ⋯⟩ =
    QuantumBlockEncoding.primitiveBits2LE 0

theorem QuantumBlockEncoding.primitiveBasisLEEquiv_two_symm_0 :
  (QuantumBlockEncoding.primitiveBasisLEEquiv
          2).symm
      ⟨0, ⋯⟩ =
    QuantumBlockEncoding.primitiveBits2LE
      0

Concrete inverse images used after `fin_cases`; these avoid relying on type
normalization between `Fin (gridSize 2)` and `Fin 4`.

Theorem6.13.10

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.13.10●1 theorem

theoremdefined in QuantumBlockEncoding/PrimitiveBasisLE.lean

complete

theorem QuantumBlockEncoding.primitiveBasisLEEquiv_two_symm_1 :
  (QuantumBlockEncoding.primitiveBasisLEEquiv 2).symm ⟨1, ⋯⟩ =
    QuantumBlockEncoding.primitiveBits2LE 1

theorem QuantumBlockEncoding.primitiveBasisLEEquiv_two_symm_1 :
  (QuantumBlockEncoding.primitiveBasisLEEquiv
          2).symm
      ⟨1, ⋯⟩ =
    QuantumBlockEncoding.primitiveBits2LE
      1

Theorem6.13.11

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.13.11●1 theorem

theoremdefined in QuantumBlockEncoding/PrimitiveBasisLE.lean

complete

theorem QuantumBlockEncoding.primitiveBasisLEEquiv_two_symm_2 :
  (QuantumBlockEncoding.primitiveBasisLEEquiv 2).symm ⟨2, ⋯⟩ =
    QuantumBlockEncoding.primitiveBits2LE 2

theorem QuantumBlockEncoding.primitiveBasisLEEquiv_two_symm_2 :
  (QuantumBlockEncoding.primitiveBasisLEEquiv
          2).symm
      ⟨2, ⋯⟩ =
    QuantumBlockEncoding.primitiveBits2LE
      2

Theorem6.13.12

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.13.12●1 theorem

theoremdefined in QuantumBlockEncoding/PrimitiveBasisLE.lean

complete

theorem QuantumBlockEncoding.primitiveBasisLEEquiv_two_symm_3 :
  (QuantumBlockEncoding.primitiveBasisLEEquiv 2).symm ⟨3, ⋯⟩ =
    QuantumBlockEncoding.primitiveBits2LE 3

theorem QuantumBlockEncoding.primitiveBasisLEEquiv_two_symm_3 :
  (QuantumBlockEncoding.primitiveBasisLEEquiv
          2).symm
      ⟨3, ⋯⟩ =
    QuantumBlockEncoding.primitiveBits2LE
      3

Definition6.13.13

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “primitive bits 2 le without”. Encode the non-target wire of a two-qubit little-endian basis state.

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. Encode the non-target wire of a two-qubit little-endian basis state.

Declaration kind. def.

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

defdefined in QuantumBlockEncoding/PrimitiveBasisLE.lean

complete

def QuantumBlockEncoding.primitiveBits2LEWithout (target : Fin 2)
  (index : Fin 4) : ℕ

def QuantumBlockEncoding.primitiveBits2LEWithout
  (target : Fin 2) (index : Fin 4) : ℕ

Encode the non-target wire of a two-qubit little-endian basis state.

Definition6.13.14

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “primitive bits 2 le grid without”. Same context code, but with the unreduced 'gridSize' domain used by the concrete matrix semantics.

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. Same context code, but with the unreduced 'gridSize' domain used by the concrete matrix semantics.

Declaration kind. def.

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

Lean code for Definition6.13.14●1 definition

defdefined in QuantumBlockEncoding/PrimitiveBasisLE.lean

complete

def QuantumBlockEncoding.primitiveBits2LEGridWithout (target : Fin 2)
  (index : Fin (QuantumBlockEncoding.gridSize 2)) : ℕ

def QuantumBlockEncoding.primitiveBits2LEGridWithout
  (target : Fin 2)
  (index :
    Fin
      (QuantumBlockEncoding.gridSize 2)) :
  ℕ

Same context code, but with the unreduced `gridSize` domain used by the
concrete matrix semantics.

Theorem6.13.15

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “split primitive wire primitive bits 2 le context 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/PrimitiveBasisLE.lean:103. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.13.15●1 theorem

theoremdefined in QuantumBlockEncoding/PrimitiveBasisLE.lean

complete

theorem QuantumBlockEncoding.splitPrimitiveWire_primitiveBits2LE_context_eq
  (target : Fin 2) (left right : Fin 4) :
  ((QuantumBlockEncoding.splitPrimitiveWire target)
          (QuantumBlockEncoding.primitiveBits2LE left)).2 =
      ((QuantumBlockEncoding.splitPrimitiveWire target)
          (QuantumBlockEncoding.primitiveBits2LE right)).2 ↔
    QuantumBlockEncoding.primitiveBits2LEWithout target left =
      QuantumBlockEncoding.primitiveBits2LEWithout target right

theorem QuantumBlockEncoding.splitPrimitiveWire_primitiveBits2LE_context_eq
  (target : Fin 2) (left right : Fin 4) :
  ((QuantumBlockEncoding.splitPrimitiveWire
            target)
          (QuantumBlockEncoding.primitiveBits2LE
            left)).2 =
      ((QuantumBlockEncoding.splitPrimitiveWire
            target)
          (QuantumBlockEncoding.primitiveBits2LE
            right)).2 ↔
    QuantumBlockEncoding.primitiveBits2LEWithout
        target left =
      QuantumBlockEncoding.primitiveBits2LEWithout
        target right

Theorem6.13.16

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “split primitive wire primitive basis le equiv two symm context 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/PrimitiveBasisLE.lean:111. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.13.16●1 theorem

theoremdefined in QuantumBlockEncoding/PrimitiveBasisLE.lean

complete

theorem QuantumBlockEncoding.splitPrimitiveWire_primitiveBasisLEEquiv_two_symm_context_eq
  (target : Fin 2)
  (left right : Fin (QuantumBlockEncoding.gridSize 2)) :
  ((QuantumBlockEncoding.splitPrimitiveWire target)
          ((QuantumBlockEncoding.primitiveBasisLEEquiv 2).symm
            left)).2 =
      ((QuantumBlockEncoding.splitPrimitiveWire target)
          ((QuantumBlockEncoding.primitiveBasisLEEquiv 2).symm
            right)).2 ↔
    QuantumBlockEncoding.primitiveBits2LEGridWithout target left =
      QuantumBlockEncoding.primitiveBits2LEGridWithout target right

theorem QuantumBlockEncoding.splitPrimitiveWire_primitiveBasisLEEquiv_two_symm_context_eq
  (target : Fin 2)
  (left right :
    Fin
      (QuantumBlockEncoding.gridSize 2)) :
  ((QuantumBlockEncoding.splitPrimitiveWire
            target)
          ((QuantumBlockEncoding.primitiveBasisLEEquiv
                2).symm
            left)).2 =
      ((QuantumBlockEncoding.splitPrimitiveWire
            target)
          ((QuantumBlockEncoding.primitiveBasisLEEquiv
                2).symm
            right)).2 ↔
    QuantumBlockEncoding.primitiveBits2LEGridWithout
        target left =
      QuantumBlockEncoding.primitiveBits2LEGridWithout
        target right

Definition6.13.17

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “primitive bits 3 le”. Explicit inverse used by finite three-wire compiler proofs.

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. Explicit inverse used by finite three-wire compiler proofs.

Declaration kind. def.

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

Lean code for Definition6.13.17●1 definition

defdefined in QuantumBlockEncoding/PrimitiveBasisLE.lean

complete

def QuantumBlockEncoding.primitiveBits3LE (index : Fin 8) :
  QuantumBlockEncoding.PrimitiveBasis 3

def QuantumBlockEncoding.primitiveBits3LE
  (index : Fin 8) :
  QuantumBlockEncoding.PrimitiveBasis 3

Explicit inverse used by finite three-wire compiler proofs.

Theorem6.13.18

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “primitive basis le equiv three symm”; the hypotheses and conclusion in the code panel fix its exact scope.

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

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

Lean code for Theorem6.13.18●1 theorem

theoremdefined in QuantumBlockEncoding/PrimitiveBasisLE.lean

complete

theorem QuantumBlockEncoding.primitiveBasisLEEquiv_three_symm (index : Fin 8) :
  (QuantumBlockEncoding.primitiveBasisLEEquiv 3).symm index =
    QuantumBlockEncoding.primitiveBits3LE index

theorem QuantumBlockEncoding.primitiveBasisLEEquiv_three_symm
  (index : Fin 8) :
  (QuantumBlockEncoding.primitiveBasisLEEquiv
          3).symm
      index =
    QuantumBlockEncoding.primitiveBits3LE
      index

Theorem6.13.19

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “primitive basis le equiv three symm wire zero”; the hypotheses and conclusion in the code panel fix its exact scope.

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

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/PrimitiveBasisLE.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.13.19●1 theorem

theoremdefined in QuantumBlockEncoding/PrimitiveBasisLE.lean

complete

theorem QuantumBlockEncoding.primitiveBasisLEEquiv_three_symm_wire_zero
  (index : Fin (QuantumBlockEncoding.gridSize 3)) :
  (QuantumBlockEncoding.primitiveBasisLEEquiv 3).symm index 0 =
    ⟨↑index % 2, ⋯⟩

theorem QuantumBlockEncoding.primitiveBasisLEEquiv_three_symm_wire_zero
  (index :
    Fin
      (QuantumBlockEncoding.gridSize 3)) :
  (QuantumBlockEncoding.primitiveBasisLEEquiv
          3).symm
      index 0 =
    ⟨↑index % 2, ⋯⟩

Theorem6.13.20

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “primitive basis le equiv three symm wire one”; the hypotheses and conclusion in the code panel fix its exact scope.

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

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/PrimitiveBasisLE.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.13.20●1 theorem

theoremdefined in QuantumBlockEncoding/PrimitiveBasisLE.lean

complete

theorem QuantumBlockEncoding.primitiveBasisLEEquiv_three_symm_wire_one
  (index : Fin (QuantumBlockEncoding.gridSize 3)) :
  (QuantumBlockEncoding.primitiveBasisLEEquiv 3).symm index 1 =
    ⟨↑index / 2 % 2, ⋯⟩

theorem QuantumBlockEncoding.primitiveBasisLEEquiv_three_symm_wire_one
  (index :
    Fin
      (QuantumBlockEncoding.gridSize 3)) :
  (QuantumBlockEncoding.primitiveBasisLEEquiv
          3).symm
      index 1 =
    ⟨↑index / 2 % 2, ⋯⟩

Theorem6.13.21

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “primitive basis le equiv three symm wire two”; 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/PrimitiveBasisLE.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.13.21●1 theorem

theoremdefined in QuantumBlockEncoding/PrimitiveBasisLE.lean

complete

theorem QuantumBlockEncoding.primitiveBasisLEEquiv_three_symm_wire_two
  (index : Fin (QuantumBlockEncoding.gridSize 3)) :
  (QuantumBlockEncoding.primitiveBasisLEEquiv 3).symm index 2 =
    ⟨↑index / 4 % 2, ⋯⟩

theorem QuantumBlockEncoding.primitiveBasisLEEquiv_three_symm_wire_two
  (index :
    Fin
      (QuantumBlockEncoding.gridSize 3)) :
  (QuantumBlockEncoding.primitiveBasisLEEquiv
          3).symm
      index 2 =
    ⟨↑index / 4 % 2, ⋯⟩

Theorem6.13.22

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “primitive basis le equiv three symm 0”; the hypotheses and conclusion in the code panel fix its exact scope. Concrete inverse images for all eight three-qubit basis states.

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

Technical source note. Concrete inverse images for all eight three-qubit basis states.

Declaration kind. theorem.

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

Lean code for Theorem6.13.22●1 theorem

theoremdefined in QuantumBlockEncoding/PrimitiveBasisLE.lean

complete

theorem QuantumBlockEncoding.primitiveBasisLEEquiv_three_symm_0 :
  (QuantumBlockEncoding.primitiveBasisLEEquiv 3).symm ⟨0, ⋯⟩ =
    QuantumBlockEncoding.primitiveBits3LE 0

theorem QuantumBlockEncoding.primitiveBasisLEEquiv_three_symm_0 :
  (QuantumBlockEncoding.primitiveBasisLEEquiv
          3).symm
      ⟨0, ⋯⟩ =
    QuantumBlockEncoding.primitiveBits3LE
      0

Concrete inverse images for all eight three-qubit basis states.

Theorem6.13.23

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.13.23●1 theorem

theoremdefined in QuantumBlockEncoding/PrimitiveBasisLE.lean

complete

theorem QuantumBlockEncoding.primitiveBasisLEEquiv_three_symm_1 :
  (QuantumBlockEncoding.primitiveBasisLEEquiv 3).symm ⟨1, ⋯⟩ =
    QuantumBlockEncoding.primitiveBits3LE 1

theorem QuantumBlockEncoding.primitiveBasisLEEquiv_three_symm_1 :
  (QuantumBlockEncoding.primitiveBasisLEEquiv
          3).symm
      ⟨1, ⋯⟩ =
    QuantumBlockEncoding.primitiveBits3LE
      1

Theorem6.13.24

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.13.24●1 theorem

theoremdefined in QuantumBlockEncoding/PrimitiveBasisLE.lean

complete

theorem QuantumBlockEncoding.primitiveBasisLEEquiv_three_symm_2 :
  (QuantumBlockEncoding.primitiveBasisLEEquiv 3).symm ⟨2, ⋯⟩ =
    QuantumBlockEncoding.primitiveBits3LE 2

theorem QuantumBlockEncoding.primitiveBasisLEEquiv_three_symm_2 :
  (QuantumBlockEncoding.primitiveBasisLEEquiv
          3).symm
      ⟨2, ⋯⟩ =
    QuantumBlockEncoding.primitiveBits3LE
      2

Theorem6.13.25

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.13.25●1 theorem

theoremdefined in QuantumBlockEncoding/PrimitiveBasisLE.lean

complete

theorem QuantumBlockEncoding.primitiveBasisLEEquiv_three_symm_3 :
  (QuantumBlockEncoding.primitiveBasisLEEquiv 3).symm ⟨3, ⋯⟩ =
    QuantumBlockEncoding.primitiveBits3LE 3

theorem QuantumBlockEncoding.primitiveBasisLEEquiv_three_symm_3 :
  (QuantumBlockEncoding.primitiveBasisLEEquiv
          3).symm
      ⟨3, ⋯⟩ =
    QuantumBlockEncoding.primitiveBits3LE
      3

Theorem6.13.26

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.13.26●1 theorem

theoremdefined in QuantumBlockEncoding/PrimitiveBasisLE.lean

complete

theorem QuantumBlockEncoding.primitiveBasisLEEquiv_three_symm_4 :
  (QuantumBlockEncoding.primitiveBasisLEEquiv 3).symm ⟨4, ⋯⟩ =
    QuantumBlockEncoding.primitiveBits3LE 4

theorem QuantumBlockEncoding.primitiveBasisLEEquiv_three_symm_4 :
  (QuantumBlockEncoding.primitiveBasisLEEquiv
          3).symm
      ⟨4, ⋯⟩ =
    QuantumBlockEncoding.primitiveBits3LE
      4

Theorem6.13.27

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “primitive basis le equiv three symm 5”; 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/PrimitiveBasisLE.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.13.27●1 theorem

theoremdefined in QuantumBlockEncoding/PrimitiveBasisLE.lean

complete

theorem QuantumBlockEncoding.primitiveBasisLEEquiv_three_symm_5 :
  (QuantumBlockEncoding.primitiveBasisLEEquiv 3).symm ⟨5, ⋯⟩ =
    QuantumBlockEncoding.primitiveBits3LE 5

theorem QuantumBlockEncoding.primitiveBasisLEEquiv_three_symm_5 :
  (QuantumBlockEncoding.primitiveBasisLEEquiv
          3).symm
      ⟨5, ⋯⟩ =
    QuantumBlockEncoding.primitiveBits3LE
      5

Theorem6.13.28

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.13.28●1 theorem

theoremdefined in QuantumBlockEncoding/PrimitiveBasisLE.lean

complete

theorem QuantumBlockEncoding.primitiveBasisLEEquiv_three_symm_6 :
  (QuantumBlockEncoding.primitiveBasisLEEquiv 3).symm ⟨6, ⋯⟩ =
    QuantumBlockEncoding.primitiveBits3LE 6

theorem QuantumBlockEncoding.primitiveBasisLEEquiv_three_symm_6 :
  (QuantumBlockEncoding.primitiveBasisLEEquiv
          3).symm
      ⟨6, ⋯⟩ =
    QuantumBlockEncoding.primitiveBits3LE
      6

Theorem6.13.29

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.13.29●1 theorem

theoremdefined in QuantumBlockEncoding/PrimitiveBasisLE.lean

complete

theorem QuantumBlockEncoding.primitiveBasisLEEquiv_three_symm_7 :
  (QuantumBlockEncoding.primitiveBasisLEEquiv 3).symm ⟨7, ⋯⟩ =
    QuantumBlockEncoding.primitiveBits3LE 7

theorem QuantumBlockEncoding.primitiveBasisLEEquiv_three_symm_7 :
  (QuantumBlockEncoding.primitiveBasisLEEquiv
          3).symm
      ⟨7, ⋯⟩ =
    QuantumBlockEncoding.primitiveBits3LE
      7

Definition6.13.30

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “primitive bits 3 le without”.

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

Lean code for Definition6.13.30●1 definition

defdefined in QuantumBlockEncoding/PrimitiveBasisLE.lean

complete

def QuantumBlockEncoding.primitiveBits3LEWithout (target : Fin 3)
  (index : Fin 8) : ℕ

def QuantumBlockEncoding.primitiveBits3LEWithout
  (target : Fin 3) (index : Fin 8) : ℕ

Definition6.13.31

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “primitive bits 3 le grid without”. Grid-sized companion of 'primitiveBits3LEWithout', used before the type normalizer has turned 'Fin (gridSize 3)' into 'Fin 8'.

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. Grid-sized companion of 'primitiveBits3LEWithout', used before the type normalizer has turned 'Fin (gridSize 3)' into 'Fin 8'.

Declaration kind. def.

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

Lean code for Definition6.13.31●1 definition

defdefined in QuantumBlockEncoding/PrimitiveBasisLE.lean

complete

def QuantumBlockEncoding.primitiveBits3LEGridWithout (target : Fin 3)
  (index : Fin (QuantumBlockEncoding.gridSize 3)) : ℕ

def QuantumBlockEncoding.primitiveBits3LEGridWithout
  (target : Fin 3)
  (index :
    Fin
      (QuantumBlockEncoding.gridSize 3)) :
  ℕ

Grid-sized companion of `primitiveBits3LEWithout`, used before the type
normalizer has turned `Fin (gridSize 3)` into `Fin 8`.

Theorem6.13.32

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “split primitive wire primitive bits 3 le context 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/PrimitiveBasisLE.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.13.32●1 theorem

theoremdefined in QuantumBlockEncoding/PrimitiveBasisLE.lean

complete

theorem QuantumBlockEncoding.splitPrimitiveWire_primitiveBits3LE_context_eq
  (target : Fin 3) (left right : Fin 8) :
  ((QuantumBlockEncoding.splitPrimitiveWire target)
          (QuantumBlockEncoding.primitiveBits3LE left)).2 =
      ((QuantumBlockEncoding.splitPrimitiveWire target)
          (QuantumBlockEncoding.primitiveBits3LE right)).2 ↔
    QuantumBlockEncoding.primitiveBits3LEWithout target left =
      QuantumBlockEncoding.primitiveBits3LEWithout target right

theorem QuantumBlockEncoding.splitPrimitiveWire_primitiveBits3LE_context_eq
  (target : Fin 3) (left right : Fin 8) :
  ((QuantumBlockEncoding.splitPrimitiveWire
            target)
          (QuantumBlockEncoding.primitiveBits3LE
            left)).2 =
      ((QuantumBlockEncoding.splitPrimitiveWire
            target)
          (QuantumBlockEncoding.primitiveBits3LE
            right)).2 ↔
    QuantumBlockEncoding.primitiveBits3LEWithout
        target left =
      QuantumBlockEncoding.primitiveBits3LEWithout
        target right

Theorem6.13.33

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “split primitive wire primitive basis le equiv three symm context 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/PrimitiveBasisLE.lean:204. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.13.33●1 theorem

theoremdefined in QuantumBlockEncoding/PrimitiveBasisLE.lean

complete

theorem QuantumBlockEncoding.splitPrimitiveWire_primitiveBasisLEEquiv_three_symm_context_eq
  (target : Fin 3)
  (left right : Fin (QuantumBlockEncoding.gridSize 3)) :
  ((QuantumBlockEncoding.splitPrimitiveWire target)
          ((QuantumBlockEncoding.primitiveBasisLEEquiv 3).symm
            left)).2 =
      ((QuantumBlockEncoding.splitPrimitiveWire target)
          ((QuantumBlockEncoding.primitiveBasisLEEquiv 3).symm
            right)).2 ↔
    QuantumBlockEncoding.primitiveBits3LEGridWithout target left =
      QuantumBlockEncoding.primitiveBits3LEGridWithout target right

theorem QuantumBlockEncoding.splitPrimitiveWire_primitiveBasisLEEquiv_three_symm_context_eq
  (target : Fin 3)
  (left right :
    Fin
      (QuantumBlockEncoding.gridSize 3)) :
  ((QuantumBlockEncoding.splitPrimitiveWire
            target)
          ((QuantumBlockEncoding.primitiveBasisLEEquiv
                3).symm
            left)).2 =
      ((QuantumBlockEncoding.splitPrimitiveWire
            target)
          ((QuantumBlockEncoding.primitiveBasisLEEquiv
                3).symm
            right)).2 ↔
    QuantumBlockEncoding.primitiveBits3LEGridWithout
        target left =
      QuantumBlockEncoding.primitiveBits3LEGridWithout
        target right