ManyBodyLedger
plain-language theorem explainer
The many-body ledger records a positive integer M of subsystems together with a map from K states to positive real ratios. Derivations of entropy from J-cost counting cite this record to formalize macrostate constraints. It is introduced by a direct structure definition that embeds the positivity requirements on M and the ratios.
Claim. A many-body ledger for a fixed number of states $K$ consists of a positive integer $M$ (the number of subsystems) and a function $r$ from the $K$ states to the positive reals such that each $r_i > 0$.
background
The module establishes J-cost as the ancestor of Shannon entropy by showing that the Gibbs distribution arises from constrained maximization on many-body systems. J-cost is the functional $J(x) = (x + x^{-1})/2 - 1$ taken from the Cost module; the Recognition Composition Law supplies the algebraic identity that makes this functional self-dual under inversion. The ledger supplies the concrete data type on which the counting argument (multinomial microstate multiplicity) and the average-cost constraint are imposed. Upstream constants include the dimensionless bridge ratio $K = phi^{1/2}$ and the active-edge count $A = 1$ per fundamental tick, both used to anchor the phi-ladder scaling of energies.
proof idea
The declaration is a pure record definition. It introduces four fields: the subsystem count M, the proof that M is positive, the ratio map from Fin K to reals, and the proof that every ratio is positive. No lemmas or tactics are invoked; the structure simply packages the data and the embedded positivity hypotheses required by the downstream average-cost and free-energy statements.
why it matters
This ledger is the data substrate for the three immediate downstream results: the definition of average J-cost, the theorem that the entropy maximizer is the Gibbs measure, and the theorem that temperature is the Lagrange multiplier fixed by the cost constraint. It realizes the module's core counting argument in which log Omega approximates M times Shannon entropy under fixed average J-cost. In the broader framework it supplies the many-body setting in which the Recognition Composition Law forces the Gibbs form and in which J-cost dominates squared-log information content, confirming that entropy is the quadratic shadow of the ancestor functional.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.