hbarQuantum
plain-language theorem explainer
hbarQuantum defines the action quantum ħ as the product of the coherence energy E_coh and the fundamental time tick τ₀ in RS-native units. Researchers deriving action integrals or Planck-scale masses in the Recognition framework cite this definition. It is realized as a direct one-line multiplication that inherits the simp attribute from its factors.
Claim. The action quantum satisfies $ħ = E_{coh} · τ_0$, where $E_{coh} = φ^{-5}$ is the coherence energy quantum and $τ_0 = 1$ is the fundamental RS time quantum.
background
The RS-native unit system defines the tick τ₀ as the atomic time interval and the coherence quantum as E_coh = φ^{-5}. The action quantum ħ is the derived product that supplies the Planck constant equivalent. Upstream, Constants.tick fixes τ₀ = 1 while cohQuantum pulls E_coh directly; the module documentation lists act as the action quantum ħ = E_coh · τ₀.
proof idea
This is a one-line definition that multiplies cohQuantum by tick and carries the @[simp] attribute for automatic reduction.
why it matters
The definition supplies the ħ factor used by action_raw to scale action counts and by hbarQuantum_eq_Ecoh to equate ħ with E_coh. It enters planckMass_rs through the expression sqrt(ħ c / G) with c = 1. It realizes the module's account of derived quanta and aligns with the φ-ladder scaling and eight-tick octave from the upstream tick definition.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.