positivitySelection
plain-language theorem explainer
Names the positivity selection principle on the golden-constraint class (no positivity): the physical scale ratio is the expanding root greater than one. The applicability witness is simply $0 < \varphi$. Anyone proving that "$r = \varphi$" is Selected (not Forced) over that class cites this package. It is a structure instance: a label string plus the applies proposition.
Claim. A named selection principle on the golden-constraint admissible set $\{ r \mid r^2 = r + 1 \}$ for the reality claim $r = \varphi$, with label "positivity: the physical scale ratio is the expanding ($> 1$) root" and applicability condition $0 < \varphi$.
background
This module exercises the third branch of the Maximal Forcing trichotomy. Forced and Independent are handled elsewhere; here the honest interim tag is Selected. The ambient class is the golden-constraint set of real ratios $r$ with $r^2 = r + 1$, deliberately without a positivity cut. That class is strictly looser than the golden-positive class, which also requires $0 < r$.
A selection principle is a named structure pairing a human-readable label with an applicability proposition, used when a claim is not forced on the current admissible set but is governed by an explicit extra principle. The claim in view is "$r = \varphi$" (the golden ratio). The conjugate root $\psi = (1-\sqrt{5})/2$ also satisfies the golden constraint and differs from $\varphi$, so the claim is not forced on the looser class.
Selected is defined as "not Forced, yet inhabited by some SelectionPrinciple." The present definition supplies that named principle: positivity, i.e. the physical scale ratio is the expanding root.
proof idea
Definitional structure instance, not a tactic proof. The SelectionPrinciple fields are filled directly: the label string records the positivity reading, and the applies field is the proposition $0 < \varphi$. No lemmas are invoked; the body is the two field assignments that witness the structure.
why it matters
Feeds the theorem that "$r = \varphi$" is Selected over the golden-only class: that result packages non-forcing with a nonempty selection principle whose witness is exactly this definition. The module doc stresses that Selected is not an endpoint. Adopting positivity as a tightening of the golden class promotes the claim to Forced (the standard forced-$\varphi$ result). Thus the third trichotomy branch is exercised honestly and then drained.
In the Recognition forcing chain this sits next to T6 ($\varphi$ as the self-similar fixed point): the algebraic golden constraint alone does not pick the expanding root; positivity is the named extra principle that does. The construction keeps the Selected tag from becoming a dumping ground for unresolved claims.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.