Astrophysics Galaxy Metallicity3 From Jcost

The mass-metallicity module

In astronomy, the mass-metallicity relation is the observed tendency for more massive galaxies to hold a higher fraction of elements heavier than hydrogen and helium. Astronomers measure this as the ratio of a galaxy's metal abundance to the Sun's, often written Z/Z_sun, and find that a galaxy ten times more massive is typically about 0.35 dex, or a factor of 2.2, more metal-rich. The relation is a key part of galaxy evolution because it ties how much gas a galaxy has to how much star formation and enrichment it has completed.

The module named Galaxy_Metallicity3_FromJCost in the framework's machine-checked library of formal theorems defines a cost function on a ratio of two real numbers, m and e. Its definition is domainCost(m, e) = Jcost(m / e), where Jcost is the framework's forced cost function. The file proves three facts: this cost is zero when m equals e, it is never negative when both inputs are positive, and a constant called phi minus 3/2 is positive. These are general properties of the cost function applied to any ratio; none of them mentions a galaxy, a metal, or a mass.

In Recognition Science, the framework models a discrete record of events, called a ledger, where each recognition event carries a forced cost. The framework's central theorem proves that any cost function satisfying five plain conditions must equal J(x) = (x + 1/x)/2 - 1. The galaxy module plugs a mass-to-enrichment ratio into that cost and checks basic sanity properties: the cost vanishes at equality, stays nonnegative for positive inputs, and a threshold constant is positive. The library's own docstring states plainly that this proves nothing specific to galaxies, because the module never defines what m and e mean in astronomical terms.

The research note attached to the module records where the idea was meant to go: a predicted scaling where Z/Z_sun equals phi^k at each mass rung, with a slope of 0.25 dex per log-mass decade, which is consistent with the observed 0.35 but not derived by the file. What the module actually establishes is a template: any subject that can define its own m and e can reuse these three proved facts. The galaxy relation itself remains a research note, not a theorem, until someone supplies definitions of mass and enrichment in the galaxy'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)

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

What this page does not claim

The module does not prove the mass-metallicity relation itself. The module does not define what m or e mean in astronomical terms. The framework does not derive the observed 0.35 slope in this file.

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/Astrophysics/Galaxy_Metallicity3_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: