currentComputerEnergy
plain-language theorem explainer
Sets the empirical modern-CMOS energy per bit operation at 10^{-15} J, for side-by-side comparison with the Landauer floor. Anyone quantifying the engineering gap to the thermodynamic limit cites this constant. It is a bare numeric definition, not a derived claim.
Claim. The reference energy cost of a present-day computer bit operation is fixed at $E_{\mathrm{CMOS}} = 10^{-15}\,\mathrm{J}$ (joules per bit operation).
background
Module INFO-004 derives Landauer's bound from Recognition Science's fundamental timescale $\tau_0$ and the J-cost of erasure. Classically, erasing one bit dissipates at least $E_{\min} = k_B T \ln 2$ as heat; RS recovers the same floor from recognition-then-forget dynamics on the $\tau_0$ clock.
To make the gap concrete, the module records an engineering benchmark: modern CMOS logic sits near $10^{-15}$ J per bit operation, while the room-temperature Landauer energy is near $10^{-21}$ J. The ratio is order $10^6$. This definition is that CMOS benchmark, not a theorem.
proof idea
Numeric constant definition only: the real value 1e-15, annotated as joules per bit operation. No lemmas, no tactics, no proof obligations.
why it matters
Direct input to the efficiency ratio in the same module, which divides this CMOS figure by the room-temperature Landauer energy and thereby exhibits the million-fold headroom above the thermodynamic floor. That ratio underwrites the module's framing on ultra-low-power computing that approaches the Landauer limit from RS $\tau_0$ and J-cost structure (INFO-004 target). It is scaffolding for comparison, not part of the forcing chain T0–T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.