PaperSevenPrimitive.lean🔗

29 explicit public declarations, in source order.

Definition10.20.1

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin paper seven select reversible program”. Physical SELECT in the declared eight-wire order.

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. Physical SELECT in the declared eight-wire order. CCX remains only in the proof IR and is compiled away by 'compileReversibleProgram'.

Declaration kind. def.

Source: QuantumBlockEncoding/Robin/PaperSevenPrimitive.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.20.1●1 definition

defdefined in QuantumBlockEncoding/Robin/PaperSevenPrimitive.lean

complete

def QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectReversibleProgram :
  QuantumBlockEncoding.ReversibleProgram 8

def QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectReversibleProgram :
  QuantumBlockEncoding.ReversibleProgram 8

Physical SELECT in the declared eight-wire order.  CCX remains only in
the proof IR and is compiled away by `compileReversibleProgram`.

Definition10.20.2

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin paper seven select 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/PaperSevenPrimitive.lean:34. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition10.20.2●1 definition

defdefined in QuantumBlockEncoding/Robin/PaperSevenPrimitive.lean

complete

def QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectBasisEquiv :
  QuantumBlockEncoding.PrimitiveBasis 8 ≃
    QuantumBlockEncoding.PrimitiveBasis 8

def QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectBasisEquiv :
  QuantumBlockEncoding.PrimitiveBasis 8 ≃
    QuantumBlockEncoding.PrimitiveBasis 8

Definition10.20.3

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin paper seven 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/PaperSevenPrimitive.lean:38. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition10.20.3●1 definition

defdefined in QuantumBlockEncoding/Robin/PaperSevenPrimitive.lean

complete

def QuantumBlockEncoding.Robin.warmRobinPaperSevenSystemBits
  (bits : QuantumBlockEncoding.PrimitiveBasis 8) : Fin 8

def QuantumBlockEncoding.Robin.warmRobinPaperSevenSystemBits
  (bits :
    QuantumBlockEncoding.PrimitiveBasis
      8) :
  Fin 8

Definition10.20.4

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin paper seven selector 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/PaperSevenPrimitive.lean:41. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition10.20.4●1 definition

defdefined in QuantumBlockEncoding/Robin/PaperSevenPrimitive.lean

complete

def QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectorBits
  (bits : QuantumBlockEncoding.PrimitiveBasis 8) : Fin 8

def QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectorBits
  (bits :
    QuantumBlockEncoding.PrimitiveBasis
      8) :
  Fin 8

Theorem10.20.5

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin paper seven select program clean action”; the hypotheses and conclusion in the code panel fix its exact scope. Clean-workspace action of the source SELECT.

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. Clean-workspace action of the source SELECT.

Declaration kind. theorem.

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

Lean code for Theorem10.20.5●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/PaperSevenPrimitive.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectProgram_cleanAction
  (bits : QuantumBlockEncoding.PrimitiveBasis 8)
  (workClean : bits 7 = 0) :
  have output :=
    QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectBasisEquiv bits;
  QuantumBlockEncoding.Robin.warmRobinPaperSevenSystemBits output =
      QuantumBlockEncoding.Robin.warmRobinSourceDTRow
        (QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectorBits
          bits)
        (QuantumBlockEncoding.Robin.warmRobinPaperSevenSystemBits
          bits) ∧
    QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectorBits output =
        QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectorBits
          bits ∧
      output 6 = bits 6 ∧ output 7 = 0

theorem QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectProgram_cleanAction
  (bits :
    QuantumBlockEncoding.PrimitiveBasis 8)
  (workClean : bits 7 = 0) :
  have output :=
    QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectBasisEquiv
      bits;
  QuantumBlockEncoding.Robin.warmRobinPaperSevenSystemBits
        output =
      QuantumBlockEncoding.Robin.warmRobinSourceDTRow
        (QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectorBits
          bits)
        (QuantumBlockEncoding.Robin.warmRobinPaperSevenSystemBits
          bits) ∧
    QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectorBits
          output =
        QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectorBits
          bits ∧
      output 6 = bits 6 ∧ output 7 = 0

Clean-workspace action of the source SELECT.

Theorem10.20.6

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin paper seven select 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/PaperSevenPrimitive.lean:56. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.20.6●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/PaperSevenPrimitive.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectProgram_workspaceClean
  (bits : QuantumBlockEncoding.PrimitiveBasis 8)
  (workClean : bits 7 = 0) :
  QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectBasisEquiv bits
      7 =
    0

theorem QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectProgram_workspaceClean
  (bits :
    QuantumBlockEncoding.PrimitiveBasis 8)
  (workClean : bits 7 = 0) :
  QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectBasisEquiv
      bits 7 =
    0

Definition10.20.7

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin paper seven select 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/PaperSevenPrimitive.lean:61. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition10.20.7●1 definition

defdefined in QuantumBlockEncoding/Robin/PaperSevenPrimitive.lean

complete

def QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectProgram :
  QuantumBlockEncoding.PrimitiveProgram 8

def QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectProgram :
  QuantumBlockEncoding.PrimitiveProgram 8

Theorem10.20.8

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin paper seven select program eval”; the hypotheses and conclusion in the code panel fix its exact scope. Exact primitive matrix for source SELECT, including its exact compiler phase.

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. Exact primitive matrix for source SELECT, including its exact compiler phase.

Declaration kind. theorem.

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

Lean code for Theorem10.20.8●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/PaperSevenPrimitive.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectProgram_eval :
  QuantumBlockEncoding.evalPrimitiveProgram
      QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectProgram =
    QuantumBlockEncoding.Robin.ComplexLCU.equivPermutationMatrix
      QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectBasisEquiv

theorem QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectProgram_eval :
  QuantumBlockEncoding.evalPrimitiveProgram
      QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectProgram =
    QuantumBlockEncoding.Robin.ComplexLCU.equivPermutationMatrix
      QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectBasisEquiv

Exact primitive matrix for source SELECT, including its exact compiler
phase.

Theorem10.20.9

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin paper seven select 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/PaperSevenPrimitive.lean:72. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.20.9●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/PaperSevenPrimitive.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectProgram_noOracleCalls :
  QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectProgram.resource.oracleCalls =
    0

theorem QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectProgram_noOracleCalls :
  QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectProgram.resource.oracleCalls =
    0

Definition10.20.10

uses 0used by 0✓L∃∀N

Plain-English reading. This abbreviation gives a shorter name to the type or expression used for “warm robin paper seven full system”.

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

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

Lean code for Definition10.20.10●1 definition

abbrevdefined in QuantumBlockEncoding/Robin/PaperSevenPrimitive.lean

complete

abbrev QuantumBlockEncoding.Robin.WarmRobinPaperSevenFullSystem : Type

abbrev QuantumBlockEncoding.Robin.WarmRobinPaperSevenFullSystem :
  Type

Definition10.20.11

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin paper seven encode bits”. Encode the declared register product into the physical wire order.

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. Encode the declared register product into the physical wire order.

Declaration kind. def.

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

Lean code for Definition10.20.11●1 definition

defdefined in QuantumBlockEncoding/Robin/PaperSevenPrimitive.lean

complete

def QuantumBlockEncoding.Robin.warmRobinPaperSevenEncodeBits
  (coefficient : Fin 2) (selector : Fin 8)
  (system : QuantumBlockEncoding.Robin.WarmRobinPaperSevenFullSystem) :
  QuantumBlockEncoding.PrimitiveBasis 8

def QuantumBlockEncoding.Robin.warmRobinPaperSevenEncodeBits
  (coefficient : Fin 2) (selector : Fin 8)
  (system :
    QuantumBlockEncoding.Robin.WarmRobinPaperSevenFullSystem) :
  QuantumBlockEncoding.PrimitiveBasis 8

Encode the declared register product into the physical wire order.

Definition10.20.12

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin paper seven bits 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. 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/PaperSevenPrimitive.lean:91. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition10.20.12●1 definition

defdefined in QuantumBlockEncoding/Robin/PaperSevenPrimitive.lean

complete

def QuantumBlockEncoding.Robin.warmRobinPaperSevenBitsIndex
  (bits : QuantumBlockEncoding.PrimitiveBasis 8) :
  QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex (Fin 2) (Fin 8)
    QuantumBlockEncoding.Robin.WarmRobinPaperSevenFullSystem

def QuantumBlockEncoding.Robin.warmRobinPaperSevenBitsIndex
  (bits :
    QuantumBlockEncoding.PrimitiveBasis
      8) :
  QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex
    (Fin 2) (Fin 8)
    QuantumBlockEncoding.Robin.WarmRobinPaperSevenFullSystem

Theorem10.20.13

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.20.13●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/PaperSevenPrimitive.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinPaperSevenBitsIndex_bijective :
  Function.Bijective
    QuantumBlockEncoding.Robin.warmRobinPaperSevenBitsIndex

theorem QuantumBlockEncoding.Robin.warmRobinPaperSevenBitsIndex_bijective :
  Function.Bijective
    QuantumBlockEncoding.Robin.warmRobinPaperSevenBitsIndex

Definition10.20.14

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin paper seven bits 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/PaperSevenPrimitive.lean:100. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition10.20.14●1 definition

defdefined in QuantumBlockEncoding/Robin/PaperSevenPrimitive.lean

complete

def QuantumBlockEncoding.Robin.warmRobinPaperSevenBitsEquiv :
  QuantumBlockEncoding.PrimitiveBasis 8 ≃
    QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex (Fin 2) (Fin 8)
      QuantumBlockEncoding.Robin.WarmRobinPaperSevenFullSystem

def QuantumBlockEncoding.Robin.warmRobinPaperSevenBitsEquiv :
  QuantumBlockEncoding.PrimitiveBasis 8 ≃
    QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex
      (Fin 2) (Fin 8)
      QuantumBlockEncoding.Robin.WarmRobinPaperSevenFullSystem

Theorem10.20.15

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin paper seven bits equiv 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. 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/PaperSevenPrimitive.lean:106. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.20.15●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/PaperSevenPrimitive.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinPaperSevenBitsEquiv_apply
  (bits : QuantumBlockEncoding.PrimitiveBasis 8) :
  QuantumBlockEncoding.Robin.warmRobinPaperSevenBitsEquiv bits =
    QuantumBlockEncoding.Robin.warmRobinPaperSevenBitsIndex bits

theorem QuantumBlockEncoding.Robin.warmRobinPaperSevenBitsEquiv_apply
  (bits :
    QuantumBlockEncoding.PrimitiveBasis
      8) :
  QuantumBlockEncoding.Robin.warmRobinPaperSevenBitsEquiv
      bits =
    QuantumBlockEncoding.Robin.warmRobinPaperSevenBitsIndex
      bits

Definition10.20.16

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin bit xor”.

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

Lean code for Definition10.20.16●1 definition

defdefined in QuantumBlockEncoding/Robin/PaperSevenPrimitive.lean

complete

def QuantumBlockEncoding.Robin.warmRobinBitXor (left right : Fin 2) : Fin 2

def QuantumBlockEncoding.Robin.warmRobinBitXor
  (left right : Fin 2) : Fin 2

Definition10.20.17

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin bit and”.

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

Lean code for Definition10.20.17●1 definition

defdefined in QuantumBlockEncoding/Robin/PaperSevenPrimitive.lean

complete

def QuantumBlockEncoding.Robin.warmRobinBitAnd (left right : Fin 2) : Fin 2

def QuantumBlockEncoding.Robin.warmRobinBitAnd
  (left right : Fin 2) : Fin 2

Definition10.20.18

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin paper seven full system perm”. Explicit full-space action of the reversible adder.

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. Explicit full-space action of the reversible adder. On dirty workspace this records the actual extension instead of claiming tensor identity.

Declaration kind. def.

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

Lean code for Definition10.20.18●1 definition

defdefined in QuantumBlockEncoding/Robin/PaperSevenPrimitive.lean

complete

def QuantumBlockEncoding.Robin.warmRobinPaperSevenFullSystemPerm
  (slot : Fin 8)
  (system : QuantumBlockEncoding.Robin.WarmRobinPaperSevenFullSystem) :
  QuantumBlockEncoding.Robin.WarmRobinPaperSevenFullSystem

def QuantumBlockEncoding.Robin.warmRobinPaperSevenFullSystemPerm
  (slot : Fin 8)
  (system :
    QuantumBlockEncoding.Robin.WarmRobinPaperSevenFullSystem) :
  QuantumBlockEncoding.Robin.WarmRobinPaperSevenFullSystem

Explicit full-space action of the reversible adder.  On dirty workspace
this records the actual extension instead of claiming tensor identity.

Theorem10.20.19

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin paper seven full system perm bijective”; 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/PaperSevenPrimitive.lean:133. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.20.19●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/PaperSevenPrimitive.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinPaperSevenFullSystemPerm_bijective
  (slot : Fin 8) :
  Function.Bijective
    (QuantumBlockEncoding.Robin.warmRobinPaperSevenFullSystemPerm slot)

theorem QuantumBlockEncoding.Robin.warmRobinPaperSevenFullSystemPerm_bijective
  (slot : Fin 8) :
  Function.Bijective
    (QuantumBlockEncoding.Robin.warmRobinPaperSevenFullSystemPerm
      slot)

Definition10.20.20

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin paper seven full system 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/PaperSevenPrimitive.lean:137. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition10.20.20●1 definition

defdefined in QuantumBlockEncoding/Robin/PaperSevenPrimitive.lean

complete

def QuantumBlockEncoding.Robin.warmRobinPaperSevenFullSystemEquiv
  (slot : Fin 8) :
  QuantumBlockEncoding.Robin.WarmRobinPaperSevenFullSystem ≃
    QuantumBlockEncoding.Robin.WarmRobinPaperSevenFullSystem

def QuantumBlockEncoding.Robin.warmRobinPaperSevenFullSystemEquiv
  (slot : Fin 8) :
  QuantumBlockEncoding.Robin.WarmRobinPaperSevenFullSystem ≃
    QuantumBlockEncoding.Robin.WarmRobinPaperSevenFullSystem

Theorem10.20.21

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin paper seven full system equiv 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. 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/PaperSevenPrimitive.lean:142. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.20.21●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/PaperSevenPrimitive.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinPaperSevenFullSystemEquiv_apply
  (slot : Fin 8)
  (system : QuantumBlockEncoding.Robin.WarmRobinPaperSevenFullSystem) :
  (QuantumBlockEncoding.Robin.warmRobinPaperSevenFullSystemEquiv slot)
      system =
    QuantumBlockEncoding.Robin.warmRobinPaperSevenFullSystemPerm slot
      system

theorem QuantumBlockEncoding.Robin.warmRobinPaperSevenFullSystemEquiv_apply
  (slot : Fin 8)
  (system :
    QuantumBlockEncoding.Robin.WarmRobinPaperSevenFullSystem) :
  (QuantumBlockEncoding.Robin.warmRobinPaperSevenFullSystemEquiv
        slot)
      system =
    QuantumBlockEncoding.Robin.warmRobinPaperSevenFullSystemPerm
      slot system

Theorem10.20.22

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin paper seven full system equiv 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/PaperSevenPrimitive.lean:147. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.20.22●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/PaperSevenPrimitive.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinPaperSevenFullSystemEquiv_clean
  (slot column : Fin 8) :
  (QuantumBlockEncoding.Robin.warmRobinPaperSevenFullSystemEquiv slot)
      (column, 0) =
    (QuantumBlockEncoding.Robin.warmRobinSourceDTRow slot column, 0)

theorem QuantumBlockEncoding.Robin.warmRobinPaperSevenFullSystemEquiv_clean
  (slot column : Fin 8) :
  (QuantumBlockEncoding.Robin.warmRobinPaperSevenFullSystemEquiv
        slot)
      (column, 0) =
    (QuantumBlockEncoding.Robin.warmRobinSourceDTRow
        slot column,
      0)

Theorem10.20.23

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin paper seven select basis action index”; 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/PaperSevenPrimitive.lean:154. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.20.23●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/PaperSevenPrimitive.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectBasisAction_index
  (bits : QuantumBlockEncoding.PrimitiveBasis 8) :
  QuantumBlockEncoding.Robin.warmRobinPaperSevenBitsEquiv
      (QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectBasisEquiv
        bits) =
    (QuantumBlockEncoding.Robin.ComplexLCU.controlledSystemEquiv
        QuantumBlockEncoding.Robin.warmRobinPaperSevenFullSystemEquiv)
      (QuantumBlockEncoding.Robin.warmRobinPaperSevenBitsEquiv bits)

theorem QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectBasisAction_index
  (bits :
    QuantumBlockEncoding.PrimitiveBasis
      8) :
  QuantumBlockEncoding.Robin.warmRobinPaperSevenBitsEquiv
      (QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectBasisEquiv
        bits) =
    (QuantumBlockEncoding.Robin.ComplexLCU.controlledSystemEquiv
        QuantumBlockEncoding.Robin.warmRobinPaperSevenFullSystemEquiv)
      (QuantumBlockEncoding.Robin.warmRobinPaperSevenBitsEquiv
        bits)

Theorem10.20.24

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin paper seven select program eval reindexed”; 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/PaperSevenPrimitive.lean:173. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.20.24●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/PaperSevenPrimitive.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectProgram_eval_reindexed :
  QuantumBlockEncoding.evalPrimitiveProgram
      QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectProgram =
    (Matrix.reindexAlgEquiv ℂ ℂ
        QuantumBlockEncoding.Robin.warmRobinPaperSevenBitsEquiv.symm)
      (QuantumBlockEncoding.Robin.ComplexLCU.selectLift
        QuantumBlockEncoding.Robin.warmRobinPaperSevenFullSystemEquiv)

theorem QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectProgram_eval_reindexed :
  QuantumBlockEncoding.evalPrimitiveProgram
      QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectProgram =
    (Matrix.reindexAlgEquiv ℂ ℂ
        QuantumBlockEncoding.Robin.warmRobinPaperSevenBitsEquiv.symm)
      (QuantumBlockEncoding.Robin.ComplexLCU.selectLift
        QuantumBlockEncoding.Robin.warmRobinPaperSevenFullSystemEquiv)

Definition10.20.25

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin paper seven workspace rotation”.

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

Lean code for Definition10.20.25●1 definition

defdefined in QuantumBlockEncoding/Robin/PaperSevenPrimitive.lean

complete

def QuantumBlockEncoding.Robin.warmRobinPaperSevenWorkspaceRotation
  (slot : Fin 8)
  (system : QuantumBlockEncoding.Robin.WarmRobinPaperSevenFullSystem) :
  Matrix (Fin 2) (Fin 2) ℂ

def QuantumBlockEncoding.Robin.warmRobinPaperSevenWorkspaceRotation
  (slot : Fin 8)
  (system :
    QuantumBlockEncoding.Robin.WarmRobinPaperSevenFullSystem) :
  Matrix (Fin 2) (Fin 2) ℂ

Theorem10.20.26

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin paper seven workspace rotation unitary”; 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/PaperSevenPrimitive.lean:201. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.20.26●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/PaperSevenPrimitive.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinPaperSevenWorkspaceRotation_unitary
  (slot : Fin 8)
  (system : QuantumBlockEncoding.Robin.WarmRobinPaperSevenFullSystem) :
  QuantumBlockEncoding.Robin.warmRobinPaperSevenWorkspaceRotation slot
      system ∈
    Matrix.unitaryGroup (Fin 2) ℂ

theorem QuantumBlockEncoding.Robin.warmRobinPaperSevenWorkspaceRotation_unitary
  (slot : Fin 8)
  (system :
    QuantumBlockEncoding.Robin.WarmRobinPaperSevenFullSystem) :
  QuantumBlockEncoding.Robin.warmRobinPaperSevenWorkspaceRotation
      slot system ∈
    Matrix.unitaryGroup (Fin 2) ℂ

Definition10.20.27

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin paper seven workspace logical unitary”.

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

Lean code for Definition10.20.27●1 definition

defdefined in QuantumBlockEncoding/Robin/PaperSevenPrimitive.lean

complete

def QuantumBlockEncoding.Robin.warmRobinPaperSevenWorkspaceLogicalUnitary :
  Matrix
    (QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex (Fin 2) (Fin 8)
      QuantumBlockEncoding.Robin.WarmRobinPaperSevenFullSystem)
    (QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex (Fin 2) (Fin 8)
      QuantumBlockEncoding.Robin.WarmRobinPaperSevenFullSystem)
    ℂ

def QuantumBlockEncoding.Robin.warmRobinPaperSevenWorkspaceLogicalUnitary :
  Matrix
    (QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex
      (Fin 2) (Fin 8)
      QuantumBlockEncoding.Robin.WarmRobinPaperSevenFullSystem)
    (QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex
      (Fin 2) (Fin 8)
      QuantumBlockEncoding.Robin.WarmRobinPaperSevenFullSystem)
    ℂ

Theorem10.20.28

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin paper seven workspace logical unitary unitary”; 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/PaperSevenPrimitive.lean:218. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.20.28●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/PaperSevenPrimitive.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinPaperSevenWorkspaceLogicalUnitary_unitary :
  QuantumBlockEncoding.Robin.warmRobinPaperSevenWorkspaceLogicalUnitary ∈
    Matrix.unitaryGroup
      (QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex (Fin 2) (Fin 8)
        QuantumBlockEncoding.Robin.WarmRobinPaperSevenFullSystem)
      ℂ

theorem QuantumBlockEncoding.Robin.warmRobinPaperSevenWorkspaceLogicalUnitary_unitary :
  QuantumBlockEncoding.Robin.warmRobinPaperSevenWorkspaceLogicalUnitary ∈
    Matrix.unitaryGroup
      (QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex
        (Fin 2) (Fin 8)
        QuantumBlockEncoding.Robin.WarmRobinPaperSevenFullSystem)
      ℂ

Theorem10.20.29

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin paper seven workspace logical unitary clean entry”; 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/PaperSevenPrimitive.lean:227. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.20.29●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/PaperSevenPrimitive.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinPaperSevenWorkspaceLogicalUnitary_cleanEntry
  (row column : Fin 8) :
  QuantumBlockEncoding.Robin.warmRobinPaperSevenWorkspaceLogicalUnitary
      (0, 0, row, 0) (0, 0, column, 0) =
    ↑(QuantumBlockEncoding.Robin.warmRobinSourceSevenCleanFormula row
        column)

theorem QuantumBlockEncoding.Robin.warmRobinPaperSevenWorkspaceLogicalUnitary_cleanEntry
  (row column : Fin 8) :
  QuantumBlockEncoding.Robin.warmRobinPaperSevenWorkspaceLogicalUnitary
      (0, 0, row, 0) (0, 0, column, 0) =
    ↑(QuantumBlockEncoding.Robin.warmRobinSourceSevenCleanFormula
        row column)