Proposal U92: Lemma.erdos_366 (∃ n>0, Nat.Full 2 n ∧ Nat.Full 3 (n+1)) is existential, so one explicit n…

Hypothesis: Lemma.erdos_366 (∃ n>0, Nat.Full 2 n ∧ Nat.Full 3 (n+1)) is existential, so one explicit n settles it, with a Lean proof by norm_num/decide on primeFactors (Nat.Full k n = ∀ p ∈ n.primeFactors, p^k ∣ n, which I printed in T119). 3-full numbers are sparse: about $c{X}^{1/3}$ of them up to X, which is roughly ${10}^7$ below ${10}^{20}$. So enumerating m = n+1 over 3-full numbers and testing whether m−1 is powerful reaches far beyond naive search. No lab entry has searched this. Method: (1) C with __int128: enumerate the 3-full m ≤ X (X = 10^18, then 10^20 if time allows) recursively as products of p^e with e≥3. (2) For each m, test n=m−1 for powerfulness. First trial-divide by primes < 2000 and reject as soon as some prime divides exactly once, which removes almost all candidates. For survivors, the cofactor r must be powerful with all prime factors >2000: accept if r=1, or r is a perfect square or cube, or r = a^2 b^3 found via Pollard rho. (3) Validate on the known reverse pair (8 is 3-full, 9 is 2-full) and with brute force below 10^7. (4) On a hit, write the Lean proof: ⟨n, by norm_num, ...⟩ with explicit factorizations via Nat.primeFactors lemmas, then check_candidate. Otherwise post the verified bound to chat. Threshold 0. Threshold: 0 (must reach) Estimated cost: 60 min Why it's new: No notebook entry or chat message touches 366 (I checked N47, N54, N55, N57, N58 and the summary N75). This is a sparse-enumeration search on an existential statement, unlike the universal-statement searches in N54, N55 and N58. Related: N47, N54, N55, N58, N75