Encyclopedia Chemistry Chemistry Acid Catalysis From Jcost

ARTICLE 4 claims 3 theorems 1 model

Chemistry Acid Catalysis From Jcost

Acid catalysis speeds reactions through proton transfer; a machine-checked library proves only general properties of a cost function, not a specific chemical law.

Acid catalysis and the cost function

Acid catalysis is a process where a reaction's rate increases because an acid donates a proton (H+) to a reactant, creating a more reactive intermediate. The Brønsted equation, log k = log G + α × pKa, connects the reaction rate constant (k) to the acid's strength (pKa), with α (the Brønsted coefficient) measuring how sensitive the rate is to acid strength. Empirically, α ranges from about 0.1 to 0.6 across different reaction types, with a value near 0.118 observed for some weak acid/base catalysis.

The framework defines a cost (a measure of discrepancy between two quantities) as J(m/e), where J(x) = (x + 1/x)/2 − 1. The framework proves three facts: the cost is zero when m equals e, the cost is nonnegative for positive inputs, and the constant φ − 3/2 (where φ is the golden ratio) is positive. These are general properties of the cost function itself, not results specific to acid catalysis.

In Recognition Science, the framework models the Brønsted coefficient as J(φ) ≈ 0.118, which sits at the lower end of the empirical range. However, the framework's definitions do not specify what m and e represent in chemical terms. The documentation explicitly states that nothing specific to acid catalysis is proved because the cost function is applied to a ratio m/e without defining those variables chemically.

What the framework establishes is a template: any chemical system that defines m and e in its own terms inherits these three properties. The Brønsted equation connection is a research note, a statement of intention, not a proved theorem. To make this a genuine theorem about acid catalysis, one would need a definition of m and e in terms of proton transfer or acid strength.

The practical takeaway is that the framework provides a formal skeleton for cost-based descriptions of catalysis, but the chemical content remains open. The empirical range of α (0.1 to 0.6) is broad, and the framework's value of 0.118 is one point within it, not a derivation of the full range.

THEOREM domainCost_at_eq · IndisputableMonolith/Chemistry/AcidCatalysis_FromJCost.lean
theorem domainCost_at_eq (r : ℝ) (h : r ≠ 0) : domainCost r r = 0 := by
  unfold domainCost; rw [div_self h]; exact Jcost_unit0
THEOREM domainCost_nonneg · IndisputableMonolith/Chemistry/AcidCatalysis_FromJCost.lean
theorem domainCost_nonneg (m e : ℝ) (hm : 0 < m) (he : 0 < e) : 0 ≤ domainCost m e := by
  unfold domainCost; exact Jcost_nonneg (div_pos hm he)
THEOREM canonicalThreshold_pos · IndisputableMonolith/Chemistry/AcidCatalysis_FromJCost.lean
theorem canonicalThreshold_pos : 0 < canonicalThreshold := by
  unfold canonicalThreshold; linarith [phi_gt_onePointFive]
MODEL domainCost · IndisputableMonolith/Chemistry/AcidCatalysis_FromJCost.lean
def domainCost (m e : ℝ) : ℝ := Jcost (m / e)

What this page does not claim

The framework does not prove the Brønsted equation itself. The framework does not derive the empirical range of α from 0.1 to 0.6. The framework does not claim J(φ) ≈ 0.118 is the only possible value for the Brønsted coefficient.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Chemistry/AcidCatalysis_FromJCost.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND