Materials Corrosion Rate From Jcost

Corrosion rate and recognition cost

Corrosion is the gradual destruction of metal by chemical reaction with its environment. Electrochemists often describe it with the Butler-Volmer equation, which relates the current density i_corr (the flow of charge per area) to the overpotential and the activation energy. A common simplification is the Tafel equation, where the log of the corrosion current is linear in the overpotential. The rate of metal loss follows from the current via Faraday's law: mass lost per time is proportional to current times molar mass divided by valence and Faraday's constant.

In Recognition Science, the framework proposes that the activation energy for corrosion is set by its cost function, a universal quantity that measures the price of a recognition event. The cost function J(x) = (x + 1/x)/2 - 1 is forced by five plain conditions, proved in the machine-checked library of formal theorems. At the recognition threshold, where the free energy change equals J times RT, the corrosion current density becomes approximately exp(-J) times the exchange current i_0, which evaluates to about 0.889 times i_0. This is a research note, not a proved result: the definition of the domain cost as J(m/e) does not yet connect m and e to actual corrosion quantities like molar mass or valence.

The formal module CorrosionRateFromJCost establishes three general facts about the function domainCost(m,e) = J(m/e). First, when m equals e, the cost is zero. Second, for positive m and e, the cost is nonnegative. Third, the number phi - 3/2 (where phi is the golden ratio) is positive. These are all true for any positive inputs, because they follow from the properties of J alone. The module also packages these into a certificate structure, showing that such a certificate exists. What the module does not do is establish anything specific to corrosion: it never defines m as a mass or e as an equivalent weight, so the corrosion interpretation remains a proposal.

The plain-language takeaway is this: the framework has a strong theorem about a universal cost function, and a plausible story about corrosion, but the bridge between them is not yet built. The formal proofs establish the cost function's basic properties, not the corrosion rate. A future theorem would need to define m and e in electrochemical terms and then derive the exponential relation. Until then, the corrosion rate from jcost is a research direction, not a result.

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]

What this page does not claim

No proved corrosion rate from the cost function exists yet. The module does not derive the Butler-Volmer or Tafel equations. No claim that the 0.889 factor matches any measured corrosion current.

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/Materials/CorrosionRateFromJCost.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: