Materials Ferromagnetic Domain From Jcost

Domain walls and the cost function

A ferromagnetic domain wall is the thin transition layer between two regions of a magnetic material where the magnetization points in different directions. In iron, these walls are roughly 40 nanometers wide. The standard physics formula for the wall width is δ_DW = π√(A/K), where A is the exchange stiffness and K is the anisotropy constant. Exchange stiffness favors wide walls, because it penalizes abrupt changes in spin direction; anisotropy favors narrow walls, because it penalizes spins that point away from the easy axis. The width is the compromise between these two competing energies.

In Recognition Science, the framework models this ratio using its cost function J(x) = (x + 1/x)/2 - 1, which is forced by five plain conditions on any recognition cost. The module domainCost defines a cost for a domain wall as J(m/e), where m and e are real numbers standing in for the material parameters. The machine-checked library of formal theorems proves three general facts about this cost: it vanishes when m equals e, it is nonnegative for positive inputs, and the threshold value φ - 3/2 is positive. These are general properties of the cost function applied to any ratio; they are not specific results about magnetism.

The research note attached to the module records the intended physical identification: A/K = J(φ)², which would give a wall width of about 0.371 nanometers for iron. The measured value is 40 nanometers, so the scale is off by roughly two orders of magnitude. The note is explicit that this is a research idea, not a theorem. The formal proofs establish only the general cost properties, not the physical identification.

What the module actually establishes is narrow but solid. It shows that the cost function has the three properties needed to serve as a building block in a larger theory, and it packages those properties into a certificate structure. The physical step, defining m and e in terms of exchange and anisotropy, remains open. The gap between 0.371 and 40 nanometers is a concrete measure of what is missing.

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

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]

What this page does not claim

The module does not prove any physical result about ferromagnetic domain walls. The identification A/K = J(φ)² is a research note, not a theorem. The predicted width of 0.371 nm does not match the measured 40 nm for iron.

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