erasureJCost
plain-language theorem explainer
The J-cost of erasing one bit is the constant J(2)=1/4, the recognition cost of collapsing two equiprobable states to one. Anyone deriving Landauer's bound inside Recognition Science cites this yardstick. It is a one-line specialization of the closed-form J-cost at ratio 2.
Claim. Define the erasure cost by $J_{\mathrm{erase}} := J(2) = \dfrac{2+2^{-1}}{2}-1 = \dfrac{1}{4}$, i.e. the unique recognition cost of the two-to-one state collapse.
background
The module derives Landauer's bound $E_{\min}=k_B T\ln 2$ from the RS recognition timescale $\tau_0$ and the J-cost. Erasure is treated as recognize-then-reset: an observer collapses an uncertain bit (two states) to a known state, paying a positive recognition cost and dissipating heat.
The unique cost functional forced by the Recognition Composition Law is $J(x)=(x+x^{-1})/2-1$ (also $\cosh(\log x)-1$), with $J(1)=0$ and $J(x)>0$ for $x\neq 1$. Upstream definitions (Cost.Jcost, ObserverForcing.cost, RefineTrigger.Jcost) all instantiate this same formula on positive ratios.
Here the ratio is the state-count ratio 2 (two microstates mapped to one), so the bare dimensionless erasure cost is simply $J(2)$.
proof idea
Pure definitional specialization: substitute $x=2$ into $J(x)=(x+x^{-1})/2-1$, yielding the closed value $(2+1/2)/2-1=1/4$. No lemmas or tactics; the body is the arithmetic expression for $J(2)$.
why it matters
Supplies the dimensionless RS-native cost that the Landauer module converts into energy via $\tau_0$ and $k_B T$. The sibling claim jcost_equals_thermodynamic is intended to identify this constant (up to the thermodynamic factor) with $\ln 2$, closing the INFO-004 derivation of $E_{\min}=k_B T\ln 2$.
The value rests on T5 J-uniqueness: only this $J$ satisfies the Recognition Composition Law, so the two-to-one collapse cost is forced rather than postulated. Downstream energy and power bounds in the same module (landauerEnergy, minimumErasurePower, landauer_from_tau0) are meant to scale this constant into physical units.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.