Merge main into bounding (resolve conflicts with #484)

[thefundamentaltheor3m]

#460 became un-mergeable after #484 (A, B and the g inequality statements) landed on main. This merges main into bounding and resolves the three conflicts:

• a/Eigenfunction.lean, b/Eigenfunction.lean: Define A, B and add inequality statements of them and g #484 only switched eig_a / eig_b to 𝓕 notation in the old SchwartzMap setting. This branch had already rewritten both proofs for RadialSchwartzMap, so the branch's versions are kept.
• g/Basic.lean: fourier_g_zero keeps this branch's version, which goes through fourier_g_apply. The duplicated open scoped FourierTransform is dropped. Define A, B and add inequality statements of them and g #484's new A, B, A_eq, B_eq, g_eq_integral_A, g_Fourier_eq_integral_B, A_neg, B_pos, g_nonpos and g_Fourier_nonneg are merged in unchanged. They use g x / 𝓕 g x, which work for the RadialSchwartzMap g through its coercion to functions and its Fourier transform instance.

Phi.lean, Psi.lean and the blueprint merge cleanly.

I've started the build workflow by hand on the head branch to validate the merge before it lands.

🤖 Generated with Claude Code

https://claude.ai/code/session_01UXLVscFdDj42KSSxpVWBHP

---

Generated by Claude Code