Materials Radiation Damage3 From Jcost

A placeholder for radiation damage

Radiation damage in solids begins when a high-energy neutron strikes an atom, knocking it from its lattice site. That first displaced atom, called a primary knock-on atom or PKA, then collides with neighbors, producing a cascade of further displacements. A standard engineering estimate says the number of displaced atoms is roughly the PKA energy divided by twice the displacement threshold energy, about 25 electronvolts for many metals. At typical neutron energies of 10 to 100 keV, a single cascade can displace hundreds or thousands of atoms.

In Recognition Science, the framework models this cascade using a cost function. The cost, a measure of how far a ratio departs from unity, is defined as J(m/e), where m is a mass and e is an energy. The framework's library, a machine-checked collection of formal theorems, proves three general facts about this cost: it is zero when the mass equals the energy, it is never negative for positive inputs, and a certain threshold constant, phi minus 3/2, is positive. These are properties of the cost function itself, not of radiation physics.

The module named materials-radiation-damage3-from-jcost contains a certificate bundling these three facts, and a proof that such a certificate exists. The research note attached to the module sketches a plan: a PKA displaces roughly phi^k secondary atoms, where phi is the golden ratio, and the cascade size follows a phi-power ladder. That note is a research idea, not a result. The formal code proves nothing about displacement cascades, because the definition of cost never mentions atoms, energies, or thresholds.

What the module does establish, in plain language, is that the cost function behaves sensibly: it vanishes at the identity, stays nonnegative, and has a positive threshold. Those facts hold for any positive inputs. The radiation-damage story would become a theorem only if the module defined m and e in terms of actual displacement physics, such as the PKA energy and the displacement threshold energy. Until then, the module is a template instantiated with a name, not a physical law.

The practical lesson for a reader is to distinguish the proved from the intended. The three cost facts are proved. The phi-ladder cascade estimate is a hypothesis with a named falsifier: a measurement of displacement counts that does not follow the phi-power scaling. The framework's honest position is that the radiation-damage application remains open, waiting for a definition that ties the cost to real material parameters.

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]

theorem cert_inhabited : Nonempty RadiationPKA3Cert := ⟨cert⟩

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

What this page does not claim

The phi-ladder cascade size is not proved; it is a research note. The module does not establish any physical property of radiation damage. The threshold phi minus 3/2 has no demonstrated connection to a displacement energy.

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