What the formal proof says

Every list of 14-point blocks on 24 points covering every 4-point set has at least 20 entries. Repeated blocks are allowed.

theorem c24_14_4_lower_twenty (T : Family 24)
    (hrows : ∀ R, R ∈ T → ValidBlock 14 R) (hcover : IsCovering 4 T) : 20 ≤ T.length

FinalCoveringBounds.lean:21Checked by Lean

Derived from the first bound by counting the blocks through each point.

theorem c25_15_5_lower_thirty_four (F : Family 25)
    (hrows : ∀ R, R ∈ F → ValidBlock 15 R) (hcover : IsCovering 5 F) : 34 ≤ F.length

FinalCoveringBounds.lean:25Checked by Lean

The core of the proof: a covering with exactly 19 blocks contradicts itself.

theorem exact_nineteen_excluded : ExactNineteenExcluded

FinalCoveringBounds.lean:16Checked by Lean

$C(22,12,2) \ge 6$

The counting input. With Schönheim’s bound it gives the old lower bound of 19.

theorem pair_cover_22_12_ge_six (F : Family 22)
    (hrows : ∀ R, R ∈ F → ValidBlock 12 R) (hcover : IsCovering 2 F) :
    6≤F.length

campaigns/async_goal/lean/recovered/PairLowerBoundRecoveredV4.lean:131Checked by Lean

$\lambda(x,y) \ge 6$

In any (24,14,4) covering, every two points lie in at least 6 common blocks.

theorem pair_floor_six (T : Family 24)
    (hrows : ∀ R, R ∈ T → ValidBlock 14 R) (hcover : IsCovering 4 T)
    (p q : Fin 24) (hpq : p≠q) : 6≤pairDegree T p q

FormalResume20261003/PairFloorV1.lean:51Checked by Lean

$(11^{23},13)\ \text{or}\ (11^{22},12^2)$

All but one or two points lie in exactly 11 blocks.

lemma degree_patterns (T : Family 24) (hrows : ∀ R, R ∈ T → ValidBlock 14 R)
    (hcover : IsCovering 4 T) (hlen : T.length = 19) :
    (∃ p, degree T p = 13 ∧ ∀ q, q ≠ p → degree T q = 11) ∨
    (∃ p q, p ≠ q ∧ degree T p = 12 ∧ degree T q = 12 ∧
      ∀ r, r ≠ p → r ≠ q → degree T r = 11)

A19PhysicalCounts.lean:30Checked by Lean

$\#\{\text{balanced components}\} \ge |L| - 19$

The Gram matrix of the degree-11 points has rank at most 19, and its kernel is spanned by balanced components of the excess graph.

lemma component_count_from_physical (T : Family 24)
    (hrows : ∀ R, R ∈ T → ValidBlock 14 R) (hcover : IsCovering 4 T) (hlen : T.length = 19) :
    Fintype.card (LowPoint T) - 19 ≤
      Nat.card {c // (lowSystem T hrows hcover).BalancedBipartite c}

A19WeightedFrontend.lean:42Checked by Lean

$\lambda(y,\sigma y) = 6,\ \lambda(y,z) = 3$

Eleven 12-point blocks covering every triple of 22 points, each point in 6 blocks, must be a doubled symmetric 2-(11,6,3) design.

theorem regular22_physical_twins (F : Family 22)
    (hrows : ∀ R, R ∈ F → ValidBlock 12 R) (hcover : IsCovering 3 F)
    (hlen : F.length=11) (hregular : ∀ p, degree F p=6) :
    ∃ σ : Fin 22 → Fin 22,
      (∀ p, σ p≠p) ∧ (∀ p, σ (σ p)=p) ∧
      (∀ p q, pairDegree F p q=if p=q ∨ q=σ p then 6 else 3) ∧
      (∀ p R, R ∈ F → (p ∈ R ↔ σ p ∈ R))

Regular22PhysicalRigidity.lean:112Checked by Lean

$\operatorname{tr}(K^2) \ge 396$

A Hermitian matrix of trace 66 and rank at most 11 has tr(K²) ≥ 66²/11. This is what rules out codegree-2 pairs.

theorem trace_square_ge_396 (K : Matrix n n ℝ) (hK : K.IsHermitian)
    (ht : K.trace = 66) (hr : K.rank ≤ 11) : 396 ≤ (K * K).trace

MatrixFoundation.lean:41Checked by Lean

The case split. “Gadget” is the agents’ name for a balanced quadruple.

lemma gadget_or_exceptional_components (T : Family 24)
    (hrows : ∀ R, R ∈ T → ValidBlock 14 R) (hcover : IsCovering 4 T) (hlen : T.length = 19) :
    HasGadget T ∨ Nonempty (ExceptionalComponents T hrows hcover)

A19ComponentDichotomy.lean:28Checked by Lean

$A^2 + A - 2I = J$

The twin classes of Step 6 form a cubic graph with this adjacency identity: the Petersen graph.

theorem adjacency_polynomial : D.adjacency * D.adjacency + D.adjacency -
    (2 : ℝ) • (1 : Matrix (Fin 10) (Fin 10) ℝ) = ones (Fin 10) (Fin 10)

QuotientMatrixGraph.lean:85Checked by Lean

Any such graph stays connected after deleting two vertices. The proof reroutes walks directly, without using that the graph is Petersen.

theorem cubic_ten_connected_delete_le_two
    (G : SimpleGraph (Fin 10)) [DecidableRel G.Adj]
    (hdegree : ∀ x, G.degree x = 3)
    (hadj : ∀ x y, G.Adj x y → G.commonNeighbors x y = ∅)
    (hnonadj : ∀ x y, x ≠ y → ¬G.Adj x y → ∃! z, z ∈ G.commonNeighbors x y)
    (R : Finset (Fin 10)) (hR : R.card ≤ 2) :
    (G.induce {x | x ∉ R}).Connected

SmallCutConnectivity.lean:125Checked by Lean

Proposition 7.

theorem gadget_impossible (T : Family 24)
    (hrows : ∀ R, R∈T → ValidBlock 14 R) (hcover : IsCovering 4 T)
    (hlen : T.length=19) (g : GadgetData T) : False

GadgetExclusion.lean:21Checked by Lean

Six triples that pairwise share exactly one point cannot fit on six points.

theorem no_six_omission_triples (P : Block 8) (F : Family 8)
    (hP : ValidBlock 2 P) (hrows : ∀ R, R ∈ F → ValidBlock 3 R)
    (havoid : ∀ R, R ∈ F → Disjoint R P)
    (hpairs : F.Pairwise (fun R S => (hits R S).length=1))
    (hlen : 6≤F.length) : False

FormalResume20261003/SixPointTriplesV1.lean:150Checked by Lean

Proposition 8.

lemma exception_impossible (T : Family 24)
    (hrows : ∀ R, R ∈ T → ValidBlock 14 R) (hcover : IsCovering 4 T) (hlen : T.length = 19)
    (E : ExceptionalComponents T hrows hcover) : False

PhysicalExceptionExclusion.lean:25Checked by Lean