pith. sign in
module module high

IndisputableMonolith.Astrophysics.StellarAssembly

show as:
view Lean formalization →

StellarAssembly defines the base recognition cost J_bit = ln φ along with StellarConfig and tick-partition functions that weight stellar mass and light by recognition cost differences. Astrophysicists deriving mass-to-light ratios from RS principles cite it as the entry point for the stellar-assembly strategy. The module consists entirely of definitions and elementary positivity lemmas with no tactic proofs.

claim$J_{bit} = ln φ$, StellarConfig as the type of stellar systems, ml_from_cost_diff as the mass-to-light map from cost differences, and the functions mass_ticks, light_ticks, total_ticks, tick_partition that assign discrete recognition ticks to mass and photon output.

background

Recognition Science builds all quantities from the J-cost functional equation and the golden-ratio fixed point φ. The module imports τ₀ = 1 tick from Constants, the Cost primitives, and the PhiSupport.Lemmas that record φ² = φ + 1 together with uniqueness of the positive root. It introduces J_bit as the elementary ledger bit cost ln φ, which becomes the scaling unit for recognition-weighted stellar collapse.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

StellarAssembly supplies the cost primitives required by the stellar-assembly strategy inside MassToLight and is imported by the central Astrophysics aggregator. It also supports the parallel nucleosynthesis-tier and observability-limit derivations by providing the shared J_bit and tick-partition objects. The module thereby removes the last external calibration step from the three independent M/L derivations.

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)