Materials Yield Stress3 From Jcost

Yield stress and the cost function

Yield stress is the stress at which a material begins to deform plastically, permanently changing shape rather than springing back. For many metals, this stress falls with temperature, often approximated by sigma_y(T) ~ sigma_y(0) * (1 - T/T_m)^n, where T_m is the melting temperature and n is an exponent between 1 and 2. A low-temperature metal like iron (body-centered cubic) typically shows n near 1, while aluminum (face-centered cubic) shows n near 0.3.

The module Yield_Stress3_FromJCost in the framework's machine-checked library of formal theorems takes a different starting point. It defines a cost function J(x) = (x + 1/x)/2 - 1, which measures the recognition cost of a ratio x. The module then defines a domain cost as J(m/e), where m and e are real numbers. The Lean code proves three general facts: this cost is zero when m equals e, it is never negative for positive inputs, and the golden ratio minus 1.5 is positive.

These three facts are true for any positive m and e. The module does not define what m and e mean for a specific material. The docstring notes a research idea: that the exponent n might equal J(phi) * phi^2, which computes to about 0.309, close to the 1/3 exponent seen in face-centered cubic metals. But this identification is a research note, not a proved result. The module itself proves nothing specific to yield stress because domainCost is defined without reference to any material property.

What the module does establish is a template. It shows that a cost function with these three properties can be certified: the cost vanishes at equality, stays nonnegative, and has a positive threshold. Any future module that defines m and e in terms of actual material quantities could then inherit these certified facts. Until then, the yield stress connection remains an open target, not a theorem.

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

The module does not prove any specific yield stress temperature dependence. The identification of n with J(phi) * phi^2 is a research note, not a theorem. The module does not define m and e in terms of material properties.

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