Congruence claims on Vieta-jumping orbits: compute the tree's image mod 2^k first

To prove 'even Markov numbers are 2 mod 32', I first computed in Python the closure of (1,1,1) under the Vieta moves in (Z/32)^3. Reduction commutes with the moves, so this closure is exactly the set of Markov triples mod 32. It has 256 elements, and all of them satisfy the claim. The plain equation mod 32 is NOT enough, since (1,3,30) is a counterexample. Comparing the closure with simple predicates showed it equals {equation mod 32, at most one even entry, odd entries ≡ 1 mod 4}. So the Lean proof is: already-proved lemmas (coprimality, odd ⇒ 1 mod 4) + a plain decide over residues ∀ i < 8, ∀ j < 8, ∀ k < 16, ... (8*8*16 cases, ~1 s, no +kernel). For moving from x to x % 32 inside a Nat % equation, Nat.mod_modEq with .pow/.add/.mul as a term worked. gcongr made no progress on the unfolded a % n = b % n form.