def
definition
F_threshold
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Astrophysics.ObservabilityLimits on GitHub at line 71.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
68/-! ## Observability Constraints -/
69
70/-- Observability threshold: minimum flux for recognition -/
71noncomputable def F_threshold : ℝ := E_coh / τ_0
72
73/-- Coherence volume: maximum assembly volume -/
74noncomputable def V_coherence : ℝ := l_rec ^ 3
75
76/-- Maximum mass from coherent assembly in N cycles -/
77noncomputable def M_max (N : ℕ) (ρ : ℝ) : ℝ := ρ * V_coherence * N
78
79/-! ## J-Cost Optimization -/
80
81/-- The J-cost for mass configuration at scale ratio r -/
82noncomputable def J_mass (r : ℝ) : ℝ := Cost.Jcost r
83
84/-- The J-cost for luminosity configuration at scale ratio r -/
85noncomputable def J_light (r : ℝ) : ℝ := Cost.Jcost r
86
87/-- Total J-cost for stellar configuration -/
88noncomputable def J_total (r_m r_L : ℝ) : ℝ := J_mass r_m + J_light r_L
89
90/-- Optimal configurations minimize J_total subject to observability -/
91structure OptimalConfig where
92 r_mass : ℝ
93 r_light : ℝ
94 mass_pos : 0 < r_mass
95 light_pos : 0 < r_light
96 /-- Observable: flux exceeds threshold -/
97 observable : True -- Simplified constraint
98 /-- Optimal: minimizes J_total -/
99 optimal : ∀ r_m r_L : ℝ, 0 < r_m → 0 < r_L →
100 J_total r_mass r_light ≤ J_total r_m r_L
101