pith. sign in
module module high

IndisputableMonolith.Chemistry.ActivationEnergy

show as:
view Lean formalization →

The ActivationEnergy module defines the J-cost function and derived objects including reactant and transition costs, activation barrier, Boltzmann factor, and Arrhenius rate. Researchers extending Recognition Science to reaction kinetics and catalysis would cite these definitions. The module consists solely of definitions and supporting properties with no theorems.

claim$J(x) = ½(x + x^{-1}) - 1$. The activation barrier equals the J-cost difference between transition state and reactant; the rate follows an Arrhenius form with that barrier in the exponent.

background

Recognition Science derives all quantities from the J-cost function introduced in the forcing chain. This module applies the function to chemistry by defining J for a reactant state, a transition state, and the barrier as their difference. It imports the base time quantum τ₀ from the Constants module and builds Boltzmann and rate expressions on top of the barrier.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

These definitions supply the J-cost objects required by the EnzymeCatalysis module to state that an enzyme acts as a J-cost lens canceling the saddle point at the active site, realizing the Q19 claim of exact saddle-point stabilization.

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)