bremermann_limit
plain-language theorem explainer
The bremermann_limit defines the maximum operations per second per joule as twice the reciprocal of the reduced Planck constant. Researchers deriving quantum bounds on information processing cite this when scaling operation rates to available energy. The definition is a direct one-line assignment that imports hbar from the RS constants module.
Claim. The Bremermann limit is the real number $B = 2 / ħ$, where $ħ$ is the reduced Planck constant.
background
The module IC-002 derives computation limits from temporal discreteness (minimum time per operation is one tick), irrationality of φ (preventing exact finite simulation), Landauer erasure cost, and the Bremermann bound. The latter follows from the energy-time relation $E t ≥ ħ/2$, so maximum operations per second per joule equal $2/ħ$. Upstream, hbar is defined in Constants as $φ^{-5} · 1$ in RS-native units and also carries the CODATA numerical value.
proof idea
One-line definition that directly assigns twice the reciprocal of the imported hbar constant.
why it matters
This supplies the constant for the downstream positivity theorem bremermann_limit_pos and the max_ops_per_sec function. It fills the IC-002.11 slot on fundamental computation limits, linking to the eight-tick octave and hbar = φ^{-5} from the forcing chain. It touches the open question of whether φ-irrationality blocks exact finite algorithms for RS dynamics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.