6.4. QuantumBlockEncoding/PrimitiveBasisLE.lean🔗

8 explicit public declarations, in source order.

Definition6.4.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. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

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

Why it is in this chapter. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

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

Why it is in this chapter. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

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

Why it is in this chapter. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

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.4.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.4.5

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.

Why it is in this chapter. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

Technical source note. Explicit inverse used by finite three-wire compiler 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.4.5●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.4.6

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.

Why it is in this chapter. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

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

Lean code for Theorem6.4.6●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

Definition6.4.7

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.

Why it is in this chapter. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

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

Lean code for Definition6.4.7●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) : ℕ

Theorem6.4.8

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.

Why it is in this chapter. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

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

Lean code for Theorem6.4.8●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