Draft: prototype rigid-space admissible core

[dagurtomas]

Status

Draft prototype — not ready to merge. Tracks #22.

This preserves the rigid-space agent's partial implementation so its design and proofs can be reviewed in GitHub rather than remaining only in a local worktree. It does not replace any comparator sorry.

Implemented prototype

• a small SpaceCode carrying points and admissible opens;
• top/intersection operations and admissible-cover axioms;
• sections, restriction maps, and a gluing axiom;
• local-ring stalk and germ interfaces;
• analytic morphism data with identity, composition, and a category instance;
• the point functor;
• affinoid-domain and admissible-cover data;
• a stored local affinoid atlas and finiteness predicates.

Required redesign before merge

• Treat this as an internal PreRigidSpace/locally ringed admissible-space layer rather than the final public RigidSpace.
• Support cover index types in Type (u + 1), matching the comparator.
• Derive stalks from the structure sheaf, or provide their universal property, rather than storing unrelated local rings and germ maps.
• Identify each affinoid chart with an actual restriction isomorphic to a canonical affinoid rigid space, including compatibility of points, admissible opens/covers, and sections. The current algebra label is insufficient.
• Construct the public rigid-space bundle from a genuine local affinoid atlas before adapting Development.lean.
• Narrow the broad Mathlib import and remove temporary linter suppression.

Checks

Passed on this branch:

• ./scripts/check_root_imports.sh
• ./scripts/check_challenge_development.sh
• lake build -q Rigid.RigidSpace.Core
• lake build -q Rigid
• git diff --check
• no sorry in Rigid/RigidSpace/Core.lean

[dagurtomas]

This prototype hand-rolls an isCover relation and the Grothendieck-topology axioms instead of using mathlib's CategoryTheory.GrothendieckTopology, Pretopology, sieves, and sheaf APIs. That is the wrong foundation for the public rigid-space model. The replacement prerequisite is tracked in #35. The branch remains available as an archive of potentially reusable morphism/category experiments.