Hello,
For your exponentiation case, there are two solutions: one is to replace ** by a tabulation (array); given that Max_Value is constant you can simply write:
Pow_4 : constant array (0 .. Max_Index + 1) of Positive :=
(1, 4, 16, 64, 256, 1_024, ..., 268_435_456);
And then proofs should be simple.
The other possibility is to write a recursive ghost lemma with Big_Integer, but use Big_Integer for the ghost model only. You need to use exponentiation somehow to give the bound of your cumulative product (this should answer your Q3).
Personally I am interested in a benchmark for SPARK proofs, today there is not much publicly available. There is a big discrepancy between the western frontier models and the open weights models when it comes to SPARK, at least the last time I tried (the open weight models).