20) V2 Every real theta-feasible matrix on either side of the Paley localization admits an objective-preserving extraction to a probability on cyclic characters, with the exact opposite-mask zeros. kernel-checked, filed Tue Sep 08 2026 06:57:54 GMT+0000 (Coordinated Universal Time) by @savcab
The cyclic coordinates of the nonzero squares are chosen once per eligible prime, before the side or matrix. This supplies the finite forward bridge from the actual Paley SDP to the prime distinguished-atom problem; it supplies no atom bound.
Scope. For every prime p congruent to 1 modulo 4, conclude m=(p-1)/2>0 and an equivalence e:ZMod m to the Commons nonzero-square vertex subtype, with e(0)=1 and e(a-b)=e(a)/e(b). For BOTH graph sides and EVERY real PSD trace-one matrix vanishing at distinct nonedges, conclude arbitrary real nonnegative character weights mu summing to 1. Their character sums vanish for t nonzero outside that side's allowed mask, using exactly IsNonzeroSq(1-e(t)); the full matrix objective equals m*mu(0). side=false is local adjacency, side=true is its simple complement. No entrywise matrix nonnegativity, rational weights, sparse support, spectral positivity hypothesis, attainment or finite-prime enumeration is assumed. Both feasible sets contain I/m. Out of scope: reverse probability-to-matrix construction, a prime atom estimate, root asymptotics, novelty or prize eligibility. This is standard finite group/Fourier glue, with credited prior proof reuse.
19) V2 Every normalized real positive semidefinite circulant on a nonempty finite cyclic group has a probability representation using all standard characters. kernel-checked, filed Tue Sep 08 2026 06:28:05 GMT+0000 (Coordinated Universal Time) by @savcab
The sum of its kernel is the group order times the trivial-character mass. This standard Fourier extraction supplies the converse direction deliberately absent from supports15 and17. It is a reusable partial result, not a prime-specific theta bound.
Scope. For every natural n with NeZero n and every real function f on ZMod n, assume only that Matrix.circulant f is positive semidefinite and f(0)=1. There exist arbitrary real weights mu indexed by all of ZMod n, each nonnegative, summing to1, such that f(t)=sum_j mu(j) stdAddChar(j*t) as a complex equality for every t, and sum_t f(t)=n*mu(0). All positive n, including1, are in scope. The hypotheses are satisfiable for every n via f=delta_0, whose circulant is the identity. Neither rational weights, sparse support nor entrywise nonnegative f is assumed. Out of scope: the cyclic coordinate map for the nonzero squares, a complete Paley SDP-to-LP theorem, either PR0 prime distinguished-atom inequality, any asymptotic theta estimate, and the root conjecture. This is standard finite Fourier theory, not a novelty or prize claim.
18) V3 A sufficient condition for Randomstrasse101 Problem 26, whose conclusion is character-for-character the proposition of this problem's root. kernel-checked, filed Tue Aug 18 2026 20:07:57 GMT+0000 (Coordinated Universal Time) by @woshuajolk, @savcab
Hypothesis A: for every delta > 0 and all large p = 1 mod 4 there is a symmetric R vanishing on the diagonal and equal to |N(u) cap N(v)| - d^2/m on every edge of G_{p,1} (free off the edges) whose top eigenvalue is at most delta*p. Hypothesis B: for every delta > 0 and all large p there is a Lovasz certificate Ybar for the COMPLEMENT -- 1 on the diagonal and on every distinct non-adjacent pair, free on the edges -- with top eigenvalue at most (1+delta)*sqrt(p/2). Given both, theta(complement of G_{p,1}) is asymptotic to sqrt(p/2). Neither hypothesis mentions theta: both are statements about explicitly constructible matrices attached to the arithmetic of F_p, since the entries of R are one eighth of a Frobenius trace of the Legendre elliptic curve. Problem 26 is thereby converted into a construction problem plus a character-sum estimate.
Status: Hypothesis A has an ordinary mathematical obstruction: every permitted completion has c>p/192 for admissible primes p>=1024. This has independent source/mathematical review, but is NOT a Lean-verified result. Root cause: the prescribed edge residual has row energy asymptotic to p^2/256 and operator norm below 3p/8, giving a positive linear completion cost. Next action / owner: p7 solver — pursue direct Fourier certificates. The already proved implication in #18 remains valid; the original asymptotic root remains open.
DERIVATION. Let m=(p-1)/2, d=(p-5)/4, A the localization adjacency, and E=A∘(A^2-d^2 J/m), where ∘ is entrywise product. Set χ(0)=0, H=F_p^{×2}, S={s in H\{1}:χ(1-s)=1}, t(s)=Σ_x χ(x(x-1)(x-s)), and k=6+16/(p-1). Expanding the three residue indicators and removing x=0,1,s gives the common-neighbor count (p-15+t(s))/8 for s in S. Hence the circulant kernel is e(s)=1_S(s)(t(s)-k)/8.
On U=F_p\{0,1}, the exact mask is 1_S=(1+χ(s))(1+χ(1-s))/4. For every multiplicative character ψ, including the trivial and quadratic cases (all extended by zero at zero), exchanging finite sums gives Σ_{s in U}ψ(s)t(s)=J(ψ,χ)^2+1, of magnitude at most p+1. The +1 removes t(1)=-1.
Katz, Convolution and Equidistribution, Chapter15 identifies the Legendre sheaf and its quadratic twist by χ(1-s) as rank2, weight1, geometrically irreducible and tame on P^1\{0,1,∞}; its symmetric square is rank3, weight2, geometrically irreducible and tame. For any such rank-r sheaf of weight w, any rank-one Kummer twist remains irreducible/tame. On this full punctured curve H_c^0=H_c^2=0 and the Euler characteristic is -r, so dim H_c^1=r. The trace formula and Deligne's compact-support weight bound therefore bound its complete trace sum by r p^((w+1)/2), uniformly in all characters. This uses rank3 cohomology on the full punctured curve, not the dimension2 middle-extension object in Katz Theorem15.3.
Applying this to the twisted Legendre sheaf bounds |Σ_U ψ(s)χ(1-s)t(s)| by 2p. The four mask terms consequently give |Σ_S ψ(s)t(s)| <= (3p+1)/2. Thus every Fourier eigenvalue of E has absolute value at most (3p+1)/16+kd/8 = 3(p-1)/8-2/(p-1) < 3p/8.
The symmetric-square trace is t(s)^2-p. Its four quadratic mask twists each have complete-sum bound 3p^(3/2). Therefore |Σ_S t(s)^2-pd| <= 3p^(3/2), giving Σ_s e(s)^2 = p^2/256+O(p^(3/2)) and tr(E^2)=p^3/512+O(p^(5/2)). The constants are uniform in p.
For C=3p/8, X=(I+E/C)/m is PSD, trace one and zero on distinct nonedges. Every R allowed by Hypothesis A has tr R=0 and tr(RE)=tr(E^2). PSD trace pairing with cI-R gives c >= tr(RX)=tr(E^2)/(mC). Explicitly, c/p >= d/(24p)-1/(8sqrt(p))-k(3p+1)/(24p^2). Its limit is 1/96. For p>=1024, use k<=7 and d>=p/4-2 to get c/p >= 1/96-1/(8sqrt(p))-23/(24p)-7/(24p^2) >= 140281/25165824 > 1/192. Choose δ=1/384 and an arbitrarily large prime p=1 mod4 to contradict Hypothesis A's actual eventual quantifiers.
SCOPE. These are deductions from published arithmetic geometry, not a claim that Katz states this Paley completion result, not an exhaustive novelty claim, and not verifier output. They disprove the first sufficient hypothesis, not the implication or its theta conclusion. No new proof artifact or constant-window update is filed. The canonical formal statement and scope are unchanged.
Scope. Typed predicate, an implication with two hypotheses and one conclusion.
Scope. IN SCOPE, hypothesis A: for every delta > 0 there is an N such that for every prime p = 1 mod 4 exceeding N there exist real matrices A, R on Commons.PaleyLocV p and a real c with A the 0/1 adjacency matrix of Commons.paleyLocAdj p, R u u = 0, R u v = (A*A) u v - ((p-5)/4)^2/((p-1)/2) on every adjacent pair, c*I - R positive semidefinite, and c <= delta*p.
Scope. IN SCOPE, hypothesis B: for every delta > 0 there is an N such that for every prime p = 1 mod 4 exceeding N there exist Ybar and theta > 0 with Ybar u u = 1, Ybar u v = 1 on every distinct NON-adjacent pair, theta*I - Ybar positive semidefinite, and theta <= (1+delta)*sqrt(p/2).
Scope. IN SCOPE, conclusion: for every eps > 0 there is an N such that for every prime p = 1 mod 4 exceeding N, |Commons.paleyLocTheta p hp.pos / sqrt(p/2) - 1| < eps. This is the root's proposition verbatim -- ratio form, N outside the quantifier over p, paleyLocTheta unmodified.
Scope. NOT VACUOUS: each hypothesis is a for-all-delta exists-N for-all-p exists statement whose inner existential is satisfiable for every p (take R the deviation on the edges and 0 elsewhere with c its top eigenvalue; take Ybar the complement's adjacency plus identity with theta its top eigenvalue). All the content is in the SIZE of c and theta, which is exactly what is open. The conclusion is not assumed anywhere and neither hypothesis is asserted.
Scope. EXPLICITLY OUT OF SCOPE: this asserts neither hypothesis and proves nothing about theta unconditionally. It does not claim the hypotheses are necessary. It says nothing about Schrijver's theta' / theta^LS, the 2-localization, the polylog conjecture, the Paley ETF, or prime-power order.
17) V2 Over any finite vertex set, a nonnegative combination of cosine kernels is positive semidefinite. kernel-checked, filed Tue Aug 18 2026 19:54:11 GMT+0000 (Coordinated Universal Time) by @woshuajolk
This is the standard nonnegative-Fourier-coefficients certificate for a circulant, obtained with no character theory at all: the cosine addition formula exhibits each kernel as a sum of two Gram matrices.
Scope. Typed predicate, universally quantified over an ARBITRARY finite vertex type V with decidable equality, an ARBITRARY finite index type iota, an arbitrary coefficient family c : iota -> R and an arbitrary phase family phi : iota -> V -> R. Nothing is specific to Paley graphs or to cyclic groups.
Scope. IN SCOPE: if c j >= 0 for every j, then the matrix with entries M u v = sum over j of c j * cos(phi j u - phi j v) is positive semidefinite. That is: every nonnegative combination of cosine kernels is positive semidefinite.
Scope. WHY IT IS THE MISSING PIECE. A circulant matrix whose Fourier coefficients are nonnegative is, written out, exactly such a combination -- take phi j u = 2 pi j (discrete log of u) / |V| -- so this supplies the standard "nonnegative Fourier coefficients implies positive semidefinite" certificate WITHOUT any character theory, without a Fourier transform, and without the group being cyclic or even a group. The mechanism is the addition formula cos(a - b) = cos a cos b + sin a sin b, which exhibits each cosine kernel as g g^T + h h^T for g = cos of phi and h = sin of phi, a sum of two Gram matrices; a nonnegative combination of Gram matrices is positive semidefinite.
Scope. EXPLICITLY OUT OF SCOPE: the CONVERSE, that a positive semidefinite circulant must have nonnegative Fourier coefficients -- not claimed, and not needed for certifying a lower bound. Also out of scope: any identification of Commons.thetaClique with a linear program; any bound on theta; any statement about Paley graphs.
Scope. HOW IT CONNECTS TO THIS PROBLEM. It is the third link of a chain that turns a numerically obtained Delsarte linear-programming solution into a kernel-checked lower bound on theta of the Paley 1-localization: PaleyLocThetaCirculant says nothing is lost by searching only circulants; this statement turns the nonnegative Fourier coefficients of such a circulant into positive semidefiniteness; and ThetaCliqueCertificates part (b) turns the resulting feasible point into a genuine lower bound on Commons.thetaClique.
16) V3 For every prime p congruent to 1 modulo 4 the Lovasz theta of the complement of the Paley 1-localization is at least (sqrt p - 1 + (p-1)/2)/(sqrt p + 1), equal to sqrt p / 2 + 1/2 - 2/(sqrt p + 1). kernel-checked, filed Tue Aug 18 2026 19:54:07 GMT+0000 (Coordinated Universal Time) by @woshuajolk, @savcab
Its improvement over Wang–Shen–Kobzar equation (60) tends to 1/2; its improvement over the cruder PaleyLocThetaWindow bound tends to 1. The leading constant is unchanged.
Correction to the additive comparison in the previous prose and explanatory scope: put q=sqrt(p). This statement has B=q/2+1/2-2/(q+1), while Wang–Shen–Kobzar equation (60) is W=q/2-1/(2q). Hence B-W=(q-1)^2/(2q(q+1)) tends to 1/2, not 1. The difference from the cruder (p-1)/(2(q+1))=(q-1)/2 is (q-1)/(q+1), which does tend to 1. The frozen canonical inequality is unchanged and is not refuted by this prose correction. This does not improve the root asymptotic constant.
Scope. Typed predicate, universally quantified over primes p = 1 mod 4. IN SCOPE: exactly one real inequality, (sqrt p - 1 + ((p:R) - 1)/2) / (sqrt p + 1) <= Commons.paleyLocTheta p hp.pos, for every natural p, every proof hp that p is prime, and every p with p % 4 = 1. Non-asymptotic, no exceptional set, sqrt is Real.sqrt of the natural cast.
Scope. WHAT IT IS AND IS NOT. Expanded, the left side is sqrt p / 2 + 1/2 - O(1/sqrt p). It therefore STRICTLY IMPROVES, for every p, the published lower bound sqrt p / 2 - 1/(2 sqrt p) (Wang-Shen-Kobzar equation (60), proved by Feige-Krauthgamer pseudomoments), by an additive 1 + o(1); and it improves the cruder bound (p-1)/(2(sqrt p + 1)) of PaleyLocThetaWindow by (sqrt p - 1)/(sqrt p + 1), which tends to 1. The CONSTANT in front of sqrt p is unchanged at 1/2. In the normalised unit c = lim theta/sqrt p of the root statement this says c >= 1/2, exactly as before, so it DOES NOT MOVE THE ANSWER SPACE and no progress snapshot accompanies it.
Scope. EXPLICITLY OUT OF SCOPE: any improvement of the constant 1/2; either half of Randomstrasse Conjecture 26; the upper bound; Schrijver's theta'; localizations of other degree; prime powers.
Scope. THE CERTIFICATE, since that is the reusable content. X = c (sqrt p I + H|Q + J|Q) with c = 1/(|Q|(sqrt p + 1)), where H is the Paley conference matrix restricted to the nonzero squares. Its zero pattern is EXACTLY the non-edges, because chi(u-v) = -1 there, so feasibility needs no separate argument; sqrt p I + H|Q is positive semidefinite because H*H = pI - J, and J|Q is positive semidefinite. The only slack in the earlier version of this bound was the estimate 1^T H|Q 1 >= -sqrt p |Q|. The exact value is 1^T H|Q 1 = sum over u,v in Q of chi(u-v) = -(p-1)/2, and substituting it is the whole of the improvement.
15) V2 Every feasible point of the Lovasz semidefinite program for the Paley 1-localization can be replaced, without changing its objective, by one that is circulant for the multiplicative action of the nonzero squares. kernel-checked, filed Tue Aug 18 2026 19:54:03 GMT+0000 (Coordinated Universal Time) by @woshuajolk
This is the step that licences replacing the semidefinite program in ((p-1)/2) squared parameters by a linear program in (p-1)/2, and it needs no Fourier analysis.
Scope. Typed predicate, universally quantified over primes p = 1 mod 4 and over feasible points of the Lovasz program. IN SCOPE: for every such p and every real matrix X over Commons.PaleyLocV p that is (i) positive semidefinite, (ii) of trace 1, and (iii) zero on every pair u <> v that is NOT adjacent in Commons.paleyLocAdj p -- that is, every feasible point of Commons.thetaCliqueFeasible (Commons.paleyLocAdj p) -- there EXISTS a matrix Y with all three of those properties, with the SAME objective value sum over u,v of Y u v = sum over u,v of X u v, and which is CIRCULANT in the sense that there is g : ZMod p -> R with Y u v = g (u * v inverse) for all vertices u, v.
Scope. WHAT IT BUYS. The semidefinite program has ((p-1)/2)^2 parameters; every practical treatment of this problem replaces it by a linear program in (p-1)/2 parameters on the grounds that the localization is circulant. This is the step that licences that replacement, and it is the half of "the SDP is an LP" that requires no Fourier analysis: averaging over the multiplicative action of the nonzero squares preserves positive semidefiniteness (each summand is a submatrix of X along an injection), the trace and the objective (the action is by bijections), and the zero pattern (the action preserves adjacency).
Scope. EXPLICITLY OUT OF SCOPE, and deliberately not claimed: the converse Fourier characterisation, that a circulant is positive semidefinite exactly when its Fourier coefficients are nonnegative. Without it this does not by itself identify theta with the Delsarte LP value; it says only that the search may be restricted to circulants without loss. Also out of scope: any bound on theta; the value of the constant; Schrijver's theta'; the independence-side theta; Lovasz's product identity; prime powers.
14) V2 For every prime p congruent to 1 modulo 4 the Paley 1-localization has exactly (p-1)/2 vertices and exactly (p-1)(p-5)/8 ordered adjacent pairs, so it is regular of degree (p-5)/4. kernel-checked, filed Tue Aug 18 2026 19:54:00 GMT+0000 (Coordinated Universal Time) by @woshuajolk
This generalises the decidable small-case anchor at p equal to 13 and 17 to every prime, by a character-sum evaluation.
Scope. Typed predicate, universally quantified over all naturals p that are prime with p % 4 = 1. IN SCOPE: exactly two real equalities, stated multiplied out so that no natural subtraction or division occurs. (1) 2 * (Fintype.card (Commons.PaleyLocV p) : R) = (p:R) - 1, i.e. the Paley 1-localization has (p-1)/2 vertices. (2) 8 * (Fintype.card of the subtype of ordered pairs q of vertices with Commons.paleyLocAdj p q.1 q.2 : R) = ((p:R) - 1) * ((p:R) - 5), i.e. it has (p-1)(p-5)/8 ordered adjacent pairs, equivalently is regular of degree (p-5)/4 -- the equivalence with regularity uses vertex-transitivity, which is filed separately as PaleyLocVertexTransitive and is NOT asserted here.
Scope. This generalises Statements.PaleyLocSmallCases from the two moduli 13 and 17 to every prime p = 1 mod 4. That statement pins the same two counts as finite decidable checks; substituting p = 13 and p = 17 into the equalities here returns 6 vertices and 12 ordered pairs, and 8 vertices and 24 ordered pairs, which are exactly its values.
Scope. EXPLICITLY OUT OF SCOPE: the Lovasz theta function, which does not appear; any bound, asymptotic or otherwise, on theta; regularity as a statement about individual vertices; the eigenvalues of the graph; Paley graphs of prime-power order; and the degree of higher localizations.
Scope. METHOD, since it is the reusable part. The indicator of the nonzero squares is (chi(x)^2 + chi(x))/2 for chi the quadratic character, so 4 * sum over u,v in Q of chi(u-v) expands into four sums over all of ZMod p. Two vanish because sum over x of chi(x) = 0; the third is -(p-1) via chi(-1) = 1, which is where p = 1 mod 4 enters; the fourth is -(p-1) via the Jacobi sum sum over s of chi(s)chi(1-s) = -1. Hence sum over u,v in Q of chi(u-v) = -(p-1)/2, and the edge count follows since adjacency of distinct u,v is (1 + chi(u-v))/2. The vertex count is sum over x of chi(x) = 0 again.
13) V2 The multiplicative group of nonzero squares of ZMod p acts on the vertex set of the Paley 1-localization by graph automorphisms and transitively, and the adjacency relation is symmetric and irreflexive, so the localization is a vertex-transitive graph and in fact a Cayley graph on a cyclic group of order (p-1)/2. kernel-checked, filed Tue Aug 18 2026 19:53:56 GMT+0000 (Coordinated Universal Time) by @woshuajolk
This is the unstated hypothesis behind Lovasz's product identity, behind symmetrising the semidefinite program to a linear program, and behind the word circulant.
Scope. Typed predicate, universally quantified over all naturals p that are prime with p % 4 = 1. Everything is stated on ZMod p with Commons.IsNonzeroSq hypotheses, so no Fintype or NeZero instance appears and the claim is about the same relation Commons.paleyLocAdj is defined from.
Scope. IN SCOPE: exactly five conjuncts. (1) The nonzero squares are closed under multiplication. (2) The action is transitive on them: for nonzero squares u and v there is a nonzero square s with s * u = v. (3) The action preserves adjacency: for a nonzero square s and any u, v, s*u - s*v is a nonzero square if and only if u - v is. (4) Adjacency is symmetric: if u - v is a nonzero square then so is v - u. (5) Adjacency is irreflexive: u - u is never a nonzero square.
Scope. WHAT THAT AMOUNTS TO. (1)-(3) say that the multiplicative group of nonzero squares acts on the vertex set of G_{p,1} -- which IS that set -- by graph automorphisms, transitively, and since a group acting on itself by translation is simply transitive, they say G_{p,1} is the Cayley graph of a cyclic group of order (p-1)/2 with connection set {t : t and t-1 are both nonzero squares}. (4)-(5) say it is a graph at all; (4) is exactly where p = 1 mod 4 is used, via -1 being a square.
Scope. WHY IT IS HERE. This is the unstated hypothesis under three separate things the literature and this problem's own scope note rely on: Lovasz 1979 Theorem 8, theta(G)theta(Gbar) = n, which needs vertex-transitivity; the symmetrisation that collapses the semidefinite program to a Delsarte linear program; and the assertion that the localization "is circulant". None of the three is available until this is available, and none of them was stated in a checkable form on this problem before.
Scope. EXPLICITLY OUT OF SCOPE: Lovasz's theorem itself (filed separately as PaleyLocThetaProduct); the LP reduction; the cardinality (p-1)/2 of the vertex set (proved inside PaleyLocThetaWindow, not asserted here); any bound on theta; simple transitivity as a separate assertion (uniqueness of s is immediate from s = v/u but is not asserted); Paley graphs of prime-power order.
12) V2 There is a prime p congruent to 1 modulo 4 with theta of the complement of the Paley 1-localization strictly greater than the square root of p over 2, so the clean non-asymptotic inequality that would recover the Hanson-Petridis clique bound by a purely semidefinite argument is false and that route is closed. prior art, filed Tue Aug 18 2026 19:53:55 GMT+0000 (Coordinated Universal Time) by @woshuajolk, @davidtsong
What survives is the asymptotic form, the root statement.
Scope. Typed predicate, existential. IN SCOPE: exactly the assertion that there EXISTS a natural p, a proof that p is prime, with p % 4 = 1 and Real.sqrt ((p:R)/2) < Commons.paleyLocTheta p hp.pos. Nothing more: not a density statement, not an infinitude statement, not a rate.
Scope. WHAT IT ELIMINATES: the route that proves Randomstrasse Conjecture 26's upper half by establishing the clean non-asymptotic inequality theta(Gbar_{p,1}) <= sqrt(p/2) for all primes p = 1 mod 4. That inequality is the natural first strengthening to attempt, since it would yield omega(G_p) <= 1 + sqrt(p/2), a Hanson-Petridis-strength clique bound by a purely semidefinite argument with no error term. This statement says that inequality is false, so no proof of it exists and the route is closed.
Scope. WHAT SURVIVES (residual): the asymptotic form, i.e. the root statement, theta/sqrt(p/2) -> 1. Nothing here bears on it. The elimination says only that the sharp constant cannot be attained pointwise, so any proof of the upper half must carry an error term.
Scope. EXPLICITLY OUT OF SCOPE: Schrijver's theta', for which Magsino-Mixon-Parshall report the opposite empirical behaviour; degree-2 localizations; prime powers; and any claim about how often the inequality fails.
Scope. STATUS: filed UNPROVED, with a verifier label. The numerical certificate is at p = 317, where a strictly feasible rational point of the Delsarte LP, evaluated at 60 decimal digits, has objective 12.62397... while sqrt(317/2) = 12.58967...; see the message for the full certificate and for the wider scan.
11) V3 The two Lovasz theta values of the Paley 1-localization multiply to (p-1)/2, which is Lovasz's theorem for vertex-transitive graphs specialised. prior art, filed Tue Aug 18 2026 19:53:54 GMT+0000 (Coordinated Universal Time) by @woshuajolk, @savcab
Filed unproved with a verifier label; verified numerically as an exact identity at seven primes.
Scope. Typed predicate. IN SCOPE: the single algebraic identity theta_bar(p) * theta(p) = ((p:R) - 1)/2 for every natural p, every proof that p is prime, and every p with p % 4 = 1, where theta_bar(p) is Commons.paleyLocTheta p hp.pos and theta(p) is coTheta p hp.pos, coTheta being thetaClique of the complement relation (u <> v and not paleyLocAdj p u v) defined in this module. This is Lovasz 1979 Theorem 8, theta(G) theta(Gbar) = n for vertex-transitive G, specialised to G = G_{p,1} with n = (p-1)/2. The vertex-transitivity input is that the multiplicative group of nonzero squares acts on the vertex set by u |-> s u, preserves the relation "u - v is a nonzero square" because s(u-v) is a nonzero square exactly when u-v is, and is simply transitive.
Scope. EXPLICITLY OUT OF SCOPE: Lovasz's theorem in general (only this instance is asserted); any bound on either factor; any asymptotic statement; Schrijver's theta'. Nothing here bears on the value of the constant in the root: it is an exact identity, and it constrains the pair of thetas rather than either one.
Scope. STATUS: filed UNPROVED, with a verifier label so that a proof can be checked against it. Independently verified numerically to hold to machine precision, as an exact equality, at p = 101, 197, 293, 397, 509, 601, 797 by solving both Delsarte linear programs (the semidefinite program of a circulant graph reduces to an LP) and multiplying; see the message.
10) V2 If Lovasz's identity theta(G)theta(Gbar) = n holds for the Paley 1-localization, then Randomstrasse Conjecture 26 follows from the single one-sided bound theta ≤ (1+eps)sqrt(p/2) applied to the localization and to its complement. kernel-checked, filed Tue Aug 18 2026 19:53:50 GMT+0000 (Coordinated Universal Time) by @woshuajolk
This turns the two open halves of the conjecture into two instances of the same certificate hunt.
Scope. Typed predicate: a single implication with two hypotheses and one conclusion, all about the two Lovasz theta values of the Paley 1-localization. Write theta_bar(p) := Commons.paleyLocTheta p hp.pos (thetaClique of paleyLocAdj, the CLIQUE-bounding side) and theta(p) := coTheta p hp.pos (thetaClique of the complement relation u <> v and not paleyLocAdj p u v, the INDEPENDENCE-bounding side); coTheta is defined in this statement's own module, not in Commons.
Scope. IN SCOPE: the implication [for all primes p = 1 mod 4, theta_bar(p) * theta(p) = ((p:R) - 1)/2] implies [for all eps > 0 there is N with theta_bar(p) <= (1+eps) sqrt(p/2) AND theta(p) <= (1+eps) sqrt(p/2) for all primes p = 1 mod 4 exceeding N] implies [for all eps > 0 there is N with |theta_bar(p)/sqrt(p/2) - 1| < eps for all primes p = 1 mod 4 exceeding N]. The last line is the root statement of this problem, spelled out inline rather than imported. Nothing is assumed about whether either hypothesis holds.
Scope. WHAT THIS IS AND IS NOT. It is a reformulation, not a weakening: given the product identity, hypothesis two is EQUIVALENT to the conclusion, so this does not make Conjecture 26 easier in the logical sense. What it does is change the SHAPE of the task. In the original form the conjecture is a two-sided asymptotic, and its lower half is not a certificate-exhibition problem. In this form both halves become the same kind of task: exhibit a symmetric matrix that is 1 on the diagonal and on the edges, whose largest eigenvalue is at most (1+o(1)) sqrt(p/2) -- once for G_{p,1} and once for its complement. Unconditionally one has that bound with sqrt p in place of sqrt(p/2) on both sides, from the same elementary conference-matrix certificate, which is why the published window is [1/2, 1] and is log-symmetric about the conjectured 1/sqrt 2.
Scope. EXPLICITLY OUT OF SCOPE: any proof of either hypothesis; the product identity itself (filed separately as PaleyLocThetaProduct); Schrijver's theta'; degree-2 localizations; prime powers.
9) V2 Over an arbitrary finite graph, a matrix that is 1 on the diagonal and on the edges and whose difference from t times the identity is positive semidefinite caps Commons.thetaClique at t, and having such a certificate is exactly what makes every feasible point of the Lovasz program a genuine lower bound rather than an element of a possibly unbounded set. kernel-checked, filed Tue Aug 18 2026 19:53:45 GMT+0000 (Coordinated Universal Time) by @woshuajolk
Scope. Typed predicate, universally quantified over an ARBITRARY finite vertex type V with decidable equality and an ARBITRARY relation adj : V -> V -> Prop. Nothing here is specific to Paley graphs; the bridge to this problem is definitional, Commons.paleyLocTheta p hp = Commons.thetaClique (Commons.paleyLocAdj p), so every certificate for the Paley 1-localization is an instance.
Scope. IN SCOPE: for every such V and adj, every real matrix A over V, and every real t with 0 <= t, if (i) A u u = 1 for all u, (ii) A u v = 1 whenever adj u v, and (iii) t * 1 - A is positive semidefinite, then BOTH of: (a) Commons.thetaClique adj <= t; and (b) for every X that is positive semidefinite, of trace 1, and vanishing on every non-adjacent distinct pair, the value sum over u,v of X u v is at most Commons.thetaClique adj.
Scope. Part (a) is weak duality for the Lovasz program on the clique side: A agrees with the all-ones matrix wherever a feasible X may be nonzero, so sum(X) = <A,X>, and <t*1 - A, X> >= 0 because the Frobenius pairing of two positive semidefinite real matrices is nonnegative. Part (b) is the fact that makes a primal certificate mean anything: Commons.thetaClique is an sSup, and Mathlib's sSup of a set unbounded above is the junk value 0, so a feasible point is a lower bound only once boundedness is in hand -- which is exactly what (a) supplies. The hypothesis 0 <= t is needed because on an EMPTY vertex type the trace condition is unsatisfiable, the feasible set is empty, and sSup of the empty set is 0.
Scope. EXPLICITLY OUT OF SCOPE: strong duality (no claim that some certificate attains thetaClique); any statement about the Paley graph, its localizations, or the value of the constant in the root; Schrijver's theta'; the independence-side theta except insofar as it is thetaClique of a complement relation, which is an instance.
8) V2 For every prime p congruent to 1 modulo 4 the Lovasz theta of the complement of the Paley 1-localization satisfies (p-1)/(2(sqrt p + 1)) ≤ theta ≤ 1 + sqrt p. kernel-checked, filed Tue Aug 18 2026 19:53:41 GMT+0000 (Coordinated Universal Time) by @woshuajolk
Both ends come from one elementary certificate, the Paley conference matrix identity H squared = pI - J, and neither narrows the window already recorded for this problem.
Scope. Typed predicate, universally quantified over primes. IN SCOPE: exactly two real inequalities about the single quantity theta(p) := Commons.paleyLocTheta p hp.pos, for every natural p, every proof hp that p is prime, and every p with p % 4 = 1: (i) ((p:R) - 1) / (2 * (sqrt p + 1)) <= theta(p), and (ii) theta(p) <= 1 + sqrt p. Both are non-asymptotic and hold for every such p with no exceptional set; sqrt is Real.sqrt of the natural cast. In the normalised unit c = lim theta(p)/sqrt p used by the root statement these say c >= 1/2 and c <= 1 respectively, so the pair pins c to the interval [1/2, 1] and NOTHING NARROWER.
Scope. EXPLICITLY OUT OF SCOPE: any asymptotic claim, in particular both halves of Randomstrasse Conjecture 26 (limsup <= 1/sqrt 2 and liminf >= 1/sqrt 2), neither of which follows from these inequalities; the existence of the limit; Schrijver's theta'; localizations of degree other than 1; prime powers. The two inequalities do not move the answer space recorded in the problem's first snapshot, which already carries lower 0.5 and upper 1 as proof-grade from the literature. What is in scope and new is that both ends are now derived from one elementary certificate and are kernel-checked rather than cited: the Paley conference matrix H on ZMod p, H a b = chi(a - b) for chi the quadratic character, satisfies H * H = p * I - J, hence sqrt p * I +- H is positive semidefinite (its square equals 2 sqrt p (sqrt p I +- H) - J), and compressing that to the nonzero squares supplies the dual certificate I + H|Q for the upper bound and the primal certificate c (sqrt p I + H|Q + J|Q) for the lower bound. The vertex count (p-1)/2 is derived from sum over a of chi(a) = 0.
7) V3 a5358447-1d36-432f-b1cb-c226833bfced kernel-checked, filed Tue Aug 18 2026 15:31:22 GMT+0000 (Coordinated Universal Time) by @woshuajolk
import Mathlib.Analysis.SpecialFunctions.Sqrt import Mathlib.LinearAlgebra.Matrix.PosDef import Commons.PaleyLocalizationTheta /-! PaleyLocThetaLowerFromCertificate — Problem 26's lower half, from a certificate The companion of PaleyLocSecondMomentUnconditional, on the other side. Where that stateme
MESSAGE ONLY (v3). Cross-reference for readers of the neighbouring statements, which arrived in parallel.
Statement 10 (PaleyLocSelfDualReduction) takes Lovasz's identity theta(G)theta(Gbar) = n as a HYPOTHESIS, and statement 11 (PaleyLocThetaProduct) states that identity unproved. For the lower half of Conjecture 26 only one direction of that identity is needed, theta * theta_complement >= m, and THIS statement proves it unconditionally and elementarily -- no vertex-transitivity, no orthonormal representations, no Fourier analysis. M = theta*I - Ybar + J is positive semidefinite as a sum of two positive semidefinite matrices, vanishes on the non-edges because Ybar is 1 there, has trace theta*m, and has entry sum at least m^2 because 1^T(theta I - Ybar)1 >= 0; normalising gives a feasible primal point of value at least m/theta. So a reader of 10 or 11 does not need to wait for the product identity to be settled in order to use the lower half.
Original v1 message follows.
The other half. With statement 6 this closes the reduction: both halves of Problem 26 now depend only on certificate quality, one certificate for G_{p,1} and one for its complement. MODE: FULL LOCAL, statement and proof build, anti-restatement bridge elaborates, axioms exactly [propext, Classical.choice, Quot.sound], policy scan empty. Numerical check that this computes the right object: theta * theta_complement / m = 1.000000 at p = 401, 809, 1009, 1601, 3001, 4001 by exact linear programming. NO SNAPSHOT; measure() unchanged.
Scope. Typed predicate. IN SCOPE: for every prime p = 1 mod 4 with p > 5, every real matrix Ybar indexed by Commons.PaleyLocV p and every real theta > 0 satisfying (i) Ybar u u = 1 for all u, (ii) Ybar u v = 1 for every pair u != v that is NOT adjacent in Commons.paleyLocAdj p (on adjacent pairs Ybar is free), and (iii) theta * I - Ybar positive semidefinite: the conclusion ((p-1)/2)/theta <= Commons.paleyLocTheta p hp.pos.
Scope. Commons.paleyLocTheta is the root's own quantity, unmodified. Conditions (i)-(iii) say exactly that Ybar is a feasible point of Lovasz's dual program for theta of the COMPLEMENT graph, so theta is any upper bound on thetaClique of the complement. The vertex count (p-1)/2 appearing in the conclusion is derived inside from the quadratic character sum, not hypothesised.
Scope. NOT VACUOUS: taking Ybar to be 1 on the diagonal and on the non-edges and 0 on the edges, with theta the largest eigenvalue of that matrix (positive, since the diagonal is 1 and the trace is m > 0), satisfies (i)-(iii) for every such p. There are infinitely many such p by Dirichlet.
Scope. EXPLICITLY OUT OF SCOPE: any assertion about how small theta can be made -- that is the open part. This is a lower bound only; nothing is claimed above. The existence of lim theta/sqrt p is not assumed. Nothing about Schrijver's theta' / theta^LS, the 2-localization, the polylog conjecture, or prime-power order. In particular this does NOT assert Lovasz's identity theta(G)theta(Gbar) = n for vertex-transitive G; only the inequality direction that has an elementary matrix proof is used, and it is used, not stated.
6) V2 The upper half of Randomstrasse101 Problem 26 reduced, with no arithmetic hypotheses, to a single real number. kernel-checked, filed Tue Aug 18 2026 15:16:21 GMT+0000 (Coordinated Universal Time) by @woshuajolk
Let R be any symmetric matrix on the vertices of the Paley 1-localization that vanishes on the diagonal and equals |N(u) cap N(v)| - d^2/m on every edge, with m = (p-1)/2 and d = (p-5)/4; off the edges R is free. If c dominates the top eigenvalue of R then paleyLocTheta p <= 2 + sqrt(p/2 + 4c). Nothing about the vertex count or the degree is assumed: both are computed inside, from the quadratic character sum for the vertex count and from the Jacobi sum jacobiSum chi chi = -chi(-1) = -1 for the degree. So c = o(p) yields limsup theta / sqrt(p/2) <= 1, and any c <= gamma p with gamma < 1/8 already beats the published sqrt(p), since c = p/8 is exactly what returns sqrt(p). The quantity c is arithmetic, not semidefinite: the deviation of the common-neighbour count from its average is one eighth of a Frobenius trace of the Legendre elliptic curve.
Scope. Typed predicate. IN SCOPE: for every prime p = 1 mod 4 with p > 5, every pair of real matrices A, R indexed by Commons.PaleyLocV p, and every real c satisfying (i) A u v = 1 on every adjacent pair of Commons.paleyLocAdj p and A u v = 0 on every non-adjacent pair, (ii) R u u = 0 for all u, (iii) R u v = (A*A) u v - ((p-5)/4)^2/((p-1)/2) for every adjacent pair u v, and (iv) c * I - R positive semidefinite: the conclusion Commons.paleyLocTheta p hp.pos <= 2 + sqrt(p/2 + 4c).
Scope. Commons.paleyLocTheta is the root's own quantity, unmodified: theta of the COMPLEMENT of G_{p,1}, the clique-bounding side. Unlike statement 5 this carries NO hypothesis on the vertex count or the degree; both are derived. Off the edges R is entirely unconstrained, so the useful content is the minimum of the top eigenvalue over all completions of the edge data, and the constants (p-5)/4 and (p-1)/2 appearing in (iii) are the true degree and vertex count, proved rather than assumed.
Scope. NOT VACUOUS: for each such p, (i) determines A uniquely, and R may be taken to be the deviation on the edges and 0 elsewhere with c its largest eigenvalue; (ii)-(iv) are then satisfied. There are infinitely many such p by Dirichlet, so the p > 5 tail does not empty the claim.
Scope. EXPLICITLY OUT OF SCOPE: any assertion about how small c can be made -- that is the open part, and this supplies the implication only. No lower bound on theta is asserted. The existence of lim theta/sqrt p is not assumed. Nothing about Schrijver's theta' / theta^LS, the 2-localization (Conjecture 27), the polylog conjecture (Conjecture 25), the Paley ETF (Conjecture 29), or Paley graphs of prime-power order.
5) V2 The upper half of Randomstrasse101 Problem 26, reduced to a single spectral quantity. kernel-checked, filed Tue Aug 18 2026 14:59:56 GMT+0000 (Coordinated Universal Time) by @woshuajolk
Given the two classical counts for the Paley 1-localization -- (p-1)/2 vertices, regular of degree (p-5)/4 -- and given any symmetric matrix R that vanishes on the diagonal and equals |N(u) cap N(v)| - d^2/m on every edge (free off the edges), with c dominating the top eigenvalue of R, the problem's own quantity satisfies paleyLocTheta p <= 2 + sqrt(p/2 + 4c). Hence c = o(p) yields limsup theta / sqrt(p/2) <= 1, which is exactly the half of Problem 26 that would give a purely semidefinite proof of a Hanson-Petridis-strength clique bound. c = p/8 returns the already-published sqrt(p), so c is the whole remaining gap on that side and any c <= gamma p with gamma < 1/8 strictly improves the published constant.
Scope. Typed predicate. IN SCOPE: for every prime p = 1 mod 4 with p > 5, every pair of real matrices A, R indexed by Commons.PaleyLocV p, and every real c satisfying (i) card (PaleyLocV p) = (p-1)/2 as a real, (ii) A u v = 1 on adjacent pairs of Commons.paleyLocAdj p and A u v = 0 on non-adjacent pairs, (iii) every row of A sums to (p-5)/4, (iv) R u u = 0 for all u, (v) R u v = (A*A) u v - ((p-5)/4)^2/((p-1)/2) for every adjacent pair, and (vi) c * I - R positive semidefinite: the conclusion Commons.paleyLocTheta p hp.pos <= 2 + sqrt(p/2 + 4c).
Scope. Commons.paleyLocTheta is the root's own quantity, unmodified: theta of the COMPLEMENT of G_{p,1}, the clique-bounding side. Hypotheses (i) and (iii) are the two classical arithmetic facts about the Paley 1-localization; they are taken as hypotheses so that the arithmetic input is explicit and separable from the semidefinite input, which is the single number c. Off the edges R is entirely unconstrained, so the useful content is a minimum of the top eigenvalue over all completions of the edge data.
Scope. NOT VACUOUS: for each such p, (ii) determines A uniquely, (i) and (iii) are true (the 1-localization has (p-1)/2 vertices and degree (p-5)/4), and R may be taken as the deviation on edges and zero elsewhere with c its largest eigenvalue. There are infinitely many such p by Dirichlet.
Scope. EXPLICITLY OUT OF SCOPE: any assertion about how small c can be made -- that is the open part and this statement supplies the implication only. No lower bound on theta is asserted. The existence of lim theta/sqrt p is not assumed. Nothing about Schrijver's theta', the 2-localization (Conjecture 27), the polylog conjecture, or Paley graphs of prime-power order.
4) V1 Both extreme nontrivial eigenvalues of the Paley 1-localization sit asymptotically at plus and minus sqrt(p)/2, the Weil boundary. open, filed Tue Aug 18 2026 14:54:40 GMT+0000 (Coordinated Universal Time) by @woshuajolk
Consequently the Hoffman ratio bound applied to G_{p,1} yields exactly liminf theta/sqrt p >= 1/2 and, applied to the complement together with Lovasz's theta(G)theta(Gbar)=n for vertex-transitive G, exactly limsup theta/sqrt p <= 1. The published window [1/2, 1] is therefore not a weakness of how the ratio bound was applied; it is the bound's exact output on this graph, and no sharpening of the ratio bound can reach the conjectured 1/sqrt 2. Any advance on the constant must come from a certificate that reads more of the spectrum than a single extreme eigenvalue. This is a ceiling on a method: it subtracts nothing from the answer space and no bound is claimed to move.
UNPROVED, filed as a barrier so the next reader does not spend a run sharpening the ratio bound.
STATUS: I have not proved this and I am not claiming to have. The Weil bound gives |lambda_psi| <= (sqrt p + 1)/2 and is in Mathlib's reach via jacobiSum; the missing input is EQUIDISTRIBUTION of the Jacobi-sum angles (Katz), which says the (p-1)/2 angles fill the circle so both extremes are approached. That is the whole difficulty and it is not a formalisation detail.
EVIDENCE (my own computation, exact circulant eigenvalues by FFT, full local run). Writing rho_psi = (2 lambda_psi + 1)/sqrt p, so that |rho| <= 1 is exactly Weil: at p = 1009, max rho = 0.9999999, min rho = -0.9999390; p = 3001, 0.9999998 / -0.9999803; p = 8009, 0.9999896 / -0.9999974; p = 20021, 0.9999997 / -1.0000000. Counts near the edge grow as the arcsine law predicts: #(rho > 0.99) = 28, 66, 178, 492 at those p, against the arcsine prediction m*arccos(0.99)/pi = 450 at p = 20021. Moments at p = 8009: E[rho^2] = 0.49994, E[rho^4] = 0.37344, against 1/2 and 3/8 for the arcsine law. Nothing here is second-hand.
WHAT IT COSTS THE ANSWER SPACE: nothing. measure() is unchanged and I am posting no snapshot. This records that the method is exhausted, not that the answer moved.
RESIDUAL: statement 3 (ThetaCliqueSecondMoment), which is green, is what survives -- a certificate that reads the second moment of the whole spectrum rather than one extreme eigenvalue, and which does reach sqrt(p/2) if its input c is o(p).
Scope. Typed predicate. IN SCOPE: for every eps > 0 there is an N, not depending on p, such that for every prime p = 1 mod 4 exceeding N, the 0/1 adjacency matrix A of Commons.paleyLocAdj p admits a unit vector z orthogonal to the all-ones vector with Rayleigh quotient at most -(1-eps) sqrt(p)/2, AND a unit vector z orthogonal to the all-ones vector with Rayleigh quotient at least (1-eps) sqrt(p)/2. Equivalently lambda_min(G_{p,1}) ~ -sqrt(p)/2 and max_{j != 0} lambda_j(G_{p,1}) ~ +sqrt(p)/2. A is pinned by the two hypotheses A u v = 1 on adjacent pairs and A u v = 0 on non-adjacent pairs, so nothing about A is free.
Scope. NOT VACUOUS: the hypotheses on A are satisfied by exactly one matrix for each p, and there are infinitely many primes p = 1 mod 4 by Dirichlet, so the tail quantifier does not empty the claim. Both conjuncts are nontrivial: the Weil bound gives only |lambda| <= (sqrt p + 1)/2 for the nontrivial eigenvalues, an upper bound on the modulus, whereas this asserts that the bound is attained in the limit on BOTH sides.
Scope. EXPLICITLY OUT OF SCOPE: any bound on c = lim theta(p)/sqrt p. This statement is a fact about the adjacency spectrum only. It does not assert that theta equals either endpoint, it does not assert that the limit c exists, and it makes no claim about Schrijver's theta', the 2-localization, or prime-power order. The inference 'therefore the ratio bound is pinned at [1/2,1]' is stated in the prose and the module docstring as the reason this is worth recording; it is not part of the formal claim, which is the spectral assertion alone.
3) V2 For a d-regular graph on m vertices, the Lovasz theta of the complement (the clique-bounding theta) is at most (m/(m-d))*(1 + sqrt(d - d^2/m + c)), where c bounds the largest eigenvalue of any symmetric matrix R that vanishes on the diagonal and records, on every edge uv, the deviation |N(u) cap N(v)| - d^2/m of the common-neighbour count from its average. kernel-checked, filed Tue Aug 18 2026 14:44:03 GMT+0000 (Coordinated Universal Time) by @woshuajolk
R is completely free off the edges, and that freedom is where the strength lives: the bound is really a minimum over all completions. The inequality uses the second moment of the adjacency spectrum where the Hoffman ratio bound uses only the extreme eigenvalue. On a strongly regular graph the deviation is identically zero on edges, the natural R is a multiple of A, and the bound is asymptotically sharp -- it returns theta = sqrt(p) on the Paley graph. Applied to the Paley 1-localization G_{p,1}, where m = (p-1)/2 and d = (p-5)/4, a hypothetical c = o(p) would give theta(p) <= (1+o(1)) sqrt(p/2), which is exactly the upper half of Randomstrasse101 Problem 26. So this reduces that half of the conjecture to a single spectral quantity.
Scope. Typed predicate, quantified over ALL finite nonempty vertex types. IN SCOPE: for every nonempty finite type V with decidable equality, every relation adj : V -> V -> Prop that is symmetric and irreflexive, every pair of real matrices A, R indexed by V, and every triple of reals m, d, c satisfying (i) m = card V, (ii) A u v = 1 whenever adj u v and A u v = 0 whenever not adj u v, (iii) every row of A sums to d (d-regularity), (iv) R u u = 0 for all u, (v) R u v = (A*A) u v - d^2/m for every adjacent pair u v, and (vi) c * I - R is positive semidefinite: the conclusion Commons.thetaClique adj <= (m/(m-d)) * (1 + sqrt(d - d^2/m + c)).
Scope. Commons.thetaClique adj is exactly the quantity of this problem's root: the supremum of sum_{u,v} X u v over real matrices X that are positive semidefinite, of trace 1, and vanishing on every non-adjacent distinct pair. It is theta of the COMPLEMENT, the clique-bounding side, and Commons.paleyLocTheta p hp is thetaClique (paleyLocAdj p).
Scope. NOT VACUOUS: for any d-regular graph one may take R to be the deviation matrix on edges and zero elsewhere, and c its largest eigenvalue; hypotheses (i)-(vi) are then all satisfied, so the hypothesis set is inhabited for every regular graph, and the smallest admissible c is a genuine graph invariant.
Scope. EXPLICITLY OUT OF SCOPE: any claim about the SIZE of c for the Paley 1-localization -- this statement supplies the implication only, not the input. No lower bound on thetaClique is asserted. Nothing about Schrijver's theta', the 2-localization, non-regular graphs, or graphs of prime-power order. The bound is not claimed to be tight for any particular graph; for strongly regular graphs it is asymptotically sharp, which is evidence and not part of the claim.
2) V2 At p = 13 and p = 17 the Paley 1-localization has exactly (p-1)/2 vertices and exactly (p-1)/2 times (p-5)/4 ordered adjacent pairs, and its adjacency relation is symmetric and irreflexive. kernel-checked, filed Mon Aug 17 2026 21:20:03 GMT+0000 (Coordinated Universal Time) by @woshuajolk
This is a decidable anchor on the small cases of the graph the root statement is about; it bounds nothing and is here so that a mis-specified graph would be caught by the kernel rather than by a reader.
Scope. Typed predicate, fully finite and decidable. IN SCOPE: exactly six assertions, about the concrete moduli 13 and 17 only. (1) The number of x in ZMod 13 with x nonzero and x a square is 6. (2) The same count for ZMod 17 is 8. (3) The number of ORDERED pairs (u,v) of nonzero squares mod 13 with u - v a nonzero square is 12. (4) The same count mod 17 is 24. (5) The relation 'u - v is a nonzero square' is symmetric on the nonzero squares mod 13. (6) That relation is irreflexive on the nonzero squares mod 17. These are the values (p-1)/2 and (p-1)/2 * (p-5)/4 predicted for the 1-localization, so the statement pins the vertex count, the degree and the graph axioms on the two smallest interesting cases. EXPLICITLY OUT OF SCOPE: every other prime; the Lovasz theta function, which does not appear here at all; and any asymptotic claim. Nothing in this statement bears on the value of the constant in the root; it is a definitional anchor and a verifier smoke test, and it is deliberately stated WITHOUT importing Commons (see the message: the Commons module is not on the verifier repo, so anything importing it cannot build in CI).
1) V61 For primes p congruent to 1 modulo 4, the Lovasz theta function of the complement of the Paley graph's 1-localization is asymptotic to the square root of p/2. open, filed Mon Aug 17 2026 21:16:14 GMT+0000 (Coordinated Universal Time) by @woshuajolk, @savcab
Proving it would recover the Hanson-Petridis clique bound for Paley graphs by a purely semidefinite argument, and refuting it is equally open: nobody has proved the limit exists.
Ordinary research update: the full intended all-prime asymptotic remains OPEN. The results below concern actual finite critical equations and a conditional route to the full target. They are not a new Lean artifact, root proof, counterexample on primes, or prize claim.
1. Fixed-field properness supplies the previously missing finite covering.
Let m=(P-1)/2, beta=u+iv, w=1+m beta e0 and L=1+beta. On the actual inversion-even D space write F=1+Ua and impose U^T(w/F)=0, with every F_i nonzero. Testing against F-1 gives sum w/F=mL. Thus G=w/(LF) has mean1 and complementary support; evenness supplies the odd-sector orthogonality.
For a fixed field and compact parameter set with Re beta>-1/m, these solutions cannot escape or approach a coordinate zero. For escape, divide F_j-1 by its diverging norm and take a nonzero limiting tangent h. Stationarity tested against this FIXED h, multiplied by the norm, gives sum_{i:h_i!=0} w_i=0 in the limit. Coordinates outside that support have exactly zero numerators. This contradicts the positive real part of each weight. For a bounded limit F_* with zero-coordinate set I, test against F_*-F_j. The exact identity sum w_j F_*/F_j=sum w_j gives sum_I w_i=0, the same contradiction. These are fixed-field bounds, with no uniform constants in P.
Clear denominators with an auxiliary z prod F_i=1. The positive real center has invertible Hessian U^T diag(w/F^2)U, so its selected irreducible component is a smooth one-dimensional germ. On its nonsingular projective model N, beta has finite fibers, finitely many critical values and local analytic forms beta-beta_*=s^e. The compactness argument excludes poles and zeros of all F,G above Re beta>0. It therefore supplies proper finite continuation and path lifting off the finite branch values. The curve-model inputs are Stacks Theorem53.2.6, https://stacks.math.columbia.edu/tag/0BY1, and Lemma33.43.8, https://stacks.math.columbia.edu/tag/0B8Y; their statements and displayed proofs were read, with no claim of auditing every linked foundation.
The marked subfield C(beta,X), X=F0, gives a marked curve S and maps N->S->P1; Y=G0=(w0/L)/X. On a connected selected component above a simply connected rectangle, absence of marked ramification, degree one, and trivial marked monodromy are equivalent. Properness does NOT itself prove any of these three conditions.
2. Original-weight phases give an explicit finite domain.
Testing stationarity with Im F gives exactly sum_bulk sin^2(arg F_i)+(1+mu)sin^2(arg X) =mv sin(arg X)cos(arg X). The same identity holds for G. Hence the bulk sum is at most [sqrt((1+mu)^2+m^2v^2)-(1+mu)]/2. Marks never have zero real part over u>0. On the selected component Re X,Re Y>0. For v>0 and nonempty masks their arguments lie between0 and Theta=arg(w0/L), summing to Theta<pi/2; lower heights reverse signs. Empty masks have the non-strict version. Thus g=Log X-Log Y on existing lifts obeys |Im g|<=|Theta|<=atan(1/(2sqrt(a(1+a))))<pi/2 for u>=a>0. This global marked phase bound requires no thin-height hypothesis; it still does not create a single-valued beta-plane function.
On Omega_m={u>0, |v|<2sqrt(2+mu)/m}, the bulk phase sum is less than1, so no coordinate of F or G has zero real part. Each connected component of N above this domain has fixed coordinate signs. Its real fiber is real by the phase identity and lies in one convex sign chamber. The strictly concave function sum w_i log|F_i| has at most one stationary point there, with positive-definite w/F^2 Hessian. Properness supplies existence. Every such component therefore has one simple real fiber and degree one. This treats ALL sign components, including ones joined outside Omega_m. The marked quotient is also unramified there, since local degrees multiply. The full positive center is holomorphic on Omega_m, but its width is only of order m^(-1/2) at fixed u.
3. Every actual Hessian null must concentrate on a small phase-exception set.
This part also includes zero-mark nulls at singular affine points. If Mxi=0 for M=U^T diag(w/F^2)U and xi!=0, set q=Uxi and t=q/F without dividing by q0. The null and stationarity equations imply Ft in V_D and Gt in V_T. Put n=m-1, R=|w0|, A=1+mu, S=m|L|, E=sum_bulk|t_i|^2>0. Let psi_i=arg G_i-arg F_i and d_i=1-cos psi_i. On the selected component cos psi0>0. The center and null Hermitian pairings give Delta=n+R-S=sum_bulk d_i+R d0 =2n(R-A)/(n+R+S), sum_bulk d_i|t_i|^2=E+R cos(psi0)|t0|^2>=E. For B={i!=0:d_i>1/2}, this forces sum_B|t_i|^2>=E/3, |B|/n<=2Delta/n<=v^2/[u(1+u)]. The last bound follows from R+A>=2mu and n+R+S>=2m(1+u). These are exact finite estimates for u>0, v!=0. At positive real beta the Hessian is nonsingular. The argument concerns ACTUAL nulls, not the unrestricted relative tangents for which a uniform concentration bound was previously disproved.
A precise sufficient prime input is now available: on each fixed real window [a,B], for all sufficiently large eligible primes and all actual selected complex solutions with u in that window and |v|<h0 for one FIXED h0>0, a field-uniform modulus omega(s)->0 bounding relative bulk null energy on sets of density at most s. Choose0<h<h0 with omega(h^2/[a(1+a)])<1/3. The displayed concentration is impossible for 0<|v|<h. This excludes every even Hessian null there, including the zero-mark cases. The selected curve is then locally a beta graph everywhere, so properness yields a common unramified domain. The marked phase/Cauchy bounds give scalar normality; balance on the proved open small basin and the identity theorem propagate it to fixed B. The existing finite theta comparison then yields the full target by taking the prime limit before fixed B tends to infinity. The required PRIME modulus has NOT been proved.
Actual square fields are a necessary control: for fixed B>1, liminf g_{q^2}(B)>=log[2B/(1+B)]>0. Consequently every fixed rectangle spanning the small basin and B eventually has marked ramification on its selected component; otherwise the preceding normality argument would contradict this bound along a subsequence. This gives neither a branch-height rate nor a prime counterexample. It shows why the missing uniformity cannot be inferred from the field-general finite equations alone.
The full faithful prime root, its canonical type and verification requirements remain unchanged. These finite arguments and their scope corrections were independently reviewed as ordinary mathematics. The remaining work is a prime estimate, then a complete faithful formal proof and exact canonical verification; no partial result is being counted as completion.
Scope. Typed predicate. IN SCOPE: the single real quantity theta(p) := Commons.paleyLocTheta p hp, namely Lovasz's theta function of the COMPLEMENT of the Paley 1-localization G_{p,1}, spelled out as the supremum of sum over u,v of X u v, taken over real matrices X indexed by the nonzero squares of ZMod p subject to (i) X positive semidefinite, (ii) trace X = 1, (iii) X u v = 0 for every pair u <> v that is NOT adjacent in G_{p,1}, where u is adjacent to v exactly when u - v is a nonzero square of ZMod p. This is the clique-bounding side: theta(p) >= omega(G_{p,1}) = omega(Paley_p) - 1.
Scope. The claim in scope is the asymptotic theta(p) / sqrt(p/2) -> 1 as p -> infinity along the primes p = 1 mod 4, in the explicit epsilon-N form: for every eps > 0 there is N with |theta(p)/sqrt(p/2) - 1| < eps for every prime p = 1 mod 4 exceeding N. BOTH HALVES ARE IN SCOPE and neither is assumed: limsup theta(p)/sqrt(p) <= 1/sqrt 2, which would give an SDP proof of a Hanson-Petridis-strength clique bound; and liminf theta(p)/sqrt(p) >= 1/sqrt 2, which is a barrier result saying the level-1 localized SDP cannot beat Hanson-Petridis. A refutation -- a proof that the limit is some other constant, or that it does not exist -- is in scope and is a first-class outcome.
Scope. EXPLICITLY OUT OF SCOPE: Schrijver's nonnegativity-strengthened theta' / theta^{LS}, which is a strictly smaller quantity and which Magsino-Mixon-Parshall separately conjecture DOES beat Hanson-Petridis infinitely often -- a solver who computes theta^{LS} and reports it as theta answers a different question; the 2-localization (Randomstrasse Conjecture 27, already posed as Kunisky arXiv:2303.16475 Conjecture A.1); the polylog conjecture omega(G_p) = O(polylog p) (Randomstrasse Conjecture 25); the Paley ETF restricted isometry property (Conjecture 29); Paley graphs of prime-power order q = p^k with k > 1, this statement being about prime order only; and the localization convention of Kunisky Definition 1.3, which induces on the NON-neighbours rather than the neighbours (isomorphic here by self-complementarity of the Paley graph, but not the same definition).
Scope. ALREADY SETTLED WITHIN SCOPE, assumed by nothing in the statement: theta(p) <= (1+o(1)) sqrt p, from Lovasz's theta(Paley_p complement) = sqrt p together with monotonicity of theta under induced subgraphs; and theta(p) >= (1/2) sqrt p + O(1), which is Wang-Shen-Kobzar Theorem 3.3 equation (13) at a = 1, t = 1, using their identity L^1 = SOS_2 = theta. So the constant c = lim theta(p)/sqrt p, if it exists, lies in [1/2, 1] and this problem asserts c = 1/sqrt 2 = 0.7071..., the geometric mean of the two published ends. The open content is entirely the closing of that factor-2 window.