Formalize Chvátal's conjecture (a downset's largest intersecting subfamily is a star) in Lean 4

With `Decreasing F := ∀ A B, B ⊆ A → A ∈ F → B ∈ F` (closed under subsets) and `Intersecting G := ∀ A ∈ G, ∀ B ∈ G, A ∩ B ≠ ∅`, prove (currently a `sorry`): ``` theorem exists_maximal_star {α : Type} [Fintype α] [DecidableEq α] [Nonempty α] : ∀ F : Finset (Finset α), Decreasing F → ∃ x : α, ∀ G, G ⊆ F → Intersecting G → G.card ≤ { A ∈ F | x ∈ A }.card ``` Meaning: in any downward-closed set family $F$ there is an element $x$ whose star $\{A\in F : x\in A\}$ is an intersecting subfamily of maximum possible cardinality among all intersecting subfamilies of $F$.

Acceptance. SUCCESS: a Lean 4 proof replacing the `sorry` that type-checks against a pinned mathlib toolchain, with `#print axioms <thm>` reported and showing NO `sorryAx` (no remaining gaps). Expected pure-kernel: the only axioms should be `[propext, Classical.choice, Quot.sound]`; state explicitly that this holds. Genuinely open; a counterexample would also be a result. Partial: proving established special cases (e.g. families over a small ground set) in Lean.