phi_pow_142_in_interval
plain-language theorem explainer
Golden ratio to the 142nd power lies inside a precomputed interval. Galactic timescale work in Recognition Science cites the containment to anchor the ratio τ★/τ₀ at phi-ladder rung 142. The proof obtains the 140th-power containment, verifies the square case from the identity φ² = φ + 1 via interval addition, rewrites the exponent as a product, and closes with the positive-multiplication lemma.
Claim. Let $I_{142}$ be the interval constructed for the 142nd power of the golden ratio. Then $I_{142}$ contains $φ^{142}$, where $φ$ is the golden ratio satisfying $φ^2 = φ + 1$.
background
The module supplies numerical interval bounds for the galactic timescale ratio τ★/τ₀ ≈ 5.75 × 10^{29}. Interval containment is the predicate lo ≤ x ≤ hi. Upstream lemmas include add_contains_add, which lifts separate containments to the sum interval, contains_point for singleton intervals, and mulPos_contains_mul, which requires positive lower bounds on both intervals and lifts containments to the product. The 140th-power containment is already established by a prior sibling result in the same module.
proof idea
The tactic proof first imports the 140th-power containment. It separately builds the 2nd-power containment by unfolding the interval definition, rewriting φ² via the golden-ratio square identity, and applying add_contains_add to the known containment of φ together with the point interval at 1. It rewrites the 142nd power as the product of the 140th and 2nd powers using the real exponent-addition rule for positive bases. It finishes by invoking mulPos_contains_mul on the two positive lower-bound facts and the two containments.
why it matters
The containment supplies the numerical anchor at exponent 142 for the theorem tau_star_is_phi_rung, which asserts an integer rung N such that the galactic ratio lies within 0.1 of the corresponding phi-rung time. It completes a verification step inside the galactic-bounds numerics that feeds the Recognition Science derivation of galactic dynamics from the forcing chain, specifically the self-similar fixed point φ (T6) and the phi-ladder mass and time formulas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.