higher_cost_lower_weight
plain-language theorem explainer
Higher J-cost states receive strictly lower Gibbs weights in any RecognitionSystem. Biologists modeling thermodynamic natural selection would cite the monotonicity to justify exponential suppression of costly configurations. The proof unfolds the exponential definition of gibbs_weight and reduces the inequality to the positivity of TR via exp_lt_exp.mpr and div_lt_div_of_pos_right.
Claim. Let $w(z) = e^{-J(z)/T_R}$ denote the Gibbs weight of state $z$ in a RecognitionSystem with recognition temperature $T_R > 0$. If $J(x) > J(y)$ then $w(x) < w(y)$.
background
A RecognitionSystem is a structure containing a positive real TR that sets the noise level: TR = 0 recovers deterministic recognition while TR → ∞ yields maximum disorder. The Gibbs weight is the unnormalized Boltzmann factor exp(-Jcost x / TR). Jcost is the recognition cost function whose properties are fixed by upstream number theory (T5 J-uniqueness and the Recognition Composition Law).
proof idea
Unfold the definition of gibbs_weight to reach exp(-Jcost x / TR) < exp(-Jcost y / TR). Apply exp_lt_exp.mpr to obtain the equivalent inequality -Jcost x / TR < -Jcost y / TR. Invoke sys.TR_pos to justify div_lt_div_of_pos_right, then finish with linarith on the supplied hypothesis Jcost x > Jcost y.
why it matters
The result supplies the monotonicity required for selection pressure inside the J-Cost Boltzmann bridge. It directly encodes the thermodynamic basis for natural selection stated in the module doc-comment. The theorem sits alongside weight_maximized_at_one and low_temp_selection to complete the biology-facing package; no downstream theorems yet depend on it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.