|
1 | 1 | # `Riemannian/Util/` — engineering tax for the Riemannian layer |
2 | 2 |
|
3 | | -Per OpenGA's anchor-purity discipline (CLAUDE.md §"Engineering tax encapsulation"), |
4 | | -anchor files expose only `**Math.**`-tagged declarations; all `**Eng.**` and |
5 | | -`**Mixed.**` plumbing supporting those proofs lives here. Files inside `Util/` |
6 | | -are content-named — the folder name carries the `Util` role; individual files |
7 | | -describe their concrete content. No `Helpers` / `Base` / `Foundation` suffixes. |
8 | | - |
9 | | -## Files, grouped by theme |
10 | | - |
11 | | -### Chart Jacobian (smoothness of chart-frame derivatives) |
12 | | - |
13 | | -| File | Role | |
14 | | -|------|------| |
15 | | -| [`Chart/ChartJacobianCLM.lean`](./Chart/ChartJacobianCLM.lean) | **Smoothness of chart-Jacobian CLM-valued functions**: CLM-valued composites (e.g. `(triv α).symmL ℝ b`, `(triv α).continuousLinearMapAt ℝ b`) in `inTangentCoordinates` form. CLM-level operators. | |
16 | | -| [`Chart/ChartJacobianEntries.lean`](./Chart/ChartJacobianEntries.lean) | **Smoothness of chart-Jacobian matrix entries**: scalar-valued entries obtained by composing the CLM with model-basis vectors and projections. Scalar-level. | |
17 | | -| [`Chart/FlatChartDerivs.lean`](./Chart/FlatChartDerivs.lean) | **Tangent bundle — chart-derivative engineering**: `mfderiv` of chart maps under the flat (Euclidean-modeled) setup. | |
18 | | - |
19 | | -### Tangent bundle / section glue |
20 | | - |
21 | | -| File | Role | |
22 | | -|------|------| |
23 | | -| [`Tangent/TangentHelpers.lean`](./Tangent/TangentHelpers.lean) | **Tangent helpers — chart-bundle smoothness bridges**: general-purpose smoothness lemmas for chart-induced tangent-bundle constructions. | |
24 | | -| [`Tangent/TangentSpaceInstances.lean`](./Tangent/TangentSpaceInstances.lean) | **Typeclass instances on `TangentSpace I x` and the tangent bundle**: `instFiniteDimensionalTangent` (def-eq lift of `FiniteDimensional ℝ E`); `instRiemannianBundleOfHasMetric` (activates Mathlib's scoped fibre instances when `[HasMetric I M]` is in scope). | |
25 | | -| [`Tangent/TensorBundleCoercions.lean`](./Tangent/TensorBundleCoercions.lean) | **Riemannian (r,s)-tensor bundle — fiber-to-model coercion algebra**: coercion-level lemmas for `Tensor⟨r,s⟩` bundle. | |
26 | | -| [`Tangent/MfderivApplySection.lean`](./Tangent/MfderivApplySection.lean) | **Smoothness of `mfderiv f` applied to a tangent-bundle section**: machinery for proving that `(mfderiv f x).comp (v x)` is smooth when `f, v` are. | |
27 | | - |
28 | | -### Metric inner / Riesz / notation |
29 | | - |
30 | | -| File | Role | |
31 | | -|------|------| |
32 | | -| [`Metric/MetricNotation.lean`](./Metric/MetricNotation.lean) | **Polymorphic metric notation `⟪·, ·⟫_g` and `‖·‖²_g`**: dispatches over tangent-vector vs. section forms via `MetricInnerHom` / `MetricNormSq` typeclasses, resolved through `[HasMetric I M]`. | |
33 | | -| [`Metric/MetricInnerSmoothness.lean`](./Metric/MetricInnerSmoothness.lean) | **`metricInner` smoothness — pointwise / set / global variants**: `ContMDiffWithinAt` / `ContMDiff` / `MDifferentiable` parity siblings of the headline `metricInner_contMDiffWithinAt` in `Metric/RiemannianMetric.lean`. | |
34 | | -| [`Metric/MetricRieszBilinForm.lean`](./Metric/MetricRieszBilinForm.lean) | **Bridge from `RiemannianMetric.inner` to `BilinearForm.Form ℝ E`**: `toBilinForm`, `toBilinForm_isPosDef`. Supports the Riesz duality methods in `Metric/RiemannianMetric.lean`. | |
35 | | -| [`Metric/CotangentFunctional.lean`](./Metric/CotangentFunctional.lean) | **Half-Koszul cotangent functional**: bilinear-form construction in the Koszul formula. | |
36 | | - |
37 | | -### Covariant derivative |
38 | | - |
39 | | -| File | Role | |
40 | | -|------|------| |
41 | | -| [`CovDeriv/CovDerivBridges.lean`](./CovDeriv/CovDerivBridges.lean) | **`covDeriv` / `covDerivAt` simp bridges**: definitional unfolding lemmas. | |
42 | | -| [`CovDeriv/CovDerivSmoothness.lean`](./CovDeriv/CovDerivSmoothness.lean) | **Tensoriality + smoothness machinery for `koszulCovDeriv`**: the proof-level workhorse behind Levi-Civita smoothness. | |
43 | | - |
44 | | -### Operator simp lemmas |
45 | | - |
46 | | -| File | Role | |
47 | | -|------|------| |
48 | | -| [`Simp/ConnectionLaplacianSimp.lean`](./Simp/ConnectionLaplacianSimp.lean) | **Connection Laplacian — simp def-unfold**: `@[simp]` lemmas exposing the definitional shape of `Δ_g` for use in `rw` and `simp` calls. | |
49 | | -| [`Simp/DivergenceSimp.lean`](./Simp/DivergenceSimp.lean) | **Divergence — simp def-unfold**: same pattern for the manifold divergence operator. | |
| 3 | +Per OpenGA's anchor-purity discipline, anchor files expose only |
| 4 | +`**Math.**`-tagged declarations; `**Eng.**` and `**Mixed.**` plumbing lives |
| 5 | +under `Util/`. The files are grouped by the downstream layer they support. |
| 6 | + |
| 7 | +## Directories |
| 8 | + |
| 9 | +| Theme | Directory | Files | |
| 10 | +| --- | --- | --- | |
| 11 | +| Chart Jacobian | [`Chart/`](./Chart/) | `ChartJacobianCLM.lean`, `ChartJacobianEntries.lean`, `FlatChartDerivs.lean` | |
| 12 | +| Tangent / section glue | [`Tangent/`](./Tangent/) | `TangentHelpers.lean`, `TangentSpaceInstances.lean`, `TensorBundleCoercions.lean`, `MfderivApplySection.lean` | |
| 13 | +| Metric inner / Riesz / notation | [`Metric/`](./Metric/) | `MetricInnerSmoothness.lean`, `MetricNotation.lean`, `MetricRieszBilinForm.lean`, `CotangentFunctional.lean` | |
| 14 | +| Covariant derivative | [`CovDeriv/`](./CovDeriv/) | `CovDerivSmoothness.lean`, `CovDerivBridges.lean` | |
| 15 | +| Operator simp lemmas | [`Simp/`](./Simp/) | `OperatorSimp.lean` | |
| 16 | + |
| 17 | +`ChartJacobianSmooth.lean` was renamed to `Chart/ChartJacobianCLM.lean` |
| 18 | +because it proves smoothness of continuous-linear-map-valued chart-Jacobian |
| 19 | +composites. `ChartJacobianSmoothness.lean` was renamed to |
| 20 | +`Chart/ChartJacobianEntries.lean` because it proves scalar matrix-entry |
| 21 | +smoothness. |
| 22 | + |
| 23 | +`ConnectionLaplacianSimp.lean` and `DivergenceSimp.lean` were merged into |
| 24 | +`Simp/OperatorSimp.lean`. `CovDerivBridges.lean` remains a separate |
| 25 | +post-`LeviCivita` bridge file: it imports `Connection.LeviCivita`, while |
| 26 | +`Connection.LeviCivita` imports `CovDerivSmoothness.lean`; absorbing the bridge |
| 27 | +lemmas into `CovDerivSmoothness.lean` would create an import cycle. |
50 | 28 |
|
51 | 29 | ## Conventions |
52 | 30 |
|
53 | | -* **Math/Eng/Mixed tag** — every declaration begins its docstring with one of |
54 | | - `**Math.**`, `**Eng.**`, `**Mixed.**`. `Util/` files are predominantly |
55 | | - `**Eng.**` (engineering plumbing) and `**Mixed.**` (math statement on top of |
56 | | - engineering proof body); occasional `**Math.**` declarations are the math |
57 | | - parity variants that match `Metric/`-anchor-headline statements at a |
58 | | - different smoothness parameter. |
59 | | -* **No `set_option linter.xxx false`** — linter regressions are fixed at the |
60 | | - declaration level via `omit [...] in <decl>` or proper refactor, never by |
61 | | - blanket disable. |
62 | | -* **Anchor purity** — anchor files in sibling folders (`Connection/`, |
63 | | - `Curvature/`, `Metric/`, `Operators/`, `Volume/`, `TensorBundle/`, |
64 | | - `Instances/`, `Manifold/`) expose only `**Math.**`. Anything else lands |
65 | | - here. |
| 31 | +* Every declaration docstring starts with `**Math.**`, `**Eng.**`, or |
| 32 | + `**Mixed.**`. |
| 33 | +* Util files may contain engineering declarations; sibling anchor folders keep |
| 34 | + the mathematical surface clean. |
| 35 | +* Subdirectory names carry the grouping role. File names describe concrete |
| 36 | + content and avoid generic `Helpers` / `Base` / `Foundation` suffixes except |
| 37 | + where the historical API name is retained. |
| 38 | + |
0 commit comments