OpenGA/OpenGALib.lean at main · MathNetwork/OpenGA · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
import OpenGALib.Algebraic
import OpenGALib.Tensor
import OpenGALib.Riemannian
import OpenGALib.GeometricMeasureTheory

/-!
# OpenGALib — Open Geometric Analysis Library

A Lean 4 library of algebraic, tensor, Riemannian-geometry,
geometric-measure-theory, and regularity primitives. Layered:

```
Algebraic ← Tensor ← Riemannian ← GeometricMeasureTheory
```

Each sub-namespace is built on Mathlib. Application papers consume this lib
as a separate sub-project (`require OpenGALib from ".."`).

## Sub-namespaces

* `Algebraic`               — field-generic computable algebraic core
                              (bilinear forms + concrete instances) plus
                              `Algebraic/Auxiliary/` combinatorial helpers
                              (Fin / Perm / Kronecker / Shuffle theory)
                              consumed by `Tensor/Alternating`.
* `Tensor`                  — vector-bundle tensor algebra: continuous
                              multilinear / alternating maps, tensor
                              products, differential forms. Independent
                              of metric.
* `Riemannian`              — Levi-Civita connection, Riemann / Ricci /
                              scalar curvature, second fundamental form,
                              manifold gradient, Hessian / Laplacian
                              operators, `(r,s)`-tensor bundle types.
* `GeometricMeasureTheory`  — finite-perimeter, varifolds, stationary,
                              tangent cones, rectifiability, isoperimetric.

The `Regularity` sub-namespace (Wickramasekera 𝒮_α + smooth regularity)
is paper-specific downstream content kept local — see `.gitignore`.

## Phase status

* **Phase A (port)** — complete. ~10 000 lines of tensor / shuffle /
  differential-form / operator content ported from external reference
  (qinz1yang/differential-geometry). See `docs/EXTERNAL_INTEGRATION_PLAN.md`.
* **Phase B (audit)** — complete. Findings in `docs/AUDIT_PHASE_B.md`. Net:
  ported content is self-contained, currently isolated from lib core; bridges
  to Curvature / Hessian-symmetry / manifold-DifferentialForm are tier-3
  Phase C work, consumer-driven.
* **Phase C (consolidation)** — in progress. Tier 1 (documentation / facade)
  current; tier 2 (naming / `@[simp]` audit) deferred; tier 3 (substantive
  bridges) consumer-driven.

## Sorry status

Per `docs/SORRY_CATALOG.md`. The Riemannian package carries zero existence
axioms; ported content carries 5 PRE-PAPER sorrys total (2 in
`Algebraic/Auxiliary/Fin`, 3 in `Algebraic/Auxiliary/ShuffleDeriv`),
all inherited from the external lib.
-/