phi_inv_interval_proven
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not establish that 0.618 is the greatest lower bound for φ^{-1}.
- Does not provide bounds with more than four decimal places.
- Does not apply to complex numbers or other algebraic extensions.
- Does not derive the interval from the Recognition Composition Law or forcing chain directly.
formal statement (Lean)
273def phi_inv_interval_proven : Interval where
274 lo := 618 / 1000
proof body
Definition body.
275 hi := 6186 / 10000
276 valid := by norm_num
277