Pointer chasing with parallel queries: machine-checked statements (M024, v0.1)

Author: Andrii Kalchuk. Four statements fully proved in Lean 4.35.0 (no sorry, standard axioms only): the exact success probability ((n+1)m - n)/m^2 of a randomised two-queries-per-round strategy for pointer chasing; a characterisation of when the answer is determined by a set of queries (iff the whole path was queried); a polynomial positivity lemma; and a lower bound 1-(1-1/m)^n, n=2r+2-t, for the probability that the transcript determines the end of the path in the randomised two-queries-per-round game. No novelty is claimed; literature check pending. Version 0.3 adds the last statement (R30); the other three files are unchanged.