10.35. QuantumBlockEncoding/RobinEvolution.lean🔗

18 explicit public declarations, in source order.

Definition10.35.1

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin target”. The fixed eight-dimensional homogeneous-Robin benchmark matrix.

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 eight-dimensional homogeneous-Robin benchmark matrix.

Declaration kind. def.

Source: QuantumBlockEncoding/RobinEvolution.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.35.1●1 definition

defdefined in QuantumBlockEncoding/RobinEvolution.lean

complete

def QuantumBlockEncoding.RobinEvolution.warmRobinTarget :
  QuantumBlockEncoding.Matrix 8 8 ℚ

def QuantumBlockEncoding.RobinEvolution.warmRobinTarget :
  QuantumBlockEncoding.Matrix 8 8 ℚ

The fixed eight-dimensional homogeneous-Robin benchmark matrix.

Definition10.35.2

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin normalizer”. Exact normalizer frozen by the warm/cold comparison contract.

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. Exact normalizer frozen by the warm/cold comparison contract.

Declaration kind. def.

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

Lean code for Definition10.35.2●1 definition

defdefined in QuantumBlockEncoding/RobinEvolution.lean

complete

def QuantumBlockEncoding.RobinEvolution.warmRobinNormalizer : ℚ

def QuantumBlockEncoding.RobinEvolution.warmRobinNormalizer :
  ℚ

Exact normalizer frozen by the warm/cold comparison contract.

Definition10.35.3

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin clean signal index”. The clean signal basis index is zero.

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 clean signal basis index is zero.

Declaration kind. def.

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

Lean code for Definition10.35.3●1 definition

defdefined in QuantumBlockEncoding/RobinEvolution.lean

complete

def QuantumBlockEncoding.RobinEvolution.warmRobinCleanSignalIndex : ℕ

def QuantumBlockEncoding.RobinEvolution.warmRobinCleanSignalIndex :
  ℕ

The clean signal basis index is zero.

Definition10.35.4

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin signal first index”. Signal-first flattening of a signal index and an eight-dimensional system 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. Signal-first flattening of a signal index and an eight-dimensional system index.

Declaration kind. def.

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

Lean code for Definition10.35.4●1 definition

defdefined in QuantumBlockEncoding/RobinEvolution.lean

complete

def QuantumBlockEncoding.RobinEvolution.warmRobinSignalFirstIndex
  (signal : ℕ) (system : Fin 8) : ℕ

def QuantumBlockEncoding.RobinEvolution.warmRobinSignalFirstIndex
  (signal : ℕ) (system : Fin 8) : ℕ

Signal-first flattening of a signal index and an eight-dimensional system index.

Theorem10.35.5

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin target eq eval robin derivative matrix”; the hypotheses and conclusion in the code panel fix its exact scope. Evaluating the symbolic Robin stencil at homogeneous boundary data gives the fixed rational benchmark entrywise.

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. Evaluating the symbolic Robin stencil at homogeneous boundary data gives the fixed rational benchmark entrywise.

Declaration kind. theorem.

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

Lean code for Theorem10.35.5●1 theorem

theoremdefined in QuantumBlockEncoding/RobinEvolution.lean

complete

theorem QuantumBlockEncoding.RobinEvolution.warmRobinTarget_eq_eval_robinDerivativeMatrix :
  QuantumBlockEncoding.RobinEvolution.warmRobinTarget = fun i j =>
    QuantumBlockEncoding.Coeff.evalWith (fun x => 0)
      (QuantumBlockEncoding.Examples.RobinHeat.robinDerivativeMatrix 3 i
        j)

theorem QuantumBlockEncoding.RobinEvolution.warmRobinTarget_eq_eval_robinDerivativeMatrix :
  QuantumBlockEncoding.RobinEvolution.warmRobinTarget =
    fun i j =>
    QuantumBlockEncoding.Coeff.evalWith
      (fun x => 0)
      (QuantumBlockEncoding.Examples.RobinHeat.robinDerivativeMatrix
        3 i j)

Evaluating the symbolic Robin stencil at homogeneous boundary data gives
the fixed rational benchmark entrywise.

Theorem10.35.6

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin target eq paper eq 9 dimensionless a 1 b 1 zero”; the hypotheses and conclusion in the code panel fix its exact scope. Relation to Guseynov--Huang--Liu Eq.

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. Relation to Guseynov--Huang--Liu Eq. (9). The paper writes the physical finite-difference matrix as 'A_GHL^(9) = Delta x^(-2) * A_tilde', with boundary entries depending on 'A1 * Delta x' and 'B1 * Delta x'. The frozen ASPBE target is the dimensionless stencil 'A_tilde' at 'A1 = B1 = 0'; the inhomogeneous constants 'A2' and 'B2' belong to the source vector rather than this matrix.

Declaration kind. theorem.

Source: QuantumBlockEncoding/RobinEvolution.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.35.6●1 theorem

theoremdefined in QuantumBlockEncoding/RobinEvolution.lean

complete

theorem QuantumBlockEncoding.RobinEvolution.warmRobinTarget_eq_paperEq9_dimensionless_A1_B1_zero :
  QuantumBlockEncoding.RobinEvolution.warmRobinTarget = fun i j =>
    QuantumBlockEncoding.Coeff.evalWith (fun x => 0)
      (QuantumBlockEncoding.Examples.RobinHeat.robinDerivativeMatrix 3 i
        j)

theorem QuantumBlockEncoding.RobinEvolution.warmRobinTarget_eq_paperEq9_dimensionless_A1_B1_zero :
  QuantumBlockEncoding.RobinEvolution.warmRobinTarget =
    fun i j =>
    QuantumBlockEncoding.Coeff.evalWith
      (fun x => 0)
      (QuantumBlockEncoding.Examples.RobinHeat.robinDerivativeMatrix
        3 i j)

Relation to Guseynov--Huang--Liu Eq. (9). The paper writes the physical
finite-difference matrix as `A_GHL^(9) = Delta x^(-2) * A_tilde`, with boundary
entries depending on `A1 * Delta x` and `B1 * Delta x`. The frozen ASPBE target
is the dimensionless stencil `A_tilde` at `A1 = B1 = 0`; the inhomogeneous
constants `A2` and `B2` belong to the source vector rather than this matrix.

Definition10.35.7

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin parameters”. Fixed paper-seeded parameters for the eight-dimensional warm instance.

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 paper-seeded parameters for the eight-dimensional warm instance.

Declaration kind. def.

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

Lean code for Definition10.35.7●1 definition

defdefined in QuantumBlockEncoding/RobinEvolution.lean

complete

def QuantumBlockEncoding.RobinEvolution.warmRobinParameters :
  QuantumBlockEncoding.GHL2025.OneTermRobinParameters

def QuantumBlockEncoding.RobinEvolution.warmRobinParameters :
  QuantumBlockEncoding.GHL2025.OneTermRobinParameters

Fixed paper-seeded parameters for the eight-dimensional warm instance.

Definition10.35.8

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin source layout”. The theorem-level register layout specialized to the warm instance.

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 theorem-level register layout specialized to the warm instance.

Declaration kind. def.

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

Lean code for Definition10.35.8●1 definition

defdefined in QuantumBlockEncoding/RobinEvolution.lean

complete

def QuantumBlockEncoding.RobinEvolution.warmRobinSourceLayout :
  QuantumBlockEncoding.RegisterLayout

def QuantumBlockEncoding.RobinEvolution.warmRobinSourceLayout :
  QuantumBlockEncoding.RegisterLayout

The theorem-level register layout specialized to the warm instance.

Definition10.35.9

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin visible partition”. The visible source register partition specialized to the warm instance.

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 visible source register partition specialized to the warm instance.

Declaration kind. def.

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

Lean code for Definition10.35.9●1 definition

defdefined in QuantumBlockEncoding/RobinEvolution.lean

complete

def QuantumBlockEncoding.RobinEvolution.warmRobinVisiblePartition :
  QuantumBlockEncoding.GHL2025.RobinRegisterPartition

def QuantumBlockEncoding.RobinEvolution.warmRobinVisiblePartition :
  QuantumBlockEncoding.GHL2025.RobinRegisterPartition

The visible source register partition specialized to the warm instance.

Definition10.35.10

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin source circuit”. The source-ordered ten-label paper transcript for the warm instance.

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-ordered ten-label paper transcript for the warm instance. The register SWAP remains a label here; executable semantics live in 'Robin.SourceBaseline.warmRobinRegisterSwapCircuit'.

Declaration kind. def.

Source: QuantumBlockEncoding/RobinEvolution.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.35.10●1 definition

defdefined in QuantumBlockEncoding/RobinEvolution.lean

complete

def QuantumBlockEncoding.RobinEvolution.warmRobinSourceCircuit :
  QuantumBlockEncoding.Circuit

def QuantumBlockEncoding.RobinEvolution.warmRobinSourceCircuit :
  QuantumBlockEncoding.Circuit

The source-ordered ten-label paper transcript for the warm instance.
The register SWAP remains a label here; executable semantics live in
`Robin.SourceBaseline.warmRobinRegisterSwapCircuit`.

Theorem10.35.11

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin source circuit gate list”; the hypotheses and conclusion in the code panel fix its exact scope. The warm adapter preserves the exact source order of all ten blocks.

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 warm adapter preserves the exact source order of all ten blocks.

Declaration kind. theorem.

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

Lean code for Theorem10.35.11●1 theorem

theoremdefined in QuantumBlockEncoding/RobinEvolution.lean

complete

theorem QuantumBlockEncoding.RobinEvolution.warmRobinSourceCircuit_gateList :
  QuantumBlockEncoding.RobinEvolution.warmRobinSourceCircuit =
    [QuantumBlockEncoding.Gate.oracleCall "H_W^(kappa)",
      QuantumBlockEncoding.Gate.oracleCall "U_indic",
      QuantumBlockEncoding.Gate.oracleCall "O_DT^S",
      QuantumBlockEncoding.Gate.oracleCall "Ry_boundary",
      QuantumBlockEncoding.Gate.oracleCall "O_DT^BS",
      QuantumBlockEncoding.Gate.oracleCall "U_indic^dagger",
      QuantumBlockEncoding.Gate.oracleCall "O_f",
      QuantumBlockEncoding.Gate.oracleCall
        "SWAP(two n-qubit registers; paper label only)",
      QuantumBlockEncoding.Gate.oracleCall "(O_D^BS)^dagger",
      QuantumBlockEncoding.Gate.oracleCall "(H_W^(kappa))^dagger"]

theorem QuantumBlockEncoding.RobinEvolution.warmRobinSourceCircuit_gateList :
  QuantumBlockEncoding.RobinEvolution.warmRobinSourceCircuit =
    [QuantumBlockEncoding.Gate.oracleCall
        "H_W^(kappa)",
      QuantumBlockEncoding.Gate.oracleCall
        "U_indic",
      QuantumBlockEncoding.Gate.oracleCall
        "O_DT^S",
      QuantumBlockEncoding.Gate.oracleCall
        "Ry_boundary",
      QuantumBlockEncoding.Gate.oracleCall
        "O_DT^BS",
      QuantumBlockEncoding.Gate.oracleCall
        "U_indic^dagger",
      QuantumBlockEncoding.Gate.oracleCall
        "O_f",
      QuantumBlockEncoding.Gate.oracleCall
        "SWAP(two n-qubit registers; paper label only)",
      QuantumBlockEncoding.Gate.oracleCall
        "(O_D^BS)^dagger",
      QuantumBlockEncoding.Gate.oracleCall
        "(H_W^(kappa))^dagger"]

The warm adapter preserves the exact source order of all ten blocks.

Theorem10.35.12

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin source circuit length”; the hypotheses and conclusion in the code panel fix its exact scope. The source-facing warm transcript contains exactly ten blocks.

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-facing warm transcript contains exactly ten blocks.

Declaration kind. theorem.

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

Lean code for Theorem10.35.12●1 theorem

theoremdefined in QuantumBlockEncoding/RobinEvolution.lean

complete

theorem QuantumBlockEncoding.RobinEvolution.warmRobinSourceCircuit_length :
  List.length
      QuantumBlockEncoding.RobinEvolution.warmRobinSourceCircuit =
    10

theorem QuantumBlockEncoding.RobinEvolution.warmRobinSourceCircuit_length :
  List.length
      QuantumBlockEncoding.RobinEvolution.warmRobinSourceCircuit =
    10

The source-facing warm transcript contains exactly ten blocks.

Theorem10.35.13

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin parameters spec”; the hypotheses and conclusion in the code panel fix its exact scope. Concrete fields of the fixed warm parameter adapter.

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. Concrete fields of the fixed warm parameter adapter.

Declaration kind. theorem.

Source: QuantumBlockEncoding/RobinEvolution.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.35.13●1 theorem

theoremdefined in QuantumBlockEncoding/RobinEvolution.lean

complete

theorem QuantumBlockEncoding.RobinEvolution.warmRobinParameters_spec :
  QuantumBlockEncoding.RobinEvolution.warmRobinParameters.n = 3 ∧
    QuantumBlockEncoding.RobinEvolution.warmRobinParameters.kappa = 7 ∧
      QuantumBlockEncoding.RobinEvolution.warmRobinParameters.functionPieces =
          1 ∧
        QuantumBlockEncoding.RobinEvolution.warmRobinParameters.polynomialDegreeCost =
          1

theorem QuantumBlockEncoding.RobinEvolution.warmRobinParameters_spec :
  QuantumBlockEncoding.RobinEvolution.warmRobinParameters.n =
      3 ∧
    QuantumBlockEncoding.RobinEvolution.warmRobinParameters.kappa =
        7 ∧
      QuantumBlockEncoding.RobinEvolution.warmRobinParameters.functionPieces =
          1 ∧
        QuantumBlockEncoding.RobinEvolution.warmRobinParameters.polynomialDegreeCost =
          1

Concrete fields of the fixed warm parameter adapter.

Theorem10.35.14

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin source layout spec”; the hypotheses and conclusion in the code panel fix its exact scope. The theorem layout is '(system, signal, pure ancilla) = (3, 9, 6)'.

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 theorem layout is '(system, signal, pure ancilla) = (3, 9, 6)'.

Declaration kind. theorem.

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

Lean code for Theorem10.35.14●1 theorem

theoremdefined in QuantumBlockEncoding/RobinEvolution.lean

complete

theorem QuantumBlockEncoding.RobinEvolution.warmRobinSourceLayout_spec :
  QuantumBlockEncoding.RobinEvolution.warmRobinSourceLayout.systemQubits =
      3 ∧
    QuantumBlockEncoding.RobinEvolution.warmRobinSourceLayout.signalQubits =
        9 ∧
      QuantumBlockEncoding.RobinEvolution.warmRobinSourceLayout.pureAncillas =
        6

theorem QuantumBlockEncoding.RobinEvolution.warmRobinSourceLayout_spec :
  QuantumBlockEncoding.RobinEvolution.warmRobinSourceLayout.systemQubits =
      3 ∧
    QuantumBlockEncoding.RobinEvolution.warmRobinSourceLayout.signalQubits =
        9 ∧
      QuantumBlockEncoding.RobinEvolution.warmRobinSourceLayout.pureAncillas =
        6

The theorem layout is `(system, signal, pure ancilla) = (3, 9, 6)`.

Theorem10.35.15

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin visible partition spec”; the hypotheses and conclusion in the code panel fix its exact scope. The visible source partition has widths '(5, 1, 3, 0, 3, 1)'.

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 visible source partition has widths '(5, 1, 3, 0, 3, 1)'.

Declaration kind. theorem.

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

Lean code for Theorem10.35.15●1 theorem

theoremdefined in QuantumBlockEncoding/RobinEvolution.lean

complete

theorem QuantumBlockEncoding.RobinEvolution.warmRobinVisiblePartition_spec :
  QuantumBlockEncoding.RobinEvolution.warmRobinVisiblePartition.mfQubits =
      5 ∧
    QuantumBlockEncoding.RobinEvolution.warmRobinVisiblePartition.indicatorQubit =
        1 ∧
      QuantumBlockEncoding.RobinEvolution.warmRobinVisiblePartition.sparseIndexQubits =
          3 ∧
        QuantumBlockEncoding.RobinEvolution.warmRobinVisiblePartition.odPureAncillaQubits =
            0 ∧
          QuantumBlockEncoding.RobinEvolution.warmRobinVisiblePartition.systemQubits =
              3 ∧
            QuantumBlockEncoding.RobinEvolution.warmRobinVisiblePartition.ancillaQubit =
              1

theorem QuantumBlockEncoding.RobinEvolution.warmRobinVisiblePartition_spec :
  QuantumBlockEncoding.RobinEvolution.warmRobinVisiblePartition.mfQubits =
      5 ∧
    QuantumBlockEncoding.RobinEvolution.warmRobinVisiblePartition.indicatorQubit =
        1 ∧
      QuantumBlockEncoding.RobinEvolution.warmRobinVisiblePartition.sparseIndexQubits =
          3 ∧
        QuantumBlockEncoding.RobinEvolution.warmRobinVisiblePartition.odPureAncillaQubits =
            0 ∧
          QuantumBlockEncoding.RobinEvolution.warmRobinVisiblePartition.systemQubits =
              3 ∧
            QuantumBlockEncoding.RobinEvolution.warmRobinVisiblePartition.ancillaQubit =
              1

The visible source partition has widths `(5, 1, 3, 0, 3, 1)`.

Theorem10.35.16

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin total qubits eq”; the hypotheses and conclusion in the code panel fix its exact scope. The visible source register partition occupies thirteen qubits.

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 visible source register partition occupies thirteen qubits.

Declaration kind. theorem.

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

Lean code for Theorem10.35.16●1 theorem

theoremdefined in QuantumBlockEncoding/RobinEvolution.lean

complete

theorem QuantumBlockEncoding.RobinEvolution.warmRobinTotalQubits_eq :
  QuantumBlockEncoding.GHL2025.oneTermRobinTotalQubits
      QuantumBlockEncoding.RobinEvolution.warmRobinParameters =
    13

theorem QuantumBlockEncoding.RobinEvolution.warmRobinTotalQubits_eq :
  QuantumBlockEncoding.GHL2025.oneTermRobinTotalQubits
      QuantumBlockEncoding.RobinEvolution.warmRobinParameters =
    13

The visible source register partition occupies thirteen qubits.

Theorem10.35.17

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin effective signal qubits eq”; the hypotheses and conclusion in the code panel fix its exact scope. The clean projection covers all ten non-system wires.

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 clean projection covers all ten non-system wires.

Declaration kind. theorem.

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

Lean code for Theorem10.35.17●1 theorem

theoremdefined in QuantumBlockEncoding/RobinEvolution.lean

complete

theorem QuantumBlockEncoding.RobinEvolution.warmRobinEffectiveSignalQubits_eq :
  QuantumBlockEncoding.GHL2025.effectiveRobinSignalQubits
      QuantumBlockEncoding.RobinEvolution.warmRobinParameters =
    10

theorem QuantumBlockEncoding.RobinEvolution.warmRobinEffectiveSignalQubits_eq :
  QuantumBlockEncoding.GHL2025.effectiveRobinSignalQubits
      QuantumBlockEncoding.RobinEvolution.warmRobinParameters =
    10

The clean projection covers all ten non-system wires.

Theorem10.35.18

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin indicator certificate”; the hypotheses and conclusion in the code panel fix its exact scope. The fixed warm indicator and its dagger form one self-inverse permutation pair.

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 fixed warm indicator and its dagger form one self-inverse permutation pair.

Declaration kind. theorem.

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

Lean code for Theorem10.35.18●1 theorem

theoremdefined in QuantumBlockEncoding/RobinEvolution.lean

complete

theorem QuantumBlockEncoding.RobinEvolution.warmRobinIndicatorCertificate :
  (QuantumBlockEncoding.GHL2025.oneTermRobinGate_U_indic_dagger
          QuantumBlockEncoding.RobinEvolution.warmRobinParameters).matrix =
      (QuantumBlockEncoding.GHL2025.oneTermRobinGate_U_indic
          QuantumBlockEncoding.RobinEvolution.warmRobinParameters).matrix ∧
    (∀ (j : ℕ),
        QuantumBlockEncoding.GHL2025.indicatorOracleImage
            QuantumBlockEncoding.RobinEvolution.warmRobinParameters
            (QuantumBlockEncoding.GHL2025.indicatorOracleImage
              QuantumBlockEncoding.RobinEvolution.warmRobinParameters
              j) =
          j) ∧
      (∀
          (i :
            Fin
              (QuantumBlockEncoding.qubitDim
                (QuantumBlockEncoding.GHL2025.oneTermRobinTotalQubits
                  QuantumBlockEncoding.RobinEvolution.warmRobinParameters))),
          ∃ j,
            QuantumBlockEncoding.GHL2025.indicatorOracleMatrix
                  QuantumBlockEncoding.RobinEvolution.warmRobinParameters
                  i j =
                QuantumBlockEncoding.Coeff.rat 1 ∧
              ∀
                (j' :
                  Fin
                    (QuantumBlockEncoding.qubitDim
                      (QuantumBlockEncoding.GHL2025.oneTermRobinTotalQubits
                        QuantumBlockEncoding.RobinEvolution.warmRobinParameters))),
                QuantumBlockEncoding.GHL2025.indicatorOracleMatrix
                      QuantumBlockEncoding.RobinEvolution.warmRobinParameters
                      i j' =
                    QuantumBlockEncoding.Coeff.rat 1 →
                  j' = j) ∧
        ∀
          (j :
            Fin
              (QuantumBlockEncoding.qubitDim
                (QuantumBlockEncoding.GHL2025.oneTermRobinTotalQubits
                  QuantumBlockEncoding.RobinEvolution.warmRobinParameters))),
          ∃ i,
            QuantumBlockEncoding.GHL2025.indicatorOracleMatrix
                  QuantumBlockEncoding.RobinEvolution.warmRobinParameters
                  i j =
                QuantumBlockEncoding.Coeff.rat 1 ∧
              ∀
                (i' :
                  Fin
                    (QuantumBlockEncoding.qubitDim
                      (QuantumBlockEncoding.GHL2025.oneTermRobinTotalQubits
                        QuantumBlockEncoding.RobinEvolution.warmRobinParameters))),
                QuantumBlockEncoding.GHL2025.indicatorOracleMatrix
                      QuantumBlockEncoding.RobinEvolution.warmRobinParameters
                      i' j =
                    QuantumBlockEncoding.Coeff.rat 1 →
                  i' = i

theorem QuantumBlockEncoding.RobinEvolution.warmRobinIndicatorCertificate :
  (QuantumBlockEncoding.GHL2025.oneTermRobinGate_U_indic_dagger
          QuantumBlockEncoding.RobinEvolution.warmRobinParameters).matrix =
      (QuantumBlockEncoding.GHL2025.oneTermRobinGate_U_indic
          QuantumBlockEncoding.RobinEvolution.warmRobinParameters).matrix ∧
    (∀ (j : ℕ),
        QuantumBlockEncoding.GHL2025.indicatorOracleImage
            QuantumBlockEncoding.RobinEvolution.warmRobinParameters
            (QuantumBlockEncoding.GHL2025.indicatorOracleImage
              QuantumBlockEncoding.RobinEvolution.warmRobinParameters
              j) =
          j) ∧
      (∀
          (i :
            Fin
              (QuantumBlockEncoding.qubitDim
                (QuantumBlockEncoding.GHL2025.oneTermRobinTotalQubits
                  QuantumBlockEncoding.RobinEvolution.warmRobinParameters))),
          ∃ j,
            QuantumBlockEncoding.GHL2025.indicatorOracleMatrix
                  QuantumBlockEncoding.RobinEvolution.warmRobinParameters
                  i j =
                QuantumBlockEncoding.Coeff.rat
                  1 ∧
              ∀
                (j' :
                  Fin
                    (QuantumBlockEncoding.qubitDim
                      (QuantumBlockEncoding.GHL2025.oneTermRobinTotalQubits
                        QuantumBlockEncoding.RobinEvolution.warmRobinParameters))),
                QuantumBlockEncoding.GHL2025.indicatorOracleMatrix
                      QuantumBlockEncoding.RobinEvolution.warmRobinParameters
                      i j' =
                    QuantumBlockEncoding.Coeff.rat
                      1 →
                  j' = j) ∧
        ∀
          (j :
            Fin
              (QuantumBlockEncoding.qubitDim
                (QuantumBlockEncoding.GHL2025.oneTermRobinTotalQubits
                  QuantumBlockEncoding.RobinEvolution.warmRobinParameters))),
          ∃ i,
            QuantumBlockEncoding.GHL2025.indicatorOracleMatrix
                  QuantumBlockEncoding.RobinEvolution.warmRobinParameters
                  i j =
                QuantumBlockEncoding.Coeff.rat
                  1 ∧
              ∀
                (i' :
                  Fin
                    (QuantumBlockEncoding.qubitDim
                      (QuantumBlockEncoding.GHL2025.oneTermRobinTotalQubits
                        QuantumBlockEncoding.RobinEvolution.warmRobinParameters))),
                QuantumBlockEncoding.GHL2025.indicatorOracleMatrix
                      QuantumBlockEncoding.RobinEvolution.warmRobinParameters
                      i' j =
                    QuantumBlockEncoding.Coeff.rat
                      1 →
                  i' = i

The fixed warm indicator and its dagger form one self-inverse permutation pair.