Chemistry Inorganic3 Crystal From Jcost

A crystal module with generic bones

Inorganic crystals melt when thermal vibrations overcome the electrostatic forces holding ions in place. Sodium chloride, common table salt, melts at 1074 K. The melting point tends to rise with ionic character: more strongly charged ions, or smaller ions, make stiffer lattices that survive higher temperatures. This is a classical trend in solid-state chemistry, quantified by empirical scales of ionic character.

The module named Inorganic3_Crystal_FromJCost in the machine-checked library of formal theorems was planned as a Recognition Science derivation of that trend. Recognition Science starts from a cost, a forced penalty for any mismatch between two quantities. The framework's central result, proved in the library, is that any cost function satisfying five plain conditions must equal J(x) = (x + 1/x)/2 - 1. The plan was to define the domain cost for a crystal as J(m/e), where m and e would stand for something like a mass and an electrostatic charge, and then derive melting temperatures.

The library file proves three facts, and only three. First, the cost vanishes when the two inputs are equal: J(m/e) = 0 when m = e. Second, the cost is never negative for positive inputs. Third, the number phi - 3/2 is positive, where phi is the golden ratio, about 1.618. These are all true, machine-checked, and completely general. They hold for any positive real numbers m and e, with no reference to crystals, ions, or melting.

The module defines domainCost as J(m/e) without ever defining what m and e mean for a crystal. The file itself says this plainly: it proves nothing specific to the subject. The melting-point formula in the research note, T_melt = 8.47 * k_B * 300K = 2541 K, is a stated intention, not a proved result. The gap is definitional: to turn the generic cost into a crystal theorem, someone must first define m and e in the crystal's own terms, for example as ionic mass and charge, and then prove the melting relation from those definitions.

What the module does establish is a pattern worth noticing. A structure named InorganCryst3Cert bundles the three generic facts into a certificate, and the library proves a certificate exists. That is a small, honest result: the generic cost function has the right shape, zero at equality and nonnegative elsewhere, to serve as a building block. The crystal-specific payoff, a derived melting point, remains open. The module is a scaffold with the crystal content still missing.

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 derive or predict any crystal melting temperature. The melting-point formula in the research note is not proved in the library file. No claim is made that the golden ratio threshold phi - 3/2 has a physical meaning for crystals.

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/Chemistry/Inorganic3_Crystal_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: