QuantumComputingBench · graph-grounded exercise book
Three reference warmups
Small API applications, not deep proof synthesis. A distinct semantic review checked exact definitions, angle conventions and assumptions; inherited fixed-reference elaboration is separate from this review. The review is not a strictly source-blind decoder certificate.
lean-standardRyMatrix-zero-corrected-v3
Supply a fully qualified lemma-application proof of the frozen formal target. Reusing the imported theorem is permitted; this tests interface application, not novel theorem discovery. Return only the proof term. Target: QuantumBlockEncoding.standardRyMatrix 0 = 1
{
"imports": [
"QuantumBlockEncoding.PrimitiveSemantics"
],
"target": "QuantumBlockEncoding.standardRyMatrix 0 = 1"
}Reference proof and semantic reconstruction
by exact QuantumBlockEncoding.standardRyMatrix_zeroThe complex 2-by-2 matrix with entries [[cos(theta/2), -sin(theta/2)], [sin(theta/2), cos(theta/2)]] equals the matrix identity when theta=0.
At zero the diagonal entries are cos(0)=1 and the off-diagonal entries are plus/minus sin(0)=0. Matrix extensionality and the four Fin 2 cases give the identity.
Historical same-core alias: lean-standardRyMatrix-zero. Not added to the native core count.
lean-flipBit-involutive-corrected-v3
Supply a fully qualified lemma-application proof of the frozen formal target. Reusing the imported theorem is permitted; this tests interface application, not novel theorem discovery. Return only the proof term. Target: ∀ bit : Fin 2, QuantumBlockEncoding.flipBit (QuantumBlockEncoding.flipBit bit) = bit
{
"imports": [
"QuantumBlockEncoding.PrimitiveSemantics"
],
"target": "∀ bit : Fin 2, QuantumBlockEncoding.flipBit (QuantumBlockEncoding.flipBit bit) = bit"
}Reference proof and semantic reconstruction
by exact QuantumBlockEncoding.flipBit_flipBitOn the two-element carrier {0,1}, the map exchanging zero and one is its own inverse.
For input zero the two images are one then zero. For input one the two images are zero then one. These exhaust the carrier, as the source fin_cases/rfl proof records.
Historical same-core alias: lean-flipBit-involutive. Not added to the native core count.
lean-planeMatrix-det-applicability-corrected-v3
Supply a fully qualified lemma-application proof of the frozen formal target. Reusing the imported theorem is permitted; this tests interface application, not novel theorem discovery. Return only the proof term. Target: ∀ {N : ℕ} (i j : Fin N), i ≠ j → ∀ theta : ℝ, (QuantumBlockEncoding.AdjacentGivens.planeMatrix i j theta).det = 1
{
"imports": [
"QuantumBlockEncoding.AdjacentGivens"
],
"target": "∀ {N : ℕ} (i j : Fin N), i ≠ j → ∀ theta : ℝ, (QuantumBlockEncoding.AdjacentGivens.planeMatrix i j theta).det = 1"
}Reference proof and semantic reconstruction
by exact QuantumBlockEncoding.AdjacentGivens.planeMatrix_detFor every natural dimension N, every ordered pair of distinct coordinate indices i,j and every real RY parameter theta, rotating the identity's rows i,j gives an N-by-N real matrix of determinant one.
Multilinear determinant expansion in two distinct replaced rows kills the two repeated-row terms. The unchanged-order and swapped-order terms give (a*d-b*c)*det(A). For (a,b,c,d)=(cos(theta/2),-sin(theta/2),sin(theta/2),cos(theta/2)), that factor is cos^2+sin^2=1. Applying determinant preservation to A=I and det(I)=1 gives the target.
Historical same-core alias: lean-planeMatrix-det-applicability. Not added to the native core count.