ledgerProperties
plain-language theorem explainer
The declaration enumerates four structural properties that the Recognition Science ledger contributes to the partition function: countable microstates, J-cost as energy, symmetry-induced degeneracy, and balance-enforced conservation. A researcher deriving statistical mechanics from the ledger sum would cite these properties to justify mapping ledger entries onto thermodynamic states. The definition is a direct list construction with no lemmas or computation.
Claim. The ledger supplies four properties for the partition function: discrete microstates from countable entries, energy assignment via the J-cost function $J(x)=(x+x^{-1})/2-1$, degeneracy from ledger symmetries, and conservation from total balance.
background
Recognition Science derives the partition function as a sum over ledger configurations weighted by J-cost. The J-cost function is the canonical map $J(x)=(x+x^{-1})/2-1$ that assigns an energy scale to each recognition event or ledger entry. Upstream lemmas establish that the cost of any recognition event equals its J-cost and that ledger factorization structures the underlying multiplicative group.
proof idea
The definition is a direct enumeration of four descriptive strings. It draws the energy role from the J_cost definition and the cost functions supplied by ObserverForcing and MultiplicativeRecognizerL4.
why it matters
The definition supplies the ledger-to-microstate correspondence required by the THERMO-002 derivation of the partition function from ledger sum. It connects the J-cost energy scale to the discrete states needed for the sum that yields free energy, average energy, and entropy. In the broader framework it bridges the T5 J-uniqueness result to thermodynamic observables while remaining within the eight-tick octave and D=3 setting.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.