ASPBE Lean Blueprint

10.7. QuantumBlockEncoding/Robin/Figure4Loaders.lean🔗

36 explicit public declarations, in source order.

Definition10.7.1
uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin paper literal boundary angle”.

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

Lean code for Definition10.7.1●1 definition
  • defdefined in QuantumBlockEncoding/Robin/Figure4Loaders.lean
    complete
    def QuantumBlockEncoding.Robin.warmRobinPaperLiteralBoundaryAngle
  (coefficient : ℚ) : ℝ
    def QuantumBlockEncoding.Robin.warmRobinPaperLiteralBoundaryAngle
  (coefficient : ℚ) : ℝ
Definition10.7.2
uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin executable standard ry boundary angle”.

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

Lean code for Definition10.7.2●1 definition
  • defdefined in QuantumBlockEncoding/Robin/Figure4Loaders.lean
    complete
    def QuantumBlockEncoding.Robin.warmRobinExecutableStandardRyBoundaryAngle
  (coefficient : ℚ) : ℝ
    def QuantumBlockEncoding.Robin.warmRobinExecutableStandardRyBoundaryAngle
  (coefficient : ℚ) : ℝ
Definition10.7.3
uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin corrected eq 27 boundary angle”. Corrected reading of Eq.

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. Corrected reading of Eq. (27) for the standard quantum-computing 'R_y' convention. The displayed single-'arccos' expression in arXiv:2506.20478 is retained above only as a literal transcript of the source typo.

Declaration kind. def.

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

Lean code for Definition10.7.3●1 definition
  • defdefined in QuantumBlockEncoding/Robin/Figure4Loaders.lean
    complete
    def QuantumBlockEncoding.Robin.warmRobinCorrectedEq27BoundaryAngle
  (coefficient : ℚ) : ℝ
    def QuantumBlockEncoding.Robin.warmRobinCorrectedEq27BoundaryAngle
  (coefficient : ℚ) : ℝ
    Corrected reading of Eq. (27) for the standard quantum-computing `R_y`
convention.  The displayed single-`arccos` expression in arXiv:2506.20478 is
retained above only as a literal transcript of the source typo.
Theorem10.7.4
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin corrected eq 27 boundary angle eq executable”; 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/Figure4Loaders.lean:30. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.7.4●1 theorem
  • theoremdefined in QuantumBlockEncoding/Robin/Figure4Loaders.lean
    complete
    theorem QuantumBlockEncoding.Robin.warmRobinCorrectedEq27BoundaryAngle_eq_executable
  (coefficient : ℚ) :
  QuantumBlockEncoding.Robin.warmRobinCorrectedEq27BoundaryAngle
      coefficient =
    QuantumBlockEncoding.Robin.warmRobinExecutableStandardRyBoundaryAngle
      coefficient
    theorem QuantumBlockEncoding.Robin.warmRobinCorrectedEq27BoundaryAngle_eq_executable
  (coefficient : ℚ) :
  QuantumBlockEncoding.Robin.warmRobinCorrectedEq27BoundaryAngle
      coefficient =
    QuantumBlockEncoding.Robin.warmRobinExecutableStandardRyBoundaryAngle
      coefficient
Theorem10.7.5
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin corrected eq 27 standard ry clean amplitude”; 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/Figure4Loaders.lean:35. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.7.5●1 theorem
  • theoremdefined in QuantumBlockEncoding/Robin/Figure4Loaders.lean
    complete
    theorem QuantumBlockEncoding.Robin.warmRobinCorrectedEq27_standardRy_cleanAmplitude
  (coefficient : ℚ) (lower : -1 ≤ ↑coefficient)
  (upper : ↑coefficient ≤ 1) :
  QuantumBlockEncoding.standardRyMatrix
      (QuantumBlockEncoding.Robin.warmRobinCorrectedEq27BoundaryAngle
        coefficient) =
    QuantumBlockEncoding.Robin.ComplexLCU.amplitudeRotation ↑coefficient
    theorem QuantumBlockEncoding.Robin.warmRobinCorrectedEq27_standardRy_cleanAmplitude
  (coefficient : ℚ)
  (lower : -1 ≤ ↑coefficient)
  (upper : ↑coefficient ≤ 1) :
  QuantumBlockEncoding.standardRyMatrix
      (QuantumBlockEncoding.Robin.warmRobinCorrectedEq27BoundaryAngle
        coefficient) =
    QuantumBlockEncoding.Robin.ComplexLCU.amplitudeRotation
      ↑coefficient
Theorem10.7.6
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin boundary angle zero guard”; 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/Figure4Loaders.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.7.6●1 theorem
  • theoremdefined in QuantumBlockEncoding/Robin/Figure4Loaders.lean
    complete
    theorem QuantumBlockEncoding.Robin.warmRobinBoundaryAngle_zero_guard :
  QuantumBlockEncoding.Robin.warmRobinPaperLiteralBoundaryAngle 0 =
      Real.pi / 2 ∧
    QuantumBlockEncoding.Robin.warmRobinExecutableStandardRyBoundaryAngle
        0 =
      Real.pi
    theorem QuantumBlockEncoding.Robin.warmRobinBoundaryAngle_zero_guard :
  QuantumBlockEncoding.Robin.warmRobinPaperLiteralBoundaryAngle
        0 =
      Real.pi / 2 ∧
    QuantumBlockEncoding.Robin.warmRobinExecutableStandardRyBoundaryAngle
        0 =
      Real.pi
Theorem10.7.7
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin figure 4 bulk coefficient abs le one”; 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/Figure4Loaders.lean:52. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.7.7●1 theorem
  • theoremdefined in QuantumBlockEncoding/Robin/Figure4Loaders.lean
    complete
    theorem QuantumBlockEncoding.Robin.warmRobinFigure4BulkCoefficient_abs_le_one
  (slot : Fin 8) :
  |↑(QuantumBlockEncoding.Robin.warmRobinFigure4BulkCoefficient slot)| ≤
    1
    theorem QuantumBlockEncoding.Robin.warmRobinFigure4BulkCoefficient_abs_le_one
  (slot : Fin 8) :
  |↑(QuantumBlockEncoding.Robin.warmRobinFigure4BulkCoefficient
          slot)| ≤
    1
Theorem10.7.8
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin figure 4 source coefficient abs le one”; 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/Figure4Loaders.lean:58. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.7.8●1 theorem
  • theoremdefined in QuantumBlockEncoding/Robin/Figure4Loaders.lean
    complete
    theorem QuantumBlockEncoding.Robin.warmRobinFigure4SourceCoefficient_abs_le_one
  (slot column : Fin 8) :
  |↑(QuantumBlockEncoding.Robin.warmRobinFigure4SourceCoefficient slot
          column)| ≤
    1
    theorem QuantumBlockEncoding.Robin.warmRobinFigure4SourceCoefficient_abs_le_one
  (slot column : Fin 8) :
  |↑(QuantumBlockEncoding.Robin.warmRobinFigure4SourceCoefficient
          slot column)| ≤
    1
Definition10.7.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 bulk control wires”.

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

Lean code for Definition10.7.9●1 definition
  • defdefined in QuantumBlockEncoding/Robin/Figure4Loaders.lean
    complete
    def QuantumBlockEncoding.Robin.warmRobinFigure4BulkControlWires :
  Fin 4 → Fin 9
    def QuantumBlockEncoding.Robin.warmRobinFigure4BulkControlWires :
  Fin 4 → Fin 9
Theorem10.7.10
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin figure 4 bulk control wires ne target”; 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/Figure4Loaders.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.7.10●1 theorem
  • theoremdefined in QuantumBlockEncoding/Robin/Figure4Loaders.lean
    complete
    theorem QuantumBlockEncoding.Robin.warmRobinFigure4BulkControlWires_ne_target
  (wire : Fin 4) :
  QuantumBlockEncoding.Robin.warmRobinFigure4BulkControlWires wire ≠ 6
    theorem QuantumBlockEncoding.Robin.warmRobinFigure4BulkControlWires_ne_target
  (wire : Fin 4) :
  QuantumBlockEncoding.Robin.warmRobinFigure4BulkControlWires
      wire ≠
    6
Definition10.7.11
uses 0used by 0✓L∃∀N

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

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

Lean code for Definition10.7.11●1 definition
  • defdefined in QuantumBlockEncoding/Robin/Figure4Loaders.lean
    complete
    def QuantumBlockEncoding.Robin.warmRobinFigure4BulkControlSlot
  (bits : QuantumBlockEncoding.PrimitiveBasis 4) : Fin 8
    def QuantumBlockEncoding.Robin.warmRobinFigure4BulkControlSlot
  (bits :
    QuantumBlockEncoding.PrimitiveBasis
      4) :
  Fin 8
Definition10.7.12
uses 0used by 0✓L∃∀N

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

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

Lean code for Definition10.7.12●1 definition
  • defdefined in QuantumBlockEncoding/Robin/Figure4Loaders.lean
    complete
    def QuantumBlockEncoding.Robin.warmRobinFigure4BulkLoaderAngle
  (bits : QuantumBlockEncoding.PrimitiveBasis 4) :
  QuantumBlockEncoding.ExactAngle
    def QuantumBlockEncoding.Robin.warmRobinFigure4BulkLoaderAngle
  (bits :
    QuantumBlockEncoding.PrimitiveBasis
      4) :
  QuantumBlockEncoding.ExactAngle
Theorem10.7.13
uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.7.13●1 theorem
  • theoremdefined in QuantumBlockEncoding/Robin/Figure4Loaders.lean
    complete
    theorem QuantumBlockEncoding.Robin.warmRobinFigure4BulkLoaderRy
  (bits : QuantumBlockEncoding.PrimitiveBasis 4) :
  QuantumBlockEncoding.standardRyMatrix
      (QuantumBlockEncoding.Robin.warmRobinFigure4BulkLoaderAngle
          bits).eval =
    if bits 3 = 1 then
      QuantumBlockEncoding.Robin.ComplexLCU.amplitudeRotation
        ↑(QuantumBlockEncoding.Robin.warmRobinFigure4BulkCoefficient
            (QuantumBlockEncoding.Robin.warmRobinFigure4BulkControlSlot
              bits))
    else 1
    theorem QuantumBlockEncoding.Robin.warmRobinFigure4BulkLoaderRy
  (bits :
    QuantumBlockEncoding.PrimitiveBasis
      4) :
  QuantumBlockEncoding.standardRyMatrix
      (QuantumBlockEncoding.Robin.warmRobinFigure4BulkLoaderAngle
          bits).eval =
    if bits 3 = 1 then
      QuantumBlockEncoding.Robin.ComplexLCU.amplitudeRotation
        ↑(QuantumBlockEncoding.Robin.warmRobinFigure4BulkCoefficient
            (QuantumBlockEncoding.Robin.warmRobinFigure4BulkControlSlot
              bits))
    else 1
Definition10.7.14
uses 0used by 0✓L∃∀N

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

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

Lean code for Definition10.7.14●1 definition
  • defdefined in QuantumBlockEncoding/Robin/Figure4Loaders.lean
    complete
    def QuantumBlockEncoding.Robin.warmRobinFigure4BulkLoaderCircuit :
  QuantumBlockEncoding.PrimitiveCircuit 9
    def QuantumBlockEncoding.Robin.warmRobinFigure4BulkLoaderCircuit :
  QuantumBlockEncoding.PrimitiveCircuit 9
Definition10.7.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 bulk loader 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/Figure4Loaders.lean:116. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition10.7.15●1 definition
  • defdefined in QuantumBlockEncoding/Robin/Figure4Loaders.lean
    complete
    def QuantumBlockEncoding.Robin.warmRobinFigure4BulkLoaderProgram :
  QuantumBlockEncoding.PrimitiveProgram 9
    def QuantumBlockEncoding.Robin.warmRobinFigure4BulkLoaderProgram :
  QuantumBlockEncoding.PrimitiveProgram 9
Theorem10.7.16
uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.7.16●1 theorem
  • theoremdefined in QuantumBlockEncoding/Robin/Figure4Loaders.lean
    complete
    theorem QuantumBlockEncoding.Robin.warmRobinFigure4BulkLoaderProgram_eval :
  QuantumBlockEncoding.evalPrimitiveProgram
      QuantumBlockEncoding.Robin.warmRobinFigure4BulkLoaderProgram =
    QuantumBlockEncoding.controlledRyBlockMatrix
      QuantumBlockEncoding.Robin.warmRobinFigure4BulkControlWires 6
      QuantumBlockEncoding.Robin.warmRobinFigure4BulkControlWires_ne_target
      QuantumBlockEncoding.Robin.warmRobinFigure4BulkLoaderAngle
    theorem QuantumBlockEncoding.Robin.warmRobinFigure4BulkLoaderProgram_eval :
  QuantumBlockEncoding.evalPrimitiveProgram
      QuantumBlockEncoding.Robin.warmRobinFigure4BulkLoaderProgram =
    QuantumBlockEncoding.controlledRyBlockMatrix
      QuantumBlockEncoding.Robin.warmRobinFigure4BulkControlWires
      6
      QuantumBlockEncoding.Robin.warmRobinFigure4BulkControlWires_ne_target
      QuantumBlockEncoding.Robin.warmRobinFigure4BulkLoaderAngle
Definition10.7.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 boundary control wires”.

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

Lean code for Definition10.7.17●1 definition
  • defdefined in QuantumBlockEncoding/Robin/Figure4Loaders.lean
    complete
    def QuantumBlockEncoding.Robin.warmRobinFigure4BoundaryControlWires :
  Fin 7 → Fin 9
    def QuantumBlockEncoding.Robin.warmRobinFigure4BoundaryControlWires :
  Fin 7 → Fin 9
Theorem10.7.18
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin figure 4 boundary control wires ne target”; 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/Figure4Loaders.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.7.18●1 theorem
  • theoremdefined in QuantumBlockEncoding/Robin/Figure4Loaders.lean
    complete
    theorem QuantumBlockEncoding.Robin.warmRobinFigure4BoundaryControlWires_ne_target
  (wire : Fin 7) :
  QuantumBlockEncoding.Robin.warmRobinFigure4BoundaryControlWires wire ≠
    6
    theorem QuantumBlockEncoding.Robin.warmRobinFigure4BoundaryControlWires_ne_target
  (wire : Fin 7) :
  QuantumBlockEncoding.Robin.warmRobinFigure4BoundaryControlWires
      wire ≠
    6
Definition10.7.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 boundary control slot”.

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

Lean code for Definition10.7.19●1 definition
  • defdefined in QuantumBlockEncoding/Robin/Figure4Loaders.lean
    complete
    def QuantumBlockEncoding.Robin.warmRobinFigure4BoundaryControlSlot
  (bits : QuantumBlockEncoding.PrimitiveBasis 7) : Fin 8
    def QuantumBlockEncoding.Robin.warmRobinFigure4BoundaryControlSlot
  (bits :
    QuantumBlockEncoding.PrimitiveBasis
      7) :
  Fin 8
Definition10.7.20
uses 0used by 0✓L∃∀N

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

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

Lean code for Definition10.7.20●1 definition
  • defdefined in QuantumBlockEncoding/Robin/Figure4Loaders.lean
    complete
    def QuantumBlockEncoding.Robin.warmRobinFigure4BoundaryControlColumn
  (bits : QuantumBlockEncoding.PrimitiveBasis 7) : Fin 8
    def QuantumBlockEncoding.Robin.warmRobinFigure4BoundaryControlColumn
  (bits :
    QuantumBlockEncoding.PrimitiveBasis
      7) :
  Fin 8
Definition10.7.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 boundary loader angle”.

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

Lean code for Definition10.7.21●1 definition
  • defdefined in QuantumBlockEncoding/Robin/Figure4Loaders.lean
    complete
    def QuantumBlockEncoding.Robin.warmRobinFigure4BoundaryLoaderAngle
  (bits : QuantumBlockEncoding.PrimitiveBasis 7) :
  QuantumBlockEncoding.ExactAngle
    def QuantumBlockEncoding.Robin.warmRobinFigure4BoundaryLoaderAngle
  (bits :
    QuantumBlockEncoding.PrimitiveBasis
      7) :
  QuantumBlockEncoding.ExactAngle
Theorem10.7.22
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin figure 4 boundary loader ry”; 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/Figure4Loaders.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.7.22●1 theorem
  • theoremdefined in QuantumBlockEncoding/Robin/Figure4Loaders.lean
    complete
    theorem QuantumBlockEncoding.Robin.warmRobinFigure4BoundaryLoaderRy
  (bits : QuantumBlockEncoding.PrimitiveBasis 7) :
  QuantumBlockEncoding.standardRyMatrix
      (QuantumBlockEncoding.Robin.warmRobinFigure4BoundaryLoaderAngle
          bits).eval =
    if
        bits 6 = 0 ∧
          ¬QuantumBlockEncoding.Robin.warmRobinFigure4TransposeBulk
              (QuantumBlockEncoding.Robin.warmRobinFigure4BoundaryControlColumn
                bits) then
      QuantumBlockEncoding.Robin.ComplexLCU.amplitudeRotation
        ↑(QuantumBlockEncoding.Robin.warmRobinFigure4SourceCoefficient
            (QuantumBlockEncoding.Robin.warmRobinFigure4BoundaryControlSlot
              bits)
            (QuantumBlockEncoding.Robin.warmRobinFigure4BoundaryControlColumn
              bits))
    else 1
    theorem QuantumBlockEncoding.Robin.warmRobinFigure4BoundaryLoaderRy
  (bits :
    QuantumBlockEncoding.PrimitiveBasis
      7) :
  QuantumBlockEncoding.standardRyMatrix
      (QuantumBlockEncoding.Robin.warmRobinFigure4BoundaryLoaderAngle
          bits).eval =
    if
        bits 6 = 0 ∧
          ¬QuantumBlockEncoding.Robin.warmRobinFigure4TransposeBulk
              (QuantumBlockEncoding.Robin.warmRobinFigure4BoundaryControlColumn
                bits) then
      QuantumBlockEncoding.Robin.ComplexLCU.amplitudeRotation
        ↑(QuantumBlockEncoding.Robin.warmRobinFigure4SourceCoefficient
            (QuantumBlockEncoding.Robin.warmRobinFigure4BoundaryControlSlot
              bits)
            (QuantumBlockEncoding.Robin.warmRobinFigure4BoundaryControlColumn
              bits))
    else 1
Definition10.7.23
uses 0used by 0✓L∃∀N

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

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

Lean code for Definition10.7.23●1 definition
  • defdefined in QuantumBlockEncoding/Robin/Figure4Loaders.lean
    complete
    def QuantumBlockEncoding.Robin.warmRobinFigure4BoundaryLoaderCircuit :
  QuantumBlockEncoding.PrimitiveCircuit 9
    def QuantumBlockEncoding.Robin.warmRobinFigure4BoundaryLoaderCircuit :
  QuantumBlockEncoding.PrimitiveCircuit 9
Definition10.7.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 boundary loader 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/Figure4Loaders.lean:198. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition10.7.24●1 definition
  • defdefined in QuantumBlockEncoding/Robin/Figure4Loaders.lean
    complete
    def QuantumBlockEncoding.Robin.warmRobinFigure4BoundaryLoaderProgram :
  QuantumBlockEncoding.PrimitiveProgram 9
    def QuantumBlockEncoding.Robin.warmRobinFigure4BoundaryLoaderProgram :
  QuantumBlockEncoding.PrimitiveProgram 9
Theorem10.7.25
uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.7.25●1 theorem
  • theoremdefined in QuantumBlockEncoding/Robin/Figure4Loaders.lean
    complete
    theorem QuantumBlockEncoding.Robin.warmRobinFigure4BoundaryLoaderProgram_eval :
  QuantumBlockEncoding.evalPrimitiveProgram
      QuantumBlockEncoding.Robin.warmRobinFigure4BoundaryLoaderProgram =
    QuantumBlockEncoding.controlledRyBlockMatrix
      QuantumBlockEncoding.Robin.warmRobinFigure4BoundaryControlWires 6
      QuantumBlockEncoding.Robin.warmRobinFigure4BoundaryControlWires_ne_target
      QuantumBlockEncoding.Robin.warmRobinFigure4BoundaryLoaderAngle
    theorem QuantumBlockEncoding.Robin.warmRobinFigure4BoundaryLoaderProgram_eval :
  QuantumBlockEncoding.evalPrimitiveProgram
      QuantumBlockEncoding.Robin.warmRobinFigure4BoundaryLoaderProgram =
    QuantumBlockEncoding.controlledRyBlockMatrix
      QuantumBlockEncoding.Robin.warmRobinFigure4BoundaryControlWires
      6
      QuantumBlockEncoding.Robin.warmRobinFigure4BoundaryControlWires_ne_target
      QuantumBlockEncoding.Robin.warmRobinFigure4BoundaryLoaderAngle
Definition10.7.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 derivative loader 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/Figure4Loaders.lean:215. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition10.7.26●1 definition
  • defdefined in QuantumBlockEncoding/Robin/Figure4Loaders.lean
    complete
    def QuantumBlockEncoding.Robin.warmRobinFigure4DerivativeLoaderProgram :
  QuantumBlockEncoding.PrimitiveProgram 9
    def QuantumBlockEncoding.Robin.warmRobinFigure4DerivativeLoaderProgram :
  QuantumBlockEncoding.PrimitiveProgram 9
Theorem10.7.27
uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.7.27●1 theorem
  • theoremdefined in QuantumBlockEncoding/Robin/Figure4Loaders.lean
    complete
    theorem QuantumBlockEncoding.Robin.warmRobinFigure4DerivativeLoaderProgram_eval :
  QuantumBlockEncoding.evalPrimitiveProgram
      QuantumBlockEncoding.Robin.warmRobinFigure4DerivativeLoaderProgram =
    QuantumBlockEncoding.controlledRyBlockMatrix
        QuantumBlockEncoding.Robin.warmRobinFigure4BoundaryControlWires
        6
        QuantumBlockEncoding.Robin.warmRobinFigure4BoundaryControlWires_ne_target
        QuantumBlockEncoding.Robin.warmRobinFigure4BoundaryLoaderAngle *
      QuantumBlockEncoding.controlledRyBlockMatrix
        QuantumBlockEncoding.Robin.warmRobinFigure4BulkControlWires 6
        QuantumBlockEncoding.Robin.warmRobinFigure4BulkControlWires_ne_target
        QuantumBlockEncoding.Robin.warmRobinFigure4BulkLoaderAngle
    theorem QuantumBlockEncoding.Robin.warmRobinFigure4DerivativeLoaderProgram_eval :
  QuantumBlockEncoding.evalPrimitiveProgram
      QuantumBlockEncoding.Robin.warmRobinFigure4DerivativeLoaderProgram =
    QuantumBlockEncoding.controlledRyBlockMatrix
        QuantumBlockEncoding.Robin.warmRobinFigure4BoundaryControlWires
        6
        QuantumBlockEncoding.Robin.warmRobinFigure4BoundaryControlWires_ne_target
        QuantumBlockEncoding.Robin.warmRobinFigure4BoundaryLoaderAngle *
      QuantumBlockEncoding.controlledRyBlockMatrix
        QuantumBlockEncoding.Robin.warmRobinFigure4BulkControlWires
        6
        QuantumBlockEncoding.Robin.warmRobinFigure4BulkControlWires_ne_target
        QuantumBlockEncoding.Robin.warmRobinFigure4BulkLoaderAngle
Definition10.7.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 indicator value”.

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

Lean code for Definition10.7.28●1 definition
  • defdefined in QuantumBlockEncoding/Robin/Figure4Loaders.lean
    complete
    def QuantumBlockEncoding.Robin.warmRobinFigure4IndicatorValue
  (column : Fin 8) : Fin 2
    def QuantumBlockEncoding.Robin.warmRobinFigure4IndicatorValue
  (column : Fin 8) : Fin 2
Definition10.7.29
uses 0used by 0✓L∃∀N

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

Lean code for Definition10.7.29●1 definition
  • defdefined in QuantumBlockEncoding/Robin/Figure4Loaders.lean
    complete
    def QuantumBlockEncoding.Robin.warmRobinFigure4BulkControlInput
  (slot : Fin 8) (indicator : Fin 2) :
  QuantumBlockEncoding.PrimitiveBasis 4
    def QuantumBlockEncoding.Robin.warmRobinFigure4BulkControlInput
  (slot : Fin 8) (indicator : Fin 2) :
  QuantumBlockEncoding.PrimitiveBasis 4
Definition10.7.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 boundary control 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/Figure4Loaders.lean:242. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition10.7.30●1 definition
  • defdefined in QuantumBlockEncoding/Robin/Figure4Loaders.lean
    complete
    def QuantumBlockEncoding.Robin.warmRobinFigure4BoundaryControlInput
  (slot column : Fin 8) (indicator : Fin 2) :
  QuantumBlockEncoding.PrimitiveBasis 7
    def QuantumBlockEncoding.Robin.warmRobinFigure4BoundaryControlInput
  (slot column : Fin 8)
  (indicator : Fin 2) :
  QuantumBlockEncoding.PrimitiveBasis 7
Theorem10.7.31
uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.7.31●1 theorem
  • theoremdefined in QuantumBlockEncoding/Robin/Figure4Loaders.lean
    complete
    theorem QuantumBlockEncoding.Robin.warmRobinFigure4BulkControlSlot_input
  (slot : Fin 8) (indicator : Fin 2) :
  QuantumBlockEncoding.Robin.warmRobinFigure4BulkControlSlot
      (QuantumBlockEncoding.Robin.warmRobinFigure4BulkControlInput slot
        indicator) =
    slot
    theorem QuantumBlockEncoding.Robin.warmRobinFigure4BulkControlSlot_input
  (slot : Fin 8) (indicator : Fin 2) :
  QuantumBlockEncoding.Robin.warmRobinFigure4BulkControlSlot
      (QuantumBlockEncoding.Robin.warmRobinFigure4BulkControlInput
        slot indicator) =
    slot
Theorem10.7.32
uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.7.32●1 theorem
  • theoremdefined in QuantumBlockEncoding/Robin/Figure4Loaders.lean
    complete
    theorem QuantumBlockEncoding.Robin.warmRobinFigure4BulkControlInput_indicator
  (slot : Fin 8) (indicator : Fin 2) :
  QuantumBlockEncoding.Robin.warmRobinFigure4BulkControlInput slot
      indicator 3 =
    indicator
    theorem QuantumBlockEncoding.Robin.warmRobinFigure4BulkControlInput_indicator
  (slot : Fin 8) (indicator : Fin 2) :
  QuantumBlockEncoding.Robin.warmRobinFigure4BulkControlInput
      slot indicator 3 =
    indicator
Theorem10.7.33
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin figure 4 boundary control slot 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/Figure4Loaders.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.7.33●1 theorem
  • theoremdefined in QuantumBlockEncoding/Robin/Figure4Loaders.lean
    complete
    theorem QuantumBlockEncoding.Robin.warmRobinFigure4BoundaryControlSlot_input
  (slot column : Fin 8) (indicator : Fin 2) :
  QuantumBlockEncoding.Robin.warmRobinFigure4BoundaryControlSlot
      (QuantumBlockEncoding.Robin.warmRobinFigure4BoundaryControlInput
        slot column indicator) =
    slot
    theorem QuantumBlockEncoding.Robin.warmRobinFigure4BoundaryControlSlot_input
  (slot column : Fin 8)
  (indicator : Fin 2) :
  QuantumBlockEncoding.Robin.warmRobinFigure4BoundaryControlSlot
      (QuantumBlockEncoding.Robin.warmRobinFigure4BoundaryControlInput
        slot column indicator) =
    slot
Theorem10.7.34
uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.7.34●1 theorem
  • theoremdefined in QuantumBlockEncoding/Robin/Figure4Loaders.lean
    complete
    theorem QuantumBlockEncoding.Robin.warmRobinFigure4BoundaryControlColumn_input
  (slot column : Fin 8) (indicator : Fin 2) :
  QuantumBlockEncoding.Robin.warmRobinFigure4BoundaryControlColumn
      (QuantumBlockEncoding.Robin.warmRobinFigure4BoundaryControlInput
        slot column indicator) =
    column
    theorem QuantumBlockEncoding.Robin.warmRobinFigure4BoundaryControlColumn_input
  (slot column : Fin 8)
  (indicator : Fin 2) :
  QuantumBlockEncoding.Robin.warmRobinFigure4BoundaryControlColumn
      (QuantumBlockEncoding.Robin.warmRobinFigure4BoundaryControlInput
        slot column indicator) =
    column
Theorem10.7.35
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin figure 4 boundary control 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/Figure4Loaders.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.7.35●1 theorem
  • theoremdefined in QuantumBlockEncoding/Robin/Figure4Loaders.lean
    complete
    theorem QuantumBlockEncoding.Robin.warmRobinFigure4BoundaryControlInput_indicator
  (slot column : Fin 8) (indicator : Fin 2) :
  QuantumBlockEncoding.Robin.warmRobinFigure4BoundaryControlInput slot
      column indicator 6 =
    indicator
    theorem QuantumBlockEncoding.Robin.warmRobinFigure4BoundaryControlInput_indicator
  (slot column : Fin 8)
  (indicator : Fin 2) :
  QuantumBlockEncoding.Robin.warmRobinFigure4BoundaryControlInput
      slot column indicator 6 =
    indicator
Theorem10.7.36
uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.7.36●1 theorem
  • theoremdefined in QuantumBlockEncoding/Robin/Figure4Loaders.lean
    complete
    theorem QuantumBlockEncoding.Robin.warmRobinFigure4DerivativeLoader_cleanEntry
  (slot column : Fin 8) :
  have indicator :=
    QuantumBlockEncoding.Robin.warmRobinFigure4IndicatorValue column;
  have bulk :=
    QuantumBlockEncoding.standardRyMatrix
      (QuantumBlockEncoding.Robin.warmRobinFigure4BulkLoaderAngle
          (QuantumBlockEncoding.Robin.warmRobinFigure4BulkControlInput
            slot indicator)).eval;
  have boundary :=
    QuantumBlockEncoding.standardRyMatrix
      (QuantumBlockEncoding.Robin.warmRobinFigure4BoundaryLoaderAngle
          (QuantumBlockEncoding.Robin.warmRobinFigure4BoundaryControlInput
            slot column indicator)).eval;
  (boundary * bulk) 0 0 =
    ↑(QuantumBlockEncoding.Robin.warmRobinFigure4SourceCoefficient slot
        column)
    theorem QuantumBlockEncoding.Robin.warmRobinFigure4DerivativeLoader_cleanEntry
  (slot column : Fin 8) :
  have indicator :=
    QuantumBlockEncoding.Robin.warmRobinFigure4IndicatorValue
      column;
  have bulk :=
    QuantumBlockEncoding.standardRyMatrix
      (QuantumBlockEncoding.Robin.warmRobinFigure4BulkLoaderAngle
          (QuantumBlockEncoding.Robin.warmRobinFigure4BulkControlInput
            slot indicator)).eval;
  have boundary :=
    QuantumBlockEncoding.standardRyMatrix
      (QuantumBlockEncoding.Robin.warmRobinFigure4BoundaryLoaderAngle
          (QuantumBlockEncoding.Robin.warmRobinFigure4BoundaryControlInput
            slot column indicator)).eval;
  (boundary * bulk) 0 0 =
    ↑(QuantumBlockEncoding.Robin.warmRobinFigure4SourceCoefficient
        slot column)