Figure4Primitive.lean🔗

54 explicit public declarations, in source order.

Definition10.10.1

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin row bulk indicator program”. Historical row-bulk indicator for rows 2 through 5 of 'D'.

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. Paper-facing backend models and concrete Robin-boundary example artifacts.

Technical source note. Historical row-bulk indicator for rows 2 through 5 of 'D'. Figure 4 acts on 'D^T', so this circuit is retained only as a source-audit guard.

Declaration kind. def.

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

Lean code for Definition10.10.1●1 definition

defdefined in QuantumBlockEncoding/Robin/Figure4Primitive.lean

complete

def QuantumBlockEncoding.Robin.warmRobinRowBulkIndicatorProgram :
  QuantumBlockEncoding.PrimitiveCircuit 4

def QuantumBlockEncoding.Robin.warmRobinRowBulkIndicatorProgram :
  QuantumBlockEncoding.PrimitiveCircuit 4

Historical row-bulk indicator for rows 2 through 5 of `D`.  Figure 4 acts
on `D^T`, so this circuit is retained only as a source-audit guard.

Definition10.10.2

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin row bulk indicator basis equiv”.

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. Paper-facing backend models and concrete Robin-boundary example artifacts.

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

Lean code for Definition10.10.2●1 definition

defdefined in QuantumBlockEncoding/Robin/Figure4Primitive.lean

complete

def QuantumBlockEncoding.Robin.warmRobinRowBulkIndicatorBasisEquiv :
  QuantumBlockEncoding.PrimitiveBasis 4 ≃
    QuantumBlockEncoding.PrimitiveBasis 4

def QuantumBlockEncoding.Robin.warmRobinRowBulkIndicatorBasisEquiv :
  QuantumBlockEncoding.PrimitiveBasis 4 ≃
    QuantumBlockEncoding.PrimitiveBasis 4

Theorem10.10.3

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin row bulk indicator basis action”; the hypotheses and conclusion in the code panel fix its exact scope.

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

Why it is in this chapter. Paper-facing backend models and concrete Robin-boundary example artifacts.

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

Lean code for Theorem10.10.3●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/Figure4Primitive.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinRowBulkIndicatorBasisAction
  (bits : QuantumBlockEncoding.PrimitiveBasis 4) :
  have output :=
    QuantumBlockEncoding.Robin.warmRobinRowBulkIndicatorBasisEquiv bits;
  output 0 = bits 0 ∧
    output 1 = bits 1 ∧
      output 2 = bits 2 ∧
        output 3 =
          if
              2 ≤ ↑(bits 0) + 2 * ↑(bits 1) + 4 * ↑(bits 2) ∧
                ↑(bits 0) + 2 * ↑(bits 1) + 4 * ↑(bits 2) ≤ 5 then
            Fin.cases 1 (fun x => 0) (bits 3)
          else bits 3

theorem QuantumBlockEncoding.Robin.warmRobinRowBulkIndicatorBasisAction
  (bits :
    QuantumBlockEncoding.PrimitiveBasis
      4) :
  have output :=
    QuantumBlockEncoding.Robin.warmRobinRowBulkIndicatorBasisEquiv
      bits;
  output 0 = bits 0 ∧
    output 1 = bits 1 ∧
      output 2 = bits 2 ∧
        output 3 =
          if
              2 ≤
                  ↑(bits 0) +
                      2 * ↑(bits 1) +
                    4 * ↑(bits 2) ∧
                ↑(bits 0) +
                      2 * ↑(bits 1) +
                    4 * ↑(bits 2) ≤
                  5 then
            Fin.cases 1 (fun x => 0)
              (bits 3)
          else bits 3

Theorem10.10.4

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin row bulk indicator program eval”; the hypotheses and conclusion in the code panel fix its exact scope.

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

Why it is in this chapter. Paper-facing backend models and concrete Robin-boundary example artifacts.

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

Lean code for Theorem10.10.4●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/Figure4Primitive.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinRowBulkIndicatorProgram_eval :
  QuantumBlockEncoding.evalPrimitiveCircuit
      QuantumBlockEncoding.Robin.warmRobinRowBulkIndicatorProgram =
    QuantumBlockEncoding.Robin.ComplexLCU.equivPermutationMatrix
      QuantumBlockEncoding.Robin.warmRobinRowBulkIndicatorBasisEquiv

theorem QuantumBlockEncoding.Robin.warmRobinRowBulkIndicatorProgram_eval :
  QuantumBlockEncoding.evalPrimitiveCircuit
      QuantumBlockEncoding.Robin.warmRobinRowBulkIndicatorProgram =
    QuantumBlockEncoding.Robin.ComplexLCU.equivPermutationMatrix
      QuantumBlockEncoding.Robin.warmRobinRowBulkIndicatorBasisEquiv

Definition10.10.5

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “primitive swap circuit”. One physical SWAP expanded into the allowed primitive basis.

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. Paper-facing backend models and concrete Robin-boundary example artifacts.

Technical source note. One physical SWAP expanded into the allowed primitive basis.

Declaration kind. def.

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

Lean code for Definition10.10.5●1 definition

defdefined in QuantumBlockEncoding/Robin/Figure4Primitive.lean

complete

def QuantumBlockEncoding.Robin.primitiveSwapCircuit {qubits : ℕ}
  (left right : Fin qubits) (distinct : left ≠ right) :
  QuantumBlockEncoding.PrimitiveCircuit qubits

def QuantumBlockEncoding.Robin.primitiveSwapCircuit
  {qubits : ℕ} (left right : Fin qubits)
  (distinct : left ≠ right) :
  QuantumBlockEncoding.PrimitiveCircuit
    qubits

One physical SWAP expanded into the allowed primitive basis.

Definition10.10.6

uses 0used by 0✓L∃∀N

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

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. Paper-facing backend models and concrete Robin-boundary example artifacts.

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

Lean code for Definition10.10.6●1 definition

defdefined in QuantumBlockEncoding/Robin/Figure4Primitive.lean

complete

def QuantumBlockEncoding.Robin.primitiveSwapBasisEquiv {qubits : ℕ}
  (left right : Fin qubits) (distinct : left ≠ right) :
  QuantumBlockEncoding.PrimitiveBasis qubits ≃
    QuantumBlockEncoding.PrimitiveBasis qubits

def QuantumBlockEncoding.Robin.primitiveSwapBasisEquiv
  {qubits : ℕ} (left right : Fin qubits)
  (distinct : left ≠ right) :
  QuantumBlockEncoding.PrimitiveBasis
      qubits ≃
    QuantumBlockEncoding.PrimitiveBasis
      qubits

Theorem10.10.7

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “primitive swap circuit eval”; the hypotheses and conclusion in the code panel fix its exact scope.

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

Why it is in this chapter. Paper-facing backend models and concrete Robin-boundary example artifacts.

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

Lean code for Theorem10.10.7●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/Figure4Primitive.lean

complete

theorem QuantumBlockEncoding.Robin.primitiveSwapCircuit_eval {qubits : ℕ}
  (left right : Fin qubits) (distinct : left ≠ right) :
  QuantumBlockEncoding.evalPrimitiveCircuit
      (QuantumBlockEncoding.Robin.primitiveSwapCircuit left right
        distinct) =
    QuantumBlockEncoding.Robin.ComplexLCU.equivPermutationMatrix
      (QuantumBlockEncoding.Robin.primitiveSwapBasisEquiv left right
        distinct)

theorem QuantumBlockEncoding.Robin.primitiveSwapCircuit_eval
  {qubits : ℕ} (left right : Fin qubits)
  (distinct : left ≠ right) :
  QuantumBlockEncoding.evalPrimitiveCircuit
      (QuantumBlockEncoding.Robin.primitiveSwapCircuit
        left right distinct) =
    QuantumBlockEncoding.Robin.ComplexLCU.equivPermutationMatrix
      (QuantumBlockEncoding.Robin.primitiveSwapBasisEquiv
        left right distinct)

Definition10.10.8

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin figure 4 register swap program”. Swap the two fixed three-qubit registers with three actual SWAPs.

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. Paper-facing backend models and concrete Robin-boundary example artifacts.

Technical source note. Swap the two fixed three-qubit registers with three actual SWAPs.

Declaration kind. def.

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

Lean code for Definition10.10.8●1 definition

defdefined in QuantumBlockEncoding/Robin/Figure4Primitive.lean

complete

def QuantumBlockEncoding.Robin.warmRobinFigure4RegisterSwapProgram :
  QuantumBlockEncoding.PrimitiveCircuit 6

def QuantumBlockEncoding.Robin.warmRobinFigure4RegisterSwapProgram :
  QuantumBlockEncoding.PrimitiveCircuit 6

Swap the two fixed three-qubit registers with three actual SWAPs.

Definition10.10.9

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin figure 4 register swap basis equiv”.

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. Paper-facing backend models and concrete Robin-boundary example artifacts.

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

Lean code for Definition10.10.9●1 definition

defdefined in QuantumBlockEncoding/Robin/Figure4Primitive.lean

complete

def QuantumBlockEncoding.Robin.warmRobinFigure4RegisterSwapBasisEquiv :
  QuantumBlockEncoding.PrimitiveBasis 6 ≃
    QuantumBlockEncoding.PrimitiveBasis 6

def QuantumBlockEncoding.Robin.warmRobinFigure4RegisterSwapBasisEquiv :
  QuantumBlockEncoding.PrimitiveBasis 6 ≃
    QuantumBlockEncoding.PrimitiveBasis 6

Theorem10.10.10

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin figure 4 register swap program eval”; the hypotheses and conclusion in the code panel fix its exact scope.

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

Why it is in this chapter. Paper-facing backend models and concrete Robin-boundary example artifacts.

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

Lean code for Theorem10.10.10●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/Figure4Primitive.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinFigure4RegisterSwapProgram_eval :
  QuantumBlockEncoding.evalPrimitiveCircuit
      QuantumBlockEncoding.Robin.warmRobinFigure4RegisterSwapProgram =
    QuantumBlockEncoding.Robin.ComplexLCU.equivPermutationMatrix
      QuantumBlockEncoding.Robin.warmRobinFigure4RegisterSwapBasisEquiv

theorem QuantumBlockEncoding.Robin.warmRobinFigure4RegisterSwapProgram_eval :
  QuantumBlockEncoding.evalPrimitiveCircuit
      QuantumBlockEncoding.Robin.warmRobinFigure4RegisterSwapProgram =
    QuantumBlockEncoding.Robin.ComplexLCU.equivPermutationMatrix
      QuantumBlockEncoding.Robin.warmRobinFigure4RegisterSwapBasisEquiv

Theorem10.10.11

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin figure 4 register swap basis action”; the hypotheses and conclusion in the code panel fix its exact scope.

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

Why it is in this chapter. Paper-facing backend models and concrete Robin-boundary example artifacts.

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

Lean code for Theorem10.10.11●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/Figure4Primitive.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinFigure4RegisterSwapBasisAction
  (bits : QuantumBlockEncoding.PrimitiveBasis 6) :
  have output :=
    QuantumBlockEncoding.Robin.warmRobinFigure4RegisterSwapBasisEquiv
      bits;
  output 0 = bits 3 ∧
    output 1 = bits 4 ∧
      output 2 = bits 5 ∧
        output 3 = bits 0 ∧ output 4 = bits 1 ∧ output 5 = bits 2

theorem QuantumBlockEncoding.Robin.warmRobinFigure4RegisterSwapBasisAction
  (bits :
    QuantumBlockEncoding.PrimitiveBasis
      6) :
  have output :=
    QuantumBlockEncoding.Robin.warmRobinFigure4RegisterSwapBasisEquiv
      bits;
  output 0 = bits 3 ∧
    output 1 = bits 4 ∧
      output 2 = bits 5 ∧
        output 3 = bits 0 ∧
          output 4 = bits 1 ∧
            output 5 = bits 2

Theorem10.10.12

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin figure 4 register swap program counts”; 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. Paper-facing backend models and concrete Robin-boundary example artifacts.

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

Lean code for Theorem10.10.12●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/Figure4Primitive.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinFigure4RegisterSwapProgram_counts :
  QuantumBlockEncoding.Robin.warmRobinFigure4RegisterSwapProgram.ryCount =
      0 ∧
    QuantumBlockEncoding.Robin.warmRobinFigure4RegisterSwapProgram.cxCount =
      9

theorem QuantumBlockEncoding.Robin.warmRobinFigure4RegisterSwapProgram_counts :
  QuantumBlockEncoding.Robin.warmRobinFigure4RegisterSwapProgram.ryCount =
      0 ∧
    QuantumBlockEncoding.Robin.warmRobinFigure4RegisterSwapProgram.cxCount =
      9

Definition10.10.13

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin homogeneous coefficient oracle”. For homogeneous 'f=1', the coefficient oracle is physically empty.

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. Paper-facing backend models and concrete Robin-boundary example artifacts.

Technical source note. For homogeneous 'f=1', the coefficient oracle is physically empty.

Declaration kind. def.

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

Lean code for Definition10.10.13●1 definition

defdefined in QuantumBlockEncoding/Robin/Figure4Primitive.lean

complete

def QuantumBlockEncoding.Robin.warmRobinHomogeneousCoefficientOracle :
  QuantumBlockEncoding.PrimitiveCircuit 1

def QuantumBlockEncoding.Robin.warmRobinHomogeneousCoefficientOracle :
  QuantumBlockEncoding.PrimitiveCircuit 1

For homogeneous `f=1`, the coefficient oracle is physically empty.

Theorem10.10.14

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin homogeneous coefficient oracle eq identity”; 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. Paper-facing backend models and concrete Robin-boundary example artifacts.

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

Lean code for Theorem10.10.14●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/Figure4Primitive.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinHomogeneousCoefficientOracle_eq_identity :
  QuantumBlockEncoding.evalPrimitiveCircuit
      QuantumBlockEncoding.Robin.warmRobinHomogeneousCoefficientOracle =
    1

theorem QuantumBlockEncoding.Robin.warmRobinHomogeneousCoefficientOracle_eq_identity :
  QuantumBlockEncoding.evalPrimitiveCircuit
      QuantumBlockEncoding.Robin.warmRobinHomogeneousCoefficientOracle =
    1

Theorem10.10.15

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin row bulk indicator cleanup”; 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. Paper-facing backend models and concrete Robin-boundary example artifacts.

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

Lean code for Theorem10.10.15●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/Figure4Primitive.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinRowBulkIndicatorCleanup :
  QuantumBlockEncoding.evalPrimitiveCircuit
      (QuantumBlockEncoding.Robin.warmRobinRowBulkIndicatorProgram ++
        List.map QuantumBlockEncoding.PrimitiveGate.dagger
          (List.reverse
            QuantumBlockEncoding.Robin.warmRobinRowBulkIndicatorProgram)) =
    1

theorem QuantumBlockEncoding.Robin.warmRobinRowBulkIndicatorCleanup :
  QuantumBlockEncoding.evalPrimitiveCircuit
      (QuantumBlockEncoding.Robin.warmRobinRowBulkIndicatorProgram ++
        List.map
          QuantumBlockEncoding.PrimitiveGate.dagger
          (List.reverse
            QuantumBlockEncoding.Robin.warmRobinRowBulkIndicatorProgram)) =
    1

Definition10.10.16

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin figure 4 dt indicator reversible program”. Two disjoint pattern-controlled flips: '011' and '100'.

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. Paper-facing backend models and concrete Robin-boundary example artifacts.

Technical source note. Two disjoint pattern-controlled flips: '011' and '100'. Wires 'q3-q5' hold the system column, 'q7' is the indicator, and 'q8' is reusable clean workspace.

Declaration kind. def.

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

Lean code for Definition10.10.16●1 definition

defdefined in QuantumBlockEncoding/Robin/Figure4Primitive.lean

complete

def QuantumBlockEncoding.Robin.warmRobinFigure4DTIndicatorReversibleProgram :
  QuantumBlockEncoding.ReversibleProgram 9

def QuantumBlockEncoding.Robin.warmRobinFigure4DTIndicatorReversibleProgram :
  QuantumBlockEncoding.ReversibleProgram 9

Two disjoint pattern-controlled flips: `011` and `100`.  Wires `q3-q5`
hold the system column, `q7` is the indicator, and `q8` is reusable clean
workspace.

Definition10.10.17

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin figure 4 dt indicator basis equiv”.

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. Paper-facing backend models and concrete Robin-boundary example artifacts.

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

Lean code for Definition10.10.17●1 definition

defdefined in QuantumBlockEncoding/Robin/Figure4Primitive.lean

complete

def QuantumBlockEncoding.Robin.warmRobinFigure4DTIndicatorBasisEquiv :
  QuantumBlockEncoding.PrimitiveBasis 9 ≃
    QuantumBlockEncoding.PrimitiveBasis 9

def QuantumBlockEncoding.Robin.warmRobinFigure4DTIndicatorBasisEquiv :
  QuantumBlockEncoding.PrimitiveBasis 9 ≃
    QuantumBlockEncoding.PrimitiveBasis 9

Definition10.10.18

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin figure 4 system bits”.

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. Paper-facing backend models and concrete Robin-boundary example artifacts.

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

Lean code for Definition10.10.18●1 definition

defdefined in QuantumBlockEncoding/Robin/Figure4Primitive.lean

complete

def QuantumBlockEncoding.Robin.warmRobinFigure4SystemBits
  (bits : QuantumBlockEncoding.PrimitiveBasis 9) : Fin 8

def QuantumBlockEncoding.Robin.warmRobinFigure4SystemBits
  (bits :
    QuantumBlockEncoding.PrimitiveBasis
      9) :
  Fin 8

Theorem10.10.19

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin figure 4 dt indicator program basis action”; the hypotheses and conclusion in the code panel fix its exact scope.

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

Why it is in this chapter. Paper-facing backend models and concrete Robin-boundary example artifacts.

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

Lean code for Theorem10.10.19●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/Figure4Primitive.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinFigure4DTIndicatorProgram_basisAction
  (bits : QuantumBlockEncoding.PrimitiveBasis 9)
  (workspaceClean : bits 8 = 0) :
  have output :=
    QuantumBlockEncoding.Robin.warmRobinFigure4DTIndicatorBasisEquiv
      bits;
  (output 7 =
      if
          QuantumBlockEncoding.Robin.warmRobinFigure4TransposeBulk
            (QuantumBlockEncoding.Robin.warmRobinFigure4SystemBits
              bits) then
        QuantumBlockEncoding.flipBit (bits 7)
      else bits 7) ∧
    output 8 = 0 ∧
      ∀ (wire : Fin 9), wire ≠ 7 → wire ≠ 8 → output wire = bits wire

theorem QuantumBlockEncoding.Robin.warmRobinFigure4DTIndicatorProgram_basisAction
  (bits :
    QuantumBlockEncoding.PrimitiveBasis 9)
  (workspaceClean : bits 8 = 0) :
  have output :=
    QuantumBlockEncoding.Robin.warmRobinFigure4DTIndicatorBasisEquiv
      bits;
  (output 7 =
      if
          QuantumBlockEncoding.Robin.warmRobinFigure4TransposeBulk
            (QuantumBlockEncoding.Robin.warmRobinFigure4SystemBits
              bits) then
        QuantumBlockEncoding.flipBit
          (bits 7)
      else bits 7) ∧
    output 8 = 0 ∧
      ∀ (wire : Fin 9),
        wire ≠ 7 →
          wire ≠ 8 →
            output wire = bits wire

Theorem10.10.20

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin figure 4 dt indicator program workspace clean”; 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. Paper-facing backend models and concrete Robin-boundary example artifacts.

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

Lean code for Theorem10.10.20●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/Figure4Primitive.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinFigure4DTIndicatorProgram_workspaceClean
  (bits : QuantumBlockEncoding.PrimitiveBasis 9)
  (workspaceClean : bits 8 = 0) :
  QuantumBlockEncoding.Robin.warmRobinFigure4DTIndicatorBasisEquiv bits
      8 =
    0

theorem QuantumBlockEncoding.Robin.warmRobinFigure4DTIndicatorProgram_workspaceClean
  (bits :
    QuantumBlockEncoding.PrimitiveBasis 9)
  (workspaceClean : bits 8 = 0) :
  QuantumBlockEncoding.Robin.warmRobinFigure4DTIndicatorBasisEquiv
      bits 8 =
    0

Definition10.10.21

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin figure 4 dt indicator program”.

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. Paper-facing backend models and concrete Robin-boundary example artifacts.

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

Lean code for Definition10.10.21●1 definition

defdefined in QuantumBlockEncoding/Robin/Figure4Primitive.lean

complete

def QuantumBlockEncoding.Robin.warmRobinFigure4DTIndicatorProgram :
  QuantumBlockEncoding.PrimitiveProgram 9

def QuantumBlockEncoding.Robin.warmRobinFigure4DTIndicatorProgram :
  QuantumBlockEncoding.PrimitiveProgram 9

Theorem10.10.22

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin figure 4 dt indicator program eval”; the hypotheses and conclusion in the code panel fix its exact scope.

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

Why it is in this chapter. Paper-facing backend models and concrete Robin-boundary example artifacts.

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

Lean code for Theorem10.10.22●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/Figure4Primitive.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinFigure4DTIndicatorProgram_eval :
  QuantumBlockEncoding.evalPrimitiveProgram
      QuantumBlockEncoding.Robin.warmRobinFigure4DTIndicatorProgram =
    QuantumBlockEncoding.Robin.ComplexLCU.equivPermutationMatrix
      QuantumBlockEncoding.Robin.warmRobinFigure4DTIndicatorBasisEquiv

theorem QuantumBlockEncoding.Robin.warmRobinFigure4DTIndicatorProgram_eval :
  QuantumBlockEncoding.evalPrimitiveProgram
      QuantumBlockEncoding.Robin.warmRobinFigure4DTIndicatorProgram =
    QuantumBlockEncoding.Robin.ComplexLCU.equivPermutationMatrix
      QuantumBlockEncoding.Robin.warmRobinFigure4DTIndicatorBasisEquiv

Theorem10.10.23

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin figure 4 dt indicator program no oracle calls”; 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. Paper-facing backend models and concrete Robin-boundary example artifacts.

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

Lean code for Theorem10.10.23●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/Figure4Primitive.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinFigure4DTIndicatorProgram_noOracleCalls :
  QuantumBlockEncoding.Robin.warmRobinFigure4DTIndicatorProgram.resource.oracleCalls =
    0

theorem QuantumBlockEncoding.Robin.warmRobinFigure4DTIndicatorProgram_noOracleCalls :
  QuantumBlockEncoding.Robin.warmRobinFigure4DTIndicatorProgram.resource.oracleCalls =
    0

Definition10.10.24

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin figure 4 address bits”. Two disjoint pattern-controlled flips: '011' and '100'.

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. Paper-facing backend models and concrete Robin-boundary example artifacts.

Technical source note. Two disjoint pattern-controlled flips: '011' and '100'. Wires 'q3-q5' hold the system column, 'q7' is the indicator, and 'q8' is reusable clean workspace. -/ def warmRobinFigure4DTIndicatorReversibleProgram : ReversibleProgram 9 := [ .x 5 ] ++ cleanC3XReversibleProgram 3 4 5 7 8 (by decide) (by decide) (by decide) (by decide) (by decide) (by decide) ++ [ .x 5, .x 3, .x 4 ] ++ cleanC3XReversibleProgram 3 4 5 7 8 (by decide) (by decide) (by decide) (by decide) (by decide) (by decide) ++ [ .x 4, .x 3 ] def warmRobinFigure4DTIndicatorBasisEquiv : PrimitiveBasis 9 ≃ PrimitiveBasis 9 := evalReversibleProgram warmRobinFigure4DTIndicatorReversibleProgram def warmRobinFigure4SystemBits (bits : PrimitiveBasis 9) : Fin 8 := ⟨(bits 3).val + 2 * (bits 4).val + 4 * (bits 5).val, by omega⟩ theorem warmRobinFigure4DTIndicatorProgram_basisAction (bits : PrimitiveBasis 9) (workspaceClean : bits 8 = 0) : let output := warmRobinFigure4DTIndicatorBasisEquiv bits output 7 = (if warmRobinFigure4TransposeBulk (warmRobinFigure4SystemBits bits) then flipBit (bits 7) else bits 7) ∧ output 8 = 0 ∧ (∀ wire : Fin 9, wire ≠ 7 → wire ≠ 8 → output wire = bits wire) := by native_decide +revert theorem warmRobinFigure4DTIndicatorProgram_workspaceClean (bits : PrimitiveBasis 9) (workspaceClean : bits 8 = 0) : warmRobinFigure4DTIndicatorBasisEquiv bits 8 = 0 := (warmRobinFigure4DTIndicatorProgram_basisAction bits workspaceClean).2.1 noncomputable def warmRobinFigure4DTIndicatorProgram : PrimitiveProgram 9 := compileReversibleProgram warmRobinFigure4DTIndicatorReversibleProgram theorem warmRobinFigure4DTIndicatorProgram_eval : evalPrimitiveProgram warmRobinFigure4DTIndicatorProgram = ComplexLCU.equivPermutationMatrix warmRobinFigure4DTIndicatorBasisEquiv := by exact compileReversibleProgram_eval _ theorem warmRobinFigure4DTIndicatorProgram_noOracleCalls : warmRobinFigure4DTIndicatorProgram.resource.oracleCalls = 0 := PrimitiveCircuit.resource_oracleCalls_eq_zero _ /-! number number Distinct D-transpose and D sparse-access programs

Declaration kind. def.

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

Lean code for Definition10.10.24●1 definition

defdefined in QuantumBlockEncoding/Robin/Figure4Primitive.lean

complete

def QuantumBlockEncoding.Robin.warmRobinFigure4AddressBits
  (bits : QuantumBlockEncoding.PrimitiveBasis 9) : Fin 8

def QuantumBlockEncoding.Robin.warmRobinFigure4AddressBits
  (bits :
    QuantumBlockEncoding.PrimitiveBasis
      9) :
  Fin 8

Definition10.10.25

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin figure 4 dt sparse access reversible program”. Convert slot 's' to 's XOR 3', then add the system column modulo eight.

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. Paper-facing backend models and concrete Robin-boundary example artifacts.

Technical source note. Convert slot 's' to 's XOR 3', then add the system column modulo eight.

Declaration kind. def.

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

Lean code for Definition10.10.25●1 definition

defdefined in QuantumBlockEncoding/Robin/Figure4Primitive.lean

complete

def QuantumBlockEncoding.Robin.warmRobinFigure4DTSparseAccessReversibleProgram :
  QuantumBlockEncoding.ReversibleProgram 9

def QuantumBlockEncoding.Robin.warmRobinFigure4DTSparseAccessReversibleProgram :
  QuantumBlockEncoding.ReversibleProgram 9

Convert slot `s` to `s XOR 3`, then add the system column modulo eight.

Definition10.10.26

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin figure 4 dt sparse access basis equiv”.

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. Paper-facing backend models and concrete Robin-boundary example artifacts.

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

Lean code for Definition10.10.26●1 definition

defdefined in QuantumBlockEncoding/Robin/Figure4Primitive.lean

complete

def QuantumBlockEncoding.Robin.warmRobinFigure4DTSparseAccessBasisEquiv :
  QuantumBlockEncoding.PrimitiveBasis 9 ≃
    QuantumBlockEncoding.PrimitiveBasis 9

def QuantumBlockEncoding.Robin.warmRobinFigure4DTSparseAccessBasisEquiv :
  QuantumBlockEncoding.PrimitiveBasis 9 ≃
    QuantumBlockEncoding.PrimitiveBasis 9

Theorem10.10.27

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin figure 4 dt sparse access program clean action”; the hypotheses and conclusion in the code panel fix its exact scope.

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

Why it is in this chapter. Paper-facing backend models and concrete Robin-boundary example artifacts.

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

Lean code for Theorem10.10.27●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/Figure4Primitive.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinFigure4DTSparseAccessProgram_cleanAction
  (bits : QuantumBlockEncoding.PrimitiveBasis 9)
  (workspaceClean : bits 8 = 0) :
  have output :=
    QuantumBlockEncoding.Robin.warmRobinFigure4DTSparseAccessBasisEquiv
      bits;
  QuantumBlockEncoding.Robin.warmRobinFigure4AddressBits output =
      QuantumBlockEncoding.Robin.warmRobinSourceDTRow
        (QuantumBlockEncoding.Robin.warmRobinFigure4AddressBits bits)
        (QuantumBlockEncoding.Robin.warmRobinFigure4SystemBits bits) ∧
    QuantumBlockEncoding.Robin.warmRobinFigure4SystemBits output =
        QuantumBlockEncoding.Robin.warmRobinFigure4SystemBits bits ∧
      output 6 = bits 6 ∧ output 7 = bits 7 ∧ output 8 = 0

theorem QuantumBlockEncoding.Robin.warmRobinFigure4DTSparseAccessProgram_cleanAction
  (bits :
    QuantumBlockEncoding.PrimitiveBasis 9)
  (workspaceClean : bits 8 = 0) :
  have output :=
    QuantumBlockEncoding.Robin.warmRobinFigure4DTSparseAccessBasisEquiv
      bits;
  QuantumBlockEncoding.Robin.warmRobinFigure4AddressBits
        output =
      QuantumBlockEncoding.Robin.warmRobinSourceDTRow
        (QuantumBlockEncoding.Robin.warmRobinFigure4AddressBits
          bits)
        (QuantumBlockEncoding.Robin.warmRobinFigure4SystemBits
          bits) ∧
    QuantumBlockEncoding.Robin.warmRobinFigure4SystemBits
          output =
        QuantumBlockEncoding.Robin.warmRobinFigure4SystemBits
          bits ∧
      output 6 = bits 6 ∧
        output 7 = bits 7 ∧ output 8 = 0

Definition10.10.28

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin figure 4 dt sparse access program”.

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. Paper-facing backend models and concrete Robin-boundary example artifacts.

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

Lean code for Definition10.10.28●1 definition

defdefined in QuantumBlockEncoding/Robin/Figure4Primitive.lean

complete

def QuantumBlockEncoding.Robin.warmRobinFigure4DTSparseAccessProgram :
  QuantumBlockEncoding.PrimitiveProgram 9

def QuantumBlockEncoding.Robin.warmRobinFigure4DTSparseAccessProgram :
  QuantumBlockEncoding.PrimitiveProgram 9

Theorem10.10.29

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin figure 4 dt sparse access program eval”; the hypotheses and conclusion in the code panel fix its exact scope.

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

Why it is in this chapter. Paper-facing backend models and concrete Robin-boundary example artifacts.

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

Lean code for Theorem10.10.29●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/Figure4Primitive.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinFigure4DTSparseAccessProgram_eval :
  QuantumBlockEncoding.evalPrimitiveProgram
      QuantumBlockEncoding.Robin.warmRobinFigure4DTSparseAccessProgram =
    QuantumBlockEncoding.Robin.ComplexLCU.equivPermutationMatrix
      QuantumBlockEncoding.Robin.warmRobinFigure4DTSparseAccessBasisEquiv

theorem QuantumBlockEncoding.Robin.warmRobinFigure4DTSparseAccessProgram_eval :
  QuantumBlockEncoding.evalPrimitiveProgram
      QuantumBlockEncoding.Robin.warmRobinFigure4DTSparseAccessProgram =
    QuantumBlockEncoding.Robin.ComplexLCU.equivPermutationMatrix
      QuantumBlockEncoding.Robin.warmRobinFigure4DTSparseAccessBasisEquiv

Definition10.10.30

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin figure 4 d sparse access reversible program”. Convert slot 's' to 's+5', then add the second register modulo eight.

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. Paper-facing backend models and concrete Robin-boundary example artifacts.

Technical source note. Convert slot 's' to 's+5', then add the second register modulo eight.

Declaration kind. def.

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

Lean code for Definition10.10.30●1 definition

defdefined in QuantumBlockEncoding/Robin/Figure4Primitive.lean

complete

def QuantumBlockEncoding.Robin.warmRobinFigure4DSparseAccessReversibleProgram :
  QuantumBlockEncoding.ReversibleProgram 9

def QuantumBlockEncoding.Robin.warmRobinFigure4DSparseAccessReversibleProgram :
  QuantumBlockEncoding.ReversibleProgram 9

Convert slot `s` to `s+5`, then add the second register modulo eight.

Definition10.10.31

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin figure 4 d sparse access basis equiv”.

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. Paper-facing backend models and concrete Robin-boundary example artifacts.

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

Lean code for Definition10.10.31●1 definition

defdefined in QuantumBlockEncoding/Robin/Figure4Primitive.lean

complete

def QuantumBlockEncoding.Robin.warmRobinFigure4DSparseAccessBasisEquiv :
  QuantumBlockEncoding.PrimitiveBasis 9 ≃
    QuantumBlockEncoding.PrimitiveBasis 9

def QuantumBlockEncoding.Robin.warmRobinFigure4DSparseAccessBasisEquiv :
  QuantumBlockEncoding.PrimitiveBasis 9 ≃
    QuantumBlockEncoding.PrimitiveBasis 9

Theorem10.10.32

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin figure 4 d sparse access program clean action”; the hypotheses and conclusion in the code panel fix its exact scope.

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

Why it is in this chapter. Paper-facing backend models and concrete Robin-boundary example artifacts.

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

Lean code for Theorem10.10.32●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/Figure4Primitive.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinFigure4DSparseAccessProgram_cleanAction
  (bits : QuantumBlockEncoding.PrimitiveBasis 9)
  (workspaceClean : bits 8 = 0) :
  have output :=
    QuantumBlockEncoding.Robin.warmRobinFigure4DSparseAccessBasisEquiv
      bits;
  QuantumBlockEncoding.Robin.warmRobinFigure4AddressBits output =
      ⟨(↑(QuantumBlockEncoding.Robin.warmRobinFigure4SystemBits bits) +
            ↑(QuantumBlockEncoding.Robin.warmRobinFigure4DOffset
                (QuantumBlockEncoding.Robin.warmRobinFigure4AddressBits
                  bits))) %
          8,
        ⋯⟩ ∧
    QuantumBlockEncoding.Robin.warmRobinFigure4SystemBits output =
        QuantumBlockEncoding.Robin.warmRobinFigure4SystemBits bits ∧
      output 6 = bits 6 ∧ output 7 = bits 7 ∧ output 8 = 0

theorem QuantumBlockEncoding.Robin.warmRobinFigure4DSparseAccessProgram_cleanAction
  (bits :
    QuantumBlockEncoding.PrimitiveBasis 9)
  (workspaceClean : bits 8 = 0) :
  have output :=
    QuantumBlockEncoding.Robin.warmRobinFigure4DSparseAccessBasisEquiv
      bits;
  QuantumBlockEncoding.Robin.warmRobinFigure4AddressBits
        output =
      ⟨(↑(QuantumBlockEncoding.Robin.warmRobinFigure4SystemBits
                bits) +
            ↑(QuantumBlockEncoding.Robin.warmRobinFigure4DOffset
                (QuantumBlockEncoding.Robin.warmRobinFigure4AddressBits
                  bits))) %
          8,
        ⋯⟩ ∧
    QuantumBlockEncoding.Robin.warmRobinFigure4SystemBits
          output =
        QuantumBlockEncoding.Robin.warmRobinFigure4SystemBits
          bits ∧
      output 6 = bits 6 ∧
        output 7 = bits 7 ∧ output 8 = 0

Definition10.10.33

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin figure 4 d sparse access program”.

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. Paper-facing backend models and concrete Robin-boundary example artifacts.

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

Lean code for Definition10.10.33●1 definition

defdefined in QuantumBlockEncoding/Robin/Figure4Primitive.lean

complete

def QuantumBlockEncoding.Robin.warmRobinFigure4DSparseAccessProgram :
  QuantumBlockEncoding.PrimitiveProgram 9

def QuantumBlockEncoding.Robin.warmRobinFigure4DSparseAccessProgram :
  QuantumBlockEncoding.PrimitiveProgram 9

Theorem10.10.34

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin figure 4 d sparse access program eval”; the hypotheses and conclusion in the code panel fix its exact scope.

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

Why it is in this chapter. Paper-facing backend models and concrete Robin-boundary example artifacts.

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

Lean code for Theorem10.10.34●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/Figure4Primitive.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinFigure4DSparseAccessProgram_eval :
  QuantumBlockEncoding.evalPrimitiveProgram
      QuantumBlockEncoding.Robin.warmRobinFigure4DSparseAccessProgram =
    QuantumBlockEncoding.Robin.ComplexLCU.equivPermutationMatrix
      QuantumBlockEncoding.Robin.warmRobinFigure4DSparseAccessBasisEquiv

theorem QuantumBlockEncoding.Robin.warmRobinFigure4DSparseAccessProgram_eval :
  QuantumBlockEncoding.evalPrimitiveProgram
      QuantumBlockEncoding.Robin.warmRobinFigure4DSparseAccessProgram =
    QuantumBlockEncoding.Robin.ComplexLCU.equivPermutationMatrix
      QuantumBlockEncoding.Robin.warmRobinFigure4DSparseAccessBasisEquiv

Definition10.10.35

uses 0used by 0✓L∃∀N

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

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. Paper-facing backend models and concrete Robin-boundary example artifacts.

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

Lean code for Definition10.10.35●1 definition

defdefined in QuantumBlockEncoding/Robin/Figure4Primitive.lean

complete

def QuantumBlockEncoding.Robin.warmRobinFigure4TransportInput
  (slot column : Fin 8) (coefficient indicator : Fin 2) :
  QuantumBlockEncoding.PrimitiveBasis 9

def QuantumBlockEncoding.Robin.warmRobinFigure4TransportInput
  (slot column : Fin 8)
  (coefficient indicator : Fin 2) :
  QuantumBlockEncoding.PrimitiveBasis 9

Theorem10.10.36

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin figure 4 transport input workspace”; 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. Paper-facing backend models and concrete Robin-boundary example artifacts.

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

Lean code for Theorem10.10.36●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/Figure4Primitive.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinFigure4TransportInput_workspace
  (slot column : Fin 8) (coefficient indicator : Fin 2) :
  QuantumBlockEncoding.Robin.warmRobinFigure4TransportInput slot column
      coefficient indicator 8 =
    0

theorem QuantumBlockEncoding.Robin.warmRobinFigure4TransportInput_workspace
  (slot column : Fin 8)
  (coefficient indicator : Fin 2) :
  QuantumBlockEncoding.Robin.warmRobinFigure4TransportInput
      slot column coefficient indicator
      8 =
    0

Theorem10.10.37

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin figure 4 transport input address”; 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. Paper-facing backend models and concrete Robin-boundary example artifacts.

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

Lean code for Theorem10.10.37●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/Figure4Primitive.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinFigure4TransportInput_address
  (slot column : Fin 8) (coefficient indicator : Fin 2) :
  QuantumBlockEncoding.Robin.warmRobinFigure4AddressBits
      (QuantumBlockEncoding.Robin.warmRobinFigure4TransportInput slot
        column coefficient indicator) =
    slot

theorem QuantumBlockEncoding.Robin.warmRobinFigure4TransportInput_address
  (slot column : Fin 8)
  (coefficient indicator : Fin 2) :
  QuantumBlockEncoding.Robin.warmRobinFigure4AddressBits
      (QuantumBlockEncoding.Robin.warmRobinFigure4TransportInput
        slot column coefficient
        indicator) =
    slot

Theorem10.10.38

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin figure 4 transport input system”; 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. Paper-facing backend models and concrete Robin-boundary example artifacts.

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

Lean code for Theorem10.10.38●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/Figure4Primitive.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinFigure4TransportInput_system
  (slot column : Fin 8) (coefficient indicator : Fin 2) :
  QuantumBlockEncoding.Robin.warmRobinFigure4SystemBits
      (QuantumBlockEncoding.Robin.warmRobinFigure4TransportInput slot
        column coefficient indicator) =
    column

theorem QuantumBlockEncoding.Robin.warmRobinFigure4TransportInput_system
  (slot column : Fin 8)
  (coefficient indicator : Fin 2) :
  QuantumBlockEncoding.Robin.warmRobinFigure4SystemBits
      (QuantumBlockEncoding.Robin.warmRobinFigure4TransportInput
        slot column coefficient
        indicator) =
    column

Theorem10.10.39

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin figure 4 transport input coefficient”; 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. Paper-facing backend models and concrete Robin-boundary example artifacts.

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

Lean code for Theorem10.10.39●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/Figure4Primitive.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinFigure4TransportInput_coefficient
  (slot column : Fin 8) (coefficient indicator : Fin 2) :
  QuantumBlockEncoding.Robin.warmRobinFigure4TransportInput slot column
      coefficient indicator 6 =
    coefficient

theorem QuantumBlockEncoding.Robin.warmRobinFigure4TransportInput_coefficient
  (slot column : Fin 8)
  (coefficient indicator : Fin 2) :
  QuantumBlockEncoding.Robin.warmRobinFigure4TransportInput
      slot column coefficient indicator
      6 =
    coefficient

Theorem10.10.40

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin figure 4 transport input indicator”; 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. Paper-facing backend models and concrete Robin-boundary example artifacts.

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

Lean code for Theorem10.10.40●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/Figure4Primitive.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinFigure4TransportInput_indicator
  (slot column : Fin 8) (coefficient indicator : Fin 2) :
  QuantumBlockEncoding.Robin.warmRobinFigure4TransportInput slot column
      coefficient indicator 7 =
    indicator

theorem QuantumBlockEncoding.Robin.warmRobinFigure4TransportInput_indicator
  (slot column : Fin 8)
  (coefficient indicator : Fin 2) :
  QuantumBlockEncoding.Robin.warmRobinFigure4TransportInput
      slot column coefficient indicator
      7 =
    indicator

Definition10.10.41

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin figure 4 register swap reversible program”.

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. Paper-facing backend models and concrete Robin-boundary example artifacts.

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

Lean code for Definition10.10.41●1 definition

defdefined in QuantumBlockEncoding/Robin/Figure4Primitive.lean

complete

def QuantumBlockEncoding.Robin.warmRobinFigure4RegisterSwapReversibleProgram :
  QuantumBlockEncoding.ReversibleProgram 9

def QuantumBlockEncoding.Robin.warmRobinFigure4RegisterSwapReversibleProgram :
  QuantumBlockEncoding.ReversibleProgram 9

Definition10.10.42

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin figure 4 register swap full basis equiv”.

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. Paper-facing backend models and concrete Robin-boundary example artifacts.

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

Lean code for Definition10.10.42●1 definition

defdefined in QuantumBlockEncoding/Robin/Figure4Primitive.lean

complete

def QuantumBlockEncoding.Robin.warmRobinFigure4RegisterSwapFullBasisEquiv :
  QuantumBlockEncoding.PrimitiveBasis 9 ≃
    QuantumBlockEncoding.PrimitiveBasis 9

def QuantumBlockEncoding.Robin.warmRobinFigure4RegisterSwapFullBasisEquiv :
  QuantumBlockEncoding.PrimitiveBasis 9 ≃
    QuantumBlockEncoding.PrimitiveBasis 9

Theorem10.10.43

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin figure 4 address bits decode”; 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. Paper-facing backend models and concrete Robin-boundary example artifacts.

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

Lean code for Theorem10.10.43●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/Figure4Primitive.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinFigure4AddressBits_decode
  (bits : QuantumBlockEncoding.PrimitiveBasis 9) (wire : Fin 3) :
  QuantumBlockEncoding.primitiveBits3LE
      (QuantumBlockEncoding.Robin.warmRobinFigure4AddressBits bits)
      wire =
    bits ⟨↑wire, ⋯⟩

theorem QuantumBlockEncoding.Robin.warmRobinFigure4AddressBits_decode
  (bits :
    QuantumBlockEncoding.PrimitiveBasis 9)
  (wire : Fin 3) :
  QuantumBlockEncoding.primitiveBits3LE
      (QuantumBlockEncoding.Robin.warmRobinFigure4AddressBits
        bits)
      wire =
    bits ⟨↑wire, ⋯⟩

Theorem10.10.44

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin figure 4 system bits decode”; 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. Paper-facing backend models and concrete Robin-boundary example artifacts.

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

Lean code for Theorem10.10.44●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/Figure4Primitive.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinFigure4SystemBits_decode
  (bits : QuantumBlockEncoding.PrimitiveBasis 9) (wire : Fin 3) :
  QuantumBlockEncoding.primitiveBits3LE
      (QuantumBlockEncoding.Robin.warmRobinFigure4SystemBits bits)
      wire =
    bits ⟨↑wire + 3, ⋯⟩

theorem QuantumBlockEncoding.Robin.warmRobinFigure4SystemBits_decode
  (bits :
    QuantumBlockEncoding.PrimitiveBasis 9)
  (wire : Fin 3) :
  QuantumBlockEncoding.primitiveBits3LE
      (QuantumBlockEncoding.Robin.warmRobinFigure4SystemBits
        bits)
      wire =
    bits ⟨↑wire + 3, ⋯⟩

Theorem10.10.45

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin figure 4 basis ext”; 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. Paper-facing backend models and concrete Robin-boundary example artifacts.

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

Lean code for Theorem10.10.45●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/Figure4Primitive.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinFigure4Basis_ext
  (left right : QuantumBlockEncoding.PrimitiveBasis 9)
  (address :
    QuantumBlockEncoding.Robin.warmRobinFigure4AddressBits left =
      QuantumBlockEncoding.Robin.warmRobinFigure4AddressBits right)
  (system :
    QuantumBlockEncoding.Robin.warmRobinFigure4SystemBits left =
      QuantumBlockEncoding.Robin.warmRobinFigure4SystemBits right)
  (coefficient : left 6 = right 6) (indicator : left 7 = right 7)
  (workspace : left 8 = right 8) : left = right

theorem QuantumBlockEncoding.Robin.warmRobinFigure4Basis_ext
  (left right :
    QuantumBlockEncoding.PrimitiveBasis 9)
  (address :
    QuantumBlockEncoding.Robin.warmRobinFigure4AddressBits
        left =
      QuantumBlockEncoding.Robin.warmRobinFigure4AddressBits
        right)
  (system :
    QuantumBlockEncoding.Robin.warmRobinFigure4SystemBits
        left =
      QuantumBlockEncoding.Robin.warmRobinFigure4SystemBits
        right)
  (coefficient : left 6 = right 6)
  (indicator : left 7 = right 7)
  (workspace : left 8 = right 8) :
  left = right

Theorem10.10.46

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin figure 4 dt sparse access transport input”; 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. Paper-facing backend models and concrete Robin-boundary example artifacts.

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

Lean code for Theorem10.10.46●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/Figure4Primitive.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinFigure4DTSparseAccess_transportInput
  (slot column : Fin 8) (coefficient indicator : Fin 2) :
  QuantumBlockEncoding.Robin.warmRobinFigure4DTSparseAccessBasisEquiv
      (QuantumBlockEncoding.Robin.warmRobinFigure4TransportInput slot
        column coefficient indicator) =
    QuantumBlockEncoding.Robin.warmRobinFigure4TransportInput
      (QuantumBlockEncoding.Robin.warmRobinSourceDTRow slot column)
      column coefficient indicator

theorem QuantumBlockEncoding.Robin.warmRobinFigure4DTSparseAccess_transportInput
  (slot column : Fin 8)
  (coefficient indicator : Fin 2) :
  QuantumBlockEncoding.Robin.warmRobinFigure4DTSparseAccessBasisEquiv
      (QuantumBlockEncoding.Robin.warmRobinFigure4TransportInput
        slot column coefficient
        indicator) =
    QuantumBlockEncoding.Robin.warmRobinFigure4TransportInput
      (QuantumBlockEncoding.Robin.warmRobinSourceDTRow
        slot column)
      column coefficient indicator

Theorem10.10.47

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin figure 4 register swap transport input”; 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. Paper-facing backend models and concrete Robin-boundary example artifacts.

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

Lean code for Theorem10.10.47●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/Figure4Primitive.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinFigure4RegisterSwap_transportInput
  (left right : Fin 8) (coefficient indicator : Fin 2) :
  QuantumBlockEncoding.Robin.warmRobinFigure4RegisterSwapFullBasisEquiv
      (QuantumBlockEncoding.Robin.warmRobinFigure4TransportInput left
        right coefficient indicator) =
    QuantumBlockEncoding.Robin.warmRobinFigure4TransportInput right left
      coefficient indicator

theorem QuantumBlockEncoding.Robin.warmRobinFigure4RegisterSwap_transportInput
  (left right : Fin 8)
  (coefficient indicator : Fin 2) :
  QuantumBlockEncoding.Robin.warmRobinFigure4RegisterSwapFullBasisEquiv
      (QuantumBlockEncoding.Robin.warmRobinFigure4TransportInput
        left right coefficient
        indicator) =
    QuantumBlockEncoding.Robin.warmRobinFigure4TransportInput
      right left coefficient indicator

Theorem10.10.48

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin figure 4 d offset after dt”; 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. Paper-facing backend models and concrete Robin-boundary example artifacts.

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

Lean code for Theorem10.10.48●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/Figure4Primitive.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinFigure4DOffset_after_DT
  (slot column : Fin 8) :
  ⟨(↑(QuantumBlockEncoding.Robin.warmRobinSourceDTRow slot column) +
          ↑(QuantumBlockEncoding.Robin.warmRobinFigure4DOffset slot)) %
        8,
      ⋯⟩ =
    column

theorem QuantumBlockEncoding.Robin.warmRobinFigure4DOffset_after_DT
  (slot column : Fin 8) :
  ⟨(↑(QuantumBlockEncoding.Robin.warmRobinSourceDTRow
              slot column) +
          ↑(QuantumBlockEncoding.Robin.warmRobinFigure4DOffset
              slot)) %
        8,
      ⋯⟩ =
    column

Theorem10.10.49

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin figure 4 d sparse access transport input”; 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. Paper-facing backend models and concrete Robin-boundary example artifacts.

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

Lean code for Theorem10.10.49●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/Figure4Primitive.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinFigure4DSparseAccess_transportInput
  (slot system : Fin 8) (coefficient indicator : Fin 2) :
  QuantumBlockEncoding.Robin.warmRobinFigure4DSparseAccessBasisEquiv
      (QuantumBlockEncoding.Robin.warmRobinFigure4TransportInput slot
        system coefficient indicator) =
    QuantumBlockEncoding.Robin.warmRobinFigure4TransportInput
      ⟨(↑system +
            ↑(QuantumBlockEncoding.Robin.warmRobinFigure4DOffset
                slot)) %
          8,
        ⋯⟩
      system coefficient indicator

theorem QuantumBlockEncoding.Robin.warmRobinFigure4DSparseAccess_transportInput
  (slot system : Fin 8)
  (coefficient indicator : Fin 2) :
  QuantumBlockEncoding.Robin.warmRobinFigure4DSparseAccessBasisEquiv
      (QuantumBlockEncoding.Robin.warmRobinFigure4TransportInput
        slot system coefficient
        indicator) =
    QuantumBlockEncoding.Robin.warmRobinFigure4TransportInput
      ⟨(↑system +
            ↑(QuantumBlockEncoding.Robin.warmRobinFigure4DOffset
                slot)) %
          8,
        ⋯⟩
      system coefficient indicator

Theorem10.10.50

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin figure 4 transported post swap cleanup”; the hypotheses and conclusion in the code panel fix its exact scope. Central cleanup root: D-transpose access, register transport, and inverse D access restore the original slot while leaving the transported row in the system register and returning 'q8' to 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. Paper-facing backend models and concrete Robin-boundary example artifacts.

Technical source note. Central cleanup root: D-transpose access, register transport, and inverse D access restore the original slot while leaving the transported row in the system register and returning 'q8' to zero.

Declaration kind. theorem.

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

Lean code for Theorem10.10.50●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/Figure4Primitive.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinFigure4TransportedPostSwapCleanup
  (slot column : Fin 8) (coefficient indicator : Fin 2) :
  have afterDT :=
    QuantumBlockEncoding.Robin.warmRobinFigure4DTSparseAccessBasisEquiv
      (QuantumBlockEncoding.Robin.warmRobinFigure4TransportInput slot
        column coefficient indicator);
  have afterSwap :=
    QuantumBlockEncoding.Robin.warmRobinFigure4RegisterSwapFullBasisEquiv
      afterDT;
  have output :=
    QuantumBlockEncoding.Robin.warmRobinFigure4DSparseAccessBasisEquiv.symm
      afterSwap;
  QuantumBlockEncoding.Robin.warmRobinFigure4AddressBits output = slot ∧
    QuantumBlockEncoding.Robin.warmRobinFigure4SystemBits output =
        QuantumBlockEncoding.Robin.warmRobinSourceDTRow slot column ∧
      output 6 = coefficient ∧ output 7 = indicator ∧ output 8 = 0

theorem QuantumBlockEncoding.Robin.warmRobinFigure4TransportedPostSwapCleanup
  (slot column : Fin 8)
  (coefficient indicator : Fin 2) :
  have afterDT :=
    QuantumBlockEncoding.Robin.warmRobinFigure4DTSparseAccessBasisEquiv
      (QuantumBlockEncoding.Robin.warmRobinFigure4TransportInput
        slot column coefficient
        indicator);
  have afterSwap :=
    QuantumBlockEncoding.Robin.warmRobinFigure4RegisterSwapFullBasisEquiv
      afterDT;
  have output :=
    QuantumBlockEncoding.Robin.warmRobinFigure4DSparseAccessBasisEquiv.symm
      afterSwap;
  QuantumBlockEncoding.Robin.warmRobinFigure4AddressBits
        output =
      slot ∧
    QuantumBlockEncoding.Robin.warmRobinFigure4SystemBits
          output =
        QuantumBlockEncoding.Robin.warmRobinSourceDTRow
          slot column ∧
      output 6 = coefficient ∧
        output 7 = indicator ∧
          output 8 = 0

Central cleanup root: D-transpose access, register transport, and inverse D
access restore the original slot while leaving the transported row in the
system register and returning `q8` to zero.

Theorem10.10.51

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin figure 4 sparse workspace clean”; 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. Paper-facing backend models and concrete Robin-boundary example artifacts.

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

Lean code for Theorem10.10.51●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/Figure4Primitive.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinFigure4SparseWorkspaceClean
  (slot column : Fin 8) (coefficient indicator : Fin 2) :
  have afterDT :=
    QuantumBlockEncoding.Robin.warmRobinFigure4DTSparseAccessBasisEquiv
      (QuantumBlockEncoding.Robin.warmRobinFigure4TransportInput slot
        column coefficient indicator);
  have afterSwap :=
    QuantumBlockEncoding.Robin.warmRobinFigure4RegisterSwapFullBasisEquiv
      afterDT;
  QuantumBlockEncoding.Robin.warmRobinFigure4DSparseAccessBasisEquiv.symm
      afterSwap 8 =
    0

theorem QuantumBlockEncoding.Robin.warmRobinFigure4SparseWorkspaceClean
  (slot column : Fin 8)
  (coefficient indicator : Fin 2) :
  have afterDT :=
    QuantumBlockEncoding.Robin.warmRobinFigure4DTSparseAccessBasisEquiv
      (QuantumBlockEncoding.Robin.warmRobinFigure4TransportInput
        slot column coefficient
        indicator);
  have afterSwap :=
    QuantumBlockEncoding.Robin.warmRobinFigure4RegisterSwapFullBasisEquiv
      afterDT;
  QuantumBlockEncoding.Robin.warmRobinFigure4DSparseAccessBasisEquiv.symm
      afterSwap 8 =
    0

Definition10.10.52

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin figure 4 former open primitive contracts”. Historical pre-T3 audit list.

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. Paper-facing backend models and concrete Robin-boundary example artifacts.

Technical source note. Historical pre-T3 audit list. 'Figure4T3.lean' now closes these obligations for fixed N=8, homogeneous f=1, and the standard-RY-corrected executable convention.

Declaration kind. def.

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

Lean code for Definition10.10.52●1 definition

defdefined in QuantumBlockEncoding/Robin/Figure4Primitive.lean

complete

def QuantumBlockEncoding.Robin.warmRobinFigure4FormerOpenPrimitiveContracts :
  List String

def QuantumBlockEncoding.Robin.warmRobinFigure4FormerOpenPrimitiveContracts :
  List String

Historical pre-T3 audit list. `Figure4T3.lean` now closes these obligations
for fixed N=8, homogeneous f=1, and the standard-RY-corrected executable
convention.

Definition10.10.53

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin figure 4 open primitive contracts”. No primitive obligations remain open for the fixed-N8 Figure-4 route.

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. Paper-facing backend models and concrete Robin-boundary example artifacts.

Technical source note. No primitive obligations remain open for the fixed-N8 Figure-4 route.

Declaration kind. def.

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

Lean code for Definition10.10.53●1 definition

defdefined in QuantumBlockEncoding/Robin/Figure4Primitive.lean

complete

def QuantumBlockEncoding.Robin.warmRobinFigure4OpenPrimitiveContracts :
  List String

def QuantumBlockEncoding.Robin.warmRobinFigure4OpenPrimitiveContracts :
  List String

No primitive obligations remain open for the fixed-N8 Figure-4 route.

Theorem10.10.54

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin figure 4 open primitive contracts eq nil”; 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. Paper-facing backend models and concrete Robin-boundary example artifacts.

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

Lean code for Theorem10.10.54●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/Figure4Primitive.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinFigure4OpenPrimitiveContracts_eq_nil :
  QuantumBlockEncoding.Robin.warmRobinFigure4OpenPrimitiveContracts = []

theorem QuantumBlockEncoding.Robin.warmRobinFigure4OpenPrimitiveContracts_eq_nil :
  QuantumBlockEncoding.Robin.warmRobinFigure4OpenPrimitiveContracts =
    []