IndisputableMonolith.Derivations.MassToLight
Module Derivations.MassToLight supplies the golden ratio φ together with auxiliary definitions for mass-to-light ratios expressed as powers of φ. Researchers constructing mass formulas on the phi-ladder cite these objects. The module contains only definitions and no theorems.
claimThe golden ratio satisfies $φ = (1 + √5)/2$. Mass-to-light ratios are realized as $φ^k$ for integer exponents k via the auxiliary maps phi_power and ml_is_phi_power.
background
The module sits in the Derivations domain and imports only Mathlib plus IndisputableMonolith.Constants. The upstream Constants module fixes the RS time quantum as τ₀ = 1 tick. Local definitions include phi, phi_power, phi_gt_one, phi_lt_two, ml_is_phi_power, cycleLength and massPhase, all built around the self-similar fixed point φ of the Recognition Composition Law.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
The module supplies the concrete φ and mass-to-light maps required by the mass formula yardstick · φ^(rung − 8 + gap(Z)). It therefore supports the phi-ladder constructions that appear after T6 in the forcing chain. No downstream declarations are recorded.
scope and limits
- Does not contain theorems or proofs.
- Does not import UnifiedForcingChain or J-cost definitions.
- Does not state the full mass formula or Berry threshold.
- Does not derive numerical bounds on α or G.
depends on (1)
declarations in this module (21)
-
structure
via -
def
phi -
def
phi_power -
lemma
phi_gt_one -
lemma
phi_lt_two -
lemma
phi_gt_1_6 -
lemma
phi_lt_1_7 -
theorem
phi_10_bounds -
theorem
phi_13_bounds -
theorem
ml_is_phi_power -
def
cycleLength -
def
massPhase -
def
lightPhase -
theorem
phase_ratio_from_topology -
theorem
ml_from_phase_ratio -
theorem
ml_consistent_with_observation -
theorem
ml_is_derived_not_input -
def
H_MLUncertaintyIsDiscrete -
theorem
ml_uncertainty_is_discrete -
def
H_MLFollowsPhiStructure -
theorem
ml_follows_phi_structure