Formal: general finite maximum entropy and the constrained Gibbs maximiser (FORM-S2)

[docxology]

Refs #85 (FORM-S2). Not closing: fep-030's disposition and the 030↔031 relation upgrade wait for independent review.

fep-030 proved only the Bernoulli and uniform cases. New:

• FEP.FiniteInformation:
  • entropy_le_log_card (H(p) ≤ log n for every finite law) and entropy_eq_log_card_iff (equality iff uniform), via crossEntropy_uniform and finiteKL ≥ 0.
  • entropy_lt_log_card_of_ne_uniform.
  • Witness boolBiased_entropy_lt_log_two.
• FEP.VariationalDuality:
  • energyGibbsLaw E β.
  • The decomposition entropy q = β⟨E⟩_q + log Z − KL(q‖p_β).
  • energyGibbs_maxEntropy: under the mean-energy constraint the Gibbs law maximises entropy, with equality iff q = p_β. Plus the strict version energyGibbs_entropy_lt_of_ne.
  • The zero-energy reduction to uniform, and a strict witness.
  • Existence of β for a given mean energy is out of scope.

Evidence:

• lake --wfail build FepSketches passes (8,997 jobs, zero warnings), and #print axioms on all 13 declarations shows only the standard three.
• Projections were regenerated by their owners, and every --check passes.
• Pins: finite_information 25 → 31, variational_duality 56 → 63, lexical declarations 1,946 → 1,959.
• check_render_log --verify-receipt, check_orphan_compiles, the formal and methods tests (157) and ruff pass.

Witness for a later 030↔031 relation review: FEP.VariationalDuality.energyGibbs_maxEntropy.