refactor(Vorspiel): rename clashing Matrix.map/forall_iff/exists_iff to vec* (Mathlib co-import)

[A-M-Berns]

This PR was prepared with the help of Claude Fable 5 to fix a naming clash between Mathlib and FFL that I encountered when working on my Formalized Agent Foundations project that uses both as a dependency. This rename would be useful for any project that requires both Mathlib and FFL to reduce naming conflicts.

--

What

Renames the three Foundation.Vorspiel.Matrix declarations that shadow existing Mathlib Matrix.* names, so Foundation can be imported alongside Mathlib's matrix/analysis theory:

Foundation decl	collides with (Mathlib)	renamed to
Matrix.map (a vector map (Fin k → α) → (Fin k → β))	Matrix.map (…Matrix.InvariantBasisNumber materializes Matrix.map.eq_1)	Matrix.vecMap
Matrix.forall_iff	Matrix.forall_iff (Mathlib.Data.Matrix.Reflection)	Matrix.vecForall_iff
Matrix.exists_iff	Matrix.exists_iff (Mathlib.Data.Matrix.Reflection)	Matrix.vecExists_iff

The ⨟ notation and all lemmas keep their behavior; the 12 call sites of forall_iff/exists_iff in BinderNotation.lean and Semantics.lean are updated.

Why

Each of these lives in the Matrix namespace and shares a name with a distinct Mathlib Matrix declaration. Importing Foundation together with the relevant Mathlib module fails at import time, e.g.:

import Foundation.Vorspiel.Matrix failed, environment already contains
'Matrix.map.eq_1' from Mathlib.LinearAlgebra.Matrix.InvariantBasisNumber

import ... failed, environment already contains 'Matrix.forall_iff'
from Mathlib.Data.Matrix.Reflection

Because Vorspiel.Matrix sits in Foundation's prelude, every Foundation module inherits the clash. It surfaces when co-importing Foundation with matrix-heavy Mathlib analysis — Mathlib.MeasureTheory.Integral.Bochner, and anything pulling EuclideanSpace/InnerProductSpace.PiL2 (which transitively imports Matrix.Reflection).

Scope / safety

• These three are the complete set of Foundation-vs-Mathlib Matrix-namespace name collisions: I intersected every Matrix.* decl in Vorspiel/Matrix.lean against Mathlib and confirmed the rest (vecConsLast, toList, foldr, foldl, appendr, …) have no Mathlib Matrix counterpart.
• Downstream, a project that co-imports Foundation with Bochner integration and with a from-scratch Brouwer development (over EuclideanSpace ℝ (Fin d)) now builds green with these renames; before them the roll-up module hit exactly the two clashes above in sequence.
• I have not run lake build Foundation against master's current toolchain locally; these are pure renames of leaf decls with all call sites updated, so they should be toolchain-agnostic — happy to let CI confirm.

Note on lemma names

I kept the map_* lemma family (map_cons, map_app, map_map_comp', …) and the section map unchanged, to keep the diff to what's needed to clear the clash. Glad to rename those to vecMap_* for consistency with the foldr_*/foldl_* convention if you'd prefer.

[SnO2WMaN]

Thanks for the PR!
Regarding this issue, I personally think that the naming in Mathlib is problematic to begin with.
I asked about it on Zulip but haven't respond yet: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Namespace.20confict.20of.20.60Matrix.60

[SnO2WMaN]

For the lemmas involving Matrix.vecMap, I think renaming them to vecMap_* would be fine. The same goes for the other definitions.

[SnO2WMaN]

Verified: a scratch module importing Mathlib.MeasureTheory.Integral.Bochner.Basic, Mathlib.Analysis.InnerProductSpace.PiL2, and Foundation.Vorspiel.Matrix together builds cleanly with no name clashes (lake build succeeded, 2494/2494 jobs). This confirms the vecMap/vecForall_iff/vecExists_iff renames resolve the collisions this PR targets.

[SnO2WMaN]

@A-M-Berns P.S.: I took a look at https://github.com/A-M-Berns/Formalized-Agent-Foundations and it looks like you're using something around the fixed-point theorem for modal logic GL.
Since we're planning to remove modal logic from Foundation, I think https://github.com/FormalizedFormalLogic/ProvabilityLogic would be useful for your purposes.
That's where we're putting the fixpoint theorem and related material.