pith. sign in
module module moderate

IndisputableMonolith.Astrophysics.ObservabilityLimits

show as:
view Lean formalization →

This module defines observability limits for Recognition Science astrophysics via quantities such as recognition length l_rec, coherence energy E_coh, and J-cost thresholds built on the golden ratio. Astrophysicists cite it when bounding stellar parameters from RS first principles without external inputs. It is a definitions module that assembles imported lemmas from phi support, nucleosynthesis tiers, and stellar assembly into concrete RS-native objects.

claim$l_{rec}$, $E_{coh}$, $F_{threshold}$, $V_{coherence}$, $M_{max}$, $J_{mass}$, $J_{light}$, $J_{total}$ and the optimal ratio on the phi-ladder, with $J_{bit}$ and $E_{coh}$ expressed via the J-cost function and golden ratio bounds.

background

Recognition Science places physical quantities on discrete phi-tiers, as stated in the NucleosynthesisTiers module: 'physical quantities occupy discrete φ-tiers'. StellarAssembly derives M/L from the recognition cost differential during collapse. Constants fixes the RS time quantum τ₀ = 1 tick. PhiSupport.Lemmas supplies the identities φ² = φ + 1 and the fixed-point property φ = 1 + 1/φ. PhiBounds gives algebraic bounds on φ = (1 + √5)/2. The Cost module supplies the underlying J-cost function.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

This module feeds the Astrophysics aggregator and the MassToLight derivation. It supplies the observability limits from λ_rec and τ0 constraints that complete the unified M/L certificate, eliminating external calibration. The downstream MassToLight doc-comment notes the three parallel strategies that rely on these limits.

scope and limits

used by (2)

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

depends on (6)

Lean names referenced from this declaration's body.

declarations in this module (21)