pith. sign in
module module high

IndisputableMonolith.Astrophysics.ObservabilityLimits

show as:
view Lean formalization →

Module defines observability limits via quantities such as recognition length l_rec, coherence energy E_coh, and maximal mass M_max drawn from phi-tier structures. RS astrophysicists cite it when constraining observable stellar parameters from recognition costs. It consists entirely of definitions and imports from nucleosynthesis tiers, stellar assembly, and phi lemmas, with no internal proofs.

claimDefinitions of $J_{ m bit}$, $\phi = (1 + \sqrt{5})/2$, $E_{ m coh}$, $l_{ m rec}$, $F_{ m threshold}$, $V_{ m coherence}$, $M_{ m max}$, $J_{ m mass}$, $J_{ m light}$, $J_{ m total}$, optimal configuration, and the claim that the optimal ratio equals a power of $\phi$.

background

Recognition Science places physical quantities on discrete phi-tiers. The nucleosynthesis tiers module derives mass-to-light ratios from the phi-tier structure of nuclear densities and photon fluxes. The stellar assembly module derives the same ratio from the recognition cost differential between photon emission and mass storage during collapse.

This module imports those results together with the cost module, the constants module fixing the time quantum at one tick, and the phi support lemmas establishing $\phi^2 = \phi + 1$ and the fixed-point identity $\phi = 1 + 1/\phi$. Phi bounds supply algebraic inequalities confirming the value of $\phi$.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies the observability limits from $\lambda_{\rm rec}$ and $\tau_0$ constraints to the Astrophysics aggregator. It is imported by the MassToLight module to complete the unified derivation of the stellar mass-to-light ratio. The downstream documentation states that the module eliminates the last external calibration input via three parallel strategies.

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)