Pith. sign in
module module high

IndisputableMonolith.Astrophysics.StellarAssembly

show as:
view Lean formalization →

StellarAssembly supplies the base recognition cost J_bit = ln φ along with StellarConfig and tick-partition helpers that weight stellar collapse by J-cost differences. Astrophysicists deriving mass-to-light ratios from recognition principles cite these definitions to eliminate external calibration. The module consists of direct definitions grounded in the golden-ratio lemmas imported from PhiSupport.

claim$J_{ m bit} = \\ln \\phi$, StellarConfig a record of recognition parameters, ml_from_cost_diff the map from cost differences to mass-to-light ratio, and tick_partition the decomposition into mass_ticks and light_ticks on the phi-ladder.

background

Recognition Science fixes the fundamental time quantum τ₀ = 1 tick. The imported PhiSupport.Lemmas establish φ² = φ + 1 and the fixed-point identity φ = 1 + 1/φ. This module defines the elementary ledger bit cost J_bit = ln φ, which quantifies the recognition cost per binary decision.

StellarConfig packages the parameters for recognition-weighted stellar assembly. Functions ml_from_cost_diff, mass_ticks, light_ticks and total_ticks implement the cost-weighted partition of stellar quantities onto the phi-ladder.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

These definitions supply the recognition-weighted collapse machinery that feeds the three parallel derivations of the stellar mass-to-light ratio in the parent Astrophysics module and its MassToLight submodule. They close the last external calibration step by grounding M/L directly in J-cost and phi-tiers.

scope and limits

used by (4)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (3)

Lean names referenced from this declaration's body.

declarations in this module (21)