tighten_Lgolden_LphiGold
plain-language theorem explainer
The positive golden-ratio class is a tightening of the golden-constraint class without positivity: every positive golden ratio is golden. Anyone tracking Selected-to-Forced drainage of "r = φ" cites this witness. The subset field projects out the positivity conjunct; the strictness witness is simply True.
Claim. The class of positive real ratios $r$ with $r^2 = r + 1$ is a tightening of the class of all real ratios satisfying the same golden constraint (no sign restriction): every positive golden ratio is golden, and the inclusion carries a strictness witness.
background
This module exercises the Selected branch of maximal forcing. Over the golden-constraint class without positivity, "r = φ" is not forced (the conjugate root ψ is an admissible counterexample), yet a named selection principle (positivity) resolves it. Selected is interim: adopting positivity as a tightening promotes the claim to Forced.
An admissibility class packages a set of admissible realizations with a label. Here Lgolden is ratios satisfying the golden constraint $r^2 = r + 1$ with no sign cut; LphiGold is the gate-tightened class of positive ratios with the same constraint (PhiAdmissible).
A Tightening from A to B is a structure with a subset field (every B-admissible realization is A-admissible) and an optional strictness witness Prop, so the core order stays usable when strictness is not yet proved.
proof idea
Definitional construction of a Tightening record. The subset field is a one-line intro: given r admissible for the positive golden class, project the second conjunct of that membership (the golden constraint) to land in the looser golden-only class. The strict_witness field is filled with True, recording that the inclusion is intended as strict without a separate proof obligation at this site.
why it matters
This is the explicit drainage arrow Lgolden → LphiGold that the module exists to exhibit. Downstream, positivity_promotes_selected_to_forced packages three facts: isPhi is Selected over the golden-only class, this tightening is nonempty, and isPhi is Forced over the positive golden class (forced_isPhi). The doc-comment there states the point: "Selected is not an endpoint... this Selected entry has a proved resolution, not a perpetual hold."
In the broader framework this sits next to T6 (φ forced as the self-similar fixed point). The golden constraint alone leaves a two-root ambiguity; positivity selects the expanding root > 1 and restores Forced status. Without this witness the Selected tag would be a dead end rather than a named, dischargeable interim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.