[WIP] Hilton-Milner formalization

AShortProofOfTheHiltonMilnerTheorem/AShortProofOfTheHiltonMilnerTheorem.lean

@@ -0,0 +1 @@
+import AShortProofOfTheHiltonMilnerTheorem.Main

AShortProofOfTheHiltonMilnerTheorem/AShortProofOfTheHiltonMilnerTheorem/Basic.lean

@@ -0,0 +1,82 @@
+import Mathlib
+
+/-!
+Shared definitions for the source-backed Hilton--Milner formalization.
+-/
+
+namespace AShortProofOfTheHiltonMilnerTheorem
+
+/-- A finite set system, represented as a finite family of finite subsets of `ℕ`. -/
+@[reducible] def SetFamily : Type := Finset (Finset ℕ)
+
+/-- The source ground set `[n] = {1, ..., n}`. -/
+def ground (n : ℕ) : Finset ℕ :=
+  Finset.Icc 1 n
+
+/-- All `k`-element subsets of the source ground set `[n]`. -/
+def kSubsets (n k : ℕ) : SetFamily :=
+  (ground n).powersetCard k
+
+/-- A finite family all of whose members are subsets of `[n]`. -/
+def FamilyOn (n : ℕ) (𝓕 : SetFamily) : Prop :=
+  ∀ ⦃F : Finset ℕ⦄, F ∈ 𝓕 → F ⊆ ground n
+
+/-- A finite family of `k`-element subsets of `[n]`. -/
+def UniformFamily (n k : ℕ) (𝓕 : SetFamily) : Prop :=
+  ∀ ⦃F : Finset ℕ⦄, F ∈ 𝓕 → F.card = k ∧ F ⊆ ground n
+
+/-- Pairwise-intersecting finite set family. -/
+def PairwiseIntersecting (𝓕 : SetFamily) : Prop :=
+  ∀ ⦃F G : Finset ℕ⦄, F ∈ 𝓕 → G ∈ 𝓕 → F ≠ G → (F ∩ G).Nonempty
+
+/-- Cross-intersecting finite set families. -/
+def CrossIntersecting (𝓐 𝓑 : SetFamily) : Prop :=
+  ∀ ⦃A B : Finset ℕ⦄, A ∈ 𝓐 → B ∈ 𝓑 → (A ∩ B).Nonempty
+
+/-- The total intersection of the family is empty. -/
+def EmptyTotalIntersection (𝓕 : SetFamily) : Prop :=
+  ∀ x : ℕ, ∃ F : Finset ℕ, F ∈ 𝓕 ∧ x ∉ F
+
+/-- After deleting any one member, the remaining family has empty total intersection. -/
+def DeletionEmptyTotalIntersection (𝓕 : SetFamily) : Prop :=
+  ∀ ⦃F₀ : Finset ℕ⦄, F₀ ∈ 𝓕 → ∀ x : ℕ,
+    ∃ F : Finset ℕ, F ∈ 𝓕 ∧ F ≠ F₀ ∧ x ∉ F
+
+/-- Replace `j` by `i` in a set when `j ∈ F` and `i ∉ F`. -/
+def shiftedSet (i j : ℕ) (F : Finset ℕ) : Finset ℕ :=
+  if j ∈ F ∧ i ∉ F then insert i (F.erase j) else F
+
+/-- The source combinatorial shifting operation `Shift_{i ← j}` on a set family. -/
+def shiftOperation (i j : ℕ) (𝓕 : SetFamily) : SetFamily :=
+  (𝓕.filter (fun F : Finset ℕ => j ∉ F ∨ i ∈ F ∨ shiftedSet i j F ∈ 𝓕)) ∪
+    ((𝓕.filter (fun F : Finset ℕ => j ∈ F ∧ i ∉ F)).image (shiftedSet i j))
+
+/-- Shiftedness over the ground set `[n]`. -/
+def ShiftedOn (n : ℕ) (𝓕 : SetFamily) : Prop :=
+  ∀ ⦃i j : ℕ⦄ ⦃F : Finset ℕ⦄,
+    i ∈ ground n → j ∈ ground n → i < j → F ∈ 𝓕 → j ∈ F → i ∉ F →
+      shiftedSet i j F ∈ 𝓕
+
+/-- The numerical upper bound in the main technical theorem. -/
+def mainTechnicalBound (n k : ℕ) : ℕ :=
+  Nat.choose n (k - 1) - Nat.choose (n - k) (k - 1) + 1
+
+/-- The numerical upper bound in the Hilton--Milner theorem. -/
+def hiltonMilnerBound (n k : ℕ) : ℕ :=
+  Nat.choose (n - 1) (k - 1) - Nat.choose (n - 1 - k) (k - 1) + 1
+
+/--
+The extremal Hilton--Milner family from the source uniqueness theorem: a single
+`k`-set `B`, together with all `k`-sets in `[n]` that contain `i` and intersect
+`B`.
+-/
+def hiltonMilnerFamily (n k i : ℕ) (B : Finset ℕ) : SetFamily :=
+  insert B ((kSubsets n k).filter (fun F : Finset ℕ => i ∈ F ∧ (F ∩ B).Nonempty))
+
+/-- The exact structural conclusion of the Hilton--Milner uniqueness theorem. -/
+def IsHiltonMilnerFamily (n k : ℕ) (𝓕 : SetFamily) : Prop :=
+  ∃ (B : Finset ℕ) (i : ℕ),
+    B ∈ kSubsets n k ∧ i ∈ ground n ∧ i ∉ B ∧
+      𝓕 = hiltonMilnerFamily n k i B
+
+end AShortProofOfTheHiltonMilnerTheorem

AShortProofOfTheHiltonMilnerTheorem/AShortProofOfTheHiltonMilnerTheorem/HiltonMilner.lean

@@ -0,0 +1,133 @@
+import AShortProofOfTheHiltonMilnerTheorem.MainTechnical
+import AShortProofOfTheHiltonMilnerTheorem.Shifting
+
+/-!
+Hilton--Milner theorem statements and uniqueness bridge lemmas.
+-/
+
+namespace AShortProofOfTheHiltonMilnerTheorem
+
+/--
+Source theorem `thm:HM`, lines 91--95; proof in lines 206--223.
+
+Source proof: first use the Frankl--Füredi shifting lemma to reduce to a shifted
+family.  Split the shifted family into sets containing `1` and sets not
+containing `1`; delete `1` from the first part to obtain `𝓐`, and call the
+second part `𝓑`.  Shiftedness gives `∂𝓑 ⊆ 𝓐`; pairwise intersection gives
+cross-intersection; empty total intersection gives nonemptiness of both parts.
+Then apply `thm:MainTechnical` on the remaining ground set.
+
+Prover notes: the Lean proof should make the reindexing from `{2, ..., n}` to a
+standard `[n-1]` ground set explicit, or add a companion bridge lemma for the
+binomial expression after deleting the distinguished element.
+-/
+theorem hiltonMilner (n k : ℕ) (𝓕 : SetFamily)
+    (hk : 0 < k) (hkn : 2 * k ≤ n)
+    (hF : UniformFamily n k 𝓕)
+    (hinter : PairwiseIntersecting 𝓕) (hempty : EmptyTotalIntersection 𝓕) :
+    𝓕.card ≤ hiltonMilnerBound n k := by
+  sorry
+
+/--
+Shifted-family uniqueness case used in source theorem `thm:StrictHM`, from the
+discussion at lines 303--326.
+
+Source proof: for shifted families, split the family as in the proof of
+Hilton--Milner.  The strict shifted variant `mainTechnical_shiftedStrictTwoB`
+rules out two or more exceptional sets, so equality forces exactly one
+exceptional `k`-set `B`; maximality then fills in all `k`-sets containing the
+center and intersecting `B`.
+
+Prover notes: this is the precise shifted classification that the final
+non-shifted theorem reduces to.  It should be proved before trying to use
+`strongShiftedReduction`.
+-/
+theorem strictHiltonMilner_shifted (n k : ℕ) (𝓕 : SetFamily)
+    (hk4 : 4 ≤ k) (hkn : 2 * k < n)
+    (hF : UniformFamily n k 𝓕)
+    (hinter : PairwiseIntersecting 𝓕) (hempty : EmptyTotalIntersection 𝓕)
+    (hshift : ShiftedOn n 𝓕)
+    (hmax : 𝓕.card = hiltonMilnerBound n k) :
+    IsHiltonMilnerFamily n k 𝓕 := by
+  sorry
+
+/--
+Non-deletion-empty bridge for source theorem `thm:StrictHM`.
+
+Source/proof bridge: if the strengthened deletion-empty property fails, then
+some member `F₀` and some element `i` have the property that every other member
+contains `i`.  The empty-total-intersection hypothesis forces `i ∉ F₀`.  Since
+the family is maximal, every `k`-set containing `i` and intersecting `F₀` must
+already be present; otherwise it could be added without breaking pairwise
+intersection or empty total intersection.  Thus the source HM form follows
+directly, without applying the strengthened shifting lemma.
+
+Prover notes: unfold `DeletionEmptyTotalIntersection` to obtain `F₀` and `i`;
+use maximality against the canonical `hiltonMilnerFamily n k i F₀`.
+-/
+lemma strictHiltonMilner_nonDeletionEmptyCase (n k : ℕ) (𝓕 : SetFamily)
+    (hk4 : 4 ≤ k) (hkn : 2 * k < n)
+    (hF : UniformFamily n k 𝓕)
+    (hinter : PairwiseIntersecting 𝓕) (hempty : EmptyTotalIntersection 𝓕)
+    (hmax : 𝓕.card = hiltonMilnerBound n k)
+    (hnotDelete : ¬ DeletionEmptyTotalIntersection 𝓕) :
+    IsHiltonMilnerFamily n k 𝓕 := by
+  sorry
+
+/--
+Deletion-empty bridge for source theorem `thm:StrictHM`.
+
+Source/proof bridge: under `DeletionEmptyTotalIntersection`, use
+`strongShiftedReduction` to reach a shifted family with no smaller cardinality.
+The Hilton--Milner upper bound and maximality force every size comparison in
+the reduction to be an equality.  Apply `strictHiltonMilner_shifted` to the
+shifted witness, then inspect the equality cases in the reduction: ordinary
+shifts must preserve the extremal HM structure, and any standard-family
+replacement can occur at equality only when the original family already has the
+same HM form.  This reflection step is the missing bridge between the existential
+shifted reduction and the final equality for the original family.
+
+Prover notes: do not use `strongShiftedReduction` as a black box only.  The proof
+must carry equality through its shift/replacement construction, using the source
+standard-family comparison when a replacement occurs.
+-/
+lemma strictHiltonMilner_deletionEmptyReduction (n k : ℕ) (𝓕 : SetFamily)
+    (hk4 : 4 ≤ k) (hkn : 2 * k < n)
+    (hF : UniformFamily n k 𝓕)
+    (hinter : PairwiseIntersecting 𝓕) (hempty : EmptyTotalIntersection 𝓕)
+    (hdelete : DeletionEmptyTotalIntersection 𝓕)
+    (hmax : 𝓕.card = hiltonMilnerBound n k) :
+    IsHiltonMilnerFamily n k 𝓕 := by
+  sorry
+
+/--
+Source theorem `thm:StrictHM`, lines 295--301; proof discussion lines 303--326.
+
+Source proof: first prove the shifted classification using the strict shifted
+variant of `thm:MainTechnical`.  For a non-shifted family, split on the stronger
+deletion-empty property from the final source lemma.  If it fails, all but one
+set contain a common center, and maximality directly gives the HM family.  If it
+holds, use the strengthened shifting reduction, but carry equality through the
+reduction so that the HM form of the shifted extremal witness reflects back to
+the original family.
+
+Prover notes: prove `strictHiltonMilner_shifted`, then the two bridge lemmas
+`strictHiltonMilner_nonDeletionEmptyCase` and
+`strictHiltonMilner_deletionEmptyReduction`; the latter is the explicit bridge
+showing that `strongShiftedReduction` is sufficient for uniqueness, not merely
+for obtaining some shifted family of no smaller cardinality.
+-/
+theorem strictHiltonMilner (n k : ℕ) (𝓕 : SetFamily)
+    (hk4 : 4 ≤ k) (hkn : 2 * k < n)
+    (hF : UniformFamily n k 𝓕)
+    (hinter : PairwiseIntersecting 𝓕) (hempty : EmptyTotalIntersection 𝓕)
+    (hmax : 𝓕.card = hiltonMilnerBound n k) :
+    ∃ (B : Finset ℕ) (i : ℕ),
+      B ∈ kSubsets n k ∧ i ∈ ground n ∧ i ∉ B ∧
+        𝓕 = hiltonMilnerFamily n k i B := by
+  classical
+  by_cases hdelete : DeletionEmptyTotalIntersection 𝓕
+  · exact strictHiltonMilner_deletionEmptyReduction n k 𝓕 hk4 hkn hF hinter hempty hdelete hmax
+  · exact strictHiltonMilner_nonDeletionEmptyCase n k 𝓕 hk4 hkn hF hinter hempty hmax hdelete
+
+end AShortProofOfTheHiltonMilnerTheorem

AShortProofOfTheHiltonMilnerTheorem/AShortProofOfTheHiltonMilnerTheorem/Main.lean

@@ -0,0 +1,19 @@
+import AShortProofOfTheHiltonMilnerTheorem.Basic
+import AShortProofOfTheHiltonMilnerTheorem.MainTechnical
+import AShortProofOfTheHiltonMilnerTheorem.Shifting
+import AShortProofOfTheHiltonMilnerTheorem.HiltonMilner
+
+/-! # A Short Proof of the Hilton--Milner Theorem
+
+Source-backed Lean statements for Bulavka and Woodroofe's short proof of the
+Hilton--Milner theorem.
+
+## File layout
+
+- `Basic`: finite-family, uniformity, intersection, shifting, and extremal-family
+  definitions shared by the whole project.
+- `MainTechnical`: the main technical inequality and shifted/strict variants.
+- `Shifting`: Frankl--Füredi and strengthened shifting reductions.
+- `HiltonMilner`: the Hilton--Milner upper bound, uniqueness statement, and bridge
+  lemmas for the equality case.
+-/

AShortProofOfTheHiltonMilnerTheorem/AShortProofOfTheHiltonMilnerTheorem/MainTechnical.lean

@@ -0,0 +1,70 @@
+import AShortProofOfTheHiltonMilnerTheorem.Basic
+
+/-!
+Source-backed statements for the main technical inequality and shifted variants.
+-/
+
+namespace AShortProofOfTheHiltonMilnerTheorem
+
+/--
+Source theorem `thm:MainTechnical`, lines 106--115.
+
+Source proof: the paper proves this by induction on `n`.  The base case
+`n = 2k - 1` uses complements.  The inductive step shifts the families, splits
+according to whether a set contains `n`, applies induction to the not-`n` and
+containing/deleted parts, treats the empty cases for `𝓑(n)`, and finishes by
+Pascal identities for binomial coefficients.
+
+Prover notes: introduce the two split families, prove the shadow and
+cross-intersection hypotheses are inherited, use `Finset.card_powersetCard`,
+`Finset.mem_shadow_iff`, and `Nat.choose` recurrence lemmas for the counting
+part.
+-/
+theorem mainTechnical (n k : ℕ) (𝓐 𝓑 : SetFamily)
+    (hk : 0 < k) (hkn : 2 * k ≤ n + 1)
+    (hA : UniformFamily n (k - 1) 𝓐) (hB : UniformFamily n k 𝓑)
+    (hcross : CrossIntersecting 𝓐 𝓑) (hne : 𝓑.Nonempty)
+    (hshadow : Finset.shadow 𝓑 ⊆ 𝓐) :
+    𝓐.card + 𝓑.card ≤ mainTechnicalBound n k := by
+  sorry
+
+/--
+Source remark `line-224`, lines 224--227.
+
+Source proof: no separate proof is given; the paper observes that the proof of
+Hilton--Milner only needs the shifted special case of `thm:MainTechnical`.
+
+Prover notes: once `mainTechnical` is available this follows immediately, but
+it is kept as a separate source-backed target because the paper highlights the
+shifted case as the actual dependency of the HM proof.
+-/
+theorem mainTechnical_shiftedSpecialCase (n k : ℕ) (𝓐 𝓑 : SetFamily)
+    (hk : 0 < k) (hkn : 2 * k ≤ n + 1)
+    (hA : UniformFamily n (k - 1) 𝓐) (hB : UniformFamily n k 𝓑)
+    (hcross : CrossIntersecting 𝓐 𝓑) (hne : 𝓑.Nonempty)
+    (hshadow : Finset.shadow 𝓑 ⊆ 𝓐)
+    (_hshiftA : ShiftedOn n 𝓐) (_hshiftB : ShiftedOn n 𝓑) :
+    𝓐.card + 𝓑.card ≤ mainTechnicalBound n k := by
+  exact mainTechnical n k 𝓐 𝓑 hk hkn hA hB hcross hne hshadow
+
+/--
+Source proof-discussion helper from the uniqueness section, lines 303--326.
+
+Source proof: for shifted families, the proof of `thm:MainTechnical` can be
+modified by strengthening `𝓑.Nonempty` to `2 ≤ 𝓑.card`.  If `𝓑(n)` is empty,
+the two-element hypothesis makes the estimate for `𝓐(n)` strict; if `𝓑(n)` is
+nonempty, the equation `(2)` estimate is already strict when `4 ≤ k`.
+
+Prover notes: reuse the induction split from `mainTechnical`, but carry strict
+inequalities through the two cases for the containing-`n` part.
+-/
+theorem mainTechnical_shiftedStrictTwoB (n k : ℕ) (𝓐 𝓑 : SetFamily)
+    (hk4 : 4 ≤ k) (hkn : 2 * k ≤ n + 1)
+    (hA : UniformFamily n (k - 1) 𝓐) (hB : UniformFamily n k 𝓑)
+    (hcross : CrossIntersecting 𝓐 𝓑) (hcardB : 2 ≤ 𝓑.card)
+    (hshadow : Finset.shadow 𝓑 ⊆ 𝓐)
+    (hshiftA : ShiftedOn n 𝓐) (hshiftB : ShiftedOn n 𝓑) :
+    𝓐.card + 𝓑.card < mainTechnicalBound n k := by
+  sorry
+
+end AShortProofOfTheHiltonMilnerTheorem