`M_max`

definition

show as: view math explainer →

module: IndisputableMonolith.Astrophysics.ObservabilityLimits
domain: Astrophysics
line: 77 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Astrophysics.ObservabilityLimits on GitHub at line 77.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  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
 102/-! ## The Derived M/L Ratio -/
 103
 104/-- At the optimum, scale ratios are related by φ.
 105
 106The constraint that both mass assembly and light emission are
 107observable, combined with J-minimization, forces:

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.