Materials Hardness Diamond Rs

Hardness and the ledger

Diamond sits at the top of the Mohs scale of mineral hardness with a value of 10, meaning it can scratch every other natural material. The scale, introduced by Friedrich Mohs in 1812, is ordinal: it ranks minerals by which one scratches which, rather than by a measured physical quantity. Diamond's status there is a classical fact, confirmed by centuries of scratching tests and by modern indentation measurements that put its Vickers hardness near 10,000 megapascals.

In Recognition Science, the framework models hardness through a ledger, a discrete record of recognition events. The framework's central object is a cost, a number that measures the price of recognizing one thing as another. The cost function J(x) = (x + 1/x)/2 - 1 is forced by five plain conditions, and it vanishes when its two inputs are equal, grows as they diverge, and stays nonnegative for positive inputs.

The module Hardness_Diamond_RS applies this cost function to the ratio m/e, where m and e are real numbers. Its machine-checked library of formal theorems proves three general facts: the cost is zero when m equals e, it is nonnegative when both inputs are positive, and the threshold phi - 3/2 is positive, where phi is the golden ratio. These facts hold for any positive real numbers m and e; they are not specific to diamond or to hardness.

What the module does not do is define m and e in terms of diamond's physical properties. The docstring records a research note: diamond's Mohs hardness of 10 is close to phi^5, about 11.09, a 10 percent difference. That observation is an identification, not a derivation. The formal theorems prove nothing about diamond itself, because the definition of domainCost as Jcost (m / e) makes no reference to any material.

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)

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

What this page does not claim

The module does not prove that diamond hardness equals phi^5. The module does not establish any physical property of diamond. The framework does not derive the Mohs scale from first principles.

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