Materials Work Hardening From Jcost

Work hardening and the cost of deformation

Work hardening, also called strain hardening, is the phenomenon in which a metal becomes harder and stronger as it is plastically deformed. Bend a paperclip back and forth and it resists more each time, until it snaps. The standard engineering description is the Hollomon equation, σ = K ε^n, which relates flow stress σ to plastic strain ε through a strength coefficient K and the work hardening exponent n. For many metals n lies between 0.1 and 0.5; for typical austenitic steels it is often near 0.2. The exponent is not a fundamental constant of nature; it depends on alloy, temperature, and processing history.

The Hollomon equation was introduced by John Herbert Hollomon in 1945 as a simple power-law fit to tensile test data. It is an empirical relation, not a derivation from first principles. Engineers use it to model forming operations, predict springback, and estimate how much a material can be shaped before it fractures. The exponent n is extracted by plotting log σ against log ε; the slope of the straight portion gives n. A higher n means the material hardens more rapidly with strain, which usually means better formability because strain is distributed more uniformly before necking begins.

In Recognition Science, the framework models the cost of recognition events through a function J(x) = (x + 1/x)/2 − 1, which is proved in the machine-checked library to be the unique cost function satisfying five plain conditions. The framework applies this cost to materials by defining a domain cost as J(m/e), where m and e are positive real numbers representing quantities in the material's deformation process. The module WorkHardeningFromJCost proves three general facts about this cost: it vanishes when m equals e, it is nonnegative for positive inputs, and the threshold φ − 3/2 is positive. These are the only theorems in the module; they are universally quantified and do not depend on any specific definition of m or e.

The research note attached to the module proposes that the work hardening exponent n equals J(φ), which evaluates to approximately 0.118, a value within the measured range for austenitic steels. That identification is a hypothesis, not a theorem, because the module never defines m and e in terms of dislocation density, grain size, or any physical mechanism. The three proved facts are true for any positive m and e, so they establish only the general shape of the cost: zero at equality, nonnegative elsewhere, and a positive threshold. They do not connect the cost to any particular material property.

The practical consequence is a template for what a recognition-based theory of hardening would need. To turn the general cost into a statement about steel, one must define m and e in the material's own terms, for example as a measure of applied strain and a measure of the material's capacity to accommodate it. Until such a definition exists, the module remains a formal skeleton: it proves that the cost behaves sensibly, but it says nothing specific about work hardening. The honest summary is that the framework provides a candidate cost function and a proof that it has the right qualitative features, while the physical bridge to Hollomon's exponent remains open.

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)

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

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

What this page does not claim

The module does not prove that the work hardening exponent equals 0.118; that remains a hypothesis. The module does not derive the Hollomon equation from Recognition Science. The module does not define m and e in terms of any physical deformation mechanism.

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/WorkHardeningFromJCost.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: