phi_beats_2
plain-language theorem explainer
The golden ratio satisfies J(φ) < J(2) for the Recognition Science cost J on positive ratios. Researchers certifying ALEXIS Experiment A predictions cite this to establish that φ-spaced pulse intervals incur strictly lower per-step cost than uniform spacing at ratio 2. The short term proof rewrites both sides to squared form, reduces the inequality via division rules, and closes it with numerical bounds on φ together with the identity φ² = φ + 1.
Claim. $J(φ) < J(2)$ where $J(x) = (x-1)^2/(2x)$ for $x > 0$.
background
The module certifies predictions for ALEXIS Experiment A, which compares φ-spaced pulse timings τ_k = τ₀ · φ^k against uniform intervals of constant length. The J-cost function is introduced in the Cost module as the squared-ratio expression J(x) = (x-1)^2/(2x), which equals the Recognition Science form (x + x^{-1})/2 - 1. The golden ratio φ is supplied by the Constants module together with the bounds 1.61 < φ < 1.62 and the quadratic identity φ² = φ + 1. Upstream results include the lemma that rewrites Jcost in squared form and the cellular-automata step definition that supplies the broader locality context for pulse sequences.
proof idea
The proof is a short term-mode sequence. It first rewrites both Jcost φ and Jcost 2 using the squared-form lemma Jcost_eq_sq. It then applies div_lt_div_iff₀ to convert the target inequality into a polynomial comparison. Finally nlinarith closes the goal using the supplied bounds φ > 1.61, φ < 1.62 and the identity φ² = φ + 1.
why it matters
This inequality is packaged directly into the PhiVsUniformCert structure that records the Experiment A prediction. It supplies the concrete comparison J(φ) < J(2) required to argue that φ-spaced intervals outperform uniform spacing among geometric sequences, thereby supporting the claim that φ minimises J among ratios > 1 of comparable scale. The result sits inside the T5 J-uniqueness step of the forcing chain and feeds the downstream certification that the φ-ladder reduces boundary J-cost relative to uniform spacing.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.