phi_pow_16_interval
plain-language theorem explainer
This definition supplies the closed rational interval [2206.9, 2207.5] that contains the golden ratio raised to the 16th power. Numerics work in Recognition Science cites it when building enclosures for higher powers of φ that enter galactic ratio comparisons. The construction is a direct definition whose only proof obligation is a norm_num check that the lower endpoint does not exceed the upper.
Claim. Let $φ$ be the golden ratio. The closed interval $[22069/10, 22075/10]$ contains $φ^{16}$.
background
The module supplies interval arithmetic for the power function, relying on the identity $x^y = exp(y · log x)$ for positive $x$ or on direct multiplication for natural-number exponents. Interval is the structure carrying rational endpoints lo and hi together with the proof obligation lo ≤ hi. The present definition gives a concrete enclosure for the special case φ^16. It rests on the basic Interval structure declared in Numerics.Interval.Basic and on the parallel Interval type in Recognition.Certification.
proof idea
The definition is a one-line wrapper that directly records the rational endpoints 22069/10 and 22075/10 and discharges the validity obligation with the norm_num tactic.
why it matters
The interval is the base case for iterated multiplication that produces φ^32, φ^51, φ^102 and ultimately φ^140, all of which appear in the galactic-bounds theorems that compare these powers against the galactic ratio. It therefore supplies the numerical foundation for the phi-ladder constructions used throughout the Recognition framework. Downstream theorems such as phi_pow_140_lt_ratio and phi_pow_142_lt_ratio_1_3 unfold this definition to obtain the required strict inequalities.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.