attemptFrequency
plain-language theorem explainer
Definition attemptFrequency fixes the Arrhenius pre-factor at 10^{13} s^{-1} to match typical bond vibration rates. Kinetic modelers working from J-cost maxima cite this value when computing rates in RS units. The entry is a bare numerical assignment.
Claim. $A = 10^{13} s^{-1}$, where $A$ is the pre-exponential factor in the Arrhenius rate law $k = A e^{-E_a/RT}$.
background
The module treats activation barriers as maxima of the J-cost function along a reaction coordinate. Boltzmann statistics over the J-landscape then recover the Arrhenius form. The pre-exponential factor is identified with the characteristic molecular vibration frequency, scaled to the eight-tick period built from the fundamental tick quantum.
proof idea
Direct constant definition with no lemma applications or tactic steps.
why it matters
Supplies the numerical constant used by eightTickPeriod and attempt_freq_8tick. It anchors the pre-exponential factor to the eight-tick octave (T7) of the forcing chain and to the RS-native time unit tick. No open scaffolding questions are attached to this entry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.