phi_bound_upper
plain-language theorem explainer
Golden ratio upper bound by 1.618034 supports interval arithmetic in Recognition numerics. Researchers handling phi-ladder calculations or decimal closures in forcing-chain proofs would invoke it to anchor numerical steps. The proof reduces to a single num_ineq tactic that accepts the standard decimal expansion of the golden ratio.
Claim. $ (1 + sqrt(5))/2 <= 1.618034 $
background
The IntervalProofs module supplies minimal helpers that convert small numerical inequalities into Lean proofs while avoiding heavy dependencies, relying instead on norm_num together with monotonicity. This lemma supplies one concrete upper bound on the golden ratio, the self-similar fixed point that appears throughout the Recognition framework. It sits downstream of the meta-realization structure for, which records structural properties required by orbit and step coherence axioms, and of the spacetime interval definition that sums eta-weighted squared components over four dimensions.
proof idea
The proof is a one-line wrapper that applies the num_ineq tactic. The tactic internally invokes norm_num to verify the decimal inequality against the known approximation of the golden ratio.
why it matters
The bound anchors numerical work involving phi, the fixed point forced at step T6 of the unified forcing chain. It closes a small decimal gap inside the numerics layer so that interval arguments can proceed without external libraries. No downstream theorems are recorded, indicating the lemma functions as a leaf utility rather than a parent result.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.