pith. sign in
module module moderate

IndisputableMonolith.Astrophysics.AccretionDiskFromJCost

show as:
view Lean formalization →

This module applies the six-clause J-cost band template to accretion disks. Researchers building Recognition Science derivations of astrophysical structures cite it within the domain certification chain. The module imports CanonicalJBand and instantiates its matched-zero and nonnegativity clauses for accretion regimes via sibling definitions and certificates.

claimThe module defines accretion regimes and certifies $J(1)=0$ together with $J(x)\geq 0$ for $x>0$ on ratios arising in accretion disks.

background

Recognition Science derives all physics from a single functional equation whose J-cost function satisfies the Recognition Composition Law. The upstream CanonicalJBand module supplies the reusable six-clause J-cost-on-ratio template used across the master cert chain; its doc-comment states that each domain cert proves matched-zero J(1)=0 and nonneg J(x)≥0 for x>0. This astrophysics module imports that template and introduces the sibling objects AccretionRegime, accretionRegimeCount, AccretionDiskCert and accretionDiskCert to instantiate the clauses for accretion disks.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies the astrophysics domain certification inside the master cert chain for B-tier whole-science openings and Plan v7 domain certs. It feeds the overall Recognition Science structure by extending the CanonicalJBand template to accretion disks, thereby linking the J-cost framework to observable astrophysical regimes.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (4)