ResourceComparison.lean🔗

13 explicit public declarations, in source order.

Definition10.22.1

uses 0used by 0✓L∃∀N

Plain-English reading. This type lists the allowed alternatives for “robin semantic tier”; its constructors are the cases that downstream code must handle.

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

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

Lean code for Definition10.22.1●1 definition

inductive(4 constructors)defined in QuantumBlockEncoding/Robin/ResourceComparison.lean

complete

inductive QuantumBlockEncoding.Robin.RobinSemanticTier : Type

inductive QuantumBlockEncoding.Robin.RobinSemanticTier :
  Type

Constructors

paperTranscript :
  QuantumBlockEncoding.Robin.RobinSemanticTier

exactStructuralLCU :
  QuantumBlockEncoding.Robin.RobinSemanticTier

exactLogicalUnitary :
  QuantumBlockEncoding.Robin.RobinSemanticTier

exactPrimitiveCircuit :
  QuantumBlockEncoding.Robin.RobinSemanticTier

Definition10.22.2

uses 0used by 0✓L∃∀N

Plain-English reading. This record groups the data and proof fields needed for “robin resource row”. A proposition-valued field is a requirement until a constructor supplies it.

Formal status. Data contract in the default import surface; proposition-valued fields are obligations, not automatically established facts.

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

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

Lean code for Definition10.22.2●1 definition

structure(5 fields)defined in QuantumBlockEncoding/Robin/ResourceComparison.lean

complete

structure QuantumBlockEncoding.Robin.RobinResourceRow : Type

structure QuantumBlockEncoding.Robin.RobinResourceRow :
  Type

Fields

identity : String

tier : QuantumBlockEncoding.Robin.RobinSemanticTier

convention : String

cost : Option QuantumBlockEncoding.BlockEncodingCost

blockedLeaf : Option String

Definition10.22.3

uses 0used by 0✓L∃∀N

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

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/ResourceComparison.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.22.3●1 definition

defdefined in QuantumBlockEncoding/Robin/ResourceComparison.lean

complete

def QuantumBlockEncoding.Robin.warmRobinPrimitiveConvention : String

def QuantumBlockEncoding.Robin.warmRobinPrimitiveConvention :
  String

Definition10.22.4

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin paper literal transcript resource row”. Historical paper-literal transcript row.

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. Historical paper-literal transcript row. This is not the certified fixed-N8 standard-RY realization, whose exact primitive cost is recorded in 'T3ResourceComparison.lean'.

Declaration kind. def.

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

Lean code for Definition10.22.4●1 definition

defdefined in QuantumBlockEncoding/Robin/ResourceComparison.lean

complete

def QuantumBlockEncoding.Robin.warmRobinPaperLiteralTranscriptResourceRow :
  QuantumBlockEncoding.Robin.RobinResourceRow

def QuantumBlockEncoding.Robin.warmRobinPaperLiteralTranscriptResourceRow :
  QuantumBlockEncoding.Robin.RobinResourceRow

Historical paper-literal transcript row. This is not the certified fixed-N8
standard-RY realization, whose exact primitive cost is recorded in
`T3ResourceComparison.lean`.

Definition10.22.5

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin five shift resource row”.

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

Lean code for Definition10.22.5●1 definition

defdefined in QuantumBlockEncoding/Robin/ResourceComparison.lean

complete

def QuantumBlockEncoding.Robin.warmRobinFiveShiftResourceRow :
  QuantumBlockEncoding.Robin.RobinResourceRow

def QuantumBlockEncoding.Robin.warmRobinFiveShiftResourceRow :
  QuantumBlockEncoding.Robin.RobinResourceRow

Definition10.22.6

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin hadamard 8 resource row”.

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

Lean code for Definition10.22.6●1 definition

defdefined in QuantumBlockEncoding/Robin/ResourceComparison.lean

complete

def QuantumBlockEncoding.Robin.warmRobinHadamard8ResourceRow :
  QuantumBlockEncoding.Robin.RobinResourceRow

def QuantumBlockEncoding.Robin.warmRobinHadamard8ResourceRow :
  QuantumBlockEncoding.Robin.RobinResourceRow

Definition10.22.7

uses 0used by 0✓L∃∀N

Plain-English reading. This type lists the allowed alternatives for “robin comparison”; its constructors are the cases that downstream code must handle.

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

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

Lean code for Definition10.22.7●1 definition

inductive(3 constructors)defined in QuantumBlockEncoding/Robin/ResourceComparison.lean

complete

inductive QuantumBlockEncoding.Robin.RobinComparison : Type

inductive QuantumBlockEncoding.Robin.RobinComparison :
  Type

Constructors

dominates : QuantumBlockEncoding.Robin.RobinComparison

tied : QuantumBlockEncoding.Robin.RobinComparison

incomparable : QuantumBlockEncoding.Robin.RobinComparison

Definition10.22.8

uses 0used by 0✓L∃∀N

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

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/ResourceComparison.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.22.8●1 definition

defdefined in QuantumBlockEncoding/Robin/ResourceComparison.lean

complete

def QuantumBlockEncoding.Robin.compareRobinRows
  (candidate baseline : QuantumBlockEncoding.Robin.RobinResourceRow) :
  QuantumBlockEncoding.Robin.RobinComparison

def QuantumBlockEncoding.Robin.compareRobinRows
  (candidate baseline :
    QuantumBlockEncoding.Robin.RobinResourceRow) :
  QuantumBlockEncoding.Robin.RobinComparison

Theorem10.22.9

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin five shift paper transcript incomparable”; 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/ResourceComparison.lean:71. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.22.9●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/ResourceComparison.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinFiveShift_paperTranscript_incomparable :
  QuantumBlockEncoding.Robin.compareRobinRows
      QuantumBlockEncoding.Robin.warmRobinFiveShiftResourceRow
      QuantumBlockEncoding.Robin.warmRobinPaperLiteralTranscriptResourceRow =
    QuantumBlockEncoding.Robin.RobinComparison.incomparable

theorem QuantumBlockEncoding.Robin.warmRobinFiveShift_paperTranscript_incomparable :
  QuantumBlockEncoding.Robin.compareRobinRows
      QuantumBlockEncoding.Robin.warmRobinFiveShiftResourceRow
      QuantumBlockEncoding.Robin.warmRobinPaperLiteralTranscriptResourceRow =
    QuantumBlockEncoding.Robin.RobinComparison.incomparable

Theorem10.22.10

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin hadamard 8 paper transcript incomparable”; 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/ResourceComparison.lean:78. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.22.10●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/ResourceComparison.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinHadamard8_paperTranscript_incomparable :
  QuantumBlockEncoding.Robin.compareRobinRows
      QuantumBlockEncoding.Robin.warmRobinHadamard8ResourceRow
      QuantumBlockEncoding.Robin.warmRobinPaperLiteralTranscriptResourceRow =
    QuantumBlockEncoding.Robin.RobinComparison.incomparable

theorem QuantumBlockEncoding.Robin.warmRobinHadamard8_paperTranscript_incomparable :
  QuantumBlockEncoding.Robin.compareRobinRows
      QuantumBlockEncoding.Robin.warmRobinHadamard8ResourceRow
      QuantumBlockEncoding.Robin.warmRobinPaperLiteralTranscriptResourceRow =
    QuantumBlockEncoding.Robin.RobinComparison.incomparable

Definition10.22.11

uses 0used by 0✓L∃∀N

Plain-English reading. This abbreviation gives a shorter name to the type or expression used for “warm robin source resource row”. Historical compatibility alias; this row is generic and paper-literal, not the certified fixed-N8 standard-RY source realization.

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

Why it is in this chapter. Paper-facing backend models and concrete Robin-boundary example artifacts.

Technical source note. Historical compatibility alias; this row is generic and paper-literal, not the certified fixed-N8 standard-RY source realization.

Declaration kind. abbrev.

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

Lean code for Definition10.22.11●1 definition

abbrevdefined in QuantumBlockEncoding/Robin/ResourceComparison.lean

complete

abbrev QuantumBlockEncoding.Robin.warmRobinSourceResourceRow :
  QuantumBlockEncoding.Robin.RobinResourceRow

abbrev QuantumBlockEncoding.Robin.warmRobinSourceResourceRow :
  QuantumBlockEncoding.Robin.RobinResourceRow

Historical compatibility alias; this row is generic and paper-literal, not
the certified fixed-N8 standard-RY source realization.

Theorem10.22.12

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin five shift source incomparable”; 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/ResourceComparison.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.22.12●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/ResourceComparison.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinFiveShift_source_incomparable :
  QuantumBlockEncoding.Robin.compareRobinRows
      QuantumBlockEncoding.Robin.warmRobinFiveShiftResourceRow
      QuantumBlockEncoding.Robin.warmRobinSourceResourceRow =
    QuantumBlockEncoding.Robin.RobinComparison.incomparable

theorem QuantumBlockEncoding.Robin.warmRobinFiveShift_source_incomparable :
  QuantumBlockEncoding.Robin.compareRobinRows
      QuantumBlockEncoding.Robin.warmRobinFiveShiftResourceRow
      QuantumBlockEncoding.Robin.warmRobinSourceResourceRow =
    QuantumBlockEncoding.Robin.RobinComparison.incomparable

Theorem10.22.13

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin hadamard 8 source incomparable”; 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/ResourceComparison.lean:95. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.22.13●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/ResourceComparison.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinHadamard8_source_incomparable :
  QuantumBlockEncoding.Robin.compareRobinRows
      QuantumBlockEncoding.Robin.warmRobinHadamard8ResourceRow
      QuantumBlockEncoding.Robin.warmRobinSourceResourceRow =
    QuantumBlockEncoding.Robin.RobinComparison.incomparable

theorem QuantumBlockEncoding.Robin.warmRobinHadamard8_source_incomparable :
  QuantumBlockEncoding.Robin.compareRobinRows
      QuantumBlockEncoding.Robin.warmRobinHadamard8ResourceRow
      QuantumBlockEncoding.Robin.warmRobinSourceResourceRow =
    QuantumBlockEncoding.Robin.RobinComparison.incomparable