Research proof index

Batch completeness theorem for Merkle trees: building the tree honestly, generating the batch proof for any selector opening at least one leaf, and verifying it against the tree's root succeeds with probability 1 under the random oracle. The proof reduces to functional_batch_completeness through simulateQ, exactly as the single-index completeness...

Completeness theorem for Merkle trees. The proof proceeds by reducing to the functional completeness theorem by a theorem about the OracleComp monad, and then applying the functional version of the completeness theorem.

A functional form of the batch completeness theorem: the honest batch proof generated from an honestly built tree, together with the true selected leaf values, recomputes the tree's root , under any hash function and any selector opening at least one leaf.

Completeness theorem for Merkle trees: for any full binary tree with 2 ^ n leaves, and for any index i, the honestly-generated opening proof verifies against the honestly-built root with probability one.

A functional completeness theorem for Merkle proofs built from buildMerkleTree_with_hash.

Assuming Plancherel's theorem (which is not yet in Mathlib), the topological closure of the span of the eigenfunctions of the harmonic oscillator is the whole Hilbert space. The proof of this result relies on fourierIntegral_zero_of_mem_orthogonal and Plancherel's theorem which together give us that the norm of f x * e ^ (- x^2 / (2 * ξ^2)) is zero fo...