psi_ne_phi

This module exercises the Selected branch of maximal forcing. The class Lgolden collects real ratios obeying the golden constraint $r^2 = r + 1$ with no positivity requirement. Over that class both expanding and contracting roots are admissible, so equality to φ cannot be forced until a selection principle is named.

Locally, ψ is defined as $(1 - \sqrt{5})/2$, the contracting root. The gate-tightened class LphiGold further demands $0 < r$, which excludes ψ and recovers the unique positive root φ. Upstream, the GoldenInt spine also names a conjugate root as $1 - \varphi$ in the integer ring $\mathbb{Z}[\varphi]$; the real definition here is the same algebraic number on $\mathbb{R}$.

The module doc states the point bluntly: Selected is an honest interim tag, not a dead end, because positivity drains it to Forced.

Tactic proof in three steps. First, $\sqrt{5} > 0$ from Real.sqrt_pos and norm_num. Second, unfold the definitions of ψ and φ and apply linarith with that positivity fact to obtain the strict inequality ψ < φ. Third, discharge inequality by ne_of_lt. No external lemmas beyond the real-arithmetic library are required.

Parent use is isPhi_not_forced_over_Lgolden: if Forced held for the claim "r = φ" over Lgolden.admissible, then the admissible witness ψ would equal φ, contradicting this theorem. That non-forcing result is the first half of the Selected story; the second half is the named positivity principle, which tightens Lgolden to LphiGold and promotes the claim to Forced.

In the broader framework this is the concrete counterexample that keeps the Selected branch honest: T6 forces φ only after positivity (or an equivalent selection) is on the table. Without this inequality, the drainage Lgolden → LphiGold would be vacuous and Selected would collapse into Independent or Forced by accident.