entropy_neg_off_eq
plain-language theorem explainer
The theorem shows that the entropy function S(r) = -log(J(r) + 1) is strictly negative for every r > 0 with r ≠ 1. Researchers deriving thermodynamics from the J-cost functional cite it to confirm the qualitative second law. The proof is a direct term reduction that unfolds the entropy definition and invokes J-cost positivity to establish that the logarithm argument exceeds 1.
Claim. Let J denote the J-cost function. Define the entropy by S(r) := -log(J(r) + 1). Then for every real number r > 0 with r ≠ 1, S(r) < 0.
background
The module derives the four thermodynamic laws from the single J-cost functional. J-cost satisfies J(r) > 0 whenever r > 0 and r ≠ 1, by the lemma Jcost_pos_of_ne_one which rewrites J as a square and applies positivity of squares and division. Entropy is introduced by the definition S(r) := -log(J(r) + 1), which is zero precisely at equilibrium where J vanishes. The module documentation states that the second law corresponds to entropy increase away from the J-cost minimum.
proof idea
The term proof unfolds the definition of entropy_RS. It applies the negation-of-negative lemma to reduce to log(J(r) + 1) > 0. Positivity of the logarithm then follows from J(r) > 0 supplied by Jcost_pos_of_ne_one, with the final arithmetic step closed by linarith.
why it matters
This theorem supplies the entropy_negative_off_eq field inside the master certificate thermodynamicLawsCert. It thereby completes the qualitative second law in the Recognition Science framework, where entropy increase equals J-cost minimization over time. The module documentation lists this as one of the four structural derivations that follow from J-cost alone.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.