phi_power
Powers of the golden ratio φ supply the candidate mass-to-light ratios in Recognition Science stellar assembly. Galaxy cluster modelers cite this definition when replacing empirical M/L inputs with values derived from recognition cost minimization on the φ-ladder. The declaration is a direct one-line definition that raises φ to an integer exponent.
claimLet φ denote the golden ratio. For each integer n define the real number φ^n.
background
The Mass-to-Light module derives the mass-to-light ratio from the recognition ledger via recognition-weighted stellar assembly rather than treating it as external data. The module states that observed M/L ≈100-500 matches φ^10 ≈123 to φ^13≈521, with three strategies (recognition cost weighting, ledger budget constraint, curvature partition) all yielding powers of φ. This rests on the forcing chain in which φ is the self-similar fixed point (T6) and on the recognition composition law that forces all dimensionless ratios to be algebraic in φ.
proof idea
The declaration is a one-line definition that directly sets phi_power n to the real number obtained by raising phi to the integer power n.
why it matters in Recognition Science
This definition supplies the algebraic form required by downstream results H_MLFollowsPhiStructure, H_MLUncertaintyIsDiscrete, ml_is_phi_power and ml_is_derived_not_input. It closes the gap between recognition cost weighting and galaxy cluster observations by providing the explicit φ-ladder values. In the framework it instantiates the claim that all dimensionless ratios are algebraic in φ, consistent with the eight-tick octave and the derivation of D=3.
scope and limits
- Does not derive the specific integer exponent n from the stellar cost function.
- Does not prove that non-power-of-φ values are unstable under recognition dynamics.
- Does not address continuous distributions or non-integer exponents for M/L.
Lean usage
theorem phi_10_bounds : phi_power 10 > 100 := by unfold phi_power; exact (phi_gt_1_6_pow_10_gt_100)formal statement (Lean)
60noncomputable def phi_power (n : ℤ) : ℝ := phi ^ n
proof body
Definition body.
61
62/-! ## Geometric Bounds Helper -/
63