10.55. QuantumBlockEncoding/StatePreparationPaperEntryCertificates.lean🔗

16 explicit public declarations, in source order.

Definition10.55.1

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “mottonen conditional angles”.

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, source-specific Hermite constructions, and concrete State Preparation / Robin 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/StatePreparationPaperEntryCertificates.lean:43. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition10.55.1●1 definition

defdefined in QuantumBlockEncoding/StatePreparationPaperEntryCertificates.lean

complete

def QuantumBlockEncoding.StatePreparationPaperEntryCertificates.mottonenConditionalAngles
  (bits : QuantumBlockEncoding.PrimitiveBasis 1) :
  QuantumBlockEncoding.ExactAngle

def QuantumBlockEncoding.StatePreparationPaperEntryCertificates.mottonenConditionalAngles
  (bits :
    QuantumBlockEncoding.PrimitiveBasis
      1) :
  QuantumBlockEncoding.ExactAngle

Definition10.55.2

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “mottonen dense ucry 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, source-specific Hermite constructions, and concrete State Preparation / Robin 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/StatePreparationPaperEntryCertificates.lean:46. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition10.55.2●1 definition

defdefined in QuantumBlockEncoding/StatePreparationPaperEntryCertificates.lean

complete

def QuantumBlockEncoding.StatePreparationPaperEntryCertificates.mottonenDenseUcryCircuit :
  QuantumBlockEncoding.PrimitiveCircuit 2

def QuantumBlockEncoding.StatePreparationPaperEntryCertificates.mottonenDenseUcryCircuit :
  QuantumBlockEncoding.PrimitiveCircuit 2

Theorem10.55.3

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “mottonen dense ucry entry zero of context ne”; 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, source-specific Hermite constructions, and concrete State Preparation / Robin 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/StatePreparationPaperEntryCertificates.lean:50. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.55.3●1 theorem

theoremdefined in QuantumBlockEncoding/StatePreparationPaperEntryCertificates.lean

complete

theorem QuantumBlockEncoding.StatePreparationPaperEntryCertificates.mottonenDenseUcry_entry_zero_of_context_ne
  (row column : Fin (QuantumBlockEncoding.gridSize 2))
  (contextNe :
    ((QuantumBlockEncoding.splitPrimitiveWire 0)
          (QuantumBlockEncoding.StatePreparationBenchmarks.primitiveLEBits
            2 row)).2 ≠
      ((QuantumBlockEncoding.splitPrimitiveWire 0)
          (QuantumBlockEncoding.StatePreparationBenchmarks.primitiveLEBits
            2 column)).2) :
  QuantumBlockEncoding.StatePreparationBenchmarks.evalPrimitiveCircuitLE
      QuantumBlockEncoding.StatePreparationPaperEntryCertificates.mottonenDenseUcryCircuit
      row column =
    0

theorem QuantumBlockEncoding.StatePreparationPaperEntryCertificates.mottonenDenseUcry_entry_zero_of_context_ne
  (row column :
    Fin (QuantumBlockEncoding.gridSize 2))
  (contextNe :
    ((QuantumBlockEncoding.splitPrimitiveWire
            0)
          (QuantumBlockEncoding.StatePreparationBenchmarks.primitiveLEBits
            2 row)).2 ≠
      ((QuantumBlockEncoding.splitPrimitiveWire
            0)
          (QuantumBlockEncoding.StatePreparationBenchmarks.primitiveLEBits
            2 column)).2) :
  QuantumBlockEncoding.StatePreparationBenchmarks.evalPrimitiveCircuitLE
      QuantumBlockEncoding.StatePreparationPaperEntryCertificates.mottonenDenseUcryCircuit
      row column =
    0

Theorem10.55.4

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “mottonen dense ucry entry 00”; 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, source-specific Hermite constructions, and concrete State Preparation / Robin 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/StatePreparationPaperEntryCertificates.lean:60. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.55.4●1 theorem

theoremdefined in QuantumBlockEncoding/StatePreparationPaperEntryCertificates.lean

complete

theorem QuantumBlockEncoding.StatePreparationPaperEntryCertificates.mottonenDenseUcry_entry_00 :
  QuantumBlockEncoding.StatePreparationBenchmarks.evalPrimitiveCircuitLE
      QuantumBlockEncoding.StatePreparationPaperEntryCertificates.mottonenDenseUcryCircuit
      0 0 =
    3 / 5

theorem QuantumBlockEncoding.StatePreparationPaperEntryCertificates.mottonenDenseUcry_entry_00 :
  QuantumBlockEncoding.StatePreparationBenchmarks.evalPrimitiveCircuitLE
      QuantumBlockEncoding.StatePreparationPaperEntryCertificates.mottonenDenseUcryCircuit
      0 0 =
    3 / 5

Theorem10.55.5

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “mottonen dense ucry entry 10”; 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, source-specific Hermite constructions, and concrete State Preparation / Robin 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/StatePreparationPaperEntryCertificates.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.55.5●1 theorem

theoremdefined in QuantumBlockEncoding/StatePreparationPaperEntryCertificates.lean

complete

theorem QuantumBlockEncoding.StatePreparationPaperEntryCertificates.mottonenDenseUcry_entry_10 :
  QuantumBlockEncoding.StatePreparationBenchmarks.evalPrimitiveCircuitLE
      QuantumBlockEncoding.StatePreparationPaperEntryCertificates.mottonenDenseUcryCircuit
      1 0 =
    4 / 5

theorem QuantumBlockEncoding.StatePreparationPaperEntryCertificates.mottonenDenseUcry_entry_10 :
  QuantumBlockEncoding.StatePreparationBenchmarks.evalPrimitiveCircuitLE
      QuantumBlockEncoding.StatePreparationPaperEntryCertificates.mottonenDenseUcryCircuit
      1 0 =
    4 / 5

Theorem10.55.6

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “mottonen dense ucry entry 22”; 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, source-specific Hermite constructions, and concrete State Preparation / Robin 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/StatePreparationPaperEntryCertificates.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.55.6●1 theorem

theoremdefined in QuantumBlockEncoding/StatePreparationPaperEntryCertificates.lean

complete

theorem QuantumBlockEncoding.StatePreparationPaperEntryCertificates.mottonenDenseUcry_entry_22 :
  QuantumBlockEncoding.StatePreparationBenchmarks.evalPrimitiveCircuitLE
      QuantumBlockEncoding.StatePreparationPaperEntryCertificates.mottonenDenseUcryCircuit
      2 2 =
    5 / 13

theorem QuantumBlockEncoding.StatePreparationPaperEntryCertificates.mottonenDenseUcry_entry_22 :
  QuantumBlockEncoding.StatePreparationBenchmarks.evalPrimitiveCircuitLE
      QuantumBlockEncoding.StatePreparationPaperEntryCertificates.mottonenDenseUcryCircuit
      2 2 =
    5 / 13

Theorem10.55.7

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “mottonen dense ucry entry 32”; 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, source-specific Hermite constructions, and concrete State Preparation / Robin 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/StatePreparationPaperEntryCertificates.lean:90. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.55.7●1 theorem

theoremdefined in QuantumBlockEncoding/StatePreparationPaperEntryCertificates.lean

complete

theorem QuantumBlockEncoding.StatePreparationPaperEntryCertificates.mottonenDenseUcry_entry_32 :
  QuantumBlockEncoding.StatePreparationBenchmarks.evalPrimitiveCircuitLE
      QuantumBlockEncoding.StatePreparationPaperEntryCertificates.mottonenDenseUcryCircuit
      3 2 =
    12 / 13

theorem QuantumBlockEncoding.StatePreparationPaperEntryCertificates.mottonenDenseUcry_entry_32 :
  QuantumBlockEncoding.StatePreparationBenchmarks.evalPrimitiveCircuitLE
      QuantumBlockEncoding.StatePreparationPaperEntryCertificates.mottonenDenseUcryCircuit
      3 2 =
    12 / 13

Definition10.55.8

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “sparse control wire”.

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, source-specific Hermite constructions, and concrete State Preparation / Robin 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/StatePreparationPaperEntryCertificates.lean:100. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition10.55.8●1 definition

defdefined in QuantumBlockEncoding/StatePreparationPaperEntryCertificates.lean

complete

def QuantumBlockEncoding.StatePreparationPaperEntryCertificates.sparseControlWire :
  Fin 1 → Fin 3

def QuantumBlockEncoding.StatePreparationPaperEntryCertificates.sparseControlWire :
  Fin 1 → Fin 3

Theorem10.55.9

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “sparse control wire 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, source-specific Hermite constructions, and concrete State Preparation / Robin 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/StatePreparationPaperEntryCertificates.lean:102. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.55.9●1 theorem

theoremdefined in QuantumBlockEncoding/StatePreparationPaperEntryCertificates.lean

complete

theorem QuantumBlockEncoding.StatePreparationPaperEntryCertificates.sparseControlWire_ne_target
  (control : Fin 1) :
  QuantumBlockEncoding.StatePreparationPaperEntryCertificates.sparseControlWire
      control ≠
    1

theorem QuantumBlockEncoding.StatePreparationPaperEntryCertificates.sparseControlWire_ne_target
  (control : Fin 1) :
  QuantumBlockEncoding.StatePreparationPaperEntryCertificates.sparseControlWire
      control ≠
    1

Definition10.55.10

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “sparse conditional angles”.

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, source-specific Hermite constructions, and concrete State Preparation / Robin 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/StatePreparationPaperEntryCertificates.lean:108. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition10.55.10●1 definition

defdefined in QuantumBlockEncoding/StatePreparationPaperEntryCertificates.lean

complete

def QuantumBlockEncoding.StatePreparationPaperEntryCertificates.sparseConditionalAngles
  (bits : QuantumBlockEncoding.PrimitiveBasis 1) :
  QuantumBlockEncoding.ExactAngle

def QuantumBlockEncoding.StatePreparationPaperEntryCertificates.sparseConditionalAngles
  (bits :
    QuantumBlockEncoding.PrimitiveBasis
      1) :
  QuantumBlockEncoding.ExactAngle

Definition10.55.11

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “sparse pruned ucry 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, source-specific Hermite constructions, and concrete State Preparation / Robin 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/StatePreparationPaperEntryCertificates.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.55.11●1 definition

defdefined in QuantumBlockEncoding/StatePreparationPaperEntryCertificates.lean

complete

def QuantumBlockEncoding.StatePreparationPaperEntryCertificates.sparsePrunedUcryCircuit :
  QuantumBlockEncoding.PrimitiveCircuit 3

def QuantumBlockEncoding.StatePreparationPaperEntryCertificates.sparsePrunedUcryCircuit :
  QuantumBlockEncoding.PrimitiveCircuit 3

Theorem10.55.12

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “sparse pruned ucry entry zero of context ne”; 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, source-specific Hermite constructions, and concrete State Preparation / Robin 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/StatePreparationPaperEntryCertificates.lean:115. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.55.12●1 theorem

theoremdefined in QuantumBlockEncoding/StatePreparationPaperEntryCertificates.lean

complete

theorem QuantumBlockEncoding.StatePreparationPaperEntryCertificates.sparsePrunedUcry_entry_zero_of_context_ne
  (row column : Fin (QuantumBlockEncoding.gridSize 3))
  (contextNe :
    ((QuantumBlockEncoding.splitPrimitiveWire 1)
          (QuantumBlockEncoding.StatePreparationBenchmarks.primitiveLEBits
            3 row)).2 ≠
      ((QuantumBlockEncoding.splitPrimitiveWire 1)
          (QuantumBlockEncoding.StatePreparationBenchmarks.primitiveLEBits
            3 column)).2) :
  QuantumBlockEncoding.StatePreparationBenchmarks.evalPrimitiveCircuitLE
      QuantumBlockEncoding.StatePreparationPaperEntryCertificates.sparsePrunedUcryCircuit
      row column =
    0

theorem QuantumBlockEncoding.StatePreparationPaperEntryCertificates.sparsePrunedUcry_entry_zero_of_context_ne
  (row column :
    Fin (QuantumBlockEncoding.gridSize 3))
  (contextNe :
    ((QuantumBlockEncoding.splitPrimitiveWire
            1)
          (QuantumBlockEncoding.StatePreparationBenchmarks.primitiveLEBits
            3 row)).2 ≠
      ((QuantumBlockEncoding.splitPrimitiveWire
            1)
          (QuantumBlockEncoding.StatePreparationBenchmarks.primitiveLEBits
            3 column)).2) :
  QuantumBlockEncoding.StatePreparationBenchmarks.evalPrimitiveCircuitLE
      QuantumBlockEncoding.StatePreparationPaperEntryCertificates.sparsePrunedUcryCircuit
      row column =
    0

Theorem10.55.13

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “sparse pruned ucry entry 00”; 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, source-specific Hermite constructions, and concrete State Preparation / Robin 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/StatePreparationPaperEntryCertificates.lean:125. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.55.13●1 theorem

theoremdefined in QuantumBlockEncoding/StatePreparationPaperEntryCertificates.lean

complete

theorem QuantumBlockEncoding.StatePreparationPaperEntryCertificates.sparsePrunedUcry_entry_00 :
  QuantumBlockEncoding.StatePreparationBenchmarks.evalPrimitiveCircuitLE
      QuantumBlockEncoding.StatePreparationPaperEntryCertificates.sparsePrunedUcryCircuit
      0 0 =
    3 / 5

theorem QuantumBlockEncoding.StatePreparationPaperEntryCertificates.sparsePrunedUcry_entry_00 :
  QuantumBlockEncoding.StatePreparationBenchmarks.evalPrimitiveCircuitLE
      QuantumBlockEncoding.StatePreparationPaperEntryCertificates.sparsePrunedUcryCircuit
      0 0 =
    3 / 5

Theorem10.55.14

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “sparse pruned ucry entry 20”; 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, source-specific Hermite constructions, and concrete State Preparation / Robin 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/StatePreparationPaperEntryCertificates.lean:135. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.55.14●1 theorem

theoremdefined in QuantumBlockEncoding/StatePreparationPaperEntryCertificates.lean

complete

theorem QuantumBlockEncoding.StatePreparationPaperEntryCertificates.sparsePrunedUcry_entry_20 :
  QuantumBlockEncoding.StatePreparationBenchmarks.evalPrimitiveCircuitLE
      QuantumBlockEncoding.StatePreparationPaperEntryCertificates.sparsePrunedUcryCircuit
      2 0 =
    4 / 5

theorem QuantumBlockEncoding.StatePreparationPaperEntryCertificates.sparsePrunedUcry_entry_20 :
  QuantumBlockEncoding.StatePreparationBenchmarks.evalPrimitiveCircuitLE
      QuantumBlockEncoding.StatePreparationPaperEntryCertificates.sparsePrunedUcryCircuit
      2 0 =
    4 / 5

Theorem10.55.15

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “sparse pruned ucry entry 44”; 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, source-specific Hermite constructions, and concrete State Preparation / Robin 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/StatePreparationPaperEntryCertificates.lean:145. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.55.15●1 theorem

theoremdefined in QuantumBlockEncoding/StatePreparationPaperEntryCertificates.lean

complete

theorem QuantumBlockEncoding.StatePreparationPaperEntryCertificates.sparsePrunedUcry_entry_44 :
  QuantumBlockEncoding.StatePreparationBenchmarks.evalPrimitiveCircuitLE
      QuantumBlockEncoding.StatePreparationPaperEntryCertificates.sparsePrunedUcryCircuit
      4 4 =
    1

theorem QuantumBlockEncoding.StatePreparationPaperEntryCertificates.sparsePrunedUcry_entry_44 :
  QuantumBlockEncoding.StatePreparationBenchmarks.evalPrimitiveCircuitLE
      QuantumBlockEncoding.StatePreparationPaperEntryCertificates.sparsePrunedUcryCircuit
      4 4 =
    1

Theorem10.55.16

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “sparse pruned ucry entry 64”; 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, source-specific Hermite constructions, and concrete State Preparation / Robin 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/StatePreparationPaperEntryCertificates.lean:153. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.55.16●1 theorem

theoremdefined in QuantumBlockEncoding/StatePreparationPaperEntryCertificates.lean

complete

theorem QuantumBlockEncoding.StatePreparationPaperEntryCertificates.sparsePrunedUcry_entry_64 :
  QuantumBlockEncoding.StatePreparationBenchmarks.evalPrimitiveCircuitLE
      QuantumBlockEncoding.StatePreparationPaperEntryCertificates.sparsePrunedUcryCircuit
      6 4 =
    0

theorem QuantumBlockEncoding.StatePreparationPaperEntryCertificates.sparsePrunedUcry_entry_64 :
  QuantumBlockEncoding.StatePreparationBenchmarks.evalPrimitiveCircuitLE
      QuantumBlockEncoding.StatePreparationPaperEntryCertificates.sparsePrunedUcryCircuit
      6 4 =
    0