phi_pow_102_lo_pos
plain-language theorem explainer
The lower endpoint of the rational interval for φ^102 is shown to be positive. Interval arithmetic for high powers of the golden ratio in galactic time ratio bounds relies on this to keep all constructed intervals in the positive orthant. The proof is a direct reduction that applies the positivity lemma for φ^51 under the definition of positive interval multiplication.
Claim. Let $I_{51}$ be the interval for $φ^{51}$ whose lower endpoint is positive. Let $I_{102}$ be the interval obtained by the positive multiplication rule applied to $I_{51}$ with itself. Then the lower endpoint of $I_{102}$ satisfies $I_{102}.lo > 0$.
background
The Numerics.Interval.GalacticBounds module builds rational intervals to bound successive powers of the golden ratio φ for numerical verification of large ratios such as τ★/τ₀ ≈ 5.75e29. mulPos constructs the product interval by setting its lower bound to the product of the input lower bounds and its upper bound to the product of the input upper bounds, provided both inputs have positive lower bounds. The upstream lemma for φ^51 establishes positivity of its lower bound by direct norm_num evaluation after unfolding the interval definition.
proof idea
Unfold the definition of the φ^102 interval, which is built by applying mulPos to the φ^51 interval with itself, then invoke mul_pos on the two copies of the φ^51 lower-bound positivity result.
why it matters
This lemma supplies the positivity hypothesis required to construct the φ^140 interval and its own lower-bound positivity statement, which in turn support containment theorems for φ^140. It belongs to the chain of interval positivity results that underwrite numerical checks on the phi-ladder and related constants in Recognition Science, including the eight-tick octave and mass formulas of the form yardstick · φ^(rung-8+gap(Z)).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.