chore(RingTheory): adapt Perfectoid field draft to current master (revival)

[sfingali]

Revival of leanprover-community#26389 (as discussed — co-authoring).

What this does: adapts Perfectoid.lean to the current master API so it compiles again:

• structure S extends P : Prop → structure S : Prop extends P (new syntax)
• UniformAddGroup → IsUniformAddGroup, TopologicalDivisionRing → IsTopologicalDivisionRing
• explicit universe levels for the : Type extends classes
• 𝒪[K] notation and the Valued field names verified against current master (no changes needed)

State: compiles against master, 13 sorrys remain — the mathematical work:

• valuedPerfectoidField.is_topological_valuation
• IsTopologicalNilpotent, val_p_lt_1
• the Tilt field instance
• PerfectoidField.isAlgClosed_iff_isAlgClosed_tilt

Proposal: I take the sorries in order (starting with val_p_lt_1 and the Frobenius-surjectivity API), you review. Happy to push directly to your branch instead if you prefer.