phiInterval
plain-language theorem explainer
phiInterval supplies the rational interval [1.618, 1.619] that contains the golden ratio φ. Numerics code throughout the Recognition framework cites it to obtain rigorous bounds on powers of φ without floating-point error. The definition is a direct record construction whose only proof obligation is discharged by norm_num.
Claim. Let $I$ be the closed interval with rational endpoints $1618/1000$ and $1619/1000$. Then $I$ contains the golden ratio $φ = (1 + √5)/2$.
background
The Numerics.Interval.Pow module supplies interval arithmetic for the power function via the identity $x^y = exp(y · log x)$ for $x > 0$, with a special direct path for natural-number exponents. Interval is the basic structure imported from Numerics.Interval.Basic: a record with fields lo : ℚ, hi : ℚ and valid : lo ≤ hi. The same Interval type appears in Recognition.Certification for certification purposes. Upstream results supply the Interval record and several empirical-program and ledger structures that rely on interval bounds for numerical verification.
proof idea
Direct definition of the Interval record. The lower and upper bounds are written as rational literals 1618/1000 and 1619/1000; the single proof obligation valid : lo ≤ hi is discharged by the norm_num tactic.
why it matters
phiInterval is the root interval for every phi_pow_n_interval definition in GalacticBounds (phi_pow_2_interval, phi_pow_140_in_interval, phi_pow_142_lt_ratio_1_3, etc.). Those bounds in turn certify inequalities involving galactic ratios and high powers of φ, anchoring the numerical side of the phi-ladder (T6) and the eight-tick octave (T7). It closes a scaffolding gap between the abstract Recognition Composition Law and concrete power estimates used in mechanism-design and simplicial-ledger modules.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.