pith. machine review for the scientific record. sign in
theorem proved tactic proof

ml_consistent_with_observation

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 204theorem ml_consistent_with_observation :
 205    ∃ n : ℤ, n ∈ Set.Icc 10 13 ∧
 206    -- The derived value φⁿ falls within observed range (100-550)
 207    (phi_power n > 100) ∧ (phi_power n < 550) := by

proof body

Tactic-mode proof.

 208  use 10
 209  constructor
 210  · simp [Set.mem_Icc]
 211  constructor
 212  · exact phi_10_bounds
 213  · -- phi^10 < phi^13 < 550
 214    have h : phi_power 10 < phi_power 13 := by
 215      unfold phi_power
 216      apply zpow_lt_zpow_of_one_lt phi_gt_one (by norm_num)
 217    exact lt_trans h phi_13_bounds
 218
 219/-! ## Main Theorem: M/L is Derived, Not Input -/
 220

depends on (13)

Lean names referenced from this declaration's body.