Formal: precision as inference and predictive-coding energy as a negative log joint (FORM-S9)

[docxology]

Refs #92 (FORM-S9). Not closing: fep-086/087/091 dispositions change only after independent review.

New section at the end of predictive_coding.lean. Narrow imports added: Convex.SpecificFunctions.Basic, Log.Deriv, Gaussian.Real.

(b) Precision as inference. Define F(π) = π·ε²/2 − log π / 2.

• precisionFreeEnergy_sub_opt gives the gap F(π) − F(1/ε²) = (ε²π − 1 − log(ε²π))/2.
• precisionFreeEnergy_min and precisionFreeEnergy_eq_iff: the unique minimiser is π* = 1/ε².
• precisionFreeEnergy_hasDerivAt gives the derivative.
• precisionFreeEnergy_strictConvexOn gives strict convexity on (0, ∞).
• precisionFreeEnergy_zero_error_unbounded: at ε = 0 there is no minimiser, since F is unbounded below.

(a) Linear-Gaussian chain.

• neg_log_gaussianPDFReal gives −log of Mathlib's Gaussian density as precision-weighted squared error minus half the log precision, plus log(2π)/2.
• gaussianChainEnergy_eq_neg_log_prod: for any finite chain, the predictive-coding energy is exactly −log ∏ N(xₗ; μₗ, vₗ) up to the constant card/2 · log(2π).
• gaussianChain_twoLevel is the two-level specialisation.

(c) twoLevel_chain_energy_witness extends the existing two-level witness: precisions 2 and 4 with errors 3 and 1 give 11 − (3/2)·log 2.

Evidence:

• lake --wfail build FepSketches passes, and every axiom set is the standard three.
• Projections were regenerated by their owners, and every --check passes, as do check_render_log --verify-receipt, theorem_ref_audit and check_orphan_compiles.
• Pins: predictive_coding 30 → 40, lexical 1,953 → 1,963. These conflict mechanically with Formal: generalized-coordinate jets are actual derivatives (FORM-S8) #157, which also edits this module; I'll rebase after it lands.
• Formal and methods tests and ruff pass.