phi_inv_pos
plain-language theorem explainer
Phi emergence derives the golden ratio from J-cost minimization in the Recognition framework. The theorem establishes that the reciprocal of phi is strictly positive. It is cited by convergence proofs for the geometric series of negative powers of phi and by positivity results for lexicon ratios. The proof is a one-line term application of one_div_pos.mpr to the already-established positivity of phi.
Claim. $1/phi > 0$
background
The PhiEmergence module derives the golden ratio phi as the self-similar fixed point of the J-cost functional under the Recognition Composition Law. Phi satisfies phi > 1 and is the unique positive solution to the fixed-point equation obtained from J-cost minimization. The upstream result in LexiconRatio states the equivalent claim 0 < phi_inv via direct application of div_pos to one_pos and Constants.phi_pos.
proof idea
The term proof obtains phi_pos by a have statement then applies one_div_pos.mpr to conclude positivity of the reciprocal.
why it matters
This result is invoked by phi_series_sum to justify convergence of the geometric series summing (1/phi)^(n+1) to phi, and by lexicon_ratio_pos together with phi_inv_unique in the linguistics module. It supplies the positivity needed for the phi-ladder and for the geometric-series step that supports the eight-tick octave (T7) in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.