exact finite logical reversible circuit
BE Case 1: finite transfer operator
A concrete non-unitary transfer is embedded in a permutation unitary and improved from (6,5,1,0) to (4,2,1,0).
Lean certified
Example Cases · Block Encoding
Block Encoding example cases
Block-encoding examples and papers: clean-block semantics, oracle access, source constructions, and same-target circuit improvements. Paper-derived cases identify the exact source equation, theorem, figure, table, or section before the ASPBE specialization.
Certified examples
Read the contract, source anchor, proof story, circuit, and Lean evidence
exact finite logical reversible circuit
BE Case 1: isolated cold reconstruction
An isolated route closes the same mathematical contract with its own exact permutation and score (5,5,1,0).
Lean certified
symbolic exact rational family
BE Case 2: cubic diagonal family, cold route
A symbolic exact family theorem replaces finite numerical acceptance with rational Householder certificates for every n.
Lean certified
symbolic exact rational family
BE Case 2: cubic diagonal family, hinted route
A direct hint becomes a short formal route with separate exact Lean roots for the input and output blocks.
Lean certified
Exact primitive source reproductions and certified same-tier winner
GHL Eq. (9) benchmark at N=8 (A1=B1=0)
Lean block-encodes the dimensionless A1=B1=0 specialization of GHL Eq. (9), explicitly distinguishes it from the physical Delta x^{-2} matrix, closes both source realizations and the evolved candidate at the exact primitive level, and certifies the candidate's same-tier improvement.
Lean certified