Add the core LocalJet coordinate object

[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 as Theorem 5.2 in Cortés--Haupt, Chapter 5.

The overall local stack is intended to proceed through:

• multi-indices and iterated derivatives,
• admissible compactly supported variations,
• local jets,
• total derivatives,
• local lagrangians and the action functional,
• the local Euler--Lagrange operator,
• and finally the first-variation criterion.

The Zulip discussion for this development is here:

• https://leanprover.zulipchat.com/#narrow/channel/479953-PhysLib/topic/ClassicalFieldTheory/

The previous PRs, #1021, #1027, and #1028, introduced the reusable MultiIndex API and the basic iterated-derivative layer on Space d. This PR begins the local jet layer by introducing the core jet object itself.

What This PR Adds

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

Concretely, it provides:

• DerivativeIndex d k for multi-indices of order at most k,
• JetCoordinates d m k,
• zeroIndex,
• the structure LocalJet d m k,
• and the first basic API around it (ext, coord, and the zero-index compatibility lemma).

Why This Is Needed

Later PRs will use this object to package local k-jet data for fields Space d → Space m.

This is the local coordinate object on which the subsequent constructions are built:

• explicit jet-coordinate conversions,
• jet evaluation jetAt,
• total derivatives of jet-dependent functions,
• and then local lagrangians and the Euler--Lagrange operator.

So this PR isolates the basic jet object before adding the more elaborate coordinate and evaluation API.

Scope Of This PR

This PR is intentionally limited to the core jet object.

It does not yet add:

• fiber-direction data on jets,
• explicit coordinate conversions,
• jet evaluation of a field at a point,
• or smoothness/support lemmas for jets.

Those appear in follow-up PRs, so that the basic local jet object can be reviewed first on its own.

Build

Locally checked with:

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

[jstoobysmith]

I'm a bit confused about what this definition is meant to represent. More specifically how this is a local jet. To me it looks it represents a point in the jet bundle when the base is Space d and the fibers are Space M (should probably generalize to U).

[jstoobysmith]

Would make own file in Space.Derivatives.

[jstoobysmith]

Hey, just wanted to check in about this PR. No rush, just making sure things don't slip through the net.

[juan-fernandez-gotherlabs]

It has been a busy week, and I want to look carefully at exactly how to handle the bundle setup. I’m still working toward the same goal. Thanks for the ping!