Formal: Helmholtz free energy as the minimum of the variational functional (FORM-S3)

[docxology]

Refs #86 (FORM-S3). Not closing: fep-013's disposition and the 013↔002 relation wait for independent review.

fep-013 proved dF/dT = −S on abstract U(T), S(T) with no link to variational free energy. New section at the end of variational_duality.lean (names are helmholtz*, distinct from #158's energyGibbsLaw):

• Decomposition helmholtz_decomposition: ⟨E⟩_q − T·H(q) = F(T) + T·KL(q‖p_T), with F = −T log Z and Gibbs law p_T ∝ exp(−E/T).
• Variational characterisation:
  • helmholtzFreeEnergy_le: F(T) = min_q (⟨E⟩_q − T·H(q)).
  • helmholtzFreeEnergy_eq_iff: the minimiser is unique, the Gibbs law.
  • helmholtzFreeEnergy_lt: strict inequality off the Gibbs law.
• Thermodynamic derivative hasDerivAt_helmholtzFreeEnergy: dF/dT = −H(p_T). This is fep-013's relation, now derived for the Gibbs family rather than assumed on abstract functions.
• Witness helmholtz_bool_uniform_gt: on the two-level system, the uniform law has strictly larger variational free energy than F(T) at every T > 0.

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: variational_duality 56 → 67, lexical 1,953 → 1,964. Expect a mechanical conflict with Formal: general finite maximum entropy and the constrained Gibbs maximiser (FORM-S2) #158, which appends to the same file.
• 181 tests and ruff pass.