quantumEnergy
plain-language theorem explainer
Minimum energy scale for a process lasting one recognition tick τ₀, taken from the energy-time uncertainty bound as ℏ/τ₀ with ℏ ≈ 1.054×10⁻³⁴ J·s. Information and thermodynamics workers cite it when comparing the quantum floor to the Landauer heat k_B T ln(2). It is a pure definitional quotient of the SI reduced Planck constant by τ₀ in seconds.
Claim. The quantum energy associated to the recognition timescale is $E_{\mathrm{q}} := \hbar / \tau_0$, where $\hbar \approx 1.054 \times 10^{-34}\,\mathrm{J\cdot s}$ and $\tau_0$ is the fundamental tick expressed in seconds. This is the energy scale suggested by $\Delta E \,\Delta t \ge \hbar/2$ for a process of duration $\tau_0$.
background
Module INFO-004 aims to derive Landauer's bound from Recognition Science's fundamental timescale τ₀. Landauer (1961) states that erasing one bit dissipates at least $E_{\min} = k_B T \ln 2$ as heat. In RS the story is that τ₀ sets the recognition clock, erasure is a recognize-then-forget act with a J-cost, and τ₀ also sets the rate at which that thermodynamic cost is paid.
The energy-time uncertainty relation $\Delta E ,\Delta t \ge \hbar/2$ supplies a separate quantum floor: any process confined to duration τ₀ must involve energy of order $\hbar/\tau_0$. This definition packages that scale in SI units so it can sit next to the thermodynamic Landauer energy and the room-temperature specializations defined alongside it.
The sibling tau0_seconds converts the RS tick into seconds; Boltzmann's constant and room temperature are likewise fixed numerically in the same module for SI comparisons.
proof idea
Definitional, not a proved theorem. The body is the single real quotient $1.054\times 10^{-34}$ divided by the SI value of the recognition tick. No lemmas are applied; the noncomputable marker is only for real arithmetic with decimal literals. Downstream equalities that mention this scale will unfold the definition by rfl or simp.
why it matters
Gives the quantum energy floor that the Landauer-from-τ₀ development places beside $k_B T \ln 2$ and the power bound $E_{\mathrm{Landauer}}/\tau_0$ for maximum-speed erasure. That comparison is the module's stated target: τ₀ both sets when the thermodynamic cost is paid and, via uncertainty, how much energy a one-tick process must carry.
In the broader RS chain the tick is the eight-tick octave timescale (forcing step T7). Here it is used only as a duration, not re-derived. The definition stays in SI numerics rather than the RS-native $\hbar = \varphi^{-5}$, so it is a bridge object for thermodynamic and patent-facing comparisons, not a forcing-chain step. The dependency graph currently lists no downstream users; siblings such as the Landauer-from-τ₀ statement and minimum erasure power are the natural consumers once wired.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.