Macrostate
plain-language theorem explainer
Macrostate encodes occupation numbers across K states for M recognition subsystems in a many-body ledger. Researchers deriving the emergence of Gibbs weights and Shannon entropy from J-cost constraints would cite this structure when counting microstates or applying Lagrange multipliers. The definition is a direct record type whose validity predicate simply enforces total occupation conservation.
Claim. A macrostate for $K$ states consists of an occupation map $n: [K] → ℕ$. It is valid for total particle number $M$ when $∑_{i=1}^K n_i = M$. The associated empirical distribution is the normalized vector $p_i = n_i/M$ for $M>0$.
background
The JCostEntropyAncestor module treats macrostates as the coarse-grained description of M independent recognition subsystems, each choosing one of K states whose J-costs are given by the functional $J(x) = ½(x + x^{-1}) − 1$. This J-cost is the fundamental energy functional imported from Cost.lean; the module shows that Shannon entropy $H(p) = −∑ p_i log p_i$ arises as the quadratic approximation to average J-cost under a fixed-energy constraint. The local theoretical setting is the backward derivation that the most probable distribution maximizes entropy subject to the cost constraint, thereby forcing the Gibbs form rather than postulating it. Upstream results supply the dimensionless bridge ratio $K = ϕ^{1/2}$ and the discrete phi-tier structure for physical densities.
proof idea
The structure is introduced by direct definition. The validity predicate is the equality of the sum of the occupation vector to M. The empirical map is the normalization of occupations by M when M is positive. No lemmas are applied; it is a foundational data type for the subsequent entropy derivations in the module.
why it matters
This structure supplies the counting object needed to prove that the Gibbs distribution is forced by constrained optimization on many-body ledgers. It connects to the Recognition Composition Law and the T5–T8 forcing chain by providing the discrete state space on which J-cost acts. The module as a whole closes the loop from J-cost to entropy, showing entropy as the second-order shadow of J-cost. It supports the claim that the recognition temperature T_R is derived rather than free.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.