Research proof index

Soundness: if findCollision returns a tuple, that tuple is a hash collision according to Collision.

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.

Batch opening uniqueness. When hashFn is injective, two batch openings for the same selector that produce the same putative root must agree on both the claimed selected values and the entire pruned authentication data.

getPutativeRoot makes one oracle query per level of idx, so it has total query bound idx.depth.

Root preservation. The single-index opening extracted from a batch opening at any selected leaf recomputes exactly the batch opening's putative root. Consequently a batch opening that verifies against a root yields, at every selected leaf, a single-index opening that verifies against the same root.

Merkle binding: from two distinct leaf values x ≠ y that produce the same putative root at the same leaf index under (possibly different) sibling proofs, the constructive search findCollision returns some. Note that idx is shared , this is binding at a fixed position. The distinct-position case requires walking down both paths to the lowest comm...