Chemistry Crystal Field3 From Jcost Cfse3 Cert

What the certificate proves

Crystal field stabilization energy (CFSE) is the energy difference that arises when metal d-electrons in a coordination complex occupy split orbital levels rather than a spherical average. In an octahedral field, the d-orbitals split into a lower-energy t2g set and a higher-energy eg set, and the CFSE for a d3 configuration is conventionally written as -1.2 times the ligand field splitting parameter Δ_o. This is a standard textbook result in inorganic chemistry, derived from the orbital occupancy and the magnitude of the splitting.

The Recognition Science declaration CFSE3Cert is a machine-checked certificate, a formal structure in the framework's library of verified theorems. It contains three statements about a function called domainCost, which is defined as J(m/e), where J is the framework's forced cost function and m and e are real numbers. The three statements are: the cost vanishes when m equals e; the cost is nonnegative when both inputs are positive; and the quantity phi minus 3/2 is positive, where phi is the golden ratio. The certificate also proves that these three statements are consistent, meaning the structure is inhabited.

In Recognition Science, the framework models recognition events as a discrete ledger, a record of comparisons, and the cost of recognition is forced by five plain conditions into the unique form J(x) = (x + 1/x)/2 - 1. The certificate's three facts are general properties of this cost function applied to any ratio of positive numbers. They hold for any m and e, without any reference to chemistry, orbitals, or transition metals. The declaration proves nothing specific to crystal fields, because the definition of domainCost does not connect m and e to any chemical quantity.

The declaration's own documentation states this plainly: it proves three general facts about J(m/e) and nothing specific to the subject. A research note in the same file records an intended application, where CFSE would equal -J(phi) times (phi + 1) times Δ_o, which evaluates to -0.309 times Δ_o. The empirical value is -1.2 times Δ_o, so the proposed formula is off by a factor of about 3.9. That comparison is a research note, not a theorem; the note itself calls the discrepancy structural.

What the certificate does establish is narrow and solid: a cost function with certain properties behaves consistently on ratios. What it does not establish is any connection between that cost function and the energy of d-electrons in a ligand field. The name CFSE3Cert records an intention, not a result. A reader should take the certificate as a verified statement about the cost function's elementary properties, and as a documented gap between a hoped-for application and the empirical chemistry it was meant to match.

structure CFSE3Cert 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

theorem cert_inhabited : Nonempty CFSE3Cert := ⟨cert⟩

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

What this page does not claim

The certificate does not derive CFSE for d3 octahedral complexes. The certificate does not show that the framework's cost function matches any measured crystal field energy. The certificate does not establish that phi minus 3/2 has any chemical meaning.

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