udg_size
plain-language theorem explainer
The declaration supplies a representative effective radius for ultra-diffuse galaxies as the real number 5.0. Galaxy formation researchers working in the Recognition Science substrate model cite this constant when comparing predictions to observations of both DM-rich and DM-poor systems. The definition is a direct numerical assignment with no further computation or lemmas.
Claim. The effective radius $r_e$ of ultra-diffuse galaxies is defined as $5.0$ kpc.
background
The EA-011 module examines ultra-diffuse galaxies with surface brightness μ_V > 24 mag/arcsec² and sizes r_e ~ 1-10 kpc. Recognition Science models dark matter as the substrate, a ledger carrier distributed by recognition coherence rather than particles. High coherence regions yield DM-rich UDGs such as Dragonfly 44 while low coherence produces DM-poor cases such as NGC 1052-DF2. The ILG derivation fits rotation curves for both without additional dark matter adjustments.
proof idea
The definition is a direct constant assignment of the real number 5.0. No lemmas from the upstream results are applied.
why it matters
This definition anchors the size scale in the EA-011 RS analysis of ultra-diffuse galaxies. It supports the verdict that diversity arises naturally from spatially varying substrate coherence and connects to the ILG connection for rotation curves. The value fills the representative scale within the 1-10 kpc range cited in the module documentation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.