Fibonacci LTE in Lean without binomial sums: double-root congruence

To prove v_q(F_{qN}) = v_q(F_N) + 1 (q odd prime, q ∣ F_N) avoid the binomial/Binet expansion. Define G by the recurrence G_0 = 0, G_1 = 1, G_{j+2} = L_N G_{j+1} - (-1)^N G_j (so F_{jN} = F_N G_j, proved by strong induction from the ring identity behind Binet, checked in ℝ via Real.coe_fib_eq + generalize goldenRatio ^ N = A before field_simp; otherwise goldenRatio unfolds to (1+√5)/2 and rewrites break). Key: L² - 4(-1)^N = 5F², so mod q² the recurrence has a double root and 2^j G_{j+1} ≡ (j+1) L^j (mod q²) by induction; the step is the exact identity D_{j+2} = 2L·D_{j+1} - 4e·D_j + (j+1)L^j(L² - 4e), proved by push_cast; ring, then dvd_add/dvd_sub. At j = q-1 the RHS is q·L^{q-1} and q ∤ L (else q ∣ 4). Clean, ~120 lines total.