Skip to content

Commit d13a3bf

Browse files
Xinze-Li-MoqianXinze-Li-Moqian
committed
Initial commit: OpenGA library
Lean 4 mathematical software library: - Riemannian (Connection, Curvature, SecondFundamentalForm, Gradient, Metric) - GeometricMeasureTheory (Variation, HasNormal, Stable, Varifold, Isoperimetric, FinitePerimeter) - MinMax (Sweepout) - Regularity (AlphaStructural, SmoothRegularity) - AltRegularity sub-project (paper companion)
0 parents  commit d13a3bf

111 files changed

Lines changed: 20815 additions & 0 deletions

File tree

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

β€Ž.astrolabesorryignoreβ€Ž

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
# Patterns to exclude from sorry catalog drift detection.
2+
# One path prefix per line. Anything matching is skipped.
3+
# Lines starting with `#` are comments.
4+
5+
# AltRegularity is a sub-project (paper companion) with its own
6+
# SORRY_CATALOG.md per CLAUDE.md. Exclude from main catalog count.
7+
AltRegularity/

β€Ž.github/workflows/ci.ymlβ€Ž

Lines changed: 82 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,82 @@
1+
name: CI
2+
3+
on:
4+
push:
5+
branches: [main]
6+
pull_request:
7+
branches: [main]
8+
9+
jobs:
10+
count-checks:
11+
name: Sorry / axiom count
12+
runs-on: ubuntu-latest
13+
steps:
14+
- uses: actions/checkout@v4
15+
16+
- name: Count sorries against SORRY_CATALOG.md
17+
run: |
18+
# Tightened regex: match only standalone `sorry` (line is exactly
19+
# whitespace-then-sorry-then-whitespace), `by sorry`, `:= sorry`.
20+
# Excludes docstring text like "sorry'd" or "left as sorry".
21+
ACTUAL=$(grep -rnE "^[[:space:]]*sorry[[:space:]]*$|by sorry|:= sorry" \
22+
--include="*.lean" \
23+
Riemannian GeometricMeasureTheory MinMax Regularity \
24+
2>/dev/null | wc -l | tr -d ' ')
25+
EXPECTED=32
26+
if [ "$ACTUAL" -ne "$EXPECTED" ]; then
27+
echo "::error::Sorry count drift: expected $EXPECTED, found $ACTUAL"
28+
echo "If the change is intentional, update SORRY_CATALOG.md (and the EXPECTED constant in this workflow)."
29+
echo "If unintentional, close the new sorry or revert the regression."
30+
exit 1
31+
fi
32+
echo "Sorry count: $ACTUAL (matches SORRY_CATALOG.md)"
33+
34+
- name: Count axioms against AXIOM_STATUS.md
35+
run: |
36+
# Match only true axiom declarations: `axiom <ident>` at start of line,
37+
# nothing trailing. Excludes docstring text where 'axiom' may begin a
38+
# wrapped sentence (e.g., `axiom about CovariantDerivative wrapping`).
39+
ACTUAL=$(grep -rnE "^axiom[[:space:]]+[a-zA-Z_][a-zA-Z0-9_']*[[:space:]]*$" \
40+
--include="*.lean" \
41+
Algebraic Riemannian GeometricMeasureTheory MinMax Regularity \
42+
2>/dev/null | wc -l | tr -d ' ')
43+
EXPECTED=0
44+
if [ "$ACTUAL" -ne "$EXPECTED" ]; then
45+
echo "::error::Axiom count drift: expected $EXPECTED, found $ACTUAL"
46+
echo "If the change is intentional, update AXIOM_STATUS.md (and the EXPECTED constant in this workflow)."
47+
echo "If unintentional, close the new axiom or revert the regression."
48+
exit 1
49+
fi
50+
echo "Axiom count: $ACTUAL (matches AXIOM_STATUS.md)"
51+
52+
build:
53+
name: Lake build
54+
runs-on: ubuntu-latest
55+
timeout-minutes: 60
56+
steps:
57+
- uses: actions/checkout@v4
58+
59+
- name: Install elan (Lean toolchain manager)
60+
run: |
61+
curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain none
62+
echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
63+
64+
- name: Print Lean version
65+
run: lean --version
66+
67+
- name: Cache .lake build artifacts
68+
uses: actions/cache@v4
69+
with:
70+
path: |
71+
.lake/build
72+
.lake/packages
73+
key: lake-${{ runner.os }}-${{ hashFiles('lake-manifest.json', 'lean-toolchain') }}
74+
restore-keys: |
75+
lake-${{ runner.os }}-
76+
77+
- name: Get Mathlib build cache
78+
run: lake exe cache get
79+
continue-on-error: true
80+
81+
- name: Build OpenGALib
82+
run: lake build

β€Ž.gitignoreβ€Ž

Lines changed: 30 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,30 @@
1+
# LaTeX build artifacts
2+
*.aux
3+
*.log
4+
*.blg
5+
*.bbl
6+
*.fdb_latexmk
7+
*.fls
8+
*.out
9+
*.toc
10+
*.synctex.gz
11+
*.pdf
12+
13+
# OS files
14+
.DS_Store
15+
16+
# IDE
17+
.vscode/
18+
19+
# Overleaf copy
20+
Thesis_Overleaf/
21+
22+
# Backup files
23+
**/backup/
24+
25+
# Reference papers
26+
resources/
27+
28+
# Lean build artifacts (Mathlib oleans, ~7G)
29+
.lake/
30+
lake-packages/

β€ŽAXIOM_STATUS.mdβ€Ž

Lines changed: 41 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,41 @@
1+
# Axiom Status
2+
3+
Central registry of `axiom` declarations in OpenGA. Every axiom carries a
4+
classification + repair plan. CI snapshots this list; new axiom additions
5+
require updating this file.
6+
7+
## Classification
8+
9+
* **PRE-PAPER** β€” gap in Mathlib API or framework primitive; closure path
10+
is framework self-build or Mathlib upstream.
11+
* **CITED-BLACK-BOX** β€” theorem quoted from a paper, body never proven in
12+
the framework.
13+
* **PAPER-INTERNAL** β€” proof obligation owned by an application paper, not
14+
the library.
15+
* **CONJECTURAL** β€” open mathematics.
16+
17+
## Current axioms
18+
19+
**Total**: **0** axioms.
20+
21+
The previous `tangentBundle_symmL_smoothAt` axiom (Phase 4.7.5.C) has
22+
been converted to a `theorem` declaration in Phase 5 (C'2) and then
23+
factored further: the public-facing
24+
`TangentBundle.symmLFlat_mdifferentiableAt` (in
25+
`Riemannian/TangentBundle/Smoothness.lean`) is closed modulo a single
26+
private helper `mfderivWithinFlat_mdifferentiableAt`, whose body is
27+
currently `sorry`'d (tracked in `SORRY_CATALOG.md`) with a detailed
28+
Mathlib-`Pullback.lean`-based proof outline. Helper closure remains a
29+
Phase 4.8 follow-up.
30+
31+
## Notes
32+
33+
* This catalog tracks **public-facing** axioms (those in OpenGA's
34+
Algebraic / Riemannian / GeometricMeasureTheory / MinMax / Regularity
35+
packages). Application papers (e.g., AltRegularity) maintain their own
36+
catalogs.
37+
* `private theorem ... := by sorry` declarations are **not** axioms (they
38+
are unfinished proofs, tracked in `SORRY_CATALOG.md`).
39+
* Updating this file: when adding a new `axiom`, add an entry with
40+
classification + repair plan. When closing an axiom (replacing with a
41+
real proof), remove its entry + record in `CHANGELOG.md` (Phase 6).

β€ŽAlgebraic.leanβ€Ž

Lines changed: 37 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,37 @@
1+
import Algebraic.BilinearForm.Basic
2+
import Algebraic.Instances.RatVector
3+
4+
/-!
5+
# Algebraic β€” field-generic computable algebraic core
6+
7+
A namespace for fully computable, field-generic algebraic structures.
8+
Currently provides:
9+
10+
- `Algebraic/BilinearForm/Basic.lean` β€” symmetric bilinear forms and
11+
their inner-product API, parameterised over any `Field π•œ`. Algebra
12+
lemmas (zero / neg / sub / add / smul) are field-generic.
13+
- `Algebraic/Instances/RatVector.lean` β€” the standard symmetric
14+
bilinear form on `Fin n β†’ β„š`, with `#eval` demonstrations producing
15+
actual rational numbers and `native_decide`-verified concrete
16+
equalities.
17+
18+
## Layering
19+
20+
This namespace is **independent of `Riemannian/`**: it provides the
21+
algebraic substrate. The Riemannian module specialises this content to
22+
`π•œ = ℝ` and adds smoothness; on a computable field like `β„š`, the same
23+
algebraic content runs as a program.
24+
25+
```
26+
Algebraic/ (π•œ-generic, computable)
27+
↑
28+
Riemannian/ (π•œ = ℝ + smoothness)
29+
```
30+
31+
## Reusability
32+
33+
`Algebraic/` is reusable across contexts that need bilinear forms
34+
without a smooth-manifold structure: quadratic forms in algebra,
35+
positive-definite forms in optimization, matrix calculus, Hermitian
36+
forms when π•œ = β„‚, etc.
37+
-/

β€ŽAlgebraic/BilinearForm/Basic.leanβ€Ž

Lines changed: 156 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,156 @@
1+
import Mathlib.LinearAlgebra.BilinearForm.Basic
2+
import Mathlib.Algebra.BigOperators.Group.Finset.Basic
3+
import Mathlib.Algebra.Order.Ring.Defs
4+
5+
/-!
6+
# Bilinear forms β€” algebraic core (field-generic)
7+
8+
A field-generic, fully computable algebraic core for symmetric
9+
positive-definite bilinear forms. This is the foundation upon which
10+
the Riemannian metric API (`Riemannian/Metric/`) is built when the
11+
field happens to be `ℝ` and smoothness is required; on a computable
12+
field like `β„š`, the same operations evaluate to actual numbers.
13+
14+
## Design
15+
16+
This file deliberately avoids:
17+
- Continuous linear maps (which require topology + `RCLike`)
18+
- Smoothness / `ContMDiff` (which require `ℝ` or `β„‚`)
19+
- Any non-computable Mathlib infrastructure
20+
21+
What remains is pure linear algebra: a bilinear form is a
22+
`B : V β†’β‚—[π•œ] V β†’β‚—[π•œ] π•œ`, with computable `inner`, `IsSymm`, and
23+
`IsPosDef` predicates.
24+
25+
## Reusability
26+
27+
The bilinear-form algebra layer is reusable across:
28+
- Riemannian metrics (when π•œ = ℝ, with smoothness added)
29+
- Hermitian forms (when π•œ = β„‚)
30+
- Quadratic forms in algebra
31+
- Positive-definite forms in optimization
32+
- Matrix calculus over arbitrary fields
33+
34+
**Ground truth**: standard linear algebra of bilinear forms.
35+
-/
36+
37+
namespace OpenGALib.BilinearForm
38+
39+
/-- A bilinear form on `V` over field `π•œ`: a linear map
40+
`V β†’β‚—[π•œ] V β†’β‚—[π•œ] π•œ`. -/
41+
abbrev Form (π•œ : Type*) [Field π•œ]
42+
(V : Type*) [AddCommGroup V] [Module π•œ V] :=
43+
V β†’β‚—[π•œ] V β†’β‚—[π•œ] π•œ
44+
45+
section Algebra
46+
47+
variable {π•œ : Type*} [Field π•œ]
48+
{V : Type*} [AddCommGroup V] [Module π•œ V]
49+
50+
/-- The bilinear form is symmetric. -/
51+
def IsSymm (B : Form π•œ V) : Prop :=
52+
βˆ€ v w, B v w = B w v
53+
54+
/-- The **inner product** $\langle v, w \rangle_B$ via a bilinear form. -/
55+
def inner (B : Form π•œ V) (v w : V) : π•œ :=
56+
B v w
57+
58+
/-- Inner product unfolds to bilinear-form application. -/
59+
@[simp]
60+
theorem inner_def (B : Form π•œ V) (v w : V) :
61+
inner B v w = B v w := rfl
62+
63+
/-! ## Algebra lemmas
64+
65+
These follow directly from `LinearMap` algebra. They form the field-
66+
generic version of the framework's `metricInner_*` lemmas. -/
67+
68+
/-- **Symmetry** (when the form is symmetric). -/
69+
theorem inner_comm {B : Form π•œ V} (hB : IsSymm B) (v w : V) :
70+
inner B v w = inner B w v :=
71+
hB v w
72+
73+
/-- **Additivity in left argument**. -/
74+
theorem inner_add_left (B : Form π•œ V) (v₁ vβ‚‚ w : V) :
75+
inner B (v₁ + vβ‚‚) w = inner B v₁ w + inner B vβ‚‚ w := by
76+
simp [inner_def, map_add, LinearMap.add_apply]
77+
78+
/-- **Additivity in right argument**. -/
79+
theorem inner_add_right (B : Form π•œ V) (v w₁ wβ‚‚ : V) :
80+
inner B v (w₁ + wβ‚‚) = inner B v w₁ + inner B v wβ‚‚ := by
81+
simp [inner_def, map_add]
82+
83+
/-- **Scalar mult in left argument**. -/
84+
theorem inner_smul_left (B : Form π•œ V) (c : π•œ) (v w : V) :
85+
inner B (c β€’ v) w = c * inner B v w := by
86+
simp [inner_def, LinearMap.smul_apply, smul_eq_mul]
87+
88+
/-- **Scalar mult in right argument**. -/
89+
theorem inner_smul_right (B : Form π•œ V) (c : π•œ) (v w : V) :
90+
inner B v (c β€’ w) = c * inner B v w := by
91+
simp [inner_def, smul_eq_mul]
92+
93+
/-- **Zero in left argument**. -/
94+
@[simp]
95+
theorem inner_zero_left (B : Form π•œ V) (w : V) :
96+
inner B 0 w = 0 := by
97+
simp [inner_def]
98+
99+
/-- **Zero in right argument**. -/
100+
@[simp]
101+
theorem inner_zero_right (B : Form π•œ V) (v : V) :
102+
inner B v 0 = 0 := by
103+
simp [inner_def]
104+
105+
/-- **Negation in left argument**. -/
106+
@[simp]
107+
theorem inner_neg_left (B : Form π•œ V) (v w : V) :
108+
inner B (-v) w = -inner B v w := by
109+
simp [inner_def, map_neg, LinearMap.neg_apply]
110+
111+
/-- **Negation in right argument**. -/
112+
@[simp]
113+
theorem inner_neg_right (B : Form π•œ V) (v w : V) :
114+
inner B v (-w) = -inner B v w := by
115+
simp [inner_def, map_neg]
116+
117+
/-- **Subtraction in left argument**. -/
118+
@[simp]
119+
theorem inner_sub_left (B : Form π•œ V) (v₁ vβ‚‚ w : V) :
120+
inner B (v₁ - vβ‚‚) w = inner B v₁ w - inner B vβ‚‚ w := by
121+
rw [sub_eq_add_neg, inner_add_left, inner_neg_left, sub_eq_add_neg]
122+
123+
/-- **Subtraction in right argument**. -/
124+
@[simp]
125+
theorem inner_sub_right (B : Form π•œ V) (v w₁ wβ‚‚ : V) :
126+
inner B v (w₁ - wβ‚‚) = inner B v w₁ - inner B v wβ‚‚ := by
127+
rw [sub_eq_add_neg, inner_add_right, inner_neg_right, sub_eq_add_neg]
128+
129+
end Algebra
130+
131+
section Order
132+
133+
variable {π•œ : Type*} [Field π•œ] [LinearOrder π•œ] [IsStrictOrderedRing π•œ]
134+
{V : Type*} [AddCommGroup V] [Module π•œ V]
135+
136+
/-- The bilinear form is positive-definite. -/
137+
def IsPosDef (B : Form π•œ V) : Prop :=
138+
βˆ€ v β‰  0, 0 < B v v
139+
140+
omit [IsStrictOrderedRing π•œ] in
141+
/-- **Positive-definite** (when the form is positive-definite). -/
142+
theorem inner_self_pos {B : Form π•œ V} (hB : IsPosDef B) (v : V) (hv : v β‰  0) :
143+
0 < inner B v v :=
144+
hB v hv
145+
146+
omit [IsStrictOrderedRing π•œ] in
147+
/-- **Self-inner non-negativity** (when positive-definite). -/
148+
theorem inner_self_nonneg {B : Form π•œ V} (hB : IsPosDef B) (v : V) :
149+
0 ≀ inner B v v := by
150+
rcases eq_or_ne v 0 with hv | hv
151+
Β· rw [hv, inner_zero_left]
152+
Β· exact le_of_lt (inner_self_pos hB v hv)
153+
154+
end Order
155+
156+
end OpenGALib.BilinearForm

0 commit comments

Comments
Β (0)