Materials Grain5

A placeholder for grain size

The Hall-Petch relation is a classic empirical law of materials science: as metal grains shrink, the yield strength rises. In its common form, σ_y = σ_0 + k·d^(-1/2), where d is the average grain diameter and k is a material constant. The law, named for E.O. Hall and N.J. Petch in the early 1950s, captures a real effect: smaller grains mean more grain boundaries, which block dislocation motion and make the metal harder to deform.

In the Recognition Science framework, the module materials grain5 was intended to derive a Hall-Petch-like scaling from the framework's cost function. The cost function J(x) = (x + 1/x)/2 - 1 measures the price of a recognition event. The module defines a domain cost as J applied to the ratio of two quantities, m and e, and then proves three facts: the cost is zero when m equals e, it is nonnegative for positive inputs, and a certain threshold φ - 3/2 is positive (φ is the golden ratio).

Those three facts are true, but they are general properties of J, not specific to grain size. The module never defines what m and e mean for a metal. The docstring admits this: it says the Lean code proves nothing specific to the subject, because domainCost is defined without reference to one. The module is a template, shared verbatim with 2,383 sibling modules, each hoping for a subject-specific definition that never arrives.

What the module does establish, in plain language, is a small piece of the framework's machinery. It shows that the cost function behaves sensibly: it bottoms out at zero when the two inputs match, and it never goes negative. The threshold φ - 3/2 ≈ 0.118 is a positive number, which the research note hoped to plug into a Hall-Petch variant as k/(0.118·d₀). But that step remains a research note, not a theorem.

The lesson for a reader: the framework's library of formal theorems contains many modules whose names promise subject matter, but the promise is only kept when the module defines its variables in that subject's terms. Here, the grain-size connection is a goal, not a result. The general cost properties are proved; the Hall-Petch derivation is not.

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

This module proves the Hall-Petch relation or any grain-size-dependent yield stress law. The quantities m and e are defined in terms of physical grain properties. The threshold φ - 3/2 has a demonstrated role in any materials phenomenon.

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