Theory KeyLemma
section ‹ KeyLemma ›
text ‹This theory establishes a "key lemma": if you draw a line
through a point inside a cone, that line will intersect the cone in
no fewer than 1 and no more than 2 points.›
theory KeyLemma
imports Classification ReverseCauchySchwarz
begin
class KeyLemma = Classification + ReverseCauchySchwarz
begin
lemma lemInsideRegularConeImplies:
assumes "insideRegularCone x p"
and "D ≠ origin"
and "l = line p D"
shows "0 < card (l ∩ regularConeSet x) ≤ 2"
proof -
define S where S: "S = (l ∩ regularConeSet x)"
define X where X: "X = (p ⊖ x)"
define a where a: "a = mNorm2 D"
define b where b: "b = 2*(tval X)*(tval D) - 2*((sComponent D) ⊙s (sComponent X))"
define c where c: "c = mNorm2 X"
define d where d: "d = (sqr b) - (4*a*c)"
have tlX: "timelike X" using lemTimelikeInsideCone assms(1) X by auto
hence cpos: "c > 0" using c by auto
have xnotp: "x ≠ p" using assms(1) by auto
have aval: "a = mNorm2 D" using a by auto
have bval: "b = 2*(X ⊙m D)"
using b local.lemSDotCommute local.right_diff_distrib' mult_assoc
using local.mdot.simps by presburger
have cval: "c = mNorm2 X" using c by auto
have dval: "d = 4 * ( (sqr (X ⊙m D)) - (mNorm2 X)*(mNorm2 D) )"
proof -
have "d = (sqr b) - (4*a*c)" using d by simp
moreover have "(sqr b) = 4*(sqr (X ⊙m D))"
using lemSqrMult[of "2" "(X ⊙m D)"] bval by auto
moreover have "4*a*c = 4*(mNorm2 X)*(mNorm2 D)"
using aval cval mult_commute mult_assoc by auto
ultimately show ?thesis using right_diff_distrib' mult_assoc by metis
qed
define r2p where r2p: "r2p = (λ r . (p⊕(r⊗D)))"
define p2r where p2r: "p2r = (λ q . (THE a . q = (p⊕(a⊗D))))"
have bij: "∀ r q . r2p r = q ⟷ (∃ w . (r2p w = q)) ∧ (p2r q = r)"
proof -
have uniqueroots: "∀ a r . r2p a = r2p r ⟶ a = r"
proof -
{ fix a r assume "r2p a = r2p r"
hence "(a⊗D) = (r⊗D)" using r2p add_diff_eq by auto
hence "((a-r)⊗D) = origin" using lemScaleDistribDiff by auto
hence "(a-r) = 0" using assms(2) by auto
hence "a = r" by simp
}
thus ?thesis by blast
qed
{ fix q r assume lhs: "r2p r = q"
have "(THE a . q = r2p a) = r"
proof -
{ fix a assume "q = r2p a"
hence "a = r" using uniqueroots lhs r2p by blast
}
hence "∀ a . q = r2p a ⟶ a = r" by auto
thus ?thesis using lhs the_equality[of "λa . q = r2p a" "r"]
by force
qed
}
hence l2r: "∀ q r . r2p r = q ⟶ (∃ w . (r2p w = q)) ∧ (p2r q = r)"
using p2r r2p by blast
{ fix r q assume ass: "(∃ w . (r2p w = q)) ∧ (p2r q = r)"
then obtain w where w: "r2p w = q" by blast
hence unique: "∀ a . q = r2p a ⟶ a = w" using uniqueroots by auto
have rdef: "r = (THE a . q = r2p a)" using ass r2p p2r by simp
have "q = r2p w" using w by simp
hence "q = r2p r" using theI[of "λ a. q = r2p a" "w"] rdef unique
by blast
}
hence "∀ q r . (∃ w . (r2p w = q)) ∧ (p2r q = r) ⟶ q = r2p r"
by blast
thus ?thesis using l2r by blast
qed
have equalr2p: "∀ x y . r2p x = r2p y ⟶ x = y" using bij by metis
have SbijRoots: "S = { y . ∃ x ∈ qroots a b c . y = r2p x }"
proof -
{ fix y assume y: "y ∈ S"
then obtain r where r: "y = r2p r" using r2p S assms by blast
hence "regularCone x (p ⊕ (r⊗D))" using r2p y S by auto
hence "r ∈ qroots a b c"
using lemWhereLineMeetsCone[of "a" "D" "b" "p" "x" "c" "r"]
a b c X by auto
hence "∃ r ∈ qroots a b c . y = r2p r" using r by blast
}
hence l2r: "S ⊆ { y . ∃ x ∈ qroots a b c . y = r2p x }" by blast
{ fix y assume y: "y ∈ { y . ∃ x ∈ qroots a b c . y = r2p x }"
then obtain r where r: "r ∈ qroots a b c ∧ y = r2p r" by blast
hence "regularCone x (r2p r)"
using lemWhereLineMeetsCone[of "a" "D" "b" "p" "x" "c" "r"]
a b c X r2p by auto
moreover have "r2p r ∈ l" using assms(3) r2p by auto
ultimately have "y ∈ S" using S r by auto
}
thus ?thesis using l2r by blast
qed
have equalcard: "((card (qroots a b c) = 1) ∨ (card (qroots a b c) = 2))
⟶ (card S = card (qroots a b c))"
proof -
{ assume cases: "card (qroots a b c) = 1 ∨ card (qroots a b c) = 2"
have case1: "card (qroots a b c) = 1 ⟶ (card S = card (qroots a b c))"
proof -
{ assume card1: "card (qroots a b c) = 1"
hence "∃ r . (qroots a b c) = {r}" by (meson card_1_singletonE)
then obtain r where r: "(qroots a b c) = {r}" by blast
hence l2r: "{ r2p r } ⊆ S" using SbijRoots by auto
{ fix y assume y: "y ∈ S"
then obtain x where x: "x ∈ qroots a b c ∧ y = r2p x"
using SbijRoots by blast
hence "r2p r = y" using bij using r by auto
}
hence "∀ y . y ∈ S ⟶ y ∈ { r2p r }" by auto
hence "S = { r2p r }" using l2r by blast
hence "∃ r . S = {r}" by blast
hence "card S = 1"
using card_1_singleton_iff[of "S"] by auto
}
thus ?thesis by auto
qed
have case2: "card (qroots a b c) = 2 ⟶ (card S = card (qroots a b c))"
proof -
{ assume card2: "card (qroots a b c) = 2"
hence "∃ r1 r2 . (qroots a b c) = {r1, r2} ∧ r1 ≠ r2"
using card_2_iff by blast
then obtain r1 r2 where rs: "(qroots a b c) = {r1,r2} ∧ r1≠r2" by blast
hence l2r: "{ r2p r1, r2p r2} ⊆ S" using SbijRoots by auto
{ fix y assume y: "y ∈ S"
then obtain x where x: "x ∈ qroots a b c ∧ y = r2p x"
using SbijRoots by blast
hence "x = r1 ∨ x = r2" using rs by auto
hence "r2p r1 = y ∨ r2p r2 = y" using x by blast
}
hence "∀ y . y ∈ S ⟶ y ∈ { r2p r1, r2p r2 }" by auto
hence S2: "S = { r2p r1, r2p r2 }" using l2r by blast
moreover have "r2p r1 ≠ r2p r2" using rs bij by metis
ultimately have "∃ y1 y2 . S = {y1, y2} ∧ y1≠y2" by blast
hence "card S = 2" using card_2_iff by blast
}
thus ?thesis by auto
qed
hence "(card S = card (qroots a b c))" using case1 cases by auto
}
thus ?thesis by auto
qed
have qc1: "¬ qcase1 a b c" using cpos by auto
have qc2: "¬ qcase2 a b c"
proof -
{ assume "qcase2 a b c"
hence qc2: "a = 0 ∧ b = 0 ∧ c > 0" using d cpos by auto
have llD: "lightlike D" using qc2 aval assms(2) by simp
have "sqr (X ⊙m D) = (mNorm2 X)*(mNorm2 D)"
using qc2 bval aval by simp
hence "orthogm X D" using llD lemSqrt0 by auto
hence parXD: "parallel X D"
using lemCausalOrthogmToLightlikeImpliesParallel tlX llD by auto
then obtain α where α: "α ≠ 0 ∧ X = (α ⊗ D)" by blast
have Dnot0: "origin ≠ D" using assms(2) by simp
hence "lightlike X"
proof -
have tsqr: "sqr (tval X) = (sqr α)* sqr (tval D)"
using lemSqrMult α by simp
have "sComponent X = (α ⊗s (sComponent D))" using α by simp
hence "sNorm2 (sComponent X) = (sqr α) * sNorm2 (sComponent D)"
using lemSNorm2OfScaled[of "α" "sComponent D"] by auto
hence "mNorm2 X = (sqr α) * mNorm2 D"
using lemMNorm2Decomposition[of "X"] tsqr
by (simp add: local.right_diff_distrib')
thus ?thesis using llD qc2 xnotp X by auto
qed
hence "False" using tlX by auto
}
thus ?thesis by auto
qed
have qc3: "qcase3 a b c ⟶ card S = 1"
proof -
{ assume "qcase3 a b c"
hence qc3: "qroots a b c = {(-c/b)}" using lemQCase3 by auto
hence "∃ val . (qroots a b c = {val})" by simp
hence "card (qroots a b c) = 1" using card_1_singleton_iff by auto
hence "card S = 1" using equalcard by auto
}
thus ?thesis by auto
qed
have qc4: "¬ qcase4 a b c"
proof -
{ assume "qcase4 a b c"
hence qc4: "a ≠ 0 ∧ d < 0" using d by auto
{ assume "a > 0"
hence tlD: "timelike D" using aval by auto
hence "sqr (X ⊙m D) ≥ (mNorm2 X)*(mNorm2 D)"
using lemReverseCauchySchwarz[of "X" "D"] tlX
using local.dual_order.order_iff_strict by blast
hence EQN: "4*sqr (X ⊙m D) ≥ 4*(mNorm2 X)*(mNorm2 D)"
using qc4 d dval local.leD by fastforce
have "(sqr b) < 4*a*c" using d qc4 by simp
hence "4*sqr (X ⊙m D) < 4*(mNorm2 X)*(mNorm2 D)"
using aval bval cval mult_assoc mult_commute
lemSqrMult[of "2" "(X ⊙m D)"] by auto
hence "False" using EQN by force
}
hence aneg: "a < 0" using qc4 by force
hence "4*a*c < 0" using cpos
by (simp add: local.mult_pos_neg local.mult_pos_neg2)
hence "d > sqr b" using d
by (metis add_commute local.add_less_same_cancel2 local.diff_add_cancel)
hence "d > 0"
using local.less_trans local.not_square_less_zero qc4 by blast
hence "False" using qc4 by auto
}
thus ?thesis by auto
qed
have qc5: "qcase5 a b c ⟶ card S = 1"
proof -
{
assume qc5: "qcase5 a b c"
hence "qroots a b c = {(-b/(2*a))}" using lemQCase5 by auto
hence "∃ val . qroots a b c = {val}" by simp
hence "card (qroots a b c) = 1" using card_1_singleton_iff by auto
hence "card S = 1" using equalcard by simp
}
thus ?thesis by simp
qed
have qc6: "qcase6 a b c ⟶ card S = 2"
proof -
{ define rd where rd: "rd = sqrt (discriminant a b c)"
define rp where rp: "rp = (-b + rd) / (2 * a)"
define rm where rm: "rm = (-b - rd) / (2 * a)"
assume qc6: "qcase6 a b c"
hence "rp ≠ rm ∧ qroots a b c = {rp, rm}"
using lemQCase6[of "a" "b" "c" "rd" "rp" "rm"] a b c rd rm rp
by auto
hence "∃ v1 v2 . qroots a b c = { v1, v2 } ∧ (v1 ≠ v2)" by blast
hence "card (qroots a b c) = 2" using card_2_iff[of "qroots a b c"] by blast
hence "card S = 2" using equalcard by simp
}
thus ?thesis by simp
qed
define n where n: "n = card S"
hence "(n = 1 ∨ n = 2)"
using qc1 qc2 qc3 qc4 qc5 qc6 lemQuadraticCasesComplete
by blast
hence "0 < n ≤ 2" by auto
thus ?thesis using n S by auto
qed
end
end