ml_is_derived_not_input

formal source

 218
 219/-! ## Main Theorem: M/L is Derived, Not Input -/
 220
 221theorem ml_is_derived_not_input :
 222    ∃ (derive : ℕ → ℤ → ℝ),
 223    (derive cycleLength = phi_power) ∧
 224    (∃ n : ℤ, derive cycleLength n > 100 ∧ derive cycleLength n < 550) := by
 225  use fun _ n => phi_power n
 226  constructor
 227  · rfl
 228  · use 10
 229    constructor
 230    · exact phi_10_bounds
 231    · exact lt_trans (by
 232        unfold phi_power
 233        apply zpow_lt_zpow_of_one_lt phi_gt_one (by norm_num)
 234      ) phi_13_bounds
 235
 236/-- **HYPOTHESIS**: Discrete uncertainty in M/L derivation.
 237
 238    STATUS: SCAFFOLD — The prediction that M/L uncertainty is discrete (following
 239    the φ-ladder) follows from the J-cost topology, but the formal proof
 240    that all intermediate values are unstable is a scaffold.
 241
 242    TODO: Formally prove the instability of non-φ-power M/L values. -/
 243def H_MLUncertaintyIsDiscrete (ML : ℝ) : Prop :=
 244  100 ≤ ML ∧ ML ≤ 550 →
 245    ∃ n : ℤ, n ∈ Set.Icc 10 13 ∧
 246    ML = phi_power n -- SCAFFOLD
 247
 248/-- The uncertainty in M/L is discrete. -/
 249theorem ml_uncertainty_is_discrete :
 250    ∀ ML : ℝ, 100 ≤ ML ∧ ML ≤ 550 →
 251    ∃ n : ℤ, n ∈ Set.Icc 10 13 := by