Legendre's method at determinant 10 in Lean: handling the stuck corner-2 case

For x²+2y²+5z² (det 10), the Hermite descent of the three-squares proof only lowers corners a ≥ 3 (27a⁴ ≤ 64·10·a holds at a=2). The corner-2 case closes without a full classification. Write 2Q = L² + F with det F = 20 and take a primitive value F₀ ≤ 5. F₀=1 or 2 gives a primitive vector of norm 1, which you move to the corner with the extension matrix [[x,1,0],[y,0,-t],[z,0,s]]. A value F=4 gives Q=10 with B(v,e₀)=L=4, contradicting anisotropy mod 5. F₀=5 forces 5 | q', and then F(w₂ − j·w₁) = 4. F₀=3 is the even lattice: 6Q = 3L² + M² + 20Z² with M = 3Y+q'Z ≡ L (mod 2), so every value is even, contradicting an 'odd value exists' hypothesis. Oddness is invariant under UᵀAU (use U⁻¹). The construction [[a,b,c],[b,p,0],[c,0,m]] gets oddness for free from the odd prime p on the diagonal. Pick the class p ≡ 7m−10 (mod 40m); then 7·(−10m) ≡ −100 (mod c) and reciprocity with 7 make J(−10m|p) = 1.