FixedN3Data.lean🔗

6 explicit public declarations, in source order.

Definition10.13.1

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin integer target”. The integer matrix 'M = 12 A', kept integral for finite decomposition proofs.

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 integer matrix 'M = 12 A', kept integral for finite decomposition proofs.

Declaration kind. def.

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

Lean code for Definition10.13.1●1 definition

defdefined in QuantumBlockEncoding/Robin/FixedN3Data.lean

complete

def QuantumBlockEncoding.Robin.warmRobinIntegerTarget :
  QuantumBlockEncoding.Matrix 8 8 ℤ

def QuantumBlockEncoding.Robin.warmRobinIntegerTarget :
  QuantumBlockEncoding.Matrix 8 8 ℤ

The integer matrix `M = 12 A`, kept integral for finite decomposition proofs.

Definition10.13.2

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin integer target rat”. Rational view of the frozen integer target.

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. Rational view of the frozen integer target.

Declaration kind. def.

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

defdefined in QuantumBlockEncoding/Robin/FixedN3Data.lean

complete

def QuantumBlockEncoding.Robin.warmRobinIntegerTargetRat :
  QuantumBlockEncoding.Matrix 8 8 ℚ

def QuantumBlockEncoding.Robin.warmRobinIntegerTargetRat :
  QuantumBlockEncoding.Matrix 8 8 ℚ

Rational view of the frozen integer target.

Theorem10.13.3

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin integer target eq twelve mul target”; the hypotheses and conclusion in the code panel fix its exact scope. Exact fixed-instance identity 'M = 12 A'.

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. Exact fixed-instance identity 'M = 12 A'.

Declaration kind. theorem.

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

Lean code for Theorem10.13.3●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/FixedN3Data.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinIntegerTarget_eq_twelve_mul_target :
  QuantumBlockEncoding.Robin.warmRobinIntegerTargetRat = fun i j =>
    12 * QuantumBlockEncoding.RobinEvolution.warmRobinTarget i j

theorem QuantumBlockEncoding.Robin.warmRobinIntegerTarget_eq_twelve_mul_target :
  QuantumBlockEncoding.Robin.warmRobinIntegerTargetRat =
    fun i j =>
    12 *
      QuantumBlockEncoding.RobinEvolution.warmRobinTarget
        i j

Exact fixed-instance identity `M = 12 A`.

Theorem10.13.4

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin normalized eq integer div 224”; the hypotheses and conclusion in the code panel fix its exact scope. Exact normalized target identity 'A / (56/3) = M / 224'.

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. Exact normalized target identity 'A / (56/3) = M / 224'.

Declaration kind. theorem.

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

Lean code for Theorem10.13.4●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/FixedN3Data.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobin_normalized_eq_integer_div_224 :
  (fun i j =>
      QuantumBlockEncoding.RobinEvolution.warmRobinTarget i j /
        QuantumBlockEncoding.RobinEvolution.warmRobinNormalizer) =
    fun i j =>
    QuantumBlockEncoding.Robin.warmRobinIntegerTargetRat i j / 224

theorem QuantumBlockEncoding.Robin.warmRobin_normalized_eq_integer_div_224 :
  (fun i j =>
      QuantumBlockEncoding.RobinEvolution.warmRobinTarget
          i j /
        QuantumBlockEncoding.RobinEvolution.warmRobinNormalizer) =
    fun i j =>
    QuantumBlockEncoding.Robin.warmRobinIntegerTargetRat
        i j /
      224

Exact normalized target identity `A / (56/3) = M / 224`.

Definition10.13.5

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin clean embed”. Signal-first clean embedding for the fixed 'signal x system' 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. Signal-first clean embedding for the fixed 'signal x system' convention.

Declaration kind. def.

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

Lean code for Definition10.13.5●1 definition

defdefined in QuantumBlockEncoding/Robin/FixedN3Data.lean

complete

def QuantumBlockEncoding.Robin.warmRobinCleanEmbed (system : Fin 8) :
  Fin (8 * 8)

def QuantumBlockEncoding.Robin.warmRobinCleanEmbed
  (system : Fin 8) : Fin (8 * 8)

Signal-first clean embedding for the fixed `signal x system` convention.

Theorem10.13.6

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin clean embed value”; 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/FixedN3Data.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.13.6●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/FixedN3Data.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinCleanEmbed_value (system : Fin 8) :
  ↑(QuantumBlockEncoding.Robin.warmRobinCleanEmbed system) = ↑system

theorem QuantumBlockEncoding.Robin.warmRobinCleanEmbed_value
  (system : Fin 8) :
  ↑(QuantumBlockEncoding.Robin.warmRobinCleanEmbed
        system) =
    ↑system