Construct the affinoid Berkovich structure sheaf and local stalks

[dagurtomas]

Parent and dependencies

Subtask of #21, split from draft PR #34. Depends on:

• Build reusable G-site/G-ringed infrastructure and its rigid instantiation #35 for reusable G-site, G-sheaf, stalk, germ, and locally G-ringed infrastructure;
• Instantiate the G-site framework for Berkovich analytic domains #38 for the Berkovich analytic-domain site;
• Construct the universe-controlled affinoid Berkovich point model #39 for the affinoid point model;
• Implement rational restriction maps on the affinoid rational basis #19 and Prove Tate acyclicity for finite rational covers #20 for rational restrictions and Tate acyclicity.

Comparator targets were added in d960950.

Goal

Construct the specific analytic structure sheaf of an affinoid Berkovich spectrum from rational localizations. First construct it on the analytic-domain G-site from #38 using #35's sheaf machinery; then derive the ordinary-open sheaf required by mathlib's LocallyRingedSpace API and prove its stalks are local rings.

This issue owns the analytic section rings and their geometric identifications. It does not own generic site, sheaf, stalk, germ, or category infrastructure.

Comparator targets

• BerkovichSpace.affinoidStructureSheaf
• affinoidStructureSheafGlobalSectionsEquiv
• affinoidStructureSheafStalkIsLocalRing
• affinoidLocallyRingedSpace (concretely assembled from the preceding data)

Scope

1. Define sections on rational/affinoid analytic domains from the corresponding rational localizations and restriction maps.
2. Prove the sheaf condition on the analytic-domain G-site using Build reusable G-site/G-ringed infrastructure and its rigid instantiation #35/Instantiate the G-site framework for Berkovich analytic domains #38 and finite rational-cover acyclicity, rather than storing an abstract gluing axiom.
3. Extend or compare that G-sheaf with a sheaf on ordinary open subsets of the affinoid point topology. The ordinary sheaf must be mathematically derived from the analytic-domain structure, not constructed as unrelated arbitrary data.
4. Identify global sections with the coordinate ring.
5. Use mathlib's sheaf-colimit stalks and the comparison with admissible neighborhoods to prove the ordinary stalks are local rings.
6. Package the ordinary point space and sheaf as AlgebraicGeometry.LocallyRingedSpace.

Explicit exclusions

• Do not define another generic G-ringed-space abstraction.
• Do not store arbitrary stalks, germs, or gluing operations.
• Do not conflate rational or affinoid domains with ordinary open subsets.

Acceptance criteria

• The analytic sheaf is tied to rational localizations on Instantiate the G-site framework for Berkovich analytic domains #38's site.
• Generic site and stalk infrastructure comes from Build reusable G-site/G-ringed infrastructure and its rigid instantiation #35 and mathlib.
• The ordinary-open sheaf is derived from, and compatible with, the analytic-domain G-sheaf.
• Global sections recover the coordinate ring and stalks are local rings.
• Production files contain no sorry.
• Focused, root-import, comparator, and full Rigid builds pass.