Add MultiIndex API for local field-theory foundations

[juanjfndz]

Summary

This PR is the first 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/

This first PR only introduces the reusable MultiIndex API needed later to index jet coordinates and iterated derivatives.

What This PR Adds

This PR adds PhysLean/Mathematics/DataStructures/MultiIndex.lean, with a small API for finitely supported multi-indices on Fin n.

Concretely, it provides:

• the type MultiIndex n := Fin n → ℕ,
• the order |I| = Σ_i I_i,
• the zero multi-index,
• increment and add operations,
• basic lemmas about order and coordinates.

Why This Is Needed

Later PRs will use multi-indices to write the local jet coordinates

u^a_I

and iterated derivatives

∂^I = ∂_1^{I_1} ... ∂_n^{I_n}.

They also appear in the local Euler--Lagrange expression

E_a(L) = Σ_{|I| ≤ k} (-D)^I (∂L / ∂u^a_I).

So even though this first PR is small and purely reusable, it is the indexing layer that the rest of the local field-theory stack will build on.

Design Notes

I have placed this in Mathematics.DataStructures rather than under ClassicalFieldTheory, since it is meant to be reusable outside the field-theory namespace as well. That follows the earlier Zulip suggestion to keep the reusable pieces out of the domain-specific layer where possible.

Build

Locally checked with:

• python3 scripts/lint-style.py PhysLean/Mathematics/DataStructures/MultiIndex.lean
• lake build PhysLean.Mathematics.DataStructures.MultiIndex
• lake build PhysLean

[jstoobysmith]

I personally would make this an structure with a single field corresponding to Fin n -> Fin d where d is the dimension. Using a structure initially will make things more difficult, as you have to define instances on it for e.g. Add, but, it gives you much more flexibility. Everytime I haven't used a structure initially I have gone on to regret it.

[juan-fernandez-gotherlabs]

Thanks — both comments made sense to me.

I have now reworked this locally so that:

• MultiIndex is a structure (with underlying map Fin n → ℕ) rather than an abbrev,
• the file lives under PhysLean/SpaceAndTime/Space/Derivatives/MultiIndex.lean,
• and the import-order issue from CI is also fixed.

I will push that update to the PR branch next.

[jstoobysmith]

We renamed ./PhysLean to ./Physlib which is why there is a merge conflict on this PR now. If you could fix it, that would be great, but if you need help feel free to let me know.

[juanjfndz]

I have now updated the PR branch to the current Physlib tree as well.

Concretely:

• the MultiIndex API remains under Space.Derivatives,
• the branch is now aligned with the PhysLean -> Physlib rename,
• and the local checks now pass again (lint-style.py, lake build Physlib.SpaceAndTime.Space.Derivatives.MultiIndex, and lake exe check_file_imports).

So this one should be back in a sane state now.

[jstoobysmith]

mentioned above, but could we replace n here with d since it is meant to be the dimension of Space.

[juan-fernandez-gotherlabs]

Good point — I have now changed this to d in the MultiIndex API so that it matches the ambient space-dimension convention more closely.

[jstoobysmith]

Great! Many thanks! This now looks good to me. I've approved this PR, but you might have to take it out of "draft" mode.

[jstoobysmith]

Thanks - I will merge shortly :).

[juanjfndz]

Many thanks!

I'll move on to the next one tomorrow:

• PR 2: Iterated derivatives

[jstoobysmith]

Great! Looking forward to it!