PaperSevenAmplitudePrimitive.lean🔗

16 explicit public declarations, in source order.

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

Lean code for Definition10.16.1●1 definition

defdefined in QuantumBlockEncoding/Robin/PaperSevenAmplitudePrimitive.lean

complete

def QuantumBlockEncoding.Robin.warmRobinPaperSevenAmplitudeControlWires :
  Fin 6 → Fin 8

def QuantumBlockEncoding.Robin.warmRobinPaperSevenAmplitudeControlWires :
  Fin 6 → Fin 8

Theorem10.16.2

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.16.2●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/PaperSevenAmplitudePrimitive.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinPaperSevenAmplitudeControlWires_ne_target
  (wire : Fin 6) :
  QuantumBlockEncoding.Robin.warmRobinPaperSevenAmplitudeControlWires
      wire ≠
    6

theorem QuantumBlockEncoding.Robin.warmRobinPaperSevenAmplitudeControlWires_ne_target
  (wire : Fin 6) :
  QuantumBlockEncoding.Robin.warmRobinPaperSevenAmplitudeControlWires
      wire ≠
    6

Definition10.16.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 amplitude 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. def.

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

Lean code for Definition10.16.3●1 definition

defdefined in QuantumBlockEncoding/Robin/PaperSevenAmplitudePrimitive.lean

complete

def QuantumBlockEncoding.Robin.warmRobinPaperSevenAmplitudeSystem
  (bits : QuantumBlockEncoding.PrimitiveBasis 6) : Fin 8

def QuantumBlockEncoding.Robin.warmRobinPaperSevenAmplitudeSystem
  (bits :
    QuantumBlockEncoding.PrimitiveBasis
      6) :
  Fin 8

Definition10.16.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 amplitude selector”.

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

Lean code for Definition10.16.4●1 definition

defdefined in QuantumBlockEncoding/Robin/PaperSevenAmplitudePrimitive.lean

complete

def QuantumBlockEncoding.Robin.warmRobinPaperSevenAmplitudeSelector
  (bits : QuantumBlockEncoding.PrimitiveBasis 6) : Fin 8

def QuantumBlockEncoding.Robin.warmRobinPaperSevenAmplitudeSelector
  (bits :
    QuantumBlockEncoding.PrimitiveBasis
      6) :
  Fin 8

Definition10.16.5

uses 0used by 0✓L∃∀N

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

Lean code for Definition10.16.5●1 definition

defdefined in QuantumBlockEncoding/Robin/PaperSevenAmplitudePrimitive.lean

complete

def QuantumBlockEncoding.Robin.warmRobinPaperSevenAmplitudeAngle
  (bits : QuantumBlockEncoding.PrimitiveBasis 6) :
  QuantumBlockEncoding.ExactAngle

def QuantumBlockEncoding.Robin.warmRobinPaperSevenAmplitudeAngle
  (bits :
    QuantumBlockEncoding.PrimitiveBasis
      6) :
  QuantumBlockEncoding.ExactAngle

Theorem10.16.6

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin paper seven amplitude ry eq rotation”; 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/PaperSevenAmplitudePrimitive.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.16.6●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/PaperSevenAmplitudePrimitive.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinPaperSevenAmplitudeRy_eq_rotation
  (bits : QuantumBlockEncoding.PrimitiveBasis 6) :
  QuantumBlockEncoding.standardRyMatrix
      (QuantumBlockEncoding.Robin.warmRobinPaperSevenAmplitudeAngle
          bits).eval =
    QuantumBlockEncoding.Robin.warmRobinPaperSevenRotation
      (QuantumBlockEncoding.Robin.warmRobinPaperSevenAmplitudeSelector
        bits)
      (QuantumBlockEncoding.Robin.warmRobinPaperSevenAmplitudeSystem
        bits)

theorem QuantumBlockEncoding.Robin.warmRobinPaperSevenAmplitudeRy_eq_rotation
  (bits :
    QuantumBlockEncoding.PrimitiveBasis
      6) :
  QuantumBlockEncoding.standardRyMatrix
      (QuantumBlockEncoding.Robin.warmRobinPaperSevenAmplitudeAngle
          bits).eval =
    QuantumBlockEncoding.Robin.warmRobinPaperSevenRotation
      (QuantumBlockEncoding.Robin.warmRobinPaperSevenAmplitudeSelector
        bits)
      (QuantumBlockEncoding.Robin.warmRobinPaperSevenAmplitudeSystem
        bits)

Definition10.16.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 amplitude context 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/PaperSevenAmplitudePrimitive.lean:58. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition10.16.7●1 definition

defdefined in QuantumBlockEncoding/Robin/PaperSevenAmplitudePrimitive.lean

complete

def QuantumBlockEncoding.Robin.warmRobinPaperSevenAmplitudeContextIndex
  (context : QuantumBlockEncoding.OtherPrimitiveWires 6 → Fin 2) :
  Fin 8 × QuantumBlockEncoding.Robin.WarmRobinPaperSevenFullSystem

def QuantumBlockEncoding.Robin.warmRobinPaperSevenAmplitudeContextIndex
  (context :
    QuantumBlockEncoding.OtherPrimitiveWires
        6 →
      Fin 2) :
  Fin 8 ×
    QuantumBlockEncoding.Robin.WarmRobinPaperSevenFullSystem

Theorem10.16.8

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.16.8●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/PaperSevenAmplitudePrimitive.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinPaperSevenAmplitudeContextIndex_bijective :
  Function.Bijective
    QuantumBlockEncoding.Robin.warmRobinPaperSevenAmplitudeContextIndex

theorem QuantumBlockEncoding.Robin.warmRobinPaperSevenAmplitudeContextIndex_bijective :
  Function.Bijective
    QuantumBlockEncoding.Robin.warmRobinPaperSevenAmplitudeContextIndex

Definition10.16.9

uses 0used by 0✓L∃∀N

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

Lean code for Definition10.16.9●1 definition

defdefined in QuantumBlockEncoding/Robin/PaperSevenAmplitudePrimitive.lean

complete

def QuantumBlockEncoding.Robin.warmRobinPaperSevenAmplitudeContextEquiv :
  (QuantumBlockEncoding.OtherPrimitiveWires 6 → Fin 2) ≃
    Fin 8 × QuantumBlockEncoding.Robin.WarmRobinPaperSevenFullSystem

def QuantumBlockEncoding.Robin.warmRobinPaperSevenAmplitudeContextEquiv :
  (QuantumBlockEncoding.OtherPrimitiveWires
        6 →
      Fin 2) ≃
    Fin 8 ×
      QuantumBlockEncoding.Robin.WarmRobinPaperSevenFullSystem

Theorem10.16.10

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.16.10●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/PaperSevenAmplitudePrimitive.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinPaperSevenAmplitudeContextEquiv_apply
  (context : QuantumBlockEncoding.OtherPrimitiveWires 6 → Fin 2) :
  QuantumBlockEncoding.Robin.warmRobinPaperSevenAmplitudeContextEquiv
      context =
    QuantumBlockEncoding.Robin.warmRobinPaperSevenAmplitudeContextIndex
      context

theorem QuantumBlockEncoding.Robin.warmRobinPaperSevenAmplitudeContextEquiv_apply
  (context :
    QuantumBlockEncoding.OtherPrimitiveWires
        6 →
      Fin 2) :
  QuantumBlockEncoding.Robin.warmRobinPaperSevenAmplitudeContextEquiv
      context =
    QuantumBlockEncoding.Robin.warmRobinPaperSevenAmplitudeContextIndex
      context

Theorem10.16.11

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.16.11●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/PaperSevenAmplitudePrimitive.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinPaperSevenAmplitude_context_iff
  (row column : QuantumBlockEncoding.PrimitiveBasis 8) :
  ((QuantumBlockEncoding.splitPrimitiveWire 6) row).2 =
      ((QuantumBlockEncoding.splitPrimitiveWire 6) column).2 ↔
    (QuantumBlockEncoding.Robin.warmRobinPaperSevenBitsEquiv row).2 =
      (QuantumBlockEncoding.Robin.warmRobinPaperSevenBitsEquiv column).2

theorem QuantumBlockEncoding.Robin.warmRobinPaperSevenAmplitude_context_iff
  (row column :
    QuantumBlockEncoding.PrimitiveBasis
      8) :
  ((QuantumBlockEncoding.splitPrimitiveWire
            6)
          row).2 =
      ((QuantumBlockEncoding.splitPrimitiveWire
            6)
          column).2 ↔
    (QuantumBlockEncoding.Robin.warmRobinPaperSevenBitsEquiv
          row).2 =
      (QuantumBlockEncoding.Robin.warmRobinPaperSevenBitsEquiv
          column).2

Theorem10.16.12

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin paper seven controlled ry eq amplitude lift”; the hypotheses and conclusion in the code panel fix its exact scope. Exact equality between the physical six-control RY block and the logical amplitude lift, including the otherwise dirty 'q7' workspace coordinate.

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 equality between the physical six-control RY block and the logical amplitude lift, including the otherwise dirty 'q7' workspace coordinate.

Declaration kind. theorem.

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

Lean code for Theorem10.16.12●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/PaperSevenAmplitudePrimitive.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinPaperSevenControlledRy_eq_amplitudeLift :
  QuantumBlockEncoding.controlledRyBlockMatrix
      QuantumBlockEncoding.Robin.warmRobinPaperSevenAmplitudeControlWires
      6
      QuantumBlockEncoding.Robin.warmRobinPaperSevenAmplitudeControlWires_ne_target
      QuantumBlockEncoding.Robin.warmRobinPaperSevenAmplitudeAngle =
    (Matrix.reindexAlgEquiv ℂ ℂ
        QuantumBlockEncoding.Robin.warmRobinPaperSevenBitsEquiv.symm)
      (QuantumBlockEncoding.Robin.ComplexLCU.amplitudeLift
        QuantumBlockEncoding.Robin.warmRobinPaperSevenWorkspaceRotation)

theorem QuantumBlockEncoding.Robin.warmRobinPaperSevenControlledRy_eq_amplitudeLift :
  QuantumBlockEncoding.controlledRyBlockMatrix
      QuantumBlockEncoding.Robin.warmRobinPaperSevenAmplitudeControlWires
      6
      QuantumBlockEncoding.Robin.warmRobinPaperSevenAmplitudeControlWires_ne_target
      QuantumBlockEncoding.Robin.warmRobinPaperSevenAmplitudeAngle =
    (Matrix.reindexAlgEquiv ℂ ℂ
        QuantumBlockEncoding.Robin.warmRobinPaperSevenBitsEquiv.symm)
      (QuantumBlockEncoding.Robin.ComplexLCU.amplitudeLift
        QuantumBlockEncoding.Robin.warmRobinPaperSevenWorkspaceRotation)

Exact equality between the physical six-control RY block and the logical
amplitude lift, including the otherwise dirty `q7` workspace coordinate.

Definition10.16.13

uses 0used by 0✓L∃∀N

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

Lean code for Definition10.16.13●1 definition

defdefined in QuantumBlockEncoding/Robin/PaperSevenAmplitudePrimitive.lean

complete

def QuantumBlockEncoding.Robin.warmRobinPaperSevenAmplitudeCircuit :
  QuantumBlockEncoding.PrimitiveCircuit 8

def QuantumBlockEncoding.Robin.warmRobinPaperSevenAmplitudeCircuit :
  QuantumBlockEncoding.PrimitiveCircuit 8

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

Lean code for Definition10.16.14●1 definition

defdefined in QuantumBlockEncoding/Robin/PaperSevenAmplitudePrimitive.lean

complete

def QuantumBlockEncoding.Robin.warmRobinPaperSevenAmplitudeProgram :
  QuantumBlockEncoding.PrimitiveProgram 8

def QuantumBlockEncoding.Robin.warmRobinPaperSevenAmplitudeProgram :
  QuantumBlockEncoding.PrimitiveProgram 8

Theorem10.16.15

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.16.15●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/PaperSevenAmplitudePrimitive.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinPaperSevenAmplitudeProgram_eval :
  QuantumBlockEncoding.evalPrimitiveProgram
      QuantumBlockEncoding.Robin.warmRobinPaperSevenAmplitudeProgram =
    (Matrix.reindexAlgEquiv ℂ ℂ
        QuantumBlockEncoding.Robin.warmRobinPaperSevenBitsEquiv.symm)
      (QuantumBlockEncoding.Robin.ComplexLCU.amplitudeLift
        QuantumBlockEncoding.Robin.warmRobinPaperSevenWorkspaceRotation)

theorem QuantumBlockEncoding.Robin.warmRobinPaperSevenAmplitudeProgram_eval :
  QuantumBlockEncoding.evalPrimitiveProgram
      QuantumBlockEncoding.Robin.warmRobinPaperSevenAmplitudeProgram =
    (Matrix.reindexAlgEquiv ℂ ℂ
        QuantumBlockEncoding.Robin.warmRobinPaperSevenBitsEquiv.symm)
      (QuantumBlockEncoding.Robin.ComplexLCU.amplitudeLift
        QuantumBlockEncoding.Robin.warmRobinPaperSevenWorkspaceRotation)

Theorem10.16.16

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.16.16●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/PaperSevenAmplitudePrimitive.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinPaperSevenAmplitudeProgram_noOracleCalls :
  QuantumBlockEncoding.Robin.warmRobinPaperSevenAmplitudeProgram.resource.oracleCalls =
    0

theorem QuantumBlockEncoding.Robin.warmRobinPaperSevenAmplitudeProgram_noOracleCalls :
  QuantumBlockEncoding.Robin.warmRobinPaperSevenAmplitudeProgram.resource.oracleCalls =
    0