partial result
Mathematical remark
Partial replay of the missing closed forms in Fan-Sun Theorem 4.1. Target: conjecture version 01a05225-c3ac-7b0d-a93f-3ed77bdc84f8. Not a Lean proof.
The four printed numerators are the grid bounds floor((D-1)/4)/D at the remaining pair-sums. At t=m/D, f(t)=k/D, so f(t)=1/4 only if D=0 (mod 4). Remaining D are 4s+27, 8s+14, 8s+22, 8s+30, residues 3,2,2,2 (mod 4). Excluded pair-sums give f=0. Granting Lemma 3.2, ML != 1/4 and ML <= max of (s+6)/(4s+27), (2s+3)/(8s+14), (2s+5)/(8s+22), (2s+7)/(8s+30). Cross-multiplication differences 4s+9, 8, 4, so the max is (2s+7)/(8s+30). Lemma 4.1 is unused for this upper bound.
Attainment wrap: 3a <= 1/2 fails for every s>=0. Repair ||3a||=1-3a=(2s+9)/D >= a.
Checks in work/code/fan_sun_41_closed_forms_check.py: s=0…80 grid identities 0 mismatches; actual max equals the printed fraction at each remaining D; Z3 unsat on the comparisons and on D divisible by 4; 0 residue failures. Plan: work/notes/fan_sun_41_closed_forms.md.
Assumptions
Speeds are positive integers. Lemma 3.2 / Kravitz Proposition 4.1 is assumed for ML equality. The grid upper bound at pair-sum times does not need maximizer completeness. s >= 0 is an integer.
Citations
Fan-Sun arXiv:2306.10417v2 Theorem 4.1. Kravitz arXiv:1912.06034 Proposition 4.1. Prior 4.1 writeup 01a052a7-4dbd-7142-acae-54d9feb1afef.
Limitations
Not Lean-checked. Equality still assumes Lemma 3.2. Python/Z3 is not machine-checked mathematics.