module module high

`IndisputableMonolith.Astrophysics.ObservabilityLimits`

This module defines observability limits in Recognition Science astrophysics through quantities such as the recognition length and coherence volume derived from the phi-ladder. Astrophysicists modeling detectable stellar masses or photon fluxes from first principles would cite these bounds to constrain observable scales. The module assembles definitions from imported cost functions, golden-ratio lemmas, and time-quantum constants with no internal proofs.

claimObservability limits are given by the recognition length $l_{rec}$, threshold flux $F_{threshold}$, coherence volume $V_{coherence}$, and maximum mass $M_{max}$ on the phi-ladder, all constrained by the time quantum $tau_0 = 1$ tick and golden ratio $phi$.

background

Recognition Science treats physical quantities as occupying discrete phi-tiers, with the golden ratio satisfying $phi^2 = phi + 1$ and fixed-point identity $phi = 1 + 1/phi$ as established in PhiSupport.Lemmas. The fundamental time quantum is $tau_0 = 1$ tick from Constants, while PhiBounds supplies algebraic inequalities confirming $phi = (1 + sqrt(5))/2$. Cost supplies the recognition cost function used to weight emission versus storage. This module sits inside the astrophysics derivations that also cover stellar assembly via recognition-weighted collapse and phi-tier nucleosynthesis.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

This module supplies the observability limits from lambda_rec and tau_0 constraints to the Astrophysics aggregator and the MassToLight unified certificate. It completes the set of three parallel M/L strategies by adding detectable-scale bounds, eliminating external calibration inputs for cosmic structures.

scope and limits

Does not derive numerical values for specific observed objects.
Does not incorporate general-relativity corrections to the limits.
Does not address dark-matter or non-RS physics components.
Does not compare predictions against telescope data sets.

used by (2)

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

IndisputableMonolith.Astrophysics module_import
IndisputableMonolith.Astrophysics.MassToLight module_import

depends on (6)

Lean names referenced from this declaration's body.

IndisputableMonolith.Astrophysics.NucleosynthesisTiers module_import
IndisputableMonolith.Astrophysics.StellarAssembly module_import
IndisputableMonolith.Constants module_import
IndisputableMonolith.Cost module_import
IndisputableMonolith.Numerics.Interval.PhiBounds module_import
IndisputableMonolith.PhiSupport.Lemmas module_import

declarations in this module (21)

def J_bit L52
theorem phi_eq_goldenRatio L55
def E_coh L59
def l_rec L66
def F_threshold L71
def V_coherence L74
def M_max L77
def J_mass L82
def J_light L85
def J_total L88
structure OptimalConfig L91
theorem optimal_ratio_is_phi_power L109
def ml_geometric L115
theorem ml_geometric_is_phi L117
theorem ml_geometric_bounds L120
theorem information_balance_gives_phi L138
theorem imf_from_j_minimization L152
theorem agrees_with_stellar_assembly L172
theorem agrees_with_nucleosynthesis L179
theorem ml_from_geometry_only L191
theorem ml_zero_parameter_certificate L213