pith. machine review for the scientific record. sign in
def definition def or abbrev high

attemptFrequency

show as:
view Lean formalization →

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 in Recognition Science

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.

scope and limits

formal statement (Lean)

 167def attemptFrequency : ℝ := 1e13

proof body

Definition body.

 168
 169/-- The 8-tick period τ = 8 / (E_coh / ℏ) gives a characteristic time. -/

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (3)

Lean names referenced from this declaration's body.