positiveClaim_independent
plain-language theorem explainer
Over golden-constraint ratios without positivity, the claim "0 < r" is independent: φ satisfies it and the conjugate root ψ does not. Anyone citing the maximal-forcing trichotomy needs this as the Independent witness. The proof exhibits the two roots and shows ψ < 0 by comparing √5 to 1.
Claim. The reality claim $C$ given by $0 < r$ is independent over the admissible class of real ratios satisfying the golden constraint $r^2 = r + 1$ (no positivity). Explicitly, there exist admissible $r_0, r_1$ with $C(r_0)$ and $\neg C(r_1)$.
background
Maximal forcing classifies reality claims over an admissible class into Forced, Selected, or Independent. Independent means two admissible realizations disagree on the claim: $\exists R_0,R_1\in\mathrm{Admissible}$ with $C(R_0)$ and $\neg C(R_1)$.
Here the class is golden-constraint ratios only: $r^2 = r + 1$, with no sign restriction. That class is strictly looser than the positive golden class used elsewhere for $\varphi$. The two real roots are $\varphi = (1+\sqrt{5})/2$ and its conjugate $\psi = (1-\sqrt{5})/2$. The claim under test is simply positivity: $0 < r$.
The module's job is to exercise the Independent branch honestly alongside Forced and Selected, so the classifier is not secretly degenerate.
proof idea
Witness independence by the pair $(\varphi,\psi)$. Both lie in the golden class: $\varphi^2=\varphi+1$ by phi_equation, and $\psi$ by psi_golden. Positivity holds at $\varphi$ by phi_pos. For the negative witness, assume $0 < \psi$ and derive a contradiction: $\sqrt{5} > \sqrt{1} = 1$ forces $\psi = (1-\sqrt{5})/2 < 0$, so linarith closes. The four conjuncts match the Independent existential package exactly.
why it matters
This is the Independent leg of all_three_branches_realized, which packages Forced (trivial claim), Selected ("$r=\varphi$" under positivity selection), and Independent (positivity itself) over the same golden-only class. That theorem's doc-comment states the point: the maximal-forcing machinery is complete and non-degenerate; the classifier is not secretly always-forced or always-independent.
In the broader RS picture, $\varphi$ is forced as the self-similar fixed point (T6) only after positivity is adopted. Over the looser golden class, positivity is not forced by the algebraic constraint alone, which is exactly what this lemma records. It is the clean counterweight to the Selected drainage path that tightens golden-only to positive-golden and promotes "$r=\varphi$" to Forced.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.