Figure4T3.lean🔗

19 explicit public declarations, in source order.

Definition10.12.1

uses 0used by 0✓L∃∀N

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

Lean code for Definition10.12.1●1 definition

defdefined in QuantumBlockEncoding/Robin/Figure4T3.lean

complete

def QuantumBlockEncoding.Robin.warmRobinFigure4PrimitiveProgram :
  QuantumBlockEncoding.PrimitiveProgram 9

def QuantumBlockEncoding.Robin.warmRobinFigure4PrimitiveProgram :
  QuantumBlockEncoding.PrimitiveProgram 9

Theorem10.12.2

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin figure 4 all workspace clean”; the hypotheses and conclusion in the code panel fix its exact scope. Both Figure-4 work wires return clean on every selector/system branch.

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. Both Figure-4 work wires return clean on every selector/system branch. The coefficient loader may superpose 'q6', but it does not alter this classical context, so the statement is quantified over both coefficient basis values.

Declaration kind. theorem.

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

Lean code for Theorem10.12.2●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/Figure4T3.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinFigure4AllWorkspaceClean
  (slot column : Fin 8) (coefficient : Fin 2) :
  have afterIndicator :=
    QuantumBlockEncoding.Robin.warmRobinFigure4DTIndicatorBasisEquiv
      (QuantumBlockEncoding.Robin.warmRobinFigure4TransportInput slot
        column coefficient 0);
  have output :=
    QuantumBlockEncoding.Robin.warmRobinFigure4PostLoaderBasisEquiv
      afterIndicator;
  output 7 = 0 ∧ output 8 = 0

theorem QuantumBlockEncoding.Robin.warmRobinFigure4AllWorkspaceClean
  (slot column : Fin 8)
  (coefficient : Fin 2) :
  have afterIndicator :=
    QuantumBlockEncoding.Robin.warmRobinFigure4DTIndicatorBasisEquiv
      (QuantumBlockEncoding.Robin.warmRobinFigure4TransportInput
        slot column coefficient 0);
  have output :=
    QuantumBlockEncoding.Robin.warmRobinFigure4PostLoaderBasisEquiv
      afterIndicator;
  output 7 = 0 ∧ output 8 = 0

Both Figure-4 work wires return clean on every selector/system branch.
The coefficient loader may superpose `q6`, but it does not alter this classical
context, so the statement is quantified over both coefficient basis values.

Definition10.12.3

uses 0used by 0✓L∃∀N

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

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

Lean code for Definition10.12.3●1 definition

defdefined in QuantumBlockEncoding/Robin/Figure4T3.lean

complete

def QuantumBlockEncoding.Robin.warmRobinFigure4LogicalMiddle :
  Matrix
    (QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex (Fin 2) (Fin 8)
      QuantumBlockEncoding.Robin.WarmRobinFigure4FullSystem)
    (QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex (Fin 2) (Fin 8)
      QuantumBlockEncoding.Robin.WarmRobinFigure4FullSystem)
    ℂ

def QuantumBlockEncoding.Robin.warmRobinFigure4LogicalMiddle :
  Matrix
    (QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex
      (Fin 2) (Fin 8)
      QuantumBlockEncoding.Robin.WarmRobinFigure4FullSystem)
    (QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex
      (Fin 2) (Fin 8)
      QuantumBlockEncoding.Robin.WarmRobinFigure4FullSystem)
    ℂ

Theorem10.12.4

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin figure 4 logical middle 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/Figure4T3.lean:44. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.12.4●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/Figure4T3.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinFigure4LogicalMiddle_apply
  (row column :
    QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex (Fin 2) (Fin 8)
      QuantumBlockEncoding.Robin.WarmRobinFigure4FullSystem) :
  QuantumBlockEncoding.Robin.warmRobinFigure4LogicalMiddle row column =
    QuantumBlockEncoding.evalPrimitiveProgram
      QuantumBlockEncoding.Robin.warmRobinFigure4MiddleProgram
      (QuantumBlockEncoding.Robin.warmRobinFigure4BitsEquiv.symm row)
      (QuantumBlockEncoding.Robin.warmRobinFigure4BitsEquiv.symm column)

theorem QuantumBlockEncoding.Robin.warmRobinFigure4LogicalMiddle_apply
  (row column :
    QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex
      (Fin 2) (Fin 8)
      QuantumBlockEncoding.Robin.WarmRobinFigure4FullSystem) :
  QuantumBlockEncoding.Robin.warmRobinFigure4LogicalMiddle
      row column =
    QuantumBlockEncoding.evalPrimitiveProgram
      QuantumBlockEncoding.Robin.warmRobinFigure4MiddleProgram
      (QuantumBlockEncoding.Robin.warmRobinFigure4BitsEquiv.symm
        row)
      (QuantumBlockEncoding.Robin.warmRobinFigure4BitsEquiv.symm
        column)

Theorem10.12.5

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin figure 4 logical middle 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/Figure4T3.lean:53. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.12.5●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/Figure4T3.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinFigure4LogicalMiddle_cleanEntry
  (coefficientRow coefficientColumn : Fin 2)
  (leftSlot rightSlot row column : Fin 8) :
  QuantumBlockEncoding.Robin.warmRobinFigure4LogicalMiddle
      (coefficientRow, leftSlot, row, 0, 0)
      (coefficientColumn, rightSlot, column, 0, 0) =
    if
        leftSlot = rightSlot ∧
          QuantumBlockEncoding.Robin.warmRobinSourceDTRow rightSlot
              column =
            row then
      QuantumBlockEncoding.Robin.ComplexLCU.amplitudeRotation
        (↑(QuantumBlockEncoding.Robin.warmRobinFigure4SourceCoefficient
            rightSlot column))
        coefficientRow coefficientColumn
    else 0

theorem QuantumBlockEncoding.Robin.warmRobinFigure4LogicalMiddle_cleanEntry
  (coefficientRow coefficientColumn :
    Fin 2)
  (leftSlot rightSlot row column :
    Fin 8) :
  QuantumBlockEncoding.Robin.warmRobinFigure4LogicalMiddle
      (coefficientRow, leftSlot, row, 0,
        0)
      (coefficientColumn, rightSlot,
        column, 0, 0) =
    if
        leftSlot = rightSlot ∧
          QuantumBlockEncoding.Robin.warmRobinSourceDTRow
              rightSlot column =
            row then
      QuantumBlockEncoding.Robin.ComplexLCU.amplitudeRotation
        (↑(QuantumBlockEncoding.Robin.warmRobinFigure4SourceCoefficient
            rightSlot column))
        coefficientRow coefficientColumn
    else 0

Theorem10.12.6

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin figure 4 primitive eval eq logical”; the hypotheses and conclusion in the code panel fix its exact scope. Exact physical-program semantics, including all macro compiler phases.

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 physical-program semantics, including all macro compiler phases.

Declaration kind. theorem.

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

Lean code for Theorem10.12.6●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/Figure4T3.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinFigure4Primitive_eval_eq_logical :
  QuantumBlockEncoding.evalPrimitiveProgram
      QuantumBlockEncoding.Robin.warmRobinFigure4PrimitiveProgram =
    (Matrix.reindexAlgEquiv ℂ ℂ
        QuantumBlockEncoding.Robin.warmRobinFigure4BitsEquiv.symm)
      (star
            (QuantumBlockEncoding.Robin.ComplexLCU.selectorLift
              QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectorPrepare) *
          QuantumBlockEncoding.Robin.warmRobinFigure4LogicalMiddle *
        QuantumBlockEncoding.Robin.ComplexLCU.selectorLift
          QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectorPrepare)

theorem QuantumBlockEncoding.Robin.warmRobinFigure4Primitive_eval_eq_logical :
  QuantumBlockEncoding.evalPrimitiveProgram
      QuantumBlockEncoding.Robin.warmRobinFigure4PrimitiveProgram =
    (Matrix.reindexAlgEquiv ℂ ℂ
        QuantumBlockEncoding.Robin.warmRobinFigure4BitsEquiv.symm)
      (star
            (QuantumBlockEncoding.Robin.ComplexLCU.selectorLift
              QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectorPrepare) *
          QuantumBlockEncoding.Robin.warmRobinFigure4LogicalMiddle *
        QuantumBlockEncoding.Robin.ComplexLCU.selectorLift
          QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectorPrepare)

Exact physical-program semantics, including all macro compiler phases.

Theorem10.12.7

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.12.7●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/Figure4T3.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinFigure4Logical_cleanEntry
  (row column : Fin 8) :
  (star
            (QuantumBlockEncoding.Robin.ComplexLCU.selectorLift
              QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectorPrepare) *
          QuantumBlockEncoding.Robin.warmRobinFigure4LogicalMiddle *
        QuantumBlockEncoding.Robin.ComplexLCU.selectorLift
          QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectorPrepare)
      (0, 0, row, 0, 0) (0, 0, column, 0, 0) =
    ↑(QuantumBlockEncoding.Robin.warmRobinSourceSevenCleanFormula row
        column)

theorem QuantumBlockEncoding.Robin.warmRobinFigure4Logical_cleanEntry
  (row column : Fin 8) :
  (star
            (QuantumBlockEncoding.Robin.ComplexLCU.selectorLift
              QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectorPrepare) *
          QuantumBlockEncoding.Robin.warmRobinFigure4LogicalMiddle *
        QuantumBlockEncoding.Robin.ComplexLCU.selectorLift
          QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectorPrepare)
      (0, 0, row, 0, 0)
      (0, 0, column, 0, 0) =
    ↑(QuantumBlockEncoding.Robin.warmRobinSourceSevenCleanFormula
        row column)

Definition10.12.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 primitive flat 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/Figure4T3.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.12.8●1 definition

defdefined in QuantumBlockEncoding/Robin/Figure4T3.lean

complete

def QuantumBlockEncoding.Robin.warmRobinFigure4PrimitiveFlatUnitary :
  Matrix (Fin (QuantumBlockEncoding.gridSize 9))
    (Fin (QuantumBlockEncoding.gridSize 9)) ℂ

def QuantumBlockEncoding.Robin.warmRobinFigure4PrimitiveFlatUnitary :
  Matrix
    (Fin
      (QuantumBlockEncoding.gridSize 9))
    (Fin
      (QuantumBlockEncoding.gridSize 9))
    ℂ

Theorem10.12.9

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin figure 4 primitive circuit 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/Figure4T3.lean:231. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.12.9●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/Figure4T3.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinFigure4PrimitiveCircuit_unitary :
  QuantumBlockEncoding.Robin.warmRobinFigure4PrimitiveFlatUnitary ∈
    Matrix.unitaryGroup (Fin (QuantumBlockEncoding.gridSize 9)) ℂ

theorem QuantumBlockEncoding.Robin.warmRobinFigure4PrimitiveCircuit_unitary :
  QuantumBlockEncoding.Robin.warmRobinFigure4PrimitiveFlatUnitary ∈
    Matrix.unitaryGroup
      (Fin
        (QuantumBlockEncoding.gridSize 9))
      ℂ

Definition10.12.10

uses 0used by 0✓L∃∀N

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

Lean code for Definition10.12.10●1 definition

defdefined in QuantumBlockEncoding/Robin/Figure4T3.lean

complete

def QuantumBlockEncoding.Robin.warmRobinFigure4PrimitiveCleanIndex
  (system : Fin 8) : Fin (QuantumBlockEncoding.gridSize 9)

def QuantumBlockEncoding.Robin.warmRobinFigure4PrimitiveCleanIndex
  (system : Fin 8) :
  Fin (QuantumBlockEncoding.gridSize 9)

Theorem10.12.11

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin figure 4 primitive circuit clean entry”; the hypotheses and conclusion in the code panel fix its exact scope. Required whole-circuit clean entry; this is symbolic, not numerical.

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. Required whole-circuit clean entry; this is symbolic, not numerical.

Declaration kind. theorem.

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

Lean code for Theorem10.12.11●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/Figure4T3.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinFigure4PrimitiveCircuit_cleanEntry
  (row column : Fin 8) :
  QuantumBlockEncoding.Robin.warmRobinFigure4PrimitiveFlatUnitary
      (QuantumBlockEncoding.Robin.warmRobinFigure4PrimitiveCleanIndex
        row)
      (QuantumBlockEncoding.Robin.warmRobinFigure4PrimitiveCleanIndex
        column) =
    ↑(QuantumBlockEncoding.Robin.warmRobinSourceSevenCleanFormula row
        column)

theorem QuantumBlockEncoding.Robin.warmRobinFigure4PrimitiveCircuit_cleanEntry
  (row column : Fin 8) :
  QuantumBlockEncoding.Robin.warmRobinFigure4PrimitiveFlatUnitary
      (QuantumBlockEncoding.Robin.warmRobinFigure4PrimitiveCleanIndex
        row)
      (QuantumBlockEncoding.Robin.warmRobinFigure4PrimitiveCleanIndex
        column) =
    ↑(QuantumBlockEncoding.Robin.warmRobinSourceSevenCleanFormula
        row column)

Required whole-circuit clean entry; this is symbolic, not numerical.

Theorem10.12.12

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin figure 4 primitive circuit clean block”; 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/Figure4T3.lean:267. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.12.12●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/Figure4T3.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinFigure4PrimitiveCircuit_cleanBlock
  (row column : Fin 8) :
  QuantumBlockEncoding.Robin.warmRobinFigure4PrimitiveFlatUnitary
      (QuantumBlockEncoding.Robin.warmRobinFigure4PrimitiveCleanIndex
        row)
      (QuantumBlockEncoding.Robin.warmRobinFigure4PrimitiveCleanIndex
        column) =
    ↑(QuantumBlockEncoding.RobinEvolution.warmRobinTarget row column /
        QuantumBlockEncoding.RobinEvolution.warmRobinNormalizer)

theorem QuantumBlockEncoding.Robin.warmRobinFigure4PrimitiveCircuit_cleanBlock
  (row column : Fin 8) :
  QuantumBlockEncoding.Robin.warmRobinFigure4PrimitiveFlatUnitary
      (QuantumBlockEncoding.Robin.warmRobinFigure4PrimitiveCleanIndex
        row)
      (QuantumBlockEncoding.Robin.warmRobinFigure4PrimitiveCleanIndex
        column) =
    ↑(QuantumBlockEncoding.RobinEvolution.warmRobinTarget
          row column /
        QuantumBlockEncoding.RobinEvolution.warmRobinNormalizer)

Definition10.12.13

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin figure 4 primitive block contains target”.

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

Why it is in this chapter. 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/Figure4T3.lean:276. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition10.12.13●1 definition

defdefined in QuantumBlockEncoding/Robin/Figure4T3.lean

complete

def QuantumBlockEncoding.Robin.warmRobinFigure4PrimitiveBlockContainsTarget :
  Prop

def QuantumBlockEncoding.Robin.warmRobinFigure4PrimitiveBlockContainsTarget :
  Prop

Theorem10.12.14

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin figure 4 primitive block contains target proof”; 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/Figure4T3.lean:284. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.12.14●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/Figure4T3.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinFigure4PrimitiveBlockContainsTarget_proof :
  QuantumBlockEncoding.Robin.warmRobinFigure4PrimitiveBlockContainsTarget

theorem QuantumBlockEncoding.Robin.warmRobinFigure4PrimitiveBlockContainsTarget_proof :
  QuantumBlockEncoding.Robin.warmRobinFigure4PrimitiveBlockContainsTarget

Definition10.12.15

uses 0used by 0✓L∃∀N

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

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

Lean code for Definition10.12.15●1 definition

defdefined in QuantumBlockEncoding/Robin/Figure4T3.lean

complete

def QuantumBlockEncoding.Robin.warmRobinFigure4PrimitivePresentation :
  QuantumBlockEncoding.Circuit

def QuantumBlockEncoding.Robin.warmRobinFigure4PrimitivePresentation :
  QuantumBlockEncoding.Circuit

Definition10.12.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 primitive resource”.

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

Lean code for Definition10.12.16●1 definition

defdefined in QuantumBlockEncoding/Robin/Figure4T3.lean

complete

def QuantumBlockEncoding.Robin.warmRobinFigure4PrimitiveResource :
  QuantumBlockEncoding.Resource

def QuantumBlockEncoding.Robin.warmRobinFigure4PrimitiveResource :
  QuantumBlockEncoding.Resource

Definition10.12.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 primitive operator candidate”.

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

Lean code for Definition10.12.17●1 definition

defdefined in QuantumBlockEncoding/Robin/Figure4T3.lean

complete

def QuantumBlockEncoding.Robin.warmRobinFigure4PrimitiveOperatorCandidate :
  QuantumBlockEncoding.OperatorBlockEncodingCandidate ℂ 3

def QuantumBlockEncoding.Robin.warmRobinFigure4PrimitiveOperatorCandidate :
  QuantumBlockEncoding.OperatorBlockEncodingCandidate
    ℂ 3

Definition10.12.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 primitive refinement”.

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

Lean code for Definition10.12.18●1 definition

defdefined in QuantumBlockEncoding/Robin/Figure4T3.lean

complete

def QuantumBlockEncoding.Robin.warmRobinFigure4PrimitiveRefinement :
  QuantumBlockEncoding.PrimitiveProgramRefinement 9

def QuantumBlockEncoding.Robin.warmRobinFigure4PrimitiveRefinement :
  QuantumBlockEncoding.PrimitiveProgramRefinement
    9

Definition10.12.19

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin figure 4 primitive verified block encoding”. Fixed-N8, f=1, standard-RY-corrected Figure-4 realization.

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. Fixed-N8, f=1, standard-RY-corrected Figure-4 realization.

Declaration kind. def.

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

Lean code for Definition10.12.19●1 definition

defdefined in QuantumBlockEncoding/Robin/Figure4T3.lean

complete

def QuantumBlockEncoding.Robin.warmRobinFigure4PrimitiveVerifiedBlockEncoding :
  QuantumBlockEncoding.VerifiedOperatorBlockEncoding ℂ 3

def QuantumBlockEncoding.Robin.warmRobinFigure4PrimitiveVerifiedBlockEncoding :
  QuantumBlockEncoding.VerifiedOperatorBlockEncoding
    ℂ 3

Fixed-N8, f=1, standard-RY-corrected Figure-4 realization.