Skip to content

Docs cleanup: drop stale spec, compress conventions and playbook (901 → 526 lines) #27

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
Xinze-Li-Moqian merged 1 commit into from
May 15, 2026
+29 −404
Merged

Docs cleanup: drop stale spec, compress conventions and playbook (901 → 526 lines) #27

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
108 changes: 16 additions & 92 deletions docs/CONVENTIONS.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,135 +1,59 @@
# OpenGA Conventions

Canonical conventions for every mathematical object in OpenGALib. Each entry
cites the textbook source of the chosen convention. **Conventions are
non-negotiable: once anchored, they are fixed.** Disagreements about
convention are answered by citation, not by re-argument.

This document is updated whenever a new convention is anchored. The Lean
source is authoritative when prose and code disagree.

## v1 — Stage I (Layer 1 foundations)

This is the founding-phase conventions document. Subsequent stages append
sections; existing sections only ever clarify, never change semantics.

---

## Layer 1: Autonomy policy

The Layer 1 stack (`OpenGALib/MetricGeometry/`) — `MetricMeasureSpace`, `LengthSpace`,
`GeodesicSpace` — is OpenGA-owned. Types, classes, headline statements, and
conventions are chosen for OpenGA's purposes; they are not constrained to
match upstream Mathlib formulations even where Mathlib has a similar
primitive. Mathlib tools (`eVariationOn`, `hausdorffMeasure`,
`IsRiemannianManifold`, …) are consumed directly when available, but always
through an OpenGA-namespace wrapper that fixes the OpenGA-side signature.

We do **not** copy Mathlib infrastructure wholesale. We do **not** re-export
Mathlib symbols under aliases. Each OpenGA Layer 1 primitive earns its
existence by carrying a distinct conceptual signature (intrinsic-metric
length functional; metric-measure triple as data; geodesic existence
predicate); when the OpenGA signature happens to coincide with a Mathlib
primitive, we use that Mathlib primitive in the body without re-defining it.

Ground truth: design philosophy §5.1 of the OpenGA charter / manifesto.
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.

---

## Curvature sign convention

OpenGA uses the **do Carmo** sign convention throughout the Riemannian and
Comparison layers:
OpenGA uses the **do Carmo** sign convention throughout the Riemannian and Comparison layers:

$$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 curvature is the trace of $R(\,\cdot\,, Y) Z$ in its first slot; sectional curvature of a 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 (modulo a sign flip in the curvature-of-a-distribution
discussion, which is irrelevant for OpenGA's intended scope).
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.

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:
The 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
(length as supremum of partition sums of distances).
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.
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`.
Implementation: `OpenGALib.pathLength` in `OpenGALib/MetricGeometry/LengthSpace.lean`, wrapping Mathlib's `eVariationOn`.

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.
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.

---

## 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.
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.

Ground truth: Burago–Burago–Ivanov §2.5.5.

The Hopf–Rinow theorem (complete Riemannian manifolds are geodesic spaces)
belongs to Layer 3a; it is not provided in Layer 1 as Layer 1 is
metric-only.
The Hopf–Rinow theorem (complete Riemannian manifolds are geodesic spaces) belongs to Layer 3a; Layer 1 is metric-only.

Implementation: `OpenGALib.GeodesicSpace` in
`OpenGALib/MetricGeometry/GeodesicSpace.lean`.
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 that 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.

No regularity / σ-finiteness / Radon hypotheses are baked into the
structure. Stronger hypotheses are added at the use site, matching Mathlib's
`MeasureTheory.Measure` discipline.

Implementation: `MetricMeasureSpace` in
`OpenGALib/MetricGeometry/MetricMeasureSpace.lean`.

---
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.

## Future sections (Stage II and later)
Ground truth: Gromov, *Metric Structures for Riemannian and Non-Riemannian Spaces*, §3¹⁄₂.5 (mm-spaces); Burago–Burago–Ivanov §1.7.

To be appended:
No regularity / σ-finiteness / Radon hypotheses are baked into the structure. Stronger hypotheses are added at the use site, matching Mathlib's `MeasureTheory.Measure` discipline.

* **Pointed Gromov–Hausdorff convergence**: base point convention, proper
metric space hypothesis, ε–δ formulation. Anchored on Gromov §3 (proper
metric spaces) and Burago–Burago–Ivanov Ch. 7.
* **Hausdorff measure notation**: `OpenGA.hausdorffMeasure d` wrapping
Mathlib's `MeasureTheory.Measure.hausdorffMeasure`. Anchored on Mattila §4.
* **Tangent cones**: rescaled-ball Gromov–Hausdorff limits, base point at
the singularity, Gromov–Hausdorff topology on isometry classes.
* **CD(K, N) / RCD(K, N) frameworks** when Layer 2 lands.
Implementation: `MetricMeasureSpace` in `OpenGALib/MetricGeometry/MetricMeasureSpace.lean`.
106 changes: 10 additions & 96 deletions docs/NAMING_CONVENTION.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,10 +1,6 @@
# Naming and Style Convention

Lib-wide rules for definitions, theorems, file structure. Goal: code reads like
textbook math at the API surface, with engineering noise hidden.

This document is **enforced**: any file refactor pass must conform. New code
should conform from the start.
Lib-wide rules for definitions, theorems, file structure. Goal: code reads like textbook math at the API surface, with engineering noise hidden. New code conforms from the start; any refactor pass must conform.

## 1. Object suffixes (definitions)

Expand All @@ -26,8 +22,7 @@ Use the smallest mathematical-meaning suffix that describes the object's *type*.
* `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`).
If the object truly *is* a function, name it like the function (e.g. `gradient`, not `gradientFunc`).

## 2. Theorem suffixes (Mathlib convention)

Expand All @@ -45,37 +40,25 @@ not `gradientFunc`).
| `_symm` | symmetry |
| `_antisymm` | antisymmetry |

Compose multiple: `riemannCurvature_inner_self_zero` (one-line inner-self
equality, RHS = 0).
Compose multiple: `riemannCurvature_inner_self_zero` (one-line inner-self equality, RHS = 0).

**Avoid** descriptive prose in theorem names: not
`riemannCurvature_inner_diagonal_zero`, not `ricci_is_symmetric_in_arguments`.
**Avoid** descriptive prose in theorem names: not `riemannCurvature_inner_diagonal_zero`, not `ricci_is_symmetric_in_arguments`.

## 3. Naming case

* `lowerCamelCase` for definitions and theorems: `riemannCurvature`, `metricInner`.
* `UpperCamelCase` for types and namespaces: `RiemannianMetric`, `SmoothVectorField`.
* No `snake_case` for identifiers; `_` only as theorem-component separator
(`riemannCurvature_antisymm`, not `riemann_curvature_antisymm` or
`RiemannCurvatureAntisymm`).
* No `snake_case` for identifiers; `_` only as theorem-component separator (`riemannCurvature_antisymm`, not `riemann_curvature_antisymm`).

## 4. Boilerplate hiding via local notation

When a fully-qualified term `Foo.bar (x := X) (y := Y) v` appears 3+ times in a
file, introduce file-local notation:
When a fully-qualified term `Foo.bar (x := X) (y := Y) v` appears 3+ times in a file, introduce file-local notation:

```lean
local notation "𝒞[" V "]" => SmoothVectorField.const (I := I) (M := M) V
local notation "cF[" V "]" => SmoothVectorField.const (I := I) (M := M) V
```

Use the resulting binding inside proofs. Limits noise to a one-line declaration
at the top of the section.

Common patterns:

* Constant section: `𝒞[V]` for `SmoothVectorField.const (I := I) (M := M) V`.
* Tangent vector at a point: `T[x]` or `Tx[x]` if the type spelling is verbose.
* Don't introduce notation for one-shot use.
Use the resulting binding inside proofs. Limits noise to a one-line declaration at the top of the section. Don't introduce notation for one-shot use.

## 5. Module docstring template

Expand All @@ -86,8 +69,6 @@ Common patterns:
<Mathematical statement of what this module provides — textbook style.
Two to four short sentences; no Lean-implementation jargon.>

<Optional: layering / context — where in the lib stack this lives.>

## Main definitions

* `name1` — one-line gloss.
Expand All @@ -101,77 +82,10 @@ Reference: <do Carmo §X / Simon §Y / Pitts §Z / etc.>
-/
```

**Removed** (avoid these in module docstrings):

* `Inspired by ...` / `Adapted from ...` — attribution belongs in the project
`NOTICE.md` if relevant.
* `## Form` — use `## Main definitions` instead.
* `## Sorry status` — `sorry`s carry per-theorem closure-path comments.
* `## Ground truth` — replace with one-line `Reference:` per theorem.
* "Real `noncomputable def`" / "Mathlib upstream candidate" — internal labels,
not user-facing docs.

## 6. Per-definition / per-theorem docstring

```lean
/-- <Mathematical statement, in display math when natural>.

Reference: do Carmo §X. -/
theorem name ... := by ...
```

Three rules:

1. First sentence is the statement (math or natural-language).
2. One reference at the end (or none if obvious).
3. No proof-strategy commentary, no "this is a Lean trick" notes. Engineering
commentary goes inside the proof body if essential.

## 7. Engineering hiding

When a theorem or instance has a long, primarily mechanical proof (50+ lines):

* If the proof has no internal cross-reference: use `where`-aux to attach helpers
to the parent definition.
* If helpers cross-reference each other: extract as file-level `private theorem`s
before the consumer.
* If the engineering is genuinely implementation-detail (instance diamond
workaround, `set_option` overrides): wrap in a small section near the top of
the file, not interleaved with math API.

Aim: a reader scrolling the file should see the math API in the first 20–30%
of lines; engineering should be visibly "below the fold".

## 8. UXTest sections

Removed. The build is the regression guard. Per-file `example` blocks that
re-state the typeclass cascade clutter the math API surface.

If a typeclass-cascade test is essential, place it in a dedicated test file
under `test/` (or use `#guard_msgs` for diagnostic regressions).

## 9. `private` versus `protected` versus public
## 6. `private` versus `protected` versus public

* Internal-only helper: `private` (file-local).
* Helper exposed to a closely related submodule but not user-facing: `protected`
(namespace-prefixed access required).
* Helper exposed to a closely related submodule but not user-facing: `protected` (namespace-prefixed access required).
* Public: no modifier.

Default to `private` for any helper without a clear API consumer.

## 10. Refactor process

When refactoring a file:

1. Apply object renames to the file (per §1).
2. Apply theorem suffix renames (per §2).
3. Introduce `local notation` for repeated boilerplate (per §4).
4. Rewrite module docstring (per §5).
5. Tighten per-definition docstrings (per §6).
6. Move long proofs to `where`-aux or `private` (per §7).
7. Remove UXTest section if present (per §8).
8. Add `private` modifiers to internal helpers (per §9).
9. Verify LSP clean.
10. Update any other file's docstring that references the old name.

The reference example for this process is `Riemannian/Curvature.lean`.
Loading
Loading