ASPBE Lean Blueprint

4.2. Main Case 1 circuits🔗

Theorem4.2.1
uses 0used by 1✓L∃∀N

The logical circuit image, not merely a matrix-table completion, is proved to be a permutation of the full basis.

Lean code for Theorem4.2.1●1 theorem
  • theoremdefined in QuantumBlockEncoding/MainCase.lean
    complete
    theorem QuantumBlockEncoding.mainCaseProCircuitImage_permutation_certificate :
  QuantumBlockEncoding.mainCaseProCircuitImageIsPermutation
    theorem QuantumBlockEncoding.mainCaseProCircuitImage_permutation_certificate :
  QuantumBlockEncoding.mainCaseProCircuitImageIsPermutation
Theorem4.2.2
uses 1used by 1✓L∃∀N

Both row and column Gram matrices of the concrete rational permutation matrix are identities. This is the project-local finite unitarity theorem.

Lean code for Theorem4.2.2●1 theorem
  • theoremdefined in QuantumBlockEncoding/MainCase.lean
    complete
    theorem QuantumBlockEncoding.mainCaseProCircuitMatrix_isRationalOrthogonal :
  QuantumBlockEncoding.BlockEncodingClassics.IsRationalOrthogonal
    QuantumBlockEncoding.mainCaseProCircuitMatrix
    theorem QuantumBlockEncoding.mainCaseProCircuitMatrix_isRationalOrthogonal :
  QuantumBlockEncoding.BlockEncodingClassics.IsRationalOrthogonal
    QuantumBlockEncoding.mainCaseProCircuitMatrix
Theorem4.2.3
uses 1used by 1✓L∃∀N

The circuit matrix has exactly the requested clean block. The proof is separate from orthogonality, so future implementations may change the off-block completion without changing the target theorem.

Lean code for Theorem4.2.3●1 theorem
  • theoremdefined in QuantumBlockEncoding/MainCase.lean
    complete
    theorem QuantumBlockEncoding.mainCaseProCircuit_blockProjection :
  QuantumBlockEncoding.mainCaseProBlockProjection
    QuantumBlockEncoding.mainCaseProCircuitMatrix
    theorem QuantumBlockEncoding.mainCaseProCircuit_blockProjection :
  QuantumBlockEncoding.mainCaseProBlockProjection
    QuantumBlockEncoding.mainCaseProCircuitMatrix
Definition4.2.4
uses 1used by 0✓L∃∀N

The candidate packages the exact target, circuit, schedule, resource record, unitarity proof, and block proof into the public verified-operator interface.

Lean code for Definition4.2.4●1 definition
  • defdefined in QuantumBlockEncoding/MainCase.lean
    complete
    def QuantumBlockEncoding.mainCaseProCircuitVerified :
  QuantumBlockEncoding.VerifiedOperatorBlockEncoding ℚ 3
    def QuantumBlockEncoding.mainCaseProCircuitVerified :
  QuantumBlockEncoding.VerifiedOperatorBlockEncoding
    ℚ 3
    Verified task-local candidate for the advertised Pro transcript image.
Theorem4.2.5
uses 0used by 1✓L∃∀N

The cold construction uses the shared partial-permutation route and exposes its clean-block target equality as a reusable certificate theorem.

Lean code for Theorem4.2.5●1 theorem
  • theoremdefined in QuantumBlockEncoding/MainCase.lean
    complete
    theorem QuantumBlockEncoding.mainCaseColdPartialPerm_clean_eq_target :
  QuantumBlockEncoding.mainCaseColdPartialPermExactCleanBlock.clean.PointwiseEq
    QuantumBlockEncoding.mainCaseColdTarget
    theorem QuantumBlockEncoding.mainCaseColdPartialPerm_clean_eq_target :
  QuantumBlockEncoding.mainCaseColdPartialPermExactCleanBlock.clean.PointwiseEq
    QuantumBlockEncoding.mainCaseColdTarget
Definition4.2.6
uses 1used by 0✓L∃∀N

The reusable exact block is promoted only after the full candidate supplies its unitary and resource-level data.

Lean code for Definition4.2.6●1 definition
  • defdefined in QuantumBlockEncoding/MainCase.lean
    complete
    def QuantumBlockEncoding.mainCaseColdPartialPermVerified :
  QuantumBlockEncoding.VerifiedOperatorBlockEncoding ℚ 3
    def QuantumBlockEncoding.mainCaseColdPartialPermVerified :
  QuantumBlockEncoding.VerifiedOperatorBlockEncoding
    ℚ 3
    Verified COLD block-encoding package for the transfer operator at the current
finite-permutation semantic tier.