ASPBE Lean Blueprint

4.1. Cold-start transfer operator🔗

Definition4.1.1
uses 0used by 1✓L∃∀N

The cold-start task fixes an 8\times8 rational transfer operator, exact normalizer 1, semantic source text, and no hidden free parameters.

Lean code for Definition4.1.1●1 definition
  • defdefined in QuantumBlockEncoding/ColdStartTransferE1.lean
    complete
    def QuantumBlockEncoding.coldE1QueryTarget :
  QuantumBlockEncoding.QueryOperatorTarget ℚ 8 8
    def QuantumBlockEncoding.coldE1QueryTarget :
  QuantumBlockEncoding.QueryOperatorTarget
    ℚ 8 8
    Operator-first target metadata for the strict cold-start benchmark.
Theorem4.1.2
uses 1used by 1✓L∃∀N

The explicit map on the full 16 basis states is injective and surjective. This closes the finite permutation leaf independently of the block-projection calculation.

Lean code for Theorem4.1.2●1 theorem
  • theoremdefined in QuantumBlockEncoding/ColdStartTransferE1.lean
    complete
    theorem QuantumBlockEncoding.coldE1CandidateImage_permutation_certificate :
  Function.Injective QuantumBlockEncoding.coldE1CandidateImage ∧
    Function.Surjective QuantumBlockEncoding.coldE1CandidateImage
    theorem QuantumBlockEncoding.coldE1CandidateImage_permutation_certificate :
  Function.Injective
      QuantumBlockEncoding.coldE1CandidateImage ∧
    Function.Surjective
      QuantumBlockEncoding.coldE1CandidateImage
Theorem4.1.3
uses 1used by 0✓L∃∀N

On the clean signal slice, the candidate permutation matrix agrees entrywise with the requested cold-start target. Together with the permutation certificate, this supplies the two semantic ingredients used by later full candidates.

Lean code for Theorem4.1.3●1 theorem
  • theoremdefined in QuantumBlockEncoding/ColdStartTransferE1.lean
    complete
    theorem QuantumBlockEncoding.coldE1Candidate_blockProjection :
  QuantumBlockEncoding.coldE1BlockProjection
    QuantumBlockEncoding.coldE1CandidateMatrix
    theorem QuantumBlockEncoding.coldE1Candidate_blockProjection :
  QuantumBlockEncoding.coldE1BlockProjection
    QuantumBlockEncoding.coldE1CandidateMatrix