erasure_jcost_pos
plain-language theorem explainer
The J-cost of bit erasure is strictly positive. Information theorists and physicists applying the Landauer principle within Recognition Science would cite this result. The proof is a term-mode reduction that unfolds the erasure definition, invokes the non-negativity and squared-form lemmas for J-cost at the specific ratio 2, then simplifies numerically to confirm the inequality.
Claim. Let $J(x) = (x-1)^2/(2x)$ for $x>0$. The J-cost of erasure satisfies $J(2)>0$.
background
The module InformationIsLedger identifies every physical fact with a recognition ratio $x>0$ whose information content is the J-cost $J(x)$. By definition $J(x)=0$ only at $x=1$ (perfect balance) and $J(x)>0$ otherwise. Upstream lemmas from the Cost module supply the algebraic identity $J(x)=(x-1)^2/(2x)$ together with the non-negativity statement $J(x)≥0$ for all $x>0$, both proved via the AM-GM inequality on the original expression $J(x)=(x+x^{-1})/2-1$.
proof idea
The term proof unfolds erasure_jcost, applies Jcost_nonneg to the hypothesis 0<2, applies Jcost_eq_sq to the hypothesis 2≠0, rewrites the equality, and finishes with norm_num to obtain the strict inequality.
why it matters
The result belongs to the IC-001 series that equates information with the physical ledger. It supplies the positivity half of the Landauer bound inside Recognition Science and sits alongside the sibling statements info_cost_pos_of_ne_one and shannon_entropy_equals_expected_jcost. It draws on the J-uniqueness and phi-ladder structure from the forcing chain but does not itself invoke the eight-tick octave or spatial dimension D=3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.