4.3. Evolved optimal-control completion
Theorem4.3.1
The evolved child keeps the equality flag and follows it with three parallel bit flips. The reduced active-register map remains a finite permutation.
Lean code for Theorem4.3.1●1 theorem
Associated Lean declarations
Associated Lean declarations
-
theoremdefined in QuantumBlockEncoding/OptimalControl.leancomplete
theorem QuantumBlockEncoding.OptimalControl.evolvedEqFlipImage_isPermutation : QuantumBlockEncoding.OptimalControl.IsPermutation QuantumBlockEncoding.OptimalControl.evolvedEqFlipImage
theorem QuantumBlockEncoding.OptimalControl.evolvedEqFlipImage_isPermutation : QuantumBlockEncoding.OptimalControl.IsPermutation QuantumBlockEncoding.OptimalControl.evolvedEqFlipImage
The evolved reduced active-register map is a permutation.
The corresponding 16\times16 matrix closes both rational Gram-matrix identities.
Lean code for Theorem4.3.2●1 theorem
Associated Lean declarations
Associated Lean declarations
-
theoremdefined in QuantumBlockEncoding/OptimalControl.leancomplete
theorem QuantumBlockEncoding.OptimalControl.evolvedEqFlipUnitary_isRationalOrthogonal : QuantumBlockEncoding.OptimalControl.IsRationalOrthogonal QuantumBlockEncoding.OptimalControl.evolvedEqFlipUnitary
theorem QuantumBlockEncoding.OptimalControl.evolvedEqFlipUnitary_isRationalOrthogonal : QuantumBlockEncoding.OptimalControl.IsRationalOrthogonal QuantumBlockEncoding.OptimalControl.evolvedEqFlipUnitary
The evolved matrix is a concrete rational unitary matrix in the project-local real/permutation sense: both its column and row Gram matrices are identity.
Although the off-block unitary completion differs from the parent construction, its clean block is the same transfer operator.
Lean code for Theorem4.3.3●1 theorem
Associated Lean declarations
Associated Lean declarations
-
theoremdefined in QuantumBlockEncoding/OptimalControl.leancomplete
theorem QuantumBlockEncoding.OptimalControl.evolvedEqFlipUnitary_cleanBlock (row col : Fin 8) : QuantumBlockEncoding.OptimalControl.evolvedEqFlipUnitary (QuantumBlockEncoding.OptimalControl.cleanIndex row) (QuantumBlockEncoding.OptimalControl.cleanIndex col) = QuantumBlockEncoding.OptimalControl.exampleOperator row col
theorem QuantumBlockEncoding.OptimalControl.evolvedEqFlipUnitary_cleanBlock (row col : Fin 8) : QuantumBlockEncoding.OptimalControl.evolvedEqFlipUnitary (QuantumBlockEncoding.OptimalControl.cleanIndex row) (QuantumBlockEncoding.OptimalControl.cleanIndex col) = QuantumBlockEncoding.OptimalControl.exampleOperator row col
The evolved concrete matrix has the required clean block.
The depth-two logical construction is packaged as a verified operator block encoding with an explicit circuit transcript, schedule, resource count, and both semantic proofs.
Lean code for Definition4.3.4●1 definition
Associated Lean declarations
Associated Lean declarations
-
defdefined in QuantumBlockEncoding/OptimalControl.leancomplete
def QuantumBlockEncoding.OptimalControl.evolvedEqFlipVerified : QuantumBlockEncoding.VerifiedOperatorBlockEncoding ℚ 3
def QuantumBlockEncoding.OptimalControl.evolvedEqFlipVerified : QuantumBlockEncoding.VerifiedOperatorBlockEncoding ℚ 3
Verified concrete depth-2 block encoding for `E_1`.
Definition4.3.5
The exact evolved solution is reused as the baseline for any later approximate optimization.
Lean code for Definition4.3.5●1 definition
Associated Lean declarations
Associated Lean declarations
-
defdefined in QuantumBlockEncoding/OptimalControl.leancomplete
def QuantumBlockEncoding.OptimalControl.evolvedEqFlipZeroErrorApprox : QuantumBlockEncoding.VerifiedApproximateOperatorBlockEncoding ℚ 3
def QuantumBlockEncoding.OptimalControl.evolvedEqFlipZeroErrorApprox : QuantumBlockEncoding.VerifiedApproximateOperatorBlockEncoding ℚ 3
The exact evolved candidate is also a zero-error approximate block encoding. This is the Lean anchor for Scenario 1 of the adaptive exact-to-approximate policy: after exact convergence, approximate search may continue, but the current champion already satisfies every nonnegative requested tolerance.