positiveIndepWitness
plain-language theorem explainer
Independence witness for the positivity claim over the golden-only ratio class: both golden roots obey r² = r + 1, yet φ > 0 while ψ < 0. Anyone citing the tri-universe classifier (all three ClaimClassification branches) depends on this certificate. The construction pairs the two roots with their admissibility lemmas and a short sign argument for ψ.
Claim. Over the three-claim golden-only universe, positivity of the scale ratio is independent: $\varphi=(1+\sqrt{5})/2$ is an admissible realization in which positivity holds, and the conjugate $\psi=(1-\sqrt{5})/2$ is an admissible realization in which positivity fails.
background
This module sits in Maximal Forcing Phase 4, which exercises the Selected branch honestly. The ambient class is golden-only ratios: real $r$ with $r^2 = r + 1$ and no sign restriction. Both roots of that quadratic live in the class: the expanding root $\varphi$ and the conjugate $\psi = (1-\sqrt{5})/2$.
An independence witness is a pair of admissible realizations that disagree on a named claim. Here the claim is positivity of the scale ratio. Upstream, phi_equation records $\varphi^2 = \varphi + 1$; a sibling lemma records the same identity for $\psi$. Claim classification then has three constructors: forced (holds in every admissible model), independent (witnessed disagreement), and selected (resolved by a named principle such as positivity).
The local point is that positivity itself is not forced over the golden-only class: $\varphi$ and $\psi$ split on the sign. That is exactly what this witness packages.
proof idea
Definitional construction of an IndependenceWitness structure. The yes-model is $\varphi$, the no-model is $\psi$. Admissibility of $\varphi$ is phi_equation; admissibility of $\psi$ is the sibling golden identity for the conjugate. The yes-side holds by the standard positivity of $\varphi$.
The no-side is a short real-arithmetic argument: assume $\psi > 0$, note $\sqrt{5} > 1$ via monotonicity of square root on $1 < 5$, unfold $\psi = (1-\sqrt{5})/2$ to get $\psi < 0$, and obtain the contradiction by linear arithmetic.
why it matters
Feeds triUniverse_classifier, the module's capstone certificate: over the golden-only class the trivial claim is forced, the $\varphi$-identity claim is selected by positivity, and the positivity claim itself is independent via $\varphi$ versus $\psi$. That classifier is the only place that uses every constructor of ClaimClassification in one theorem.
In the Recognition forcing picture this closes the third branch story. Forced claims (cost, $\varphi$, dimension, $\alpha$) and independent claims (mass yardstick) already appear elsewhere; here independence of positivity is exhibited explicitly so that selection-by-positivity is not a dead end. Adopting positivity as a tightening of the golden-only class promotes the $\varphi$ claim to forced, matching the drainage narrative in the module doc and the T6 landmark that $\varphi$ is the self-similar fixed point of the physical scale.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.