E_coh
plain-language theorem explainer
E_coh sets the coherence energy scale to φ^{-5} in RS-native units. Astrophysicists deriving observability limits for stellar systems cite it to fix the minimum flux threshold F_threshold ~ E_coh/τ_0. The definition is a direct assignment drawn from the phi-ladder scaling already fixed in the constants layer.
Claim. $E_ {coh} := φ^{-5}$ (RS-native units, with φ the golden ratio).
background
The Astrophysics.ObservabilityLimits module derives mass-to-light ratios from recognition constraints on stellar systems. Observable flux must satisfy F ≥ F_threshold ~ E_coh/τ_0, with mass assembly limited by coherence volume V ~ l_rec³. The module states that the optimal configuration minimizes total J-cost J_total = J_mass(M) + J_light(L) and yields M/L ∈ {φ^n : n ∈ [0,3]} with typical value ≈ φ. Upstream, l_rec is defined as Real.sqrt(1/Real.pi) (Planck scale in natural units), G as λ_rec² c³/(π ℏ), and tick as the fundamental time quantum τ_0 = 1/(8 J_bit).
proof idea
The declaration is a direct noncomputable definition that assigns the constant φ^{-5} with no lemmas or tactics applied.
why it matters
E_coh supplies the energy scale that fixes the recognition threshold inside the module's derivation of M/L ~ φ^n. It aligns with the RS-native ħ = φ^{-5} and supports the main geometric result M/L ∈ {φ^n : n ∈ [0,3]}. The definition closes one link in the chain from pure recognition constraints to observable stellar properties.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.