diff --git a/AShortProofOfTheHiltonMilnerTheorem/AShortProofOfTheHiltonMilnerTheorem.lean b/AShortProofOfTheHiltonMilnerTheorem/AShortProofOfTheHiltonMilnerTheorem.lean new file mode 100644 index 0000000..2540e1d --- /dev/null +++ b/AShortProofOfTheHiltonMilnerTheorem/AShortProofOfTheHiltonMilnerTheorem.lean @@ -0,0 +1 @@ +import AShortProofOfTheHiltonMilnerTheorem.Main diff --git a/AShortProofOfTheHiltonMilnerTheorem/AShortProofOfTheHiltonMilnerTheorem/Basic.lean b/AShortProofOfTheHiltonMilnerTheorem/AShortProofOfTheHiltonMilnerTheorem/Basic.lean new file mode 100644 index 0000000..e775df4 --- /dev/null +++ b/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 diff --git a/AShortProofOfTheHiltonMilnerTheorem/AShortProofOfTheHiltonMilnerTheorem/Blueprint.md b/AShortProofOfTheHiltonMilnerTheorem/AShortProofOfTheHiltonMilnerTheorem/Blueprint.md new file mode 100644 index 0000000..631f7af --- /dev/null +++ b/AShortProofOfTheHiltonMilnerTheorem/AShortProofOfTheHiltonMilnerTheorem/Blueprint.md @@ -0,0 +1,176 @@ +# Formalization Blueprint: docs/source/A_short_proof_of_the_Hilton-Milner_theorem.tex + +- Source: `docs/source/A_short_proof_of_the_Hilton-Milner_theorem.tex` +- Nearby PDF checked: `docs/bulavka_woodroofe2024_hilton_milner.pdf` +- Target Lean entry file: `AShortProofOfTheHiltonMilnerTheorem/Main.lean` +- Status: statement/source review approved; strict Hilton--Milner bridge corrections added for proof handoff. Lean proofs remain as `sorry` skeletons for a user-started prove workflow. + +## Planner Checklist + +- [x] Identify definitions and notation that must exist before theorem statements. +- [x] Split large source theorems into Lean-sized lemmas. +- [x] Record source labels/pages/equations for every generated declaration. +- [x] Check local project and Mathlib names before introducing duplicates. +- [x] Verify drafted Lean statements match the source document. +- [x] Run independent statement/source verification review and apply corrections. +- [x] Attach the complete source proof text when available, or explicitly record why it is unavailable. +- [x] Record a natural-language proof strategy or source proof pointer for each theorem/lemma. +- [x] Resolve all construction stubs before proof handoff. +- [x] Mark stable theorem/lemma/example `sorry` declarations ready for a user-started prove workflow. (Checked after independent review stamped every source entry.) + +## Import Plan + +Direct Lean imports expected in generated Lean files only: +- `Mathlib` + +Root coverage: +- `AShortProofOfTheHiltonMilnerTheorem.lean` imports `AShortProofOfTheHiltonMilnerTheorem.Main`. + +## Suggested Search Modules + +Non-gating modules or namespaces to search while proving. Do not force these into `.lean` imports unless the prover actually needs them. +- `Mathlib.Combinatorics.SetFamily.Shadow` for `Finset.shadow`, `Finset.mem_shadow_iff`, and shadow monotonicity. +- `Mathlib.Combinatorics.SetFamily.Intersecting` for Mathlib's `Set.Intersecting` reference definition. +- `Mathlib.Data.Finset.Powerset` for `Finset.powersetCard` and cardinality of fixed-size subsets. +- `Mathlib.Data.Nat.Choose.Basic` and nearby binomial lemmas for Pascal identities. +- `Mathlib.Data.Finset.Interval` for `Finset.Icc` facts about the ground set `[n]`. + +Search notes from the planner refresh: +- `Finset.powersetCard`, `Finset.mem_powersetCard`, and `Finset.card_powersetCard` are the Mathlib fixed-cardinality subset interface. +- `Finset.shadow`, `Finset.mem_shadow_iff`, `Finset.shadow_mono`, and `Finset.shadow_monotone` are the Mathlib shadow interface matching the source shadow under uniformity. +- `Nat.choose_succ_succ`, `Nat.choose_succ_left`, and `Nat.choose_succ_right` are the likely Pascal/binomial recurrence lemmas. + +## Generated File Layout + +- Aggregator entry file: `AShortProofOfTheHiltonMilnerTheorem/Main.lean` +- `AShortProofOfTheHiltonMilnerTheorem/Basic.lean`: finite-family, uniformity, intersection, shifting, and extremal-family definitions. +- `AShortProofOfTheHiltonMilnerTheorem/MainTechnical.lean`: the main technical inequality and shifted/strict variants. +- `AShortProofOfTheHiltonMilnerTheorem/Shifting.lean`: Frankl--Furedi and strengthened shifting reductions. +- `AShortProofOfTheHiltonMilnerTheorem/HiltonMilner.lean`: the HM bound, uniqueness statement, and equality-case bridge lemmas. + +## Lean Representation Plan + +The source works with finite set systems of subsets of `[n] = {1, ..., n}`. The Lean draft uses finite set families directly: + +- `SetFamily := Finset (Finset ℕ)` represents a finite family of finite sets of natural numbers. +- `ground n := Finset.Icc 1 n` represents `[n]`. +- `kSubsets n k := (ground n).powersetCard k` represents all `k`-element subsets of `[n]`. +- `FamilyOn n 𝓕` and `UniformFamily n k 𝓕` record that every member of `𝓕` lies in `[n]` and has cardinality `k`. +- `PairwiseIntersecting 𝓕` says distinct members of `𝓕` have nonempty intersection. +- `CrossIntersecting 𝓐 𝓑` says every `A ∈ 𝓐` intersects every `B ∈ 𝓑`. +- `EmptyTotalIntersection 𝓕` says no natural number is contained in all members of `𝓕`. +- `DeletionEmptyTotalIntersection 𝓕` formalizes the strengthened property in the final lemma: after deleting any fixed `F₀`, the remaining family has empty total intersection. +- `shiftedSet`, `shiftOperation`, and `ShiftedOn n 𝓕` formalize the shifting definition from lines 138-146. +- `Finset.shadow 𝓑` is Mathlib's one-element-deletion shadow. Under `UniformFamily n k 𝓑`, this matches the source shadow of all `(k-1)`-subsets of members of `𝓑`. +- `mainTechnicalBound n k` and `hiltonMilnerBound n k` name the two binomial upper bounds. +- `hiltonMilnerFamily n k i B` represents the extremal family consisting of `B` and all `k`-sets in `[n]` that contain `i` and intersect `B`. +- `IsHiltonMilnerFamily n k 𝓕` names the exact existential conclusion of the uniqueness theorem, so bridge lemmas can pass the HM structure around without duplicating the long existential. + +Representation bridge notes: +- The source's inequalities `2k - 1 ≤ n`, `k ≤ n/2`, and `k < n/2` are encoded over naturals as `2 * k ≤ n + 1`, `2 * k ≤ n`, and `2 * k < n` respectively. +- The draft adds `0 < k` where the source uses `(k-1)`-element families but leaves positivity implicit. This is a domain clarification for natural-number indexing, not intended as a mathematical weakening for the paper's positive-uniformity setting. + +## Source Statement Inventory + +### thm:HM + +- Kind: theorem +- Source locator: `docs/source/A_short_proof_of_the_Hilton-Milner_theorem.tex:91-95`; proof at lines 198-223 after Lemma `lem:Frankl-Furedi` is introduced. +- Planned Lean declarations: `hiltonMilner`; supporting definitions `SetFamily`, `ground`, `UniformFamily`, `PairwiseIntersecting`, `EmptyTotalIntersection`, `hiltonMilnerBound`. +- Dependencies: `franklFurediShifted`, `mainTechnical`, shifting definitions, shadow containment for the HM split families. +- Formal statement review: Lean states the cardinal upper bound for any finite family of `k`-element subsets of `[n]` that is pairwise intersecting and has empty total intersection. The source condition `k ≤ n/2` is encoded as `2 * k ≤ n`; the conclusion is `𝓕.card ≤ hiltonMilnerBound n k`. +- Source qualifiers: mathematical object class is a finite family of `k`-element subsets of `[n]`; quantifiers are over natural parameters `n k` and a family `𝓕`; parameter domain includes `k ≤ n/2` and implicit positive `k`; side conditions are pairwise intersection and empty total intersection; output is an upper bound on `|𝓕|` by the stated binomial expression. +- Lean coverage: `UniformFamily n k 𝓕` covers `k`-element subsets of `[n]`; `PairwiseIntersecting 𝓕` covers pairwise-intersecting; `EmptyTotalIntersection 𝓕` covers `⋂_{F∈𝓕} F = ∅`; `2 * k ≤ n` covers `k ≤ n/2`; `hiltonMilnerBound` is exactly `{n-1 choose k-1} - {n-1-k choose k-1} + 1` using `Nat.choose`. +- Scope changes: finite-family representation by `Finset`; explicit `0 < k`; natural-arithmetic encoding of `k ≤ n/2` as `2 * k ≤ n`. +- Statement verification status: approved by codex verifier +- Complete source proof: Given the lemma, the proof of Theorem~\ref{thm:HM} is nearly immediate. Let $\mathcal{F}$ be a shifted family satisfying the conditions of the theorem. Define $\mathcal{A}=\{F\setminus1 : F\in\mathcal{F}\text{ with }1\in\mathcal{F}\}$ and $\mathcal{B}=\{F : F\in\mathcal{F}\text{ with }1\notin\mathcal{F}\}$. Since $\mathcal{F}$ is shifted, if $F\in\mathcal{F}$ does not have $1$, then $(F\setminus i)\cup1\in\mathcal{F}$ for each $i\in F$. It follows that $\partial\mathcal{B}\subseteq\mathcal{A}$. Since $\mathcal{F}$ is intersecting, also $\mathcal{A},\mathcal{B}$ are cross-intersecting systems of subsets of $\{2,\dots,n\}$. Since $\mathcal{F}$ has empty intersection, both of $\mathcal{A},\mathcal{B}$ are nonempty. The desired bound is now immediate from Theorem~\ref{thm:MainTechnical}. +- Source proof / prover notes: First use `franklFurediShifted` to reduce to shifted `𝓕`. Split members according to whether they contain `1`, deleting `1` from the containing part to define `𝓐`, and keeping the non-containing part as `𝓑` on the remaining ground set. Prove shadow containment from shiftedness, cross-intersection from pairwise intersection, and nonemptiness from empty total intersection. Apply `mainTechnical` with the ground set reindexed from `{2, ..., n}` to `[n-1]`; the binomial expression then matches `hiltonMilnerBound`. + +### thm:MainTechnical + +- Kind: theorem +- Source locator: `docs/source/A_short_proof_of_the_Hilton-Milner_theorem.tex:106-115`; proof at lines 155-196. +- Planned Lean declarations: `mainTechnical`; supporting definitions `UniformFamily`, `CrossIntersecting`, `mainTechnicalBound`. +- External Mathlib reference in the statement: Finset shadow for the source shadow operator. +- Dependencies: shifting preservation facts, induction on `n`, fixed-size subset counting, binomial/Pascal identities, complement argument in the base case. +- Formal statement review: Lean states the source inequality for finite families `𝓐` of `(k-1)`-sets and `𝓑` of `k`-sets in `[n]`, with cross-intersection, nonempty `𝓑`, and `Finset.shadow 𝓑 ⊆ 𝓐`. +- Source qualifiers: object classes are two uniform finite set families over `[n]`; quantifier order is `n`, `k`, `𝓐`, `𝓑`; parameter domain is `2k-1 ≤ n` and implicit `0 < k`; side conditions are cross-intersection, nonempty `𝓑`, and shadow containment; output is the cardinal inequality with binomial bound `{n choose k-1} - {n-k choose k-1} + 1`. +- Lean coverage: `hkn : 2 * k ≤ n + 1` encodes `2k-1 ≤ n`; `UniformFamily n (k - 1) 𝓐` and `UniformFamily n k 𝓑` cover the uniform families; `CrossIntersecting 𝓐 𝓑` covers cross-intersection; `𝓑.Nonempty` covers nonempty `𝓑`; `Finset.shadow 𝓑 ⊆ 𝓐` covers `∂𝓑 ⊆ 𝓐`; `mainTechnicalBound` covers the exact numeric bound. +- Scope changes: finite-family representation by `Finset`; explicit `0 < k`; natural-arithmetic encoding `2 * k ≤ n + 1`; Mathlib one-step shadow used with the uniformity bridge noted above. +- Statement verification status: approved by codex verifier +- Complete source proof: We carry out a straightforward induction on $n$. If $n=2k-1$, then the upper bound is ${n \choose k-1}$, and the result follows by noticing that if a $(k-1)$-element set is in $\mathcal{A}$, then its complement cannot be in $\mathcal{B}$ (and vice-versa). For the inductive step, we may assume that $\mathcal{A}$ and $\mathcal{B}$ are shifted; otherwise, shift. Let $\mathcal{A}(\neg n),\mathcal{B}(\neg n)$ consist of the subsets in $\mathcal{A},\mathcal{B}$ that do not contain $n$. It is immediate that these are shifted, cross-intersecting, and satisfy the shadow condition. Let $\mathcal{A}(n),\mathcal{B}(n)$ be obtained by taking subsets that contain $n$, then deleting $n$. These are also shifted, cross-intersecting, and satisfy the shadow condition. As $\mathcal{A}$ and $\mathcal{B}$ are shifted, $\mathcal{A}(\neg n)$ and $\mathcal{B}(\neg n)$ are nonempty, so induction gives equation (1): $|\mathcal{A}(\neg n)|+|\mathcal{B}(\neg n)|\leq {n-1\choose k-1}-{n-1-k\choose k-1}+1$. For $\mathcal{A}(n),\mathcal{B}(n)$: if $\mathcal{A}(n)$ is empty then the shadow condition makes $\mathcal{B}(n)$ empty; if $\mathcal{B}(n)$ is empty, shiftedness and nonempty $\mathcal{B}$ give $\{1,\dots,k\}\in\mathcal{B}$, so every set in $\mathcal{A}(n)$ intersects it and $|\mathcal{A}(n)|\leq {n-1\choose k-2}-{n-1-k\choose k-2}$; if $\mathcal{B}(n)$ is nonempty, induction gives equation (2), $|\mathcal{A}(n)|+|\mathcal{B}(n)|\leq {n-1\choose k-2}-{n-1-k\choose k-2}$. Combine with Pascal's identity. +- Source proof / prover notes: Formal proof should introduce no-containing and containing/deleted subfamilies, prove they partition both families by membership of `n`, apply induction to the not-`n` part and either induction or direct counting to the `n` part, then finish with `Nat.choose` Pascal identities. Search `Finset.card_powersetCard`, `Finset.mem_shadow_iff`, and `Nat.choose` recurrence lemmas. + +### lem:Frankl-Furedi + +- Kind: lemma +- Source locator: `docs/source/A_short_proof_of_the_Hilton-Milner_theorem.tex:201-206`; proof at lines 230-255. +- Planned Lean declarations: `franklFurediShifted`; supporting definitions `ShiftedOn`, `shiftOperation`, `UniformFamily`, `PairwiseIntersecting`, `EmptyTotalIntersection`. +- Dependencies: combinatorial shifting operation, preservation of pairwise intersection and cardinality under shifts, termination of repeated shifts, and the fallback argument using the boundary of `{1, ..., k+1}`. +- Formal statement review: Lean states existence of a shifted family `𝓕'` on the same ground set with the same uniformity, pairwise-intersection, and empty-total-intersection properties, and with `𝓕.card ≤ 𝓕'.card`. +- Source qualifiers: object class is a pairwise-intersecting family of `k`-element subsets of `[n]`; side condition is empty total intersection; output codomain is an existential shifted family satisfying the same properties and cardinality at least the original. +- Lean coverage: `UniformFamily n k 𝓕`, `PairwiseIntersecting 𝓕`, `EmptyTotalIntersection 𝓕`; existential witness `𝓕' : SetFamily` with `ShiftedOn n 𝓕'`, same properties, and `𝓕.card ≤ 𝓕'.card`. +- Scope changes: finite-family representation by `Finset`; explicit `0 < k`; shiftedness is restricted to `i,j ∈ ground n`, matching shifts over `[n]`. +- Statement verification status: approved by codex verifier +- Complete source proof: Given $\mathcal{F}$ as in Theorem~\ref{thm:HM}, apply shifting operations $\operatorname{Shift}_{i\leftarrow j}$. Each such operation preserves the pairwise-intersecting property and cardinality, but may or may not result in a system with a common element of intersection. If a sequence of shifting operations ends in a shifted system with empty intersection, then we are done. Otherwise, some shift results in a system where every set contains $i_0$. Before this step every set contains either $i_0$ or $j_0$. Relabel to `1` and `2`, continue shifting over all `3 ≤ i < j`. Then `{1,3,...,k+1}` and `{2,3,...,k+1}` are in the system. Since every set contains `1` or `2`, add all `k`-element subsets containing `{1,2}` if needed. Thus the boundary of `{1,...,k+1}` is contained in the system; it has empty intersection and is preserved by further shifts, so shifting to stability gives the result. +- Source proof / prover notes: This is the deepest shifting reduction. The proof likely needs separate lemmas for shift preservation, a finite termination measure for repeated shifts, relabeling invariance, and the boundary subfamily witness for empty intersection. Do not try to prove it by pure simplification. + +### line-224 + +- Kind: remark formalized as a theorem-shaped special case +- Source locator: `docs/source/A_short_proof_of_the_Hilton-Milner_theorem.tex:224-227` +- Planned Lean declarations: `mainTechnical_shiftedSpecialCase`. +- Dependencies: same as `mainTechnical`, plus `ShiftedOn n 𝓐` and `ShiftedOn n 𝓑` hypotheses. +- Formal statement review: The source remark is meta-mathematical: the HM proof needs only the shifted case of Theorem 2. The Lean declaration records the mathematical shifted special case by adding shiftedness hypotheses to `mainTechnical` and retaining the same conclusion. +- Source qualifiers: follow-on claim about the preceding proof's dependency on a shifted-special-case theorem. +- Lean coverage: `mainTechnical_shiftedSpecialCase` covers the shifted-special-case theorem. It does not formalize proof-dependency minimality itself. +- Scope changes: partial coverage of a prose remark; converted to a theorem statement rather than a meta-theorem about the proof script. +- Statement verification status: approved by codex verifier +- Complete source proof: no separate proof text; the remark says, "This proof requires only the special case of Theorem~\ref{thm:MainTechnical} where the set systems are shifted." +- Source proof / prover notes: Once `mainTechnical` is proved this special case follows immediately, but in the source it is intended as a possible independent target for the HM proof. + +### proof-discussion-strict-main-technical + +- Kind: theorem helper extracted from proof discussion. +- Source locator: `docs/source/A_short_proof_of_the_Hilton-Milner_theorem.tex:303-326` in the uniqueness section. +- Planned Lean declarations: `mainTechnical_shiftedStrictTwoB`. +- Dependencies: shifted version of `mainTechnical`, induction split used in `thm:MainTechnical`, the strict `|𝓑| ≥ 2` case analysis, and binomial inequalities around equation `(2)`. +- Formal statement review: Lean records the shifted strict variant explicitly: for shifted cross-intersecting families satisfying the shadow condition, if `4 ≤ k`, `2k - 1 ≤ n`, and `𝓑` has at least two members, then the same upper bound from `mainTechnical` is not attained. +- Source qualifiers: object classes are the same two uniform shifted finite set families as in the shifted special case of Theorem 2; parameter domain includes `k ≥ 4`, `2k - 1 ≤ n`, and `|𝓑| ≥ 2`; side conditions are cross-intersection, shadow containment, and shiftedness; output is the strict inequality `|𝓐| + |𝓑| < {n \choose k-1} - {n-k \choose k-1} + 1`. +- Lean coverage: `hk4 : 4 ≤ k`; `hkn : 2 * k ≤ n + 1`; `UniformFamily n (k - 1) 𝓐` and `UniformFamily n k 𝓑`; `CrossIntersecting 𝓐 𝓑`; `hcardB : 2 ≤ 𝓑.card`; `Finset.shadow 𝓑 ⊆ 𝓐`; `ShiftedOn n 𝓐`; `ShiftedOn n 𝓑`; conclusion `𝓐.card + 𝓑.card < mainTechnicalBound n k`. +- Scope changes: finite-family representation by `Finset`; natural-arithmetic encoding `2 * k ≤ n + 1`; this helper covers only the shifted proof-discussion variant, not a separate non-shifted theorem. +- Statement verification status: approved by codex verifier +- Complete source proof: The proof for a shifted family requires a straightforward modification of Theorem~\ref{thm:MainTechnical}. Require `k ≥ 4` and strengthen nonempty `\mathcal{B}` to `|\mathcal{B}| ≥ 2`; with this strengthened hypothesis, the inequality is strict. In the induction step, `\mathcal{B}(n)` is empty or nonempty. If empty, then because `\mathcal{B}` has at least two elements, `\mathcal{A}(n)` is strictly smaller than the displayed bound. If nonempty, the bound in equation `(2)` is already strict when `k ≥ 4`. Hence each induction step yields a strict inequality. +- Source proof / prover notes: Reuse the split-family proof of `mainTechnical`, but strengthen the estimates for the containing-`n` part. In the empty `𝓑(n)` case use `2 ≤ 𝓑.card` to avoid equality; in the nonempty case use the strictness of the final binomial comparison for `k ≥ 4`. + +### thm:StrictHM + +- Kind: theorem +- Source locator: `docs/source/A_short_proof_of_the_Hilton-Milner_theorem.tex:295-301`; proof discussion at lines 303-326 and dependent lemma at lines 328-363. +- Planned Lean declarations: `strictHiltonMilner`; supporting definitions `hiltonMilnerFamily` and `IsHiltonMilnerFamily`; supporting lemmas `mainTechnical_shiftedStrictTwoB`, `strictHiltonMilner_shifted`, `strictHiltonMilner_nonDeletionEmptyCase`, `strictHiltonMilner_deletionEmptyReduction`, and `strongShiftedReduction`. +- Dependencies: `hiltonMilner`, shifted strict variant `mainTechnical_shiftedStrictTwoB`, shifted classification `strictHiltonMilner_shifted`, the non-deletion-empty maximality bridge, the deletion-empty reflection bridge using `strongShiftedReduction`, and the extremal-family construction. +- Formal statement review: Lean states that if the HM hypotheses hold, `4 ≤ k`, `2 * k < n`, and the HM upper bound is achieved, then `𝓕` equals `hiltonMilnerFamily n k i B` for some `B ∈ kSubsets n k` and `i ∈ ground n` with `i ∉ B`. +- Source qualifiers: object class and hypotheses are those of `thm:HM`; additional parameter domain `4 ≤ k < n/2`; equality/image condition is attaining the upper bound; output is existence of a `k`-set `B` and element `i ∉ B` such that the family consists exactly of `B` plus all `k`-sets containing `i` and intersecting `B`. +- Lean coverage: HM hypotheses are repeated as `UniformFamily`, `PairwiseIntersecting`, and `EmptyTotalIntersection`; `hmax : 𝓕.card = hiltonMilnerBound n k` covers attaining the upper bound; `hiltonMilnerFamily` and `IsHiltonMilnerFamily` cover the exact family description; `B ∈ kSubsets n k`, `i ∈ ground n`, and `i ∉ B` cover the existential qualifiers. +- Scope changes: finite-family representation by `Finset`; strict `k < n/2` encoded as `2 * k < n`; Lean explicitly asserts `i ∈ [n]` and `B ⊆ [n]`, which are implicit in the source family description. +- Statement verification status: approved by codex verifier +- Complete source proof: The source requires `k ≥ 4` to avoid technicalities and reduce to shifted families. For shifted families, modify Theorem~\ref{thm:MainTechnical} by strengthening nonempty `\mathcal{B}` to `|\mathcal{B}| ≥ 2`; with this strengthened hypothesis the inequality is strict. If `\mathcal{B}(n)` is empty, `|\mathcal{B}| ≥ 2` makes `\mathcal{A}(n)` strictly smaller than the bound. If `\mathcal{B}(n)` is nonempty, the bound in equation (2) is already strict when `k ≥ 4`. Thus the induction step yields a strict inequality. Theorem~\ref{thm:StrictHM} follows for shifted families by applying this variant to the same split families as in the HM proof. For non-shifted families, split on `DeletionEmptyTotalIntersection`. If it fails, some `F₀` and center `i` make every other set contain `i`; empty total intersection gives `i ∉ F₀`, and maximality fills exactly the HM family. If it holds, apply the strengthened shifting lemma, use the HM upper bound and maximality to force equality throughout the reduction, classify the shifted witness, and reflect the equality case back through the shifts or standard-family replacement. +- Source proof / prover notes: Use `mainTechnical_shiftedStrictTwoB` to prove the shifted classification `strictHiltonMilner_shifted`. Then prove `strictHiltonMilner_nonDeletionEmptyCase` for the failure of the deletion-empty property. In the deletion-empty case, `strictHiltonMilner_deletionEmptyReduction` must not treat `strongShiftedReduction` as a mere black box: it must carry equality through the reduction and show that the shifted witness having HM form implies the original family already has HM form. +- Proof bridge helper declarations: + - `strictHiltonMilner_shifted`: shifted equality case from the strict variant of the main technical theorem. + - `strictHiltonMilner_nonDeletionEmptyCase`: handles the case where deleting one member leaves a common center in all remaining sets. + - `strictHiltonMilner_deletionEmptyReduction`: uses `strongShiftedReduction` plus equality-case reflection to transfer the shifted HM structure back to the original family. + +### line-328 + +- Kind: lemma +- Source locator: `docs/source/A_short_proof_of_the_Hilton-Milner_theorem.tex:328-334`; proof at lines 336-363. +- Planned Lean declarations: `strongShiftedReduction`; supporting definition `DeletionEmptyTotalIntersection`. +- Dependencies: shifting operation, strengthened no-common-intersection-after-deletion invariant, standard family comparison, preservation of boundary subfamilies under shifts. +- Formal statement review: Lean states the strengthened shifting reduction: from a pairwise-intersecting uniform family on `[n]` satisfying the deletion-empty-total-intersection property, there exists a shifted family with the same properties and no smaller cardinality. +- Source qualifiers: object class is a pairwise-intersecting family of `k`-element subsets of `[n]`; additional property is that for every `F₀ ∈ 𝓕`, the intersection over `𝓕 \ {F₀}` is empty; output is a shifted family satisfying the same properties and with cardinality at least the original. +- Lean coverage: `UniformFamily n k 𝓕`, `PairwiseIntersecting 𝓕`, and `DeletionEmptyTotalIntersection 𝓕`; existential witness with `ShiftedOn n`, same properties, and `𝓕.card ≤ 𝓕'.card`. +- Scope changes: finite-family representation by `Finset`; explicit `0 < k`; deletion of a member is represented by requiring, for each natural `x`, a witness `F ∈ 𝓕` with `F ≠ F₀` and `x ∉ F`. +- Statement verification status: approved by codex verifier +- Complete source proof: By the standard family, mean the shifted family with $A=\{2,\dots,k+1\}$, $A'=\{2,\dots,k,k+2\}$, and all `k`-element sets that both contain `1` and intersect `A` and `A'`. It is obvious that the standard family is at least as large as any family where all but two sets contain `1`. Given `𝓕`, perform shifts. If these terminate in a shifted family with the desired properties, we are done. Otherwise, a shift destroys the additional property; stop just before and relabel to get a family containing sets with `1` not `2`, with `2` not `1`, with both `1` and `2`, and possibly `B={3,...,k+2}`. Assume all sets containing both `1,2` and intersecting `B` are present. Since these sets have no common intersection other than `1,2`, shifts over all `3≤i hj hmov.1) (fun hi => hmov.2 hi) + +private lemma shiftOperation_eq_uvCompression (i j : ℕ) (𝓕 : SetFamily) : + shiftOperation i j 𝓕 = UV.compression ({i} : Finset ℕ) ({j} : Finset ℕ) 𝓕 := by + ext G + simp only [shiftOperation, UV.compression, Finset.mem_union, Finset.mem_filter, + Finset.mem_image, shiftedSet_eq_uvCompress] + constructor + · intro hG + rcases hG with hstay | hmove + · rcases hstay with ⟨hGmem, hstay⟩ + left + refine ⟨hGmem, ?_⟩ + rcases hstay with hjnot | hiin | hcompmem + · rw [uvCompress_singleton_eq_self_of_not_movable (Or.inl hjnot)] + exact hGmem + · rw [uvCompress_singleton_eq_self_of_not_movable (Or.inr hiin)] + exact hGmem + · exact hcompmem + · rcases hmove with ⟨a, hmov, hcompaG⟩ + rcases hmov with ⟨ha, hja, hia⟩ + by_cases hGmem : G ∈ 𝓕 + · left + refine ⟨hGmem, ?_⟩ + rw [← hcompaG, UV.compress_idem] + simpa [hcompaG] using hGmem + · right + exact ⟨⟨a, ha, hcompaG⟩, hGmem⟩ + · intro hG + rcases hG with hstay | hmove + · rcases hstay with ⟨hGmem, hcompmem⟩ + left + exact ⟨hGmem, Or.inr (Or.inr hcompmem)⟩ + · rcases hmove with ⟨hpre, hGnot⟩ + rcases hpre with ⟨a, ha, hcompaG⟩ + right + have hja : j ∈ a := by + by_contra hjnot + have hself : UV.compress ({i} : Finset ℕ) ({j} : Finset ℕ) a = a := + uvCompress_singleton_eq_self_of_not_movable (Or.inl hjnot) + have hGa : G = a := hcompaG.symm.trans hself + exact hGnot (by simpa [hGa] using ha) + have hia : i ∉ a := by + by_contra hiin + have hself : UV.compress ({i} : Finset ℕ) ({j} : Finset ℕ) a = a := + uvCompress_singleton_eq_self_of_not_movable (Or.inr hiin) + have hGa : G = a := hcompaG.symm.trans hself + exact hGnot (by simpa [hGa] using ha) + exact ⟨a, ⟨ha, hja, hia⟩, hcompaG⟩ + +private lemma shiftOperation_card (i j : ℕ) (𝓕 : SetFamily) : + (shiftOperation i j 𝓕).card = 𝓕.card := by + rw [shiftOperation_eq_uvCompression] + exact UV.card_compression ({i} : Finset ℕ) ({j} : Finset ℕ) 𝓕 + +private lemma shiftOperation_mem_cases (i j : ℕ) (𝓕 : SetFamily) {A : Finset ℕ} + (hA : A ∈ shiftOperation i j 𝓕) : + (A ∈ 𝓕 ∧ (j ∉ A ∨ i ∈ A ∨ shiftedSet i j A ∈ 𝓕)) ∨ + ∃ F : Finset ℕ, F ∈ 𝓕 ∧ j ∈ F ∧ i ∉ F ∧ shiftedSet i j F = A := by + unfold shiftOperation at hA + simp only [Finset.mem_union, Finset.mem_filter, Finset.mem_image] at hA + rcases hA with hA | hA + · exact Or.inl hA + · rcases hA with ⟨F, hF, rfl⟩ + exact Or.inr ⟨F, hF.1, hF.2.1, hF.2.2, rfl⟩ + +private lemma mem_shiftedSet_inserted_of_movable {i j : ℕ} {F : Finset ℕ} + (hjF : j ∈ F) (hiF : i ∉ F) : + i ∈ shiftedSet i j F := by + unfold shiftedSet + rw [if_pos ⟨hjF, hiF⟩] + simp + +private lemma mem_shiftedSet_of_mem_ne_erased {i j x : ℕ} {F : Finset ℕ} + (hxF : x ∈ F) (hxj : x ≠ j) : + x ∈ shiftedSet i j F := by + unfold shiftedSet + by_cases h : j ∈ F ∧ i ∉ F + · rw [if_pos h] + exact Finset.mem_insert.mpr (Or.inr (Finset.mem_erase.mpr ⟨hxj, hxF⟩)) + · rw [if_neg h] + exact hxF + +private lemma not_mem_shiftedSet_erased_of_movable {i j : ℕ} {F : Finset ℕ} + (hij : i < j) (hjF : j ∈ F) (hiF : i ∉ F) : + j ∉ shiftedSet i j F := by + unfold shiftedSet + rw [if_pos ⟨hjF, hiF⟩] + have hji : j ≠ i := Nat.ne_of_gt hij + simp [hji] + +private lemma mem_of_mem_shiftedSet_ne_inserted_of_movable {i j x : ℕ} {F : Finset ℕ} + (hjF : j ∈ F) (hiF : i ∉ F) + (hx : x ∈ shiftedSet i j F) (hxi : x ≠ i) : + x ∈ F := by + unfold shiftedSet at hx + rw [if_pos ⟨hjF, hiF⟩] at hx + rcases Finset.mem_insert.mp hx with hxi' | hxerase + · exact False.elim (hxi hxi') + · exact (Finset.mem_erase.mp hxerase).2 + +private lemma shiftedSet_ne_self_of_movable {i j : ℕ} {F : Finset ℕ} + (hjF : j ∈ F) (hiF : i ∉ F) : + shiftedSet i j F ≠ F := by + intro h + have hi_shift : i ∈ shiftedSet i j F := mem_shiftedSet_inserted_of_movable hjF hiF + have : i ∈ F := by simpa [h] using hi_shift + exact hiF this + +private lemma shiftedSet_inter_shiftedSet_nonempty_of_movable {i j : ℕ} {F G : Finset ℕ} + (hjF : j ∈ F) (hiF : i ∉ F) (hjG : j ∈ G) (hiG : i ∉ G) : + (shiftedSet i j F ∩ shiftedSet i j G).Nonempty := by + refine ⟨i, ?_⟩ + exact Finset.mem_inter.mpr + ⟨mem_shiftedSet_inserted_of_movable hjF hiF, + mem_shiftedSet_inserted_of_movable hjG hiG⟩ + +private lemma kept_inter_shiftedSet_nonempty_of_pairwise (i j : ℕ) (𝓕 : SetFamily) + (hij : i < j) (hinter : PairwiseIntersecting 𝓕) + {A G : Finset ℕ} + (hA : A ∈ 𝓕) + (hAkeep : j ∉ A ∨ i ∈ A ∨ shiftedSet i j A ∈ 𝓕) + (hG : G ∈ 𝓕) (hjG : j ∈ G) (hiG : i ∉ G) : + (A ∩ shiftedSet i j G).Nonempty := by + by_cases hiA : i ∈ A + · refine ⟨i, ?_⟩ + exact Finset.mem_inter.mpr + ⟨hiA, mem_shiftedSet_inserted_of_movable hjG hiG⟩ + by_cases hjA : j ∈ A + · have hshiftA : shiftedSet i j A ∈ 𝓕 := by + rcases hAkeep with hjnotA | hi_or_shift + · exact False.elim (hjnotA hjA) + · rcases hi_or_shift with hiA' | hshiftA + · exact False.elim (hiA hiA') + · exact hshiftA + have hshiftA_ne_G : shiftedSet i j A ≠ G := by + intro hEq + have hi_shiftA : i ∈ shiftedSet i j A := + mem_shiftedSet_inserted_of_movable hjA hiA + have : i ∈ G := by simpa [hEq] using hi_shiftA + exact hiG this + rcases hinter hshiftA hG hshiftA_ne_G with ⟨x, hx⟩ + have hxShiftA : x ∈ shiftedSet i j A := (Finset.mem_inter.mp hx).1 + have hxG : x ∈ G := (Finset.mem_inter.mp hx).2 + have hxi : x ≠ i := by + intro hxi' + exact hiG (by simpa [hxi'] using hxG) + have hxj : x ≠ j := by + intro hxj' + have : j ∈ shiftedSet i j A := by simpa [hxj'] using hxShiftA + exact not_mem_shiftedSet_erased_of_movable hij hjA hiA this + have hxA : x ∈ A := + mem_of_mem_shiftedSet_ne_inserted_of_movable hjA hiA hxShiftA hxi + refine ⟨x, ?_⟩ + exact Finset.mem_inter.mpr + ⟨hxA, mem_shiftedSet_of_mem_ne_erased hxG hxj⟩ + · have hAG_ne : A ≠ G := by + intro hEq + exact hjA (by simpa [hEq] using hjG) + rcases hinter hA hG hAG_ne with ⟨x, hx⟩ + have hxA : x ∈ A := (Finset.mem_inter.mp hx).1 + have hxG : x ∈ G := (Finset.mem_inter.mp hx).2 + have hxj : x ≠ j := by + intro hxj' + exact hjA (by simpa [hxj'] using hxA) + refine ⟨x, ?_⟩ + exact Finset.mem_inter.mpr + ⟨hxA, mem_shiftedSet_of_mem_ne_erased hxG hxj⟩ + +private lemma shiftOperation_pairwise_of_lt (i j : ℕ) (𝓕 : SetFamily) + (hij : i < j) (hinter : PairwiseIntersecting 𝓕) : + PairwiseIntersecting (shiftOperation i j 𝓕) := by + intro A B hA hB hAB + rcases shiftOperation_mem_cases i j 𝓕 hA with hAkeep | hAmove + · rcases shiftOperation_mem_cases i j 𝓕 hB with hBkeep | hBmove + · exact hinter hAkeep.1 hBkeep.1 hAB + · rcases hBmove with ⟨G, hG, hjG, hiG, hshiftG⟩ + simpa [hshiftG] using + kept_inter_shiftedSet_nonempty_of_pairwise i j 𝓕 hij hinter + hAkeep.1 hAkeep.2 hG hjG hiG + · rcases hAmove with ⟨F, hF, hjF, hiF, hshiftF⟩ + rcases shiftOperation_mem_cases i j 𝓕 hB with hBkeep | hBmove + · rcases kept_inter_shiftedSet_nonempty_of_pairwise i j 𝓕 hij hinter + hBkeep.1 hBkeep.2 hF hjF hiF with ⟨x, hx⟩ + refine ⟨x, ?_⟩ + have hxB : x ∈ B := (Finset.mem_inter.mp hx).1 + have hxShiftF : x ∈ shiftedSet i j F := (Finset.mem_inter.mp hx).2 + exact Finset.mem_inter.mpr ⟨by simpa [hshiftF] using hxShiftF, hxB⟩ + · rcases hBmove with ⟨G, hG, hjG, hiG, hshiftG⟩ + simpa [hshiftF, hshiftG] using + shiftedSet_inter_shiftedSet_nonempty_of_movable hjF hiF hjG hiG + +private lemma mem_shiftOperation_self_or_shifted_of_mem (i j : ℕ) {𝓕 : SetFamily} + {F : Finset ℕ} (hF : F ∈ 𝓕) : + F ∈ shiftOperation i j 𝓕 ∨ shiftedSet i j F ∈ shiftOperation i j 𝓕 := by + classical + unfold shiftOperation + by_cases hmove : j ∈ F ∧ i ∉ F + · by_cases hshift : shiftedSet i j F ∈ 𝓕 + · left + exact Finset.mem_union.mpr + (Or.inl (Finset.mem_filter.mpr ⟨hF, Or.inr (Or.inr hshift)⟩)) + · right + exact Finset.mem_union.mpr + (Or.inr (Finset.mem_image.mpr ⟨F, Finset.mem_filter.mpr ⟨hF, hmove⟩, rfl⟩)) + · left + have hkeep : j ∉ F ∨ i ∈ F ∨ shiftedSet i j F ∈ 𝓕 := by + by_cases hjF : j ∈ F + · right + left + by_contra hiF + exact hmove ⟨hjF, hiF⟩ + · exact Or.inl hjF + exact Finset.mem_union.mpr (Or.inl (Finset.mem_filter.mpr ⟨hF, hkeep⟩)) + +private lemma not_mem_shiftedSet_of_not_mem_ne_inserted {i j x : ℕ} {F : Finset ℕ} + (hxF : x ∉ F) (hxi : x ≠ i) : + x ∉ shiftedSet i j F := by + unfold shiftedSet + by_cases hmove : j ∈ F ∧ i ∉ F + · rw [if_pos hmove] + intro hx + rcases Finset.mem_insert.mp hx with hxi' | hxerase + · exact hxi hxi' + · exact hxF (Finset.mem_of_mem_erase hxerase) + · rw [if_neg hmove] + exact hxF + +private lemma shiftOperation_common_inserted_of_not_empty {i j : ℕ} {𝓕 : SetFamily} + (hempty : EmptyTotalIntersection 𝓕) + (hnot : ¬ EmptyTotalIntersection (shiftOperation i j 𝓕)) : + ∀ ⦃A : Finset ℕ⦄, A ∈ shiftOperation i j 𝓕 → i ∈ A := by + classical + unfold EmptyTotalIntersection at hempty hnot + push Not at hnot + rcases hnot with ⟨x, hxcommon⟩ + have hxi : x = i := by + rcases hempty x with ⟨F, hFmem, hxF⟩ + rcases mem_shiftOperation_self_or_shifted_of_mem i j (𝓕 := 𝓕) hFmem with hFshift | hshiftF + · exact False.elim (hxF (hxcommon F hFshift)) + · by_contra hne + exact not_mem_shiftedSet_of_not_mem_ne_inserted hxF hne (hxcommon (shiftedSet i j F) hshiftF) + intro A hA + simpa [hxi] using hxcommon A hA + +private lemma cover_and_opposite_side_of_common_shift {i j : ℕ} {𝓕 : SetFamily} + (hempty : EmptyTotalIntersection 𝓕) + {F : Finset ℕ} (hFmem : F ∈ 𝓕) (hjF : j ∈ F) (hiF : i ∉ F) + (hnot : ¬ EmptyTotalIntersection (shiftOperation i j 𝓕)) : + (∀ ⦃A : Finset ℕ⦄, A ∈ 𝓕 → i ∈ A ∨ j ∈ A) ∧ + (∃ A : Finset ℕ, A ∈ 𝓕 ∧ j ∈ A ∧ i ∉ A) ∧ + (∃ B : Finset ℕ, B ∈ 𝓕 ∧ i ∈ B ∧ j ∉ B) := by + classical + have hcommon := shiftOperation_common_inserted_of_not_empty (i := i) (j := j) + (𝓕 := 𝓕) hempty hnot + have hcover : ∀ ⦃A : Finset ℕ⦄, A ∈ 𝓕 → i ∈ A ∨ j ∈ A := by + intro A hA + by_cases hiA : i ∈ A + · exact Or.inl hiA + · by_cases hjA : j ∈ A + · exact Or.inr hjA + · exfalso + have hAshift : A ∈ shiftOperation i j 𝓕 := by + unfold shiftOperation + exact Finset.mem_union.mpr + (Or.inl (Finset.mem_filter.mpr ⟨hA, Or.inl hjA⟩)) + exact hiA (hcommon hAshift) + refine ⟨hcover, ⟨F, hFmem, hjF, hiF⟩, ?_⟩ + rcases hempty j with ⟨B, hBmem, hjB⟩ + rcases hcover hBmem with hiB | hjB' + · exact ⟨B, hBmem, hiB, hjB⟩ + · exact False.elim (hjB hjB') + +private lemma shiftedSet_mem_shiftOperation_of_mem_shiftOperation (i j : ℕ) {𝓕 : SetFamily} + {A : Finset ℕ} (hA : A ∈ shiftOperation i j 𝓕) : + shiftedSet i j A ∈ shiftOperation i j 𝓕 := by + rw [shiftOperation_eq_uvCompression] at hA ⊢ + rw [shiftedSet_eq_uvCompress] + exact UV.compress_mem_compression_of_mem_compression hA + +private lemma shiftOperation_idem (i j : ℕ) (𝓕 : SetFamily) : + shiftOperation i j (shiftOperation i j 𝓕) = shiftOperation i j 𝓕 := by + simp [shiftOperation_eq_uvCompression, UV.compression_idem] + +private lemma shiftOperation_empty_or_bad_shape {i j : ℕ} {𝓕 : SetFamily} + (hempty : EmptyTotalIntersection 𝓕) + {F : Finset ℕ} (hFmem : F ∈ 𝓕) (hjF : j ∈ F) (hiF : i ∉ F) : + EmptyTotalIntersection (shiftOperation i j 𝓕) ∨ + ((∀ ⦃A : Finset ℕ⦄, A ∈ 𝓕 → i ∈ A ∨ j ∈ A) ∧ + (∃ A : Finset ℕ, A ∈ 𝓕 ∧ j ∈ A ∧ i ∉ A) ∧ + (∃ B : Finset ℕ, B ∈ 𝓕 ∧ i ∈ B ∧ j ∉ B)) := by + by_cases h : EmptyTotalIntersection (shiftOperation i j 𝓕) + · exact Or.inl h + · exact Or.inr <| cover_and_opposite_side_of_common_shift (i := i) (j := j) + (𝓕 := 𝓕) hempty hFmem hjF hiF h + +private lemma opposite_side_sets_intersect_off_pair {i j : ℕ} {𝓕 : SetFamily} + (hinter : PairwiseIntersecting 𝓕) + {A B : Finset ℕ} (hA : A ∈ 𝓕) (_hjA : j ∈ A) (hiA : i ∉ A) + (hB : B ∈ 𝓕) (hiB : i ∈ B) (hjB : j ∉ B) : + ∃ x : ℕ, x ∈ A ∧ x ∈ B ∧ x ≠ i ∧ x ≠ j := by + have hAB : A ≠ B := by + intro hEq + exact hiA (by rw [hEq]; exact hiB) + rcases hinter hA hB hAB with ⟨x, hx⟩ + have hxA : x ∈ A := (Finset.mem_inter.mp hx).1 + have hxB : x ∈ B := (Finset.mem_inter.mp hx).2 + refine ⟨x, hxA, hxB, ?_, ?_⟩ + · intro hxi + exact hiA (by simpa [hxi] using hxA) + · intro hxj + exact hjB (by simpa [hxj] using hxB) + +/-- +Source lemma `lem:Frankl-Furedi`, lines 201--206. + +Source proof: apply shifts. If shifting terminates in a shifted family with +empty total intersection, done. Otherwise a last bad shift makes all sets +contain one element; relabel it and its partner to `1` and `2`, continue shifting +on labels at least `3`, add the `k`-sets containing `{1,2}` if necessary, and +use the boundary of `{1, ..., k+1}` as an empty-intersection subfamily preserved +by further shifts. + +Prover notes: prove or import separate facts for preservation of cardinality, +pairwise intersection, uniformity, and the empty-intersection fallback under +combinatorial shifts. A termination measure for repeated shifts will be needed. +-/ +lemma franklFurediShifted (n k : ℕ) (𝓕 : SetFamily) + (hk : 0 < k) (hF : UniformFamily n k 𝓕) + (hinter : PairwiseIntersecting 𝓕) (hempty : EmptyTotalIntersection 𝓕) : + ∃ 𝓕' : SetFamily, + UniformFamily n k 𝓕' ∧ PairwiseIntersecting 𝓕' ∧ + EmptyTotalIntersection 𝓕' ∧ ShiftedOn n 𝓕' ∧ 𝓕.card ≤ 𝓕'.card := by + classical + by_cases hshift : ShiftedOn n 𝓕 + · exact franklFurediShifted_of_shifted n k 𝓕 hF hinter hempty hshift + · -- TODO: formalize the non-shifted Frankl--Furedi shifting construction. + -- This branch needs repeated shifts, preservation lemmas, and the + -- empty-intersection boundary fallback described in the source proof. + rw [ShiftedOn] at hshift + push Not at hshift + rcases hshift with ⟨i, j, F, hi, hj, hij, hFmem, hjF, hiF, hbad⟩ + let 𝓖 : SetFamily := shiftOperation i j 𝓕 + have hGunif : UniformFamily n k 𝓖 := by + dsimp [𝓖] + exact shiftOperation_uniform n k i j 𝓕 hi hF + have hGinter : PairwiseIntersecting 𝓖 := by + dsimp [𝓖] + exact shiftOperation_pairwise_of_lt i j 𝓕 hij hinter + have hmove : shiftedSet i j F ∈ 𝓖 := by + dsimp [𝓖] + exact shiftedSet_mem_shiftOperation_of_movable i j 𝓕 hFmem hjF hiF + have hGcard : 𝓖.card = 𝓕.card := by + dsimp [𝓖] + exact shiftOperation_card i j 𝓕 + -- `hbad` is the first concrete bad shift: replacing `j` by `i` in `F` + -- leaves the current family. If this shift destroys empty total + -- intersection, the new helper below extracts the structural fallback data + -- used in the Frankl--Furedi proof. + have hbadShape : + ¬ EmptyTotalIntersection 𝓖 → + (∀ ⦃A : Finset ℕ⦄, A ∈ 𝓕 → i ∈ A ∨ j ∈ A) ∧ + (∃ A : Finset ℕ, A ∈ 𝓕 ∧ j ∈ A ∧ i ∉ A) ∧ + (∃ B : Finset ℕ, B ∈ 𝓕 ∧ i ∈ B ∧ j ∉ B) := by + intro hnot + dsimp [𝓖] at hnot + exact cover_and_opposite_side_of_common_shift (i := i) (j := j) (𝓕 := 𝓕) + hempty hFmem hjF hiF hnot + -- The remaining proof must either iterate good shifts preserving + -- `EmptyTotalIntersection`, or invoke the full Frankl--Furedi + -- relabel-and-boundary fallback starting from `hbadShape`. + sorry + +/-- +Source lemma `line-328`, lines 328--334; proof in lines 336--363. + +Source proof: perform shifts while preserving the stronger property that every +one-set deletion leaves empty total intersection. If a shift would destroy this +property, stop just before it, relabel to obtain sets with `1` not `2`, with `2` +not `1`, and with both; compare with the standard family built from +`{2, ..., k+1}` and `{2, ..., k, k+2}`. After restricted shifts on labels at +least `3`, either replace by the standard family or use the two preserved +boundary subfamilies to continue shifting until stable. + +Prover notes: this is stronger than `franklFurediShifted`; expect helper lemmas +for the standard family, the two boundary subfamilies, and preservation of the +deletion-empty invariant under restricted shifts. The bare existential output +does not by itself reflect uniqueness of the original extremal family; the final +theorem uses bridge lemmas for that step. +-/ +lemma strongShiftedReduction (n k : ℕ) (𝓕 : SetFamily) + (hk : 0 < k) (hF : UniformFamily n k 𝓕) + (hinter : PairwiseIntersecting 𝓕) + (hdelete : DeletionEmptyTotalIntersection 𝓕) : + ∃ 𝓕' : SetFamily, + UniformFamily n k 𝓕' ∧ PairwiseIntersecting 𝓕' ∧ + DeletionEmptyTotalIntersection 𝓕' ∧ ShiftedOn n 𝓕' ∧ 𝓕.card ≤ 𝓕'.card := by + by_cases hshift : ShiftedOn n 𝓕 + · exact ⟨𝓕, hF, hinter, hdelete, hshift, le_rfl⟩ + · -- TODO: formalize the strengthened shifting construction from the source proof. + -- The proof must preserve `DeletionEmptyTotalIntersection` through restricted + -- shifts and the standard-family replacement step. + sorry + +end AShortProofOfTheHiltonMilnerTheorem diff --git a/AShortProofOfTheHiltonMilnerTheorem/EPFLemmaPrint.lean b/AShortProofOfTheHiltonMilnerTheorem/EPFLemmaPrint.lean new file mode 100644 index 0000000..3c811b1 --- /dev/null +++ b/AShortProofOfTheHiltonMilnerTheorem/EPFLemmaPrint.lean @@ -0,0 +1,8 @@ +import AShortProofOfTheHiltonMilnerTheorem.Basic + +#print AShortProofOfTheHiltonMilnerTheorem.ground +#print AShortProofOfTheHiltonMilnerTheorem.shiftedSet +#print AShortProofOfTheHiltonMilnerTheorem.hiltonMilnerFamily +#print AShortProofOfTheHiltonMilnerTheorem.IsHiltonMilnerFamily +#print AShortProofOfTheHiltonMilnerTheorem.EmptyTotalIntersection +#print AShortProofOfTheHiltonMilnerTheorem.DeletionEmptyTotalIntersection diff --git a/AShortProofOfTheHiltonMilnerTheorem/README.md b/AShortProofOfTheHiltonMilnerTheorem/README.md new file mode 100644 index 0000000..e6ef6d5 --- /dev/null +++ b/AShortProofOfTheHiltonMilnerTheorem/README.md @@ -0,0 +1,29 @@ +# A Short Proof of the Hilton-Milner Theorem + +Lean 4 source-backed formalization setup for Denys Bulavka and Russ Woodroofe, +*A short proof of the Hilton-Milner Theorem*. + +The active formalization is in: + +- `AShortProofOfTheHiltonMilnerTheorem/` +- `AShortProofOfTheHiltonMilnerTheorem.lean` + +The Lean declarations are split by proof role: + +- `Basic.lean`: finite-family, uniformity, intersection, shifting, and extremal-family definitions. +- `MainTechnical.lean`: the main technical inequality and shifted/strict variants. +- `Shifting.lean`: Frankl--Furedi and strengthened shifting reductions. +- `HiltonMilner.lean`: the HM bound, uniqueness statement, and equality-case bridge lemmas. + +## Status + +- `lake build AShortProofOfTheHiltonMilnerTheorem` succeeds. +- Current version is a source-backed theorem skeleton with `sorry` proof obligations. +- The formalization focuses on finite set families, cross-intersection, shadows, shifting, + the Hilton-Milner bound, and the uniqueness bridge described in the source. + +See: + +- `AShortProofOfTheHiltonMilnerTheorem/Blueprint.md` +- `docs/source/A_short_proof_of_the_Hilton-Milner_theorem.tex` +- `docs/bulavka_woodroofe2024_hilton_milner.pdf` diff --git a/AShortProofOfTheHiltonMilnerTheorem/docs/2411.02513.source b/AShortProofOfTheHiltonMilnerTheorem/docs/2411.02513.source new file mode 100644 index 0000000..0412147 Binary files /dev/null and b/AShortProofOfTheHiltonMilnerTheorem/docs/2411.02513.source differ diff --git a/AShortProofOfTheHiltonMilnerTheorem/docs/bulavka_woodroofe2024_hilton_milner.images.txt b/AShortProofOfTheHiltonMilnerTheorem/docs/bulavka_woodroofe2024_hilton_milner.images.txt new file mode 100644 index 0000000..9d698ac --- /dev/null +++ b/AShortProofOfTheHiltonMilnerTheorem/docs/bulavka_woodroofe2024_hilton_milner.images.txt @@ -0,0 +1,6 @@ +page num type width height color comp bpc enc interp object ID x-ppi y-ppi size ratio +-------------------------------------------------------------------------------------------- + 1 0 stencil 1 1 - 1 1 image no [inline] 1 150 1B - + 5 1 stencil 1 1 - 1 1 image no [inline] 2 150 1B - + 5 2 stencil 1 1 - 1 1 image no [inline] 2 150 1B - + 5 3 stencil 1 1 - 1 1 image no [inline] 2 150 1B - diff --git a/AShortProofOfTheHiltonMilnerTheorem/docs/bulavka_woodroofe2024_hilton_milner.pdf b/AShortProofOfTheHiltonMilnerTheorem/docs/bulavka_woodroofe2024_hilton_milner.pdf new file mode 100644 index 0000000..0c39db6 Binary files /dev/null and b/AShortProofOfTheHiltonMilnerTheorem/docs/bulavka_woodroofe2024_hilton_milner.pdf differ diff --git a/AShortProofOfTheHiltonMilnerTheorem/docs/bulavka_woodroofe2024_hilton_milner.txt b/AShortProofOfTheHiltonMilnerTheorem/docs/bulavka_woodroofe2024_hilton_milner.txt new file mode 100644 index 0000000..ec15b2a --- /dev/null +++ b/AShortProofOfTheHiltonMilnerTheorem/docs/bulavka_woodroofe2024_hilton_milner.txt @@ -0,0 +1,248 @@ + A SHORT PROOF OF THE HILTON-MILNER THEOREM + + DENYS BULAVKA AND RUSS WOODROOFE + + Abstract. We give a short and relatively elementary proof of the Hilton-Milner + Theorem. + + + + +arXiv:2411.02513v4 [math.CO] 19 Nov 2025 + The Hilton-Milner Theorem gives the maximum size of a uniform pairwise-intersecting + family of sets that do not share a common element. + Theorem 1 (Hilton and Milner 1967 [9]). Let k ≤ n/2. If F is a family  of +  pairwise- +  + n−1 + intersecting k-element subsets of [n], where F ∈F F = ∅, then |F | ≤ k−1 − n−1−k +1. + T + k−1 + + In the current article, we will show Theorem 1 to follow quickly from the following + theorem, which we believe to be of some independent interest. Two set systems A and + B are cross-intersecting if for every A ∈ A, B ∈ B, the intersection A ∩ B is nonempty. + The shadow ∂B of a k-element set B consists of all the (k − 1)-element subsets of B; + the shadow of a uniform set family is the union of the shadows of its constituent sets, + thus consists of all (k − 1)-element subsets of constituent sets. + Theorem 2. Let 2k − 1 ≤ n, let A be a family of (k − 1)-element subsets of [n], and let + B be a family of k-element subsets of [n]. If A, B are cross-intersecting, B is nonempty, + and ∂B ⊆ A, then ! ! + n n−k + |A| + |B| ≤ − + 1. + k−1 k−1 + Note that the bound of Theorem 1 is attained with a single k-element set B that + does not contain 1, together with all the k-element sets that contain 1 and intersect B; + the bound of Theorem 2 is attained with a single k-element set and all (k − 1)-element + sets that intersect it. + Our proof of Theorem 1 may be viewed as injective. Other recent proofs of Theorem 1 + were given in [4, 10], but instead of relying on a simple cross-intersecting type theorem, + both of these proofs rely on a certain “partial complement” operation. In somewhat + older work [6] (see also [3]), Frankl and Tokushige gave a proof of Hilton-Milner from + a different cross-intersection theorem, but the proof is less elementary than that of + Theorem 2, requiring the Schützenberger-Kruskal-Katona Theorem. A recent preprint + of Wu, Li, Feng, Liu and Yu [12] (now published) gives a proof based on still another + cross-intersecting theorem, but the existing proofs of this underlying result also seem + to be somewhat more difficult than our approach. + Work of the first author is partially supported by the Israel Science Foundation grant ISF-2480/20 + and the AARMS postdoctoral fellowship. Work of the second author is supported in part by the + Slovenian Research Agency (research program P1-0285 and research projects J1-9108, J1-2451, J1- + 3003, and J1-50000). + 1 + A SHORT PROOF OF THE HILTON-MILNER THEOREM 2 + +Shifting. We recall that a system F of subsets of [n] is shifted if for each i < j, +whenever F ∈ F , j ∈ F and i ∈ / F , then also (F \ j) ∪ i ∈ F . Here, we abuse notation +to identify i, j with the singleton subsets {i}, {j} where it causes no confusion. The +(combinatorial) shifting operation Shifti←j is defined as + Shifti←j F = {F ∈ F : j ∈ + / F or i ∈ F or (F \ j) ∪ i ∈ F } + ∪ {(F \ j) ∪ i : F ∈ F is such that j ∈ F, i ∈ + / F}. + It is well-known that repeated applications of Shifti←j over i < j will eventually +reduce an arbitrary set system to a shifted set system, that the operation preserves the +cross-intersecting property, and that ∂ Shifti←j F ⊆ Shifti←j ∂F [1, 2, 7, 8]. + +Proof of Theorem 2. We carry out a straightforward induction on n. +   + n +If n = 2k − 1, then the upper bound is k−1 , and the result follows by noticing that if +a (k − 1)-element set is in A, then its complement cannot be in B (and vice-versa). + For the inductive step, we may assume that A and B are shifted; otherwise, shift. +Let A(¬n), B(¬n) consist of the subsets in A, B (respectively) that do not contain n. It +is immediate that A(¬n), B(¬n) are shifted, cross-intersecting, and satisfy the shadow +condition. Let A(n), B(n) be obtained by taking the families consisting of the subsets in +A, B that contain n, then deleting n from each subset. It follows quickly from definitions +that A(n), B(n) are shifted, cross-intersecting, and satisfy the shadow condition. + As A and B are shifted, so A(¬n) and B(¬n) are nonempty, and hence by induction + ! ! + n−1 n−1−k +(1) |A(¬n)| + |B(¬n)| ≤ − + 1. + k−1 k−1 + For A(n), B(n), there are a few easy cases: + If A(n) is empty, then (by the shadow condition) also B(n) is empty. + If B(n) is empty, then since B is nonempty and shifted, we have {1, . . . , k} ∈ B. +Since +  setin A(n) intersects with {1, . . . , k}, we get |A(n)| + |B(n)| = |A(n)| ≤ +  every + n−1 + k−2 + − n−1−k + k−2 + . + If B(n) is nonempty, then by induction it holds that + ! ! + n−1 n − 1 − (k − 1) + |A(n)| + |B(n)| ≤ − +1 + k−2 k−2 + ! ! + n−1 n−1−k +(2) ≤ − . + k−2 k−2 +The result now follows from (1), the bound on |A(n)|+|B(n)|, and the Pascal’s Triangle +identity.  + +Proof of Theorem 1. We will use the following lemma of Frankl and Füredi: +Lemma 3 (essentially Frankl and Füredi [5]). If F is a pairwise-intersecting family of +k-element subsets of [n] with F ∈F F = ∅, then there is a shifted family F ′ satisfying + T + +the same properties and with |F ′| ≥ |F |. + A SHORT PROOF OF THE HILTON-MILNER THEOREM 3 + +Given the lemma, the proof of Theorem 1 is nearly immediate. Let F be a shifted +family satisfying the conditions of the theorem. Define + A = {F \ 1 : F ∈ F with 1 ∈ F } + B = {F : F ∈ F with 1 ∈ + / F }. +Since F is shifted, if F ∈ F does not have 1, then (F \ i) ∪ 1 ∈ F for each i ∈ F . It +follows that ∂B ⊆ A. Since F is intersecting, also A, B are cross-intersecting systems +of subsets of {2, . . . , n}. Since F has empty intersection, both of A, B are nonempty. +The desired bound is now immediate from Theorem 2.  +Remark 4. This proof requires only the special case of Theorem 2 where the set systems +are shifted. +Proof of Lemma 3. For completeness, we also prove the lemma. +Given F as in Theorem 1, apply shifting operations Shifti←j . Each such operation +preserves the pairwise-intersecting property and cardinality, but may or may not result +in a system with a common element of intersection. + If a sequence of shifting operations ends in a shifted system with empty intersection, +then we are certainly done. + Otherwise, some Shifti0 ←j0 results in a system where every set contains i0 . Thus, +before this step, we have a system F where every set contains either i0 or j0 . Relabel +i0 to 1 and j0 to 2, and continue applying Shifti←j operations over all 3 ≤ i < j. Thus, +after these additional shift operations, we have {1, 3, . . . , k + 1} and {2, 3, . . . , k + 1} +in the system. Without loss of generality (since every set in F contains 1 or 2), we +also have all k-element subsets containing {1, 2}; otherwise, add them. Thus, we have +∂ {1, . . . , k + 1} contained in our system. As ∂ {1, . . . , k + 1} has empty intersection and +is preserved under all further shift operations (over 1 ≤ i < j), the result follows.  +Discussion. In addition to being short and direct, our proof is relatively elementary, +using only shifting theory. Indeed, we recover a completely elementary proof of the +restriction of the Hilton-Milner Theorem to shifted systems. + A main difficulty in proofs of Hilton-Milner and/or Erdős-Ko-Rado type results is re- +lating systems of (k −1)-element subsets to systems of k-element subsets. Our approach +handles this with the shadow containment condition of Theorem 2. + Our motivation here comes partly from combinatorial algebraic topology. In par- +ticular, the simplicial complex generated by a shifted family of k-element sets has +homology with generators in B (using notation as in the proof of Theorem 1). Thus, +Lemma 3 transforms the combinatorial property of empty intersection into a homolog- +ical property. Kalai comments on similar connections between intersection theorems +and homology in [11, Section 6.4]. + The approach also gives a unified proof of the well-known Erdős-Ko-Rado Theorem. +More concretely, if we relax the hypothesis +   of Theorem 2 to allow B to be empty, then the +corresponding bound is |A| + |B| ≤ n−1 k−1 + . Erdős-Ko-Rado now follows from replacing +Theorem 2 with the relaxed cross-intersection theorem in the proof of Theorem 1. The +proof is similar to (and only slightly more complicated than) the standard inductive +proof of Erdős-Ko-Rado for shifted systems. + A SHORT PROOF OF THE HILTON-MILNER THEOREM 4 + + The approach also recovers uniqueness of the largest family for Theorem 1 when +n/2 > k ≥ 4. Here, we strengthen the hypothesis of Theorem 2 to require B to have at +least two elements. We discuss the details in the following section. +Uniqueness of the Hilton-Milner family. As mentioned in the discussion, the same +techniques give uniqueness of the maximum family in Theorem 1. We prove: +Theorem 5. In the situation of Theorem 1, if 4 ≤ k < n/2 and |F | achieves the upper +bound, then there is some k-set B and i ∈ / B so that F consists of B together with all +k-sets that both contain i and intersect B. + We require k ≥ 4 in order to avoid some technicalities. In particular, there is another +family achieving the bound for k = 3. See [10] for more details and a different argument. + As in the proof of Theorem 1, we reduce to a shifted family, and prove for a shifted +family. + The proof for a shifted family requires a completely straightforward modification of +Theorem 2. We obviously require k ≥ 4. We also strengthen the hypothesis to require +|B| ≥ 2, replacing the condition that |B| ≥ 1; with the strengthened hypothesis, the +inequality is strict. Then in the proof, we may have |B(n)| empty or nonempty. If +empty, then since B has at least two elements, so A(n) is strictly smaller than the given +bound. If nonempty, then the bound in (2) is already strict so long as k ≥ 4. In either +case, the induction step yields a strict inequality. + Theorem 5 follows for shifted families by applying the variant of Theorem 2 with +|B| ≥ 2 to the same families as in the proof of Theorem 1. + It remains only to reduce to shifted families. This reduction requires a bit of care. +We did not find the following lemma in the literature, although we believe it to be +known to experts in the field. +Lemma 6. Let F be a family of pairwise-intersecting k-element subsets of [n] with the +additional property that for any F0 ∈ F , the intersection F\{F0 } F is empty. Then + T + +there is a shifted family F ′ satisfying the same properties and with |F ′| ≥ |F |. +Proof. By the standard family, we mean the shifted family with A = {2, . . . , k + 1}, +A′ = {2, . . . , k, k + 2}, and all k-element sets that both contain 1 and intersect A and +A′ . It is obvious that the standard family is at least as large as any family where all +but two sets contain 1. + Given F , we perform a sequence of shifts. If these terminate in a shifted family with +the desired properties, then we are done. Otherwise, an operation results in a family +without the additional property. Stopping just before this operation and relabeling +elements, we have a family containing sets with 1 and not 2, with 2 and not 1, with +both 1 and 2, and possibly the set B = {3, . . . , k + 2}. + We may assume without loss of generality that we have all sets containing both 1, 2 +and intersecting with B. Since these sets do not have any common intersection other +than 1, 2, the operations Shifti←j over all 3 ≤ i < j preserve the additional property. + After shifting over 3 ≤ i < j, if we have only one set with 1 and not 2, or only one +set with 2 and not 1, then we replace with the standard family. Otherwise, we have +in the family {a, 3, . . . , k + 1} and {a, 3, . . . , k, k + 2} for a = 1, 2, along with all sets + A SHORT PROOF OF THE HILTON-MILNER THEOREM 5 + +containing {1, 2} and intersecting B. In particular, the family contains as subfamilies +both ∂ {1, . . . , k + 1} and ∂ {1, . . . , k, k + 2}. Both subfamilies have empty intersection +and are preserved under all shift operations, so we can now shift until the system +stabilizes.  +Acknowledgements. We particularly thank Dániel Gerbner for several helpful com- +ments about preprints of the paper. We also thank Peter Frankl, Balázs Patkós, John +Shareshian, and Tamás Szőnyi. + References + [1] Peter Frankl, The shifting technique in extremal set theory, Surveys in combinatorics 1987 (New + Cross, 1987), London Math. Soc. Lecture Note Ser., vol. 123, Cambridge Univ. Press, Cambridge, + 1987, pp. 81–110. + [2] , Shadows and shifting, Graphs Combin. 7 (1991), no. 1, 23–29. + [3] , New inequalities for cross-intersecting families, Mosc. J. Comb. Number Theory 6 (2016), + no. 4, 27–32. + [4] , A simple proof of the Hilton-Milner theorem, Mosc. J. Comb. Number Theory 8 (2019), + no. 2, 97–101. + [5] Peter Frankl and Zoltán Füredi, Nontrivial intersecting families, J. Combin. Theory Ser. A 41 + (1986), no. 1, 150–153. + [6] Peter Frankl and Norihide Tokushige, Some best possible inequalities concerning cross-intersecting + families, J. Combin. Theory Ser. A 61 (1992), no. 1, 87–97. + [7] Dániel Gerbner and Balázs Patkós, Extremal finite set theory, Discrete Mathematics and its Ap- + plications (Boca Raton), CRC Press, Boca Raton, FL, 2019. + [8] Jürgen Herzog and Takayuki Hibi, Monomial ideals, Graduate Texts in Mathematics, vol. 260, + Springer-Verlag London Ltd., London, 2011. + [9] A. J. W. Hilton and E. C. Milner, Some intersection theorems for systems of finite sets, Quart. + J. Math. Oxford Ser. (2) 18 (1967), 369–384. +[10] Glenn Hurlbert and Vikram Kamat, New injective proofs of the Erdős-Ko-Rado and Hilton-Milner + theorems, Discrete Math. 341 (2018), no. 6, 1749–1754, arXiv:1609.04714. +[11] Gil Kalai, Algebraic shifting, Computational commutative algebra and combinatorics (Osaka, + 1999), Adv. Stud. Pure Math., vol. 33, Math. Soc. Japan, Tokyo, 2002, pp. 121–163. +[12] Yongjiang Wu, Yongtao Li, Lihua Feng, Jiuqiang Liu, and Guihai Yu, Maximal intersecting + families revisited, Discrete Math. 349 (2026), no. 1, Paper No. 114654, 18, arXiv:2411.03674. + + Einstein Institute of Mathematics, Hebrew University, Jerusalem 91904, Israel + Current address: Department of Mathematics & Statistics, Dalhousie University, 6297 Castine Way, +PO BOX 15000, Halifax, NS, Canada, B3H 4R2 + Email address: denys.bulavka@dal.ca + URL: https://kam.mff.cuni.cz/∼dbulavka/ + + Univerza na Primorskem, Glagoljaška 8, 6000 Koper, Slovenia + Email address: russ.woodroofe@famnit.upr.si + URL: https://osebje.famnit.upr.si/∼russ.woodroofe/ + \ No newline at end of file diff --git a/AShortProofOfTheHiltonMilnerTheorem/docs/source/00README.json b/AShortProofOfTheHiltonMilnerTheorem/docs/source/00README.json new file mode 100644 index 0000000..501ebec --- /dev/null +++ b/AShortProofOfTheHiltonMilnerTheorem/docs/source/00README.json @@ -0,0 +1,17 @@ +{ + "sources" : [ + { + "usage" : "toplevel", + "filename" : "A_short_proof_of_the_Hilton-Milner_theorem.tex" + }, + { + "usage" : "ignore", + "filename" : "8_Users_russw_Documents_Research_mypapers_A_short_proof_of_the_Hilton-Milner_theorem_hamsplain.bst" + } + ], + "spec_version" : 1, + "texlive_version" : "2025", + "process" : { + "compiler" : "latex" + } +} diff --git a/AShortProofOfTheHiltonMilnerTheorem/docs/source/8_Users_russw_Documents_Research_mypapers_A_short_proof_of_the_Hilton-Milner_theorem_hamsplain.bst b/AShortProofOfTheHiltonMilnerTheorem/docs/source/8_Users_russw_Documents_Research_mypapers_A_short_proof_of_the_Hilton-Milner_theorem_hamsplain.bst new file mode 100644 index 0000000..4a6c776 --- /dev/null +++ b/AShortProofOfTheHiltonMilnerTheorem/docs/source/8_Users_russw_Documents_Research_mypapers_A_short_proof_of_the_Hilton-Milner_theorem_hamsplain.bst @@ -0,0 +1,1285 @@ +%%% ==================================================================== +%%% @BibTeX-style-file{ +%%% author = "American Mathematical Society", +%%% version = "1.2beta", +%%% date = "13-Oct-1994", +%%% time = "15:30:52 EDT", +%%% filename = "hamsplain.bst", +%%% copyright = "Copyright (C) 1994 American Mathematical Society, +%%% all rights reserved. Copying of this file is +%%% authorized only if either: +%%% (1) you make absolutely no changes to your copy, +%%% including name; OR +%%% (2) if you do make changes, you first rename it +%%% to some other name. +%%% [Name changed to hamsplain.bst]", +%%% address = "American Mathematical Society, +%%% Technical Support, +%%% Electronic Products and Services, +%%% P. O. Box 6248, +%%% Providence, RI 02940, +%%% USA", +%%% telephone = "401-455-4080 or (in the USA and Canada) +%%% 800-321-4AMS (321-4267)", +%%% FAX = "401-331-3842", +%%% email = "tech-support@math.ams.org (Internet)", +%%% codetable = "ISO/ASCII", +%%% keywords = "bibtex, bibliography, amslatex, ams-latex", +%%% supported = "yes?", +%%% abstract = "BibTeX bibliography style `hamsplain' for BibTeX +%%% versions 0.99a or later and LaTeX version 2e. +%%% Produces alphabetic-label bibliography items in +%%% a form typical for American Mathematical Society +%%% publications. Modified by Greg Kuperberg to +%%% include an eprint field for e-print archives." +%%% } +%%% ==================================================================== + +% See the file btxbst.doc for extra documentation other than +% what is included here. And see btxhak.tex for a description +% of the BibTeX language and how to use it. + +% This defines the types of fields that can occur in a database entry +% for this particular bibliography style. Except for `language', +% this is the standard list from plain.bst. + +%% Types of entries currently allowed in a BibTeX file: +%% +%% ARTICLE -- An article from a journal or magazine. +%% +%% BOOK -- A book with an explicit publisher. +%% +%% BOOKLET -- A work that is printed and bound, +%% but without a named publisher or sponsoring institution. +%% +%% CONFERENCE -- The same as INPROCEEDINGS, +%% included for Scribe compatibility. +%% +%% INBOOK -- A part of a book, +%% which may be a chapter (or section or whatever) and/or a range of pages. +%% +%% INCOLLECTION -- A part of a book having its own title. +%% +%% INPROCEEDINGS -- An article in a conference proceedings. +%% +%% MANUAL -- Technical documentation. +%% +%% MASTERSTHESIS -- A Master's thesis. +%% +%% MISC -- Use this type when nothing else fits. +%% +%% PHDTHESIS -- A PhD thesis. +%% +%% PROCEEDINGS -- The proceedings of a conference. +%% +%% TECHREPORT -- A report published by a school or other institution, +%% usually numbered within a series. +%% +%% UNPUBLISHED -- A document having an author and title, but not formally +%% published. +ENTRY + { address + author + booktitle + chapter + doi + edition + editor + eprint + howpublished + institution + journal + key + language + month + note + number + organization + pages + publisher + school + series + title + type + url + volume + year + } + {} + { label extra.label } + +% Removed after.sentence, after.block---not needed. + +INTEGERS { output.state before.all mid.sentence } + +FUNCTION {init.state.consts} +{ #0 'before.all := + #1 'mid.sentence := +} + +% Scratch variables: + +STRINGS { s t } + +% Utility functions + +FUNCTION {shows} +{ duplicate$ ":::: `" swap$ * "'" * top$ +} + +FUNCTION {showstack} +{"STACK=====================================================================" +top$ +stack$ +"ENDSTACK==================================================================" +top$ +} + +FUNCTION {not} +{ { #0 } + { #1 } + if$ +} + +FUNCTION {and} +{ 'skip$ + { pop$ #0 } + if$ +} + +FUNCTION {or} +{ { pop$ #1 } + 'skip$ + if$ +} + +FUNCTION {field.or.null} +{ duplicate$ empty$ + { pop$ "" } + 'skip$ + if$ +} + +FUNCTION {emphasize} +{ duplicate$ empty$ + { pop$ "" } + { "\emph{" swap$ * "}" * } + if$ +} + +% n.dashify is used to make sure page ranges get the TeX code +% (two hyphens) for en-dashes. + +FUNCTION {n.dashify} +{ 't := + "" + { t empty$ not } + { t #1 #1 substring$ "-" = + { t #1 #2 substring$ "--" = not + { "--" * + t #2 global.max$ substring$ 't := + } + { { t #1 #1 substring$ "-" = } + { "-" * + t #2 global.max$ substring$ 't := + } + while$ + } + if$ + } + { t #1 #1 substring$ * + t #2 global.max$ substring$ 't := + } + if$ + } + while$ +} + +% tie.or.space.connect connects two items with a ~ if the +% second item is less than 3 letters long, otherwise it just puts an +% ordinary space. + +FUNCTION {tie.or.space.connect} +{ duplicate$ text.length$ #3 < + { "~" } + { " " } + if$ + swap$ * * +} + +FUNCTION {add.space.if.necessary} +{ duplicate$ "" = + 'skip$ + { " " * } + if$ +} + +% either.or.check gives a warning if two mutually exclusive fields +% were used in the database. + +FUNCTION {either.or.check} +{ empty$ + 'pop$ + { "can't use both " swap$ * " fields in " * cite$ * warning$ } + if$ +} + +% output.nonnull is called by output. + +FUNCTION {output.nonnull} +% remove the top item from the stack because it's in the way. +{ 's := + output.state mid.sentence = +% If we're in mid-sentence, add a comma to the new top item and write it + { ", " * write$ } +% Otherwise, if we're at the beginning of a bibitem, + { output.state before.all = +% just write out the top item from the stack; + 'write$ +% and the last alternative is that we're at the end of the current +% bibitem, so we add a period to the top stack item and write it out. + { add.period$ " " * write$ } + if$ + mid.sentence 'output.state := + } + if$ +% Put the top item back on the stack that we removed earlier. + s +} + +% Output checks to see if the stack top is empty; if not, it +% calls output.nonnull to write it out. + +FUNCTION {output} +{ duplicate$ empty$ + 'pop$ + 'output.nonnull + if$ +} + +% Standard warning message for a missing or empty field. For the user +% we call any such field `missing' without respect to the distinction +% made by BibTeX between missing and empty. + +FUNCTION {missing.warning} +{ "missing " swap$ * " in " * cite$ * warning$ } + +% Output.check is like output except that it gives a warning on-screen +% if the given field in the database entry is empty. t is the field +% name. + +FUNCTION {output.check} +{ 't := + duplicate$ empty$ + { pop$ t missing.warning } + 'output.nonnull + if$ +} + +FUNCTION {output.bibitem} +{ newline$ + "\bibitem{" write$ + cite$ write$ + "}" write$ + newline$ +% This empty string is the first thing that will be written +% the next time write$ is called. Done this way because each +% item is saved on the stack until we find out what punctuation +% should be added after it. Therefore we need an empty first item. + "" + before.all 'output.state := +} + +FUNCTION {fin.entry} +{ add.period$ + write$ + newline$ +} + +% Removed new.block, new.block.checka, new.block.checkb, new.sentence, +% new.sentence.checka, and new.sentence.checkb functions here, since they +% don't seem to be needed in the AMS style. Also moved some real +% basic functions like `and' and 'or' earlier in the file. + +INTEGERS { nameptr namesleft numnames } + +% The extra section to write out a language field was added +% for AMSPLAIN.BST. Not present in plain.bst. + +FUNCTION {format.language} +{ language empty$ + { "" } + { " (" language * ")" * } + if$ +} + +% This version of format.names puts names in the format +% +% First von Last, Jr. +% +% (i.e., first name first, no abbreviating to initials). + +FUNCTION {format.names} +{ 's := + #1 'nameptr := + s num.names$ 'numnames := + numnames 'namesleft := + { namesleft #0 > } + { s nameptr "{ff~}{vv~}{ll}{, jj}" format.name$ 't := + nameptr #1 > + { namesleft #1 > + { ", " * t * } + { numnames #2 > + { "," * } + 'skip$ + if$ + t "others" = + { " et~al." * } + { " and " * t * } + if$ + } + if$ + } + 't + if$ + nameptr #1 + 'nameptr := + namesleft #1 - 'namesleft := + } + while$ +} + +FUNCTION {format.authors} +{ author empty$ + { "" } + { extra.label "\bysame" = + {"\bysame"} + { author format.names } + if$ + } + if$ +} + +FUNCTION {format.editors} +{ editor empty$ + { "" } + { editor format.names + editor num.names$ #1 > + { " (eds.)" * } + { " (ed.)" * } + if$ + } + if$ +} + +FUNCTION {format.nonauthor.editors} +{ editor empty$ + { "" } + { editor format.names + editor num.names$ #1 > + { ", eds." * } + { ", ed." * } + if$ + } + if$ +} + +FUNCTION {format.title} +{ title empty$ + { "" } + { title "t" change.case$ emphasize } + if$ +} + +% Function modified to wrap the eprint number in an mbox construction - GJK + +FUNCTION {format.eprint} +{ eprint empty$ + { "" } + %{ "\mbox{" eprint * "}" * } + { "{" eprint * "}" * } + if$ +} + +FUNCTION {format.doi} +{ doi empty$ + { "" } + %{ "\mbox{" doi * "}" * } + { "{" doi * "}" * } + if$ +} + +FUNCTION {format.journal.vol.year} +{ journal empty$ + { "journal name" missing.warning ""} + { journal } + if$ + volume empty$ + 'skip$ + { " \textbf{" * volume * "}" * } + if$ + year empty$ + { "year" missing.warning } + { " (" * year * ")" * } + if$ +} + +% For formatting the issue number for a journal article. + +FUNCTION {format.number} +{ number empty$ + { "" } + { "no.~" number * } + if$ +} + +% For formatting miscellaneous dates + +FUNCTION {format.date} +{ year empty$ + { month empty$ + { "" } + { "there's a month but no year in " cite$ * warning$ + month + } + if$ + } + { month empty$ + 'year + { month " " * year * } + if$ + } + if$ +} + +%% The volume, series and number information is sort of tricky. +%% This code handles it as follows: +%% If the series is present, and the volume, but not the number, +%% then we do "\emph{Book title}, Series Name, vol. 000" +%% If the series is present, and the number, but not the volume, +%% then we do "\emph{Book title}, Series Name, no. 000" +%% If the series is present, and both number and volume, +%% then we do "\emph{Book title}, vol. XX, Series Name, no. 000" +%% Finally, if the series is absent, +%% then we do "\emph{Book title}, vol. XX" +%% or "\emph{Book title}, no. 000" +%% and if both volume and number are present, give a warning message. + +FUNCTION {format.bookvolume.series.number} +{ volume empty$ + { "" % Push the empty string as a placeholder in case everything else + % is empty too. + series empty$ + 'skip$ + { pop$ series } % if series is not empty put in stack + if$ + number empty$ + 'skip$ + { duplicate$ empty$ % if no preceding material, + 'skip$ % do nothing, otherwise + { ", " * } % add a comma and space to separate. + if$ + "no." number tie.or.space.connect * % add the number information + } + if$ + } +%% If the volume is NOT EMPTY: + { "vol." volume tie.or.space.connect % vol. XX + number empty$ + { series empty$ + 'skip$ + { series ", " * swap$ *} % Series Name, vol. XX + if$ + } + { series empty$ + { "can't use both volume and number if series info is missing" + warning$ + "in BibTeX entry type `" type$ * "'" * top$ + } + { ", " * series * ", no." * number tie.or.space.connect } + if$ + } + if$ + } + if$ + +} % end of format.bookvolume.series.number + +%% format.inproc.title.where.editors is used by inproceedings entry types + +FUNCTION {format.inproc.title.address.editors} +{ booktitle empty$ + { "" } +%% No case changing or emphasizing for the title. We want initial +%% caps, roman. + { booktitle } + if$ +%% We add parentheses around the address (place where conference +%% was held). + address empty$ + 'skip$ + { add.space.if.necessary "(" * address * ")" * } + if$ +%% Likewise we add parentheses around the editors' names. + editor empty$ + 'skip$ + { add.space.if.necessary "(" * format.nonauthor.editors * ")" * } + if$ +} + +%% format.incoll.title.editors is similar to format.inproc... but +%% omits the address. For collections that are not proceedings volumes. + +FUNCTION {format.incoll.title.editors} +{ booktitle empty$ + { "" } +%% No case changing or emphasizing for the title. We want initial +%% caps, roman. + { booktitle } + if$ +%% We add parentheses around the editors' names. + editor empty$ + 'skip$ + { add.space.if.necessary "(" * format.nonauthor.editors * ")" * } + if$ +} + +% Desired output for format.number.series: +% +% Lecture Notes in Math., no.~1224 + +FUNCTION {format.number.series} +{ series empty$ + { number empty$ + { "" } + { "there's a number but no series in " cite$ * warning$ } + if$ + } + { series + number empty$ + 'skip$ + { ", no.~" * number * } + if$ + } + if$ +} + +FUNCTION {format.edition} +{ edition empty$ + { "" } + { output.state mid.sentence = + { edition "l" change.case$ " ed." * } + { edition "t" change.case$ " ed." * } + if$ + } + if$ +} + +INTEGERS { multiresult } + +FUNCTION {multi.page.check} +{ 't := + #0 'multiresult := + { multiresult not + t empty$ not + and + } + { t #1 #1 substring$ + duplicate$ "-" = + swap$ duplicate$ "," = + swap$ "+" = + or or + { #1 'multiresult := } + { t #2 global.max$ substring$ 't := } + if$ + } + while$ + multiresult +} + +FUNCTION {format.pages} +{ pages empty$ + { "" } + { pages n.dashify } + if$ +} + +FUNCTION {format.book.pages} +{ pages empty$ + { "" } + { pages multi.page.check + { "pp.~" pages n.dashify * } + { "p.~" pages * } + if$ + } + if$ +} + +FUNCTION {format.chapter.pages} +{ chapter empty$ + 'format.pages + { type empty$ + { "ch.~" } + { type "l" change.case$ " " * } + if$ + chapter * + pages empty$ + 'skip$ + { ", " * format.book.pages * } + if$ + } + if$ +} + +FUNCTION {empty.misc.check} +{ author empty$ title empty$ howpublished empty$ + month empty$ year empty$ note empty$ + and and and and and + key empty$ not and + { "all relevant fields are empty in " cite$ * warning$ } + 'skip$ + if$ +} + +FUNCTION {format.thesis.type} +{ type empty$ + 'skip$ + { pop$ + type "t" change.case$ + } + if$ +} + +FUNCTION {format.tr.number} +{ type empty$ + { "Tech. Report" } + 'type + if$ + number empty$ + { "t" change.case$ } + { number tie.or.space.connect } + if$ +} + +% The format.crossref functions haven't been paid much attention +% at the present time (June 1990) and could probably use some +% work. MJD + +FUNCTION {format.article.crossref} +{ key empty$ + { journal empty$ + { "need key or journal for " cite$ * " to crossref " * crossref * + warning$ + "" + } + { "In " journal * } + if$ + } + { "In " key * } + if$ + " \cite{" * crossref * "}" * +} + +FUNCTION {format.crossref.editor} +{ editor #1 "{vv~}{ll}" format.name$ + editor num.names$ duplicate$ + #2 > + { pop$ " et~al." * } + { #2 < + 'skip$ + { editor #2 "{ff }{vv }{ll}{ jj}" format.name$ "others" = + { " et~al." * } + { " and " * editor #2 "{vv~}{ll}" format.name$ * } + if$ + } + if$ + } + if$ +} + +FUNCTION {format.book.crossref} +{ volume empty$ + { "empty volume in " cite$ * "'s crossref of " * crossref * warning$ + "In " + } + { "Vol." volume tie.or.space.connect + " of " * + } + if$ + editor empty$ + editor field.or.null author field.or.null = + or + { key empty$ + { series empty$ + { "need editor, key, or series for " cite$ * " to crossref " * + crossref * warning$ + "" * + } + { series * } + if$ + } + { key * } + if$ + } + { format.crossref.editor * } + if$ + " \cite{" * crossref * "}" * +} + +FUNCTION {format.incoll.inproc.crossref} +{ editor empty$ + editor field.or.null author field.or.null = + or + { key empty$ + { booktitle empty$ + { "need editor, key, or booktitle for " cite$ * " to crossref " * + crossref * warning$ + "" + } + { "In \emph{" booktitle * "}" * } + if$ + } + { "In " key * } + if$ + } + { "In " format.crossref.editor * } + if$ + " \cite{" * crossref * "}" * +} + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +% The main functions for each entry type. + +% journal, vol and year are formatted together because they are +% not separated by commas. + +FUNCTION {article} +{ output.bibitem + format.authors "author" output.check + format.title "title" output.check + crossref missing$ + { format.journal.vol.year output + format.number output + format.pages "pages" output.check + } + { format.article.crossref output.nonnull + format.pages output + } + if$ + format.language * + format.eprint output +% format.doi output + note output + fin.entry +} + +FUNCTION {book} +{ output.bibitem + author empty$ + { format.editors "author and editor" output.check } + { format.authors output.nonnull + crossref missing$ + { "author and editor" editor either.or.check } + 'skip$ + if$ + } + if$ + format.title "title" output.check + format.edition output + crossref missing$ + { format.bookvolume.series.number output + publisher "publisher" output.check + address output + } + { format.book.crossref output.nonnull + } + if$ + format.date "year" output.check + format.language * + format.eprint output +% format.doi output + note output + fin.entry +} + +FUNCTION {booklet} +{ output.bibitem + format.authors output + format.title "title" output.check + howpublished output + address output + format.date output + format.eprint output +% format.doi output + note output + fin.entry +} + +FUNCTION {inbook} +{ output.bibitem + author empty$ + { format.editors "author and editor" output.check } + { format.authors output.nonnull + crossref missing$ + { "author and editor" editor either.or.check } + 'skip$ + if$ + } + if$ + title "title" output.check + crossref missing$ + { format.bookvolume.series.number output + format.chapter.pages "chapter and pages" output.check + format.number.series output + publisher "publisher" output.check + address output + } + { format.chapter.pages "chapter and pages" output.check + format.book.crossref output.nonnull + } + if$ + format.edition output + format.date "year" output.check + format.book.pages output + format.language * + format.eprint output +% format.doi output + note output + fin.entry +} + +FUNCTION {incollection} +{ output.bibitem + format.authors "author" output.check + format.title "title" output.check + crossref missing$ + { format.incoll.title.editors "booktitle" output.check + format.bookvolume.series.number output + publisher "publisher" output.check + address output + format.edition output + format.date "year" output.check + } + { format.incoll.inproc.crossref output.nonnull + } + if$ + format.eprint output +% format.doi output + note output + format.book.pages output + format.language * + fin.entry +} + +FUNCTION {inproceedings} +{ output.bibitem + format.authors "author" output.check + format.title "title" output.check + crossref missing$ + { format.inproc.title.address.editors "booktitle" output.check + format.bookvolume.series.number output + organization output + publisher output + format.date "year" output.check + } + { format.incoll.inproc.crossref output.nonnull + } + if$ + format.eprint output +% format.doi output + note output + format.book.pages output + format.language * + fin.entry +} + +FUNCTION {conference} { inproceedings } + +FUNCTION {manual} +{ output.bibitem + author empty$ + { organization empty$ + 'skip$ + { organization output.nonnull + address output + } + if$ + } + { format.authors output.nonnull } + if$ + format.title "title" output.check + author empty$ + { organization empty$ + { address output } + 'skip$ + if$ + } + { organization output + address output + } + if$ + format.edition output + format.date output + format.eprint output +% format.doi output + note output + fin.entry +} + +FUNCTION {mastersthesis} +{ output.bibitem + format.authors "author" output.check + format.title "title" output.check + "Master's thesis" format.thesis.type output.nonnull + school "school" output.check + address output + format.date "year" output.check + format.eprint output +% format.doi output + note output + fin.entry +} + +FUNCTION {misc} +{ output.bibitem + format.authors output + format.title output + howpublished output + format.date output + format.eprint output +% format.doi output + note output + format.book.pages output + fin.entry + empty.misc.check +} + +FUNCTION {phdthesis} +{ output.bibitem + format.authors "author" output.check + format.title "title" output.check + "Ph.D. thesis" format.thesis.type output.nonnull + school "school" output.check + address output + format.date "year" output.check + format.eprint output +% format.doi output + note output + format.book.pages output + fin.entry +} + +FUNCTION {proceedings} +{ output.bibitem + editor empty$ + { organization output } + { format.editors output.nonnull } + if$ + format.title "title" output.check + format.bookvolume.series.number output + address empty$ + { editor empty$ + 'skip$ + { organization output } + if$ + publisher output + format.date "year" output.check + } + { address output.nonnull + editor empty$ + 'skip$ + { organization output } + if$ + publisher output + format.date "year" output.check + } + if$ + format.eprint output +% format.doi output + note output + fin.entry +} + +FUNCTION {techreport} +{ output.bibitem + format.authors "author" output.check + format.title "title" output.check + format.tr.number output.nonnull + institution "institution" output.check + address output + format.date "year" output.check + format.eprint output +% format.doi output + note output + fin.entry +} + +FUNCTION {unpublished} +{ output.bibitem + format.authors "author" output.check + format.title "title" output.check + note "note" output.check + format.date output + format.eprint output +% format.doi output + fin.entry +} + +FUNCTION {default.type} { misc } + +MACRO {jan} {"January"} + +MACRO {feb} {"February"} + +MACRO {mar} {"March"} + +MACRO {apr} {"April"} + +MACRO {may} {"May"} + +MACRO {jun} {"June"} + +MACRO {jul} {"July"} + +MACRO {aug} {"August"} + +MACRO {sep} {"September"} + +MACRO {oct} {"October"} + +MACRO {nov} {"November"} + +MACRO {dec} {"December"} + +READ + +FUNCTION {sortify} +{ purify$ + "l" change.case$ +} + +INTEGERS { len } + +FUNCTION {chop.word} +{ 's := + 'len := + s #1 len substring$ = + { s len #1 + global.max$ substring$ } + 's + if$ +} + +FUNCTION {sort.format.names} +{ 's := + #1 'nameptr := + "" + s num.names$ 'numnames := + numnames 'namesleft := + { namesleft #0 > } + { nameptr #1 > + { " " * } + 'skip$ + if$ + s nameptr "{vv{ } }{ll{ }}{ ff{ }}{ jj{ }}" format.name$ 't := + nameptr numnames = t "others" = and + { "et al" * } + { t sortify * } + if$ + nameptr #1 + 'nameptr := + namesleft #1 - 'namesleft := + } + while$ +} + +FUNCTION {sort.format.title} +{ 't := + "A " #2 + "An " #3 + "The " #4 t chop.word + chop.word + chop.word + sortify + #1 global.max$ substring$ +} + +FUNCTION {author.sort} +{ author empty$ + { key empty$ + { "to sort, need author or key in " cite$ * warning$ + "" + } + { key sortify } + if$ + } + { author sort.format.names } + if$ +} + +FUNCTION {author.editor.sort} +{ author empty$ + { editor empty$ + { key empty$ + { "to sort, need author, editor, or key in " cite$ * warning$ + "" + } + { key sortify } + if$ + } + { editor sort.format.names } + if$ + } + { author sort.format.names } + if$ +} + +FUNCTION {author.organization.sort} +{ author empty$ + { organization empty$ + { key empty$ + { "to sort, need author, organization, or key in " cite$ * warning$ + "" + } + { key sortify } + if$ + } + { "The " #4 organization chop.word sortify } + if$ + } + { author sort.format.names } + if$ +} + +FUNCTION {editor.organization.sort} +{ editor empty$ + { organization empty$ + { key empty$ + { "to sort, need editor, organization, or key in " cite$ * warning$ + "" + } + { key sortify } + if$ + } + { "The " #4 organization chop.word sortify } + if$ + } + { editor sort.format.names } + if$ +} + +FUNCTION {presort} +{ type$ "book" = + type$ "inbook" = + or + 'author.editor.sort + { type$ "proceedings" = + 'editor.organization.sort + { type$ "manual" = + 'author.organization.sort + 'author.sort + if$ + } + if$ + } + if$ + " " + * + year field.or.null sortify + * + " " + * + title field.or.null + sort.format.title + * + #1 entry.max$ substring$ + 'sort.key$ := +} + +ITERATE {presort} + +SORT + +STRINGS { longest.label prev.author this.author } + +INTEGERS { number.label longest.label.width } + +FUNCTION {initialize.longest.label} +{ "" 'longest.label := + #1 'number.label := + #0 'longest.label.width := + "abcxyz" 'prev.author := + "" 'this.author := +} + +FUNCTION {longest.label.pass} +{ number.label int.to.str$ 'label := + number.label #1 + 'number.label := + label width$ longest.label.width > + { label 'longest.label := + label width$ 'longest.label.width := + } + 'skip$ + if$ + author empty$ + { editor empty$ + { "" } + 'editor + if$ + } + 'author + if$ + 'this.author := + this.author prev.author = + { "\bysame" 'extra.label := } + { "" 'extra.label := + this.author "" = + { "abcxyz" } + 'this.author + if$ + 'prev.author := + } + if$ +} + +EXECUTE {initialize.longest.label} + +ITERATE {longest.label.pass} + +FUNCTION {begin.bib} +{ preamble$ empty$ + 'skip$ + { preamble$ write$ newline$ } + if$ + "\providecommand{\bysame}{\leavevmode\hbox to3em{\hrulefill}\thinspace}" + write$ newline$ + "\providecommand{\href}[2]{#2}" + write$ newline$ + "\begin{thebibliography}{" longest.label * "}" * write$ newline$ +} + +EXECUTE {begin.bib} + +EXECUTE {init.state.consts} + +ITERATE {call.type$} + +FUNCTION {end.bib} +{ newline$ + "\end{thebibliography}" write$ newline$ +} + +EXECUTE {end.bib} +%% \CharacterTable +%% {Upper-case \A\B\C\D\E\F\G\H\I\J\K\L\M\N\O\P\Q\R\S\T\U\V\W\X\Y\Z +%% Lower-case \a\b\c\d\e\f\g\h\i\j\k\l\m\n\o\p\q\r\s\t\u\v\w\x\y\z +%% Digits \0\1\2\3\4\5\6\7\8\9 +%% Exclamation \! Double quote \" Hash (number) \# +%% Dollar \$ Percent \% Ampersand \& +%% Acute accent \' Left paren \( Right paren \) +%% Asterisk \* Plus \+ Comma \, +%% Minus \- Point \. Solidus \/ +%% Colon \: Semicolon \; Less than \< +%% Equals \= Greater than \> Question mark \? +%% Commercial at \@ Left bracket \[ Backslash \\ +%% Right bracket \] Circumflex \^ Underscore \_ +%% Grave accent \` Left brace \{ Vertical bar \| +%% Right brace \} Tilde \~} diff --git a/AShortProofOfTheHiltonMilnerTheorem/docs/source/A_short_proof_of_the_Hilton-Milner_theorem.tex b/AShortProofOfTheHiltonMilnerTheorem/docs/source/A_short_proof_of_the_Hilton-Milner_theorem.tex new file mode 100644 index 0000000..031bfe0 --- /dev/null +++ b/AShortProofOfTheHiltonMilnerTheorem/docs/source/A_short_proof_of_the_Hilton-Milner_theorem.tex @@ -0,0 +1,374 @@ +\batchmode +\makeatletter +\def\input@path{{"/Users/russw/Documents/Research/mypapers/A short proof of the Hilton-Milner theorem/"}} +\makeatother +\documentclass[12pt,oneside,english,lowtilde]{amsart} +\usepackage[T1]{fontenc} +\usepackage[latin9]{inputenc} +\usepackage{babel} +\usepackage{url} +\usepackage{amstext} +\usepackage{amsthm} +\usepackage{amssymb} +\usepackage{geometry} +\geometry{verbose,tmargin=3cm,bmargin=3cm,lmargin=3cm,rmargin=3cm} +\usepackage[dvips,pdfusetitle, + bookmarks=true,bookmarksnumbered=false,bookmarksopen=false, + breaklinks=false,pdfborder={0 0 1},backref=false,colorlinks=false] + {hyperref} +\usepackage{breakurl} + +\makeatletter +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% Textclass specific LaTeX commands. +\newlength{\lyxlabelwidth} % auxiliary length +\theoremstyle{plain} +\newtheorem{thm}{\protect\theoremname} +\theoremstyle{plain} +\newtheorem{lem}[thm]{\protect\lemmaname} +\theoremstyle{remark} +\newtheorem{rem}[thm]{\protect\remarkname} + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% User specified LaTeX commands. +%% Latin modern fonts should prevent arXiv fuzziness +\usepackage{lmodern} + +%% minimize spacing around wrap-figs +\setlength\intextsep{.5em} + +\makeatother + +\providecommand{\lemmaname}{Lemma} +\providecommand{\remarkname}{Remark} +\providecommand{\theoremname}{Theorem} + +\begin{document} +\global\long\def\link{\operatorname{link}}% + +\global\long\def\del{\operatorname{del}}% + +\global\long\def\cone{\operatorname{Cone}}% + +\global\long\def\depth{\operatorname{depth}}% + +\global\long\def\shift{\operatorname{Shift}}% + +\global\long\def\symdiff{\ominus}% + +\global\long\def\shiftext{\shift^{\wedge}}% + +\global\long\def\extalg{\bigwedge}% + +\global\long\def\ff{\mathbb{F}}% + +\global\long\def\bdry{\partial}% + +% Default proof to no "Proof." at start +\renewcommand{\proofname}{\hskip-\labelsep\spacefactor3000 } +\title{A short proof of the Hilton-Milner Theorem} +\author{Denys Bulavka and Russ Woodroofe} +\thanks{Work of the first author is partially supported by the Israel Science +Foundation grant ISF-2480/20 and the AARMS postdoctoral fellowship. +Work of the second author is supported in part by the Slovenian Research +Agency (research program P1-0285 and research projects J1-9108, J1-2451, +J1-3003, and J1-50000).} +\address{Einstein Institute of Mathematics, Hebrew University, Jerusalem 91904, +Israel} +\curraddr{Department of Mathematics \& Statistics, Dalhousie University, 6297 +Castine Way, PO BOX 15000, Halifax, NS, Canada, B3H 4R2} +\email{denys.bulavka@dal.ca} +\urladdr{\url{https://kam.mff.cuni.cz/~dbulavka/}} +\address{Univerza na Primorskem, Glagoljaka 8, 6000 Koper, Slovenia} +\email{russ.woodroofe@famnit.upr.si} +\urladdr{\url{https://osebje.famnit.upr.si/~russ.woodroofe/}} +\begin{abstract} +We give a short and relatively elementary proof of the Hilton-Milner +Theorem. +\end{abstract} + +\maketitle +The Hilton-Milner Theorem gives the maximum size of a uniform pairwise-intersecting +family of sets that do not share a common element. +\begin{thm}[Hilton and Milner 1967 \cite{Hilton/Milner:1967}] +\label{thm:HM}Let $k\leq n/2$. If $\mathcal{F}$ is a family of +pairwise-intersecting $k$-element subsets of $[n]$, where $\bigcap_{F\in\mathcal{F}}F=\emptyset$, +then $\left|\mathcal{F}\right|\leq{n-1 \choose k-1}-{n-1-k \choose k-1}+1$. +\end{thm} + +In the current article, we will show Theorem~\ref{thm:HM} to follow +quickly from the following theorem, which we believe to be of some +independent interest. Two set systems $\mathcal{A}$ and $\mathcal{B}$ +are \emph{cross-intersecting} if for every $A\in\mathcal{A},B\in\mathcal{B}$, +the intersection $A\cap B$ is nonempty. The \emph{shadow} $\bdry B$ +of a $k$-element set $B$ consists of all the $(k-1)$-element subsets +of $B$; the shadow of a uniform set family is the union of the shadows +of its constituent sets, thus consists of all $(k-1)$-element subsets +of constituent sets. +\begin{thm} +\label{thm:MainTechnical}Let $2k-1\leq n$, let $\mathcal{A}$ be +a family of $(k-1)$-element subsets of $[n]$, and let $\mathcal{B}$ +be a family of $k$-element subsets of $[n]$. If $\mathcal{A},\mathcal{B}$ +are cross-intersecting, $\mathcal{B}$ is nonempty, and $\bdry\mathcal{B}\subseteq\mathcal{A}$, +then +\[ +\left|\mathcal{A}\right|+\left|\mathcal{B}\right|\leq{n \choose k-1}-{n-k \choose k-1}+1. +\] +\end{thm} + +Note that the bound of Theorem~\ref{thm:HM} is attained with a single +$k$-element set $B$ that does not contain $1$, together with all +the $k$-element sets that contain $1$ and intersect $B$; the bound +of Theorem~\ref{thm:MainTechnical} is attained with a single $k$-element +set and all $(k-1)$-element sets that intersect it. + +Our proof of Theorem~\ref{thm:HM} may be viewed as injective. Other +recent proofs of Theorem~\ref{thm:HM} were given in \cite{Frankl:2019,Hurlbert/Kamat:2018}, +but instead of relying on a simple cross-intersecting type theorem, +both of these proofs rely on a certain ``partial complement'' operation. +In somewhat older work \cite{Frankl/Tokushige:1992} (see also \cite{Frankl:2016}), +Frankl and Tokushige gave a proof of Hilton-Milner from a different +cross-intersection theorem, but the proof is less elementary than +that of Theorem~\ref{thm:MainTechnical}, requiring the Schtzenberger-Kruskal-Katona +Theorem. A recent preprint of Wu, Li, Feng, Liu and Yu \cite{Wu/Li/Feng/Liu/Yu:2026} +(now published) gives a proof based on still another cross-intersecting +theorem, but the existing proofs of this underlying result also seem +to be somewhat more difficult than our approach. + +\subsection*{Shifting} + +We recall that a system $\mathcal{F}$ of subsets of $[n]$ is \emph{shifted} +if for each $ik\geq4$. Here, we strengthen the hypothesis of Theorem~\ref{thm:MainTechnical} +to require $\mathcal{B}$ to have at least two elements. We discuss +the details in the following section. + +\subsection*{Uniqueness of the Hilton-Milner family} + +As mentioned in the discussion, the same techniques give uniqueness +of the maximum family in Theorem~\ref{thm:HM}. We prove: +\begin{thm} +\label{thm:StrictHM}In the situation of Theorem~\ref{thm:HM}, if +$4\leq k