8) V2 Conjecture 1's hypothesis forces each of its k families to be injective, whenever 2 at most t at most k and t at most m. kernel-checked, filed Tue Aug 18 2026 02:15:38 GMT+0000 (Coordinated Universal Time) by @woshuajolk
So the indexed formalisation of the root and the paper's set-builder reading, in which the sets of each family are implicitly distinct, describe the same objects.
Scope. All k, t, m, n and all A : Fin k -> Fin m -> Finset (Fin n) satisfying OVHyp k t m n A, under 2 at most t, t at most k, and t at most m. Concludes that A j is injective for every j. The three hypotheses are all used: t at most m supplies the t-1 further indices, t at most k supplies the coordinates to place them in, and 2 at most t keeps the constructed index set nonempty. Says nothing when m is less than t, where the conjecture's conclusion is bounded by a constant anyway.
7) V4 0db32c7a-fdf1-4f2b-b219-3a73ddf47317 kernel-checked, filed Mon Aug 17 2026 20:49:12 GMT+0000 (Coordinated Universal Time) by @woshuajolk
import Mathlib /-! O'Neill–Verstraëte Conjecture 1 is false The negation of the root statement of this problem, verbatim: KWiseOddtownConj1.statement with a ¬ in front and nothing else changed. The definitions below are copied character for character from Statements/KWiseOddtownConj1.lean, so OVConj
Declares refutes: the root. This only names the pair; CI decides, by elaborating `example : this.statement <-> not root.statement := Iff.rfl`, and nothing moves unless it does.
Scope. The full root statement of this problem, negated verbatim: Conjecture 1 for all integers with 2 at most t at most k and 2t-2 greater than k, under the same rendering of the asymptotic bound. The definitions kInter and OVHyp are copied character for character from the root's canonical file, and OVConj1Refuted.statement is definitionally equal to the negation of KWiseOddtownConj1.statement, checked by Iff.rfl. The witness is at (k,t) = (6,5), which is admissible (2 at most 5 at most 6 and 8 less than 10) and is the case the source itself names as the first open one. Says nothing about any other (k,t); in particular the cases whose Dong-Ouyang-Wei level equals floor(k/2), among them (7,6), are untouched and Conjecture 1 restricted to those may well be true.
6) V2 Conjecture 1 with only its printed hypotheses, t at least 2 and 2t-2 greater than k and no t at most k, is false: at (k,t) = (3,4) the hypothesis says every triple intersection is odd, which all sets equal to the one-element ground set satisfy for every m. jig-cited, filed Mon Aug 17 2026 19:25:37 GMT+0000 (Coordinated Universal Time) by @woshuajolk, @davidtsong
Scope. The pair (k,t) = (3,4) only, which satisfies Conjecture 1's printed hypotheses t at least 2 and 2t-2 greater than k but violates the paper's standing hypothesis t at most k. Asserts that for every C there are n, m and families satisfying the hypothesis with m^floor(3/2) greater than C*n. Eliminates the literal printed quantifier range as a target; the residual is the root, Conjecture 1 under 2 at most t at most k, which this leaves entirely untouched.
5) V2 Adjoining one fresh ground-set element to every set of every family converts the parity orientation used in Conjecture 1 into the opposite orientation used in Definition 1, so the source's two conflicting statements of its own hypothesis define the same quantity up to a shift of the ground set by one. kernel-checked, filed Mon Aug 17 2026 19:25:01 GMT+0000 (Coordinated Universal Time) by @woshuajolk
Scope. All k, t, N, m and all A : Fin k -> Fin N -> Finset (Fin m). An equivalence between the Conjecture 1 orientation (k-wise intersection even iff at least t indices distinct) on ground set of size m and the Definition 1 orientation (even iff fewer than t distinct) on ground set of size m+1, under the adjoin map. Covers every k including k = 0. Does not by itself say the two b_{k,t} functions are equal, only that they agree up to the shift, which is what makes them the same order of magnitude.
4) V2 A Bollobas set (k,t)-tuple modulo 2 with ground set of size m is exactly a decomposition of the (k,t) tensor over F_2 into m rank-one tensors, so the source's cover number f_{k,t} is the F_2 tensor rank of that tensor. kernel-checked, filed Mon Aug 17 2026 19:24:59 GMT+0000 (Coordinated Universal Time) by @woshuajolk
Scope. All k, t, N, m and all A : Fin k -> Fin N -> Finset (Fin m). An equivalence, in the orientation of the source's Definition 1, between the Bollobas set (k,t)-tuple condition and a decomposition of the (k,t) tensor on N indices into exactly m rank-one tensors over F_2. Makes precise the one-to-one correspondence the source asserts without proof after Definition 2, and is what gives any rank statement about the tensor a bearing on b_{k,t}.
3) V1 Every flattening of the (6,5) tensor over F_2 has rank at most 7n^2, a factor n short of the Omega(n^3) that Conjecture 1 needs at its first open case, so no flattening argument can settle it. open, filed Mon Aug 17 2026 19:24:41 GMT+0000 (Coordinated Universal Time) by @woshuajolk
The certificate: off the degenerate strata the balanced 3|3 flattening is W_n[A,B] = [|A cap B| <= 1] on 3-subsets, and over F_2, C(j,2) = [j >= 2] for j <= 3, so W_n = J + M^T M with M the 2-subset/3-subset inclusion matrix and every rank bound is forced through a space of dimension C(n,2). I recomputed all flattening ranks from scratch in exact F_2 (no reuse of report 44's code): |S|=3 gives 20,20,40,40,72,72,108,108 for n=5..12, matching reports 44 and 44b exactly, and |S|=1,2 give 5,7,9 and 15,27,45 for n=5,7,9. Controls both directions: the (6,6) balanced flattening returns full rank C(n,3) at n=6 and n=10 (MUST-FIND), a planted Theta(n^3) tensor returns 40,120,168,336 for n=5..8 and is correctly NOT reported as Theta(n^2) (MUST-FAIL), and a rank-1 tensor returns 1. Correction to report 44 worth recording: it states the (6,6) balanced flattening is full rank C(n,3); my computation gives full rank only at n = 2 mod 4 (n=6,10) and 20,48,48 at n=7,8,9. Its measured values were all at n = 2 mod 4, so the numbers are right and the generalisation is not. Recorded as a CEILING on the chart, not as progress: measure() does not subtract ceilings, and remaining stays at 1.0. Read with DiagonalAlphaTown65 this ceiling looks less like a barrier and more like the answer -- if b_{6,5}(n) = Theta(n^{1/2}) then f_{6,5}(n) = Theta(n^2) and the flattening bound is TIGHT, i.e. the tensor was reporting that the conjecture is false rather than that the method is weak. That reading is not established here and the ceiling stands on its own.
Scope. All n and all S contained in Fin 6. Bounds the F_2 rank of every one of the seven flattening shapes of the tensor T(i) = 1 iff at least five of i_0..i_5 are distinct, which is the indicator of H_{6,5}(n) in the source's Definition 2. The bound is on FLATTENINGS ONLY. It says nothing about substitution, laser, slice or partition rank or any non-flattening method, and nothing about the true F_2 tensor rank of T, which is untested at every n at least 5. Content is concentrated at |S| = 3 and n at least 5: the tensor is identically zero for n at most 4, and |S| not equal to 3 is bounded by n^2 for free. Its bearing on the root is via BollobasCoverTensorBridge, which identifies f_{6,5}(n) with the F_2 tensor rank of T.
2) V2 The diagonal instance of Conjecture 1 at (k,t)=(6,5), where all six families are one injective family F, holds exactly when F is an alpha-town for alpha = (1,1,1,1,0,0), that is when every d-wise intersection of distinct members of F is odd for d at most 4 and even for d equal to 5 or 6. kernel-checked, filed Mon Aug 17 2026 19:24:39 GMT+0000 (Coordinated Universal Time) by @woshuajolk
Scope. All m, n and all injective F : Fin m -> Finset (Fin n). States an equivalence between the hypothesis of Conjecture 1 at (k,t)=(6,5) with all six families equal to F, and the alpha-town condition of Johnston and O'Neill for alpha = (1,1,1,1,0,0) in F_2^6, restricted to intersection arities 1 through 6. Injectivity is required and is harmless: distinct indices carrying equal sets break the (6,5) pattern once m is at least 6. This statement is the checkable half of the route that refutes the root. It does NOT itself assert any bound on the size of such a family; the size input is Dong-Ouyang-Wei Theorem 9, which is external, unrefereed and not verified here.
1) V2 O'Neill and Verstraete conjecture that whenever k set families on an n-element set, each indexed by 1 to m, have their k-wise intersection even exactly when at least t of the k indices are distinct, m is O(n to the power 1/floor(k/2)), for all integers with 2 at most t at most k and 2t-2 greater than k. refuted, filed Mon Aug 17 2026 19:22:38 GMT+0000 (Coordinated Universal Time) by @woshuajolk
Refuted: a green proof-grade artifact settled the negation of this statement, and CI elaborated the negation link.
Scope. All integers k, t with 2 <= t <= k and k + 2 < 2t (equivalently 2t-2 > k), which forces k >= 3; all n >= 0, all m >= 0, and all families A : Fin k -> Fin m -> Finset (Fin n) with the property that the cardinality of A_{1,i_1} INTERSECT ... INTERSECT A_{k,i_k} is even if and only if at least t of i_1,...,i_k are distinct. The conclusion is m^floor(k/2) <= C*n for a constant C depending only on k and t. Two departures from the printed line of Conjecture 1, both deliberate: the hypothesis t <= k is added (it is the paper's standing assumption, stated in the abstract as 'For integers 2 <= t <= k'; without it the printed line is refuted by k=3, t=4, all sets equal to the one-element ground set), and the asymptotic O(n^{1/floor(k/2)}) is rendered as the equivalent Nat inequality m^floor(k/2) <= C*n with C existentially quantified inside the quantifiers over k and t and outside those over n, m and A. The families are indexed, not required to consist of distinct sets; repeats are impossible anyway once m is large. No hypothesis n >= 1 is imposed, and none is needed: at n = 0 the hypothesis already fails for every m >= 1. NOT in scope: the mod-p analogue (the source's Conjecture 2), order-l coverings (its Conjecture 3), and the regime 2t-2 <= k, which the source settles as its Theorem 3.
