structure definition def or abbrev

`OptimalConfig`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  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:
 108  r_mass / r_light = φ^n for some integer n -/

depends on (14)

Lean names referenced from this declaration's body.

J_total in IndisputableMonolith.Astrophysics.ObservabilityLimits decl_use
scale in IndisputableMonolith.Cosmology.LargeScaleStructureFromRS decl_use
forces in IndisputableMonolith.Foundation.MagnitudeOfMismatch decl_use
Observable in IndisputableMonolith.Foundation.RecognitionForcing decl_use
for in IndisputableMonolith.Foundation.UniversalForcingSelfReference decl_use
Observable in IndisputableMonolith.Measurement.RSNative.Core decl_use
and in IndisputableMonolith.NumberTheory.CirclePhaseLift decl_use
that in IndisputableMonolith.NumberTheory.PhiLadderLattice decl_use
mass_pos in IndisputableMonolith.Physics.MesonSpectrumFromPhiLadder decl_use
Observable in IndisputableMonolith.Quantum.Observables decl_use
L in IndisputableMonolith.Recognition decl_use
M in IndisputableMonolith.Recognition decl_use
L in IndisputableMonolith.Recognition.Cycle3 decl_use
M in IndisputableMonolith.Recognition.Cycle3 decl_use