Materials Grain Boundary2 From Jcost

A grain boundary strength formula

In materials science, the Hall-Petch relation describes how the yield strength of a polycrystalline metal rises as its grains shrink. The classical form is σ_y = σ_0 + k_HP · d^(−1/2), where d is the average grain diameter and k_HP is a constant that depends on the material. The framework's research note proposes that k_HP = J(φ) · G · b, where G is the shear modulus and b is the Burgers vector, a vector that measures the slip of a crystal lattice. That proposal is a structural guess, not a proved result.

The module itself, Grain_Boundary2_FromJCost, defines a cost function as domainCost (a measure of recognition cost) equal to J(m/e), where J is the forced cost function from the framework's core theorem. The machine-checked library of formal theorems proves three general facts about this function: it vanishes when m equals e, it is never negative for positive inputs, and the number φ − 3/2 is positive. These facts hold for any positive inputs m and e, so they say nothing specific to grain boundaries. The library proves no statement that connects this cost to the Hall-Petch coefficient.

The module also packages those three proofs into a structure called HallPetchCoeffCert, which certifies that the general properties hold. The name suggests a certificate for the Hall-Petch coefficient, but the certificate contains no definition of m or e in terms of grain size, shear modulus, or Burgers vector. Without such a definition, the module cannot establish the proposed formula. The research note itself says the paragraph above is a research note recording where the idea was meant to go, not a result.

What the module does establish is a small, clean example of the framework's cost function at work: it shows that J(m/e) behaves sensibly for any positive ratio, and it records a positive threshold value. The grain boundary application remains a target for future work, waiting for a definition of m and e in materials terms. Until then, the honest summary is that the framework proves the mathematics of the cost function, not the metallurgy.

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 Hall-Petch formula k_HP = J(phi) * G * b is not proved by this module. The module does not show that grain boundaries obey the cost function. The value phi - 3/2 is not shown to relate to any measured material property.

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