gibbsPD
plain-language theorem explainer
Packages the Gibbs measure into a ProbabilityDistribution structure to serve as the equilibrium reference for J-descent dynamics. Researchers deriving the second law from Recognition Science first principles cite this when invoking the variational principle or free-energy monotonicity. The definition is a direct wrapper that supplies the nonneg and sum_one fields from the upstream positivity and normalization theorems on gibbs_measure.
Claim. Let $sys$ be a recognition system with positive temperature $T_R$ and let $X:Ω→ℝ$ assign a cost coordinate to each state in a finite nonempty set $Ω$. The Gibbs probability distribution is the function $p(ω)=exp(-J(X(ω))/T_R)/Z$, where $Z$ is the partition function; this $p$ satisfies $p(ω)≥0$ for all $ω$ and $∑_ω p(ω)=1$, and is packaged as an element of the ProbabilityDistribution structure.
background
RecognitionSystem is the structure containing a positive real TR that sets the recognition temperature, with beta defined as its reciprocal. ProbabilityDistribution Ω is the structure whose fields are a function p:Ω→ℝ together with proofs of non-negativity and normalization to one. The upstream gibbs_measure definition supplies p(ω)=gibbs_weight sys (X ω)/partition_function sys X, which equals exp(-J(X(ω))/TR)/Z; its positivity and summation-to-one are established by the theorems gibbs_measure_pos and gibbs_measure_sum_one.
proof idea
One-line wrapper that sets the p field to gibbs_measure sys X and populates the nonneg and sum_one fields by direct appeal to gibbs_measure_pos and gibbs_measure_sum_one.
why it matters
This definition supplies the equilibrium reference peq used by every monotonicity result in the module. It is invoked by free_energy_antitone (showing free energy decreases along any JDescentOperator fixing the Gibbs state), by free_energy_ge_equilibrium (the variational principle), and by second_law (the bundled statement of the second law). In the Recognition Science setting it realizes the unique minimizer of recognition free energy, consistent with the J-uniqueness and self-similar fixed-point steps of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.