Add coordinate-level jet points

[juanjfndz]

Summary

This PR is the next step in a planned local Classical Field Theory development for PhysLib, aimed
at a formalization of the local Euler--Lagrange criterion appearing in Cortes--Haupt, Chapter 5.

The previous PRs introduced:

• reusable multi-index infrastructure,
• iterated spatial derivatives,
• admissible compactly supported variations,
• and bounded derivative indices.

This PR begins the jet-coordinate layer by introducing the core coordinate-level jet point object.

What This PR Adds

This PR adds Physlib/ClassicalFieldTheory/Local/JetPoint.lean, together with its import in
Physlib.lean.

Concretely, it provides:

• JetCoordinates d m k,
• JetPoint d m k,
• coordinate and value projections,
• basic coordinate extensionality and base-coordinate conversions,
• jetCoordinatesAt,
• and jetAt.

Interpretation

The object introduced here is the coordinate-level point of the locally trivialized k-jet bundle
for fields Space d -> EuclideanSpace ℝ (Fin m).

It formalizes only the local coordinate model
Jet^k(Omega, R^m) ~= Omega x V; it does not attempt to define global jet bundles.

The zero-th order field value is not stored separately in JetPoint; it is recovered as the zero
derivative coordinate.

The jet-coordinate data is kept in scalar component form,
DerivativeIndex d k -> Fin m -> ℝ, because the local Euler--Lagrange formulas are indexed by
both the derivative index I and the field component a.

Reference

The reference for this local development is:

• Vicente Cortes and Alexander S. Haupt, Lecture Notes on Mathematical Methods of Classical
  Physics, arXiv:1612.03100v2, Chapter 5.

arXiv link: https://arxiv.org/abs/1612.03100

Scope Of This PR

This PR is intentionally limited to the core jet-point object and the basic jetAt evaluation map.

It does not yet add:

• jet fiber-direction data,
• affine-line operations in the jet fiber,
• smoothness or support lemmas for jet-coordinate maps,
• total derivatives,
• or Lagrangians.

Those pieces are intended for follow-up PRs so that the core coordinate object can be reviewed on
its own.

Build

Locally checked with:

• python3 scripts/lint-style.py Physlib/ClassicalFieldTheory/Local/JetPoint.lean
• lake exe runPhyslibLinters Physlib/ClassicalFieldTheory/Local/JetPoint.lean
• lake build Physlib.ClassicalFieldTheory.Local.JetPoint
• lake build Physlib
• lake exe check_file_imports

[jstoobysmith]

Would change to to be for fields Space d -> EuclideanSpace ℝ (Fin n) or similar

[jstoobysmith]

Would make this a map to EuclideanSpace

[jstoobysmith]

Likewise with the above.

[jstoobysmith]

If this is AI generated, please can you make sure the reference is correct.

[juanjfndz]

Thanks, I have pushed a correction addressing these points.

The field target in this PR is now Space d → EuclideanSpace ℝ (Fin m) rather than
Space d → Space m. This has been updated in the module overview, the JetPoint docstring,
JetPoint.value, jetCoordinatesAt, jetAt, and the zero-order value lemmas.

I kept JetCoordinates d m k in scalar component form,
DerivativeIndex d k → Fin m → ℝ, since this file is explicitly the local coordinate model with
coordinates u^a_I, and the later Euler--Lagrange coordinate formulas are indexed componentwise
by both I and a. I added a docstring clarification to make that interpretation explicit.

I also checked the reference. The source is Vicente Cortes and Alexander S. Haupt,
Lecture Notes on Mathematical Methods of Classical Physics, arXiv:1612.03100v2:
https://arxiv.org/abs/1612.03100. This is the paper/notes we are using as the reference for this
local development.

The scope of the PR is unchanged: it still only contains the core JetPoint object and jetAt;
fiber directions, affine line maps, regularity/support lemmas, total derivatives, Lagrangians, and
Euler--Lagrange material remain deferred to later PRs.

[jstoobysmith]

I've asked @or4nge19 to also have a look at this PR - since he knows a bit about this area.

[or4nge19]

I think it would be nice to know what is the plan (if any) for this set of PRs, so that they could be placed where they best fit, within the longer jet/variational ideal pipeline in physlib (currently in advanced stage of WIP).

Anyhow, the object here (and in the previous PRs) seems not yet a jet bundle or an intrinsic finite jet (mathlib's target, see here and here and here for early partial implementations) but the coordinate table of a flat trivial local model, obtained by applying the existing coordinate iterated-derivative operator. That is useful layer, for later Euler-Lagrange coordinate formulas among other things, as long as we do not treat JetPoint d m k as the public ontology of jets and have the idea, perhaps a TODO, to eventually derive or discharge most of the definitions (and lemmas/theorems) here from a 'deeper' (Fréchet/Taylor/contact) substrate API.

In particular, I would suggest adding to the module/docstring something along these lines:

• JetPoint is a coordinate readout for the trivial bundle Space d × EuclideanSpace ℝ (Fin m).
• Equality of these objects is equality of chosen coordinate data, not a germ/contact equivalence.
• Coordinate Euler-Lagrange formulas should eventually be derived from Fréchet/Taylor/contact data, not used as the foundational definition.

Also, since the target is now EuclideanSpace, you may want to consider adding coordVector so higher-order coordinates have the same bundled readout as value. Something like:

def JetPoint.coordVector (J : JetPoint d m k) (I : DerivativeIndex d k) :
    EuclideanSpace ℝ (Fin m)

[or4nge19]

Re-iterating on the message I'd add two comments/future tasks along these lines, or as TODOs

• Equality of these objects is equality of chosen coordinate data, not a germ/contact equivalence.
• Coordinate Euler-Lagrange formulas should eventually be derived from Fréchet/Taylor/contact data, not used as the foundational definition.

[juanjfndz]

Thanks @jstoobysmith and @or4nge19 for the comments and context.

For the longer plan, I had outlined the local CFT stack in this Physlib Zulip thread:
https://leanprover.zulipchat.com/#narrow/channel/479953-Physlib/topic/ClassicalFieldTheory/with/582986380

I am keeping that roadmap message updated as the project adapts, and I am also adjusting the
planned PR labels so that they do not suggest that this stack is defining the foundational ontology
of jets.

The reference I am using for this local development is Cortes--Haupt, Lecture Notes on
Mathematical Methods of Classical Physics, arXiv:1612.03100v2:
https://arxiv.org/abs/1612.03100

More specifically, the current stack is aimed at Chapter 5, Section 5.1:

• bounded derivative indices correspond to the multi-indices I with |I| ≤ k used in the local
  coordinates u^a_I;
• this PR is the coordinate readout of the local trivial model Jet^k(Ω, R^m) ≃ Ω × V;
• the next coordinate fiber/affine-line layer corresponds to the j^k(f + εh) calculation in the
  proof of Theorem 5.2;
• the regularity/support layer supplies the smoothness and compact-support infrastructure used in
  that variational calculation;
• total derivatives correspond to the operators D_i, D_I, and (-D)^I;
• the later Lagrangian/action and Euler--Lagrange layers correspond to equation (5.1), equations
  (5.2)/(5.3), and the proof of Theorem 5.2.

So I will update the module documentation/TODOs to make explicit that this is a coordinate readout
layer for the flat/trivial local model, not a jet bundle or intrinsic finite-jet construction. In
particular, equality here is equality of chosen coordinate data, not germ/contact equivalence, and
the coordinate Euler--Lagrange formulas should eventually be related to or derived from a deeper
Fréchet/Taylor/contact API.

I can also add the bundled coordVector projection you suggested.

If there is a better location or naming convention for this coordinate-readout layer within the
longer jet/variational pipeline, I am happy to adjust the namespace/file organization before
continuing with the follow-up PRs.