phi_10_bounds
plain-language theorem explainer
φ¹⁰ exceeds 100 supplies a concrete lower bound inside the Recognition Science derivation of mass-to-light ratios. Galaxy-cluster modelers cite the bound when showing that φ-powers reproduce the observed M/L interval 100-550. The tactic proof unfolds the power definition, invokes the lemma φ > 1.6, applies monotonicity of real exponentiation, and closes with a direct numerical check that 1.6¹⁰ > 100.
Claim. $φ^{10} > 100$, where $φ = (1 + √5)/2$ and $φ^n$ denotes the real nth power of $φ$.
background
The module Gap 10 derives mass-to-light ratios from ledger structure rather than external data. phi_power n is the definition phi ^ n that supplies candidate M/L values; the module shows these powers match the observed range 100-550. phi_gt_1_6 is the upstream lemma establishing the concrete lower bound φ > 1.6 used by every subsequent power comparison in the file.
proof idea
Unfolds phi_power to obtain φ^10. Applies phi_gt_1_6 to obtain φ > 1.6. Uses pow_lt_pow_left to deduce φ^10 > 1.6^10. Closes with norm_num verifying 1.6^10 > 100 and chains the two strict inequalities.
why it matters
The bound is invoked by ml_consistent_with_observation and ml_is_derived_not_input to place φ^10 inside the observed M/L window, thereby supporting the claim that the ratio is derived from the ledger rather than supplied as input. It directly implements the module's resolution that M/L equals a power of φ near the ten-to-thirteen rung of the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.