Crown graphs maximise the representation number of bipartite graphs

1 Introduction

• For even N ≥10, crown graphs require the longest minimum-length uniform representations among bipartite graphs, with maximum word length N⌈N/4⌉.The crown H_n,n has representation number ⌈n/2⌉ for n ≥5, and the common extremal value is 2 for 1 ≤ n ≤3, 3 for n = 4, and ⌈n/2⌉ for n ≥5.Source: §1 · p. 2

1.1 Previous work and the remaining difficulty

• Earlier work left the equal-even-part case unresolved; the paper develops Mozhui and Krishna’s local construction by choosing orders that avoid an extra permutation.For at least four pairs, every failure is witnessed by two fixed vectors or three vectors with one unspecified entry between them.Source: §1.1 · pp. 2–3

1.2 Outline of the proof

• Under the simplest choice of extreme values, quadratic obstruction growth versus exponentially many choices settles all large cases without changing the matching; for k ≥ 8, any matching of A has a suitable orientation.For small k, the proof varies the matching and unspecified entries.Source: §1.2 · p. 3

1.3 Conventions

• The conventions allow adding isolated vertices before constructing a representation and deleting them afterward; cyclic rotation preserves the represented graph.Theorem 1.1 includes disconnected graphs, isolated vertices, and vertices with identical neighborhoods, and the two parts may differ in size.Source: §1 · p. 2, §1.3 · p. 3

2 From neighbourhoods to orders

• Five gaps in the local word xyxy encode whether a vertex b alternates with both, one, or neither of x and y.The middle gap gives adjacency to both; adjacent inner gaps give adjacency to exactly one; outer gaps give adjacency to neither.Source: §2 · p. 4
• Each neighbourhood becomes a rank vector whose entries specify insertion positions, with stars independently completed by 0 or 4.For one pair, ranks 0 and 4 mean adjacency to neither endpoint; ranks 1, 2, and 3 encode adjacency to x only, both, or y only.Source: §2 · p. 4
• The ordering lemma gives rank-respecting permutations in which every pair of B letters appears in both relative orders exactly when no two completed vectors are strictly coordinatewise comparable.The permutations are assembled into a k-uniform word representing the graph when that condition holds.Source: §2 · p. 4
• The local words and intervening words make each vertex occur k times and ensure alternation exactly for adjacent pairs.For B letters, alternation is equivalent to having the same relative order in every permutation; the ordering lemma rules this out.Source: §2 · p. 5
• Repeated neighbourhoods can share completed rank vectors and be restored after the finite-case matching is chosen.Tie-breaking ensures identical-neighbourhood letters occur in both relative orders.Source: §2 · p. 5

3 Completing the unspecified entries

• Rows with at least two stars can be completed with both extremes, making them incomparable with every other row and removable from the feasibility test.One-star rows are represented by Boolean variables, with 0 and 1 assigning their starred rank to 0 and 4.Source: §3 · p. 5
• The comparison constraints give a complete feasibility test: reject strictly comparable fixed rows or a forced-1 variable whose implication closure reaches a variable forced to 0.A one-star row can be strictly smaller than a fixed row only at rank 0, and strictly larger only at rank 4.Source: §3 · pp. 5–6
• For k ≥4, feasibility fails exactly for a strictly comparable fixed pair or a one-star row directly forced both to 0 and 1.In a three-row obstruction, the fixed rows have ranks 1, 2, 3 at every coordinate except the star coordinate; the middle row is adjacent to all but that pair.Source: §3 · p. 6
• For k = 3, longer implication paths may occur, so the finite-case argument records their full implication closure.The four-coordinate argument excludes longer contradictory chains because four increasing positive ranks cannot fit in {1, 2, 3}.Source: §3 · pp. 6–7
• With a coordinate whose entries are only 1 or stars, feasibility fails exactly for the specified three-row obstruction, even when k = 3.The fixed rows both have rank 1 at that coordinate, while the one-star row is forced in opposite directions; other coordinates have ranks 1, 2, 3.Source: §3 · p. 7

4.1 Orienting a fixed matching: k ≥8

• At k = 8, the union bound for strict comparisons is 120/128 = 15/16, so some orientation of any fixed matching has no strict comparison.The bound remains below one for larger k, yielding a representing word by Lemma 2.2.Source: §4.1 · p. 8

4.2 Averaging over matchings: k = 6, 7

• Choosing uniformly among oriented perfect matchings of A, each prescribed k-element set of first endpoints has k! matching bijections to its complement; two rows partition A into four adjacency classes.Source: §4.2 · p. 8

4.3 Five pairs

• For k = 5, allowing optimal star assignments bounds the probability of a fixed-pair obstruction by 1/70.The maximum M5 is 216 at a permutation of (3, 3, 4), with Q5 = 30240; a feasible matching then proves the balanced ten-by-ten case.Source: §4.3 · pp. 9–10
• For k = 5, the total probability bound also accounts for three-row obstructions, while ignoring further necessary conditions inside the central row’s pair.The evaluated cases include 8640/665280 = 1/77 for k = 6 and 86400/17297280 = 5/1001 for k = 7.Source: §4.3 · pp. 9–10

5 The finite cases

• For balanced parts of sizes six and eight, two finite assertions are proved by showing no family obstructs every oriented matching.The common approach describes an obstructing family and rules out its existence.Source: §5 · p. 10

5.1 Obstructions for four pairs

• For four pairs, the minimal obstructions comprise 81 pair patterns and 24 triple patterns per representative matching.Across representative matchings, these yield 4,935 distinct obstructions: 2,415 pairs and 2,520 triples.Source: §5.1 · p. 10

5.2 Implication paths for three pairs

• For three pairs, obstructions may involve longer implication paths, represented by retained supports—sets of rows forcing a Boolean value—which capture every deduction within any selected family of at most six rows.Source: §5.2 · pp. 10–11

5.3 Boolean encoding and symmetry

• A Boolean formula is satisfiable exactly when a family of at most 2k neighbourhoods obstructs every oriented matching.The encoding imposes obstruction membership and symmetry-breaking comparisons under relabelling.Source: §5.3 · pp. 11–12

5.4 Checking the contradictions

• Both formulas are unsatisfiable, with their clause-addition certificates checked using reverse unit propagation.The F4 certificate has 34,482 additions; the F3 refutation has 3,305 additions and uses a 141,926-clause subformula.Source: §5.4 · p. 12
• The finite assertions establish the balanced bound for k = 3, 4, completing the balanced cases alongside the probability estimates.The obstruction lists, refutations, and implications from obstructing families to satisfying assignments also have Lean proofs.Source: §5.4 · pp. 12–13

6.1 Adding one permutation

• When |A| = 2k with k ≥2, appending one permutation gives every bipartite graph on A ⊔B a (k + 1)-uniform representation.The construction preserves alternation for edges and breaks it for nonedges.Source: §6.1 · p. 13
• Padding with isolated vertices gives R(G) ≤1 + ⌈m/2⌉ for m ≥3 and R(G) ≤3 for m ≤4, covering the smaller-part cases needed when m + n ≥9.For even m and n > m, the one-permutation lemma suffices; when n = m, the proof uses (5.4).Source: §6.1 · p. 13

6.2 Odd parts of nearly equal size

• For 5 ≤m ≤n with m odd, a distinguished-coordinate choice excludes every possible obstruction and yields the bound R(G) ≤⌈m/2⌉.The choice of one vertex ensures either that its complementary neighbourhood is absent or that no two distinct degree-k vertices are both adjacent to it.Source: §6.2 · pp. 13–14
• For odd smaller parts m = 2k −1 ≥5 with m ≤n ≤m+2, k-uniform representations give the bound ⌈(m+n)/4⌉ = k and complete the theorem.The lemma applies when the larger part has size at most 2k + 1.Source: §6.2 · p. 14

• The formula uses clauses for the membership implications and representative matchings, with additional clauses encoding the cardinality bound and lexicographic comparisons.Source: A The Boolean encoding · p. 15

A.1 Counting the selected neighbourhoods

• Counter variables q_i,j encode whether at least j of the selectors s_0, . . . , s_i−1 are true, with thresholds through 2k + 1.The final clause ¬q_h,2k+1 excludes a seventh or ninth selected neighbourhood when k is 3 or 4, respectively.Source: §A.1 · p. 15
• The counter recurrence is encoded by four clauses, and induction on i establishes the stated meaning of each counter variable.Source: §A.1 · p. 15
• The final threshold clause imposes that at most 2k selector variables are true.The encoding represents false by a variable constrained to be false, and true by its negation.Source: §A.1 · p. 15

A.2 Lexicographic comparisons

• Lexicographic clauses exclude a first difference of (0, 1), while auxiliary variables track whether extended prefixes remain equal.The largest selector vector in each full permutation orbit satisfies every comparison, preserving the existence of an obstructing family under relabelling.Source: §A.2 · pp. 15–16

A.3 The complete formulas

• The complete formula combines membership, matching, counter, symmetry, and constant clauses; its variable classes sum to the total variable count.The larger three-pair formula reflects longer implication paths in three coordinates.Source: §A.3 · p. 16

B Verification and reproduction

• The repository includes Lean proofs, finite data, and verification programs; validation/verify.py checks the certificate arguments and exact arithmetic.Source: B Verification and reproduction · p. 16

B.1 From rank patterns to clauses

• Each rank row determines a unique neighbourhood mask for a fixed oriented matching, linking the rank-pattern data to the mask-subset obstruction lists.The four-pair generator lists 81 pair patterns and 24 triple patterns for each representative matching; three-pair obstruction lists come from the support construction.Source: §B.1 · p. 16
• The DIMACS encoding uses one-based variable identifiers, with selectors first and the false variable at h + 1.A negative unit clause forces the false variable to be false, so its negative literal represents true.Source: §B.1 · p. 16
• Symmetry clauses compare bits under specified vertex permutations; omitting tautologies and repeated literals preserves truth values.The regenerated clause lists are checked against the exact formulas supplied to the certificate checkers.Source: §B.1 · p. 16
• The three-pair refutation uses a subformula of F3 whose clauses are mapped back to the full formula, while the four-pair refutation uses its own formula and certificate.The clause correspondence ensures that the contradiction applies to the formula constructed from neighbourhoods.Source: §B.1 · p. 17

B.2 Soundness of certificate verification

• If unit propagation derives a contradiction after assuming every literal of a proposed clause false, the current formula entails that clause.Inductively, every checked addition follows from the original formula, and the final empty clause proves unsatisfiability.Source: §B.2 · p. 17
• The illustrative certificate first derives both q and ¬q under ¬p, then obtains a contradiction after adding p.The three-pair certificate lists propagation clauses, and the checker verifies that each is unit or yields the terminal contradiction.Source: §B.2 · p. 17
• The certificates were generated with Z3 4.13.3, and the four-pair refutation is checked by two implementations.Lean separately checks propositional proofs of the contradictions and implications from obstructing families to satisfying assignments.Source: §B.2 · p. 17

B.3 Reproduction

• Run python3 validation/verify.py from the repository root to check the obstruction data, regenerate formulas, verify refutations, and check probability tables and rational bounds.The checks need Python 3.10 or later and a GCC-compatible C++17 compiler; no solver or internet connection is needed.Source: §B.3 · p. 17

B.4 Lean formalisation

• The Lean development fixes its toolchain and library versions, with Theorem 1.1 and Corollary 1.2 in lean/Crown/Main.lean.Separate modules formalise crown values, finite graph assertions, and odd part sizes, including the five-by-seven case.Source: §B.4 · pp. 17–18
• The Lean build assembles the proofs, compares statements against separate specifications, and checks exported proofs with the Lean kernel.The formal proofs use propositional extensionality, classical choice, and quotient soundness.Source: §B.4 · p. 18