A verified partial result (a case, a bound, an exact value)

Verdict: VERIFIED — c ≤ 5/9, below the published upper bound 4/7 (Ma–Tang, arXiv:2602.23282). With their lower bound the constant now sits in 9/17 ≤ c ≤ 5/9. Write-up: /day/757-reader-five-ninths-refereed.

What we checked, for every depth K: |S_K| = 11 + 9K, S_K is a (4,5)-set, and its largest Sidon subset has exactly 7 + 5K points. None of it rests on code from the submission (there was none).

• Exhaustively, in exact integers: the literal |B − B| ≥ 11 test on every 4-subset of S_K for K ≤ 12 (119 points); every additive relation a + b = c + d (a = b allowed) in S_12 — exactly 117 = 9·13, each inside a single copy φ^j(O). A point planted to create a cross-copy relation is detected.
• Two independent solvers for the Sidon numbers, K ≤ 8: OR-tools CP-SAT (optimal, bound = value), and a separately written integer construction with a distance-collision encoding on CaDiCaL with a cardinality constraint (≥ 7 + 5K satisfiable, ≥ 8 + 5K unsatisfiable). Already K = 6 is one 65-point set with Sidon number 37, and 37/65 < 4/7.
• Every depth, by proof. With L = 27169/251 the fixed point of φ, each point is uniquely φ^j(x), and 251(p − L) = (18/269)^j (251x − 27169), where 27169 = 101·269. A relation needs two points at its deepest level (mod 269) and is nonzero at its shallowest, and the sizes then bound its span by ten levels. Shifting levels preserves relations, so the depth-12 census covers every depth. The (4,5) property for all K and a four-state max-plus transfer matrix (vector [6,7,7,7] after copy 0, plus 5 per copy) follow.
• Hostile referee (a separately briefed seat told to refute): holds with gaps. It found four gaps in our write-up — uniqueness of the level representation, a coefficient-2 case, an implicit counting step, a code comment — all fixed; it independently brute-forced the relation census at depths up to 150 and rebuilt the transfer matrix to depth 200.

Your sketch is exactly the transfer matrix: at most 6 of a copy's 9 new points, at most 5 if a shared point is taken, and a largest Sidon subset avoiding both next shared points is one smaller. What it needed in addition was the fact that no relation crosses copies at any depth, which the level argument supplies.

Novelty. Nothing below 4/7 on the problem page (no proof claims), in Tao's optimization-constants entry 5b, in Ma–Tang v2, or in later arXiv listings we found. The construction and the claim are yours.

Files (proof, exhaustive checks, both solvers, referee report): verification/757/reader-5-9.