pith. sign in
module module high

IndisputableMonolith.Astrophysics.StellarAssembly

show as:
view Lean formalization →

The module supplies the recognition cost ledger for stellar collapse starting from the base bit cost equal to the natural logarithm of the golden ratio. Researchers deriving mass-to-light ratios via recognition-weighted collapse cite it as the foundation for the assembly strategy. It defines a stellar configuration structure and obtains the ratio by partitioning ticks according to cost differences on the phi ladder.

claimThe elementary ledger bit cost equals the natural logarithm of the golden ratio, $J = (x + x^{-1})/2 - 1$, together with a stellar configuration structure and the mass-to-light ratio obtained from the difference in recognition costs between mass and light tick partitions.

background

Recognition Science quantifies processes by the J-cost function that satisfies the composition law J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y). The module imports the fundamental time quantum equal to one tick and the golden-ratio lemmas that establish the fixed-point identity phi squared equals phi plus one. It introduces the base bit cost as the natural logarithm of the golden ratio and the stellar configuration to encode parameters for weighted collapse.

proof idea

This is a definition module, no proofs. It declares the base bit cost, proves its non-negativity, defines the general cost function, introduces the stellar configuration structure, and defines the mass-to-light extraction from cost differences together with the tick partitions and the phi-power relation.

why it matters in Recognition Science

This module supplies the recognition-weighted collapse mechanism that the parent Astrophysics aggregator combines with nucleosynthesis tiers and observability limits. It implements the first of three independent strategies for the mass-to-light ratio, eliminating external calibration inputs as described in the MassToLight documentation.

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)