Short-root neighbours of long roots in type F4

The integral span of the short-root weights detects every coroot. Together with the F4 length bounds, this supplies a descending-free root string through each long root.

theorem TauCeti.DynkinType.exists_f4_short_neighbor_of_long (α : Fin 48) (hα : f4Length α = 2) : ∃ (β : Fin 48) (γ : Fin 48), f4Length β = 1 ∧ RootPairing.pairing f4SimplyConnectedRootDatum β α = -1 ∧ f4SimplyConnectedRootDatum.root γ = f4SimplyConnectedRootDatum.root β + f4SimplyConnectedRootDatum.root α ∧ f4Length γ = 1 ∧ RootPairing.chainBotCoeff α β = 0

Every long F₄ root has a short neighbour one step away in a descending-free root string. Concretely, for a long root α there is a short root β with ⟨β, α∨⟩ = -1; then β + α is a short root and the root string through β in the α direction has bottom coefficient zero.