Chemistry Radical Clock3 From Jcost

Radical Clock Calibration

A radical clock is a chemical reaction whose speed is known well enough to time other, faster reactions. The classic example is the ring opening of cyclopropylmethyl, which proceeds at a rate of about 10^8 per second. Chemists use such clocks to measure how quickly a short-lived intermediate appears or disappears.

In Recognition Science, the framework models recognition cost with a function J(x) = (x + 1/x)/2 - 1. The module Radical_Clock3_FromJCost defines a domain cost as J applied to the ratio of two quantities, m and e. The machine-checked library of formal theorems proves three facts about this cost: it is zero when m equals e, it is never negative for positive inputs, and the threshold phi - 3/2 is positive. These are general properties of the cost function, not results about any particular chemistry.

The research note attached to the module records an intended application: a rate constant k predicted as J(phi) times kT/h, giving about 7e11 per second. That number is roughly a thousand times larger than the measured radical clock rate. A revised guess, J(phi) raised to a power times a maximum rate, is labeled structural, meaning it is a direction for future work, not a derived result.

What the module actually establishes is limited to the three general facts. The definition of domainCost does not specify what m and e mean for a radical clock, so the module proves nothing about ring openings or rate constants. The chemistry content is a research note, shared verbatim with 2383 sibling modules, recording where the idea was meant to go.

In plain language: the framework's cost function has clean mathematical properties, and the module certifies those properties. The leap from cost to chemical kinetics is not made. A reader should treat the radical clock connection as an open target, not a theorem.

def domainCost (m e : ℝ) : ℝ := Jcost (m / e)

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 (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 : 0 < canonicalThreshold := by
  unfold canonicalThreshold; linarith [phi_gt_onePointFive]

def domainCost (m e : ℝ) : ℝ := Jcost (m / e)

What this page does not claim

The module does not prove any rate constant for cyclopropylmethyl ring opening. The structural guess k = J(phi)^n * k_max is not a derived result. The research note is not a theorem about chemistry.

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/Radical_Clock3_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: