Proof of `Uniform tuple images on prescribed Gram orbits` (5th statement)
groundedproofs/Lax342547Proofs/FrameTuples.lean · lax-342547
What this proof establishes
no assumptions
Assuming the claims on the left, the claim on the right holds — checked by the archive's pipeline. Proof code is not displayed here.
Description
The primal tuple observation has the prescribed Gram and transforms covariantly. Transitivity of the paired orbit bijects every pair of completion fibers, so its pushforward is exactly uniform on the orbit.