Paper deep dive
Exact Zarankiewicz Values On Two Finite Frontier Slices
Koyar Afrasyab
Intelligence
Status: succeeded | Model: Gemma-4-26B-A4B | Prompt: intel-v1 | Confidence: 95%
Last extracted: 8/11/2026, 5:23:38 AM
Summary
This paper presents computer-assisted proofs for exact Zarankiewicz numbers Z(m,n,3,3) for specific finite slices of bipartite graphs. Key results include Z(12,n,3,3)=6n for 18<=n<=22, Z(13,22,3,3)=137, and several other exact values or bounds for dimensions involving 13, 14, 15, and 16 rows. The methodology relies on certificate-based verification using Farkas certificates, degree profile reduction, and modular Gram tests to exclude hypothetical matrices.
Entities (7)
Relation Signals (6)
Koyar Afrasyab → authored → Exact Zarankiewicz Values On Two Finite Frontier Slices
confidence 99% · Exact Zarankiewicz Values on Two Finite Frontier Slices Koyar Afrasyab
Z(12,18,3,3) → hasvalue → 108
confidence 99% · Z(12,18,3,3) <= 108... The 18-column witness has 108 ones
Z(13,22,3,3) → hasvalue → 137
confidence 99% · Z(13,22,3,3) = 137
Z(12,n,3,3) → hasformula → 6n
confidence 95% · Z(12,n,3,3) = 6n (18 <= n <= 22)
Z(13,22,3,3) → provedby → Farkas certificate
confidence 90% · eliminating the remaining six by ... exact Farkas certificates.
Z(12,18,3,3) → provedby → Farkas certificate
confidence 90% · The load-bearing new upper bounds are the exact 12 x 18 ... certificate packages.
Cypher Suggestions (0)
No Cypher suggestions yet.
Abstract
Abstract:The Zarankiewicz number Z(m,n,s,t) is the maximum number of edges in a bipartite graph with parts of orders m and n containing no copy of Ks,t. We give one combined, certificate-based computer-assisted proof for two finite slices and a corrected neighboring frontier: Z(12,n,3,3) = 6n (18 <= n <= 22), Z(13,22,3,3) = 137, Z(13, 18, 3, 3) = 116, Z(14, 18, 3, 3) = 124, Z(15,18,3,3) = 132, Z(14, 17, 3, 3) = 118, Z(15, 17, 3, 3) = 126, 132 <= Z(16,17,3,3) <= 133. The load-bearing new upper bounds are the exact 12 x 18 and 13 x 18 certificate packages. Their orbit certificates exclude every hypothetical matrix at the next edge count. Deletion lemmas and explicit witnesses close four neighboring cells, while the 16 x 17 entry is deliberately reported as an interval because only its 132-edge lower witness and the published 133 upper bound are certified here. Separately, the 13 x 22 proof excludes 138 ones by reducing to 83 degree profiles, rationally separating 77 of them, and eliminating the remaining six by marked-row congruences, leave enumeration, modular Gram tests, and exact Farkas certificates. All accepted claims are replayed by standard-library Python and exact integer/rational arithmetic; floating-point optimization is used only to discover certificates.
Tags
Links
- Source: https://arxiv.org/abs/2608.08154v1
- Canonical: https://arxiv.org/abs/2608.08154v1
Trouble viewing inline? Open PDF directly →
Full Text
35,595 characters extracted from source content.
Expand or collapse full text
Exact Zarankiewicz Values on Two Finite Frontier Slices Koyar Afrasyab (Date: 8 August 2026) Abstract. The Zarankiewicz number Z(m,n,s,t)Z(m,n,s,t) is the maximum number of edges in a bipartite graph with parts of orders m and n containing no copy of Ks,tK_s,t. We give one combined, certificate-based computer-assisted proof for two finite slices and a corrected neighboring frontier: Z(12,n,3,3)=6n(18≤n≤22),Z(13,22,3,3)=137,Z(13,18,3,3)=116,Z(14,17,3,3)=118,Z(14,18,3,3)=124,Z(15,17,3,3)=126,Z(15,18,3,3)=132,132≤Z(16,17,3,3)≤133. gatheredZ(12,n,3,3)=6n (18≤ n≤ 22), (13,22,3,3)=137,\\ Z(13,18,3,3)=116, (14,17,3,3)=118,\\ Z(14,18,3,3)=124, (15,17,3,3)=126,\\ Z(15,18,3,3)=132, 132 (16,17,3,3)≤ 133. gathered The load-bearing new upper bounds are the exact 12×1812× 18 and 13×1813× 18 certificate packages. Their orbit certificates exclude every hypothetical matrix at the next edge count. Deletion lemmas and explicit witnesses close four neighboring cells, while the 16×1716× 17 entry is deliberately reported as an interval because only its 132-edge lower witness and the published 133 upper bound are certified here. Separately, the 13×2213× 22 proof excludes 138 ones by reducing to 83 degree profiles, rationally separating 77 of them, and eliminating the remaining six by marked-row congruences, leave enumeration, modular Gram tests, and exact Farkas certificates. All accepted claims are replayed by standard-library Python and exact integer/rational arithmetic; floating-point optimization is used only to discover certificates. Key words and phrases: Zarankiewicz number, extremal bipartite graph, forbidden submatrix, computer-assisted proof, Farkas certificate, block design 2020 Mathematics Subject Classification: 05C35, 05D99, 68R10, 90C05 Independent researcher. Email: koyar@kinvectum.com. 1. Introduction The Zarankiewicz problem asks for the maximum number of edges in a bipartite graph avoiding a specified complete bipartite subgraph. It was posed by Zarankiewicz in 1951 [8] and was placed in its modern extremal form by Kővári, Sós and Turán [5]. Although the asymptotic theory is extensive, exact values for moderate finite parameters remain difficult. The difficulty is particularly pronounced for K3,3K_3,3-free graphs: useful counting inequalities leave a small but highly structured set of integer configurations, while direct exhaustive search suffers from severe symmetry and proof-certification costs. Write Z(m,n,s,t)Z(m,n,s,t) for the maximum number of edges in a subgraph of Km,nK_m,n containing no Ks,tK_s,t. Roman’s linear-programming framework [6] and later strengthened relaxations [2] provide effective finite upper bounds. SAT-based methods have also been developed for exact finite cases [7]. The classical finite table of Collins, Riasanovsky, Wallace and Radziszowski [3] supplies, among other inputs, Z(13,17,3,3)≤110Z(13,17,3,3)≤ 110 and Z(16,17,3,3)≤133Z(16,17,3,3)≤ 133. On the lower-bound side, Bhan, Nobili, Raghuraman and Langer [1] reported the 12-by-22 value and a 137-edge construction for the 13-by-22 parameter, with upper bound 140. 137≤Z(13,22,3,3)≤140.137 (13,22,3,3)≤ 140. The present paper adds the exact 12-by-18 certificate and its deletion consequences, and completes the 13-by-22 upper bound. Theorem 1.1. Z(12,n,3,3) (12,n,3,3) =6n =6n (18≤n≤22), (18≤ n≤ 22), Z(13,22,3,3) (13,22,3,3) =137, =137, Z(13,18,3,3) (13,18,3,3) =116, =116, Z(14,17,3,3) (14,17,3,3) =118, =118, Z(14,18,3,3) (14,18,3,3) =124, =124, Z(15,17,3,3) (15,17,3,3) =126, =126, Z(15,18,3,3) (15,18,3,3) =132, =132, 132≤Z(16,17,3,3) 132 (16,17,3,3) ≤133. ≤ 133. The values at n=18,19,20,21n=18,19,20,21, the 1313-by-2222 upper bound, the four neighboring frontier equalities, and the 132-edge 1616-by-1717 construction are the claims assembled here. The n=22n=22 equality and its classical design are retained as prior material. The proof is computer-assisted but certificate based. It is not a report of a mixed-integer solver returning “infeasible.” Every load-bearing numerical assertion is replayed by explicit finite data and exact arithmetic. The 12-by-n strip, the 13-by-2222 theorem, and the corrected frontier package retain separate certificate directories under proof/z12_18_21/, proof/, and proof/frontier_closure/; the combined verification gate runs the first two and the frontier package’s own gate. Theorem 1.2. There is no 13×2213× 22 binary matrix with 138138 ones and no all-one 3×33× 3 submatrix. Consequently, Z(13,22,3,3)=137. Z(13,22,3,3)=137. For the 13-by-22 component, the proof is computer-assisted but certificate based. It is not a report of a mixed-integer solver returning “infeasible.” Every load-bearing numerical assertion is replayed by short exact-arithmetic programs from explicit finite data. The architecture has three layers. (i) A global degree-profile argument reduces 138138 edges to 8383 profiles and eliminates 7777 by exact rational Farkas certificates. (i) A direct marked-row congruence argument excludes the exceptional profile 61873916^187^39^1. (i) The remaining five profiles are reduced to finite residual block-design problems on twelve points. Exhaustive leave-multigraph enumeration, necessary Gram conditions, and exact Farkas certificates exclude all residual cases. The source archive includes both certificate systems, all nested witnesses, independent profile enumerators, and a one-command verification gate. The result should nevertheless be regarded as a new computer-assisted proof pending independent reproduction and peer review. 2. The exact 12×n12× n strip We first isolate the 12-row result. Identify each column with a support in [12][12] and let λT _T be the number of columns containing a row triple T. The K3,3K_3,3-free condition is λT≤2 _T≤ 2 for every T∈([12]3)T∈ [12]3. The load-bearing upper bound is the exact certificate proof Z(12,18,3,3)≤108.Z(12,18,3,3)≤ 108. Its self-contained verifier enumerates 303 degree profiles for the neighboring 12×1712× 17 bound and 51 profiles for the 11×1811× 18 bound. Those bounds force any hypothetical 109-one 12×1812× 18 matrix into four normalized containment cases. The orbit trees in proof/z12_18_21/ contain exact rational dual leaves and exhaustive integer branches for all four cases; the standard-library replay accepts every certificate. The 18-column witness has 108 ones and row-triple histogram (6,68,146)(6,68,146) for multiplicities (0,1,2)(0,1,2). Four further witnesses are the first 19, 20, 21, and 22 blocks of the explicit classical 3-(12,6,2)(12,6,2) Hadamard design listed in Appendix A; their histograms are (3,54,163)(3,54,163), (1,38,181)(1,38,181), (0,20,200)(0,20,200), and (0,0,220)(0,0,220), respectively. Thus the lower bounds are 108,114,120,126,132108,114,120,126,132. Lemma 2.1 (Minimum-column deletion). For every m,n,s,tm,n,s,t with n≥2n≥ 2, Z(m,n,s,t)≤⌊n−1Z(m,n−1,s,t)⌋.Z(m,n,s,t)≤ nn-1\,Z(m,n-1,s,t) . Proof. If an e-edge m×nm× n matrix existed, some column would have degree at most ⌊e/n⌋ e/n . Deleting it leaves at least e−⌊e/n⌋e- e/n edges in an admissible m×(n−1)m×(n-1) matrix. Taking e one larger than the displayed floor makes this residual count exceed Z(m,n−1,s,t)Z(m,n-1,s,t), a contradiction. ∎ Applying the lemma successively from Z(12,18,3,3)=108Z(12,18,3,3)=108 gives Z(12,19,3,3)≤114,Z(12,20,3,3)≤120,Z(12,21,3,3)≤126,Z(12,22,3,3)≤132.Z(12,19,3,3)≤ 114, (12,20,3,3)≤ 120, (12,21,3,3)≤ 126, (12,22,3,3)≤ 132. The nested witnesses attain all four bounds, proving the first line of Theorem 1.1. The n=22n=22 equality is included for a unified statement but is not claimed as a new value. 3. Corrected finite-frontier closure The second reproducibility package, under proof/frontier_closure/, proves the new exact value Z(13,18,3,3)=116.Z(13,18,3,3)=116. Its verifier reduces a hypothetical 117-edge matrix to 19 column-degree profiles. Thirteen profiles are separated by exact integer-scaled Farkas certificates; the remaining six are eliminated by marked-row deficit averaging, exact point-type enumeration, and 12 symmetry-orbit pair-packing certificates. The packaged 116-edge witness is checked exhaustively over all row triples. The package’s optional dependency replay rechecks the earlier 12-by-17 and 12-by-18 certificates. Four neighboring equalities follow by the one-row density lemma and explicit witnesses. Collins et al. [3] give the published bound Z(13,17,3,3)≤110Z(13,17,3,3)≤ 110, so a 119-edge 14×1714× 17 matrix would leave at least 119−⌊119/14⌋=111>110119- 119/14 =111>110 edges after deleting a row; hence Z(14,17)≤118Z(14,17)≤ 118. Similarly, 125−⌊125/14⌋=117>116,127−⌊127/15⌋=119>118,125- 125/14 =117>116, 127- 127/15 =119>118, give the upper bounds Z(14,18)≤124Z(14,18)≤ 124 and Z(15,17)≤126Z(15,17)≤ 126. Finally, 133−⌊133/15⌋=125>124133- 133/15 =125>124 gives Z(15,18)≤132Z(15,18)≤ 132. The corresponding 118-, 124-, 126-, and 132-edge witnesses are stored and checked in the same package. For 16×1716× 17, the supplied 132-edge witness gives the lower bound Z(16,17)≥132Z(16,17)≥ 132, while the published table gives Z(16,17)≤133Z(16,17)≤ 133. We therefore record only 132≤Z(16,17,3,3)≤133.132 (16,17,3,3)≤ 133. No SAT timeout, unsuccessful construction search, or unverified DRAT claim is used in this interval. Remark 3.1 (Boundary of the retained frontier claims). If cijc_ij is the number of columns containing both rows i and j, deleting those rows removes di+dj−cijd_i+d_j-c_ij edges, so the remaining edge count is e−di−dj+cije-d_i-d_j+c_ij. Earlier exploratory certificates based on this reduction are not retained here: the explicit 126-edge 15×1715× 17 and 132-edge 16×1716× 17 witnesses rule out the former 125125- and 130130-edge exact claims, and no independently replayed certificate for the associated upper-bound claim is included. The paper therefore records only the certified statements in Theorem 1.1. 4. Block formulation and the lower bound Let X=[13]X=[13]. Identify the jjth column of a binary 13×2213× 22 matrix with its support Ej⊆XE_j X, and put dj=|Ej|d_j=|E_j|. For each triple T∈(X3)T∈ X3, define λT=|j:T⊆Ej|. _T=|\j:T E_j\|. The matrix is K3,3K_3,3-free if and only if (1) λT≤2(T∈(X3)). _T≤ 2 (T∈ X3). Repeated columns are allowed throughout. The supplementary file proof/data/z13_22_137_blocks.json contains 2222 blocks with total size 137137. Direct enumeration of all (133)=286 133=286 triples verifies (1). Thus (2) Z(13,22,3,3)≥137.Z(13,22,3,3)≥ 137. The same lower bound was first reported in [1]. A matrix plot of the independently checked witness is shown in Figure˜1; its block supports are listed in Appendix˜B. 1234567891011121314151617181920212212345678910111213 Figure 1. A checked 13×2213× 22 matrix with 137137 ones. Black cells are ones. Every triple of rows is contained in at most two columns. 5. Global reduction at 138 edges Assume for contradiction that blocks E1,…,E22E_1,…,E_22 satisfy (1) and (3) ∑j=122dj=138. _j=1^22d_j=138. Double counting incidences between blocks and row triples gives (4) ∑j=122(dj3)=∑T∈(X3)λT≤2(133)=572. _j=1^22 d_j3= _T∈ X3 _T≤ 2 133=572. Define the integer penalty (5) p(d)=(d3)−15d+70,0≤d≤13.p(d)= d3-15d+70, 0≤ d≤ 13. Its values are d012345678910111213p(d)70554026145006194070110161. array[]c|rd&0&1&2&3&4&5&6&7&8&9&10&11&12&13\\ p(d)&70&55&40&26&14&5&0&0&6&19&40&70&110&161. array Thus p(d)≥0p(d)≥ 0, with equality precisely for d=6,7d=6,7. Combining (3)–(5), (6) ∑j=122p(dj)=∑j(dj3)−15⋅138+70⋅22≤42. _j=1^22p(d_j)= _j d_j3-15· 138+70· 22≤ 42. Exact integer enumeration of all histograms (n0,…,n13)(n_0,…,n_13) satisfying ∑dnd=22,∑dnd=138,∑dp(d)nd≤42 _dn_d=22, _ddn_d=138, _dp(d)n_d≤ 42 leaves exactly 8383 degree profiles. This is independently regenerated by enumerate138.py and verify_138_reduction.py; no degree window is assumed. 5.1. The block-polytope relaxation For a profile (nd)(n_d), choose a degree f with nf>0n_f>0 and, by row symmetry, fix one f-block as F=1,…,fF=\1,…,f\. For every remaining allowed support B⊆XB X, let xB≥0x_B≥ 0 denote its multiplicity. Every actual matrix yields an integral feasible point of the following relaxation: (7) ∑B⊇TxB _B Tx_B ≤2−[T⊆F] ≤ 2-1[T F] (T∈(X3)), (T∈ X3), (8) ∑B∋r(|B|−12)xB _B r |B|-12x_B ≤132−[r∈F](f−12) ≤ 132-1[r∈ F] f-12 (r∈X), (r∈ X), (9) ∑B⊇P(|B|−2)xB _B P(|B|-2)x_B ≤22−[P⊆F](f−2) ≤ 22-1[P F](f-2) (P∈(X2)), (P∈ X2), (10) ∑|B|=dxB _|B|=dx_B =nd−[d=f] =n_d-1[d=f] (d active). (d active). The row and pair inequalities are nonnegative sums of triple-capacity inequalities; they are retained because they yield much shorter dual certificates. Lemma 5.1 (Exact Farkas criterion). Write (7)–(9) as Ax≤bAx≤ b, and (10) as Ex=eEx=e, with x≥0x≥ 0. If rational vectors α≥0α≥ 0 and unrestricted β satisfy ATα+ETβ≥0,bTα+eTβ<0,A^Tα+E^Tβ≥ 0, b^Tα+e^Tβ<0, then the profile is impossible. Proof. For a feasible x, 0≤xT(ATα+ETβ)=αTAx+βTEx≤αTb+βTe<0,0≤ x^T(A^Tα+E^Tβ)=α^TAx+β^TEx≤α^Tb+β^Te<0, a contradiction. This is the standard alternative theorem of Farkas [4]. ∎ The verifier regenerates every subset B of each active degree and checks every dual coefficient using fractions.Fraction. Stored rational certificates exclude 7777 of the 8383 profiles. The six not separated by this global relaxation are (11) 6187391,61676,5161477, 5261278,4161378,5361079. split&6^187^39^1, 6^167^6, 5^16^147^7, \ 5^26^127^8, 4^16^137^8, 5^36^107^9. split 6. Marked-row deficits For every triple T, put δT=2−λT≥0,Dr=∑T∋rδT. _T=2- _T≥ 0, D_r= _T r _T. If s=572−∑j(dj3)s=572- _j d_j3 is the unused triple capacity, then (12) ∑r∈XDr=3s. _r∈ XD_r=3s. Since a fixed row belongs to (122)=66 122=66 triples, each of capacity two, (13) Dr=132−∑j:r∈Ej(dj−12).D_r=132- _j:r∈ E_j d_j-12. This formula gives both congruence restrictions and a local design interpretation. 6.1. The profile 61873916^187^39^1 For this profile, s=23s=23, so ∑rDr=69 _rD_r=69. Contributions from degree-six and degree-seven blocks in (13) are 1010 and 1515, both zero modulo five; the degree-nine contribution is 28≡3(mod5)28≡ 3 5. Thus Dr≡2(mod5),r∉E9,4(mod5),r∈E9.D_r≡ cases2 5,&r∉ E_9,\\ 4 5,&r∈ E_9. cases The residue-minimal total is 4⋅2+9⋅4=444· 2+9· 4=44. Since the actual total is 6969, only five increments of size five are available, and at least eight rows have residue-minimal deficit. For a row outside the degree-nine block with Dr=2D_r=2, if a,ba,b count degree-six and degree-seven blocks through r, then (13) gives 2a+3b=262a+3b=26, hence (a,b)=(13,0)(a,b)=(13,0) or (10,2)(10,2). Deleting r leaves blocks of sizes five and six on twelve points. Pair-capacity degrees imply, respectively, total size-five incidence at most 60<6560<65, or at most 48<5048<50. Both are impossible. Therefore all four rows outside E9E_9 consume an increment. At least eight rows inside E9E_9 consequently have Dr=4D_r=4. For such a row, 2a+3b=202a+3b=20. The case (a,b)=(10,0)(a,b)=(10,0) is ruled out by the residual degree-nine block: its eight points permit at most three size-five incidences and the other four at most five, totaling 44<5044<50. Hence each of these at least eight rows lies in exactly two of the three degree-seven columns. Yet any fixed pair of degree-seven columns can share at most two such rows inside E9E_9, since three shared rows together with E9E_9 would form a K3,3K_3,3. The three pairs account for at most six rows, a contradiction. Proposition 6.1. The profile 61873916^187^39^1 is impossible. 7. The marked-row leave method It remains to exclude the five profiles in (11) containing only degrees four through seven. Fix a row r and delete it from every block containing it. The resulting residual blocks lie on the twelve-point set X∖rX \r\. Definition 7.1. The leave multigraph LrL_r has vertex set X∖rX \r\ and gives the pair x,y\x,y\ multiplicity δrxy _rxy. Its total edge multiplicity is DrD_r and every edge multiplicity lies in 0,1,2\0,1,2\. Suppose the residual blocks have active sizes s and that point x occurs in ux,su_x,s blocks of size s. Pair capacity through r,x\r,x\ gives (14) ex=22−∑s(s−1)ux,s,e_x=22- _s(s-1)u_x,s, where exe_x is the degree of x in LrL_r. In addition, (15) ∑xux,s=sns,∑xex=2Dr. _xu_x,s=sn_s, _xe_x=2D_r. Equations (14)–(15) give a finite list of point-type multisets. Let M be the point-by-residual-block incidence matrix. Its Gram matrix Q=MMTQ=M^T is determined by the point types and the leave: (16) Qxx=∑sux,s,Qxy=2−δrxy(x≠y).Q_x= _su_x,s, Q_xy=2- _rxy (x≠ y). Consequently, (17) rankp(Q)≤qrank_F_p(Q)≤ q for every prime p, where q is the number of residual blocks. When q=12q=12, M is square and (18) det(Q)=det(M)2 (Q)= (M)^2 must be a nonnegative integer square. The verifier uses (17) for p=101,103,107p=101,103,107 and (18) only as necessary conditions. Cases passing these screens are retained. For every surviving typed leave, the possible residual blocks form a finite linear factorization system. It requires the prescribed incidence count of every point in every size class, the prescribed pair multiplicities 2−δrxy2- _rxy, and the prescribed number of blocks of each size. An integral residual design would give a nonnegative integral solution. Each screened case is instead excluded by an integer-scaled rational Farkas vector whose inequalities are checked over every eligible residual block. Proposition 7.2 (Certified local screen). For each local parameter tuple invoked below, the program local_screen_general.cpp enumerates every point-type distribution satisfying (14)–(15), every loopless leave multigraph with edge multiplicities at most two and the prescribed degree sequence, and every case surviving (17) or (18). The Python verifier then checks an exact Farkas certificate for every retained factorization case. The proposition is a finite computational statement. Its implementation is deliberately small: the C++ source is approximately four kilobytes, and the certificate checker uses only the Python standard library. The complete enumeration counts used below are summarized in Table˜1. Branch Local parameters type multisets leaves certified survivors Common D=7D=7 (a,b)=(5,5)(a,b)=(5,5) 19 8,641 0 Common D=7D=7 (a,b)=(8,3)(a,b)=(8,3) 37 6,733 4 51614775^16^147^7, inside (a,b)=(6,4)(a,b)=(6,4) 508 43,715 0 51614775^16^147^7, inside (a,b)=(3,6)(a,b)=(3,6) 6 534 0 52612785^26^127^8, c=2c=2 (10,1),(7,3),(4,5)(10,1),(7,3),(4,5) – – 195+217+28 53610795^36^107^9, c=3c=3 (8,2),(5,4),(2,6)(8,2),(5,4),(2,6) – – 4,746+656+3 41613784^16^137^8, inside (8,3),(5,5)(8,3),(5,5) 41+48 367+275 12+3 Table 1. Selected exact local-enumeration counts. A dash indicates that only the final screened-case count is used in the proof report. 8. The common deficit-seven branch Four of the remaining profiles may force a row outside all degree-five blocks with Dr=7D_r=7. If a,ba,b denote the numbers of degree-six and degree-seven columns through r, then (13) leaves (a,b)=(5,5),(8,3),(11,1).(a,b)=(5,5),(8,3),(11,1). The (11,1)(11,1) branch has no point-type distribution. For (5,5)(5,5), all 8,6418,641 leave graphs fail the Gram-rank condition. The (8,3)(8,3) branch has 3737 point-type distributions and 6,7336,733 leave graphs; four cases survive the Gram screen. Three have immediate exact local Farkas certificates. The fourth case is fractionally feasible and therefore requires an integral refinement. The verifier enumerates all systems of its three residual size-six blocks, obtaining exactly 285285 systems. The full automorphism group preserving the typed leave is S2×S3×S6S_2× S_3× S_6, of order 8,6408,640, and partitions the systems into three orbits of sizes 1515, 180180, and 9090. The first two representatives have no completion by eight residual size-five blocks; the third has exactly four completions. For each of these four local completions, and for each of the four relevant global profiles, a separate rational completion certificate excludes the remaining columns. Thus sixteen exact completion certificates close the branch. Lemma 8.1. No marked row outside all exceptional small blocks can realize the common deficit-seven configuration used in the profiles 616766^167^6, 51614775^16^147^7, 52612785^26^127^8, or 53610795^36^107^9. 9. Elimination of the five final profiles We now combine residue baselines with Propositions˜7.2 and 8.1. 9.1. The profile 616766^167^6 Here s=42s=42, so ∑rDr=126 _rD_r=126, and every Dr≡2(mod5)D_r≡ 2 5. If no row had deficit 22 or 77, then every deficit would be at least 1212, giving a total at least 156156. Every deficit-two local type is rejected by point-type or Gram screening, while every deficit-seven type is rejected by Lemma˜8.1. Hence the profile is impossible. 9.2. The profile 51614775^16^147^7 Let c∈0,1c∈\0,1\ record membership in the unique degree-five block. Then Dr≡2−c(mod5)D_r≡ 2-c 5. The minimum cases D=2D=2 for c=0c=0 and D=1D=1 for c=1c=1 are locally impossible. The next baseline has deficit seven on the eight outside rows and six on the five inside rows, totaling 8⋅7+5⋅6=86.8· 7+5· 6=86. The required total is 111111, only five increments of size five larger, so some row attains this baseline. Outside rows are impossible by Lemma˜8.1; the inside possibilities (a,b)=(3,6),(6,4),(9,2),(12,0)(a,b)=(3,6),(6,4),(9,2),(12,0) are all rejected by exact local screening. Thus the profile is impossible. 9.3. The profile 52612785^26^127^8 Let c∈0,1,2c∈\0,1,2\ count the two degree-five blocks through the marked row. The initial cases (c,D)=(0,2),(1,1),(2,0)(c,D)=(0,2),(1,1),(2,0) are impossible. The next residue baseline has total 7⋅13−10=81,7· 13-10=81, whereas the required total is 9696. Thus a baseline row exists. The c=0c=0 and c=1c=1 branches reduce to earlier screens. For c=2,D=5c=2,D=5, the possible values are (a,b)=(10,1),(7,3),(4,5),(1,7).(a,b)=(10,1),(7,3),(4,5),(1,7). The last has no point types. The first three yield 195195, 217217, and 2828 screened cases, respectively, all excluded by exact Farkas certificates. 9.4. The profile 53610795^36^107^9 The initial c=0,1,2c=0,1,2 cases are again impossible. The next baseline has total 7⋅13−15=76,7· 13-15=76, while the required total is 8181, so a baseline row exists. The branches c=0,1,2c=0,1,2 have already been excluded. For c=3,D=4c=3,D=4, the possibilities (a,b)=(8,2),(5,4),(2,6)(a,b)=(8,2),(5,4),(2,6) produce 4,7464,746, 656656, and 33 screened local cases. Every one of the 5,4055,405 factorization systems has an exact integer-scaled Farkas certificate. 9.5. The profile 41613784^16^137^8 There are nine rows outside and four inside the degree-four block. Their minimum-residue baseline is 9⋅2+4⋅4=34,9· 2+4· 4=34, whereas the required total is 8484. If neither minimum occurred, the total would be at least 9999, so a row of deficit two outside or deficit four inside must occur. Outside deficit-two rows are impossible. For an inside deficit-four row, the residual exceptional block has size three. The endpoint branches have no point types; the two nontrivial branches leave 1212 and 33 screened factorization cases, all excluded by exact certificates. Proposition 9.1. None of the five profiles 61676,5161477,5261278,4161378,53610796^167^6, 5^16^147^7, 5^26^127^8, 4^16^137^8, 5^36^107^9 can occur in a K3,3K_3,3-free 13×2213× 22 matrix with 138138 ones. 10. Proof of the main theorem Proof of Theorem˜1.2. The witness in Appendix˜B proves (2). Suppose a 138138-one matrix existed. The penalty enumeration (6) places its degree multiset among 8383 profiles. Exact global Farkas certificates exclude 7777 profiles. Proposition˜6.1 excludes 61873916^187^39^1, and Proposition˜9.1 excludes the five remaining profiles. Therefore no 138138-one matrix exists. Deleting ones shows that no larger K3,3K_3,3-free matrix exists either, so the checked 137137-one construction is optimal. ∎ 11. Verification, reproducibility, and trust boundary The complete proof artifact is designed to separate discovery from verification. 11.1. One-command verification From the repository root, run cd proof python3 verify_all.py The verifier compiles local_screen_general.cpp with a C++17 compiler if needed, then performs the following checks: 1. validates the 137137-one witness over all 286286 row triples; 2. independently re-enumerates the 8383 possible 138138-edge degree profiles; 3. replays 7777 global rational Farkas certificates; 4. checks the elementary exclusion of 61873916^187^39^1; 5. exhaustively regenerates every marked-row point-type and leave case used for the five final profiles; 6. verifies every local and completion certificate coefficient exactly. 7. runs the nested 12-by-18 through 12-by-22 witness scans and deletion-chain checks in proof/z12_18_21/. The expected final line is ALL EXACT-VALUE VERIFICATION GATES PASSED 12-BY-18-THROUGH-22 GATE PASSED The frontier gate is run separately from its directory: cd proof/frontier_closure python3 verify_all.py python3 mutation_tests.py python3 frontier_propagation.py It verifies 13 global and 12 local frontier certificates, six explicit witnesses, the five exact equalities above, and the 132≤Z(16,17)≤133132≤ Z(16,17)≤ 133 interval. The optional dependency flag replays the bundled 12-row package. 11.2. Certificate counts The complete development archive also retains an earlier certified 139139-edge exclusion. Across all retained gates, the checker verifies 125,983125,983 candidate-block coefficients for the historical 139139 proof, 390,039390,039 for the global 138138 reduction, and 5,262,3925,262,392 for the final local proof, totaling 5,778,4145,778,414 exact nonnegativity checks. The 139139 component is not logically needed for Theorem˜1.2; it is retained as an independent regression test. 11.3. What is and is not trusted The proof depends on: • exhaustive finite integer enumeration in the supplied C++ source; • Python integer and Fraction arithmetic; • explicit Farkas vectors stored in JSON; • the explicit lower-bound witness. Floating-point linear programming was used during discovery to locate dual vectors. Before inclusion, these vectors were rationalized or integer-scaled, and the final checker verifies their defining inequalities from scratch. No floating-point solver status, MILP infeasibility flag, tolerance, or randomized search result is a premise. The only symmetry reduction in the integral common-D=7D=7 branch constructs all 8,6408,640 group elements explicitly, verifies that each preserves point types and leave multiplicities, and checks orbit coverage of all 285285 labeled systems. Repeated columns remain permitted throughout. 11.4. Epistemic status The package has passed its internal exact-arithmetic gate and an adversarial audit targeting omitted degree profiles, hidden simplicity assumptions, incomplete leave enumeration, invalid rank or determinant implications, symmetry loss, and numerical tolerance. Independent reproduction, a second implementation of the local enumerator, and expert peer review remain desirable. Accordingly, this manuscript reports a complete reproducible computer-assisted proof, not a peer-reviewed consensus result. 12. Discussion The proof illustrates a useful division of labor for finite extremal problems. A coarse global relaxation disposes of most degree patterns efficiently. The few profiles surviving the relaxation are not random hard instances: they are nearly balanced around the zero-penalty degrees six and seven, and their small unused triple capacity forces strong congruences on marked-row deficits. Passing to the leave of a marked row converts those congruences into a compact residual packing problem whose Gram matrix is almost determined. The method is potentially reusable. For nearby K3,3K_3,3-free matrix problems, one may seek a supporting line for d↦(d3)d d3, enumerate low-penalty degree profiles, apply global dual separation, and reserve exact leave enumeration for the integrality-only residue. The computational burden is then concentrated in small, transparent certificate families rather than a monolithic SAT or MILP run. A literature and repository audit dated 3 August 2026 located no prior publication or public preprint reporting the exact values Z(12,18,3,3)=108Z(12,18,3,3)=108, Z(12,19,3,3)=114Z(12,19,3,3)=114, Z(12,20,3,3)=120Z(12,20,3,3)=120, or Z(12,21,3,3)=126Z(12,21,3,3)=126. The audit treats the n=22n=22 value and the 3-(12,6,2)(12,6,2) design as prior/classical material, and it records the scope and limitation of the search in the accompanying 12-row package. For Z(13,22,3,3)Z(13,22,3,3), the 137-edge construction was previously reported while the exact upper bound is supplied here. These priority statements are necessarily provisional and should be rechecked during peer review. The frontier audit dated 3 August 2026 located no prior indexed report of Z(13,18)=116Z(13,18)=116, Z(14,17)=118Z(14,17)=118, Z(14,18)=124Z(14,18)=124, Z(15,17)=126Z(15,17)=126, or Z(15,18)=132Z(15,18)=132, nor of the 132-edge 16×1716× 17 construction. This is a dated search finding rather than a universal nonpublication guarantee. Acknowledgements OpenAI GPT 5.6 Sol High was used for assistance with exploratory reasoning, implementation, verification, manuscript integration, and packaging. The author is solely responsible for the mathematical claims and final manuscript. No heuristic solver status is used as a theorem. Appendix A The nested 1212-row witness family The following 22 supports form the verified classical 3-(12,6,2)(12,6,2) design. Every triple of row labels occurs in exactly two supports. The first n supports therefore give the lower-bound witness for each 18≤n≤2218≤ n≤ 22. The machine-readable CSV files under proof/z12_18_21/data/ are the load-bearing representation used by the verifier. 12,7,8,9,11,1221,3,4,5,6,1031,2,3,4,8,942,4,5,8,10,1151,4,6,7,8,1163,5,6,8,9,1171,2,3,5,7,1181,2,6,9,10,1191,2,5,6,8,12103,4,5,7,8,12111,3,6,7,9,12121,2,4,7,10,12132,3,5,9,10,12144,6,8,9,10,12152,3,4,6,11,12161,4,5,9,11,12175,6,7,10,11,12181,3,8,10,11,12191,5,7,8,9,10202,3,6,7,8,10212,4,5,6,7,9223,4,7,9,10,11 array[]r l1&\2,7,8,9,11,12\\\ 2&\1,3,4,5,6,10\\\ 3&\1,2,3,4,8,9\\\ 4&\2,4,5,8,10,11\\\ 5&\1,4,6,7,8,11\\\ 6&\3,5,6,8,9,11\\\ 7&\1,2,3,5,7,11\\\ 8&\1,2,6,9,10,11\\\ 9&\1,2,5,6,8,12\\\ 10&\3,4,5,7,8,12\\\ 11&\1,3,6,7,9,12\\\ 12&\1,2,4,7,10,12\\\ 13&\2,3,5,9,10,12\\\ 14&\4,6,8,9,10,12\\\ 15&\2,3,4,6,11,12\\\ 16&\1,4,5,9,11,12\\\ 17&\5,6,7,10,11,12\\\ 18&\1,3,8,10,11,12\\\ 19&\1,5,7,8,9,10\\\ 20&\2,3,6,7,8,10\\\ 21&\2,4,5,6,7,9\\\ 22&\3,4,7,9,10,11\ array Appendix B The 137137-edge witness Rows are labeled 1,…,131,…,13. The following 2222 column supports have total size 137137: B1=2,4,6,7,11,13B2=3,6,7,8,10,13B3=3,4,6,8,11,12B4=1,3,8,9,10,12B5=1,3,4,6,9,13B6=1,2,3,8,11,13B7=1,2,4,6,8,10B8=1,2,3,6,7,12B9=2,7,8,10,11,12B10=2,6,8,9,12,13B11=2,3,4,7,8,9B12=2,3,4,10,12,13B13=1,2,7,9,10,13B14=2,3,6,9,10,11B15=3,7,9,11,12,13B16=1,3,4,7,10,11B17=1,2,4,9,11,12B18=1,5,6,10,11,12,13B19=1,5,6,7,8,9,11B20=4,5,8,9,10,11,13B21=1,4,5,7,8,12,13B22=4,5,6,7,9,10,12 array[]@l@B_1=\2,4,6,7,11,13\&B_2=\3,6,7,8,10,13\\\ B_3=\3,4,6,8,11,12\&B_4=\1,3,8,9,10,12\\\ B_5=\1,3,4,6,9,13\&B_6=\1,2,3,8,11,13\\\ B_7=\1,2,4,6,8,10\&B_8=\1,2,3,6,7,12\\\ B_9=\2,7,8,10,11,12\&B_10=\2,6,8,9,12,13\\\ B_11=\2,3,4,7,8,9\&B_12=\2,3,4,10,12,13\\\ B_13=\1,2,7,9,10,13\&B_14=\2,3,6,9,10,11\\\ B_15=\3,7,9,11,12,13\&B_16=\1,3,4,7,10,11\\\ B_17=\1,2,4,9,11,12\&B_18=\1,5,6,10,11,12,13\\\ B_19=\1,5,6,7,8,9,11\&B_20=\4,5,8,9,10,11,13\\\ B_21=\1,4,5,7,8,12,13\&B_22=\4,5,6,7,9,10,12\\\ array The first seventeen blocks have size six and the final five have size seven. The accompanying verifier checks that each row triple occurs in at most two blocks. References [1] J. Bhan, N. Nobili, S. Raghuraman, and P. Langer, New bounds for Zarankiewicz numbers via reinforced LLM evolutionary search, arXiv:2605.01120, 2026. [2] S. Davies, P. Gill, and D. Horsley, Improved upper bounds on Zarankiewicz numbers, Discrete Math. 349 (2026), no. 5, 114924. doi:10.1016/j.disc.2025.114924. [3] A. F. Collins, A. W. N. Riasanovsky, J. C. Wallace, and S. P. Radziszowski, Zarankiewicz numbers and bipartite Ramsey numbers, arXiv:1604.01257, 2016. arXiv:1604.01257. [4] J. Farkas, Theorie der einfachen Ungleichungen, J. Reine Angew. Math. 124 (1902), 1–27. doi:10.1515/crll.1902.124.1. [5] T. Kővári, V. T. Sós, and P. Turán, On a problem of K. Zarankiewicz, Colloq. Math. 3 (1954), 50–57. doi:10.4064/cm-3-1-50-57. [6] S. Roman, A problem of Zarankiewicz, J. Combin. Theory Ser. A 18 (1975), no. 2, 187–198. doi:10.1016/0097-3165(75)90007-2. [7] Y. Tan, An attack on Zarankiewicz’s problem through SAT solving, arXiv:2203.02283, 2022. [8] K. Zarankiewicz, Problem P 101, Colloq. Math. 2 (1951), 301.