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

[mirajcs]

---

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]

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]

PR summary 977f84bd6e

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)	2426

---

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

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

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

The doc-module for scripts/pr_summary/declarations_diff.sh 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).

---

⚠️ Workflow documentation reminder

This PR modifies files under .github/workflows/.
Please update docs/workflows.md if the workflow inventory, triggers, or behavior changed.

Modified workflow files:

• .github/workflows/build_template.yml

[github-actions]

✅ PR Title Formatted Correctly

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

[mirajcs]

Ready for review. All CI checks are passing.

[vihdzp]

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?

[mirajcs]

@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]

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

[wwylele]

Please don't make changes to CI in an unrelated PR.