erasure_jcost_eq
plain-language theorem explainer
The J-cost of information erasure equals exactly one quarter in Recognition Science units. Researchers deriving thermodynamic bounds from the ledger would cite this when quantifying minimal erasure expense. The proof is a direct algebraic reduction that unfolds the erasure cost and J-cost definitions then normalizes numerically.
Claim. The information cost of erasure satisfies $J_ {erasure} = 1/4$.
background
The InformationIsLedger module states that information is the physical ledger: every recognition ratio x > 0 carries J-cost J(x) with J(x) = 0 precisely when x = 1, J nonnegative, symmetric under x to 1/x, and Shannon entropy equal to expected J-cost. The module lists eight core theorems including the Landauer principle that erasure costs at least k_B T ln(2) in physical units. Upstream cost modules supply the integral form of Phi but this equality rests on the local J-cost definition.
proof idea
The proof is a one-line wrapper that unfolds erasure_jcost and Jcost then applies norm_num to obtain the constant 1/4.
why it matters
This supplies IC-001.18 and is referenced inside the ic001_certificate that declares the full Information IS the Ledger derivation complete. It quantifies the minimal ledger cost of erasure, consistent with the Recognition Composition Law and the phi-based constants of the forcing chain. No open scaffolding remains for this step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.