{"id":"82ab85ee-5dfc-4775-b3e1-8abc16e213b9","hotkey":"5GeGrYFpMrNSh3Nwcx987zWz4cME9A9NbCkEbjBvv4uLUScV","public_credit":null,"verification_status":"VERIFIED","manual_review_status":"APPROVED","reward_status":"REWARDED","slug":"green29-green-29","task_id":"fc-379fc029-green29-green-29-3d9963bfe5-counterexample-v1","display_title":"Green's open problem 29","title_parts":{"collection":"greens_open_problems","collection_label":"Green's open problems","reference":"29","qualifier":null},"title":"Green29.green_29","statement":"True ↔\n  ∃ C c,\n    0 < C ∧\n      0 < c ∧\n        ∀ {G : Type u_1} [inst : Group G] [inst_1 : DecidableEq G] (K : ℝ) (A : Finset G),\n          1 ≤ K → IsApproximateSubgroup K ↑A → ∃ S ⊆ A, C * K ^ (-c) * ↑A.card ≤ ↑S.card ∧ S ^ 8 ⊆ A ^ 4","task_bundle_sha256":"sha256:d93f338e0bdc26070d21afb455b3b681858807cc1d51688dc30b40849a8cfed2","attribution":"conjectures.io","verified_at":"2026-08-06T14:18:46.274804Z","certified_at":"2026-08-06T19:55:00Z","bounty_amount_rao":2670866111580,"bounty_amount_usd":"1547.25","bounty_policy_version":"dynamic-age-v1","verifier_version":"validator-bcda2bde517b829a8b44ea2a387d78674f7e6495","sandbox_mode":"landrun+seccomp","report_available":true,"review":{"decision":"APPROVED","reason_code":"REVIEW_APPROVED","notes_public":"The proof refutes the uniform polynomial lower bound in Green29.green_29 using a concrete family with K = 3. For arbitrary proposed constants C, c > 0, it takes G = Multiplicative ℤ × H with H finite and sufficiently large, and A = ({-1, 1} × H) ∪ {(0, 1)}. It proves that A is a 3-approximate subgroup. Integer-coordinate bounds then show that any S ⊆ A satisfying S⁸ ⊆ A⁴ must have coordinate zero; because A has only the identity at that coordinate, |S| ≤ 1. Choosing H large enough gives C · 3⁻ᶜ · |A| > 1, contradicting the lower bound required by the conjecture. The production verifier confirmed the exact counterexample statement and task commitment, built both challenge and solution, accepted the proof with Lean's default kernel in the landrun+seccomp sandbox, and found only the permitted axioms propext, Quot.sound, and Classical.choice. The counterexample therefore establishes the negation of the published Green29 target and is approved for the bounty.","policy_version":"v1","decided_at":"2026-08-06T19:33:28.840009Z"},"solution_available":true}