Astrophysics Galaxy Sfr3 From Jcost Gal Sfr3 Cert

What the certificate proves

A star formation rate is how fast a galaxy turns gas into new stars, usually given in solar masses per year. Astronomers observe a rough relation called the galaxy main sequence: more massive galaxies form stars faster, with a power-law exponent near 0.7. The declaration GalSFR3Cert in the Recognition Science library sounds like it certifies a derivation of that exponent. It does not.

The certificate is a small machine-checked structure. It packages three general facts about a function called domainCost, which is defined for two real numbers m and e as J(m/e), where J is the framework's cost function. The three facts are: the cost is zero when the two inputs are equal; the cost is never negative when both inputs are positive; and a certain constant, phi minus 3/2, is positive. The structure is inhabited, meaning a certificate exists. All of this is proved in the framework's machine-checked library of formal theorems.

What the certificate does not do is connect those facts to galaxies. The letters m and e could stand for mass and something else, but the definition never says what they mean for a galaxy. The docstring records a research note where the author hoped the exponent 0.7 might emerge from the golden ratio phi, but the note is not a theorem. The Lean code proves nothing about star formation rates, the main sequence, or any astrophysical quantity.

In plain terms: the certificate is a true but empty shell. It establishes three properties of a cost function that happens to be named with astrophysical vocabulary. The actual derivation of a galaxy scaling law remains open. A reader should not take the name GalSFR3Cert as evidence that Recognition Science has explained the galaxy main sequence.

structure GalSFR3Cert 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 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 certificate derives the galaxy main sequence exponent. The certificate defines m and e in astrophysical terms. The certificate proves any specific property of star formation rates.

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