H_MLFollowsPhiStructure
plain-language theorem explainer
The declaration states that stellar mass-to-light ratios equal some integer power of the golden ratio φ. Galaxy formation modelers using Recognition Science would reference this when replacing empirical M/L inputs with ledger-derived values. It is introduced as a direct existential quantification over the exponent n in the phi_power definition. The statement encodes the hypothesis without deriving the specific power from the underlying cost function.
Claim. There exists an integer $n$ such that the derived mass-to-light ratio equals $phi^n$, where $phi$ is the golden ratio.
background
The module addresses Gap 10 by deriving the mass-to-light ratio from recognition cost weighting during stellar assembly rather than treating it as an external parameter. The phi_power definition supplies the candidate values directly as integer powers of φ. Upstream results supply the ledger L that conserves recognition events and the recognition structure M that partitions mass and light phases across the cycle.
proof idea
The definition is a direct encoding of the hypothesis as an existential statement over the integers. It asserts the existence of n such that the derived ratio matches the output of phi_power at that n. No additional lemmas or tactics are invoked beyond the phi_power helper itself.
why it matters
This definition supplies the formal hypothesis for the core prediction that M/L ratios follow the φ-structure in stellar assembly. It closes the derivation strategy in the module by linking recognition-weighted integration to the observed range φ^10 to φ^13. The result supports replacement of empirical constants with algebraic expressions in φ, consistent with the fixed point at T6 and the eight-tick octave. The open task is to derive the specific exponent from the stellar cost function.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.