pith. machine review for the scientific record. sign in
module module high

IndisputableMonolith.Chemistry.ActivationEnergy

show as:
view Lean formalization →

The ActivationEnergy module defines the J-cost function J(x) = ½(x + 1/x) - 1 and builds chemical activation barriers, Boltzmann factors, and Arrhenius rates from it in RS-native units. Researchers modeling reaction kinetics inside the Recognition Science framework cite these definitions when linking J-cost to transition-state stabilization. The module consists of direct definitions plus elementary nonnegativity and monotonicity statements.

claim$J(x) = ½(x + x^{-1}) - 1$. Activation barrier equals $J_transition - J_reactant$, Boltzmann factor is $exp(-activationBarrier)$, and Arrhenius rate is the temperature-dependent form built from these quantities.

background

The module resides in the Chemistry domain and imports the RS time quantum τ₀ = 1 tick from Constants. It introduces the J-cost function, which measures the recognition defect of a configuration x, together with reactant and transition-state specializations J_reactant and J_transition. ActivationBarrier is formed as their difference, after which boltzmannFactor and arrheniusRate are defined directly from it.

proof idea

This is a definition module. It states the J-cost formula, constructs the barrier and rate objects as immediate applications of J, and records the elementary facts barrier_nonneg, higher_barrier_slower, and higher_temp_faster.

why it matters in Recognition Science

These definitions supply the J-cost language required by the EnzymeCatalysis module, which treats enzymes as J-cost lenses that cancel the saddle at the transition state. The module thereby embeds classical activation-energy concepts inside the T5 J-uniqueness and RCL structure of Recognition Science.

scope and limits

used by (1)

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

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (22)