Update#1
Merged
Merged
Conversation
Xinze-Li-Moqian
added a commit
that referenced
this pull request
May 9, 2026
- Remove .codex-gitconfig: Windows-specific Codex tooling artifact accidentally bundled with the contribution; not project state. - Drop Loop space stanza from Riemannian.lean public API list. The file and import are retained; names (BasedLoop, FreeLoop, LoopInterval) are not yet committed as stable surface pending iteration over Mathlib.Topology.Path. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Xinze-Li-Moqian
added a commit
that referenced
this pull request
May 9, 2026
- Remove .codex-gitconfig: Windows-specific Codex tooling artifact accidentally bundled with the contribution; not project state. - Drop Loop space stanza from Riemannian.lean public API list. The file and import are retained; names (BasedLoop, FreeLoop, LoopInterval) are not yet committed as stable surface pending iteration over Mathlib.Topology.Path.
Xinze-Li-Moqian
added a commit
that referenced
this pull request
May 9, 2026
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/. - 153 import lines rewritten from `import Foo.Bar` to `import OpenGALib.Foo.Bar` across 60 files (includes Riemannian.LoopSpace from PR #1). - 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; 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.
Xinze-Li-Moqian
added a commit
that referenced
this pull request
May 10, 2026
Substantive progress on manifold scalar Hessian-Lie: * `mfderiv_extChartAt_eq_id_eventually` (Helper #1): chart's mfderiv at base-point-in-coherent-nbhd is identity. Closed via `continuousLinearMapAt_trivializationAt_eq_core` + `coordChange_self` + `IsLocallyConstantChartedSpace`. ~20 lines, Mathlib upstream PR candidate. * Inner locality bridges (`h_inner_W`, `h_inner_V`) within main proof: `mfderiv f y (W y) = fderivWithin f_loc s (phi y) (W y)` on chart- coherent nbhd. Closed via `MDifferentiableAt.mfderiv` + `writtenInExtChartAt` unfolding + chart coherence. * Local pullback vectors `V_loc, W_loc : E_M → E_M` defined. Remaining: outer mfderiv chart-pullback + `mlieBracket` unfolding via `mlieBracketWithin_apply` + match against `flat_hessianLieWithin_apply`. ~30-50 lines of careful term-mode Lean.
Xinze-Li-Moqian
added a commit
that referenced
this pull request
May 10, 2026
`h_outer_W`/`h_outer_V`: outer mfderiv'd functions reformulated as `g_chart ∘ phi` where `g_chart : E_M → F` is the flat chart-form. Closed via `phi.symm ∘ phi = id` on chart source. Remaining: chain rule (`mfderiv (g_chart ∘ phi) x = fderiv g_chart (phi x) ∘ mfderiv phi x` + Helper #1) + flat Within application + RHS bridge via `mlieBracketWithin_apply`. ~30-50 lines.
Xinze-Li-Moqian
added a commit
that referenced
this pull request
May 10, 2026
Document concrete remaining steps after Helpers #1, #2 + locality bridges: 1. Smoothness of g_chart from f C² + V/W C¹ 2. Apply Helper #2 to LHS terms 3. Substitute V/W base-point identities 4. Apply flat_hessianLieWithin_apply 5. RHS bridge via Helper #2 + mlieBracketWithin_apply + Helper #1 Each step bounded mechanical follow-up. File: 1 sorry, build clean.
Xinze-Li-Moqian
added a commit
that referenced
this pull request
May 10, 2026
…cker `change` tactic to inline `extChartAt I x` for `rw [Helper #2]` fails due to `TangentSpace 𝓘(ℝ,F) (g_chart_W (...))` basepoint def-eq under HSub instance synthesis. Workaround requires explicit `@HSub.hSub` ascription or `show`-based goal restructuring (~30-40 lines). State: 1 sorry remaining (main body), Helpers #1, #2 + locality bridges + base-point identities all closed.
Xinze-Li-Moqian
added a commit
that referenced
this pull request
May 10, 2026
Multiple attempts to apply Helper #2 via rw/simp_only/show all blocked by Lean's `set phi := extChartAt I x` interaction with pattern matching. Architectural path documented; ~30-50 lines of careful term-mode work remains. State: 1 sorry, build clean. Helpers #1, #2 + locality + base-point identities all closed (~150 lines real proof in this file).
Xinze-Li-Moqian
added a commit
that referenced
this pull request
May 10, 2026
Added mDirDeriv-form Helper #2 (`mDirDeriv_chart_compose_apply`) — F-typed wrapper that sidesteps the basepoint HSub elaboration issue. Main theorem proof body now substantially fleshed out: * Re-fold to mDirDeriv form via show * Apply mDirDeriv-form Helper #2 to LHS terms (works on F-typed mDirDeriv) * Substitute V/W base-point identities * Apply flat_hessianLieWithin_apply * RHS: rewrite mDirDeriv f x via Filter.EventuallyEq.mfderiv_eq + Helper #2 * mlieBracketWithin_apply expansion via Helper #1 (chart mfderiv = id) Remaining gaps: * Smoothness premises sorry'd (5 sub-sorrys for f_loc C², V/W_loc, g_chart_W/V) * `mpullbackWithin V (range I)` vs `V ∘ phi.symm` identification (needs chart-inverse mfderiv = id helper) * `ContinuousLinearMap.id.inverse` simplification Architectural path complete; closure is substantive Lean engineering.
Xinze-Li-Moqian
added a commit
that referenced
this pull request
May 10, 2026
…lans 5 remaining sorrys in main theorem (4 smoothness + 1 mpullbackWithin bridge). All have concrete repair paths via: * hV.coordSmoothAt + IsLocallyConstantChartedSpace + extChartAt_symm pull * fderivWithin smoothness + clm_apply chain rule * chart-inverse mfderiv = id helper (analog of Helper #1) Bianchi I, flat Hessian-Lie, Helpers #1+#2, locality bridges, base-point identities, RHS bridge structure all in place (~250 lines real proof).
Xinze-Li-Moqian
added a commit
that referenced
this pull request
May 10, 2026
Closed via hV/hW.mdifferentiableAt → mdifferentiableAt_totalSpace projection → congr_of_eventuallyEq with chart-coherent identification of trivAt.cLMA = id (Helper #1 logic) → MDifferentiableWithinAt.differentiableWithinAt_comp_extChartAt_symm. Sorry count: 5 → 3. Riemannian package: 8 → 6.
Xinze-Li-Moqian
added a commit
that referenced
this pull request
May 10, 2026
After substantial closure in HessianLie.lean: - Helpers #1, #2: 0 sorry - Flat Hessian-Lie (univ + Within): 0 sorry - Inner/outer locality bridges: closed inline - Base-point V/W identities: closed - f_loc, V_loc, W_loc, g_chart_W, g_chart_V smoothness: all closed - Only h_lieBr_eq's mpullbackWithin bridge remaining Riemannian package: 8 → 4 sorrys this session.
Xinze-Li-Moqian
added a commit
that referenced
this pull request
May 10, 2026
id.inverse simplification in main theorem Helper #3 (`mfderivWithin_extChartAt_symm_eq_id_at_base`) closed via mfderiv_extChartAt_comp_mfderivWithin_extChartAt_symm + Helper #1. Main theorem: rewrite chain reaches `id (lieBracketWithin (mpullbackWithin V) (mpullbackWithin W) (range I) (phi x))` form. Final step needs: * `id v = v` (trivial) * `mpullbackWithin V (range I) =ᶠ V_loc` on chart-target nbhd within range I, via Helper #3 extended to nbhd + lieBracketWithin congruence
Xinze-Li-Moqian
added a commit
that referenced
this pull request
May 10, 2026
…-sorry) Final closure step: extended Helper #3 to chart-target nbhd via `Filter.Tendsto.mono_left` of phi.symm continuity + chart-coherence pull-back. Then `Filter.EventuallyEq.lieBracketWithin_vectorField_eq_of_mem` bridges `mpullbackWithin V (range I)` to `V_loc` (and same for W). The complete proof chain now: * Bianchi I (Connection/Bianchi.lean): 0-sorry ✓ * Flat scalar Hessian-Lie (univ + Within): 0-sorry ✓ * Helper #1 (chart mfderiv = id eventually): 0-sorry ✓ * Helper #2 (chart-compose mfderiv → fderivWithin): 0-sorry ✓ * mDirDeriv-form Helper #2: 0-sorry ✓ * Helper #3 (chart-inverse mfderivWithin = id at base): 0-sorry ✓ * Helper #3 extended (eventually within range I): 0-sorry ✓ * mfderiv_iterate_sub_eq_mlieBracket_apply (manifold scalar Hessian-Lie): 0-sorry ✓ (~250 lines real proof) Riemannian package: 4 → 3 sorrys (only Curvature.lean's 3 remaining, which are unblocked by this closure).
Xinze-Li-Moqian
added a commit
that referenced
this pull request
May 10, 2026
Restructure 726-line monolithic `Foundations/HessianLie.lean` into single-responsibility modules: * `HessianLie/Flat.lean` (105 lines) — flat fderiv versions * `HessianLie/ChartHelpers.lean` (175 lines) — Helper #1, #2, #3 * `HessianLie/Manifold.lean` (315 lines) — manifold version + mDirDeriv `HessianLie.lean` becomes a 30-line facade re-exporting the three. Engineering improvements: * Extracted 4 named helper lemmas in Manifold.lean (`MDifferentiableAt_of_tangent_bundle_section`, `DifferentiableWithinAt_chart_pullback_of_section`, `mfderiv_inner_eq_fderivWithin_eventually`, `mpullbackWithin_extChartAt_symm_eq_eventually`, `mlieBracket_eq_lieBracketWithin_chart_pullback`) — eliminates V/W code duplication in main proof body * Tightened docstrings (concise + structured) * Removed dev-comment noise; kept algorithmic 1-2 line annotations * `omit` clauses for unused typeclass instances * Total: 726 → 595 lines (-18%) with cleaner separation All 3 modules + facade build clean, 0-sorry. Riemannian package: 3 sorrys remaining (all in Curvature.lean).
Xinze-Li-Moqian
added a commit
that referenced
this pull request
May 13, 2026
Port external `riemannSec_eq_zero_of_Z_eq_zero` to OpenGALib's SmoothVectorField interface. Strategy: local frame `e.localFrame basisF` at `x` + smooth bump `χ` with `tsupport χ ⊆ e.baseSet` produces a finite-sum decomposition `Z =ᶠ ∑ gᵢ • s'ᵢ` near `x` where each `gᵢ x = 0` (since `Z x = 0` and `localFrame_coeff` is linear). Apply Z-slot scalar Leibniz (`riemannCurvature_smul_third_scalar_field`) and additivity (`riemannCurvature_add_third`) inductively to each summand; the empty case reduces via the zero-section identity for `leviCivitaConnection.isCovariantDerivativeOnUniv`. Item #2 in the Bochner closure plan (#1 = Z-slot locality landed).
Xinze-Li-Moqian
added a commit
that referenced
this pull request
May 13, 2026
…d + vanishing + eq_at Five new lemmas mirroring the Z-slot machinery for the first slot of riemannCurvature. The X-slot scalar Leibniz has clean cancellation (no h_interior required, no curvature correction): the Y(f) boundary contributions from the inner-section Leibniz pair against the Lie-bracket smul-Leibniz with opposite sign. * `riemannCurvature_smul_first_scalar_field`: R(f•X, Y) Z x = f x • R(X, Y) Z x * `riemannCurvature_add_first`: R(X+X', Y) Z = R(X, Y) Z + R(X', Y) Z * `riemannCurvature_eq_of_X_eventuallyEq`: X =ᶠ X' near x ⇒ R(X, Y) Z x = R(X', Y) Z x * `riemannCurvature_eq_zero_of_X_eq_zero_field`: X x = 0 ⇒ R(X, Y) Z x = 0 * `riemannCurvature_eq_of_X_eq_at`: X x = X' x ⇒ R(X, Y) Z x = R(X', Y) Z x Same chart-frame + bump + induction template as Z-slot vanishing, using `mlieBracket_smul_left` and `mlieBracket_add_left` for the direction-slot Leibniz rules. Item #4 in the Bochner closure plan (Z-slot chain #1-#3 already landed).
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
2 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.
No description provided.