6.1. QuantumBlockEncoding/CircuitSemantics.lean🔗

41 explicit public declarations, in source order.

Definition6.1.1

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “qubit dim”. A finite-dimensional basis size for an 'n'-qubit register.

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. A finite-dimensional basis size for an 'n'-qubit register.

Declaration kind. def.

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

Lean code for Definition6.1.1●1 definition

defdefined in QuantumBlockEncoding/CircuitSemantics.lean

complete

def QuantumBlockEncoding.qubitDim (qubits : ℕ) : ℕ

def QuantumBlockEncoding.qubitDim
  (qubits : ℕ) : ℕ

A finite-dimensional basis size for an `n`-qubit register.

Definition6.1.2

uses 0used by 0✓L∃∀N

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

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

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. Structured semantic obligation for the matrix layer. This mirrors 'GHL2025.ObligationRecord' without importing 'GHL2025', so the semantics backend can stay below paper-specific files in the import graph.

Declaration kind. structure.

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

Lean code for Definition6.1.2●1 definition

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

complete

structure QuantumBlockEncoding.SemanticObligation : Type

structure QuantumBlockEncoding.SemanticObligation :
  Type

Structured semantic obligation for the matrix layer.

This mirrors `GHL2025.ObligationRecord` without importing `GHL2025`, so the
semantics backend can stay below paper-specific files in the import graph.

Fields

description : String

source : String

proved : Bool

Definition6.1.3

uses 0used by 0✓L∃∀N

Plain-English reading. This record groups the data and proof fields needed for “gate matrix”. A proposition-valued field is a requirement until a constructor supplies it. One gate together with its matrix on the full 'qubits'-qubit Hilbert space.

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

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. One gate together with its matrix on the full 'qubits'-qubit Hilbert space. The matrix is supplied by a lower-level certificate for the gate family.

Declaration kind. structure.

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

Lean code for Definition6.1.3●1 definition

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

complete

structure QuantumBlockEncoding.GateMatrix.{u} (α : Type u) (qubits : ℕ) : Type u

structure QuantumBlockEncoding.GateMatrix.{u}
  (α : Type u) (qubits : ℕ) : Type u

One gate together with its matrix on the full `qubits`-qubit Hilbert space.
The matrix is supplied by a lower-level certificate for the gate family.

Fields

gate : QuantumBlockEncoding.Gate

matrix : QuantumBlockEncoding.Matrix (QuantumBlockEncoding.qubitDim qubits) (QuantumBlockEncoding.qubitDim qubits) α

unitary : QuantumBlockEncoding.SemanticObligation

Definition6.1.4

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “gate matrices match circuit”. Check that a list of gate matrices labels exactly the same circuit gates.

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. Check that a list of gate matrices labels exactly the same circuit gates.

Declaration kind. def.

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

Lean code for Definition6.1.4●1 definition

defdefined in QuantumBlockEncoding/CircuitSemantics.lean

complete

def QuantumBlockEncoding.gateMatricesMatchCircuit.{u} {α : Type u}
  {qubits : ℕ} :
  QuantumBlockEncoding.Circuit →
    List (QuantumBlockEncoding.GateMatrix α qubits) → Bool

def QuantumBlockEncoding.gateMatricesMatchCircuit.{u}
  {α : Type u} {qubits : ℕ} :
  QuantumBlockEncoding.Circuit →
    List
        (QuantumBlockEncoding.GateMatrix α
          qubits) →
      Bool

Check that a list of gate matrices labels exactly the same circuit gates.

Definition6.1.5

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “eval gate matrices”. Evaluate a list of full-space gate matrices to a circuit matrix.

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. Evaluate a list of full-space gate matrices to a circuit matrix. The fold uses the usual right-action convention for a circuit list '[g₁, g₂, ...]': the resulting matrix is 'g_k * ... * g₂ * g₁'.

Declaration kind. def.

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

Lean code for Definition6.1.5●1 definition

defdefined in QuantumBlockEncoding/CircuitSemantics.lean

complete

def QuantumBlockEncoding.evalGateMatrices.{u} {α : Type u} [OfNat α 0]
  [OfNat α 1] [HAdd α α α] [HMul α α α] {qubits : ℕ}
  (gates : List (QuantumBlockEncoding.GateMatrix α qubits)) :
  QuantumBlockEncoding.Matrix (QuantumBlockEncoding.qubitDim qubits)
    (QuantumBlockEncoding.qubitDim qubits) α

def QuantumBlockEncoding.evalGateMatrices.{u}
  {α : Type u} [OfNat α 0] [OfNat α 1]
  [HAdd α α α] [HMul α α α] {qubits : ℕ}
  (gates :
    List
      (QuantumBlockEncoding.GateMatrix α
        qubits)) :
  QuantumBlockEncoding.Matrix
    (QuantumBlockEncoding.qubitDim qubits)
    (QuantumBlockEncoding.qubitDim qubits)
    α

Evaluate a list of full-space gate matrices to a circuit matrix.

The fold uses the usual right-action convention for a circuit list
`[g₁, g₂, ...]`: the resulting matrix is `g_k * ... * g₂ * g₁`.

Theorem6.1.6

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “eval with foldl add mul”; the hypotheses and conclusion in the code panel fix its exact scope. Evaluate one symbolic matrix-product entry as a concrete finite Rat fold.

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. Evaluate one symbolic matrix-product entry as a concrete finite Rat fold. The project-local 'Coeff' matrices are syntactic, so a raw 'Matrix.mul' entry does not simplify away zero summands. This lemma moves the finite product entry through 'Coeff.evalWith', where later path-isolation proofs can use ordinary rational arithmetic without expanding the whole symbolic expression.

Declaration kind. theorem.

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

Lean code for Theorem6.1.6●1 theorem

theoremdefined in QuantumBlockEncoding/CircuitSemantics.lean

complete

theorem QuantumBlockEncoding.Matrix.evalWith_foldl_add_mul (env : String → ℚ)
  {rows mid cols : ℕ}
  (A : QuantumBlockEncoding.Matrix rows mid QuantumBlockEncoding.Coeff)
  (B : QuantumBlockEncoding.Matrix mid cols QuantumBlockEncoding.Coeff)
  (i : Fin rows) (j : Fin cols) (ks : List (Fin mid))
  (acc : QuantumBlockEncoding.Coeff) :
  QuantumBlockEncoding.Coeff.evalWith env
      (List.foldl (fun acc k => acc + A i k * B k j) acc ks) =
    List.foldl
      (fun acc k =>
        acc +
          QuantumBlockEncoding.Coeff.evalWith env (A i k) *
            QuantumBlockEncoding.Coeff.evalWith env (B k j))
      (QuantumBlockEncoding.Coeff.evalWith env acc) ks

theorem QuantumBlockEncoding.Matrix.evalWith_foldl_add_mul
  (env : String → ℚ) {rows mid cols : ℕ}
  (A :
    QuantumBlockEncoding.Matrix rows mid
      QuantumBlockEncoding.Coeff)
  (B :
    QuantumBlockEncoding.Matrix mid cols
      QuantumBlockEncoding.Coeff)
  (i : Fin rows) (j : Fin cols)
  (ks : List (Fin mid))
  (acc : QuantumBlockEncoding.Coeff) :
  QuantumBlockEncoding.Coeff.evalWith env
      (List.foldl
        (fun acc k => acc + A i k * B k j)
        acc ks) =
    List.foldl
      (fun acc k =>
        acc +
          QuantumBlockEncoding.Coeff.evalWith
              env (A i k) *
            QuantumBlockEncoding.Coeff.evalWith
              env (B k j))
      (QuantumBlockEncoding.Coeff.evalWith
        env acc)
      ks

Evaluate one symbolic matrix-product entry as a concrete finite Rat fold.

The project-local `Coeff` matrices are syntactic, so a raw `Matrix.mul` entry
does not simplify away zero summands.  This lemma moves the finite product
entry through `Coeff.evalWith`, where later path-isolation proofs can use
ordinary rational arithmetic without expanding the whole symbolic expression.

Theorem6.1.7

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “eval with mul apply”; the hypotheses and conclusion in the code panel fix its exact scope. Evaluate one entry of 'Matrix.mul' by evaluating each path contribution.

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. Evaluate one entry of 'Matrix.mul' by evaluating each path contribution. This is the local matrix-semantics block needed before a focused Robin seven-gate path proof can avoid syntactic 'Coeff.add' blow-up.

Declaration kind. theorem.

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

Lean code for Theorem6.1.7●1 theorem

theoremdefined in QuantumBlockEncoding/CircuitSemantics.lean

complete

theorem QuantumBlockEncoding.Matrix.evalWith_mul_apply (env : String → ℚ)
  {rows mid cols : ℕ}
  (A : QuantumBlockEncoding.Matrix rows mid QuantumBlockEncoding.Coeff)
  (B : QuantumBlockEncoding.Matrix mid cols QuantumBlockEncoding.Coeff)
  (i : Fin rows) (j : Fin cols) :
  QuantumBlockEncoding.Coeff.evalWith env (A.mul B i j) =
    List.foldl
      (fun acc k =>
        acc +
          QuantumBlockEncoding.Coeff.evalWith env (A i k) *
            QuantumBlockEncoding.Coeff.evalWith env (B k j))
      0 (List.finRange mid)

theorem QuantumBlockEncoding.Matrix.evalWith_mul_apply
  (env : String → ℚ) {rows mid cols : ℕ}
  (A :
    QuantumBlockEncoding.Matrix rows mid
      QuantumBlockEncoding.Coeff)
  (B :
    QuantumBlockEncoding.Matrix mid cols
      QuantumBlockEncoding.Coeff)
  (i : Fin rows) (j : Fin cols) :
  QuantumBlockEncoding.Coeff.evalWith env
      (A.mul B i j) =
    List.foldl
      (fun acc k =>
        acc +
          QuantumBlockEncoding.Coeff.evalWith
              env (A i k) *
            QuantumBlockEncoding.Coeff.evalWith
              env (B k j))
      0 (List.finRange mid)

Evaluate one entry of `Matrix.mul` by evaluating each path contribution.

This is the local matrix-semantics block needed before a focused Robin
seven-gate path proof can avoid syntactic `Coeff.add` blow-up.

Theorem6.1.8

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “eval with mul eq zero of all paths zero”; the hypotheses and conclusion in the code panel fix its exact scope. Evaluate one matrix-product entry as zero when every evaluated path contribution is zero.

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. Evaluate one matrix-product entry as zero when every evaluated path contribution is zero. This is the zero-support companion to 'evalWith_mul_unique_path'. It lets paper-specific product proofs avoid expanding a large symbolic 'Coeff' fold when they have already isolated gate-local support facts.

Declaration kind. theorem.

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

Lean code for Theorem6.1.8●1 theorem

theoremdefined in QuantumBlockEncoding/CircuitSemantics.lean

complete

theorem QuantumBlockEncoding.Matrix.evalWith_mul_eq_zero_of_all_paths_zero
  (env : String → ℚ) {rows mid cols : ℕ}
  (A : QuantumBlockEncoding.Matrix rows mid QuantumBlockEncoding.Coeff)
  (B : QuantumBlockEncoding.Matrix mid cols QuantumBlockEncoding.Coeff)
  (i : Fin rows) (j : Fin cols)
  (hzero :
    ∀ (k : Fin mid),
      QuantumBlockEncoding.Coeff.evalWith env (A i k) *
          QuantumBlockEncoding.Coeff.evalWith env (B k j) =
        0) :
  QuantumBlockEncoding.Coeff.evalWith env (A.mul B i j) = 0

theorem QuantumBlockEncoding.Matrix.evalWith_mul_eq_zero_of_all_paths_zero
  (env : String → ℚ) {rows mid cols : ℕ}
  (A :
    QuantumBlockEncoding.Matrix rows mid
      QuantumBlockEncoding.Coeff)
  (B :
    QuantumBlockEncoding.Matrix mid cols
      QuantumBlockEncoding.Coeff)
  (i : Fin rows) (j : Fin cols)
  (hzero :
    ∀ (k : Fin mid),
      QuantumBlockEncoding.Coeff.evalWith
            env (A i k) *
          QuantumBlockEncoding.Coeff.evalWith
            env (B k j) =
        0) :
  QuantumBlockEncoding.Coeff.evalWith env
      (A.mul B i j) =
    0

Evaluate one matrix-product entry as zero when every evaluated path contribution
is zero.

This is the zero-support companion to `evalWith_mul_unique_path`.  It lets
paper-specific product proofs avoid expanding a large symbolic `Coeff` fold
when they have already isolated gate-local support facts.

Theorem6.1.9

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “eval with mul unique path”; the hypotheses and conclusion in the code panel fix its exact scope. Evaluate one matrix-product entry when all evaluated paths except 'k0' vanish.

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. Evaluate one matrix-product entry when all evaluated paths except 'k0' vanish. This is the reusable path-isolation block for later Robin gamma3 work: a theorem about the seven-gate product can first prove zero-support facts for all unwanted intermediate states, then reduce the evaluated product to the single surviving contribution.

Declaration kind. theorem.

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

Lean code for Theorem6.1.9●1 theorem

theoremdefined in QuantumBlockEncoding/CircuitSemantics.lean

complete

theorem QuantumBlockEncoding.Matrix.evalWith_mul_unique_path (env : String → ℚ)
  {rows mid cols : ℕ}
  (A : QuantumBlockEncoding.Matrix rows mid QuantumBlockEncoding.Coeff)
  (B : QuantumBlockEncoding.Matrix mid cols QuantumBlockEncoding.Coeff)
  (i : Fin rows) (j : Fin cols) (k0 : Fin mid)
  (hzero :
    ∀ (k : Fin mid),
      k ≠ k0 →
        QuantumBlockEncoding.Coeff.evalWith env (A i k) *
            QuantumBlockEncoding.Coeff.evalWith env (B k j) =
          0) :
  QuantumBlockEncoding.Coeff.evalWith env (A.mul B i j) =
    QuantumBlockEncoding.Coeff.evalWith env (A i k0) *
      QuantumBlockEncoding.Coeff.evalWith env (B k0 j)

theorem QuantumBlockEncoding.Matrix.evalWith_mul_unique_path
  (env : String → ℚ) {rows mid cols : ℕ}
  (A :
    QuantumBlockEncoding.Matrix rows mid
      QuantumBlockEncoding.Coeff)
  (B :
    QuantumBlockEncoding.Matrix mid cols
      QuantumBlockEncoding.Coeff)
  (i : Fin rows) (j : Fin cols)
  (k0 : Fin mid)
  (hzero :
    ∀ (k : Fin mid),
      k ≠ k0 →
        QuantumBlockEncoding.Coeff.evalWith
              env (A i k) *
            QuantumBlockEncoding.Coeff.evalWith
              env (B k j) =
          0) :
  QuantumBlockEncoding.Coeff.evalWith env
      (A.mul B i j) =
    QuantumBlockEncoding.Coeff.evalWith
        env (A i k0) *
      QuantumBlockEncoding.Coeff.evalWith
        env (B k0 j)

Evaluate one matrix-product entry when all evaluated paths except `k0` vanish.

This is the reusable path-isolation block for later Robin gamma3 work: a
theorem about the seven-gate product can first prove zero-support facts for all
unwanted intermediate states, then reduce the evaluated product to the single
surviving contribution.

Theorem6.1.10

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “eval with mul two path”; the hypotheses and conclusion in the code panel fix its exact scope. Evaluate one matrix-product entry when all evaluated paths except 'k0' and 'k1' vanish.

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. Evaluate one matrix-product entry when all evaluated paths except 'k0' and 'k1' vanish. This is the two-path companion to 'evalWith_mul_unique_path'. A seven-gate product proof can first establish that only two intermediate rows contribute, then reduce the evaluated product to their sum using this theorem.

Declaration kind. theorem.

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

Lean code for Theorem6.1.10●1 theorem

theoremdefined in QuantumBlockEncoding/CircuitSemantics.lean

complete

theorem QuantumBlockEncoding.Matrix.evalWith_mul_two_path (env : String → ℚ)
  {rows mid cols : ℕ}
  (A : QuantumBlockEncoding.Matrix rows mid QuantumBlockEncoding.Coeff)
  (B : QuantumBlockEncoding.Matrix mid cols QuantumBlockEncoding.Coeff)
  (i : Fin rows) (j : Fin cols) (k0 k1 : Fin mid) (hk0_ne_k1 : k0 ≠ k1)
  (hzero :
    ∀ (k : Fin mid),
      k ≠ k0 →
        k ≠ k1 →
          QuantumBlockEncoding.Coeff.evalWith env (A i k) *
              QuantumBlockEncoding.Coeff.evalWith env (B k j) =
            0) :
  QuantumBlockEncoding.Coeff.evalWith env (A.mul B i j) =
    QuantumBlockEncoding.Coeff.evalWith env (A i k0) *
        QuantumBlockEncoding.Coeff.evalWith env (B k0 j) +
      QuantumBlockEncoding.Coeff.evalWith env (A i k1) *
        QuantumBlockEncoding.Coeff.evalWith env (B k1 j)

theorem QuantumBlockEncoding.Matrix.evalWith_mul_two_path
  (env : String → ℚ) {rows mid cols : ℕ}
  (A :
    QuantumBlockEncoding.Matrix rows mid
      QuantumBlockEncoding.Coeff)
  (B :
    QuantumBlockEncoding.Matrix mid cols
      QuantumBlockEncoding.Coeff)
  (i : Fin rows) (j : Fin cols)
  (k0 k1 : Fin mid) (hk0_ne_k1 : k0 ≠ k1)
  (hzero :
    ∀ (k : Fin mid),
      k ≠ k0 →
        k ≠ k1 →
          QuantumBlockEncoding.Coeff.evalWith
                env (A i k) *
              QuantumBlockEncoding.Coeff.evalWith
                env (B k j) =
            0) :
  QuantumBlockEncoding.Coeff.evalWith env
      (A.mul B i j) =
    QuantumBlockEncoding.Coeff.evalWith
          env (A i k0) *
        QuantumBlockEncoding.Coeff.evalWith
          env (B k0 j) +
      QuantumBlockEncoding.Coeff.evalWith
          env (A i k1) *
        QuantumBlockEncoding.Coeff.evalWith
          env (B k1 j)

Evaluate one matrix-product entry when all evaluated paths except `k0` and `k1`
vanish.

This is the two-path companion to `evalWith_mul_unique_path`.  A seven-gate
product proof can first establish that only two intermediate rows contribute,
then reduce the evaluated product to their sum using this theorem.

Theorem6.1.11

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “eval with mul identity right apply”; the hypotheses and conclusion in the code panel fix its exact scope. Evaluating a symbolic matrix after multiplying on the right by the identity recovers the evaluated entry.

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. Evaluating a symbolic matrix after multiplying on the right by the identity recovers the evaluated entry. The statement is evaluation-level, not syntactic: 'Coeff' deliberately stores matrix products as explicit fold expressions, so the raw 'Coeff' term still contains zero summands.

Declaration kind. theorem.

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

Lean code for Theorem6.1.11●1 theorem

theoremdefined in QuantumBlockEncoding/CircuitSemantics.lean

complete

theorem QuantumBlockEncoding.Matrix.evalWith_mul_identity_right_apply
  (env : String → ℚ) {n : ℕ}
  (A : QuantumBlockEncoding.Matrix n n QuantumBlockEncoding.Coeff)
  (i j : Fin n) :
  QuantumBlockEncoding.Coeff.evalWith env
      (A.mul
        (QuantumBlockEncoding.Matrix.identity n
          QuantumBlockEncoding.Coeff)
        i j) =
    QuantumBlockEncoding.Coeff.evalWith env (A i j)

theorem QuantumBlockEncoding.Matrix.evalWith_mul_identity_right_apply
  (env : String → ℚ) {n : ℕ}
  (A :
    QuantumBlockEncoding.Matrix n n
      QuantumBlockEncoding.Coeff)
  (i j : Fin n) :
  QuantumBlockEncoding.Coeff.evalWith env
      (A.mul
        (QuantumBlockEncoding.Matrix.identity
          n QuantumBlockEncoding.Coeff)
        i j) =
    QuantumBlockEncoding.Coeff.evalWith
      env (A i j)

Evaluating a symbolic matrix after multiplying on the right by the identity
recovers the evaluated entry.

The statement is evaluation-level, not syntactic: `Coeff` deliberately stores
matrix products as explicit fold expressions, so the raw `Coeff` term still
contains zero summands.

Theorem6.1.12

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “cast square apply”; the hypotheses and conclusion in the code panel fix its exact scope. Entry-level bridge for square matrix casts along a dimension equality.

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. Entry-level bridge for square matrix casts along a dimension equality. This keeps paper-specific finite-entry proofs from unfolding a large casted matrix when the only content is that the row and column values are unchanged.

Declaration kind. theorem.

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

Lean code for Theorem6.1.12●1 theorem

theoremdefined in QuantumBlockEncoding/CircuitSemantics.lean

complete

theorem QuantumBlockEncoding.Matrix.cast_square_apply.{u} {α : Type u} {m n : ℕ}
  (h : m = n) (M : QuantumBlockEncoding.Matrix m m α) (i j : Fin n) :
  cast ⋯ M i j = M ⟨↑i, ⋯⟩ ⟨↑j, ⋯⟩

theorem QuantumBlockEncoding.Matrix.cast_square_apply.{u}
  {α : Type u} {m n : ℕ} (h : m = n)
  (M : QuantumBlockEncoding.Matrix m m α)
  (i j : Fin n) :
  cast ⋯ M i j = M ⟨↑i, ⋯⟩ ⟨↑j, ⋯⟩

Entry-level bridge for square matrix casts along a dimension equality.

This keeps paper-specific finite-entry proofs from unfolding a large casted
matrix when the only content is that the row and column values are unchanged.

Theorem6.1.13

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “eval with eval gate matrices single”; the hypotheses and conclusion in the code panel fix its exact scope. Evaluation-level single-gate reduction for 'evalGateMatrices'.

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. Evaluation-level single-gate reduction for 'evalGateMatrices'. This is the entry helper for prepared composite gates: the matrix semantics of a singleton gate list evaluates to the supplied gate matrix entry, even though the underlying symbolic 'Coeff' expression is still a folded multiplication by the identity matrix.

Declaration kind. theorem.

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

Lean code for Theorem6.1.13●1 theorem

theoremdefined in QuantumBlockEncoding/CircuitSemantics.lean

complete

theorem QuantumBlockEncoding.evalWith_evalGateMatrices_single (env : String → ℚ)
  {qubits : ℕ}
  (gateMatrix :
    QuantumBlockEncoding.GateMatrix QuantumBlockEncoding.Coeff qubits)
  (i j : Fin (QuantumBlockEncoding.qubitDim qubits)) :
  QuantumBlockEncoding.Coeff.evalWith env
      (QuantumBlockEncoding.evalGateMatrices [gateMatrix] i j) =
    QuantumBlockEncoding.Coeff.evalWith env (gateMatrix.matrix i j)

theorem QuantumBlockEncoding.evalWith_evalGateMatrices_single
  (env : String → ℚ) {qubits : ℕ}
  (gateMatrix :
    QuantumBlockEncoding.GateMatrix
      QuantumBlockEncoding.Coeff qubits)
  (i j :
    Fin
      (QuantumBlockEncoding.qubitDim
        qubits)) :
  QuantumBlockEncoding.Coeff.evalWith env
      (QuantumBlockEncoding.evalGateMatrices
        [gateMatrix] i j) =
    QuantumBlockEncoding.Coeff.evalWith
      env (gateMatrix.matrix i j)

Evaluation-level single-gate reduction for `evalGateMatrices`.

This is the entry helper for prepared composite gates: the matrix semantics of
a singleton gate list evaluates to the supplied gate matrix entry, even though
the underlying symbolic `Coeff` expression is still a folded multiplication by
the identity matrix.

Definition6.1.14

uses 0used by 0✓L∃∀N

Plain-English reading. This record groups the data and proof fields needed for “circuit matrix semantics”. A proposition-valued field is a requirement until a constructor supplies it. Circuit-level matrix semantics assembled from gate-level matrices.

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

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. Circuit-level matrix semantics assembled from gate-level matrices. This does not certify that individual oracle matrices are correct; it gives the project a stable Lean target for composing those certificates once they exist.

Declaration kind. structure.

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

Lean code for Definition6.1.14●1 definition

structure(5 fields)defined in QuantumBlockEncoding/CircuitSemantics.lean

complete

structure QuantumBlockEncoding.CircuitMatrixSemantics.{u} (α : Type u) [OfNat α 0]
  [OfNat α 1] [HAdd α α α] [HMul α α α] (qubits : ℕ) : Type u

structure QuantumBlockEncoding.CircuitMatrixSemantics.{u}
  (α : Type u) [OfNat α 0] [OfNat α 1]
  [HAdd α α α] [HMul α α α] (qubits : ℕ) :
  Type u

Circuit-level matrix semantics assembled from gate-level matrices.

This does not certify that individual oracle matrices are correct; it gives the
project a stable Lean target for composing those certificates once they exist.

Fields

circuit : QuantumBlockEncoding.Circuit

gateMatrices : List (QuantumBlockEncoding.GateMatrix α qubits)

gateListMatches : QuantumBlockEncoding.gateMatricesMatchCircuit self.circuit self.gateMatrices = true

matrix : QuantumBlockEncoding.Matrix (QuantumBlockEncoding.qubitDim qubits) (QuantumBlockEncoding.qubitDim qubits) α

matrix_eq_eval : self.matrix.PointwiseEq (QuantumBlockEncoding.evalGateMatrices self.gateMatrices)

Definition6.1.15

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “of gate matrices”. Build circuit semantics directly from aligned gate matrices.

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. Build circuit semantics directly from aligned gate matrices.

Declaration kind. def.

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

Lean code for Definition6.1.15●1 definition

defdefined in QuantumBlockEncoding/CircuitSemantics.lean

complete

def QuantumBlockEncoding.CircuitMatrixSemantics.ofGateMatrices.{u}
  {α : Type u} [OfNat α 0] [OfNat α 1] [HAdd α α α] [HMul α α α]
  {qubits : ℕ} (circuit : QuantumBlockEncoding.Circuit)
  (gateMatrices : List (QuantumBlockEncoding.GateMatrix α qubits))
  (h :
    QuantumBlockEncoding.gateMatricesMatchCircuit circuit gateMatrices =
      true) :
  QuantumBlockEncoding.CircuitMatrixSemantics α qubits

def QuantumBlockEncoding.CircuitMatrixSemantics.ofGateMatrices.{u}
  {α : Type u} [OfNat α 0] [OfNat α 1]
  [HAdd α α α] [HMul α α α] {qubits : ℕ}
  (circuit : QuantumBlockEncoding.Circuit)
  (gateMatrices :
    List
      (QuantumBlockEncoding.GateMatrix α
        qubits))
  (h :
    QuantumBlockEncoding.gateMatricesMatchCircuit
        circuit gateMatrices =
      true) :
  QuantumBlockEncoding.CircuitMatrixSemantics
    α qubits

Build circuit semantics directly from aligned gate matrices.

Definition6.1.16

uses 0used by 0✓L∃∀N

Plain-English reading. This record groups the data and proof fields needed for “prepared circuit entry target”. A proposition-valued field is a requirement until a constructor supplies it. Typed target for relating an active circuit-matrix entry to a prepared composition entry.

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

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. Typed target for relating an active circuit-matrix entry to a prepared composition entry. This is intentionally only an interface. It records the two matrix entries and the exact equality a paper-specific composition backend must prove; it does not assert that the active circuit already contains the prepared blocks.

Declaration kind. structure.

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

Lean code for Definition6.1.16●1 definition

structure(12 fields)defined in QuantumBlockEncoding/CircuitSemantics.lean

complete

structure QuantumBlockEncoding.PreparedCircuitEntryTarget.{u} (α : Type u)
  (activeDim preparedDim : ℕ) : Type u

structure QuantumBlockEncoding.PreparedCircuitEntryTarget.{u}
  (α : Type u)
  (activeDim preparedDim : ℕ) : Type u

Typed target for relating an active circuit-matrix entry to a prepared
composition entry.

This is intentionally only an interface.  It records the two matrix entries
and the exact equality a paper-specific composition backend must prove; it
does not assert that the active circuit already contains the prepared blocks.

Fields

activeMatrix : QuantumBlockEncoding.Matrix activeDim activeDim α

preparedMatrix : QuantumBlockEncoding.Matrix preparedDim preparedDim α

activeRow : Fin activeDim

activeCol : Fin activeDim

preparedRow : Fin preparedDim

preparedCol : Fin preparedDim

activeEntry : α

activeEntry_eq : self.activeEntry = self.activeMatrix self.activeRow self.activeCol

preparedEntry : α

preparedEntry_eq : self.preparedEntry = self.preparedMatrix self.preparedRow self.preparedCol

activeSource : QuantumBlockEncoding.SemanticObligation

preparedComposition : QuantumBlockEncoding.SemanticObligation

Definition6.1.17

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “entry equality statement”. The prepared-composition equality required by the target.

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 prepared-composition equality required by the target.

Declaration kind. def.

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

Lean code for Definition6.1.17●1 definition

defdefined in QuantumBlockEncoding/CircuitSemantics.lean

complete

def QuantumBlockEncoding.PreparedCircuitEntryTarget.entryEqualityStatement.{u}
  {α : Type u} {activeDim preparedDim : ℕ}
  (target :
    QuantumBlockEncoding.PreparedCircuitEntryTarget α activeDim
      preparedDim) :
  Prop

def QuantumBlockEncoding.PreparedCircuitEntryTarget.entryEqualityStatement.{u}
  {α : Type u} {activeDim preparedDim : ℕ}
  (target :
    QuantumBlockEncoding.PreparedCircuitEntryTarget
      α activeDim preparedDim) :
  Prop

The prepared-composition equality required by the target.

Definition6.1.18

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “matrix entry equality statement”. The same equality stated directly on the backing matrices.

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 same equality stated directly on the backing matrices.

Declaration kind. def.

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

Lean code for Definition6.1.18●1 definition

defdefined in QuantumBlockEncoding/CircuitSemantics.lean

complete

def QuantumBlockEncoding.PreparedCircuitEntryTarget.matrixEntryEqualityStatement.{u}
  {α : Type u} {activeDim preparedDim : ℕ}
  (target :
    QuantumBlockEncoding.PreparedCircuitEntryTarget α activeDim
      preparedDim) :
  Prop

def QuantumBlockEncoding.PreparedCircuitEntryTarget.matrixEntryEqualityStatement.{u}
  {α : Type u} {activeDim preparedDim : ℕ}
  (target :
    QuantumBlockEncoding.PreparedCircuitEntryTarget
      α activeDim preparedDim) :
  Prop

The same equality stated directly on the backing matrices.

Theorem6.1.19

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “entry equality statement iff matrix entry equality statement”; the hypotheses and conclusion in the code panel fix its exact scope. The cached entry equality is equivalent to the backing matrix-entry equality.

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 cached entry equality is equivalent to the backing matrix-entry equality. Paper-specific targets can prove whichever side their local backend exposes without changing the semantic obligation being tracked.

Declaration kind. theorem.

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

Lean code for Theorem6.1.19●1 theorem

theoremdefined in QuantumBlockEncoding/CircuitSemantics.lean

complete

theorem QuantumBlockEncoding.PreparedCircuitEntryTarget.entryEqualityStatement_iff_matrixEntryEqualityStatement.{u}
  {α : Type u} {activeDim preparedDim : ℕ}
  (target :
    QuantumBlockEncoding.PreparedCircuitEntryTarget α activeDim
      preparedDim) :
  target.entryEqualityStatement ↔ target.matrixEntryEqualityStatement

theorem QuantumBlockEncoding.PreparedCircuitEntryTarget.entryEqualityStatement_iff_matrixEntryEqualityStatement.{u}
  {α : Type u} {activeDim preparedDim : ℕ}
  (target :
    QuantumBlockEncoding.PreparedCircuitEntryTarget
      α activeDim preparedDim) :
  target.entryEqualityStatement ↔
    target.matrixEntryEqualityStatement

The cached entry equality is equivalent to the backing matrix-entry equality.

Paper-specific targets can prove whichever side their local backend exposes
without changing the semantic obligation being tracked.

Definition6.1.20

uses 0used by 0✓L∃∀N

Plain-English reading. This record groups the data and proof fields needed for “block extraction target”. A proposition-valued field is a requirement until a constructor supplies it. A paper-level block-extraction target against a concrete circuit matrix.

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

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. A paper-level block-extraction target against a concrete circuit matrix. The current project can now state the missing equation in matrix terms. The actual block projection from signal/system registers remains a later proof obligation, tracked explicitly by 'blockProjection' and 'blockCorrect'.

Declaration kind. structure.

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

Lean code for Definition6.1.20●1 definition

structure(7 fields)defined in QuantumBlockEncoding/CircuitSemantics.lean

complete

structure QuantumBlockEncoding.BlockExtractionTarget.{u} (α : Type u) [OfNat α 0]
  [OfNat α 1] [HAdd α α α] [HMul α α α] (rows cols signalDim : ℕ) :
  Type u

structure QuantumBlockEncoding.BlockExtractionTarget.{u}
  (α : Type u) [OfNat α 0] [OfNat α 1]
  [HAdd α α α] [HMul α α α]
  (rows cols signalDim : ℕ) : Type u

A paper-level block-extraction target against a concrete circuit matrix.

The current project can now state the missing equation in matrix terms.  The
actual block projection from signal/system registers remains a later proof
obligation, tracked explicitly by `blockProjection` and `blockCorrect`.

Fields

unitaryMatrix : QuantumBlockEncoding.Matrix (signalDim * rows) (signalDim * cols) α

targetMatrix : QuantumBlockEncoding.Matrix rows cols α

normalizer : α

signalIndex : Fin signalDim

blockMatrix : QuantumBlockEncoding.Matrix rows cols α

blockProjection : QuantumBlockEncoding.SemanticObligation

blockCorrect : QuantumBlockEncoding.SemanticObligation

Definition6.1.21

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “block extraction branch contribution sum”. Fold a finite family of branch contributions into one projected block entry.

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. Fold a finite family of branch contributions into one projected block entry. This is deliberately minimal: it provides a typed target for paper-specific projection/summation proofs without assuming commutativity, a ring structure, or a normal form for symbolic coefficients.

Declaration kind. def.

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

Lean code for Definition6.1.21●1 definition

defdefined in QuantumBlockEncoding/CircuitSemantics.lean

complete

def QuantumBlockEncoding.blockExtractionBranchContributionSum.{u}
  {α : Type u} [OfNat α 0] [HAdd α α α] {branchDim : ℕ}
  (branchContribution : Fin branchDim → α) : α

def QuantumBlockEncoding.blockExtractionBranchContributionSum.{u}
  {α : Type u} [OfNat α 0] [HAdd α α α]
  {branchDim : ℕ}
  (branchContribution :
    Fin branchDim → α) :
  α

Fold a finite family of branch contributions into one projected block entry.

This is deliberately minimal: it provides a typed target for paper-specific
projection/summation proofs without assuming commutativity, a ring structure,
or a normal form for symbolic coefficients.

Definition6.1.22

uses 0used by 0✓L∃∀N

Plain-English reading. This record groups the data and proof fields needed for “block extraction branch contribution target”. A proposition-valued field is a requirement until a constructor supplies it. Typed interface for decomposing one block-extracted matrix entry into finite branch contributions.

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

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. Typed interface for decomposing one block-extracted matrix entry into finite branch contributions. The interface records the candidate contribution family and the exact block-entry and branch-sum propositions that must be proved. It is not itself a proof that the family is sourced from the backend or that the branch sum equals the block entry; those remain explicit semantic obligations.

Declaration kind. structure.

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

Lean code for Definition6.1.22●1 definition

structure(14 fields)defined in QuantumBlockEncoding/CircuitSemantics.lean

complete

structure QuantumBlockEncoding.BlockExtractionBranchContributionTarget.{u}
  (α : Type u) [OfNat α 0] [OfNat α 1] [HAdd α α α] [HMul α α α]
  (rows cols signalDim branchDim : ℕ) : Type u

structure QuantumBlockEncoding.BlockExtractionBranchContributionTarget.{u}
  (α : Type u) [OfNat α 0] [OfNat α 1]
  [HAdd α α α] [HMul α α α]
  (rows cols signalDim branchDim : ℕ) :
  Type u

Typed interface for decomposing one block-extracted matrix entry into finite
branch contributions.

The interface records the candidate contribution family and the exact
block-entry and branch-sum propositions that must be proved.  It is not itself
a proof that the family is sourced from the backend or that the branch sum
equals the block entry; those remain explicit semantic obligations.

Fields

extractionTarget : QuantumBlockEncoding.BlockExtractionTarget α rows cols signalDim

systemRow : Fin rows

systemCol : Fin cols

selectedBranch : Fin branchDim

branchContribution : Fin branchDim → α

selectedContribution : α

selectedContribution_eq : self.selectedContribution = self.branchContribution self.selectedBranch

branchSum : α

branchSum_eq : self.branchSum = QuantumBlockEncoding.blockExtractionBranchContributionSum self.branchContribution

blockEntry : α

blockEntry_eq : self.blockEntry = self.extractionTarget.blockMatrix self.systemRow self.systemCol

backendSource : QuantumBlockEncoding.SemanticObligation

selectedBranchCorrect : QuantumBlockEncoding.SemanticObligation

branchSummationCorrect : QuantumBlockEncoding.SemanticObligation

Definition6.1.23

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “selected branch statement”. The selected-branch identity exposed by the target.

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 selected-branch identity exposed by the target.

Declaration kind. def.

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

Lean code for Definition6.1.23●1 definition

defdefined in QuantumBlockEncoding/CircuitSemantics.lean

complete

def QuantumBlockEncoding.BlockExtractionBranchContributionTarget.selectedBranchStatement.{u}
  {α : Type u} [OfNat α 0] [OfNat α 1] [HAdd α α α] [HMul α α α]
  {rows cols signalDim branchDim : ℕ}
  (target :
    QuantumBlockEncoding.BlockExtractionBranchContributionTarget α rows
      cols signalDim branchDim) :
  Prop

def QuantumBlockEncoding.BlockExtractionBranchContributionTarget.selectedBranchStatement.{u}
  {α : Type u} [OfNat α 0] [OfNat α 1]
  [HAdd α α α] [HMul α α α]
  {rows cols signalDim branchDim : ℕ}
  (target :
    QuantumBlockEncoding.BlockExtractionBranchContributionTarget
      α rows cols signalDim branchDim) :
  Prop

The selected-branch identity exposed by the target.

Definition6.1.24

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “projection summation statement”. The projection/summation theorem still required for the target.

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 projection/summation theorem still required for the target.

Declaration kind. def.

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

Lean code for Definition6.1.24●1 definition

defdefined in QuantumBlockEncoding/CircuitSemantics.lean

complete

def QuantumBlockEncoding.BlockExtractionBranchContributionTarget.projectionSummationStatement.{u}
  {α : Type u} [OfNat α 0] [OfNat α 1] [HAdd α α α] [HMul α α α]
  {rows cols signalDim branchDim : ℕ}
  (target :
    QuantumBlockEncoding.BlockExtractionBranchContributionTarget α rows
      cols signalDim branchDim) :
  Prop

def QuantumBlockEncoding.BlockExtractionBranchContributionTarget.projectionSummationStatement.{u}
  {α : Type u} [OfNat α 0] [OfNat α 1]
  [HAdd α α α] [HMul α α α]
  {rows cols signalDim branchDim : ℕ}
  (target :
    QuantumBlockEncoding.BlockExtractionBranchContributionTarget
      α rows cols signalDim branchDim) :
  Prop

The projection/summation theorem still required for the target.

Definition6.1.25

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “backend expansion statement”. The backend expansion theorem needed to close 'projectionSummationStatement'.

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 backend expansion theorem needed to close 'projectionSummationStatement'. This version is stated directly in terms of the extraction target's block matrix entry and the candidate branch-contribution fold. It is useful as a proof-DAG interface because paper-specific projection backends can target this statement without depending on the record's cached 'blockEntry' and 'branchSum' fields.

Declaration kind. def.

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

Lean code for Definition6.1.25●1 definition

defdefined in QuantumBlockEncoding/CircuitSemantics.lean

complete

def QuantumBlockEncoding.BlockExtractionBranchContributionTarget.backendExpansionStatement.{u}
  {α : Type u} [OfNat α 0] [OfNat α 1] [HAdd α α α] [HMul α α α]
  {rows cols signalDim branchDim : ℕ}
  (target :
    QuantumBlockEncoding.BlockExtractionBranchContributionTarget α rows
      cols signalDim branchDim) :
  Prop

def QuantumBlockEncoding.BlockExtractionBranchContributionTarget.backendExpansionStatement.{u}
  {α : Type u} [OfNat α 0] [OfNat α 1]
  [HAdd α α α] [HMul α α α]
  {rows cols signalDim branchDim : ℕ}
  (target :
    QuantumBlockEncoding.BlockExtractionBranchContributionTarget
      α rows cols signalDim branchDim) :
  Prop

The backend expansion theorem needed to close `projectionSummationStatement`.

This version is stated directly in terms of the extraction target's block
matrix entry and the candidate branch-contribution fold.  It is useful as a
proof-DAG interface because paper-specific projection backends can target this
statement without depending on the record's cached `blockEntry` and `branchSum`
fields.

Theorem6.1.26

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “selected branch statement of 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/CircuitSemantics.lean:595. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.1.26●1 theorem

theoremdefined in QuantumBlockEncoding/CircuitSemantics.lean

complete

theorem QuantumBlockEncoding.BlockExtractionBranchContributionTarget.selectedBranchStatement_of_eq.{u}
  {α : Type u} [OfNat α 0] [OfNat α 1] [HAdd α α α] [HMul α α α]
  {rows cols signalDim branchDim : ℕ}
  (target :
    QuantumBlockEncoding.BlockExtractionBranchContributionTarget α rows
      cols signalDim branchDim) :
  target.selectedBranchStatement

theorem QuantumBlockEncoding.BlockExtractionBranchContributionTarget.selectedBranchStatement_of_eq.{u}
  {α : Type u} [OfNat α 0] [OfNat α 1]
  [HAdd α α α] [HMul α α α]
  {rows cols signalDim branchDim : ℕ}
  (target :
    QuantumBlockEncoding.BlockExtractionBranchContributionTarget
      α rows cols signalDim branchDim) :
  target.selectedBranchStatement

Theorem6.1.27

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “projection summation statement iff backend expansion statement”; 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/CircuitSemantics.lean:603. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.1.27●1 theorem

theoremdefined in QuantumBlockEncoding/CircuitSemantics.lean

complete

theorem QuantumBlockEncoding.BlockExtractionBranchContributionTarget.projectionSummationStatement_iff_backendExpansionStatement.{u}
  {α : Type u} [OfNat α 0] [OfNat α 1] [HAdd α α α] [HMul α α α]
  {rows cols signalDim branchDim : ℕ}
  (target :
    QuantumBlockEncoding.BlockExtractionBranchContributionTarget α rows
      cols signalDim branchDim) :
  target.projectionSummationStatement ↔ target.backendExpansionStatement

theorem QuantumBlockEncoding.BlockExtractionBranchContributionTarget.projectionSummationStatement_iff_backendExpansionStatement.{u}
  {α : Type u} [OfNat α 0] [OfNat α 1]
  [HAdd α α α] [HMul α α α]
  {rows cols signalDim branchDim : ℕ}
  (target :
    QuantumBlockEncoding.BlockExtractionBranchContributionTarget
      α rows cols signalDim branchDim) :
  target.projectionSummationStatement ↔
    target.backendExpansionStatement

Theorem6.1.28

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “projection summation statement of backend expansion statement”; 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/CircuitSemantics.lean:629. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.1.28●1 theorem

theoremdefined in QuantumBlockEncoding/CircuitSemantics.lean

complete

theorem QuantumBlockEncoding.BlockExtractionBranchContributionTarget.projectionSummationStatement_of_backendExpansionStatement.{u}
  {α : Type u} [OfNat α 0] [OfNat α 1] [HAdd α α α] [HMul α α α]
  {rows cols signalDim branchDim : ℕ}
  (target :
    QuantumBlockEncoding.BlockExtractionBranchContributionTarget α rows
      cols signalDim branchDim)
  (hexpansion : target.backendExpansionStatement) :
  target.projectionSummationStatement

theorem QuantumBlockEncoding.BlockExtractionBranchContributionTarget.projectionSummationStatement_of_backendExpansionStatement.{u}
  {α : Type u} [OfNat α 0] [OfNat α 1]
  [HAdd α α α] [HMul α α α]
  {rows cols signalDim branchDim : ℕ}
  (target :
    QuantumBlockEncoding.BlockExtractionBranchContributionTarget
      α rows cols signalDim branchDim)
  (hexpansion :
    target.backendExpansionStatement) :
  target.projectionSummationStatement

Theorem6.1.29

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “backend expansion statement of projection summation statement”; 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/CircuitSemantics.lean:640. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.1.29●1 theorem

theoremdefined in QuantumBlockEncoding/CircuitSemantics.lean

complete

theorem QuantumBlockEncoding.BlockExtractionBranchContributionTarget.backendExpansionStatement_of_projectionSummationStatement.{u}
  {α : Type u} [OfNat α 0] [OfNat α 1] [HAdd α α α] [HMul α α α]
  {rows cols signalDim branchDim : ℕ}
  (target :
    QuantumBlockEncoding.BlockExtractionBranchContributionTarget α rows
      cols signalDim branchDim)
  (hprojection : target.projectionSummationStatement) :
  target.backendExpansionStatement

theorem QuantumBlockEncoding.BlockExtractionBranchContributionTarget.backendExpansionStatement_of_projectionSummationStatement.{u}
  {α : Type u} [OfNat α 0] [OfNat α 1]
  [HAdd α α α] [HMul α α α]
  {rows cols signalDim branchDim : ℕ}
  (target :
    QuantumBlockEncoding.BlockExtractionBranchContributionTarget
      α rows cols signalDim branchDim)
  (hprojection :
    target.projectionSummationStatement) :
  target.backendExpansionStatement

Definition6.1.30

uses 0used by 0✓L∃∀N

Plain-English reading. This record groups the data and proof fields needed for “circuit block encoding claim”. A proposition-valued field is a requirement until a constructor supplies it. A circuit-level block encoding claim bundling a circuit matrix semantics with a block extraction target and a dimension compatibility proof.

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

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. A circuit-level block encoding claim bundling a circuit matrix semantics with a block extraction target and a dimension compatibility proof. The 'blockCorrect' obligation tracks the main mathematical claim: (⟨signalIdx| ⊗ I) U (|signalIdx⟩ ⊗ I) = targetMatrix / normalizer. This does not assert the claim is true; it records what needs proving.

Declaration kind. structure.

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

Lean code for Definition6.1.30●1 definition

structure(4 fields)defined in QuantumBlockEncoding/CircuitSemantics.lean

complete

structure QuantumBlockEncoding.CircuitBlockEncodingClaim.{u} (α : Type u)
  [OfNat α 0] [OfNat α 1] [HAdd α α α] [HMul α α α]
  (qubits dim signalDim : ℕ) : Type u

structure QuantumBlockEncoding.CircuitBlockEncodingClaim.{u}
  (α : Type u) [OfNat α 0] [OfNat α 1]
  [HAdd α α α] [HMul α α α]
  (qubits dim signalDim : ℕ) : Type u

A circuit-level block encoding claim bundling a circuit matrix semantics
with a block extraction target and a dimension compatibility proof.

The `blockCorrect` obligation tracks the main mathematical claim:
(⟨signalIdx| ⊗ I) U (|signalIdx⟩ ⊗ I) = targetMatrix / normalizer.
This does not assert the claim is true; it records what needs proving.

Fields

semantics : QuantumBlockEncoding.CircuitMatrixSemantics α qubits

target : QuantumBlockEncoding.BlockExtractionTarget α dim dim signalDim

dimCompat : QuantumBlockEncoding.qubitDim qubits = signalDim * dim

blockCorrect : QuantumBlockEncoding.SemanticObligation

Definition6.1.31

uses 0used by 0✓L∃∀N

Plain-English reading. This record groups the data and proof fields needed for “finite block composition contract”. A proposition-valued field is a requirement until a constructor supplies it. Typed contract for a finite-dimensional LCU/block-composition step.

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

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. Typed contract for a finite-dimensional LCU/block-composition step. This is intentionally contract-only: it states the exact matrix objects and obligations that a later theorem must connect, without treating a cited LCU result or a paper theorem as a Lean proof.

Declaration kind. structure.

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

Lean code for Definition6.1.31●1 definition

structure(15 fields)defined in QuantumBlockEncoding/CircuitSemantics.lean

complete

structure QuantumBlockEncoding.FiniteBlockCompositionContract.{u} (α : Type u)
  [OfNat α 0] [OfNat α 1] [HAdd α α α] [HMul α α α]
  (qubits dim signalDim : ℕ) : Type u

structure QuantumBlockEncoding.FiniteBlockCompositionContract.{u}
  (α : Type u) [OfNat α 0] [OfNat α 1]
  [HAdd α α α] [HMul α α α]
  (qubits dim signalDim : ℕ) : Type u

Typed contract for a finite-dimensional LCU/block-composition step.

This is intentionally contract-only: it states the exact matrix objects and
obligations that a later theorem must connect, without treating a cited LCU
result or a paper theorem as a Lean proof.

Fields

sourceAnchor : String

lcuSourceAnchor : String

theoremAnchor : String

claim : QuantumBlockEncoding.CircuitBlockEncodingClaim α qubits dim signalDim

expectedTarget : QuantumBlockEncoding.BlockExtractionTarget α dim dim signalDim

targetMatrix : QuantumBlockEncoding.Matrix dim dim α

normalizer : α

claimTargetMatches : self.claim.target = self.expectedTarget

targetMatrixMatches : self.expectedTarget.targetMatrix = self.targetMatrix

targetNormalizerMatches : self.expectedTarget.normalizer = self.normalizer

circuitUnitary : QuantumBlockEncoding.SemanticObligation

lcuComposition : QuantumBlockEncoding.SemanticObligation

blockProjection : QuantumBlockEncoding.SemanticObligation

normalizedBlockEquality : QuantumBlockEncoding.SemanticObligation

finalExtraction : QuantumBlockEncoding.SemanticObligation

Definition6.1.32

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “signal system block row index”. Compound row index for a signal value and a system-row 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. Compound row index for a signal value and a system-row index.

Declaration kind. def.

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

Lean code for Definition6.1.32●1 definition

defdefined in QuantumBlockEncoding/CircuitSemantics.lean

complete

def QuantumBlockEncoding.signalSystemBlockRowIndex
  (rows signalIdx systemIdx : ℕ) : ℕ

def QuantumBlockEncoding.signalSystemBlockRowIndex
  (rows signalIdx systemIdx : ℕ) : ℕ

Compound row index for a signal value and a system-row index.

Definition6.1.33

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “signal system block col index”. Compound column index for a signal value and a system-column 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. Compound column index for a signal value and a system-column index.

Declaration kind. def.

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

Lean code for Definition6.1.33●1 definition

defdefined in QuantumBlockEncoding/CircuitSemantics.lean

complete

def QuantumBlockEncoding.signalSystemBlockColIndex
  (cols signalIdx systemIdx : ℕ) : ℕ

def QuantumBlockEncoding.signalSystemBlockColIndex
  (cols signalIdx systemIdx : ℕ) : ℕ

Compound column index for a signal value and a system-column index.

Theorem6.1.34

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “signal system block row index 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.

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

Lean code for Theorem6.1.34●1 theorem

theoremdefined in QuantumBlockEncoding/CircuitSemantics.lean

complete

theorem QuantumBlockEncoding.signalSystemBlockRowIndex_zero
  (rows systemIdx : ℕ) :
  QuantumBlockEncoding.signalSystemBlockRowIndex rows 0 systemIdx =
    systemIdx

theorem QuantumBlockEncoding.signalSystemBlockRowIndex_zero
  (rows systemIdx : ℕ) :
  QuantumBlockEncoding.signalSystemBlockRowIndex
      rows 0 systemIdx =
    systemIdx

Theorem6.1.35

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “signal system block col index 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.

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

Lean code for Theorem6.1.35●1 theorem

theoremdefined in QuantumBlockEncoding/CircuitSemantics.lean

complete

theorem QuantumBlockEncoding.signalSystemBlockColIndex_zero
  (cols systemIdx : ℕ) :
  QuantumBlockEncoding.signalSystemBlockColIndex cols 0 systemIdx =
    systemIdx

theorem QuantumBlockEncoding.signalSystemBlockColIndex_zero
  (cols systemIdx : ℕ) :
  QuantumBlockEncoding.signalSystemBlockColIndex
      cols 0 systemIdx =
    systemIdx

Theorem6.1.36

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “signal system block row index lt”; the hypotheses and conclusion in the code panel fix its exact scope. The row compound index stays inside a signal × row matrix.

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 row compound index stays inside a signal × row matrix.

Declaration kind. theorem.

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

Lean code for Theorem6.1.36●1 theorem

theoremdefined in QuantumBlockEncoding/CircuitSemantics.lean

complete

theorem QuantumBlockEncoding.signalSystemBlockRowIndex_lt {signalDim rows : ℕ}
  (signalIdx : Fin signalDim) (i : Fin rows) :
  QuantumBlockEncoding.signalSystemBlockRowIndex rows ↑signalIdx ↑i <
    signalDim * rows

theorem QuantumBlockEncoding.signalSystemBlockRowIndex_lt
  {signalDim rows : ℕ}
  (signalIdx : Fin signalDim)
  (i : Fin rows) :
  QuantumBlockEncoding.signalSystemBlockRowIndex
      rows ↑signalIdx ↑i <
    signalDim * rows

The row compound index stays inside a signal × row matrix.

Theorem6.1.37

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “signal system block col index lt”; the hypotheses and conclusion in the code panel fix its exact scope. The column compound index stays inside a signal × column matrix.

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 column compound index stays inside a signal × column matrix.

Declaration kind. theorem.

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

Lean code for Theorem6.1.37●1 theorem

theoremdefined in QuantumBlockEncoding/CircuitSemantics.lean

complete

theorem QuantumBlockEncoding.signalSystemBlockColIndex_lt {signalDim cols : ℕ}
  (signalIdx : Fin signalDim) (j : Fin cols) :
  QuantumBlockEncoding.signalSystemBlockColIndex cols ↑signalIdx ↑j <
    signalDim * cols

theorem QuantumBlockEncoding.signalSystemBlockColIndex_lt
  {signalDim cols : ℕ}
  (signalIdx : Fin signalDim)
  (j : Fin cols) :
  QuantumBlockEncoding.signalSystemBlockColIndex
      cols ↑signalIdx ↑j <
    signalDim * cols

The column compound index stays inside a signal × column matrix.

Definition6.1.38

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “signal system block projection”. Block projection: extract the '(signalIdx, signalIdx)' block from a signal × system matrix.

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. Block projection: extract the '(signalIdx, signalIdx)' block from a signal × system matrix. Given a matrix M of size '(signalDim * rows) × (signalDim * cols)', the helpers 'signalSystemBlockRowIndex' and 'signalSystemBlockColIndex' map a pair '(i, j)' of system indices to the compound row and column indices in the full matrix that correspond to signal register value 'idx' and system indices '(i, j)'. The block '(⟨signalIdx| ⊗ I) M (|signalIdx⟩ ⊗ I)' is then: blockMatrix i j = M (signalIdx * rows + i) (signalIdx * cols + j)

Declaration kind. def.

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

Lean code for Definition6.1.38●1 definition

defdefined in QuantumBlockEncoding/CircuitSemantics.lean

complete

def QuantumBlockEncoding.signalSystemBlockProjection.{u} {α : Type u}
  [OfNat α 0] (signalDim rows cols : ℕ)
  (M :
    QuantumBlockEncoding.Matrix (signalDim * rows) (signalDim * cols) α)
  (signalIdx : Fin signalDim) : QuantumBlockEncoding.Matrix rows cols α

def QuantumBlockEncoding.signalSystemBlockProjection.{u}
  {α : Type u} [OfNat α 0]
  (signalDim rows cols : ℕ)
  (M :
    QuantumBlockEncoding.Matrix
      (signalDim * rows)
      (signalDim * cols) α)
  (signalIdx : Fin signalDim) :
  QuantumBlockEncoding.Matrix rows cols α

Block projection: extract the `(signalIdx, signalIdx)` block from a
signal × system matrix.

Given a matrix M of size `(signalDim * rows) × (signalDim * cols)`, the helpers
`signalSystemBlockRowIndex` and `signalSystemBlockColIndex` map a pair `(i, j)`
of system indices to the compound row and column indices in the full matrix
that correspond to signal register value `idx` and system indices `(i, j)`.

The block `(⟨signalIdx| ⊗ I) M (|signalIdx⟩ ⊗ I)` is then:
  blockMatrix i j = M (signalIdx * rows + i) (signalIdx * cols + j)

Theorem6.1.39

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “signal system block projection 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/CircuitSemantics.lean:764. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.1.39●1 theorem

theoremdefined in QuantumBlockEncoding/CircuitSemantics.lean

complete

theorem QuantumBlockEncoding.signalSystemBlockProjection_apply.{u} {α : Type u}
  [OfNat α 0] {signalDim rows cols : ℕ}
  (M :
    QuantumBlockEncoding.Matrix (signalDim * rows) (signalDim * cols) α)
  (signalIdx : Fin signalDim) (i : Fin rows) (j : Fin cols) :
  QuantumBlockEncoding.signalSystemBlockProjection signalDim rows cols M
      signalIdx i j =
    M
      ⟨QuantumBlockEncoding.signalSystemBlockRowIndex rows ↑signalIdx
          ↑i,
        ⋯⟩
      ⟨QuantumBlockEncoding.signalSystemBlockColIndex cols ↑signalIdx
          ↑j,
        ⋯⟩

theorem QuantumBlockEncoding.signalSystemBlockProjection_apply.{u}
  {α : Type u} [OfNat α 0]
  {signalDim rows cols : ℕ}
  (M :
    QuantumBlockEncoding.Matrix
      (signalDim * rows)
      (signalDim * cols) α)
  (signalIdx : Fin signalDim)
  (i : Fin rows) (j : Fin cols) :
  QuantumBlockEncoding.signalSystemBlockProjection
      signalDim rows cols M signalIdx i
      j =
    M
      ⟨QuantumBlockEncoding.signalSystemBlockRowIndex
          rows ↑signalIdx ↑i,
        ⋯⟩
      ⟨QuantumBlockEncoding.signalSystemBlockColIndex
          cols ↑signalIdx ↑j,
        ⋯⟩

Definition6.1.40

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “total circuit qubits”. Total qubits needed for a circuit operating on 'system' system qubits and 'signal' signal qubits.

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. Total qubits needed for a circuit operating on 'system' system qubits and 'signal' signal qubits.

Declaration kind. def.

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

Lean code for Definition6.1.40●1 definition

defdefined in QuantumBlockEncoding/CircuitSemantics.lean

complete

def QuantumBlockEncoding.totalCircuitQubits (system signal : ℕ) : ℕ

def QuantumBlockEncoding.totalCircuitQubits
  (system signal : ℕ) : ℕ

Total qubits needed for a circuit operating on `system` system qubits
and `signal` signal qubits.

Definition6.1.41

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “block extraction target”. Build a BlockExtractionTarget from a CircuitMatrixSemantics by computing the block projection.

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. Build a BlockExtractionTarget from a CircuitMatrixSemantics by computing the block projection. The circuit matrix is square with dimension 'signalDim * dim', and we extract the '(signalIdx, signalIdx)' block.

Declaration kind. def.

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

Lean code for Definition6.1.41●1 definition

defdefined in QuantumBlockEncoding/CircuitSemantics.lean

complete

def QuantumBlockEncoding.CircuitMatrixSemantics.blockExtractionTarget.{u}
  {α : Type u} [OfNat α 0] [OfNat α 1] [HAdd α α α] [HMul α α α]
  {qubits : ℕ}
  (sem : QuantumBlockEncoding.CircuitMatrixSemantics α qubits)
  (dim signalDim : ℕ)
  (hDim : QuantumBlockEncoding.qubitDim qubits = signalDim * dim)
  (targetMatrix : QuantumBlockEncoding.Matrix dim dim α)
  (normalizer : α) (signalIdx : Fin signalDim) :
  QuantumBlockEncoding.BlockExtractionTarget α dim dim signalDim

def QuantumBlockEncoding.CircuitMatrixSemantics.blockExtractionTarget.{u}
  {α : Type u} [OfNat α 0] [OfNat α 1]
  [HAdd α α α] [HMul α α α] {qubits : ℕ}
  (sem :
    QuantumBlockEncoding.CircuitMatrixSemantics
      α qubits)
  (dim signalDim : ℕ)
  (hDim :
    QuantumBlockEncoding.qubitDim qubits =
      signalDim * dim)
  (targetMatrix :
    QuantumBlockEncoding.Matrix dim dim α)
  (normalizer : α)
  (signalIdx : Fin signalDim) :
  QuantumBlockEncoding.BlockExtractionTarget
    α dim dim signalDim

Build a BlockExtractionTarget from a CircuitMatrixSemantics by computing
the block projection. The circuit matrix is square with dimension
`signalDim * dim`, and we extract the `(signalIdx, signalIdx)` block.