min_entropy
plain-language theorem explainer
The J-cost function reaches its global minimum of zero precisely when its argument is one, marking a deterministic configuration with zero defect. Researchers deriving information theory from Recognition Science cite this to establish the lower bound on entropy measures. The proof is a direct one-line term application of the Jcost unit lemma.
Claim. $J(1) = 0$, where the J-cost function is given by $J(x) = (x-1)^2/(2x)$.
background
In the InformationTheoryFromRS module, Shannon entropy is identified with the average J-cost over a probability distribution. The J-cost itself is defined in the Cost module as the squared ratio $J(x) = (x-1)^2/(2x)$, which vanishes exactly at the unit argument. Entropy of an initial configuration is defined as its total defect, so zero defect yields the minimum entropy state; thermodynamic versions express entropy via partition functions and average energies, all consistent with this minimum at the ground state.
proof idea
The proof is a one-line term wrapper that applies the Jcost_unit0 lemma from the Cost module (and its duplicate in JcostCore). That lemma itself reduces by simp on the J-cost definition at argument one.
why it matters
This theorem supplies the min_H field inside the informationTheoryCert structure, which certifies that the five Shannon axioms are realized with non-negative entropy in the RS setting. It anchors the minimum-entropy case in the derivation of information theory from J-cost, aligning with the framework claim that entropy equals average defect. No open questions are addressed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.