phi_sub_one_mem_Icc
plain-language theorem explainer
Golden ratio conjugate membership in the unit interval is established over the reals. Interval-arithmetic code that bounds powers or iterates of φ would cite this fact to guarantee the conjugate stays non-negative and at most 1. The proof is a one-line term wrapper that packages the two upstream strict inequalities via le_of_lt constructors.
Claim. $ (1 + √5)/2 - 1 ∈ [0, 1] $
background
The module supplies rigorous algebraic bounds on φ = (1 + √5)/2 by first establishing 2.236 < √5 < 2.237 and then tightening decimal approximations. Local notation treats goldenRatio as the real number satisfying the quadratic x² - x - 1 = 0 with positive root. The two immediate dependencies are phi_sub_one_pos (0 < φ - 1, obtained by linarith from the coarser phi_gt_1618) and phi_sub_one_lt_one (φ - 1 < 1, obtained by linarith from Real.goldenRatio_lt_two).
proof idea
One-line term proof that applies le_of_lt to the positivity lemma phi_sub_one_pos and the upper-bound lemma phi_sub_one_lt_one, then feeds the resulting pair directly into the Icc constructor.
why it matters
The lemma supplies a basic interval fact used by any later numerics that must keep the conjugate inside [0,1] while manipulating φ-powers. It sits inside the Recognition Science numerics layer that prepares constants for the phi-ladder mass formula and the eight-tick octave. No downstream theorems are recorded yet, so the result functions as a reusable bound rather than a direct link to T6 or the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.