No prose has been written for this declaration yet. The Lean source and graph data below render
without it.
generate prose now
formal statement (Lean)
128theorem rate_enhancement (enz : Enzyme) (h : IsIdealEnzyme enz)
129 (hx : enz.transition_state_coord ≠ 1) :
130 catalyzedRate enz / uncatalyzedRate enz.transition_state_coord =
131 Real.exp (uncatalyzedBarrier enz.transition_state_coord) := by
proof body
Term-mode proof.
132 rw [ideal_enzyme_unit_rate enz h]
133 unfold uncatalyzedRate boltzmannFactor
134 rw [one_div]
135 rw [Real.exp_neg]
136
137/-! ## φ-Scaling of Active Site Rungs -/
138
139/-- The transition-state J-cost scales with a φ-ladder rung. -/
depends on (22)
Lean names referenced from this declaration's body.
-
of
in IndisputableMonolith.Astrophysics.NucleosynthesisTiers
decl_use
-
boltzmannFactor
in IndisputableMonolith.Chemistry.ActivationEnergy
decl_use
-
boltzmannFactor
in IndisputableMonolith.Chemistry.EnzymeCatalysis
decl_use
-
catalyzedRate
in IndisputableMonolith.Chemistry.EnzymeCatalysis
decl_use
-
Enzyme
in IndisputableMonolith.Chemistry.EnzymeCatalysis
decl_use
-
ideal_enzyme_unit_rate
in IndisputableMonolith.Chemistry.EnzymeCatalysis
decl_use
-
IsIdealEnzyme
in IndisputableMonolith.Chemistry.EnzymeCatalysis
decl_use
-
uncatalyzedBarrier
in IndisputableMonolith.Chemistry.EnzymeCatalysis
decl_use
-
uncatalyzedRate
in IndisputableMonolith.Chemistry.EnzymeCatalysis
decl_use
-
rung
in IndisputableMonolith.Compat.Constants
decl_use
-
rung
in IndisputableMonolith.Engineering.AsteroidOreSpectroscopy
decl_use
-
of
in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization
decl_use
-
cost
in IndisputableMonolith.Foundation.MultiplicativeRecognizerL4
decl_use
-
cost
in IndisputableMonolith.Foundation.ObserverForcing
decl_use
-
of
in IndisputableMonolith.Foundation.PhiForcingDerived
decl_use
-
of
in IndisputableMonolith.Foundation.SpectralEmergence
decl_use
-
of
in IndisputableMonolith.Information.PhysicsComplexityStructure
decl_use
-
boltzmannFactor
in IndisputableMonolith.Information.ShannonEntropy
decl_use
-
rung
in IndisputableMonolith.Masses.AnchorPolicy
decl_use
-
rung
in IndisputableMonolith.Masses.RSBridge.Anchor
decl_use
-
rung
in IndisputableMonolith.RSBridge.Anchor
decl_use
-
boltzmannFactor
in IndisputableMonolith.Thermodynamics.BoltzmannDistribution
decl_use