Docs pass 2: tighter cuts across all four files (526 → 213 lines)

docs/CONVENTIONS.md

@@ -1,59 +1,45 @@
 # OpenGA Conventions
 
-Canonical conventions for the mathematical objects in OpenGALib. Each entry cites the textbook source. **Conventions are non-negotiable once anchored** — disagreements are answered by citation, not by re-argument. The Lean source is authoritative when prose and code disagree.
+Canonical conventions, each with textbook source. **Non-negotiable once anchored** — disagreements are answered by citation. The Lean source is authoritative when prose and code disagree.
 
----
+## Curvature sign
 
-## Curvature sign convention
-
-OpenGA uses the **do Carmo** sign convention throughout the Riemannian and Comparison layers:
+OpenGA uses do Carmo's convention throughout Riemannian and Comparison:
 
 $$R(X, Y) Z = \nabla_X \nabla_Y Z - \nabla_Y \nabla_X Z - \nabla_{[X, Y]} Z.$$
 
-Ricci curvature is the trace of $R(\,\cdot\,, Y) Z$ in its first slot; sectional curvature of a 2-plane spanned by $X, Y$ is
+Ricci is the trace of $R(\,\cdot\,, Y) Z$ in its first slot; sectional curvature of the 2-plane spanned by $X, Y$ is
 
 $$K(X, Y) = \frac{\langle R(X, Y) Y, X \rangle}{\langle X, X \rangle \langle Y, Y \rangle - \langle X, Y \rangle^2}.$$
 
-Ground truth: do Carmo, *Riemannian Geometry*, Ch. 4 §2 (definition of $R$), Ch. 4 §3 (Ricci and sectional curvatures). This is the convention used by Petersen, Cheeger–Ebin, and the majority of the geometric-analysis literature.
+Ground truth: do Carmo, *Riemannian Geometry*, Ch. 4 §2–§3. Same convention as Petersen and Cheeger–Ebin.
 
 Implementation: `OpenGALib/Riemannian/Curvature/RiemannCurvature.lean`.
 
----
-
 ## Length functional
 
-The length of a continuous path in a pseudo-extended-metric space is the metric-side total variation:
+Length of a continuous path in a pseudo-extended-metric space is the metric-side total variation:
 
 $$\operatorname{pathLength}(\gamma) := \operatorname{eVariationOn}(\gamma, [0, 1]).$$
 
-Ground truth: Burago–Burago–Ivanov, *A Course in Metric Geometry*, §2.1.
-
-This is OpenGA's canonical "length" primitive. It does not reference any smooth structure on the target space, so it applies uniformly to metric spaces, Riemannian manifolds (via the `OpenGALib/Bridges/RiemannianToLength` bridge), Alexandrov spaces, and limits of these.
-
-Implementation: `OpenGALib.pathLength` in `OpenGALib/MetricGeometry/LengthSpace.lean`, wrapping Mathlib's `eVariationOn`.
+Ground truth: Burago–Burago–Ivanov §2.1.
 
-The Mathlib tangent-integral length `Manifold.pathELength` (used inside `IsRiemannianManifold`) is a *separate* concept and lives only at the Riemannian boundary. Equality of the two on `C¹` paths over Riemannian manifolds is the content of the `IsRiemannianManifold.toLengthSpace` bridge.
+Applies uniformly to metric spaces, Riemannian manifolds (via `Bridges/RiemannianToLength`), Alexandrov spaces, and limits. The Mathlib tangent-integral length `Manifold.pathELength` (used inside `IsRiemannianManifold`) is a *separate* concept; equality on `C¹` paths is the content of `IsRiemannianManifold.toLengthSpace`.
 
----
+Implementation: `OpenGALib.pathLength` in `OpenGALib/MetricGeometry/LengthSpace.lean`, wrapping `eVariationOn`.
 
 ## Geodesic existence
 
-A `GeodesicSpace` is a length space in which the path-length infimum is attained between every pair of points. The class only asserts existence — neither uniqueness nor regularity is part of the OpenGA definition.
+`GeodesicSpace` = length space in which the path-length infimum is attained between every pair of points. Existence only — neither uniqueness nor regularity is part of the definition.
 
-Ground truth: Burago–Burago–Ivanov §2.5.5.
-
-The Hopf–Rinow theorem (complete Riemannian manifolds are geodesic spaces) belongs to Layer 3a; Layer 1 is metric-only.
+Ground truth: Burago–Burago–Ivanov §2.5.5. Hopf–Rinow (complete Riemannian ⇒ geodesic) belongs to Layer 3a; Layer 1 is metric-only.
 
 Implementation: `OpenGALib.GeodesicSpace` in `OpenGALib/MetricGeometry/GeodesicSpace.lean`.
 
----
-
 ## Metric measure space
 
-A `MetricMeasureSpace M` is a `structure` carrying a `PseudoEMetricSpace M` together with a `MeasureTheory.Measure M`. The metric and measure are stored as data (not as typeclasses) so a single carrier may host multiple metric-measure structures.
-
-Ground truth: Gromov, *Metric Structures for Riemannian and Non-Riemannian Spaces*, §3¹⁄₂.5 (mm-spaces); Burago–Burago–Ivanov §1.7.
+`MetricMeasureSpace M` = `structure` carrying a `PseudoEMetricSpace M` together with a `MeasureTheory.Measure M`. Both stored as data (not typeclasses), so a single carrier may host multiple metric-measure structures. No regularity / σ-finiteness / Radon hypotheses baked in — added at the use site, matching Mathlib's `MeasureTheory.Measure` discipline.
 
-No regularity / σ-finiteness / Radon hypotheses are baked into the structure. Stronger hypotheses are added at the use site, matching Mathlib's `MeasureTheory.Measure` discipline.
+Ground truth: Gromov §3¹⁄₂.5 (mm-spaces); Burago–Burago–Ivanov §1.7.
 
 Implementation: `MetricMeasureSpace` in `OpenGALib/MetricGeometry/MetricMeasureSpace.lean`.

docs/NAMING_CONVENTION.md

@@ -4,25 +4,18 @@ Lib-wide rules for definitions, theorems, file structure. Goal: code reads like
 
 ## 1. Object suffixes (definitions)
 
-Use the smallest mathematical-meaning suffix that describes the object's *type*.
+Use the smallest math-meaning suffix that describes the object's *type*.
 
 | Suffix | Meaning | Example |
 |---|---|---|
 | `Endo` | endomorphism `V → V` | `curvatureEndo`, `ricciEndo` |
-| `Tensor` | tensor (typically `(0,k)`-tensor as bilinear form) | `ricciTensor`, `metricTensor` |
+| `Tensor` | tensor (typically `(0,k)` as bilinear form) | `ricciTensor`, `metricTensor` |
 | `Bilin` | bilinear form, when `Tensor` is ambiguous | `koszulBilin` |
-| `Sharp` | musical isomorphism $\sharp$ (raise indices via metric) | `ricciSharp` |
-| `Flat` | musical isomorphism $\flat$ (lower indices via metric) | `gradFlat` |
+| `Sharp` / `Flat` | musical iso $\sharp$ / $\flat$ | `ricciSharp`, `gradFlat` |
 | `Dual` | dual vector / dual operation | `metricDual` |
-| `Form` | when the math name is "X form" | `quadraticForm` (avoid bare `Form` for tensors) |
+| `Form` | when the math name is "X form" | `quadraticForm` |
 
-**Avoid these engineering suffixes**:
-
-* `TraceMap`, `Map`, `Func`, `Fn`, `Function`
-* `At` / `AtPoint` / `Pt` (when the basepoint is just an argument)
-* `Tower`, `Stack`, `Wrapper`, `Aux`, `Bundle` (when not literally a vector bundle)
-
-If the object truly *is* a function, name it like the function (e.g. `gradient`, not `gradientFunc`).
+Avoid engineering suffixes: `Map`, `Func`, `Fn`, `Function`, `At` / `AtPoint` / `Pt` (when basepoint is just an argument), `Tower`, `Stack`, `Wrapper`, `Aux`, `Bundle` (when not literally a vector bundle). If the object truly *is* a function, name it like one (`gradient`, not `gradientFunc`).
 
 ## 2. Theorem suffixes (Mathlib convention)