ml_derivation_complete
plain-language theorem explainer
The mass-to-light ratio derivation certificate establishes that the derived M/L equals the golden ratio φ with the stellar-assembly, nucleosynthesis-tier and geometric-observability routes all returning the identical value and the result lying inside the observed interval. Stellar-population modelers would cite the result to replace empirical calibration with a ledger-derived constant. The proof is a term-mode refinement that invokes the three-strategies agreement theorem to discharge the equality conjuncts and directly supplies the range and φ
Claim. The derived mass-to-light ratio equals the golden ratio $φ$, the stellar-assembly, nucleosynthesis-tier and geometric-observability derivations each equal the derived ratio, the value lies in the open interval $(0.5,5)$, and there exists an integer $n∈{0,1,2,3}$ such that the derived ratio equals $φ^n$.
background
The module derives the stellar mass-to-light ratio from Recognition Science by three independent routes. Stellar assembly equates the ratio to exp(Δδ/J_bit) which collapses to a power of φ. Nucleosynthesis places nuclear and photon processes on discrete φ-tiers, again yielding φ^Δn. Geometric limits from recognition wavelength, coherence time and energy force the ratio onto the same φ-ladder. The upstream theorem three_strategies_agree proves that the three routes return identical values while ml_derived_value identifies the common result with Constants.phi. ml_derived itself is defined as Constants.phi.
proof idea
The term proof obtains the agreement hypothesis from three_strategies_agree. It refines the goal into the six conjuncts. The first conjunct is discharged by ml_derived_value. The next three equalities are obtained by rewriting with the components of the agreement hypothesis. The range conjunct is supplied directly by ml_in_observed_range. The final existential is witnessed by n=1 together with zpow_one and ml_derived_value.
why it matters
This theorem supplies the final certificate that the mass-to-light ratio is derived rather than calibrated, completing the zero-parameter status claim for Recognition Science. It assembles ml_derived_value and three_strategies_agree into a single statement that all astrophysical inputs are now internal to the framework. The result places M/L on the φ-ladder, consistent with the self-similar fixed point forced at T6 of the unified forcing chain and with the module's claim that no external calibration remains once the ledger structure is fixed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.