one_div_phi_lt

The module certifies that the ILG fractional exponent α and amplitude C are a priori predictions from self-similarity, not post-hoc SPARC fits. The derivation chain runs RCL → unique J-cost → φ as the self-similar scale ratio → memory kernel → α = (1 − 1/φ)/2 and C = φ⁻².

Here φ is the golden ratio (φ² = φ + 1), already forced in the Recognition chain (T6). The sibling lower bound φ > 1.61 is recorded as phi_gt_onePointSixOne. Inverting that inequality supplies a usable upper bound on 1/φ, which is the only numerical input needed to push α above a fixed decimal floor.

The locked exponent is α_Lock := (1 − 1/φ)/2. Bounding 1/φ from above immediately yields a strict lower bound on α_Lock, separating the prediction from later data comparison.

Start from the upstream lemma φ > 1.61 and positivity of φ. Because the map x ↦ 1/x is strictly decreasing on positives, Mathlib’s one_div_lt_one_div_of_lt gives 1/φ < 1/1.61. A one-line calc then finishes with norm_num: 1/1.61 < 0.622. No expansion of φ itself is required.

Feeds directly into alphaLock_gt, which proves α_Lock > 0.189 by rewriting α_Lock = (1 − 1/φ)/2 and applying this upper bound on 1/φ. That numerical floor is part of the a priori prediction certificate: the paper’s gap was that (A, α, r₀) looked free in SPARC fits; the module shows α is forced by self-similarity (φ-structure of the memory kernel) before any fit. The bound is a small but necessary decimal bridge between the exact algebraic form α = (1 − 1/φ)/2 ≈ 0.191 and the concrete inequality band used in the certificate. Framework landmarks: T6 (φ forced) and the ILG kernel step of the forcing chain.