Weak compactness implies stationary reflection and Mahloness

Suppose, towards a contradiction, that S has no stationary initial segment at an uncountable regular rho<kappa. By F3 choose a club C of infinite strong-limit cardinals below kappa. Then A=S intersect C is a stationary set of infinite cardinals by F6. For each alpha<kappa, A intersect alpha satisfies F2's hypotheses: below kappa its initial segments are subsets of the assumed nonstationary S initial segments, and at any regular rho>=kappa it is bounded, hence nonstationary by F6. Thus every A intersect alpha admits a regressive injection.

At level alpha take all pairs (alpha,f), where f is an injective regressive function on A intersect alpha with values in alpha. This level is nonempty by step 1.1; at alpha=0 it contains the empty function. Its size is at most $2^{\mathrm{\mid }\alpha \times \alpha \mathrm{\mid }}<\kappa$ by F3 (the finite cases also satisfy the bound). Order nodes by restriction at earlier levels. Restrictions remain injective and regressive and have values in the earlier alpha because f(beta)<beta, so every node has the required full chain of predecessors. This is a kappa-tree. F1 supplies a cofinal branch whose union is a regressive injection on A. F4 makes some fibre stationary, whereas injectivity makes it have at most one element, impossible by F6. This contradiction proves reflection for every S. The argument retains F5 through its cited suppliers.

Let D be any club in kappa. It is stationary by F6, so step 2.1 gives an uncountable regular rho<kappa with D intersect rho stationary, hence unbounded in rho. Since D is closed and rho is a nonzero limit ordinal, rho belongs to D. Therefore every club meets the uncountable regular cardinals below kappa, proving Mahloness under F1's inherited definition. Finally intersect this stationary set with the strong-limit club C from F3. Every element of the intersection is uncountable, regular and strong limit, hence inaccessible, and the intersection is stationary by F6. This proves the last assertion.