Riemannian volume layer: chart-pullback construction + BG signature + foundation polish#21
Closed
Xinze-Li-Moqian wants to merge 524 commits into
Closed
Riemannian volume layer: chart-pullback construction + BG signature + foundation polish#21Xinze-Li-Moqian wants to merge 524 commits into
Xinze-Li-Moqian wants to merge 524 commits into
Conversation
…ivity
Self-build framework lemma `OpenGALib.posDefBilin_isCoercive`: a continuous
positive-definite bilinear form on a finite-dim normed space is coercive
(`∃ c > 0, ∀ v, c*‖v‖² ≤ B v v`). Proof via min on compact unit sphere
+ quadratic homogeneity.
Apply to discharge `isVonNBounded` in
`RiemannianMetric.toBundleContMDiffRiemannianMetric`: level set
`{v | g.metricTensor x v v < 1}` is contained in metric ball of radius
`√(1/c) + 1`, hence von Neumann bounded
(`NormedSpace.isVonNBounded_of_isBounded`).
`contMDiff` field remains as documented PRE-PAPER sorry — Phase 1C spike
narrowed it to a chart-pullback equation
`(T_dual x).linearMapAt y ((g.metricTensor y) ((T_tan x).symm y v)) w
= (g.metricTensor y v) w`
which holds because the dual / tangent trivializations cancel on the chart
base set, but discharging requires a `Trivialization.symmL` +
dual-cancellation framework helper. The bridge is symbolic (framework's
public IPS API does not route through Mathlib's bundle path — see
`Metric/MathlibBridge.lean` "Phase 1C architectural lesson").
SORRY_CATALOG.md: bridge contMDiff entry added (PRE-PAPER, repair plan
documented).
Build: 3522 jobs pass.
Branch RG-metric-tangent: 4 commits. * Phase 1B spike: Mathlib RiemannianBundle bridge + architectural finding (NACG diamond identified) * Phase 1C: cascade migration of [InnerProductSpace ℝ E] → [NormedSpace ℝ E] in 18 files; framework bridges (NormedSpace, IsTopologicalAddGroup, ContinuousConstSMul) on TangentSpace; documented irreducible NACG diamond * Bridge isVonNBounded closure via self-build OpenGALib.posDefBilin_isCoercive Build: 3522 jobs pass.
- CLAUDE.md → .claude/CLAUDE.md (Claude Code project memory location) - SORRY_CATALOG.md → docs/SORRY_CATALOG.md (internal tracking, off root) - AXIOM_STATUS.md deleted (catalog held 0 entries) - .astrolabesorryignore deleted (referenced removed AltRegularity, no consumer) - docs/PHASE_4_7_REDESIGN_PLAN, PHASE_5_AUDIT, PHASE_5_PLAN, REFACTOR_PLAN, RIEMANNIAN_STANDALONE, SOFTWARE_QUALITY_AUDIT deleted (working memos, not lib content) Reference fixups: - Riemannian.lean / Riemannian/Metric.lean: docstring path docs/AXIOM_STATUS.md → docs/SORRY_CATALOG.md - .github/workflows/ci.yml: update SORRY_CATALOG.md path; rename axiom step to "expect zero" (no longer references deleted AXIOM_STATUS.md) Top-level Markdown is now README.md only.
Mathlib-style layout: every Lean module now lives under OpenGALib/, with OpenGALib.lean as the only root entry. Five sub-namespace umbrellas (Algebraic, Riemannian, GeometricMeasureTheory, MinMax, Regularity) and their subdirectories moved verbatim into OpenGALib/. - 152 import lines rewritten from `import Foo.Bar` to `import OpenGALib.Foo.Bar` across 59 files. - 24 docstring path references rewritten to the OpenGALib/ prefix. - lakefile globs collapse to `.andSubmodules `OpenGALib`. - CI sorry/axiom grep paths updated to scan `OpenGALib`. - references/ directory deleted (cite_verification table outdated since AltRegularity moved out; removed mention from CLAUDE.md). Namespaces inside files are unchanged (`namespace Riemannian` stays as-is); folder structure is now decoupled from Lean namespaces, mirroring the Mathlib pattern. Build verified end-to-end (3523 jobs, no new errors or warnings).
The MinMax subtree (Sweepout/{Defs, ONVP, NonExcessive, MinMaxLimit,
MassCancellation, HomotopicMinimization, Interpolation, PullTight}) was
CLS22 / Almgren-Pitts / DLT13 paper terminology, conflicting with the
"MinMax must not reference paper-specific concepts" rule. Min-max /
sweepout content belongs in a paper-companion repo, not the lib.
- 9 files deleted (~1100 LOC, 12 sorry'd statements removed).
- OpenGALib.lean: drop import + remove MinMax from layering diagram and
sub-namespace list.
- OpenGALib/Riemannian.lean: drop MinMax from layering ASCII; AltRegularity
consumer line removed (consumer moved out earlier).
- OpenGALib/Riemannian/BumpFunction.lean: drop "GMT / MinMax" downstream
mention.
- OpenGALib/GeometricMeasureTheory/{FlatDistance, Varifold}.lean: drop
"Used by Sweepout" docstring entries.
- docs/SORRY_CATALOG.md: drop MinMax row, totals 32 → 20.
- .github/workflows/ci.yml: EXPECTED 32 → 20.
- .claude/CLAUDE.md: rewrite Architecture section (4 sub-namespaces:
Algebraic, Riemannian, GMT, Regularity).
Build verified (3514 jobs, no new warnings).
Foundations/ was a misnomer: it bundled engineering infrastructure
(Notation, Tactic, Attributes — no mathematical content) with HessianLie
(genuine manifold lemma: mfderiv_iterate_sub_eq_mlieBracket_apply).
Splitting cleanly:
- OpenGALib/Riemannian/Foundations/{Notation,Tactic,Attributes}.lean
→ OpenGALib/Riemannian/Util/{Notation,Tactic,Attributes}.lean
(engineering layer, Mathlib-style: notation macros, simp set
declarations, tactic re-exports)
- OpenGALib/Riemannian/Foundations/HessianLie.lean
→ OpenGALib/Riemannian/HessianLie.lean
OpenGALib/Riemannian/Foundations/HessianLie/{ChartHelpers,Flat,Manifold}.lean
→ OpenGALib/Riemannian/HessianLie/{...}.lean
(peer to Connection/, Curvature/, etc.)
- 11 import lines rewritten across Riemannian + Curvature + Metric/Basic.
- Riemannian.lean docstring section "Foundations" → "Util — engineering
layer (no mathematical content)"; UXTestFoundations section renamed.
Build verified (3514 jobs, no new warnings).
…ure_antisymm
Engineering layer (Util/) gains its first real Riemann-tensor
infrastructure. The polish target on riemannCurvature_antisymm shrinks
12 lines → 3 lines while preserving the same mathematical content,
demonstrating the API design pattern for downstream curvature work
(Bianchi I, Curvature.lean's diagonal/symm theorems).
Util/ additions:
- Util/Attributes.lean: register_simp_attr riem_simp (paralleling
metric_simp). Declaration only — populated by lemmas in math files.
- Util/Tactic.lean: macro "riem_normalize" : tactic => simp only
[riem_simp]. Real executable tactic in Util, not just docstrings.
Math layer (Connection/Bianchi.lean) additions:
- riemannCurvature_unfold (@[riem_simp]): definitional expansion of
R(X,Y)Z to ∇∇ - ∇∇ - ∇_{[·,·]} form, as a rewrite. rfl proof.
- covDeriv_lambda_mlieBracket_swap: pulls Lie-bracket antisymmetry
through covDeriv's direction argument. Kept OUT of riem_simp because
the rewrite is symmetric in X ↔ Y and would loop a simp set; used
as explicit rw step instead.
Polished proof:
riemannCurvature_antisymm (X Y Z : Π x : M, TangentSpace I x) (x : M) :
riemannCurvature X Y Z x = -riemannCurvature Y X Z x := by
simp only [riem_simp]
rw [covDeriv_lambda_mlieBracket_swap]
abel
3 lines, each is one math step: (1) unfold R, (2) bracket-swap, (3)
algebraic close. Build verified (3514 jobs).
… def
Mathematical notation should expose the math object directly, without
Lean elaboration noise. Two fixes:
1. Notation eta-reduction (in Connection/Bianchi.lean):
- ∇[X] Y := covDeriv X Y (was: fun x => covDeriv X Y x)
- ⟦X, Y⟧ := VectorField.mlieBracket _ X Y
- Riem(X, Y) Z := riemannCurvature X Y Z
The eta-expansion fun x => f x is a Lean elaboration artifact that
does not match simp's normal form, breaking pattern matching for
subsequent rewrites. Mathematicians write ∇_X Y for the section
directly; ((∇_X Y))(x) for evaluation. The eta-reduced notation
matches both intuitions cleanly.
2. riemannCurvature def cleanup:
Replaced 4-line let-binding form with a single-line direct
expression: covDeriv X (covDeriv Y Z) x - covDeriv Y (covDeriv X Z)
x - covDeriv (mlieBracket I X Y) Z x. Reads as math without the
`let nablaYZ := fun x => covDeriv Y Z x` boilerplate.
3. Notations relocated to Connection/Bianchi.lean (sealed against
circular import of Util/Notation.lean ← Curvature ← Connection ←
Bianchi). Util/Notation.lean now hosts only post-Bianchi notations
(Ric, scal_g, II, H_g, grad_g).
Polish status of riemannCurvature_antisymm:
theorem riemannCurvature_antisymm (X Y Z) (x) :
Riem(X, Y) Z x = -Riem(Y, X) Z x := by
simp only [riem_simp]
rw [covDeriv_lambda_mlieBracket_swap]
abel
3 lines, math-faithful statement. Build verified (3514 jobs).
Architecture: `OpenGALib/Riemannian/Util/` → `OpenGALib/Util/`. Util is project-level engineering layer (Mathlib pattern), not a Riemannian-specific subnamespace. Future GMT / Regularity engineering content lands here naturally without further refactor. Notation tier split (3 files instead of 2): - Util/Notation/Connection.lean — pre-Bianchi: ⟪,⟫_g, ‖,‖²_g, ∇[X] Y, ⟦X, Y⟧. Imported by Bianchi so its def body reads as math. - Util/Notation/Riemann.lean — Riem(X, Y) Z. Imported by Curvature. - Util/Notation/Curvature.lean — Ric(X, Y), scal_g, II, H_g, grad_g. Post-Curvature tier; for end-user consumers. Riemann curvature def cleanup: - Removed `let nablaYZ := fun x => covDeriv Y Z x` boilerplate; body is now a single direct expression matching the math: `covDeriv X (covDeriv Y Z) x - covDeriv Y (covDeriv X Z) x - covDeriv (mlieBracket I X Y) Z x` Polish targets achieved: - riemannCurvature_def @[riem_simp] (rfl proof, `Util/Attributes`-tagged) - covDeriv_mlieBracket_swap_apply helper (no longer in simp set, used as explicit rw to avoid X↔Y loops) - riemannCurvature_antisymm in Curvature.lean (reads as `Riem(X, Y) Z x = -Riem(Y, X) Z x` with notation) - riem_normalize macro tactic in Util/Tactic.lean - Polished antisymm proof: simp only [riem_simp]; rw [...]; abel Notation forms intentionally rejected: - 𝒯[x] (clash with array indexing) - 𝒯 x / Tan x (clash with function application + typeclass inference failures with abbrev-based shorthands) - 𝔛(M) for vector fields (parser/typeclass issues in upstream files that can't transitively import the notation file) Kept literals: TangentSpace I x, Π x : M, TangentSpace I x. Math readability cost is small; software-engineering simplicity is large. Build verified (3517 jobs, no new warnings).
…duction Goal: same operation never costs more than the first time. Each recurring workflow becomes either a script (text-level) or a Lake script (AST-level), pointed to from a single decision tree. scripts/: - rewrite-import.sh OLD NEW — bulk import path rewrite, refuses dirty working tree, prefix match. - lean-grep.sh — grep -r restricted to .lean (excludes .lake/, .git/). - README.md — convention: lift into scripts/ after 3+ repetitions. docs/REFACTOR_PLAYBOOK.md: - Decision tree mapping refactor type → tool (LSP rename / scripts / Lake script / manual). - Pre-flight checklist (clean working tree, atomic commits, build). - Lake script vs bash matrix (Lake for AST-aware, bash for text). - Pitfall log from this lib's actual history: sed-corrupts-docstrings, open-scoped-namespace-not-imported, notation-parser-conflicts (T[x] vs Lean array indexing, T x vs function application), eta-reduction in notation RHS, typeclass inference stuck on _ in notation, force-pushing trailers persists in GitHub contributor cache. - Self-extending: playbook entry added to "Adding to this playbook" rule for 3+-repeat operations.
OpenGALib treats other Lean math libs as study material to learn from, not as code to copy in. Cloning a reference lib (e.g., qinz1yang/differential-geometry) into external/ is OK locally for browsing, but its files never enter our git history. When we incorporate ideas from a reference, we re-implement in our own conventions (notation, naming, simp set) under OpenGALib/, with the "Inspired by" credit in commit messages.
…spaces
Survey of qinz1yang/differential-geometry (cloned to external/, in
.gitignore) produces these architectural decisions for selective
integration into OpenGALib over time. No file content is ported in
this commit — only namespace skeleton + plan doc.
Skeleton:
- OpenGALib/Tensor/ — top-level (general, no metric):
- Multilinear/ — multilinear bundle
- Alternating/ — alternating bundle
- Product/ — tensor product bundle
- Mixed/ — mixed multilinear bundle
- DifferentialForm/ — differential forms
- OpenGALib/Riemannian/Tensor/ — Riemannian-specific tensor
(RSTensor: contraction, Lie
derivative, metric on tensors)
- OpenGALib/Riemannian/Operators/ — second-order operators on
Riemannian manifolds (Hessian,
Laplacian, NormGradSq, VossWeyl)
- OpenGALib/Algebraic/Auxiliary/ — math helpers (Fin equivalences,
Perm, Shuffle decomposition).
NOT engineering Util — these
are linear algebra primitives.
Plan doc: docs/EXTERNAL_INTEGRATION_PLAN.md
- Decisions: which subdirs get ported, which get skipped, where each
lands in OpenGALib.
- Architectural rationale: Tensor is top-level (no metric required;
Riemannian consumes it); Auxiliary is math (Algebraic/), not Util.
- Porting convention: re-implement in our notation/conventions, atomic
commit per coherent unit, attribution in commit message.
- Suggested order of operations (dep order, no deadline).
Skipped subdirs (out of OpenGALib's current focus):
- Analysis/ (122 files): Sobolev/Laplacian PDE
- Integral/ (92 files): manifold integration (revisit when consumer needs it)
- Synthetic/ (65 files): synthetic differential geometry — different paradigm
- External/ (92 files): their internal Mathlib gap-fillers
- VectorBundle/{VectorField, Section}: subsumed by Mathlib + our SmoothVectorField
Empty .gitkeep files mark intent without committing content prematurely.
Each subsequent atomic commit will replace one .gitkeep with real
content, ported to our conventions.
Inspired by qinz1yang/differential-geometry — architectural decisions,
not file content.
Step 1 of qinz1yang/differential-geometry integration plan (see docs/EXTERNAL_INTEGRATION_PLAN.md). Adds 4 declarations to extend Mathlib's `Module.Basis`: - `Module.Basis.cDualBasis` — continuous dual basis induced by a basis of `E`, transported across `(E →ₗ[𝕜] 𝕜) ≃ₗ[𝕜] (E →L[𝕜] 𝕜)`. - `Module.Basis.cDualBasis_apply_self` — duality pairing `b i (B j) = δᵢⱼ`. - `exists_predual_basis` — given a basis of the continuous dual, a predual basis of the original space exists. - `cdual_sum_repr` — sum representation of any continuous functional in a basis (continuous-linear analogue of `Module.Basis.sum_dual_apply_smul_coord`). Pure linear algebra over a `FiniteDimensional 𝕜 E` `[NormedSpace 𝕜 E]` ambient. No manifold dependency. Inspired by qinz1yang/differential-geometry/Tensor/Auxiliary/Basis.lean (authors: Jack McCarthy). Re-implemented under `OpenGALib.Algebraic.Auxiliary`. Decision: deferred porting Fin / Perm / MultiKroneckerDelta from their `Tensor/Auxiliary/`. Audit shows `Tensor/Multilinear/*` only imports `Auxiliary/Basis`, not the others. Fin / Perm / Kronecker get ported when starting Step 3 (`Tensor/Alternating/`), which actually consumes them — avoiding speculative ports of code with no current consumer. Build verified (3518 jobs, +1 file from prior commit).
Polish on top of dxww123's PR #2 ("Add zero varifold API"). Their original proof used `ext + constructor + case-split + cases hp` (8 lines mechanical). One-line term-mode using `Set.eq_empty_iff_forall_notMem` is cleaner and avoids the redundant backward direction (vacuous from `p ∈ ∅`). Inspired by review of qinz1yang/differential-geometry codebase patterns; standard Mathlib idiom for "this set is empty" proofs.
…g foundations Step 2 (Multilinear) complete + Step 3 (Alternating) partial. Inspired by qinz1yang/differential-geometry; re-implemented in OpenGALib namespace tier with our software-first conventions. Tensor/Multilinear/ (5 files, complete): - Bundle: vector bundle of continuous multilinear maps. Diamond-resolved smoothness via cpolynomial decomposition. - Comp: helper for diag-composition smoothness, sidesteps the ContinuousLinearMap.addCommMonoid vs NormedAddCommGroup-derived diamond via contDiff_clm_apply_iff + cpolynomialAt_uncurry_compContinuousLinearMap. - Basis, Fiber, Field: dimension/basis/sections. - Flip: argument exchange for CMM-valued CMMs. Tensor/Alternating/ (5 files, partial — Curry/Basis/Wedge deferred): - Bundle: alternating-maps vector bundle. - Comp: composition operations (incl. compContinuousAlternatingMap₂). - Congr, FDeriv, Flip: domDomCongr, fderiv-evaluation, alternating flip. Algebraic/Auxiliary/ (5 new files): - Fin: index-juggling lemmas (2 PRE-PAPER sorrys inherited from external). - Perm: permutation conjugations + Cauchy-Binet block-permutation. - MultiKroneckerDelta: generalized Kronecker delta with Cauchy-Binet identity. - LIContDiff: smoothness through linear-isometric embedding. - ShuffleSplit: side classification on ModSumCongr; removeNone properties. OpenGALib.lean: + import OpenGALib.Tensor.
…mapL Completes the alternating-algebra layer end-to-end. Wedge product, graded Leibniz, and the elementary-covector basis are now in the lib. Algebraic/Auxiliary/ (2 new files): - ShuffleDecomposition (~970 lines): bijection between left/right shuffle cosets and reduced ModSumCongr, the combinatorial heart of the wedge Leibniz rule. - ShuffleDeriv (~290 lines): sign-preserving (k, σ) ↔ (τ, j) bijection for graded d-Leibniz. Carries 3 PRE-PAPER sorrys (rank-injectivity counting, cardinality balance, sign on canonical Quotient.out') inherited from the external lib's also-unproven version. Tensor/Alternating/ (3 new files): - Curry (684 lines): uncurryFin / curryFin / uncurrySum / uncurryFinAdd + sign formulas + lift-comp-domCoprod identity. - Basis (~373 lines): elementary k-covectors + basis expansion via dual. - Wedge (~754 lines): wedge product, bilinearity, sign, associativity, Leibniz rule, basis expansion. Tensor/Product/ (2 new files, step-4 subset needed by Wedge): - HomEquiv: tensor-hom equivalence + induced normed-space structure on finite-dim TensorProduct. - Defs: TensorProduct.mapL + mapLBilinear + mapLBilinear_contDiff + ContinuousAlternatingMap.tensorProductMap. The original Tensor0SBundle / RSTensor section is dropped — that content belongs in Riemannian/Tensor/. Step 3 footprint total: 23 ported files (Auxiliary 7, Multilinear 6, Alternating 8, Product partial 2). Approx 6500 lines.
Adds Hessian + Laplacian operator API as a self-build framework subset,
reusing existing Levi-Civita / gradient / metric primitives. Chart-Christoffel
and divergence-theorem dependencies deliberately deferred — those belong with
the chart-machinery / RSTensor layer.
Hessian.lean (199 lines):
- hessianVF f X Y x := ⟨∇_X (∇^M f), Y⟩_g(x). One-liner via covDeriv +
manifoldGradient + metricInner.
- pointwiseBilin I M carrier abbrev for clients to plug concrete chart-Hessian.
- IsPointwiseSymm predicate.
- frobeniusSqFun, traceFun against canonical Module.finBasis ℝ E.
- bilinForm_trace_sq_le_card_mul_frobenius_sq: pure linear-algebra CS bound
(∑ B(v_i, v_i))² ≤ |ι| · ∑_{i,j} B(v_i, v_j)².
- traceFun_sq_le_dim_mul_frobeniusSqFun: pointwise specialisation, the
inequality used downstream of the Bochner identity to bound (Δf)² ≤ n·|Hess f|².
- traceFun_sq_div_dim_le_frobeniusSqFun: divided form.
Laplacian.lean:
- laplacianViaTrace B x := traceFun B x. Trace-of-Hessian definition (no
divergence-theorem dependency).
- laplacianViaTrace_add, _smul: linearity.
- laplacianViaTrace_sq_le_dim_mul_frobeniusSqFun: CS bound restated.
Deferred (out of scope here):
- Chart-Christoffel formula + concrete chartHessianTensor (~700 lines of
chart machinery).
- Voss-Weyl chart Δ formula (depends on divergence theorem / integration).
- Smoothness of Hessian as section of (0,2)-bundle (depends on RSTensor).
Inspired by qinz1yang/differential-geometry/Geometry/Hessian.lean +
Laplacian.lean (algebraic CS layer) — chart-coordinate machinery dropped.
Smooth differential n-forms on a normed space E valued in F. Builds on the already-ported Alternating layer (Bundle, FDeriv, Wedge). Defs.lean (~80 lines): - structure DifferentialForm n E F: smooth function E → E [⋀^Fin n]→L[ℝ] F. - notation Ω^n⟮E, F⟯. - FunLike + ext lemma. - Algebra: zero / add / neg / sub / scalar smul instances. Congr.lean (~60 lines): index reordering along an equivalence on the indexing type, propagating through the smooth-function layer. Rough.lean (~430 lines): point-eval computational layer — pointwise evaluation, smoothness lemmas, exterior derivative on representatives. Basic.lean (~480 lines): polished public API — wedge, pullback, exterior derivative, identities. Total ~1050 lines. All clean per LSP diagnostics. Inspired by qinz1yang/differential-geometry/DifferentialForm/* (authors: Yury Kudryashov, Jack McCarthy). Re-implemented in OpenGALib.Tensor.DifferentialForm namespace tier; semantics unchanged.
Step 4 余 — Tensor/Product/ (5 files, ~1340 lines):
- Pretrivialization: pretrivialization + coordinate change for tensor-product bundle.
- Bundle: vector-bundle structure on the tensor product of two vector bundles.
- Fiber: fibre-level normed instances + CLE to model fibre.
- Section: tensor product of smooth sections.
- Basis: basis of the tensor product of finite-dim spaces.
Tensor/Product is now end-to-end: HomEquiv + Defs (mapL) + bundle layer.
Step 7 prerequisite — Tensor/Multilinear/Curry (75 lines):
- continuousMultilinearMap_curryEquiv r r': isometry between (r+r')-multilinear
and r-multilinear-of-r'-multilinear via Fin (r+r') ≃ Fin r ⊕ Fin r'.
- continuousMultilinearMap_curryLeft / uncurryLeft as CLMs + round-trip.
Step 7 subset — Riemannian/Tensor/ (4 files, ~1320 lines):
- Defs: model fibres + (0,s) covariant + (r,s) mixed tensor bundle types.
(0,s) tensor bundle = Bundle.continuousMultilinearMap on TangentSpace.
- ChartJacobianSmooth + ChartJacobianSmoothness: smoothness of CLM-valued
composites involving tangent-bundle trivialisation Jacobians.
- BundleSectionContinuity: continuity of tensor-bundle sections.
Namespace: external used `DifferentialGeometry.Tensor`; renamed to
`OpenGALib` (with sub-namespaces preserved) for naming consistency.
Step 7 余 (Field, Contract, LieDerivative, Metric) deferred — depends on
Multilinear/Tensor (937 lines), which depends on VectorBundle/Section
(plan-skipped). Will revisit if a downstream consumer needs it.
Step 5 (Mixed) deferred — depends on Multilinear/Dual (1183 lines) +
VectorBundle/{Dual, Equiv}; speculative for current consumers.
Step 9 (Curvature merge) deferred to Phase B (audit pass) — substantive
decision rather than mechanical port; we have Levi-Civita-route curvature,
external uses chart-Christoffel route.
Inspired by qinz1yang/differential-geometry/{Tensor/Product, Tensor/Multilinear,
Tensor/RSTensor}/* (authors: Yuan Liao, Jack McCarthy).
Phase B audit: - Scanned for any pre-port file consuming Phase A ported content. - Result: zero pre-port files import or reference any ported public identifier. All ported content is currently isolated from the lib analytical core (GMT, Riemannian/Curvature/Connection/Gradient, Regularity). - Findings + repair plans recorded in docs/AUDIT_PHASE_B.md. Phase C tier 1 (documentation / facade — low risk): - OpenGALib.lean: refreshed top-level facade. Updated layering diagram to include Tensor; added phase status section (A complete / B complete / C in progress); summarised sorry status. - OpenGALib/Tensor.lean: expanded facade with sub-module index by category + Phase B note that Tensor namespace is currently a self- contained algebraic layer with no internal lib consumer (suitable for future Mathlib upstream PR or downstream bridge work). - OpenGALib/Riemannian.lean: added Operators/ and Tensor/ entries to the Files section; cross-referenced the Phase B audit plan for Curvature bridge. No semantic changes; pure documentation. Phase C tier 2 (naming consolidation, @[simp]/@[ext] audit) and tier 3 (substantive bridges: Curvature → tensor section, Hessian symmetry via HessianLie, manifold- valued DifferentialForm) are consumer-driven and deferred until pull surfaces.
docs/NAMING_CONVENTION.md: lib-wide rules for definitions, theorems, file structure. Goal: code reads like textbook math at the API surface, with engineering noise hidden. Enforced on all subsequent file refactors. Riemannian/Curvature.lean (901 → 760 lines, LSP clean): Renames (per §1, §2 of convention): - ricciTraceMap → curvatureEndo (the endomorphism z ↦ R(z, X) Y, before trace). - ricciFormAt → ricciTensor (drop "FormAt" engineering suffix). - ricciEndo → ricciSharp (musical isomorphism Ric#). - riemannCurvature_inner_diagonal_zero → riemannCurvature_inner_self_zero (Mathlib _self suffix convention). Local notation (per §4): - `cF[V]` for `SmoothVectorField.const (I := I) (M := M) V`. Replaces 84 verbose occurrences inside long ricciTensor body. Module docstring rewrite (per §5): - Textbook math statement of Riemann / Ricci / scalar curvature. - Main definitions + Main results indices. - Single Reference: do Carmo §4 line. - Removed: ## Form, ## Sorry status, ## Ground truth verbose enumerations. Per-theorem docstring tightening (per §6): - riemannCurvature_antisymm, ricci, riemannCurvature_inner_self_zero, ricci_symm, ricciTensor, ricciSharp, scalarCurvature: all docstrings now one-sentence math statement + Reference line, plus closure path for sorry'd theorems. UXTest section removed (per §8). Cross-file docstring updates: LeviCivita.lean / Smoothness.lean / HessianLie.lean / Riemannian.lean: 4 references to old names updated. No behaviour change (these were docstring-only mentions). This file is now the reference for the lib-wide refactor pass per docs/NAMING_CONVENTION.md §10.
Apply docs/NAMING_CONVENTION.md to three files. Reference example was
Riemannian/Curvature.lean; this commit scales the same standard.
Riemannian/Gradient.lean (132 → 71 lines, -46%):
- Module docstring rewritten textbook-style with Main definitions / results
indices and a single Reference: do Carmo §3 ex. 8.
- Removed: ## Form section, Real noncomputable def labels, UXTest section.
- Rename: manifoldGradient_riesz → manifoldGradient_inner_eq (describes the
result, not the proof technique).
Riemannian/Operators/Hessian.lean (199 → 186 lines):
- Module docstring rewritten with Main definitions / results indices.
- Removed: ## Form 2-layer enumeration, Inspired by, Ground truth boilerplate.
- Renames per NAMING_CONVENTION §1, §2:
- hessianVF → hessian (drop VF engineering suffix; vector-field input is
the only form here).
- pointwiseBilin → Bilin (drop redundant prefix; abbrev returns Type).
- frobeniusSqFun → frobeniusSq (drop Fun engineering suffix).
- traceFun → trace (drop Fun engineering suffix).
- traceFun_sq_le_dim_mul_frobeniusSqFun → trace_sq_le_dim_mul_frobeniusSq
(consistent with new names).
- traceFun_sq_div_dim_le_frobeniusSqFun → trace_sq_div_dim_le_frobeniusSq.
- Per-theorem docstrings tightened to 1-line math statement.
Riemannian/Operators/Laplacian.lean (92 → 95 lines):
- Module docstring rewritten.
- Rename: laplacianViaTrace → laplacian (drop ViaTrace boilerplate; this is
the canonical Laplace-Beltrami).
- Theorem renames cascade: laplacianViaTrace_add → laplacian_add etc.
Cross-file docstring updates:
- Tensor.lean: pointwiseBilin → Operators.Bilin in Phase B audit note.
- docs/AUDIT_PHASE_B.md: rename references + replace Finding 3 with note
that the snake_case/camelCase inconsistency is being resolved by Phase C
tier 2 per NAMING_CONVENTION (4 files refactored so far).
- Riemannian.lean facade: manifoldGradient_riesz → manifoldGradient_inner_eq.
LSP clean across all six files.
Consolidate `Metric.lean` (facade) + `Metric/{Basic, Riesz, Smooth, RieszSmooth}.lean`
into a single `Metric.lean` (785 lines across 5 files → 507 lines, -36%).
Structure follows verifiable-object decomposition (Typeclass → Inner →
TangentSpace instances → Riesz duality → Smoothness), not textbook-chapter
splits. Engineering helpers (`toBilinForm`, `clmDualEquiv`,
`metricToDual_isInvertible`, `metricRiesz_eq_inverse`,
`metricInverse_mdifferentiableAt`) made `private`. Only `metricToDualEquiv`
remains public (consumed by `Curvature.lean`).
`Metric/MathlibBridge.lean` retained as forward-compat (carries 2
PRE-PAPER sorrys); no longer cross-references deleted sub-files.
Downstream import paths updated: `Connection/{Koszul, KoszulCotangent,
LeviCivita}`, `Util/{Notation/Connection, Tactic}` now import
`Riemannian.Metric` (unified) instead of sub-files.
SelfTest section deleted (74 lines of `example` blocks; documentation,
not test). Module docstring rewritten to standard
`Main definitions` / `Main results` index per
`docs/NAMING_CONVENTION.md` reference style (Curvature.lean).
Build verified: `lake build OpenGALib.Riemannian` clean.
Lift the 4-time-repeated refactor pattern (Curvature, Gradient,
Operators/{Hessian, Laplacian}, Metric) into a documented procedure
with when-to-use / when-not / 10-step procedure / pitfall list.
Pitfalls captured from session experience: `where`-aux cross-reference
limit, sed double-substitution on `local notation` lines, BSD vs GNU
sed `\b`, Unicode `quotPrecheck` failure, `set_option ... in`
non-propagation, `Internal.lean` cyclic-import trap, post-merge
linter `unused section variable` cleanup.
Decision tree updated with new branch.
Consolidate `TangentBundle/{Smoothness, SmoothSection, SmoothVectorField,
MFDerivSmooth}.lean` into single `TangentBundle.lean` (1306 → 913 lines, -30%).
Sub-directory removed.
Structure follows verifiable-object decomposition:
1. Chart-coherence typeclass `IsLocallyConstantChartedSpace`.
2. `TangentSmoothAt` predicate + algebra (`zero/add/sub/neg/smul`) +
`tangent_smooth` tactic.
3. Chart-frame infrastructure: flat-typed `symmLFlat` /
`continuousLinearMapAtFlat` / `mfderivWithinFlat` + Layer 1-4 framework
smoothness theorems (mostly `private`).
4. Bundled `Riemannian.SmoothVectorField` + algebra.
5. `mfderiv_const_dir_smoothAt`, `mfderiv_smoothDir_smoothAt`.
Engineering helpers made `private`:
- `mfderiv_extChartAt_apply_smoothAt`
- `ContMDiffOn.{add_normed, finset_sum_normed}` (`_root_` decls)
- `contMDiffOn_clm_of_components`
- `contMDiffOn_continuousLinearMapAt_apply`
- `contMDiffOn_continuousLinearMapAtFlat`
- `contMDiffOn_mfderivWithinFlat`
- `mfderivWithinFlat_mdifferentiableWithinAt`
- `symmLFlat_eventuallyEq_mfderivWithinFlat`
- `mfderivWithinFlat`
Public API surface (used externally):
- `IsLocallyConstantChartedSpace` typeclass + accessor + `H`-self instance.
- `OpenGALib.TangentSmoothAt` + algebra closure + `tangent_smooth` tactic.
- `TangentBundle.symmLFlat` / `continuousLinearMapAtFlat` defs.
- `TangentBundle.symmLFlat_mdifferentiableAt`.
- `TangentBundle.continuousLinearMapAtFlat_contMDiffAt`.
- `TangentBundle.contMDiff_constSection_TangentSpace` (used by SVF.const).
- `Riemannian.SmoothVectorField` + algebra + `const`.
- `OpenGALib.mfderiv_const_dir_smoothAt`, `mfderiv_smoothDir_smoothAt`.
Imports redirected: `Riemannian.lean`, `Metric.lean`, `Curvature.lean`,
`Connection/{KoszulCotangent, LeviCivita, Smoothness}.lean`,
`HessianLie/ChartHelpers.lean`.
UX test section (33 lines of `tangent_smooth` regression `example` blocks)
deleted — documentation, not test.
Build verified: full `lake build` of `Riemannian + GeometricMeasureTheory +
Regularity` clean. Pre-existing sorries unchanged.
Single-file polish per NAMING_CONVENTION: - BumpFunction.lean: 263 → 130 lines (-50%). Remove SelfTest, drop Layer 1-4 narrative + Phase-tracking commentary. Module docstring rewritten textbook-style. - Instances/EuclideanSpace.lean: 107 → 53 lines (-50%). UXTest section removed (kept the substantive theorem `metricInner_eq_real_inner_self` in main body). - SecondFundamentalForm.lean: 163 → 79 lines (-52%). UXTest removed. Per-theorem docstrings reduced to one-line math statements. Build clean. No identifier renames; all external consumers unaffected.
- Connection.lean facade: 229 → 24 lines (-89%). Drop the 193-line UXTest section (8 example blocks for typeclass cascade regression); module docstring rewritten as a sub-module index. - Connection/Smoothness.lean: 104 → 31 lines (-70%). Drop the PRE-PAPER status / closure-path narrative; keep just the `covDeriv_const_smoothVF_smoothAt` theorem. The 4 Koszul/LeviCivita/KoszulCotangent/Bianchi sub-files retained intact: their docstrings are math-content (algebraic identities, do Carmo §2 Theorem 3.6 derivations) rather than UXTest decoration. Full consolidation deferred — single-file would be ~1700 lines and the sub-files map cleanly to math sub-objects (Koszul construction → Riesz extraction → curvature → Bianchi). Build verified clean.
Two small cosmetic improvements aligning with Mathlib idiom. 1. `Measure.IsRiemannianVolume` dot notation. Move `IsRiemannianVolume` from `OpenGA.Comparison.BishopGromov` namespace to `MeasureTheory.Measure` namespace (Mathlib-extension pattern), and swap argument order so `μ : Measure X` is the first explicit arg. The hypothesis now reads `μ.IsRiemannianVolume n_M` — same shape as Mathlib's `μ.IsFiniteMeasure`, `μ.IsLocallyFiniteMeasure`, etc. Drops the previous `local notation:50 m:51 " ≃ " "vol_g"` hack (which split-literal abused notation to get paper-shape) — dot notation is the standard Mathlib idiom for this. 2. RHS uses Mathlib's `μH[d]` scoped notation (`MeasureTheory.Measure.hausdorffMeasure d`) instead of the long fully-qualified call. `open scoped MeasureTheory` enables it. Sorry 32, shake 35, three linters all 0, lake build 3640 jobs clean.
The predicate `∃ c > 0, c ≠ ⊤ ∧ μ = c · μH[n]` was named `IsRiemannianVolume`, which is mathematically misleading: * The canonical Riemannian volume `vol_g` is **uniquely** determined by chart-pullback `vol_g|_U = √det(g_ij) · Lebesgue` (no scalar freedom). The predicate as stated admits arbitrary positive multiples — `2·vol_g`, `(1/π)·vol_g`, etc. — none of which are "the" Riemannian volume. * `vol_g = α(n) · μH[n]` only for a *specific* Federer–Hausdorff normalization constant `α(n) = ω_n / 2^n` (Mathlib's diameter-based convention); the predicate doesn't pin down `c = α(n)`. * The Hausdorff-multiple form is generic measure theory (parameterized over `[EMetricSpace X] [BorelSpace X]`), not Riemannian-specific. Rename + relocate: * `Comparison/Util/RiemannianVolume.lean` → `MetricGeometry/Util/ScalarMultipleOfHausdorff.lean` (generic measure-theoretic predicate ⇒ Layer 1 metric/measure util). * `Measure.IsRiemannianVolume` → `Measure.IsScalarMultipleOfHausdorff` (honest about what it actually says). * BG hypothesis updated: `μ.IsScalarMultipleOfHausdorff n_M`. The Bishop–Gromov volume comparison is scale-invariant, so this weaker predicate is sufficient as a hypothesis. The future Layer 3a real definition of `vol_g` (chart-pullback) will live in `OpenGALib/Riemannian/Util/RiemannianVolume.lean` (pending) and is a *specific* instance of this predicate; BG could optionally tighten its hypothesis to require the exact `vol_g` once that lands. Sorry 32, shake 35, three linters all 0, lake build 3640 jobs clean.
Open `riemannian-volume` Layer 3a sub-project: build canonical Riemannian volume `vol_g` with multi-view bridges, closing the `IsScalarMultipleOfHausdorff` BG stopgap when Phase 3 (Hausdorff bridge) lands. This commit lands **Phase 1 skeleton**: signature for the chart-pullback construction. Three PRE-PAPER sorries with full repair plans: * `Riemannian/Volume/ChartPullback.lean:75` — `volumeMeasure g : Measure M`. Construction body sorry'd; docstring carries the 3-step repair plan (chart-wise pushforward + chart-invariance via `g' = Jᵀ·g·J` cancelling the Lebesgue Jacobian + partition-of-unity glue). * `Riemannian/Volume/ChartPullback.lean:89` — `IsLocallyFiniteMeasure` instance. * `Riemannian/Volume/ChartPullback.lean:98` — `SigmaFinite` instance. Notation `dV_g[g]` for `volumeMeasure g`, scoped to `Riemannian`. Folder structure prepared for Phase 2-5 siblings: OpenGALib/Riemannian/Volume/ ├── ChartPullback.lean ← Phase 1 (THIS COMMIT) ├── VolumeForm.lean ← Phase 2 (pending) — top-form bridge ├── Hausdorff.lean ← Phase 3 (pending) — closes BG stopgap ├── Exponential.lean ← Phase 4 (pending) — exp_p pullback └── UniversalProperty.lean ← Phase 5 (pending) — uniqueness Ground truth: do Carmo Ch.1; Petersen Ch.7 §1; Lee Ch.16. CI baselines updated: * `EXPECTED` (sorry count): 32 → 35 (3 new Phase 1 sorries documented in `docs/SORRY_CATALOG.md`). * `EXPECTED_SHAKE`: 35 → 36 (one false-positive on `Mathlib.MeasureTheory.Constructions.BorelSpace.Basic` — needed for `[BorelSpace M]` typeclass but shake's constant-reachability analysis doesn't see it). `OpenGALib/Riemannian.lean` umbrella imports the new file. Three linters all 0, lake build 3641 jobs clean.
Phase 2 of `riemannian-volume` branch: pointwise Riemannian volume form at each point. The bridge theorem `vol_g(A) = ∫_A |dV_g|` is deferred to a Phase 2 follow-up commit (requires form-integration API on the alternating-form bundle, not yet in Mathlib or OpenGA Tensor layer). New file `Riemannian/Volume/VolumeForm.lean`: * `volumeFormAt g x : AlternatingMap ℝ (TangentSpace I x) ℝ (Fin n)` — the top alternating form on `T_xM` characterizing the Riemannian volume element. Sorry'd PRE-PAPER; repair plan in docstring (Gram-determinant construction + chart-invariance). * Notation `dV_g[g, x]` scoped to `Riemannian`. * Bridge theorem `volumeMeasure_eq_integral_volumeForm` documented in docstring but not declared (would require integration of forms over manifolds — separate infrastructure). Ground truth: Lee *Smooth Manifolds* Ch.16 Thm 16.32; do Carmo Ch.1 Prop 1.7; Petersen Ch.7 §1. CI: `EXPECTED` sorry count 35 → 36; shake unchanged at 36. SORRY_CATALOG updated. Three linters all 0, build 3642 jobs clean.
The Phase 2 commit (5b6bfc6) added volumeFormAt sorry but the CI baseline + catalog row didn't make it into the same commit. This follow-up commits the missing book-keeping. No code change.
Phase 3 of `riemannian-volume`: identification of `vol_g` with the
Federer-normalized n-dim Hausdorff measure,
vol_g = α(n) · μH[n]_{d_g} (Federer §3.2.46-50)
This is the **closing bridge** for the Bishop–Gromov hypothesis: once
proven, the headline `μ.IsScalarMultipleOfHausdorff n_M` constraint
(`Comparison/BishopGromov/VolumeComparison.lean`) can tighten to
`μ = volumeMeasure g`, removing the scale-invariance loosening.
New file `Riemannian/Volume/Hausdorff.lean`:
* `alphaFedererConstant n : ℝ≥0∞` — the Federer normalization. PRE-PAPER;
repair plan: explicit value `ω_n / 2^n` via Mathlib unit-ball volume.
* `volumeMeasure_eq_alphaFederer_smul_hausdorffMeasure` — the headline
bridge theorem. **CITED-BLACK-BOX (Federer §3.2.46-50)**: OpenGA
imports the statement; the proof, involving covering lemmas + density
estimates + rectifiability, is delegated to Federer's monograph.
**Typeclass diamond resolution.** The naive variable block with both
`[TopologicalSpace M]` and `[EMetricSpace M]` declares two different
`TopologicalSpace M` instances on the same type; `[BorelSpace M]` binds
to one of them, and `hausdorffMeasure` synthesis looks for the other,
failing with `failed to synthesize BorelSpace M`. Fix: drop the
explicit `[TopologicalSpace M]` from the variable block, let
`[EMetricSpace M]` provide it transitively. Same lesson applies to
future Riemannian/Volume files using Hausdorff measure.
Ground truth: Federer §3.2.46-50; Mattila Ch.6; Morgan Thm 2.1;
Krantz–Parks Ch.5.
CI: `EXPECTED` 36 → 38 (one PRE-PAPER constant + one CITED-BLACK-BOX
theorem). SORRY_CATALOG updated.
Three linters all 0, build 3643 jobs clean.
Phase 4 of `riemannian-volume`: deferred until Mathlib upstream lands
`Riemannian.expMap` (smooth-side, via geodesic ODE) or OpenGA framework
self-builds it on top of `riemannianEDist` + chart ODE.
New file `Riemannian/Volume/Exponential.lean` — declaration-empty,
documents the planned bridge equation
vol_g|_U = (exp_p)_* (det(d exp_p) · Lebesgue|_{T_pM})
and the Jacobi-field decomposition
det(d exp_p(t·ξ)) = t^{n-1} · J_ξ(t)
that fuels the Riccati / Hessian comparison in Bishop–Gromov's proper
proof, plus Cheeger–Colding splitting, Toponogov, Rauch, and the
broader Layer 3b comparison-geometry chain.
The file places `Riemannian/Volume/Exponential.lean` in the right
location so when Mathlib (or OpenGA) provides `expMap` smooth
interface, the bridge can be declared in this exact file without
further refactoring.
Ground truth: do Carmo Ch.10 §1 Prop 1.1; Petersen Ch.6 §3;
Sakai §III.4; Chavel §III.1; Cheeger–Ebin §1.4.
CI: sorry / shake unchanged (zero new declarations).
Three linters all 0, build 3644 jobs clean.
Phase 5 of `riemannian-volume`: uniqueness companion to the chart-pullback construction. Among all Borel measures on `M`, `vol_g` is the unique measure satisfying the chart-pullback formula (`vol_g(A) = ∫_φ(A) √det(g_ij ∘ φ⁻¹)` on every chart-coordinate open set). New file `Riemannian/Volume/UniversalProperty.lean`: * `volumeMeasure_unique` — measure-theoretic uniqueness theorem. PRE-PAPER; repair plan: Mathlib `Measure.ext_of_iUnion` on a π-system of chart-coordinate opens generating the Borel σ-algebra. Depends on Phase 1 follow-up (`volumeMeasure_chart_pullback_eq`). Estimated 30-50 LOC. Ground truth: standard measure-theoretic uniqueness (implicit in do Carmo Ch.1, Lee Ch.16; explicit in Bourbaki *Variétés Différentielles*). **Phase 5 closes out the `riemannian-volume` branch skeletons**: OpenGALib/Riemannian/Volume/ ├── ChartPullback.lean ✓ Phase 1 (volumeMeasure, locallyFinite, sigmaFinite) ├── VolumeForm.lean ✓ Phase 2 (volumeFormAt) ├── Hausdorff.lean ✓ Phase 3 (Federer bridge — closes BG stopgap) ├── Exponential.lean ✓ Phase 4 (placeholder, Mathlib gap on expMap) └── UniversalProperty.lean ✓ Phase 5 (uniqueness) All five views of Riemannian volume have their bridge-statement location reserved. Each repair plan (PRE-PAPER) details what's needed to close that phase's sorries. Phase 4 is the heaviest (Mathlib upstream exp-map gap); Phases 1-2-5 are framework self-build (~300-400 LOC total); Phase 3 is CITED-BLACK-BOX (Federer §3.2.46-50). CI: `EXPECTED` 38 → 39 (one PRE-PAPER uniqueness theorem). SORRY_CATALOG updated. Three linters all 0, build 3645 jobs clean.
First piece of *real* Phase 1 work (not skeleton): the Gram-matrix
infrastructure underlying the chart-pullback formula.
New file `Riemannian/Volume/Util/GramDeterminant.lean` (real defs +
real proof, **zero sorry**):
* `Riemannian.RiemannianMetric.gramMatrix g x b` —
`(g_x(b_i, b_j))_{ij}` Gram matrix of the metric at `x` relative
to a basis `b` of `T_xM`.
* `Riemannian.RiemannianMetric.sqrtGramDet g x b` — `√det(gramMatrix)`,
the volume Jacobian factor in the chart-pullback formula
`vol_g|_U(A) = ∫_φ(A) √det(g_ij ∘ φ⁻¹)(y) dy`.
* `Riemannian.RiemannianMetric.gramMatrix_symm` — proven via
`g.symm` (Mathlib RiemannianMetric symmetry field).
Sorry count unchanged at 39, shake unchanged at 36. Build 3646 jobs
clean. Three linters all 0.
Next pieces of Phase 1 (real work, separate commits):
* Phase 1b: `gramMatrix.posDef` + `sqrtGramDet_pos` (positive
definiteness ⟹ det positive ⟹ sqrt det positive).
* Phase 1c: chart-frame specialization (use `extChartAt` derivative
to pull back the standard basis of `E` to `T_xM`).
* Phase 1d: per-chart measure construction + chart-invariance.
* Phase 1e: partition-of-unity glue (closes the headline
`volumeMeasure` sorry).
Each is its own commit. Phase 1a establishes the foundation.
Phase 1b of `riemannian-volume` Layer 3a sub-project: positivity of the Gram-matrix determinant and its square root — the strict-positivity of the volume Jacobian factor. `Riemannian/Volume/Util/GramDeterminant.lean` extended with: * `gramMatrix_posDef` — Gram matrix is positive definite. **PRE-PAPER**: proof unrolls the Finsupp double-sum via bilinearity of `g.inner x` and uses `metricInner_self_pos` on the linearCombination `v = b.repr.symm y` (nonzero when `y ≠ 0`). Estimated 30-50 LOC of bilinear-form-on-basis manipulation; sorry'd pending an explicit `Finsupp.sum_apply_bilin`-style helper. * `gramMatrix_det_pos` — proven (`Matrix.PosDef.det_pos` chain). * `sqrtGramDet_nonneg` — proven (trivial `Real.sqrt_nonneg`). * `sqrtGramDet_pos` — proven (`Real.sqrt_pos.mpr` + `gramMatrix_det_pos`). So **three real proofs, one sorry'd posDef** in this commit. The sorry is contained in a single foundational lemma; once filled (likely as a single bilinear-form-on-Finsupp helper), the three downstream theorems need no change. CI: `EXPECTED` sorry 39 → 40; `EXPECTED_SHAKE` 36 → 37 (one false-positive on `Mathlib.Analysis.Matrix.PosDef` import — needed for `Matrix.PosDef.det_pos` but shake doesn't see through the chain). SORRY_CATALOG updated. Three linters all 0, build 3646 jobs clean.
Closes the gramMatrix_posDef sorry and adds the Phase 1c
basis-change transformation lemmas — the abstract precursor to
chart-invariance of the Riemannian volume.
* gramMatrix_posDef — Hermitian via TrivialStar reduction to
gramMatrix_symm; quadratic-form positivity expands
star y ⬝ᵥ G *ᵥ y into g_x(v, v) with v = b.equivFun.symm y ≠ 0.
* gramMatrix_basis_change — G(b') = Pᵀ · G(b) · P via
bilinearity expansion over Basis.sum_repr.
* sqrtGramDet_basis_change — |det P| · √det G(b) via
det_mul + sqrt_sq_eq_abs.
* Reorg: bilinear sum-distribution helpers
(metricInner_sum_smul_left/right) moved before posDef so
both posDef and basis-change consume them.
Sorry count 40 → 39 (Riemannian 9 → 8). CI EXPECTED updated;
catalog row pruned.
The chart-pullback Jacobian weight √det(g_ij(x)) for the chart-induced
basis at α — the integrand in the textbook chart-pullback formula
vol_g|_U(A) = ∫_{φ(A)} √det(g_ij ∘ φ⁻¹)(y) dy.
* chartSqrtGramDet g α x := Real.sqrt (chartGramMatrix g α x).det
* chartSqrtGramDet_pos — strict positivity on the trivialization
base set, via chartGramMatrix_det_pos + Real.sqrt_pos.
* chartSqrtGramDet_contMDiffOn — C^∞ on the base set, via
Real.contDiffAt_sqrt composed with chartGramMatrix_det_contMDiffOn.
* chartGramMatrix_eq_gramMatrix_chartBasisFamily — bridge from
MusicalIso's chart-specialized chartGramMatrix to the abstract
g.gramMatrix x (chartBasisFamily α hx) from Volume/Util/GramDeterminant.
* chartSqrtGramDet_eq_sqrtGramDet_chartBasisFamily — sqrt-level
bridge; specializing sqrtGramDet_basis_change through this gives
the chart-overlap |det P|·√det g transformation.
Wired into OpenGALib/Riemannian.lean. Sorry count unchanged at 39.
…k (0-sorry)
Chart-overlap pullback formulae for chartGramMatrix and chartSqrtGramDet,
via the abstract Basis.toMatrix change-of-basis path.
* transitionMatrix α₀ α₁ hx₀ hx₁ :=
(chartBasisFamily α₀ hx₀).toMatrix (chartBasisFamily α₁ hx₁)
— abstract LinearAlgebra precursor of the chart-transition derivative.
* chartGramMatrix_pullback_eq_mul — G_{α₁}(x) = Pᵀ · G_{α₀}(x) · P
via gramMatrix_basis_change + chartGramMatrix bridge.
* chartGramMatrix_det_pullback — det G_{α₁}(x) = (det P)² · det G_{α₀}(x).
* chartSqrtGramDet_pullback — chartSqrtGramDet g α₁ x =
|det P| · chartSqrtGramDet g α₀ x, the change-of-variables Jacobian
factor that the volume measure must absorb at chart overlaps.
The analysis-side identification transitionMatrix.det = (tangentCoordChange).det
is deferred until B3 change-of-variables needs it.
Wired into OpenGALib/Riemannian.lean. Sorry count unchanged at 39.
… bridge
Connects the abstract Basis.toMatrix change-of-basis matrix
`transitionMatrix α₀ α₁ hx₀ hx₁` to Mathlib's analysis-side
`tangentCoordChange I α₁ α₀ x`, the Fréchet derivative of the chart
transition map. This bridge is what makes the abstract |det P|
Jacobian factor admissible to Mathlib's change-of-variables theorems
(which consume |det fderiv|).
* transitionMatrix_eq_toMatrix_tangentCoordChange — full matrix-level
identification: transitionMatrix α₀ α₁ hx₀ hx₁ =
LinearMap.toMatrix (finBasis E) (finBasis E)
(tangentCoordChange I α₁ α₀ x).toLinearMap.
Index swap (α₁ α₀ on RHS) reflects contravariance of basis change
vs. forward chart transition.
* transitionMatrix_det_eq_tangentCoordChange_det — det specialization,
via LinearMap.det_toMatrix.
Proof uses Bundle.Trivialization.comp_continuousLinearEquivAt_eq_coord_change
+ VectorBundleCore.localTriv_coordChange_eq to identify e₀ ∘ e₁.symm
with tangentCoordChange I α₁ α₀ x pointwise.
ChartTransition.lean now ~210 LOC, completing B1 (external equivalent: 370 LOC).
Sorry count unchanged at 39.
Per-chart Riemannian volume measure, built from chartSqrtGramDet via the
three-step pushforward construction:
chartLocalMeasure g α := (extChartAt I α).symm.map
((modelHaar.restrict (extChartAt I α).target).withDensity
(ENNReal.ofReal ∘ chartSqrtGramDet g α ∘ (extChartAt I α).symm))
* modelHaar — canonical additive Haar measure on E induced by
Module.finBasis ℝ E.
* modelHaar_isAddHaarMeasure / modelHaar_sigmaFinite — derived
instances via Basis.addHaar's existing instances.
* chartLocalMeasure_def — unfolding lemma (rfl).
File-local Borel structures on E, M (private local instances) to avoid
diamond with downstream typeclass search.
This is the per-chart artifact that B3 (chart-overlap invariance) and
Glue (partition-of-unity sum) will build on. Wired into Riemannian.lean.
Sorry count unchanged at 39.
Foundational set-theoretic and analytic lemmas about the chart-transition
map on the overlap of two chart sources. These feed the upcoming B3
invariance theorem.
* extChartAt_image_measurableSet_of_open_subset_source — image of
an open subset of (chartAt α).source under extChartAt is Borel-
measurable in E (works without [I.Boundaryless] via I being a
closed embedding, hence measurable embedding).
* extChartAt_transition_image — extChartAt I α₁ ∘ (extChartAt I α₀).symm
carries (extChartAt I α₀) '' U to (extChartAt I α₁) '' U.
* extChartAt_transition_injOn_overlap_image — injectivity of the
chart-transition map on the overlap image, via injectivity of
extChartAt I α₁ on its source.
* extChartAt_transition_hasFDerivWithinAt_on_overlap_image — chart-
transition map has Fréchet derivative tangentCoordChange I α₀ α₁ x
on the overlap image, reduced from the range-I version via
HasFDerivWithinAt.mono on (extChartAt α₀).target ⊆ range I.
Wired into Riemannian.lean. Sorry count unchanged at 39.
Adds the chart-local pushforward → setLIntegral identification needed
for B3, and brings the entire Volume folder into compliance with
OpenGA engineering conventions.
ChartLocalIntegral.lean (new, 0-sorry):
* measurableSet_extChartAt_target
* aemeasurable_extChartAt_symm_restrict_target
* chartSqrtGramDet_continuousOn_source (ContMDiffOn → ContinuousOn)
* aemeasurable_chartSqrtGramDet_symm_pullback
* chartLocalMeasure_lintegral — full pushforward identity
* chartLocalMeasure_setLintegral_indicator
* setLIntegral_target_eq_setLIntegral_image — indicator trick
* chartLocalMeasure_lintegral_U_eq_setLIntegral_image — manifold-side
set-lintegral = chart-image set-lintegral on E.
Audit cleanup across all Volume/Util/Chart*.lean files:
* Removed `set_option linter.unusedSectionVars false` (was lazy carry-
over from external/differential-geometry style); the file-level
bypass is replaced by precise `omit [...] in` clauses on each
declaration that doesn't need a particular instance.
* All Volume files now pass MathTag, AnchorPurity, Naming linters
with 0 baseline; shake reports 0 unused imports; build is clean
with 0 unusedSectionVars warnings inside Volume/.
Wired ChartLocalIntegral into Riemannian.lean. Sorry count unchanged at 39.
…e identities
Four chart-overlap inverse-determinant identities, cancelling the
Jacobian factor in the upcoming B3 change-of-variables step.
* tangentCoordChange_comp_self_overlap — at a common overlap point,
tangentCoordChange α₁ α₀ x ∘ tangentCoordChange α₀ α₁ x = id_E.
Via Mathlib's triple-composition identity + self-identity.
* tangentCoordChange_det_mul_inv_det_eq_one — det product = 1, via
LinearMap.det_comp applied to the composition identity.
* abs_det_tangentCoordChange_mul_abs_det_inv — |det| product = 1.
* ennreal_abs_det_tangentCoordChange_mul_abs_det_inv — ENNReal.ofReal
of |det| product = 1, the form consumed by the change-of-variables
step of B3.
All declarations use omit [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
[NeZero (Module.finrank ℝ E)] since these are about Mathlib's
tangentCoordChange and don't need OpenGA's Riemannian structure.
Sorry count unchanged at 39. Build clean, no linter warnings.
…Measure (0-sorry)
The centerpiece of riemannian-volume: the two chart-local volume
measures at α₀ and α₁ give the same lintegral on any measurable
function over the chart-source overlap.
* chartSqrtGramDet_pullback_tangentCoordChange — combined pullback
formula in Mathlib's tangentCoordChange language:
chartSqrtGramDet g α₁ x = |det(tcc α₁ α₀ x)| · chartSqrtGramDet g α₀ x.
Bridges abstract chartSqrtGramDet_pullback through
transitionMatrix_det_eq_tangentCoordChange_det.
* chartLocalMeasure_lintegral_U_eq_of_overlap — the invariance theorem.
Convert both sides to chart-image setLIntegrals on E, apply
Mathlib's lintegral_image_eq_lintegral_abs_det_fderiv_mul with the
chart transition map, cancel the Jacobian via
ennreal_abs_det_tangentCoordChange_mul_abs_det_inv.
* chartLocalMeasure_restrict_overlap_eq — restricted-measure form,
via Measure.ext_of_lintegral.
With this in place, partition-of-unity glue (Glue.lean equivalent) can
combine chart-local measures into a chart-independent global measure,
closing the volumeMeasure sorry in Volume/ChartPullback.lean.
Sorry count unchanged at 39 (proof contributes 0). Volume folder
remains audit-clean: MathTag/AnchorPurity/Naming/shake/unusedSectionVars
all 0 violations.
…easure sorry
Glues the chart-local measures into a global Borel measure on M via a
smooth partition of unity, closing the long-standing volumeMeasure sorry.
* chartAtlasPOU I M — canonical smooth partition of unity on M,
subordinate to chart-source family, via Mathlib's existence
SmoothPartitionOfUnity.exists_isSubordinate_chartAt_source.
* chartAtlasPOU_isSubordinate — corresponding subordination property.
* riemannianMeasure g ρ : Measure M — the global glued measure as
Measure.sum (fun α => (chartLocalMeasure g α).withDensity (ρ α)).
* volumeMeasure g (in ChartPullback.lean) — closed:
:= riemannianMeasure g (chartAtlasPOU I M).
Diamond fix: MeasurableSpace M and BorelSpace M moved from file-local
private instances to consumer-supplied variable-block instances, so the
result type Measure M agrees with the downstream ChartPullback consumer
(which has its own [MeasurableSpace M] [BorelSpace M]). E and H Borel
structures remain file-local since they only appear inside the
construction, not in the public result type.
Shake cleanup: ChartLocalMeasure now imports ChartSqrtGramDet directly
(was transitively via ChartTransition). PartitionOfUnityGlue imports
ChartLocalMeasure directly (was via ChartLocalIntegral). CI shake
baseline 37 → 38 (net +1 from 2 new files).
Sorry count 39 → 38 (volumeMeasure closed). The remaining 2 sorries in
ChartPullback are the IsLocallyFiniteMeasure and SigmaFinite instances,
both Properties batch.
…OfHausdorff stopgap)
The Bishop-Gromov volume comparison theorem is now stated directly on
the canonical Riemannian volume vol_g, eliminating the stopgap
`(μ : Measure M) (hμ : μ.IsScalarMultipleOfHausdorff n_M)`
parameterization.
* BG hypotheses now: just hRic (Ricci lower bound) + (p, r, R, admissibility).
* Conclusion: dV_g[(HasMetric.metric : RiemannianMetric I M)].real B(p, R) /
V_K^n_M(R) ≤ ... / V_K^n_M(r).
* Variable block adds [SigmaCompactSpace M] (required by volumeMeasure).
* Drops MetricGeometry/Util/ScalarMultipleOfHausdorff import (no longer
used by BG — the predicate definition file stays for Hausdorff.lean's
future Federer-bridge consequence).
The proof remains sorry; the new signature is the *final form* against
which the Jacobi-field-comparison proof (exponential chart polar
coordinates) will close. Crucially, BG no longer requires the Federer
bridge `vol_g = α(n) · μH[n]` — that bridge becomes an independent
result for Hausdorff-form consumers, not on BG's critical path.
Ground truth path: do Carmo Ch.10 §2 Thm 2.2; Petersen Ch.9 Thm 27.
Sorry count unchanged at 38.
Pre-refactor cleanup of the Riemannian metric anchor, in preparation for
the explicit-g cascade across the curvature/operator/Bochner stack.
* Add method-call wrappers that the cascade will rely on:
- g.metricNormSq x V — pointwise squared norm
- g.metricInnerSection V W : M → ℝ — section inner product
- g.metricNormSqSection V : M → ℝ — section squared norm
Each with simp/metric_simp unfolding + nonneg lemmas.
* Promote metricInner_{add,smul}_{left,right} from `metric_simp`-only
to `@[simp, metric_simp]`, matching Mathlib's `inner_{add,smul}_*`
simp convention. (The zero/neg/sub family was already correct;
add/smul was an asymmetric omission.)
* Document the `set_option backward.isDefEq.respectTransparency false`
workaround on `instFiniteDimensionalTangent`. Explanation: Mathlib's
`TangentSpace I x := E` is a non-reducible `def`; strict isDefEq
(Lean 4 default) refuses to unfold it during instance synthesis,
blocking `FiniteDimensional ℝ E → FiniteDimensional ℝ (TangentSpace I x)`.
Disabling transparency-respect forces aggressive unfolding for this
one synthesis. Tracking diagnosis via Mathlib `#defeq_abuse`.
These three changes prepare the file as the "无懈可击" foundation for
the cascade refactor — every `_g`-style typeclass notation in the
curvature/operator/Bochner layers will now have a clean method-call
target on `g : RiemannianMetric I M`.
Sorry count unchanged at 38. Build clean.
Splits the Riemannian metric anchor along anchor-purity lines to truly
remove Eng plumbing from the Math-API file. Resolves the cycle that
previously forced `private toBilinForm` + `instance` exemptions to live
in the anchor.
Restructure:
* NEW: Metric/HasMetric.lean (51 LOC) — tiny type-level anchor
holding only `abbrev RiemannianMetric` + `class HasMetric`. No
methods, no instances. Imported by both `Metric/RiemannianMetric.lean`
and the new Util files, breaking the previous import cycle.
* NEW: Util/MetricRieszBilinForm.lean — `toBilinForm` +
`toBilinForm_isPosDef` (Eng bilinear-form bridge to algebraic-core
`BilinearForm.Form`). Takes `RiemannianMetric I M` as literal param
type so dot notation works.
* NEW: Util/TangentSpaceInstances.lean — both typeclass instances
(`instFiniteDimensionalTangent`, `instRiemannianBundleOfHasMetric`).
Imports HasMetric.lean (not RiemannianMetric.lean), no cycle.
* Metric/RiemannianMetric.lean (344 LOC, down from 363): now pure
Math API. Imports HasMetric + both Util files transitively, so
downstream consumers of this anchor still get the full setup.
AnchorPurity verified: 0 Eng/Mixed declarations remain.
* Downstream import tightening (3 files): ChartBasis.lean, VolumeForm.lean,
HasNormal.lean now import the lighter HasMetric.lean / TangentSpaceInstances.lean
instead of the full RiemannianMetric.lean. Per shake suggestions.
* CI shake baseline 38 → 39 (small structural drift from file split).
Sorry count unchanged at 38. Build clean.
This was the actual fix the user pushed back for after I'd reverted twice:
solving the cycle by extracting the type-level definitions to their own
tiny file, not retreating to `private` + exemptions.
Adds a topic-grouped reader's guide to the 15-file `Riemannian/Util/` directory. Files were flat with no sub-grouping; the README makes the five themes explicit: * Chart Jacobian (smoothness of chart-frame derivatives) * Tangent bundle / section glue * Metric inner / Riesz / notation * Covariant derivative * Operator simp lemmas Each entry has a one-sentence role description so a reader can navigate without opening every file. Convention section explains the Math/Eng/Mixed tagging, no-linter-bypass rule, and anchor-purity discipline. Naming wart documented: `ChartJacobianSmooth.lean` (CLM-valued) and `ChartJacobianSmoothness.lean` (scalar matrix entries) are genuinely different files, not duplicates. Future rename pass could clarify. Does not move any files or change build/sorry/shake state.
Adds a reader's guide to the top-level `OpenGALib/Util/` directory, complementing the existing per-layer `Riemannian/Util/README.md` and the `Linter/README.md` subdirectory. Distinguishes top-level Util (cross-layer engineering: notation, tactics, attributes, mfderiv extensions, architecture linters) from per-layer Util (layer-scoped engineering tax). Per CLAUDE.md §Architecture two-tier Util discipline. Lists each file (Attributes, Notation, Tactic, MFDeriv, Linter) with a one-sentence role description, and points to the Linter/ subdirectory which has its own README. Conventions section covers cross-layer scope rule, no-variable-block-for-general-lemmas, attribute/notation/lemma separation, and the procedure for adding a new linter. No code change.
The defining PDE of infinitesimal isometries: a Killing field's second covariant derivative is determined by the Riemann curvature acting on itself. Foundation for the Bochner–Yano dimension bound `dim Isom(M) ≤ n(n+1)/2` and rigidity of constant-curvature manifolds. Statement-only commit: theorem `IsKilling.second_covDeriv_eq_curvature` landed in `Curvature/RiemannCurvature.lean:817` with full repair plan in docstring. Infrastructure (`IsKilling`, `covDeriv`, `riemannCurvature`, `mlieBracket`, metric-compatibility, Killing equation) already in place; estimated 80-120 LOC for the proof body. Reference: do Carmo §3 Ex. 5; Petersen Ch. 8 §2; Cheeger–Ebin §1.84. Sorry count 38 → 39. SORRY_CATALOG.md updated with new entry + correction of stale bianchi_second line number (Connection.lean:956 → LeviCivita.lean:921). CI EXPECTED bumped. This is intended as a tractable independent math task for a future contributor — same difficulty profile as `bianchi_second` (mechanical proof, all infrastructure in position), but a different mathematical locale (isometries instead of curvature symmetries).
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Draft PR. Multi-commit feature branch staging the riemannian-volume sub-project + foundational refactors that motivate it.
Major milestones (most recent first)
Foundation polish (5 commits)
62bfea6Add statement-only sorry: Killing field PDE (∇²_{Y,Z} X = R(X, Y) Z). New math TODO assigned to @zhifeizhu92, branch `killing-pde` linked to Prove IsKilling.second_covDeriv_eq_curvature (Killing field PDE) #20.081a802OpenGALib/Util: README (top-level cross-layer engineering).0abdb9eRiemannian/Util: README inventory + conventions.6312583RiemannianMetric anchor refactor: split type / class to `Metric/HasMetric.lean`; Eng plumbing (`toBilinForm`, fibre instances) moved to `Util/MetricRieszBilinForm.lean`, `Util/TangentSpaceInstances.lean`. Anchor file now 0 Eng/Mixed declarations — pure Math API.e1da355RiemannianMetric polish: section-form wrappers (metricNormSq,metricInnerSection,metricNormSqSection), simp parity for_add/_smul, documented + later eliminatedset_option backward.isDefEq.respectTransparency false.Bishop–Gromov signature (1 commit)
9fd1435BG stated directly onvol_g(dropμ + IsScalarMultipleOfHausdorffstopgap). Federer bridge no longer on BG's critical path.riemannian-volume Phase 1: chart-pullback construction (10 commits)
827ba02Glue:chartAtlasPOU+riemannianMeasure→ closesvolumeMeasuresorry.vol_gnow a real definition.856f3afB3 main theoremchartLocalMeasure_lintegral_U_eq_of_overlap(chart-overlap invariance).83822cfB3 batch 3: tangentCoordChange composition + det-inverse identities.dd7e3b3B3 batch 2: ChartLocalIntegral (pushforward → setLIntegral) + Util linter cleanup (set_optionpurge).354fa71B3 batch 1: chart-overlap geometric plumbing.d0b9d9dChartLocalMeasure construction.1896ef5,ff90c37B1: chart-transition matrix + Gram pullback (with analysis-sidetangentCoordChangebridge).13b8895chartSqrtGramDet + bridge to abstract sqrtGramDet.498d90c,727f264Phase 1b/1c:gramMatrix_posDef+ basis-change formulae.d6c3f46Phase 1a: abstractgramMatrix+sqrtGramDet.Phase 2-5 skeletons (4 commits, all sorry'd with repair plans)
c839d55Phase 5:volumeMeasure_unique(universal property).1ed9883Phase 4: exponential-map bridge (placeholder, blocked on MathlibexpMap).0700ca9Phase 3: Hausdorff bridge (vol_g = α(n) · μH[n]).5b6bfc6Phase 2:volumeFormAtpointwise top-form.e710ea1(CI bump).799a892Phase 1 chart-pullback skeleton.State
Sorry delta breakdown (32 → 39)
The +7 sorries are all statement-only PRE-PAPER additions with full repair plans in docstrings + tracked in #5–#20:
Volume/ChartPullback.lean(volumeMeasure CLOSED in this PR; locally-finite + sigma-finite remain)Volume/VolumeForm.lean(top form)Volume/Hausdorff.lean(Federer bridge, blocked-upstream)Volume/UniversalProperty.lean(uniqueness)Curvature/RiemannCurvature.lean(Killing field PDE, new this PR)Net: closed 1 critical sorry (
volumeMeasureis now real), added 7 statement-only with explicit repair paths.Tracking issues
Why merge as draft now
killing-pdebranch can keep diverging without surprises.