accretion_efficiency
plain-language theorem explainer
The declaration fixes the accretion efficiency at the constant 0.1 for use in Recognition Science models of gamma-ray burst energies. Modelers computing total GRB output from accreted mass fractions cite this value directly. The definition is a one-line constant assignment with no computation or hypotheses.
Claim. The accretion efficiency is the real constant $0.1$.
background
This definition sits in the Gamma-Ray Bursts module of Recognition Science, tied to the paper RS_Gamma_Ray_Bursts.tex. The module imports Mathlib and JcostCore, placing the constant inside the cost-function framework that underlies mass and energy ladders. It supplies the numerical factor converting accreted mass to radiated energy in the subsequent grb_energy definition.
proof idea
The declaration is a direct constant assignment of 0.1 to the real type; no lemmas or tactics are applied.
why it matters
The constant is referenced by grb_energy, grb_energy_positive, and typical_grb_in_range, anchoring the energy scale for both long and short bursts. It supplies the concrete efficiency input required by the Recognition Science treatment of gamma-ray bursts while remaining consistent with the phi-ladder mass formulas and the eight-tick octave structure of the unified forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.