phi_lo_pos
The lemma establishes that the lower endpoint of the rational interval containing the golden ratio is strictly positive. Numerics constructing bounds for high powers of phi in galactic ratio estimates would cite this result to preserve positivity under multiplication. The proof is a one-line term that unfolds the explicit interval definition and normalizes the rational comparison.
claimLet $I$ be the closed rational interval with endpoints $1618/1000$ and $1619/1000$ containing the golden ratio $phi = (1 + sqrt{5})/2$. Then the lower endpoint satisfies $0 < I.lo$.
background
The module works with rational intervals to bound powers of the golden ratio when estimating the ratio of characteristic times $tau star / tau_0 approx 5.75e29$. An Interval is a structure carrying rational endpoints lo and hi with lo leq hi. The definition phiInterval fixes lo := 1618/1000 and hi := 1619/1000. Upstream the Certification.Interval supplies the corresponding real closed interval while Basic.Interval supplies the rational version used here. The UniversalForcingSelfReference.for structure records the meta-realization properties that situate these numerical bounds inside the self-reference axioms.
proof idea
The proof is a one-line term that unfolds phiInterval to expose the concrete rational lower bound 1618/1000 and then applies norm_num to discharge the inequality 0 < 1618/1000.
why it matters in Recognition Science
This positivity result is invoked directly to obtain the lower bound of phi_pow_38_interval via mulPos and to prove phi_pow_38_lo_pos; it likewise supports the containment argument in phi_pow_140_in_interval. It anchors the phi-ladder numerics that follow from the self-similar fixed point T6. The module doc ties the construction to the large galactic time ratio, consistent with the eight-tick octave and D=3 spatial dimensions of the forcing chain.
scope and limits
- Does not verify that the interval contains the exact algebraic value of phi.
- Does not supply bounds for arbitrary real exponents.
- Does not translate the rational interval into physical units or constants.
- Does not address interval validity under the full forcing chain T0-T8.
formal statement (Lean)
30lemma phi_lo_pos : (0 : ℚ) < phiInterval.lo := by
proof body
Term-mode proof.
31 unfold phiInterval; norm_num
32
33/-- Interval for φ^32 = (φ^16)^2 -/