erasure_jcost
plain-language theorem explainer
erasure_jcost defines the information cost of a 2-to-1 bit erasure as the value of the J-cost function at ratio 2. Researchers deriving the Landauer bound inside Recognition Science cite this when quantifying the minimal positive cost of erasing one bit from equiprobable states. The definition is a direct one-line instantiation of the general J-cost on the binary ratio.
Claim. The J-cost of bit erasure is defined as $J(2)$, where $J(x) = (x + x^{-1})/2 - 1$ gives the information cost of recognition ratio $x$.
background
The InformationIsLedger module identifies every physical fact with a recognition ratio $x > 0$ whose information content is its J-cost. J-cost vanishes only at $x = 1$ (balanced ledger state) and is strictly positive otherwise; the module further equates Shannon entropy with expected J-cost. Upstream lemmas establish that the cost of any RecognitionEvent is its J-cost and that J is nonnegative for positive ratios.
proof idea
This is a one-line definition that applies the J-cost function to the constant 2.
why it matters
The definition supplies the concrete value used by erasure_jcost_eq and erasure_jcost_pos to prove the cost equals 1/4 and is positive. It fills the Landauer-principle slot (IC-001.17) in the module's core list, anchoring the claim that information is the physical ledger. The construction sits inside the T5 J-uniqueness and RCL framework, providing a numerical instance of information cost before phi-ladder scaling is applied.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.