 Fixed point of boxed negated provability

A formula provably equivalent to a boxed formula satisfies $F\to \square F$ in GL. The displayed fixed point then gives both $\square \square F$ and $\square \neg \square F$ under $F$, hence $\square \perp$. Boxed explosion proves the reverse implication. Under arithmetic realization this is a formal inconsistency statement; Sigma-1 soundness excludes its provability, while second incompleteness excludes provability of its negation.