Sanity check: $f(0,1) = 1$

Non-blind read-back — not independent testimony. This read-back was written by the same agent that drafted the Lean statements of this proposal (not by a blind auditor with a fresh context), and that agent had seen the source material and knew the intended meaning while writing it. Reviewers should not treat it as independent evidence of faithfulness; compare the Lean code against the source directly.

The statement asserts the equality $f(0,1) = 1$ of natural numbers, with no hypotheses. Here $f(n,k)$ is the sunflower threshold: the least $m\in\mathbb N$ (with $\inf\emptyset := 0$) such that for every type $\alpha$ and every family $\mathcal F$ of subsets of $\alpha$ all of whose members have $\operatorname{ncard} = n$ and with $m \le \operatorname{ncard}(\mathcal F)$, some subfamily $\mathcal S\subseteq\mathcal F$ with $\operatorname{ncard}(\mathcal S)=k$ has all pairwise intersections of distinct members equal to one common set ($\operatorname{ncard}$ counts elements of finite sets and is $0$ on infinite sets). With $n=0$ and $k=1$ it therefore says: the least $m$ such that every family of sets of $\operatorname{ncard}$ $0$ (i.e. empty sets or infinite sets) having $\operatorname{ncard}$ at least $m$ contains a one-member subfamily (a one-member family is automatically a sunflower), equals $1$.