phi_pow_140_lo_pos
plain-language theorem explainer
This lemma proves that the lower endpoint of the rational interval for φ^140 is strictly positive. Researchers constructing high-power golden-ratio bounds for galactic time ratios would cite it when extending the phi-ladder. The proof is a direct one-line reduction that applies the positive-interval multiplication rule to already-established lower-bound positivity results for the factors φ^102 and φ^38.
Claim. Let $I_{140}$ be the interval obtained by multiplying the intervals for $φ^{102}$ and $φ^{38}$ via the positive-multiplication operation. Then the lower endpoint of $I_{140}$ satisfies $I_{140}.lo > 0$.
background
The module supplies rational-interval approximations to high powers of the golden ratio φ to bound galactic-scale ratios τ★ / τ₀ ≈ 5.75e29. An Interval is a closed rational interval with lower endpoint lo and upper endpoint hi satisfying lo ≤ hi. The mulPos operation returns the product interval whose lower bound is the product of the input lower bounds (and likewise for the upper bounds) whenever both inputs have positive lower bounds. Upstream lemmas already establish that the lower bounds of the φ^102 interval (itself the product of two φ^51 intervals) and the φ^38 interval (product of φ^37 and φ) are positive.
proof idea
Unfold the definition of the φ^140 interval (which applies mulPos to the φ^102 and φ^38 intervals) and invoke the mul_pos lemma on the lower-bound positivity results for those two factors.
why it matters
The positivity result is required to define the intervals for φ^142 = φ^140 × φ^2 and φ^145 = φ^140 × φ^5 and to prove that those intervals contain the corresponding real powers of the golden ratio. It supports the phi-ladder numerics that feed the Recognition Science forcing chain (T5–T8), where φ is the self-similar fixed point and high powers appear in mass formulas and the eight-tick octave. No open scaffolding questions are closed by this lemma.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.