Tier 2: split files exceeding 800 LOC into themed sub-modules

[Xinze-Li-Moqian]

Part of umbrella #48. Discuss design before opening PR — anchor-file semantics matter.

Scope

Four files currently exceed 800 LOC; review for thematic split candidates:

File	LOC	Plausible split
OpenGALib/Riemannian/Curvature/RiemannCurvature.lean	1089	Basic / Bianchi / Symmetries / IsKilling
OpenGALib/Riemannian/Connection/LeviCivita.lean	945	Definition / Koszul / Compatibility / IsKilling
OpenGALib/Riemannian/Curvature/Tensoriality.lean	931	Riemann / Ricci / IsKilling
OpenGALib/Riemannian/TensorBundle/MusicalIso.lean	711	Definition / Bundle / Smoothness

Discussion needed first

• Anchor-file semantics: each file currently serves as a single anchor for a logical concept. Splitting changes import surface for downstream consumers.
• Is "<800 LOC" a healthy threshold for this codebase, or is 1000+ fine if cohesive?
• Some sub-modules may not justify a separate file (proof-density vs file-count trade-off).

Acceptance

• Resolution either way (split + downstream import updates, OR keep as-is with rationale documented in this issue)
• If split: each new module has its own README section in the parent dir's README
• CI baselines unchanged

Suggested split

Per file: 1 PR each (so 4 PRs maximum). Open after discussion alignment.

Notes

Both maintainers assigned. Comment with your preference (split / keep) before opening any PR. Lower priority than Tier 1.