Pith. sign in
module module moderate

IndisputableMonolith.Astrophysics.AccretionDiskFromJCost

show as:
view Lean formalization →

This module applies the six-clause J-cost-on-ratio template to accretion disks. It defines the regime and certifies the required J-properties for that astrophysics domain. Recognition Science researchers building domain certificates from the master chain would cite it. The module consists of definitions that instantiate the imported CanonicalJBand structure with no internal proofs.

claimThe accretion disk certification asserts that the J-cost function on disk ratios satisfies $J(1)=0$, $J(x)\ge 0$ for $x>0$, and the remaining four clauses of the canonical band template.

background

The module resides in the Astrophysics domain and imports the CanonicalJBand template. That template supplies the reusable six-clause J-cost-on-ratio structure used for B-tier whole-science openings and the forty-something domain certificates. The clauses begin with matched-zero $J(1)=0$ and nonnegativity $J(x)\ge 0$ for $x>0$.

Sibling definitions include AccretionRegime, which parametrizes the conditions for applying J-cost to disk accretion, and AccretionDiskCert, which packages the full set of verified properties. The module follows the standard pattern for domain-specific instantiations of the J-band.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the accretion-disk instantiation of the J-cost band inside the Recognition Science master certificate chain. It contributes one of the domain certificates that assemble the full physics derivation from the forcing chain. No downstream theorems are listed yet.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (4)