diff --git a/docs/CONVENTIONS.md b/docs/CONVENTIONS.md index d16c0c3..25de74e 100644 --- a/docs/CONVENTIONS.md +++ b/docs/CONVENTIONS.md @@ -1,58 +1,20 @@ # 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`. @@ -60,76 +22,38 @@ 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`. diff --git a/docs/NAMING_CONVENTION.md b/docs/NAMING_CONVENTION.md index e48f86e..0d9551d 100644 --- a/docs/NAMING_CONVENTION.md +++ b/docs/NAMING_CONVENTION.md @@ -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) @@ -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) @@ -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 @@ -86,8 +69,6 @@ Common patterns: - - ## Main definitions * `name1` — one-line gloss. @@ -101,77 +82,10 @@ Reference: -/ ``` -**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 -/-- . - -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`. diff --git a/docs/REFACTOR_PLAYBOOK.md b/docs/REFACTOR_PLAYBOOK.md index ec42025..4d19385 100644 --- a/docs/REFACTOR_PLAYBOOK.md +++ b/docs/REFACTOR_PLAYBOOK.md @@ -1,11 +1,6 @@ # Refactor Playbook -Source of truth for OpenGALib refactor workflows. Sister to `scripts/` -(reusable codemods) and the project's CLAUDE.md (architectural stance). - -The goal: **same operation never costs more than the first time**. - ---- +Source of truth for OpenGALib refactor workflows. Sister to `scripts/` (reusable codemods) and the project's CLAUDE.md (architectural stance). Goal: **same operation never costs more than the first time**. ## Decision tree @@ -50,64 +45,6 @@ What's the refactor about? redirect downstream imports + delete sub-files. ``` ---- - -## Pre-flight checklist (always) - -1. **`git status` clean.** No uncommitted changes. The bulk operation - should be a single revertible step. -2. **Snapshot commit** of the current good state if there's any pending - work: `git commit -am "snapshot before X refactor"`. -3. **One refactor concern per commit.** Don't bundle "rename + reorganize - + add deprecation alias" into one diff. Three separate commits. -4. **`lake build` after each commit.** Catches silent breakage early - when revert is still cheap. - -If anything fails: `git reset --hard HEAD~1` and retry. The atomic-commit -discipline makes rollback one command. - ---- - -## Lake script vs bash — when to use which - -| Need | Tool | Reason | -|------|------|--------| -| File text replacement | bash + sed/perl | Milliseconds, well-understood | -| Import path rewrite | `scripts/rewrite-import.sh` | Already written | -| `grep` on Lean source only | `scripts/lean-grep.sh` | Excludes `.lake/`, `.git/` | -| Rename identifier in code only (skip docstrings) | Lake script | Needs Lean syntax tree | -| Find all theorems whose statement uses X | Lake script | Needs `Lean.Environment` API | -| Audit `@[simp]` lemma RHS shapes | Lake script | Needs elaborator | -| Generate a typeclass dependency graph | Lake script | Needs full elab info | -| One-off file munging | Inline shell command | Don't bother formalizing | - -**Rule of thumb:** if the codemod would need to *understand* Lean -syntax or semantics, write it in Lean (Lake script). Otherwise bash is -faster to write and run. - -### Lake script template - -In `lakefile.lean`: - -```lean -script myCodemod (args : List String) do - match args with - | [arg1, arg2] => - -- ... do work using IO + Lean APIs ... - return 0 - | _ => - IO.eprintln "Usage: lake script run myCodemod ARG1 ARG2" - return 1 -``` - -Invoke: `lake script run myCodemod foo bar`. - -For AST-level work, `import Lean` and use `Lean.Environment`, -`Lean.Syntax`, `Lean.Elab.*`. Mathlib's `scripts/` directory has good -examples. - ---- - ## Pitfalls (encountered, in this lib's history) 1. **Text-level sed corrupts docstrings.** `sed 's/X/Y/g'` on `.lean` @@ -151,24 +88,17 @@ examples. reliable and self-explaining. See `/tmp/strip_uxtest.py` style: collect target files via `glob`, walk lines, locate start/end, splice. -7. **`.gitkeep` is dead weight in non-empty directories.** It exists to - make Git track empty dirs; once the dir has any other file, the - `.gitkeep` is a stale signal. Periodic - `find . -name .gitkeep -path '*//*'` audit catches it. - -8. **Bulk attribution-paragraph strip needs paragraph-level matching.** +7. **Bulk attribution-paragraph strip needs paragraph-level matching.** Phase A external ports left `**Inspired by** /...` paragraphs (multi-line, ending at blank line or `-/`). A line-level grep+replace only catches one line; you need to walk lines and skip from `Inspired by` line through next blank line / `-/` / next `## ` heading. -9. **Force-pushing to remove an oversight is partially effective.** +8. **Force-pushing to remove an oversight is partially effective.** `Co-Authored-By: ...` trailers, once pushed to a public repo, remain in GitHub's contributor cache even after the commit is force-pushed away. The orphan commit is still server-side. Lesson: **don't push to a public repo with a trailer you'd regret**. - Memory `feedback_release_repo_attribution.md` enforces this for - MathNetwork/OpenGA going forward. --- @@ -329,16 +259,3 @@ Saves ~30 min vs hand-writing. work on macOS BSD sed. Use the Edit tool's `replace_all` mode for cross-platform identifier renames within a single file. ---- - -## Adding to this playbook - -When a refactor pattern is performed **3+ times** with the same -manual workaround, lift it into: - -* a `scripts/` entry (if shell-tool-shaped), or -* a `lake script` entry (if AST-aware), and -* a row in the decision tree above + a Pitfall note if it has a known - failure mode. - -The playbook is dogfood. Trust accumulates over commits. diff --git a/docs/RIEMANNIAN_FRAMEWORK_SPEC.md b/docs/RIEMANNIAN_FRAMEWORK_SPEC.md deleted file mode 100644 index 8c04808..0000000 --- a/docs/RIEMANNIAN_FRAMEWORK_SPEC.md +++ /dev/null @@ -1,130 +0,0 @@ -# Riemannian framework spec - -This document specifies the typeclass-level definition of the -"Riemannian manifold" object in OpenGALib. It is the reference for -contributors adding new geometric structures or new operators. - -The spec is a mathematical artifact, not engineering documentation: -just as a paper §1.1 fixes the formal meaning of `(M, g)` for the rest -of the paper, this file fixes its formal meaning for the rest of the -framework. - -## §1 Definitions - -### §1.1 Smooth manifold - -``` -class SmoothManifold (M : Type*) [TopologicalSpace M] where - E : Type* -- model fibre, with NACG + NormedSpace ℝ - H : Type* -- chart codomain, with TopologicalSpace - modelI : ModelWithCorners ℝ E H - -- + chart machinery + IsManifold modelI ∞ M -``` - -Mathematical content: a topological space $M$ together with a chart -atlas modeled on $H$, factoring through a model with corners -$\text{modelI} : H \to E$, such that the transition functions are -$C^\infty$. - -The fields `E, H, modelI` are framework-internal: a downstream -operator that says "let $M$ be a smooth manifold" requires only -`[SmoothManifold M]`, not the five-typeclass cascade. - -### §1.2 Riemannian manifold - -``` -class RiemannianManifold (M : Type*) [TopologicalSpace M] - extends SmoothManifold M where - toRiemannianMetric : RiemannianMetric modelI M -``` - -Mathematical content: a smooth manifold equipped with a smooth, -symmetric, positive-definite tensor field $g_x : T_xM \times T_xM \to -\mathbb{R}$. Equivalent to the textbook data $(M, g)$. - -The metric is exposed as a `[RiemannianMetric modelI M]` instance via -`RiemannianManifold.toRiemannianMetric`. Existing operators written -against `RiemannianMetric I M` keep working under this instance. - -## §2 Backward-compatibility bridges - -For any `[RiemannianManifold M]`, the following typeclasses synthesize -automatically: - -* `NormedAddCommGroup E` via `SmoothManifold.normedAddCommGroup_E` -* `NormedSpace ℝ E` via `SmoothManifold.normedSpace_E` -* `TopologicalSpace H` via `SmoothManifold.topologicalSpace_H` -* `ChartedSpace H M` via `SmoothManifold.chartedSpace_M` -* `IsManifold modelI ∞ M` via `SmoothManifold.isManifold_M` -* `RiemannianMetric modelI M` via `RiemannianManifold.toRiemannianMetric` - -Operators in `Riemannian/Connection.lean`, `Riemannian/Gradient.lean`, -`Riemannian/Curvature.lean`, etc. take these as separate typeclass -arguments. They all compose under `[RiemannianManifold M]` without -the user mentioning $E, H, \text{modelI}$ explicitly. - -## §3 Notation contract - -Notations in `Util/Notation/` activate under `open scoped Riemannian -OpenGALib`. Once `[RiemannianManifold M]` is in scope, the user writes: - -| Notation | Meaning | -|------------------|------------------------------------------| -| `metricInner V W`| $g_x(V, W)$ | -| `⟪V, W⟫_g` | polymorphic inner product (point/section) | -| `‖V‖²_g` | polymorphic squared norm | -| `grad_g f` | manifold gradient $\nabla^M f$ | -| `Δ_g f` | scalar Laplacian $\operatorname{tr}_g \operatorname{Hess} f$ | -| `hess_g f` | Hessian as `(0,2)`-tensor section | -| `Ric(X, Y)` | Ricci tensor on smooth vector fields | -| `Ric_g(v, w) x` | Ricci tensor pointwise | - -Notation never exposes $\text{modelI}$ or $E$. If a notation requires -explicit annotation, the spec is wrong; fix the typeclass, not the -notation. - -## §4 Extension policy - -To add a new geometric structure on smooth manifolds: - -1. Define `class XManifold (M : Type*) [TopologicalSpace M] extends - SmoothManifold M where ...`. -2. Bundle the structural data fields. Mark typeclass-valued fields with - square brackets: `[fieldName : SomeTypeclass ...]` so they expose - as instances automatically. -3. Provide bridge instances to existing structure-specific typeclasses - if the new structure is a refinement. -4. Add a §1.x entry below documenting the new class and its bridges. -5. Update `Util/Notation/` if the new structure introduces new - conventional notation (LaTeX-aligned, no machinery suffixes). - -### Currently registered structures - -* **`§1.1 SmoothManifold M`** — base smooth structure. -* **`§1.2 RiemannianManifold M`** — extends with metric. - -(Future: `LorentzianManifold`, `KählerManifold`, `SymplecticManifold`, -`ContactManifold` — all extend `SmoothManifold M` per §4.) - -## §5 Anti-patterns - -Things this spec prohibits (lint these out in review): - -* **Manifold operator with `[I]`-bracket notation**. `Δ_g[I] f` is - legacy; new code uses `Δ_g f` under `[RiemannianManifold M]`. -* **Operator parameterizing over `I` explicitly** in user-facing - signature. `(I := I)` belongs in framework internals; user-facing - defs take `[RiemannianManifold M]` and read `modelI` if needed. -* **Two named defs for the same math object** (e.g. `manifoldGradientNormSq` - parallel to `‖grad_g f‖²_g`). One canonical form. Polymorphic - notation if the form recurs across types. -* **Duplicate typeclass fields**. If `XManifold M` extends - `SmoothManifold M`, do not re-declare `E, H, modelI` — inherit them. - -## §6 Versioning - -This spec versions with the framework. Breaking changes to a -registered class or its bridge instances require a release note in -the changelog. Adding new classes per §4 is non-breaking. - -**Current version**: 0.1 (initial spec, two registered classes).