feat(Geometry): Mostow rigidity, algebraic form

[alreadydone]

No description provided.

[alreadydone]

@kim-em This PR now contains two tasks mostow_rigidity and mostow_rigidity_compact. The workspace for the former was generated successfully, but for the latter it contains several errors: see the ChallengeDeps.lean generated. Most notably, the section Topology is not ended, and variable (p q : ℕ) is dropped, leading to errors. Can you maybe ask Claude to fix these bugs?

(I should have also mentioned that open MeasureTheory is duplicated in Challenge.lean. Moreover, if I don't put mostow_rigidity in a separate namespace LeanEval.Geometry section, Challenge.lean will miss the line open LeanEval.Geometry and report errors like PO doesn't exist.)