Implement the ordinary Berkovich locally ringed core

[dagurtomas]

Parent

Production-layer subtask of #21, split from the oversized prototype in draft PR #34. Completed by cec20f0.

Goal

Represent the ordinary locally ringed topological core of a Berkovich space using mathlib, rather than the custom PreBerkovichSpace structure in #34.

Implemented production layer

Rigid/Berkovich/LocallyRingedSpace.lean defines:

• Rigid.Berkovich.LocallyRingedCore K as the mathlib over category of locally ringed spaces over Spec (ULift K);
• LocallyRingedCore.locallyRingedSpaceFunctor and its faithful instance via Over.forget;
• the underlying point functor, continuous point maps, identity/composition, and natural point homeomorphism;
• thin section, stalk, local-ring, and germ adapters derived from the mathlib structure sheaf.

The norm, analytic domains, admissible G-topology, and affinoid atlas are excluded from this core.

Universe correction

The comparator now places BerkovichSpace K in Type (u + 2) and its points, ordinary sections, stalks, and locally ringed model one universe above K. This lets the final public object contain the locally ringed core without shrinking genuinely large topological or sheaf data.

Downstream public adapters

The following comparator declarations remain placeholders until #41 defines the genuine atlas-bearing BerkovichSpace and its projection to this core:

• BerkovichSpace.locallyRingedSpaceFunctor;
• BerkovichSpace.toLocallyRingedSpace;
• BerkovichSpace.pointHomeomorphToLocallyRingedSpace;
• BerkovichSpace.locallyRingedSpaceFunctorFaithful;
• pointHomeomorphToLocallyRingedSpace_naturality.

They are now thin assembly adapters owned by #41. Replacing the public BerkovichSpace with LocallyRingedCore alone would omit the analytic-domain and affinoid-atlas structure.

Verification

• production files contain no sorry;
• focused module and target builds pass;
• root-import and comparator checks pass;
• full lake build -q Rigid passes.

[dagurtomas]

Claimed. I will implement the ordinary locally ringed core as a production layer without replacing the public BerkovichSpace by a core-only scaffold. The final adapter bodies will be closed only when the atlas-bearing public type can project to this layer.

[dagurtomas]

Completed by cec20f0. The production core is implemented and verified. The five thin adapters from the final atlas-bearing BerkovichSpace are explicitly transferred to #41.