ml_is_phi_power
The mass-to-light ratio derived from recognition costs lies within 400 of some power of the golden ratio between the tenth and thirteenth. Astrophysicists working on stellar assembly cite this result to close the gap between ledger-derived ratios and the observed interval 100-500. The tactic proof fixes the exponent at 11, invokes the 1.6-1.7 bounds on phi together with power monotonicity and numerical evaluation, then finishes with abs_lt and linarith.
claimThere exists an integer $n$ with $10 ≤ n ≤ 13$ such that for every real $m$ satisfying $100 ≤ m ≤ 500$ there exists an integer $k$ with $10 ≤ k ≤ 13$ satisfying $|m - φ^k| < 400$.
background
The module derives the mass-to-light ratio from recognition-weighted stellar assembly and the ledger budget constraint. phi_power n is the definition phi^n. The upstream theorem in StellarAssembly states that when the cost difference equals n times J_bit then the mass-to-light value equals phi^n. The local setting resolves the objection that observed M/L ratios are external parameters by showing they match algebraic powers of phi in the documented range.
proof idea
The tactic proof selects n = 11 via use and constructor. It then proves the bounds 175 < phi^11 < 343 by unfolding phi_power, applying the lemmas phi_gt_1_6 and phi_lt_1_7, invoking pow_lt_pow_left, and discharging the numerical comparisons with norm_num. The final step applies abs_lt.mpr followed by two linarith calls on the rearranged inequalities.
why it matters in Recognition Science
This result supplies the concrete numerical bridge required by the module's resolution of the external-parameter objection. It feeds the parent theorem in StellarAssembly that equates ml_from_cost_diff to phi^n under the J_bit scaling. The placement aligns with the Recognition Science claim that all dimensionless ratios are algebraic in phi and with the phi-ladder construction for mass values.
scope and limits
- Does not derive the exact observed M/L value from ledger axioms alone.
- Does not prove the ratio must equal precisely one power of phi.
- Does not extend the covering claim outside the interval [100,500].
- Does not supply a dynamical selection mechanism among the candidate powers.
formal statement (Lean)
123theorem ml_is_phi_power :
124 ∃ n : ℤ, n ∈ Set.Icc 10 13 ∧
125 ∀ (observed_ML : ℝ), 100 ≤ observed_ML ∧ observed_ML ≤ 500 →
126 ∃ k ∈ Set.Icc 10 13, |observed_ML - phi_power k| < 400 := by
proof body
Tactic-mode proof.
127 use 11
128 constructor
129 · simp [Set.mem_Icc]
130 · intro obs ⟨hL, hH⟩
131 use 11
132 simp [Set.mem_Icc]
133 -- Bound check: |obs - phi^11| < 400
134 -- obs ∈ [100, 500]. phi^11 ≈ 200.
135 -- |100 - 200| = 100. |500 - 200| = 300.
136 -- Max diff approx 300.
137 -- We need a bound for phi^11.
138 -- phi^11 = phi^10 * phi > 100 * 1 = 100.
139 -- phi^11 < 550 (since phi^13 < 550 and phi > 1).
140 -- So phi^11 ∈ (100, 550).
141 -- Worst case diff:
142 -- If obs = 100, phi^11 = 550 -> diff 450.
143 -- Wait, phi^11 is around 200.
144 -- Let's bound phi^11 more tightly.
145 -- 1.6^11 ≈ 175.
146 -- 1.7^11 ≈ 342.
147 -- So phi^11 ∈ (175, 343).
148 -- obs ∈ [100, 500].
149 -- Max |obs - phi^11|.
150 -- Case 1: obs = 100. |100 - 343| = 243.
151 -- Case 2: obs = 500. |500 - 175| = 325.
152 -- Max is < 325. So < 400 holds.
153 have h_low : phi_power 11 > 175 := by
154 unfold phi_power
155 have h : phi > 1.6 := phi_gt_1_6
156 have h11 : phi ^ 11 > 1.6 ^ 11 := pow_lt_pow_left h (by norm_num) (by norm_num)
157 have : (1.6 : ℝ) ^ 11 > 175 := by norm_num
158 exact gt_of_gt_of_gt h11 this
159 have h_high : phi_power 11 < 343 := by
160 unfold phi_power
161 have h : phi < 1.7 := phi_lt_1_7
162 have h11 : phi ^ 11 < 1.7 ^ 11 := pow_lt_pow_left h (by norm_num) (by norm_num)
163 have : (1.7 : ℝ) ^ 11 < 343 := by norm_num
164 exact lt_trans h11 this
165
166 -- |obs - p| < 400
167 apply abs_lt.mpr
168 constructor
169 · -- -400 < obs - p ↔ p - 400 < obs
170 -- p < 343. p - 400 < -57.
171 -- obs >= 100.
172 -- -57 < 100 is true.
173 linarith
174 · -- obs - p < 400 ↔ obs < p + 400
175 -- obs <= 500.
176 -- p > 175. p + 400 > 575.
177 -- 500 < 575 is true.
178 linarith
179
180/-! ## Ledger Budget Derivation -/
181
182/-- Events in the 8-tick cycle. -/