Prove IsKilling.second_covDeriv_eq_curvature (Killing field PDE)#22
Closed
Xinze-Li-Moqian wants to merge 524 commits into
Closed
Prove IsKilling.second_covDeriv_eq_curvature (Killing field PDE)#22Xinze-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.
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).
Xinze-Li-Moqian
changed the title
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
4 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.
Closes #20.
Task
Prove the Killing field PDE — sorry-replacement work for issue #20.
```lean
theorem IsKilling.second_covDeriv_eq_curvature
(X : SmoothVectorField I M) (_hX : IsKilling X)
(Y Z : SmoothVectorField I M) (x : M) :
(∇[Y] (∇[Z] X)) x - (∇[∇[Y] Z] X) x = Riem(X, Y) Z x
```
Located at `OpenGALib/Riemannian/Curvature/RiemannCurvature.lean:817`.
Branch
Based off `riemannian-volume` (which carries the statement-only sorry). The current diff includes the 24 `riemannian-volume` commits; the proof contribution will appear as new commits on top as @zhifeizhu92 pushes to the `killing-pde` branch.
Once the parent PR #21 (Riemannian volume layer) lands in `main`, this PR can be rebased so the diff shows only the proof body change.
Repair plan (per docstring)
The standard proof composes:
Sketch:
The bulk of the proof is sign-bookkeeping across the 6 permutations.
Acceptance
References
OpenGA's curvature convention is `R(X, Y) Z := ∇_X ∇_Y Z - ∇_Y ∇_X Z - ∇_{[X, Y]} Z` (matches Petersen). do Carmo uses the opposite sign — when porting do Carmo's proof, flip R-signs.