efficiencyRatio
plain-language theorem explainer
Modern CMOS energy per bit divided by the room-temperature Landauer energy defines a dimensionless efficiency gap of order 10^6. Thermodynamics-of-computation and RS information workers cite it when comparing practical hardware to the k_B T ln 2 floor. The body is a one-line quotient of two already-fixed real constants.
Claim. Define the efficiency ratio $\eta := E_{\mathrm{CMOS}} / E_L(T_{\mathrm{room}})$, where $E_{\mathrm{CMOS}} = 10^{-15}\,\mathrm{J}$ is the energy per bit operation in modern CMOS and $E_L(T_{\mathrm{room}})$ is the Landauer energy $k_B T\ln 2$ at room temperature.
background
Module INFO-004 derives the Landauer bound (minimum energy to erase one bit) from Recognition Science's fundamental timescale $\tau_0$ and the J-cost of recognition-then-forgetting. Classically, erasing one bit raises entropy by $k_B\ln 2$ and dissipates heat $Q = k_B T\ln 2$.
Sibling definitions fix the comparison numbers: current computer energy is the empirical CMOS figure $10^{-15}$ J per bit operation; Landauer energy at room temperature is $k_B T\ln 2$ evaluated at $T = 300,\mathrm{K}$, stated nearby as about $2.87\times 10^{-21}$ J. The ratio of those two energies is the natural dimensionless gap between practice and the thermodynamic floor.
Upstream edges into Hamiltonian emergence and universal self-reference supply the broader RS operator setting; they are not used in the arithmetic of this definition.
proof idea
Pure definition: the real is the quotient of currentComputerEnergy by landauerRoomTemp. No lemmas, no tactics, no proof obligations beyond noncomputable real division of two positive constants already introduced in the same module.
why it matters
The module targets ultra-low-power computing that approaches the Landauer limit, framed as patent- and paper-relevant thermodynamics of information from RS. This ratio makes the gap quantitative: practice sits roughly a million times above the $k_B T\ln 2$ floor tied to $\tau_0$ and J-cost. No downstream theorems yet consume it; it is a comparison constant for the INFO-004 narrative rather than a step in the T0–T8 forcing chain. It sits beside positivity and room-temp value lemmas that pin the denominator.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.