SourceBaseline.lean🔗

16 explicit public declarations, in source order.

Definition10.24.1

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin printed boundary angle”. Literal angle printed in the source-side formula.

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. Literal angle printed in the source-side formula.

Declaration kind. def.

Source: QuantumBlockEncoding/Robin/SourceBaseline.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.24.1●1 definition

defdefined in QuantumBlockEncoding/Robin/SourceBaseline.lean

complete

def QuantumBlockEncoding.Robin.warmRobinPrintedBoundaryAngle (ratio : ℝ) : ℝ

def QuantumBlockEncoding.Robin.warmRobinPrintedBoundaryAngle
  (ratio : ℝ) : ℝ

Literal angle printed in the source-side formula.

Definition10.24.2

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin standard ry boundary angle”. Angle required by the standard 'Ry(theta)' half-angle 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. Angle required by the standard 'Ry(theta)' half-angle convention.

Declaration kind. def.

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

Lean code for Definition10.24.2●1 definition

defdefined in QuantumBlockEncoding/Robin/SourceBaseline.lean

complete

def QuantumBlockEncoding.Robin.warmRobinStandardRyBoundaryAngle
  (ratio : ℝ) : ℝ

def QuantumBlockEncoding.Robin.warmRobinStandardRyBoundaryAngle
  (ratio : ℝ) : ℝ

Angle required by the standard `Ry(theta)` half-angle convention.

Theorem10.24.3

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.24.3●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/SourceBaseline.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinStandardRyBoundaryAngle_eq_twice_printed
  (ratio : ℝ) :
  QuantumBlockEncoding.Robin.warmRobinStandardRyBoundaryAngle ratio =
    2 * QuantumBlockEncoding.Robin.warmRobinPrintedBoundaryAngle ratio

theorem QuantumBlockEncoding.Robin.warmRobinStandardRyBoundaryAngle_eq_twice_printed
  (ratio : ℝ) :
  QuantumBlockEncoding.Robin.warmRobinStandardRyBoundaryAngle
      ratio =
    2 *
      QuantumBlockEncoding.Robin.warmRobinPrintedBoundaryAngle
        ratio

Definition10.24.4

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin register swap pairs”. The actual logical wire pairs for swapping two three-qubit registers.

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 actual logical wire pairs for swapping two three-qubit registers.

Declaration kind. def.

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

Lean code for Definition10.24.4●1 definition

defdefined in QuantumBlockEncoding/Robin/SourceBaseline.lean

complete

def QuantumBlockEncoding.Robin.warmRobinRegisterSwapPairs : List (ℕ × ℕ)

def QuantumBlockEncoding.Robin.warmRobinRegisterSwapPairs :
  List (ℕ × ℕ)

The actual logical wire pairs for swapping two three-qubit registers.

Definition10.24.5

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin register swap circuit”. Executable transcript fragment: three real SWAPs, never 'swap 0 0'.

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. Executable transcript fragment: three real SWAPs, never 'swap 0 0'.

Declaration kind. def.

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

Lean code for Definition10.24.5●1 definition

defdefined in QuantumBlockEncoding/Robin/SourceBaseline.lean

complete

def QuantumBlockEncoding.Robin.warmRobinRegisterSwapCircuit :
  QuantumBlockEncoding.Circuit

def QuantumBlockEncoding.Robin.warmRobinRegisterSwapCircuit :
  QuantumBlockEncoding.Circuit

Executable transcript fragment: three real SWAPs, never `swap 0 0`.

Theorem10.24.6

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin register swap circuit gate list”; 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/SourceBaseline.lean:36. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.24.6●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/SourceBaseline.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinRegisterSwapCircuit_gateList :
  QuantumBlockEncoding.Robin.warmRobinRegisterSwapCircuit =
    [QuantumBlockEncoding.Gate.swap 0 3,
      QuantumBlockEncoding.Gate.swap 1 4,
      QuantumBlockEncoding.Gate.swap 2 5]

theorem QuantumBlockEncoding.Robin.warmRobinRegisterSwapCircuit_gateList :
  QuantumBlockEncoding.Robin.warmRobinRegisterSwapCircuit =
    [QuantumBlockEncoding.Gate.swap 0 3,
      QuantumBlockEncoding.Gate.swap 1 4,
      QuantumBlockEncoding.Gate.swap 2 5]

Theorem10.24.7

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin register swap circuit length”; 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/SourceBaseline.lean:41. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.24.7●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/SourceBaseline.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinRegisterSwapCircuit_length :
  List.length QuantumBlockEncoding.Robin.warmRobinRegisterSwapCircuit =
    3

theorem QuantumBlockEncoding.Robin.warmRobinRegisterSwapCircuit_length :
  List.length
      QuantumBlockEncoding.Robin.warmRobinRegisterSwapCircuit =
    3

Definition10.24.8

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin register swap wire”. Fixed wire-index action induced by the register swap.

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. Fixed wire-index action induced by the register swap.

Declaration kind. def.

Source: QuantumBlockEncoding/Robin/SourceBaseline.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.24.8●1 definition

defdefined in QuantumBlockEncoding/Robin/SourceBaseline.lean

complete

def QuantumBlockEncoding.Robin.warmRobinRegisterSwapWire (wire : Fin 6) :
  Fin 6

def QuantumBlockEncoding.Robin.warmRobinRegisterSwapWire
  (wire : Fin 6) : Fin 6

Fixed wire-index action induced by the register swap.

Theorem10.24.9

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin register swap wire involution”; 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/SourceBaseline.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.24.9●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/SourceBaseline.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinRegisterSwapWire_involution
  (wire : Fin 6) :
  QuantumBlockEncoding.Robin.warmRobinRegisterSwapWire
      (QuantumBlockEncoding.Robin.warmRobinRegisterSwapWire wire) =
    wire

theorem QuantumBlockEncoding.Robin.warmRobinRegisterSwapWire_involution
  (wire : Fin 6) :
  QuantumBlockEncoding.Robin.warmRobinRegisterSwapWire
      (QuantumBlockEncoding.Robin.warmRobinRegisterSwapWire
        wire) =
    wire

Theorem10.24.10

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.24.10●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/SourceBaseline.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinRegisterSwapWire_bijective :
  Function.Bijective
    QuantumBlockEncoding.Robin.warmRobinRegisterSwapWire

theorem QuantumBlockEncoding.Robin.warmRobinRegisterSwapWire_bijective :
  Function.Bijective
    QuantumBlockEncoding.Robin.warmRobinRegisterSwapWire

Definition10.24.11

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin generic source open contracts”. Obligations outside the fixed benchmark: arbitrary size and literal-source routes.

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. Obligations outside the fixed benchmark: arbitrary size and literal-source routes.

Declaration kind. def.

Source: QuantumBlockEncoding/Robin/SourceBaseline.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.24.11●1 definition

defdefined in QuantumBlockEncoding/Robin/SourceBaseline.lean

complete

def QuantumBlockEncoding.Robin.warmRobinGenericSourceOpenContracts :
  List String

def QuantumBlockEncoding.Robin.warmRobinGenericSourceOpenContracts :
  List String

Obligations outside the fixed benchmark: arbitrary size and literal-source routes.

Theorem10.24.12

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin generic source open contracts nonempty”; 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/SourceBaseline.lean:73. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.24.12●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/SourceBaseline.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinGenericSourceOpenContracts_nonempty :
  QuantumBlockEncoding.Robin.warmRobinGenericSourceOpenContracts ≠ []

theorem QuantumBlockEncoding.Robin.warmRobinGenericSourceOpenContracts_nonempty :
  QuantumBlockEncoding.Robin.warmRobinGenericSourceOpenContracts ≠
    []

Definition10.24.13

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin fixed n 8 source open contracts”. The fixed-N8, f=1, standard-RY-corrected source route is closed.

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 fixed-N8, f=1, standard-RY-corrected source route is closed.

Declaration kind. def.

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

Lean code for Definition10.24.13●1 definition

defdefined in QuantumBlockEncoding/Robin/SourceBaseline.lean

complete

def QuantumBlockEncoding.Robin.warmRobinFixedN8SourceOpenContracts :
  List String

def QuantumBlockEncoding.Robin.warmRobinFixedN8SourceOpenContracts :
  List String

The fixed-N8, f=1, standard-RY-corrected source route is closed.

Theorem10.24.14

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin fixed n 8 source open contracts eq nil”; 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/SourceBaseline.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.24.14●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/SourceBaseline.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinFixedN8SourceOpenContracts_eq_nil :
  QuantumBlockEncoding.Robin.warmRobinFixedN8SourceOpenContracts = []

theorem QuantumBlockEncoding.Robin.warmRobinFixedN8SourceOpenContracts_eq_nil :
  QuantumBlockEncoding.Robin.warmRobinFixedN8SourceOpenContracts =
    []

Definition10.24.15

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 open contracts”. Historical compatibility alias for the generic, arbitrary-n and paper-literal obligations.

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 for the generic, arbitrary-n and paper-literal obligations. It does not describe the certified fixed-N8 route.

Declaration kind. abbrev.

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

Lean code for Definition10.24.15●1 definition

abbrevdefined in QuantumBlockEncoding/Robin/SourceBaseline.lean

complete

abbrev QuantumBlockEncoding.Robin.warmRobinSourceOpenContracts : List String

abbrev QuantumBlockEncoding.Robin.warmRobinSourceOpenContracts :
  List String

Historical compatibility alias for the generic, arbitrary-n and
paper-literal obligations. It does not describe the certified fixed-N8 route.

Theorem10.24.16

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.24.16●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/SourceBaseline.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinSourceOpenContracts_nonempty :
  QuantumBlockEncoding.Robin.warmRobinSourceOpenContracts ≠ []

theorem QuantumBlockEncoding.Robin.warmRobinSourceOpenContracts_nonempty :
  QuantumBlockEncoding.Robin.warmRobinSourceOpenContracts ≠
    []