Skip to content

feat(Geometry/Curve): add Frenet–Serret framework#38348

Open
mirajcs wants to merge 28 commits intoleanprover-community:masterfrom
mirajcs:curves
Open

feat(Geometry/Curve): add Frenet–Serret framework#38348
mirajcs wants to merge 28 commits intoleanprover-community:masterfrom
mirajcs:curves

Conversation

@mirajcs
Copy link
Copy Markdown

@mirajcs mirajcs commented Apr 21, 2026

This PR introduces a basic formalization of smooth parametrized curves in ℝ³
(EuclideanSpace ℝ (Fin 3)) together with the Frenet frame and partial proofs
of the Frenet–Serret formulas.

Main contributions:

  • Define ParametrizedDifferentiableCurve as a smooth map on an open interval.
  • Define arc length and arc-length parametrization.
  • Define geometric quantities:
    • curvature κ(t) = ‖α''(t)‖
    • tangent, normal, and binormal vector fields
    • torsion via ‖B'(t)‖
  • Introduce the FrenetFrame structure.
  • Prove key Frenet–Serret formulas:
    • T' = κ • N
    • B' = -τ • N
    • N' = -κ • T + τ • B

The implementation relies on existing analysis and inner product space
infrastructure, as well as properties of the cross product in ℝ³.
Some intermediate lemmas about orthogonality and cross-product identities
are included.

At present, some results assume nonvanishing curvature/torsion and include
auxiliary hypotheses about derivatives. These can be streamlined in future work.

This development is intended as a foundation for further formalization of
classical differential geometry (curves and surfaces).

@github-actions github-actions Bot added the new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! label Apr 21, 2026
@github-actions
Copy link
Copy Markdown

github-actions Bot commented Apr 21, 2026

Welcome new contributor!

Thank you for contributing to Mathlib! If you haven't done so already, please review our contribution guidelines, as well as the style guide and naming conventions. In particular, we kindly remind contributors that we have guidelines regarding the use of AI when making pull requests.

We use a review queue to manage reviews. If your PR does not appear there, it is probably because it is not successfully building (i.e., it doesn't have a green checkmark), has the awaiting-author tag, or another reason described in the Lifecycle of a PR. The review dashboard has a dedicated webpage which shows whether your PR is on the review queue, and (if not), why.

If you haven't already done so, please come to https://leanprover.zulipchat.com/, introduce yourself, and mention your new PR.

Thank you again for joining our community.

@github-actions
Copy link
Copy Markdown

github-actions Bot commented Apr 21, 2026 •
edited
Loading

PR summary 7f61520af4

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference
Mathlib.Geometry.Curves.Basic (new file) 2429
Mathlib.Geometry.Curves.FrenetFrame (new file) 2430

Declarations diff

+ Curvature3
+ FrenetFrame
+ FrenetSerretFrameVectorsExistence
+ ParametrizedDifferentiableCurve
+ ParametrizedDifferentiableCurve3
+ Torsion3
+ arcLength
+ arcLength3
+ binormal_cross
+ curveBinormal3
+ curveNormal3
+ curveTangent3
+ derivBinormal
+ derivTangent
+ deriv_normal
+ dot_tangent
+ frenetTrihedron
+ gsFrenetFrame
+ gsFrenetFrame_orthonormal
+ isArcLengthParametrized
+ isArcLengthParametrized3
+ orthogonality_tangent_normal
+ rawFrenetVecs
+ regularCurve
+ regularCurve3

You can run this locally as follows 
## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

No changes to technical debt.

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.sh pr_summary
  • The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
  • The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

@github-actions
Copy link
Copy Markdown

github-actions Bot commented Apr 21, 2026 •
edited
Loading

✅ PR Title Formatted Correctly

The title of this PR has been updated to match our commit style conventions.
Thank you!

@mirajcs mirajcs changed the title Add Frenet–Serret framework for parametrized curves in ℝ³ feat(Geometry/Curve): add Frenet–Serret framework Apr 21, 2026
@mirajcs
Copy link
Copy Markdown
Author

mirajcs commented Apr 22, 2026

Ready for review. All CI checks are passing.

@vihdzp
Copy link
Copy Markdown
Collaborator

vihdzp commented Apr 22, 2026

a) There seems to be a generalization of this to finitely many dimensions. Could we develop this instead, and get the case dim = 3 as a special case if need be?
b) Was any of this written by AI?

@vihdzp vihdzp added the t-differential-geometry Manifolds etc label Apr 22, 2026
@mirajcs
Copy link
Copy Markdown
Author

mirajcs commented Apr 22, 2026

@vihdzp Thanks for the feedback!

a) That’s a good point. I focused on the 3-dimensional case to keep the development concrete, but I agree that a formulation in arbitrary finite dimensions would be more natural. I believe this should go through an alternating multilinear construction (or equivalently via a Hodge-star-type operator), so that the 3D cross product appears as a special case. I’ll look into whether the current development can be refactored along these lines and whether this generalization fits well with existing mathlib abstractions.

b) I did not generate the code with AI. I have used AI tools occasionally to explore tactics or get ideas, but all code has been written and verified by me.

@vihdzp
Copy link
Copy Markdown
Collaborator

vihdzp commented Apr 22, 2026

The Hodge star is a longstanding TODO... that by itself would be a good project.

@sgouezel sgouezel removed their assignment Apr 26, 2026
wwylele
wwylele reviewed Apr 26, 2026
View reviewed changes
Comment thread .github/workflows/build_template.yml Outdated
@ocfnash ocfnash added the awaiting-author A reviewer has asked the author a question or requested changes. label Apr 28, 2026
bryangingechen
bryangingechen reviewed Apr 29, 2026
View reviewed changes
Comment thread Mathlib/Geometry/Curves/Basic.lean Outdated
**Reference:** https://en.wikipedia.org/wiki/Frenet%E2%80%93Serret_formulas#Formulas_in_n_dimensions -/
structure ParametrizedDifferentiableCurve where
n : ℕ
h3 : 3 ≤ n
Copy link
Copy Markdown
Contributor

@bryangingechen bryangingechen Apr 29, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I don't think this restriction should be in the definition. Certainly we want to be able to talk about parametrized differentiable curves when n=2 (and possibly even n=1) and I think theorems that only apply with specific conditions on n should be stated with those as hypotheses.

Copy link
Copy Markdown
Author

@mirajcs mirajcs Apr 29, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I agree with you and will remove the condition. Thank you

@bryangingechen
Copy link
Copy Markdown
Contributor

bryangingechen commented Apr 29, 2026

I suggest splitting this PR up a bit. Certainly the definition of parametrized curves and very basic API for working with curves should be a separate PR from Frenet-Serret material.

@bryangingechen
Copy link
Copy Markdown
Contributor

bryangingechen commented Apr 29, 2026

Ah, I just realized that there's already #36731 which covers the plane case. Perhaps you can take a look at the work there and coordinate with the author. I recommend also posting about your plans on Zulip for more feedback.

@mirajcs
Copy link
Copy Markdown
Author

mirajcs commented Apr 29, 2026

@bryangingechen Thank you for pointing that out. I separated the file and the work in #36731 for the 2D case, so there will be no conflict with mine.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@bryangingechen bryangingechen bryangingechen left review comments

@ocfnash ocfnash ocfnash left review comments

+1 more reviewer

@wwylele wwylele wwylele left review comments

Reviewers whose approvals may not affect merge requirements

Assignees

@ocfnash ocfnash

Labels

awaiting-author A reviewer has asked the author a question or requested changes. new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-differential-geometry Manifolds etc

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

6 participants

@mirajcs @vihdzp @bryangingechen @wwylele @ocfnash @sgouezel