stateProbability
plain-language theorem explainer
The definition computes the probability of state i as its J-cost Boltzmann weight divided by the partition function over all states. Researchers deriving thermodynamic distributions from Recognition Science J-cost minimization would cite this when linking to Fermi-Dirac or Bose-Einstein statistics via 8-tick phases. It is implemented as a direct division of the per-state weight by the normalizing sum.
Claim. For positive ratios $r_1, ..., r_n > 0$ and temperature $T > 0$, the probability of state $i$ is $P_i = w(r_i, T) / Z(r, T)$, where $w$ denotes the J-cost Boltzmann weight $w(r, T) = jcostBoltzmann(r, T)$ and $Z$ is the partition function summing the weights over all states.
background
The J-Cost to Thermodynamics Bridge module connects Recognition Science's J-cost functional to thermodynamic distributions. The J-cost is given by $J(x) = ½(x + 1/x) - 1$ for ratio $x$, with the Boltzmann weight emerging as the distribution minimizing average J-cost subject to constraints; temperature acts as the Lagrange multiplier. Upstream results include the fundamental time quantum tick $τ_0 = 1$ from Constants, the 8-tick phase function $kπ/4$ for $k = 0..7$ from EightTick, and spin-statistics definitions from QFT.SpinStatistics that tie odd phases to fermions.
proof idea
This definition is a one-line wrapper that applies jcostBoltzmann to the ratio for state i and divides the result by the partitionFunction over all states.
why it matters
This definition supplies the normalized probabilities required for the module's main theorems on Boltzmann, Fermi-Dirac, and Bose-Einstein distributions arising from J-cost minimization. It supports the connection from 8-tick phases to spin-statistics, where odd phases produce antisymmetric weights and the +1 in the Fermi-Dirac denominator. The placement advances the framework's derivation of thermodynamics from the Recognition Composition Law and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.