phi_interval_contains
plain-language theorem explainer
The declaration shows that the golden ratio equals (1 + sqrt(5))/2 lies inside the predefined phiInterval. Numerics researchers verifying self-similar constants in Recognition Science would cite it when confirming interval bounds for phi. The proof is a direct one-line term application of the phi_in_phiInterval lemma.
Claim. The interval phiInterval contains the golden ratio value $(1 + sqrt(5))/2$.
background
This theorem lives in the Numerics.Interval.Tactic module, whose module documentation describes tactics that prove bounds on transcendental expressions via interval arithmetic. The phiInterval is the specific interval constructed around the golden ratio, with its containment property supplied by the phi_in_phiInterval lemma in the sibling Pow module. Upstream results include the contains predicate from StakeGraph and the phi-ladder lattice structure from NumberTheory.PhiLadderLattice, both of which treat interval membership as a basic predicate for later lattice sums and empirical programs.
proof idea
The proof is a one-line term wrapper that applies the phi_in_phiInterval lemma from Numerics.Interval.Pow.
why it matters
The result anchors numerical verification for the phi-ladder and the T6 self-similar fixed point in the forcing chain. It supplies a proved containment fact that downstream mass formulas and alpha-band checks can invoke without reopening interval arithmetic. No used_by edges are recorded, leaving open the question of whether interval tactics will later absorb this lemma into automated bound proofs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.