phi_pow_145_in_interval
plain-language theorem explainer
The theorem establishes that φ^145 lies inside the interval obtained by multiplying the intervals for φ^140 and φ^5 under positive lower bounds. Numerics researchers bounding the galactic ratio τ★/τ₀ in Recognition Science would cite it to extend the phi-ladder containments. The proof reduces the exponent via the real power addition identity and applies the multiplication lemma for positive intervals.
Claim. Let $I_{140}$ and $I_5$ be the intervals containing $φ^{140}$ and $φ^5$ with positive lower bounds. Let $I_{145}$ be the product interval $mulPos(I_{140}, I_5)$. Then $φ^{145} ∈ I_{145}$.
background
In the GalacticBounds module, intervals bound successive powers of the golden ratio φ to support ratio comparisons without direct high-exponent evaluation. The contains predicate holds when a real x satisfies lo ≤ x ≤ hi. The mulPos operation builds the product interval only when both input intervals have positive lower bounds, and mulPos_contains_mul transfers containment to the product under those conditions.
proof idea
The proof obtains the containment hypotheses for the 140 and 5 cases from prior theorems. It rewrites φ^145 as φ^140 · φ^5 via the real exponent addition rule (valid for positive base). It then applies mulPos_contains_mul using the positivity lemmas for the lower bounds of both intervals.
why it matters
This containment feeds directly into ratio_lt_phi_pow_145, which establishes galactic_ratio < φ^145 and thereby anchors the numerical bound τ★/τ₀ ≈ 5.75e29 inside the phi-ladder. It closes one link in the Recognition Science numerics that ultimately supports the derivation of D = 3 and the alpha band from the functional equation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.