QuantumBlockEncoding/Robin/ResourceComparison.lean

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

inductive RobinSemanticTier where
  | paperTranscript
  | exactStructuralLCU
  | exactLogicalUnitary
  | exactPrimitiveCircuit
deriving Repr, DecidableEq

commit-pinned source · Verso Blueprint panel

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.

structure RobinResourceRow where
  identity : String
  tier : RobinSemanticTier
  convention : String
  cost : Option BlockEncodingCost
  blockedLeaf : Option String
deriving Repr, DecidableEq

commit-pinned source · Verso Blueprint panel

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

def warmRobinPrimitiveConvention : String :=
  "logical one-qubit rotations plus CNOT; SWAP is three CNOTs; all truth-table logic, PREPARE, SELECT, and uncompute are expanded"

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

commit-pinned source · Verso Blueprint panel

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

def warmRobinPaperLiteralTranscriptResourceRow : RobinResourceRow where
  identity := "paper-literal-unexpanded-transcript"
  tier := .paperTranscript
  convention := warmRobinPrimitiveConvention
  cost := none
  blockedLeaf := some
    "arbitrary-n source interpretation and the paper-literal single-arccos convention remain open"

commit-pinned source · Verso Blueprint panel

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

def warmRobinFiveShiftResourceRow : RobinResourceRow where
  identity := "five-shift-weighted-permutation"
  tier := .exactStructuralLCU
  convention := warmRobinPrimitiveConvention
  cost := none
  blockedLeaf := some warmRobinHistoricalStructuralCandidateBlockedLeaf

commit-pinned source · Verso Blueprint panel

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

def warmRobinHadamard8ResourceRow : RobinResourceRow where
  identity := "hadamard-eight-weighted-permutation"
  tier := .exactLogicalUnitary
  convention := warmRobinPrimitiveConvention
  cost := none
  blockedLeaf := none

commit-pinned source · Verso Blueprint panel

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

inductive RobinComparison where
  | dominates
  | tied
  | incomparable
deriving Repr, DecidableEq

commit-pinned source · Verso Blueprint panel

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

noncomputable def compareRobinRows
    (candidate baseline : RobinResourceRow) : RobinComparison := by

commit-pinned source · Verso Blueprint panel

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.

theorem warmRobinFiveShift_paperTranscript_incomparable :
    compareRobinRows warmRobinFiveShiftResourceRow
        warmRobinPaperLiteralTranscriptResourceRow =
      .incomparable := by

commit-pinned source · Verso Blueprint panel

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.

theorem warmRobinHadamard8_paperTranscript_incomparable :
    compareRobinRows warmRobinHadamard8ResourceRow
        warmRobinPaperLiteralTranscriptResourceRow =
      .incomparable := by

commit-pinned source · Verso Blueprint panel

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.

abbrev warmRobinSourceResourceRow : RobinResourceRow :=
  warmRobinPaperLiteralTranscriptResourceRow

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “warm robin five shift source incomparable”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem warmRobinFiveShift_source_incomparable :
    compareRobinRows warmRobinFiveShiftResourceRow warmRobinSourceResourceRow =
      .incomparable :=
  warmRobinFiveShift_paperTranscript_incomparable

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “warm robin hadamard 8 source incomparable”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem warmRobinHadamard8_source_incomparable :
    compareRobinRows warmRobinHadamard8ResourceRow warmRobinSourceResourceRow =
      .incomparable :=
  warmRobinHadamard8_paperTranscript_incomparable

commit-pinned source · Verso Blueprint panel