Erdos 364: kernel-certified verification up to 10^14

The `erdos_364` statement (no three consecutive powerful numbers, `FormalConjectures/ErdosProblems/364.lean`) now has verified partial progress: Lean 4 proofs of the bounded forms

```lean
theorem no_powerful_triple_up_to_1e12 :
∀ n : ℕ, n + 2 ≤ 10^12 → ¬ (Powerful n ∧ Powerful (n+1) ∧ Powerful (n+2))

theorem no_powerful_triple_up_to_1e14 :
∀ n : ℕ, n + 2 ≤ 10^14 → ¬ (Powerful n ∧ Powerful (n+1) ∧ Powerful (n+2))
```

checked end to end by the kernel: axioms exactly `{propext, Classical.choice, Quot.sound}`, no `sorry`, no `native_decide`. The `Powerful` definition is carried byte-identically from this repository's `FormalConjecturesForMathlib/Data/Nat/Full.lean` (commit e923379e6 pinned), and the bridge file proves that `erdos_364` implies each bounded form, so the statements are literal finite fragments of the catalogued conjecture.

Code, proofs, and certificate records: https://github.com/ibrahimmian36/Optio

The proof enumerates the odd powerful numbers a^2 b^3 of each interval with a fueled kernel-computable generator, locates every pair at distance 2 by a verified sorted scan (3,524 chunk certificates across the two bounds), and kills each of the seven candidate middles (the A076445 members) with an explicit witness prime. For calibration: uncertified computations reach further (exhaustively to 10^22 via OEIS A060355's b-file; conditionally to ~7.38e28 via A076445 if that list is complete, which does not appear to be established). The contribution here is that everything below 10^14 is checked by a proof kernel rather than trusted code.

Would a small PR adding a reference note to the `erdos_364` docstring be welcome, and if so in what form? Happy to follow whatever convention you prefer for verified partial results.

Start with the erdos_364 statement and docstring in FormalConjectures/ErdosProblems/364.lean, then inspect nearby conjecture entries for the project's reference-note convention. If the maintainers approve the form, add a concise note describing the kernel-checked bounds through 10^14 and the external proof records; the Lean file should still parse without introducing proof changes.

Written by the indexing model from the issue text.