Implement the rigid-space admissible-site core

[dagurtomas]

Goal

Implement rigid spaces from an admissible locally affinoid site:

• points and admissible opens;
• admissible-cover axioms;
• structure sheaf, stalks, and germs;
• analytic morphisms and the category;
• local affinoid atlas data.

Current work

Claimed by the project coding-agent track in agent/rigid-space-core. The first attempt isolated a universe constraint: the public object must remain in Type (u + 1), so the next implementation uses a small internal code and exposes points/opens through ULift.

Binary products, closed immersions, canonical affinoid realizations, and comparison are deferred.

[dagurtomas]

Status correction after reviewing PR #32 and the local prototype:

• Follow-up 483f94b removed the point-only RigidSpace production scaffold and restored the four affected comparator bodies (RigidSpace, Point, ofAffinoid, and pointsOfAffinoidEquiv) to honest sorrys.
• The uncommitted prototype remains in /tmp/rigid-rigid-space-core, but it is not merge-ready. It currently gives a substantive admissible site/sheaf/category skeleton, yet an “affinoid domain” is only labelled by an affinoid algebra; it is not identified with a restriction isomorphic to the corresponding affinoid spectrum. Its cover-index universes also do not yet match the comparator API.

Acceptance criteria for this issue:

1. Introduce an internal locally ringed admissible-space/pre-rigid-space layer, rather than publishing a point-only RigidSpace.
2. Support the comparator's Type (u + 1) cover index families and actual Grothendieck/pretopology axioms.
3. Make stalks genuinely arise from the structure sheaf (or provide their required universal property), not arbitrary local rings with arbitrary germ maps.
4. Define the public rigid-space type by a local affinoid atlas whose charts are identified with restrictions to canonical affinoid spaces, including compatibility of points, admissible opens/covers, and structure sheaves—not merely by attaching an affinoid-algebra label.
5. Adapt Development.lean only after this model exists and passes the comparator unchanged.

The issue remains claimed by the project coding-agent track while that prototype is redesigned.

[dagurtomas]

The current agent prototype is now preserved for review in draft PR #33. The PR is not merge-ready; its description lists the required chart, stalk, and universe redesign.

[dagurtomas]

Blocked on #35, which will define the admissible G-topology through mathlib's sites API. Draft PR #33 has been closed because its custom cover relation duplicates that API.