Forcing is not monotone toward weaker conditions

For the formula $\check{p}\in \dot{G}$, a membership witness r in F1 must lie below one of the three displayed coefficients and force check p equal to that coefficient's check name. By F4, the entries with coefficients 1 and q cannot qualify. The entry with coefficient p qualifies exactly when $r\le p$. Since p is an atom, the full witness set is therefore precisely $\{p\}$.

This witness set is dense below p: the only condition below p is p itself. It is not dense below 1: q is below 1 and its only refinement is q, which is not p. Thus $p⊩\check{p}\in \dot{G}$ and $1⊮\check{p}\in \dot{G}$, despite $p\le 1$. The proposed persistence to weaker conditions is false.

F2 gives exactly the valid direction: if a condition forces a formula, every stronger condition does. The calculation uses neither the existence of a generic nor AC, and it distinguishes failure to force at 1 from forcing the negation at 1. In fact 1 cannot force that negation, since its extension p forces the formula.