Astrophysics Observability Limits Ml Geometric Bounds

The geometric bound

The mass-to-light ratio M/L of a galaxy or star cluster is a number astronomers use to say how much mass shines for a given amount of light. A ratio of 1 means the system radiates like the Sun; a ratio of 10 means it is ten times darker than the Sun per unit mass. In the Recognition Science framework, the declaration ml_geometric_bounds is a proved theorem: it states that the geometric mass-to-light ratio, written ml_geometric, lies strictly between 1 and 2. The proof is a direct consequence of the definition, which sets ml_geometric equal to the golden ratio φ ≈ 1.618, and of two earlier theorems showing that φ is greater than 1 and less than 2. The result is machine-checked, meaning a computer verified every step from the definitions to the conclusion.

The golden ratio is the number that satisfies r² = r + 1, about 1.618. It appears throughout mathematics, from the pentagon to Fibonacci numbers. In the framework's library, the same number emerges from a cost-minimization argument: a stellar system is observable only if its photon flux exceeds a threshold, and its mass is limited by a coherence volume. Minimizing the total recognition cost under those constraints yields a ratio that is a power of φ. The theorem ml_geometric_bounds is the narrow, formal statement that the particular ratio chosen, φ itself, sits in the interval (1, 2). It does not say which power of φ a real galaxy has; it only bounds the base value.

What the theorem does not claim is as important as what it proves. It does not assert that any real galaxy has M/L exactly equal to 1.618. It does not say that the framework derives the observed mass-to-light ratios of real galaxies from first principles. The theorem is a statement about a definition: it establishes that the defined quantity falls in a certain range. The framework's own documentation notes that the value matches other strategies within the framework, but that is a consistency check, not an empirical prediction. The physical bridge, from the framework's recognition cost to actual stellar populations, remains a modeling choice, not a proved consequence.

/-- The geometric M/L matches observations -/
theorem ml_geometric_bounds : 1 < ml_geometric ∧ ml_geometric < 2 := by
  unfold ml_geometric φ
  constructor
  · exact Constants.one_lt_phi
  · exact Constants.phi_lt_two

/-- The M/L ratio from geometric constraints -/
noncomputable def ml_geometric : ℝ := φ

/-- Information content of mass vs light.

The ledger tracks:
- Mass events: I_mass = n_mass × J_bit information
- Light events: I_light = n_light × J_bit information

Conservation: I_mass + I_light = I_total

At equilibrium, the ratio n_mass/n_light = φ because φ is the
unique fixed point of the J-cost recursion. -/
theorem information_balance_gives_phi :
    ∃ (ratio : ℝ), ratio = φ ∧ ratio ^ 2 = ratio + 1 := by
  use φ
  constructor
  · rfl
  · unfold φ
    exact PhiSupport.phi_squared

What this page does not claim

This answer does not claim that any real galaxy has a mass-to-light ratio exactly equal to the golden ratio. This answer does not claim that the framework derives observed galaxy mass-to-light ratios from first principles. This answer does not claim that the theorem proves the physical observability constraints; those are modeled, not proved.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Astrophysics/ObservabilityLimits.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: