Stream: General

Topic: I've apparently proven a false theorem in Isabelle.

Craig Alan Feinstein (Jan 10 2025 at 06:00):

When I was working on proving the Bruck Ryser Chowla theorem, I stumbled upon this false theorem:

theory Bruck_Ryser_Chowla_Improved imports
  Fishers_Inequality.Fishers_Inequality

begin

sublocale ordered_bibd ⊆ ordered_regular_pairwise_balance 𝒱s ℬs Λ 𝗋
  by unfold_locales

context ordered_sym_bibd

begin

lemma brc_v_1_mod_4:
      assumes "𝗏 = 1 mod 4"
        shows "(1 - Λ) * 𝗏^2 = (𝗄 - Λ)"
proof -
  have "(1 - Λ) * 𝗏^2 =  (𝗄 - Λ)"
    using assms t_design_min_v by linarith
  then show ?thesis by blast
qed

end

According my understanding of the Fisher's Inequality library, this means that if there is a symmetric block design (v,k,Λ) where v = 1 mod 4, the equation (1 - Λ) * 𝗏^2 = (𝗄 - Λ) must hold true. However, the projective plane of order 3 exists, where (v,k,Λ)=(13,4,1), yet the equation (1 - 1) * 13^2 = (4 - 1) is false. What is going on?

Craig Alan Feinstein (Jan 10 2025 at 06:31):

Interestingly if one assumes that v=3 mod 4, Isabelle will not accept the proof.

Fabian Huch (Jan 10 2025 at 09:19):

I think you want to assume v mod 4 = 1, here you're assuming that v=1

Fabian Huch (Jan 10 2025 at 09:21):

Which gives you the obvious contradiction

Craig Alan Feinstein (Jan 10 2025 at 14:36):

Thank you! Glad to know Isabelle is right. That really threw me off.

Last updated: Apr 03 2025 at 20:22 UTC