Astrophysics Accretion Disk Stability3 From Jcost

Disk instability and the cost threshold

An accretion disk is a flat, rotating flow of gas falling toward a star or black hole. In the standard model by Shakura and Sunyaev, the disk's state depends on its surface density, the amount of material per unit area. Below a critical density the disk is cool and dim; above it, heating and ionization run away, producing an outburst. The threshold is not arbitrary: in the Recognition Science framework, the critical density is the value where the framework's cost function equals its value at the golden ratio φ ≈ 1.618.

The framework's cost function, cost, measures the price of a recognition event, a discrete record of a comparison. For any positive ratio x, the cost is J(x) = (x + 1/x)/2 - 1, a formula forced by five plain conditions. The function vanishes when the two compared quantities are equal, and it is always nonnegative. At the golden ratio, J(φ) equals φ - 3/2, a positive number about 0.118. The disk's critical surface density is the one that makes J(Σ/Σ_crit) equal to that same value.

The framework's machine-checked library of formal theorems proves three general facts about this cost function: it vanishes when the ratio is 1, it is nonnegative for positive inputs, and the threshold φ - 3/2 is positive. These are proved for any positive numbers m and e, with no reference to disks. The framework's own definition of the disk cost is just J(m/e), with m and e left unspecified.

In plain language, the framework establishes the arithmetic backbone of the instability criterion. It shows that the cost function has the right basic behavior to serve as a threshold detector: zero at balance, positive away from it, and a specific positive value at the golden ratio. What it does not do is connect m and e to any physical surface density. The research note in the framework records the intended application, an outburst threshold in X-ray novae at about φ times a baseline surface density, but that connection is not proved in the code. The gap is a definition of m and e in disk terms.

What this means for a reader is that the framework supplies a candidate shape for the instability threshold, and the machine-checked part guarantees the candidate has the right formal properties. The step from a general cost function to a real disk remains open. The framework is a template with the physics left as a research note, not a completed astrophysical derivation.

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 framework does not prove that any real accretion disk becomes unstable at the golden-ratio density. The framework does not define m and e in terms of surface density or any other disk quantity. The research note about the outburst threshold is not a proved result.

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