pith. sign in
module module moderate

IndisputableMonolith.Astrophysics.AccretionDiskFromJCost

show as:
view Lean formalization →

The module applies the reusable J-cost band template to define accretion regimes and certificates for astrophysical disks. Recognition Science researchers cite it when extending the master certification chain to the astrophysics domain. It consists of sibling definitions for regime classification and disk certification that instantiate the six-clause template without internal proofs.

claimAccretion disk certification holds when the J-cost on the disk ratio satisfies the matched-zero condition $J(1)=0$ and the nonnegativity condition $J(x)geq 0$ for $x>0$, together with the remaining four clauses of the Canonical J-Band template.

background

Recognition Science derives domain results from the J-functional equation via a reusable six-clause template. The upstream CanonicalJBand module supplies this template, which each domain cert must instantiate by proving matched-zero and nonnegativity on the relevant ratio. The present module sits inside the astrophysics domain and introduces the concrete objects AccretionRegime and AccretionDiskCert that carry the template into disk dynamics.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies one of the Plan v7 domain certs in the master certification chain. It feeds the B-tier whole-science openings by providing the astrophysics-specific instantiation of the J-cost band, allowing downstream results on accretion phenomena to inherit the six-clause guarantees.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (4)