phi_inv_interval_proven
plain-language theorem explainer
phi_inv_interval_proven supplies a closed rational interval proven to contain the reciprocal of the golden ratio. Researchers establishing numerical enclosures for φ in Recognition Science would reference this when certifying bounds without relying on approximate arithmetic. The definition constructs the structure directly and discharges the ordering constraint with a single norm_num call on rationals.
Claim. The closed interval $[618/1000, 6186/10000]$ on the rationals, equipped with the proof that its lower endpoint does not exceed its upper endpoint.
background
The module develops rigorous algebraic bounds for the golden ratio φ = (1 + √5)/2 and its reciprocal. It proceeds by establishing integer bounds on √5 via squaring, such as 2.236² < 5 < 2.237², then deriving corresponding bounds on φ and 1/φ. An Interval is a structure consisting of rational lower and upper bounds together with a proof that the lower bound is at most the upper bound. This construction appears in both the Basic numerics module and the Certification module, where it serves as a decidable enclosure for real quantities.
proof idea
The declaration is a direct definition of the Interval structure. The only non-trivial field is the validity proof lo ≤ hi, which is supplied by the norm_num tactic. This tactic performs the arithmetic verification that 618/1000 ≤ 6186/10000 by reducing to integer multiplication and comparison.
why it matters
This interval definition is invoked by the theorem that confirms φ^{-1} lies inside it, thereby contributing to the collection of proven bounds on the golden ratio. In the Recognition Science framework it supports the identification of phi as the self-similar fixed point (T6) and the eight-tick octave structure (T7). It closes a numerical certification step that can be used in downstream proofs involving constants expressed in RS-native units.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.