Astrophysics Observability Limits Agrees With Nucleosynthesis

The common mass-to-light ratio

The mass-to-light ratio, usually written M/L, is a basic way to describe a star system: how many solar masses of material it holds for every solar luminosity it puts out. A high ratio means a dim, heavy system; a low one means a bright, light one. In the Recognition Science framework, two separate derivations, one from how stars assemble and one from the sequence of nuclear fusion stages, each arrive at the same value for this ratio. The declaration agrees_with_nucleosynthesis is the machine-checked statement that these two numbers are equal: the ratio from the observability derivation is exactly the ratio from the nucleosynthesis derivation.

That shared value is the golden ratio, φ, approximately 1.618. The observability derivation starts from a simple constraint: for a system to be visible at all, its photon flux must exceed a threshold set by the framework's fundamental tick, and its mass must fit within a coherence volume. Minimizing the total recognition cost under those constraints yields a ratio that is a power of φ. The nucleosynthesis derivation, by contrast, arrives at the same φ from the tiers of fusion burning. The theorem ml_from_geometry_only packages the result: there exists a mass-to-light ratio equal to φ, greater than 1 and less than 5, that matches both derivations.

This agreement is a consistency result within the framework, not a measurement. It proves that two different paths, one geometric and one nuclear, point to the same number. It does not claim that real galaxies all have M/L equal to 1.618. Observed mass-to-light ratios vary widely with galaxy type, from less than one in some blue star-forming regions to tens in dark-matter-dominated ellipticals. The framework's φ is a characteristic value from its internal derivations, not a universal constant of observed astrophysics.

The declaration also does not claim that the framework derives the observed distribution of mass-to-light ratios, nor that it explains dark matter. The theorem's own bounds are loose, only requiring the ratio to lie between 1 and 5. What the declaration establishes is narrower and precise: within the framework's own models, the mass-to-light ratio that emerges from observability limits is the same as the one that emerges from nucleosynthesis tiers, and that common value is the golden ratio.

/-- The geometric M/L agrees with nucleosynthesis M/L -/
theorem agrees_with_nucleosynthesis :
    ml_geometric = NucleosynthesisTiers.ml_nucleosynthesis := by
  unfold ml_geometric φ
  rw [NucleosynthesisTiers.ml_nucleosynthesis_eq_phi]
  rfl

theorem ml_geometric_is_phi : ml_geometric = φ := rfl

/-- **Main Theorem**: The stellar M/L ratio is derived from geometric
observability constraints (l_rec, τ_0, E_coh) via J-cost minimization.

This provides a third independent derivation agreeing with Strategies 1 and 2. -/
theorem ml_from_geometry_only :
    ∃ (ml : ℝ),
    ml = φ ∧
    1 < ml ∧ ml < 5 ∧
    ml = StellarAssembly.ml_stellar ∧
    ml = NucleosynthesisTiers.ml_nucleosynthesis := by
  use ml_geometric
  refine ⟨rfl, ?_, ?_, agrees_with_stellar_assembly, agrees_with_nucleosynthesis⟩
  · exact ml_geometric_bounds.1
  · linarith [ml_geometric_bounds.2]

What this page does not claim

Real galaxies all have mass-to-light ratio exactly equal to the golden ratio. The framework derives the observed distribution of mass-to-light ratios across galaxy types. The framework explains dark matter or the discrepancy between its characteristic ratio and observed values.

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: