positiveClaim
plain-language theorem explainer
Packages the positivity assertion "0 < r" as a RealityClaim on real scale ratios. Cited by anyone checking the Independent branch of the maximal-forcing trichotomy over the golden-only class (no positivity built in). Definitional: a one-line structure instance whose holds predicate is strict positivity.
Claim. The reality claim on $r \in \mathbb{R}$ with audit label $\"0 < r\"$ and holding predicate $r \mapsto (0 < r)$.
background
A RealityClaim is a pair of audit-facing label and a predicate holds on realizations. Here the realization type is $\mathbb{R}$, standing for candidate scale ratios.
The ambient module studies the third trichotomy branch Selected over the golden-only admissible class: ratios obeying $r^2 = r + 1$ with no positivity requirement. Both the golden ratio $\varphi = (1+\sqrt{5})/2$ and its conjugate $\psi = (1-\sqrt{5})/2$ satisfy that algebraic constraint, so "$r = \varphi$" is not forced. Positivity is the named selection principle that picks the expanding root.
This claim is the Independent counterpart in the same class: $\varphi$ satisfies $0 < r$ while $\psi$ does not, so the predicate is neither forced nor selected over golden-only admissibility.
proof idea
Pure definitional packaging. The structure fields are filled by the string label "0 < r" and the predicate fun r => 0 < r. No lemmas or tactics.
why it matters
Supplies the Independent leg of the completeness theorem all_three_branches_realized: one Forced claim, one Selected claim (isPhi under positivity selection), and this Independent claim, all over the same golden-only class. That theorem's doc states the point: the classifier is non-degenerate, not secretly always-forced or always-independent.
Downstream, positiveClaim_independent builds the two-model witness ($\varphi$ yes, $\psi$ no), positiveIndepWitness packages the same pair for triUniverse, and triUniverse itself lists this claim among its three branch exemplars. In the broader maximal-forcing story, Selected is not a dead end: tightening Lgolden by positivity promotes isPhi to Forced. This definition is the contrasting Independent specimen that keeps the trichotomy honest.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.