Petty’s Conjecture Holds in Lₚ for 2 ≤ p ≤ 4: d+1 Equidistant Points in Every Dimension d

We prove Petty's conjecture for all finite-dimensional real \(L_p\) subspaces with \(2\le p\le4\). Every \(d\)-dimensional real linear subspace of \(L_p\), over any measure space, contains \(d+1\) equidistant points. More strongly, every equilateral subset extends to exactly \(d+1\) points, preserving its original points and common distance. Every equilateral set is affinely independent, so every maximal equilateral set has cardinality \(d+1\). This extends the \(2\le p\le4\) case of Kusner's conjecture from coordinate spaces to arbitrary subspaces and complements the constructions of linear excess for every fixed \(p>4\). The proof combines conditional positivity of the powered distance kernel, a circumradius estimate, and Brouwer's fixed-point theorem. The main theorems are formalised in Lean.