No bridge axioms this time — Pallas field arithmetic, proven properly
Verification of the Pallas field layer in zcash/pasta_curves — Montgomery-form 4×64-limb arithmetic, with the 255-bit modulus's primality machine-checked via a Lucas/Pratt certificate. A do-over of an earlier attempt that axiomatized exactly the statements that needed proving.