Materials Hardness3 From Phi Ladder

Hardness and the phi ladder

Hardness measures how well a solid resists being scratched or indented. The common scales are relative: Mohs hardness ranks minerals from talc at 1 to diamond at 10, while the Vickers scale (HV) measures the force per unit area of an indentation. Diamond sits near 10000 HV, corundum near 2000, quartz near 1000, calcite near 200, and talc near 30.

In Recognition Science, a ledger (a discrete record of events) assigns a cost to any ratio between two quantities. The framework's cost function J(x) = (x + 1/x)/2 - 1 is zero when the ratio is 1, and it grows as the ratio moves away from 1. The golden ratio φ ≈ 1.618 emerges as the unique self-similar scaling in this system.

The module Hardness3_FromPhiLadder proposes to connect these ideas. The research note records that diamond/talc ≈ 333, while φ^15 ≈ 1364, and φ^12 ≈ 322, which is close to the Mohs ratio 10/1. These are empirical observations, not derivations.

What the machine-checked library of formal theorems actually proves is narrower. It defines a cost function on a ratio m/e, and proves three general facts: the cost is zero when m equals e, it is never negative for positive inputs, and the number φ - 3/2 is positive. These are true for any positive numbers m and e, with no reference to hardness or materials.

The module assembles these three facts into a certificate structure, which is a formal package saying the cost function behaves this way. The certificate exists, but it is empty of material content: it would become a theorem about hardness only if m and e were defined in terms of actual material properties, which the module does not do.

In plain terms, the module proves a small, general fact about the cost function and leaves the hardness connection as a stated intention. The empirical ratios are suggestive, but the formal bridge from cost to diamond or talc is not built.

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]

structure Hardness3Cert where
  cost_at_eq : ∀ r : ℝ, r ≠ 0 → domainCost r r = 0
  cost_nonneg : ∀ m e : ℝ, 0 < m → 0 < e → 0 ≤ domainCost m e
  threshold_pos : 0 < canonicalThreshold

What this page does not claim

The module does not prove any specific hardness values or ratios. The module does not define m and e in terms of actual material properties. The empirical phi-ladder ratios are observations, not derivations.

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