In $\textit{Set Theory}$ by Jech 1978 edition, in the proof of Lemma 32.5 which you can hopefully see at the google book link

http://books.google.com/books?id=pLxq0myANiEC&pg=PA389&lpg=PA389&dq=weakly+compact+less+than+measurable&source=bl&ots=0DjaJGx_1D&sig=Av3IvVVUAkmQgUly0jNqbGN5Pz4&hl=en&sa=X&ei=fcADU-L4JIyBogTwwoGAAg&ved=0CCwQ6AEwAA#v=onepage&q=weakly%20compact%20less%20than%20measurable&f=false

In the course of the proof using the tree property, he produces from any weakly compact cardinal $\kappa$ a non principal $L_\alpha$-ultrafilter $U$ on $\kappa$, which is $L_\alpha$-$\kappa$ complete, and moreover the intersection of $\kappa$ many elements of $U$ (taken in $V$) is nonempty.

The latter implies that countable intersection (taken in $V$) is nonempty. This fact implies iterability for example by 19.13 of Kanamori. So $L_\alpha$ with this ultrafilter can be iterated of length $\text{Ord}$

However, $0^\sharp$ follows from the existence of a mouse (iterable premouse). But $0^\sharp$ has stronger consistency strength than a weakly compact.

Is this $(L_\alpha, U)$ not a pre-mouse? I have found varying definition of pre-mouse. One definition has the addition condition that $\kappa$ should be the largest cardinal of $L_\alpha$. This seems like it may not hold since at the beginning of the proof, the proof chooses an $\alpha$ such that $L_\alpha \models ZF^-$.

I would like to have the $\text{Ord}$ length iteration for what I am trying to do; however, I am troubled by whether or not this would give an iterable premouse and hence imply sharps.

Thanks for any clarification you can provide.

In $\textit{Set Theory}$ by Jech 1978 edition, in the proof of Lemma 32.5 which you can hopefully see at the Google book link.

In the course of the proof using the tree property, he produces from any weakly compact cardinal $\kappa$ a non principal $L_\alpha$-ultrafilter $U$ on $\kappa$, which is $L_\alpha$-$\kappa$ complete, and moreover the intersection of $\kappa$ many elements of $U$ (taken in $V$) is nonempty.

The latter implies that countable intersection (taken in $V$) is nonempty. This fact implies iterability for example by 19.13 of Kanamori. So $L_\alpha$ with this ultrafilter can be iterated of length $\text{Ord}$

However, $0^\sharp$ follows from the existence of a mouse (iterable premouse). But $0^\sharp$ has stronger consistency strength than a weakly compact.

Is this $(L_\alpha, U)$ not a pre-mouse? I have found varying definition of pre-mouse. One definition has the addition condition that $\kappa$ should be the largest cardinal of $L_\alpha$. This seems like it may not hold since at the beginning of the proof, the proof chooses an $\alpha$ such that $L_\alpha \models ZF^-$.

I would like to have the $\text{Ord}$ length iteration for what I am trying to do; however, I am troubled by whether or not this would give an iterable premouse and hence imply sharps.

Thanks for any clarification you can provide.