Materials Hardness Mohs Rs

Hardness and the phi-ladder

The Mohs scale, introduced by Friedrich Mohs in 1812, ranks minerals by scratch resistance: talc is 1, gypsum 2, up to diamond at 10. Each higher mineral scratches all lower ones. It is an ordinal scale, not a linear one; the gap between 9 and 10 is far larger than between 1 and 2. The scale remains useful in field geology because it needs no equipment, only a fingernail, a copper coin, a steel blade, and a set of reference minerals.

Recognition Science models hardness as a discrete record of recognition events, a ledger of costs for comparing one material's response to another's. The framework's central cost function is J(x) = (x + 1/x)/2 - 1, which vanishes when two materials are identical and grows as they diverge. The framework models the Mohs steps as powers of the golden ratio phi = (1 + sqrt(5))/2 ≈ 1.618: talc sits near phi^1, topaz near phi^6 ≈ 17.9, diamond near phi^7 ≈ 29. This phi-ladder is a research note, a definitional choice about how to assign numbers to steps, not a proved result about minerals.

What the module actually proves is three general facts about the cost function, none of them specific to hardness. It proves that the cost of comparing a material to itself is zero, that the cost is never negative for positive inputs, and that phi - 3/2 is positive. These hold for any positive real numbers m and e plugged into J(m/e). The module defines a certificate bundling these three facts, and proves that certificate exists. The claim that this says something about Mohs hardness would require a definition of m and e in terms of mineral properties, which the module does not provide.

In plain language: the machine-checked library of formal theorems proves a small, true statement about a mathematical function, and attaches a research note guessing that the function might describe hardness. The guess is not part of the proof. The library's theorems are correct; the connection to Mohs is an untested hypothesis awaiting a definition of what hardness means in the framework's own terms.

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 phi-ladder is not a proved result about Mohs hardness. The module does not define hardness in terms of any measurable mineral property. The cost function's general theorems do not establish a physical connection to scratching.

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_Mohs_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: