Add zero varifold API#2
Merged
Merged
Conversation
Xinze-Li-Moqian
added a commit
that referenced
this pull request
May 10, 2026
`mfderiv_chart_compose_apply`: chart-pullback chain rule for `g ∘ extChartAt I x` at base point. Closure path documented; ~30-40 line bounded follow-up. SORRY_CATALOG updated.
Xinze-Li-Moqian
added a commit
that referenced
this pull request
May 10, 2026
`mfderiv_chart_compose_apply` 0-sorry: for flat `g : E_M → F` DifferentiableWithinAt `range I` at `phi x`, manifold mfderiv of `g ∘ extChartAt I x` at x equals flat `fderivWithin g (range I) (phi x)`. Proof: composition MDifferentiableAt via `DifferentiableWithinAt.comp_ mdifferentiableWithinAt` + `MDifferentiableWithinAt.mdifferentiableAt`, then `MDifferentiableAt.mfderiv` chart-unfold, then `writtenInExtChartAt` = g on phi.target, then `fderivWithin` congruence on `nhdsWithin range I`. Riemannian package: 5 → 4 sorrys. Catalog updated.
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
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
…-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 10, 2026
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.
Xinze-Li-Moqian
added a commit
that referenced
this pull request
May 13, 2026
Add `riemannCurvature_eq_of_Z_eventuallyEq`: if Z =ᶠ[𝓝 x] Z' then R(X, Y) Z x = R(X, Y) Z' x. Each of the three terms in `riemannCurvature_def` is treated via the new public `covDeriv_congr_eventuallyEq_field` (locality of covDeriv in the differentiated field), which is a direct application of Mathlib's `IsCovariantDerivativeOn.congr_of_eventuallyEq` evaluated at X(x) — no direction-smoothness required. Warm-up step (item #2 in the Bochner closure plan) for the Z-slot vanishing → X/Y-slot mirror → pointwise-eq bundling chain.
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).
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.