ErdosProblems/349: (3/2, 2) is not a good pair (mod-3 obstruction)

[cepadugato]

Summary

Stacked on #4233 (its commits are included). Adds one further fully-proven partial result on the open Erdős Problem 349 — the negative companion of dyadic_two_isGoodPair:

@[category research solved, AMS 11]
theorem three_halves_two_not_isGoodPair : ¬ IsGoodPair (3/2) 2

Every term of ⌊(3/2)·2ⁿ⌋ = 1, 3, 6, 12, 24, … except the first is a multiple of 3, and the first is 1 — so every subset sum is ≡ 0 or 1 (mod 3), and the infinitely many integers ≡ 2 (mod 3) are never reached. Together with dyadic_two_isGoodPair this pins the α = 2 fiber on both sides around the dyadic coefficients.

Honesty notes

• The open problem remains open: answer(sorry) and all pre-existing statements are untouched (pure addition, +61 lines on top of ErdosProblems/349: integer characterization and dyadic fiber (partial results) #4233, 0 deletions).
• The full characterization of the α = 2 fiber over real t (good iff t = 2⁻ᵏ, cf. W. van Doorn, arXiv:2602.23394, Prop. 2 — mind the n-indexing offset) needs real-parameter machinery and is not claimed here.

Verification

• Builds under the repo toolchain (Lean v4.27.0): lake env lean FormalConjectures/ErdosProblems/349.lean → exit 0; only the pre-existing open statements emit sorry warnings.
• #print axioms Erdos349.three_halves_two_not_isGoodPair → [propext, Classical.choice, Quot.sound] (no sorryAx, no native_decide).

🤖 Generated with Claude Code

[github-actions]

👋 This is an automated welcome message. 🤖
Thanks for the contributions!

A few friendly reminders while the review gets started:

• Please take a look at the style guidelines,
  especially the conventions for references, categories, AMS tags, and answer(sorry).
• You can manage some PR labels by leaving a comment with +label-name or -label-name; for example, +awaiting-author or -awaiting-author.
• This repository is mainly for formalised statements. Proofs longer than about 25-50 lines are usually out of scope; longer proofs are welcome to be included/linked via the formal_proof mechanism.

Thanks again for helping improve Formal Conjectures.

[mo271]

thanks, LGTM only one nit:

most (all?) of those should be marked category textbook or possibly category test:
for instance the fact exists_finset_sum_two_pow that one can write numbers in binary expansion is rather textbook than research solved