diff --git a/docs/CONVENTIONS.md b/docs/CONVENTIONS.md index 25de74e..00d60cd 100644 --- a/docs/CONVENTIONS.md +++ b/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`. diff --git a/docs/NAMING_CONVENTION.md b/docs/NAMING_CONVENTION.md index 0d9551d..5095446 100644 --- a/docs/NAMING_CONVENTION.md +++ b/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) diff --git a/docs/REFACTOR_PLAYBOOK.md b/docs/REFACTOR_PLAYBOOK.md index 4d19385..9e7afb5 100644 --- a/docs/REFACTOR_PLAYBOOK.md +++ b/docs/REFACTOR_PLAYBOOK.md @@ -1,261 +1,55 @@ # Refactor Playbook -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 - -``` -What's the refactor about? -├─ Rename a single identifier (def, theorem, structure field)? -│ └─ VSCode F2 (Rename Symbol). -│ Lean LSP scans the import graph semantically. -│ Doesn't touch docstrings/comments. Safest possible. -│ -├─ Rewrite an import path prefix across many files? -│ └─ scripts/rewrite-import.sh OLD_PREFIX NEW_PREFIX -│ Idempotent, refuses dirty working tree, prefix-match. -│ -├─ Move file or directory? -│ └─ git mv first, then scripts/rewrite-import.sh. -│ git mv preserves rename detection in history. -│ -├─ Introduce or migrate notation? -│ └─ Hand-write a 5-line example file FIRST. Verify parsing, -│ typeclass inference, simp interaction — before any sweep. -│ THEN bulk-migrate via perl/sed AND audit docstrings -│ (text replace catches them too — see Pitfalls #2). -│ -├─ Change a typeclass cascade or generic signature? -│ └─ Manual. No bulk tool helps. Build incrementally. -│ Use git checkpoints between each step. -│ -├─ Need an AST-aware operation (rename only in code, not in -│ docstrings; find all theorems referencing X; etc.)? -│ └─ Lake script. See "Lake script vs bash" below. -│ -├─ Bulk delete dead content (e.g., a sub-package being removed)? -│ └─ git rm -r + scripts/lean-grep.sh to find dangling refs + -│ manual cleanup of those refs. -│ -└─ Consolidate textbook-style sub-files into a single verifiable - object (e.g., `Metric/{Basic, Riesz, Smooth, RieszSmooth}.lean` - → `Metric.lean`)? - └─ See "Verifiable-object consolidation" below. - Merge + private engineering + section organization + - redirect downstream imports + delete sub-files. -``` - -## Pitfalls (encountered, in this lib's history) - -1. **Text-level sed corrupts docstrings.** `sed 's/X/Y/g'` on `.lean` - files matches `X` inside `/-- ... -/` blocks too. After bulk - migration, search docstrings with `scripts/lean-grep.sh ''` - and clean residual mentions. Or use VSCode F2 (semantic) when - available. - -2. **`open scoped X` requires the namespace to exist via imports.** - Adding `open scoped X` to a file whose import graph doesn't reach a - `namespace X` declaration produces "unknown namespace X" build - error. After any sweep that adds scoped opens, verify with - `scripts/lean-grep.sh 'open scoped'`. - -3. **Notation prefix conflicts with built-in syntax.** - - `T[x]` clashes with Lean's array indexing (`term[term]`) - - `T x` (where `T` is an identifier) is parsed as function - application, beating a `notation:max "T " x:max` pattern - - Solutions that work: paren form (`Tan(x)`, like `Ric(X, Y)`), - bracket form with non-identifier prefix (`∇[X]`, since `∇` is in - Unicode category `Sm`, not `Lu`). - -4. **Notation requires careful eta-reduction.** `fun x => f x` - wrappers in notation RHS create lambdas that don't beta-reduce in - simp's normal form, breaking pattern matches in subsequent rewrites. - Always eta-reduce: `notation X => f` not `notation X => fun x => f x`. - -5. **Typeclass inference can fail through `_` in notation.** A - `notation:max "Tan(" x ")" => TangentSpace _ x` gets stuck when - Lean can't pin the implicit `I : ModelWithCorners` from - surrounding context. If this happens repeatedly, either: - (a) keep the original verbose form `TangentSpace I x`, or - (b) make `I` explicit in the notation. - `abbrev`-based shorthands hit similar issues. - -6. **Library-wide section deletion needs Python, not sed.** When deleting - a section bracketed by patterns like `^/-! ## UXTest` ... `^end XYZTest` - across many files, BSD `sed -i` patterns get fragile (different test - sections have different end-marker names). Python with `re.match` per - line, plus a backwards search for the matching `end XYZTest`, is - reliable and self-explaining. See `/tmp/strip_uxtest.py` style: - collect target files via `glob`, walk lines, locate start/end, splice. - -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. - -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**. - ---- +Source of truth for refactor workflows. Sister to `scripts/` (codemods) and CLAUDE.md (architectural stance). Goal: **same operation never costs more than the first time**. + +## Decision: pick the right tool + +| Refactor | Tool | +|---|---| +| Rename a single identifier | VSCode F2 (Lean LSP, semantic, skips docstrings) | +| Rewrite an import path prefix | `scripts/rewrite-import.sh OLD NEW` | +| Move file or directory | `git mv` then `scripts/rewrite-import.sh` | +| Introduce or migrate notation | Hand-write a 5-line example file FIRST (verify parsing, typeclass inference, simp interaction), then bulk-migrate, then audit docstrings (sed catches them too) | +| Change a typeclass cascade | Manual, incremental, git checkpoints | +| AST-aware (rename in code only, find theorems referencing X, audit `@[simp]` shapes) | Lake script (`import Lean`, use `Lean.Environment` etc.) | +| Bulk delete dead content | `git rm -r` then `scripts/lean-grep.sh` for dangling refs | +| Consolidate sub-files into one anchor | See "Verifiable-object consolidation" below | + +## Pitfalls (from this lib's history) + +1. **`sed` corrupts docstrings.** Matches inside `/-- ... -/` too. After bulk migration, `scripts/lean-grep.sh ''` and clean residual mentions. +2. **`open scoped X` requires the namespace to exist via imports.** Otherwise "unknown namespace X" build error. Verify with `scripts/lean-grep.sh 'open scoped'`. +3. **Notation prefix conflicts with built-in syntax.** `T[x]` clashes with array indexing; `T x` (identifier prefix) loses to function application. Use paren form (`Ric(X, Y)`) or non-identifier prefix (`∇[X]`, where `∇` is Unicode `Sm`, not `Lu`). +4. **Notation requires eta-reduction.** `fun x => f x` in notation RHS breaks simp pattern matches. Always `notation X => f`, never `notation X => fun x => f x`. +5. **Typeclass inference fails through `_` in notation.** `notation "Tan(" x ")" => TangentSpace _ x` gets stuck when Lean can't pin the implicit. Either keep the verbose form or make the implicit explicit in the notation. +6. **Library-wide section deletion needs Python, not sed.** Different end-markers (`end XYZTest`) need per-line scanning with backwards-match for the closing token. BSD `sed -i` patterns are too fragile. +7. **Bulk attribution-paragraph strip needs paragraph-level matching.** `Inspired by ...` blocks span multiple lines ending at blank line / `-/` / next `## `. Line-level grep+replace only catches one line. +8. **Force-pushing doesn't fully remove a pushed `Co-Authored-By` trailer.** GitHub's contributor cache retains the orphan commit. Don't push to a public repo with a trailer you'd regret. ## Verifiable-object consolidation -The refactor that turns a *textbook-chapter*-shaped split (`Foo/Basic.lean` -+ `Foo/Riesz.lean` + `Foo/Smooth.lean` + ... + `Foo.lean` facade) into -a single *verifiable-object*-shaped file (one `Foo.lean` containing the -full public API of one math object). - -Performed for: `Riemannian/Curvature.lean`, `Riemannian/Gradient.lean`, -`Riemannian/Operators/{Hessian, Laplacian}.lean` (rename + doc cleanup, -no merge), `Riemannian/Metric.lean` (5 → 1 merge), -`Riemannian/TangentBundle.lean` (4 → 1 merge), -`Riemannian/HessianLie.lean` (4 → 1 merge), -`Riemannian/Connection.lean` (5 → 1 merge, ~2100 line single file). - -### When to use - -* The current split corresponds to a workflow stage (`Basic` → - `Riesz` → `Smooth`), not to a sub-object boundary. -* Every consumer needs the union of two or more sub-files anyway - (e.g., `LeviCivita.lean` needed both `Riesz` and `RieszSmooth`). -* The facade is just `import Sub1; import Sub2; import Sub3` with - re-export semantics, no value beyond namespace bundling. -* Sub-files share the same `variable` block — duplication is itself - a smell. - -### When NOT to use - -* The sub-files correspond to genuinely separate math objects - (e.g., `riemannCurvature` vs `ricci` could plausibly be split if - consumers diverge — though currently they don't). -* The split provides actual modularity (consumer A imports only - the lightweight typeclass def, consumer B imports the heavy - smoothness theorems). Check `lean-grep` for asymmetric usage - before merging. -* Sub-file is a forward-compat / Mathlib-bridge / experimental - layer with its own life cycle (`MathlibBridge.lean` stayed - separate after the Metric refactor for this reason). +Turn a textbook-chapter-shaped split (`Foo/{Basic, Riesz, Smooth}.lean` + `Foo.lean` facade) into one anchor `Foo.lean` containing the full public API. -### Procedure +**Use when:** sub-files correspond to workflow stages, not sub-objects; every consumer needs the union; the facade is just `import; import; import`; sub-files share the same `variable` block. -1. **Identify the object.** Read the sub-files. Confirm they're all - API for the same math object (`RiemannianMetric` typeclass + - inner + Riesz + smoothness = one object; not four). +**Don't use when:** sub-files are genuinely separate math objects; the split provides real asymmetric modularity; the sub-file has its own life cycle (Mathlib-bridge, experimental). -2. **Audit external consumers.** For every public symbol in the - sub-files, grep the entire repo for references outside the - sub-files themselves: - ``` - scripts/lean-grep.sh '\b(symbol1|symbol2|...)\b' - ``` - Mark each as: (a) public, externally consumed; (b) internal - only — candidate for `private`. +**Procedure:** -3. **Audit external imports.** For each sub-file, grep `import` of - that path: - ``` - scripts/lean-grep.sh 'import OpenGALib.Riemannian.Metric\.' - ``` - List the consumer files. They will need their `import` lines - redirected. +1. **Audit consumers.** `scripts/lean-grep.sh '\b(symbol1|symbol2|...)\b'`. Mark public vs internal-only (the latter → `private` after merge). +2. **Audit imports.** `scripts/lean-grep.sh 'import OpenGALib.Foo\.'`. List consumer files to redirect. +3. **Write the unified file.** Single import block, single variable block, sections ordered by dependency, internal helpers `private`. +4. **Redirect imports** in consumer files (collapse multi-imports to one). +5. **Delete sub-files**, then `lake build OpenGALib.` to verify. -4. **Plan section structure.** Order by dependency / use flow, - not by file-of-origin. For Metric: Typeclass → Inner + - algebra → TangentSpace instances → Riesz → Smoothness. - -5. **Write the unified file.** One `import` block (union), - one `variable` block (factored across sections where - applicable), section comments mark the structure. Engineering - helpers get `private` if step 2 says they're internal-only. - -6. **Redirect imports.** For each consumer file from step 3, - replace `import OpenGALib.Foo.Sub1` (etc.) with the single - `import OpenGALib.Foo`. Multiple sub-imports collapse to one - line. - -7. **Delete sub-files.** `rm OpenGALib/Foo/Sub*.lean`. - -8. **Verify per-file.** `lake env lean OpenGALib/Foo.lean` (LSP - diagnostics — silent = clean). Then each downstream consumer. - Then full `lake build OpenGALib.`. - -9. **Drop SelfTest sections.** Sub-file facades often have - `example` blocks proving the typeclass cascade works. These - are documentation, not tests — delete on consolidation. - -10. **Module docstring.** Rewrite to `# Object` + 1-paragraph - summary + `## Main definitions` + `## Main results` + - `Reference: `. Drop historical/phase-tracking - narrative. - -### Programmatic consolidation for large multi-file merges - -For `Connection/{5 files}.lean` (2500 lines) and similar large refactors, -hand-writing a unified `.lean` file is too costly. Use a Python script: - -1. Walk each sub-file in dep order (bottom-up: leaf first, facade last). -2. Collect imports / `open` / `open scoped` into sets (deduped at write time). -3. Strip per-sub-file leading docstring + `namespace X` / `end X` wrappers. -4. Detect notation-using lines that need denotation (e.g. `∇[X] Y` → `covDeriv X Y`) - if the unified file imports nothing downstream — handle by inline regex *or* - manual fix after build error report. -5. Tag known-internal symbols `private` via post-pass regex - (`^(theorem|def|noncomputable\s+def) ` → prepend `private`). -6. Write unified file with one module docstring at top. - -Pattern as run on Connection: ~50-line script, 90% mechanical, manual -fix-up of the 1-2 notation-bearing lines after first build attempt. -Saves ~30 min vs hand-writing. +For 2000+ line merges, automate steps 3-5 with a Python script: walk sub-files in dep order, dedupe imports/opens, strip per-file docstring + namespace wrappers, post-pass regex to tag `private`. ### Pitfalls specific to consolidation -* **Cyclic import via `Internal.lean` split.** Tempted to put - engineering in `Foo/Internal.lean` and re-import from - `Foo.lean`? `Foo/Internal.lean` would need the typeclass - defined in `Foo.lean` first. Solution: keep everything in - `Foo.lean`, use `private` + sections instead of file split. - (Tried during Metric refactor, abandoned.) - -* **`where`-aux blocks don't cross-reference.** Tempted to extract - proof helpers into `where`-aux at the bottom of a theorem? They - can't see each other. If `helper2` references `helper1`'s type, - `where`-aux won't compile. Solution: keep them inline as - `have` clauses, or extract to top-level `private theorem`s - outside the `where`-aux. (Tried during Curvature refactor on - `ricciFormAt`, reverted.) - -* **`backward.isDefEq.respectTransparency false` propagation.** - TangentSpace instance bridges need this option in scope. When - consolidating, the `set_option ... in` markers must come *with* - each instance/theorem that needs them, not at file top - (file-level `set_option` doesn't propagate transparently - through subsequent `instance` decls in the way you'd expect). - -* **Linter `unused section variable` after consolidation.** When - merging, a single `variable [g : RiemannianMetric I M]` block - covers both the typeclass-needing and typeclass-free theorems. - The linter flags theorems where `g` is unused. Add `omit [g] - in` (or `omit [IsManifold I ∞ M] in`, etc.) before each - affected theorem. - -* **Unicode notation `quotPrecheck` failure.** `local notation - "𝒞[" V "]" => SmoothVectorField.const ...` failed because Lean - rejects `𝒞` as an identifier head. Fall back to ASCII (`cF[V]`) - or use a Unicode symbol that's category `Sm` (e.g. `∇`, `⟦⟧`). - -* **`sed` double-substitution on `notation` lines.** `local - notation "cF[" V "]" => SmoothVectorField.const X V` — running - `sed 's|SmoothVectorField.const X V|cF[V]|g'` substitutes the - RHS too, producing recursive `notation "cF[" V "]" => cF[V]`. - Always exclude the notation declaration line from the sed - pass, or use the Edit tool with `replace_all=false` to be - surgical. - -* **BSD `sed -i` differs from GNU.** `\b` word boundary doesn't - work on macOS BSD sed. Use the Edit tool's `replace_all` mode - for cross-platform identifier renames within a single file. - +- **No `Internal.lean` split.** Tempting to extract engineering into `Foo/Internal.lean` and re-import — produces cyclic deps. Use `private` + sections inside the anchor instead. +- **`where`-aux blocks can't cross-reference.** Extract helpers as top-level `private theorem`s, not `where`-aux at the bottom. +- **`set_option backward.isDefEq.respectTransparency false`** must come *with* each instance/theorem that needs it, not at file top. +- **`unused section variable` after consolidation:** a single `variable [g : RiemannianMetric I M]` block covers typeclass-needing and typeclass-free theorems; add `omit [g] in` before each unaffected theorem. +- **`quotPrecheck` on Unicode notation prefix.** Lean rejects `𝒞` (Unicode category `Lu`) as identifier head. Fall back to ASCII (`cF[V]`) or category-`Sm` symbols (`∇`, `⟦⟧`). +- **`sed` self-substitution on notation lines.** `sed 's|RHS|cF[V]|g'` rewrites the notation declaration too. Exclude the declaration line or use Edit-tool with `replace_all=false`. +- **BSD vs GNU `sed -i`.** `\b` word boundary doesn't work on macOS. Use the Edit tool for cross-platform identifier renames. diff --git a/docs/SORRY_CATALOG.md b/docs/SORRY_CATALOG.md index 7644870..ccebe15 100644 --- a/docs/SORRY_CATALOG.md +++ b/docs/SORRY_CATALOG.md @@ -1,115 +1,29 @@ # Sorry Catalog -Central registry of `sorry` occurrences in OpenGALib. Every sorry carries a -classification and (for PRE-PAPER) a closure path. CI snapshots the total -count; new sorry additions require updating this file. - -## Scope - -This catalog covers `Algebraic`, `Tensor`, `MetricGeometry`, `Riemannian`, `Bridges`, -`Comparison`, and `GeometricMeasureTheory`. +Each `sorry` carries its closure plan in its docstring. This file lists the open count by classification + module; the strict baseline is enforced by `.github/workflows/ci.yml` (`EXPECTED` constant). ## Classification -* **PRE-PAPER** — gap in Mathlib API or framework primitive; closure path is - framework self-build or Mathlib upstream. -* **CITED-BLACK-BOX** — theorem quoted from a paper, body never proven in - the framework. The named theorem is the value; the proof is delegated to - the citation. +- **PRE-PAPER** — Mathlib API gap or framework primitive missing; closure path is self-build or Mathlib upstream. +- **CITED-BLACK-BOX** — theorem quoted from a paper as given; body never proven in the framework. The named theorem is the value. -## Total counts +## Open sorries (current) | Module | PRE-PAPER | CITED-BLACK-BOX | Total | |--------|-----------|------------------|-------| | Algebraic | 5 | 0 | 5 | | Tensor | 9 | 0 | 9 | | MetricGeometry | 0 | 0 | 0 | -| Riemannian | 1 | 0 | 1 | +| Riemannian | varies | 0 | — | | Bridges | 1 | 0 | 1 | | Comparison | 1 | 0 | 1 | | GeometricMeasureTheory | 5 | 10 | 15 | -| **Total** | **22** | **10** | **32** | - -CI workflow `.github/workflows/ci.yml` asserts the total equals 32 -(`EXPECTED=32`). - -## Algebraic (5) - -| File:line | Identifier | Classification | Notes | -|-----------|-----------|---------------|-------| -| `Auxiliary/Fin.lean:86` | `addCases_succAbove_castAdd` | PRE-PAPER | Mathlib gap on `Fin.addCases` ∘ `Fin.succAbove` interaction. Mechanical case split. | -| `Auxiliary/Fin.lean:98` | `addCases_succAbove_natAdd` | PRE-PAPER | Sister lemma to above. Same shape. | -| `Auxiliary/ShuffleDeriv.lean:284` | `derivShuffleEquivLeft` injectivity branch | PRE-PAPER | Internal case in shuffle-derivative bijection. Inherited from external lib port. | -| `Auxiliary/ShuffleDeriv.lean:300` | `derivShuffleEquivLeft` surjectivity (cardinality) | PRE-PAPER | Cardinality balance `(m+n+1)·C(m+n,m) = C(m+n+1,m+1)·(m+1)`. Inherited from external lib. | -| `Auxiliary/ShuffleDeriv.lean:312` | `derivShuffleEquivLeft_sign` | PRE-PAPER | Sign of canonical `Quotient.out'` representatives. Inherited from external lib. | - -## Tensor (9) - -| File:line | Identifier | Classification | Notes | -|-----------|-----------|---------------|-------| -| `Alternating/Wedge.lean:378` | `uncurryFin_wedge_productL_precompL` | PRE-PAPER | Algebraic identity matching LHS/RHS via `derivShuffleEquivLeft`. Closure path documented in proof body. | -| `Alternating/Wedge.lean:387` | `uncurryFin_wedge_productL_precompR` | PRE-PAPER | Sister identity with sign `(-1)^m`. | -| `Alternating/Wedge.lean:715` | `domDomCongr_finAddFlip_wedge_self` | PRE-PAPER | Depends on removed Mathlib lemma `Equiv.Perm.finAddFlip_equiv_eqFin`. Currently unused; revisit if needed. | -| `DifferentialForm/Basic.lean:194` | `ederiv_basis_expansion` | PRE-PAPER | Basis expansion of exterior derivative. Mechanical from `fderiv_basis`. | -| `DifferentialForm/Basic.lean:286` | `iprod_wedge` algebra | PRE-PAPER | Interior product / wedge product interaction; algebraic. | -| `DifferentialForm/Basic.lean:293` | `pullback.smooth` | PRE-PAPER | Smoothness of `ω ∘ fderiv f` composition. | -| `DifferentialForm/Basic.lean:323` | `pullback_ederiv` (differentiability gap) | PRE-PAPER | Inner gap in pullback-commutes-with-ederiv proof. | -| `DifferentialForm/Basic.lean:326` | `pullback_ederiv` (outer) | PRE-PAPER | Outer goal of same proof. | -| `Product/Pretrivialization.lean:281` | `tensorProductCoordChange_contMDiffOn` | PRE-PAPER | Bundle pretrivialization plumbing; Mathlib gap on tensor-product bundle smoothness. | - -## Riemannian (1) - -| File:line | Identifier | Classification | Notes | -|-----------|-----------|---------------|-------| -| `Connection.lean:956` | `bianchi_second` | PRE-PAPER | Differential Bianchi identity $(\nabla_X R)(Y,Z) W + \text{cyclic} = 0$. Statement-only commit (`a08f02a`). Repair plan (in docstring): expand `riemannCurvature_commutator_form`, distribute `covDeriv_sub_field` to 12 cov-deriv-of-cov-deriv terms, group into 6 pairs via torsion-freeness, close via `bianchi_first` + `SmoothVectorField.mlieBracket_jacobi`. Infrastructure in place; estimated 80-120 LOC. | - -The Bochner stack (closed via commit `de19ee7`) remains unconditional; -this is a *new* statement-only addition. Closure path documented above. - -## Bridges (1) - -| File:line | Identifier | Classification | Notes | -|-----------|-----------|---------------|-------| -| `RiemannianToLength.lean:101` | `IsRiemannianManifold.toLengthSpace` (`≤` direction) | PRE-PAPER | The bound `pathLength γ_continuous ≤ Manifold.pathELength I γ_smooth 0 1` for the `Path` constructed from a Mathlib smooth `γ : ℝ → M`. Closure path: partition-telescoping via `IsRiemannianManifold.out`, `Manifold.riemannianEDist_le_pathELength`, `Manifold.pathELength_add`, `Manifold.pathELength_mono` (~60–100 LOC). Repair trigger: first downstream consumer that destructures the `iInf` equation. See module docstring for the full repair plan. | - -## Comparison (1) - -| File:line | Identifier | Classification | Notes | -|-----------|-----------|---------------|-------| -| `BishopGromov/VolumeComparison.lean:39` | `bishopGromov_volume_comparison` | PRE-PAPER | **North-star.** Headline Bishop–Gromov volume comparison theorem (do Carmo Ch.10 §2 Thm 2.2 / Petersen Ch.9 Thm 27). Statement landed as the multi-stage driver of OpenGA Layer 1+3a+3b development. Closure path (sketched in the theorem docstring): Riccati comparison → Laplacian comparison → polar-coordinates volume comparison; each step needs Layer 3a infrastructure (smooth radial distance on `M ∖ Cut(p)`, Hessian comparison, polar-coordinates change-of-variables on Riemannian manifolds) that is not yet present. Sibling files in `Comparison/BishopGromov/` will host the chain. The proof, once landed, will also close the `Bridges/RiemannianToLength` `≤` sorry as a side effect. | - -## GeometricMeasureTheory (15) -| File:line | Identifier | Classification | Notes | -|-----------|-----------|---------------|-------| -| `Rectifiability.lean:85` | `isRectifiable_of_stationary_density_pos` | CITED-BLACK-BOX | Allard 1972 / Pitts 1981 rectifiability theorem. | -| `HasNormal.lean:128` | `tangentCone_unitNormal_exists` body | PRE-PAPER | Currently `Classical.choose` over trivial existence. Real repair: extract cone normal from chart-rescale weak limit. | -| `FinitePerimeter.lean:83` | perimeter measurability | PRE-PAPER | Mathlib BV-on-charted-manifold gap. | -| `FinitePerimeter.lean:135` | reduced-boundary trichotomy | PRE-PAPER | Density-based trichotomy (interior / boundary / exterior). | -| `Varifold.lean:114` | `density_nonneg` | PRE-PAPER | Direct from definition of density via mass. | -| `Varifold.lean:141` | support characterization | PRE-PAPER | Standard support-via-positive-mass-on-balls. | -| `Isoperimetric/SobolevPoincare.lean:156` | Sobolev–Poincaré inequality | CITED-BLACK-BOX | Maggi 2012 §13. | -| `Isoperimetric/Euclidean.lean:111` | Euclidean isoperimetric (eq form) | CITED-BLACK-BOX | Maggi 2012 §14. | -| `Isoperimetric/Euclidean.lean:135` | Euclidean isoperimetric (sharp constant) | CITED-BLACK-BOX | Maggi 2012 §14. | -| `Isoperimetric/ReducedBoundary.lean:113` | reduced boundary structure | CITED-BLACK-BOX | De Giorgi structure theorem; Maggi 2012 §15. | -| `Isoperimetric/ReducedBoundary.lean:152` | reduced boundary (variant) | CITED-BLACK-BOX | Maggi 2012 §15. | -| `Isoperimetric/BVFunction.lean:114` | BV approximation | CITED-BLACK-BOX | Maggi 2012 §10. | -| `Isoperimetric/Coarea.lean:73` | coarea formula | CITED-BLACK-BOX | Maggi 2012 §18. | -| `Isoperimetric/Coarea.lean:117` | coarea (variant) | CITED-BLACK-BOX | Maggi 2012 §18. | -| `Isoperimetric/Relative.lean:87` | relative isoperimetric | CITED-BLACK-BOX | Maggi 2012 §16. | +The Riemannian count drifts as feature branches add statement-only sorries. CI `EXPECTED` is the authoritative current value. For per-file location and repair plans, `grep -rn "sorry" OpenGALib/` and read each docstring. -## Notes +## Discipline -* PRE-PAPER is **not permanent technical debt**: every PRE-PAPER entry has a - concrete closure path (either Mathlib API to extend, or framework - self-build to perform). The classification distinguishes "ready to close - with focused work" from "deliberately delegated to a citation". -* CITED-BLACK-BOX entries are **stable by design**: the framework states a - named theorem from the literature and uses it without re-proving the body. - These are the seven Maggi 2012 / Allard 1972 references plus the Bochner - identity. -* Updating this file: when adding a new `sorry`, append a row with - classification + notes, and bump `EXPECTED` in `.github/workflows/ci.yml`. - When closing a sorry (replacing with a real proof), remove its row and - decrement `EXPECTED`. The per-module sub-table count must equal the - summary table count. +- Substantive chain proofs stay 0-sorry, non-circular. +- Never silently weaken a statement to remove a sorry. +- When adding a new `sorry`: write the repair plan in its docstring and bump `EXPECTED` in `ci.yml`. +- When closing a `sorry`: remove it and decrement `EXPECTED`.