Astrophysics Mass To Light Ml Derived Value

The declared value

In astrophysics, the mass-to-light ratio (M/L) of a stellar population compares how much matter it holds to how much light it emits. A galaxy of old, dim stars has a high M/L; a region of young, bright stars has a low one. Observed values for stars and galaxies typically fall between 0.5 and 5 in solar units, where the Sun itself is 1 by definition.

Within the Recognition Science framework, a machine-checked library of formal theorems contains a declaration called ml_derived_value. The declaration proves, by definition, that the framework's derived mass-to-light ratio equals the golden ratio φ ≈ 1.618. The proof is a reflexivity step: the derived value is defined to be φ, so the theorem that they are equal is immediate. This is not a derivation from deeper principles; it is an identification.

The framework's documentation describes three strategies that are supposed to arrive at this same value independently: weighting by recognition cost, a tiered structure of nuclear and photon fluxes, and geometric observability limits. A hypothesis states that all three agree, but the convergence proof is marked NEEDS_DEFS, meaning it is not yet complete. The theorem ml_derived_value itself does not depend on those strategies; it only asserts the equality with φ.

What the declaration genuinely establishes is narrow. It proves the number φ lies strictly between 1 and 2, and therefore within the observed range [0.5, 5] solar units. It also proves that if an observed M/L falls outside that interval, it cannot equal the derived value. These are real, checkable facts, but they are bounds, not a measurement. The framework does not claim to have measured any star's M/L; it proposes a characteristic value and invites comparison.

The honest reading is this: the framework has chosen to define its characteristic M/L as the golden ratio, and has formally recorded that choice. The empirical question, whether real stellar populations cluster on the φ-ladder {1, 1.618, 2.618, 4.236}, remains open. The declaration makes that question precise, which is a useful service, but it does not answer it.

/-- **THEOREM (TRIVIAL)**: M/L matches φ by definition.

    This identifies the derived M/L value with the golden ratio.
    It is the *conclusion* of the three-strategy derivation chain. -/
theorem ml_derived_value : ml_derived = Constants.phi := rfl

/-- **HYPOTHESIS**: All three derivation strategies agree.

    STATUS: NEEDS_DEFS — Requires formalizing:
    - StellarAssembly.ml_stellar (J-cost weighting)
    - NucleosynthesisTiers.ml_nucleosynthesis (φ-tier structure)
    - ObservabilityLimits.ml_geometric (observability constraints)

    Each is defined in its respective module but the convergence proof
    is not yet complete.

    The hypothesis structure makes explicit what needs to be proven. -/
def H_ThreeStrategiesAgree : Prop :=
    StellarAssembly.ml_stellar = NucleosynthesisTiers.ml_nucleosynthesis ∧
    NucleosynthesisTiers.ml_nucleosynthesis = ObservabilityLimits.ml_geometric ∧
    ObservabilityLimits.ml_geometric = ml_derived

/-- **THEOREM (RIGOROUS)**: φ is strictly between 1 and 2. -/
theorem phi_bounds : 1 < φ ∧ φ < 2 := by
  constructor
  · -- 1 < φ: Since √5 > 1, we have (1 + √5)/2 > 1
    unfold φ Constants.phi
    have h_sqrt5_gt_1 : 1 < Real.sqrt 5 := by
      rw [show (1 : ℝ) = Real.sqrt 1 by norm_num]
      exact Real.sqrt_lt_sqrt (by norm_num) (by norm_num)
    linarith
  · -- φ < 2: Since √5 < 3, we have (1 + √5)/2 < 2
    unfold φ Constants.phi
    have h_sqrt5_lt_3 : Real.sqrt 5 < 3 := by
      rw [show (3 : ℝ) = Real.sqrt 9 by norm_num]
      exact Real.sqrt_lt_sqrt (by norm_num) (by norm_num)
    linarith

/-- **THEOREM (RIGOROUS)**: φ is in the observed range [0.5, 5] solar units.

    This proves the range property for the φ value itself. Once `ml_derived_value`
    is proven (showing ml_derived = φ), this immediately gives `ml_in_observed_range`. -/
theorem phi_in_observed_range : 0.5 < φ ∧ φ < 5 := by
  constructor
  · -- 0.5 < φ: Since φ = (1 + √5)/2 and √5 > 0, we have φ > 0.5
    unfold φ Constants.phi
    have h_sqrt5_pos : 0 < Real.sqrt 5 := Real.sqrt_pos.mpr (by norm_num : (5 : ℝ) > 0)
    linarith
  · -- φ < 5: Since φ = (1 + √5)/2 and √5 < 3, we have φ < 2 < 5
    unfold φ Constants.phi
    have h_sqrt5_lt_3 : Real.sqrt 5 < 3 := by
      rw [show (3 : ℝ) = Real.sqrt 9 by norm_num]
      exact Real.sqrt_lt_sqrt (by norm_num) (by norm_num)
    linarith

/-- **THEOREM (RIGOROUS)**: The M/L derivation is falsifiable -/
theorem ml_derivation_falsifiable :
    -- If observed M/L differs significantly from φ-ladder, theory is falsified
    (∀ obs : ℝ, obs ∉ Set.Icc 0.5 5 → obs ≠ ml_derived) ∧
    -- Specific prediction
    (ml_derived = φ) := by
  constructor
  · intro obs hobs h
    -- If obs = ml_derived, then obs ∈ [0.5, 5] by ml_in_observed_range
    rw [h] at hobs
    have ⟨h1, h2⟩ := ml_in_observed_range
    apply hobs
    exact ⟨le_of_lt h1, le_of_lt h2⟩
  · exact ml_derived_value

What this page does not claim

The declaration does not derive M/L from the cost function J or from the forcing chain. The declaration does not prove that any observed star has M/L = φ. The declaration does not establish zero-parameter status; that certificate is a scaffold hypothesis.

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/MassToLight.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: