Materials Dislocation Density From Jcost

Dislocation density and J-cost

Dislocation density, usually written ρ, is the total length of dislocation lines per unit volume in a crystal, a measure of how badly its atomic planes have been deformed. In the Taylor hardening law, the flow stress of a metal rises with the square root of this density: σ_flow = α × G × b × √ρ, where G is the shear modulus, b is the Burgers vector (the slip step size), and α is a dimensionless constant. For face-centered cubic metals, measured α values sit roughly between 0.1 and 0.5, with a typical empirical value near 0.118.

In Recognition Science, the framework models a universal cost function J(x) = (x + 1/x)/2 − 1, which measures the price of a mismatch between a measured value and an expected value. The framework's library, a machine-checked collection of formal theorems, proves three general facts about this cost: it vanishes when measured equals expected, it is never negative for positive inputs, and the golden-ratio constant φ − 3/2 is positive. These are properties of the cost function itself, not of any particular material.

What the module does is define a domain cost as J(measured / expected) and bundle the three proved facts into a certificate structure. The plain-language content is deliberately modest: at equilibrium (measured equals expected) the cost is zero, and away from equilibrium it is nonnegative. The research note attached to the module records an intended application: at hardening saturation, ρ × b² = J(φ), which would tie the dislocation density directly to the golden ratio. That application is not proved in the module, because the module defines its cost without reference to a specific physical meaning for measured and expected.

The distinction matters. The Taylor law and the empirical α range are standard materials science, measured facts. The three cost-function theorems are proved in the framework. The saturation relation ρ × b² = J(φ) is a hypothesis, a prediction with a named falsifier: if measured ρ × b² at saturation disagrees with J(φ) beyond experimental error, the identification fails. The module itself establishes only the general cost properties, not the material-specific claim.

def domainCost (measured expected : ℝ) : ℝ := Jcost (measured / expected)

theorem domainCost_at_equilibrium (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 (measured expected : ℝ) : ℝ := Jcost (measured / expected)

What this page does not claim

The module proves no material-specific theorem about dislocation density. The saturation relation ρ × b² = J(φ) is not established by the module. The empirical α range 0.1–0.5 is a measured fact, not a framework derivation.

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