Numina/aqft in lean - #38
Merged
Merged
Conversation
…spacetime model Stage 1 of notes/agents/plan-levi-civita-geodesics: new §10.4 nodes for a pseudo-Riemannian metric, metric-compatible and Levi-Civita connections, the Koszul formula and existence/uniqueness, the chart-free geodesic definition (affinely parametrised, imposed at interior parameters), and the Minkowski and isometry lemmas. def:trip and def:causal-trip now cite def:geodesic. Not yet formalized. Spacetime gains the instance field boundaryless : model.Boundaryless, which the new layer relies on (open chart targets). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
New Physicslib4/Geometry/PseudoRiemannian/{Basic,LeviCivita}.lean:
PseudoRiemannianMetric and the spacetime instance, metric compatibility and
Levi-Civita connections on Mathlib's CovariantDerivative, with the musical
isomorphism, Koszul formula, uniqueness and existence stated as sorry'd
theorems, and leviCivita chosen from existence. Blueprint links recorded.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Stage 3 of the Levi-Civita plan: bijective_val, IsLeviCivitaFor.koszul and IsLeviCivitaFor.uniqueness, following Mathlib's Riemannian proofs with the nondegenerate metric in place of the inner product. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…metric Completes stage 3: the Koszul connection (koszulAux, flatEquiv, leviCivitaAux, koszulConnection) is a covariant derivative, compatible with g and torsion-free, so exists_isLeviCivitaFor holds without sorry. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
New Physicslib4/Spacetime/AlongPath.lean: derivatives of functions vanishing along a path, locality of covariant derivatives along a path, globalising local vector fields, a local left inverse of a smooth path, and extension of a path's velocity to a smooth vector field. These make the chart-free geodesic definition well defined and non-vacuous. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
IsGeodesic is now the chart-free condition: at every interior parameter, the Levi-Civita derivative of any smooth extension of the velocity along itself vanishes. The five proofs that relied on the placeholder are repaired: - Minkowski straight segments are geodesics (new Geometry/PseudoRiemannian/ Flat.lean: the flat connection is Levi-Civita for a constant metric; standardMinkowski_isGeodesic_iff characterises geodesics by zero acceleration); - Lorentz transformations, isometries and cross-metric isometries map geodesics to geodesics (Koszul-formula naturality of the Levi-Civita connection). The Restriction on IsGeodesic is removed. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…stage 5) Drop the 57 formalization notes and the placeholder remark after def:causal-trip, which described IsGeodesic := True, and update the stale docstrings. Rewrite the blueprint's isometry lemmas to the Koszul-invariance route used in Lean, replacing the pullback-connection nodes by lmm:isometry-pullback-metric, -metric-derivative and -lie-bracket. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Adds the 24 new §10.4 entries (Lemma 311 not formalised), removes the geodesic-placeholder caveat, and renumbers items and pages for the 322-page build (597 declarations, 595 formalised). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
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
1 participant
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.
Added geodesics