Repository navigation
[FORM-S2] General finite maximum entropy and the constrained Gibbs maximiser (fep-030) #85
Description
Activity
Status update (2026-10-09). Delivered in #158 (via integration #164), merged to
main:entropy_le_log_cardandentropy_eq_log_card_iff(H ≤ log n, with equality iff uniform), the Gibbs maximum-entropy theoremenergyGibbs_maxEntropywith its strict form, the zero-energy reduction, and strict Boolean witnesses. Existence of β for a given mean energy remains out of scope. Suggested qualified witness for a later 030↔031 relation review:FEP.VariationalDuality.energyGibbs_maxEntropy.Evidence:
lake --wfail build FepSketchespasses at the pin (Lean v4.34.1, Mathlibd13f23b7), every new declaration depends only onpropext/Classical.choice/Quot.sound, and all generator--checks plus hosted CI pass.Remaining for closure: independent semantic review of the delivered statements against the topic's theorem proxy. Per this issue's claim boundary, no disposition in
config/theorem_maturity.yamlwas changed, and none may change without that review.Delivered on
main:FEP.FiniteInformation.entropy_le_log_card(unconditionalH ≤ log n),FEP.VariationalDuality.energyGibbs_maxEntropy,energyGibbs_entropy_lt_of_neandboolBiased_entropy_lt_zeroEnergyGibbs. Still open: thefep-030 → fep-031edge inconfig/formalism_relations.yamlremainsconceptual; review and upgrade it with witnessFEP.VariationalDuality.energyGibbs_maxEntropy, or record its blocker. TheTODO.mdrow is narrowed in #171 to the remaining clause.
Scope ID:
FORM-S2. Size: Minor. Scoped on 2026-10-08 in SCOPE-2026-10-08.md; acceptance remains open.Owner: core thermodynamics/information bodies and the variational-duality foundation.
Dependencies: FORM-D3
Work
fep-030 'Maximum Entropy Principle' proves only the Bernoulli and uniform cases; coverage marks general MaxEnt out of scope. Prove
H(p) ≤ log nwith equality iffpis uniform, and that the Gibbs law uniquely maximisesHunder a mean-energy constraint, both fromfiniteKL ≥ 0and the fep-058/059 Gibbs certificate. Existence of β for a given mean energy may be staged separately.Acceptance
Unconditional
H ≤ log n, a strict witness off the Gibbs law, and a reviewed 030↔031 relation upgraded from conceptual with a qualified witness.Failure controls and claim boundary
No disposition promotion from compilation, import or numerical agreement; the maturity record changes only after independent semantic review. No duplicate topics and no automatic sealed-roster expansion.
Canonical references
Closure requires actual exact-source commands, results and retained receipts, with independent review where specified. Remove its open TODO row only after acceptance; retain delivery facts in changelog/history. Size describes implementation scope, not a semantic-version promise.