Formal: generalized-coordinate jets are actual derivatives (FORM-S8)

[docxology]

Refs #91 (FORM-S8). Not closing: fep-089/090 dispositions change only after independent review.

In predictive_coding.lean, FiniteJet had a combinatorial shift with no link to derivatives. New in FEP.PredictiveCoding:

• functionJet order f t: coordinate k is iteratedDeriv k f t for k ≤ order.
• shift_one_functionJet: below the truncation order, shifting the jet of f equals the jet of deriv f. The generalized-coordinate D operator is differentiation.
• shift_functionJet: the m-fold version, which gives the jet of iteratedDeriv m f.
• shift_one_functionJet_top: the truncation boundary. At the top coordinate the shift gives 0, while the derivative's jet keeps iteratedDeriv (order+1) f t.
• exp_jet_shift_witness: for Real.exp, every retained coordinate is nonzero and the shift matches deriv.

Evidence:

• Narrow Mathlib imports added: IteratedDeriv.Defs and ExpDeriv.
• lake --wfail build FepSketches passes, and every axiom set is the standard three.
• Projections were regenerated by their owners, and every --check passes.
• Pins: predictive_coding 30 → 37, lexical declarations 1,946 → 1,953.
• check_render_log --verify-receipt, check_orphan_compiles, the formal and methods tests (157) and ruff pass.