Cao-Chen-Miller Egg-Drop Refutation

Abstract

A correct bounded egg-drop strategy separates all hidden points by fixed-length binary transcripts. At four dimensions, five eggs, and side length five, the conjectured nine-drop budget has too few transcripts.

Definition 1.1 (Hidden critical points).

$$\forall d\in \mathrm{Nat},\forall N\in \mathrm{Fin}\left(d\right)\to \mathrm{Nat},\mathrm{Point}\left(N\right)=\left(\forall i\in \mathrm{Fin}\left(d\right),\mathrm{Fin}\left(N\left(i\right)\right)\right)$$

Formalization. D5/S3/Observer/Budget/CaoChenMillerEggDropRefutation.Point (✓ std3).

Citation. Xiangwen Cao and Zongyun Chen and Steven J. Miller (2025). Egg Drop Problems: They Are All They Are Cracked Up To Be!. DOI: 10.48550/arXiv.2511.18330. URL: https://arxiv.org/abs/2511.18330.

Commentary.

For side function N on Fin d, Point(N) is the dependent product of Fin(N(i)). The zero-based representatives encode the paper’s coordinates 1 through N(i).

Definition 1.2 (Discrete query locations).

$$\forall d\in \mathrm{Nat},\forall N\in \mathrm{Fin}\left(d\right)\to \mathrm{Nat},\mathrm{Query}\left(N\right)=\left(\forall i\in \mathrm{Fin}\left(d\right),\mathrm{Fin}\left(N\left(i\right)+1\right)\right)$$

Formalization. D5/S3/Observer/Budget/CaoChenMillerEggDropRefutation.Query (✓ std3).

Citation. Xiangwen Cao and Zongyun Chen and Steven J. Miller (2025). Egg Drop Problems: They Are All They Are Cracked Up To Be!. DOI: 10.48550/arXiv.2511.18330. URL: https://arxiv.org/abs/2511.18330.

Commentary.

Query(N) is the dependent product of Fin(N(i)+1), representing physical query coordinates 0 through N(i). For integer hidden coordinates, a real drop position has the same outcomes as its coordinatewise floor, so real-valued positions reduce to this discrete carrier.

Definition 1.3 (Broken-or-intact query outcome).

$$\forall d\in \mathrm{Nat},\forall N\in \mathrm{Fin}\left(d\right)\to \mathrm{Nat},\forall q\in \mathrm{Query}\left(N\right),\forall x\in \mathrm{Point}\left(N\right),\mathrm{dropOutcome}\left(q,x\right)=\mathrm{if}\left(\forall i\in \mathrm{Fin}\left(d\right),\mathrm{val}\left(q\left(i\right)\right)\le \mathrm{val}\left(x\left(i\right)\right),1,0\right)$$

Formalization. D5/S3/Observer/Budget/CaoChenMillerEggDropRefutation.dropOutcome (✓ std3).

Citation. Xiangwen Cao and Zongyun Chen and Steven J. Miller (2025). Egg Drop Problems: They Are All They Are Cracked Up To Be!. DOI: 10.48550/arXiv.2511.18330. URL: https://arxiv.org/abs/2511.18330.

Commentary.

A hidden value h(i) encodes the physical coordinate x(i)=h(i)+1, while q(i) is the physical query coordinate. Hence q(i)<x(i) is equivalent to val(q(i))<=val(h(i)); the value is one exactly when this holds in every coordinate, and is zero otherwise.

Definition 1.4 (Adaptive strategies with egg and drop budgets).

$$\forall d\in \mathrm{Nat},\forall N\in \mathrm{Fin}\left(d\right)\to \mathrm{Nat},\begin{array}{r}\mathrm{EggStrategy}\left(N\right):\mathrm{Nat}\to \left(\mathrm{Nat}\to \mathrm{Type}\right),\\ \mathrm{stop}\left(\right):\forall e\in \mathrm{Nat},\forall h\in \mathrm{Nat},\mathrm{Point}\left(N\right)\to \mathrm{EggStrategy}\left(N,e,h\right),\\ \mathrm{drop}\left(\right):\forall e\in \mathrm{Nat},\forall h\in \mathrm{Nat},\mathrm{Query}\left(N\right)\to \left(\mathrm{EggStrategy}\left(N,e,h\right)\to \left(\mathrm{EggStrategy}\left(N,e+1,h\right)\to \mathrm{EggStrategy}\left(N,e+1,h+1\right)\right)\right).\end{array}$$

Formalization. D5/S3/Observer/Budget/CaoChenMillerEggDropRefutation.EggStrategy (✓ std3).

Citation. Xiangwen Cao and Zongyun Chen and Steven J. Miller (2025). Egg Drop Problems: They Are All They Are Cracked Up To Be!. DOI: 10.48550/arXiv.2511.18330. URL: https://arxiv.org/abs/2511.18330.

Commentary.

A stop node returns a point at any remaining budget. A drop node asks one query from Query(N), sends outcome zero to a child with one fewer egg, sends outcome one to a child with the same egg count, and consumes one drop.

Definition 1.5 (Terminal prediction).

$$\forall d\in \mathrm{Nat},\forall N\in \mathrm{Fin}\left(d\right)\to \mathrm{Nat},(\forall e\in \mathrm{Nat},\forall h\in \mathrm{Nat},\forall g\in \mathrm{Point}\left(N\right),\forall x\in \mathrm{Point}\left(N\right),\mathrm{prediction}\left((\mathrm{stop}\left(g\right):\mathrm{EggStrategy}\left(N,e,h\right)),x\right)=g)\wedge (\forall e\in \mathrm{Nat},\forall h\in \mathrm{Nat},\forall q\in \mathrm{Query}\left(N\right),\forall b\in \mathrm{EggStrategy}\left(N,e,h\right),\forall t\in \mathrm{EggStrategy}\left(N,e+1,h\right),\forall x\in \mathrm{Point}\left(N\right),\mathrm{prediction}\left(\mathrm{drop}\left(q,b,t\right),x\right)=\mathrm{if}\left(\mathrm{dropOutcome}\left(q,x\right)=0,\mathrm{prediction}\left(b,x\right),\mathrm{prediction}\left(t,x\right)\right))$$

Formalization. D5/S3/Observer/Budget/CaoChenMillerEggDropRefutation.prediction (✓ std3).

Source. Repository-derived.

Acknowledgement. Xiangwen Cao and Zongyun Chen and Steven J. Miller (2025). Egg Drop Problems: They Are All They Are Cracked Up To Be!. DOI: 10.48550/arXiv.2511.18330. URL: https://arxiv.org/abs/2511.18330.

Commentary.

Prediction follows the outcome-selected branch until a stop node and returns that node’s point.

Definition 1.6 (Fixed-length padded transcript).

$$\forall d\in \mathrm{Nat},\forall N\in \mathrm{Fin}\left(d\right)\to \mathrm{Nat},(\forall e\in \mathrm{Nat},\forall h\in \mathrm{Nat},\forall g\in \mathrm{Point}\left(N\right),\forall x\in \mathrm{Point}\left(N\right),\forall j\in \mathrm{Fin}\left(h\right),\mathrm{paddedTranscript}\left((\mathrm{stop}\left(g\right):\mathrm{EggStrategy}\left(N,e,h\right)),x,j\right)=0)\wedge \left((\forall e\in \mathrm{Nat},\forall h\in \mathrm{Nat},\forall q\in \mathrm{Query}\left(N\right),\forall b\in \mathrm{EggStrategy}\left(N,e,h\right),\forall t\in \mathrm{EggStrategy}\left(N,e+1,h\right),\forall x\in \mathrm{Point}\left(N\right),\mathrm{paddedTranscript}\left(\mathrm{drop}\left(q,b,t\right),x,0\right)=\mathrm{dropOutcome}\left(q,x\right))\wedge (\forall e\in \mathrm{Nat},\forall h\in \mathrm{Nat},\forall q\in \mathrm{Query}\left(N\right),\forall b\in \mathrm{EggStrategy}\left(N,e,h\right),\forall t\in \mathrm{EggStrategy}\left(N,e+1,h\right),\forall x\in \mathrm{Point}\left(N\right),\forall j\in \mathrm{Fin}\left(h\right),\mathrm{paddedTranscript}\left(\mathrm{drop}\left(q,b,t\right),x,\mathrm{succ}\left(j\right)\right)=\mathrm{if}\left(\mathrm{dropOutcome}\left(q,x\right)=0,\mathrm{paddedTranscript}\left(b,x,j\right),\mathrm{paddedTranscript}\left(t,x,j\right)\right))\right)$$

Formalization. D5/S3/Observer/Budget/CaoChenMillerEggDropRefutation.paddedTranscript (✓ std3).

Source. Repository-derived.

Acknowledgement. Xiangwen Cao and Zongyun Chen and Steven J. Miller (2025). Egg Drop Problems: They Are All They Are Cracked Up To Be!. DOI: 10.48550/arXiv.2511.18330. URL: https://arxiv.org/abs/2511.18330.

Commentary.

The first coordinate at a drop node is its observed outcome. Later coordinates recurse into the selected child, while every coordinate after a stop node is zero. Thus every transcript has the full budgeted function type Fin h to Fin 2.

Definition 1.7 (Exact recovery).

$$\forall d\in \mathrm{Nat},\forall N\in \mathrm{Fin}\left(d\right)\to \mathrm{Nat},\forall e\in \mathrm{Nat},\forall h\in \mathrm{Nat},\forall s\in \mathrm{EggStrategy}\left(N,e,h\right),(\mathrm{Correct}\left(s\right))\iff (\forall x\in \mathrm{Point}\left(N\right),\mathrm{prediction}\left(s,x\right)=x)$$

Formalization. D5/S3/Observer/Budget/CaoChenMillerEggDropRefutation.Correct (✓ std3).

Citation. Xiangwen Cao and Zongyun Chen and Steven J. Miller (2025). Egg Drop Problems: They Are All They Are Cracked Up To Be!. DOI: 10.48550/arXiv.2511.18330. URL: https://arxiv.org/abs/2511.18330.

Commentary.

A strategy is correct when its terminal prediction equals every possible hidden point.

Definition 1.8 (The conjectured drop budget).

$$\forall d\in \mathrm{Nat},\forall k\in \mathrm{Nat},\forall N\in \mathrm{Fin}\left(d\right)\to \mathrm{Nat},\mathrm{paperBound}\left(d,k,N\right)=\mathrm{natCeil}\left((k-d+1:\mathrm{Real})\cdot \mathrm{rpow}\left(\sum _{i\in \mathrm{Fin}\left(d\right)}((N\left(i\right):\mathrm{Real})),(k-d+1:\mathrm{Real}{)}^{-1}\right)\right)$$

Formalization. D5/S3/Observer/Budget/CaoChenMillerEggDropRefutation.paperBound (✓ std3).

Citation. Xiangwen Cao and Zongyun Chen and Steven J. Miller (2025). Egg Drop Problems: They Are All They Are Cracked Up To Be!. DOI: 10.48550/arXiv.2511.18330. URL: https://arxiv.org/abs/2511.18330.

Commentary.

The natural offset k-d+1 and each side length are coerced to the reals. The exponent is the real inverse of the coerced offset, rpow is real exponentiation, and natCeil is the natural ceiling.

Definition 1.9 (Universal budget assertion).

$$(claim)\iff (\forall d\in \mathrm{Nat},\forall k\in \mathrm{Nat},\forall N\in \mathrm{Fin}\left(d\right)\to \mathrm{Nat},(1\le d)\Rightarrow ((d\le k)\Rightarrow ((\forall i\in \mathrm{Fin}\left(d\right),0<N\left(i\right))\Rightarrow (\exists s\in \mathrm{EggStrategy}\left(N,k,\mathrm{paperBound}\left(d,k,N\right)\right),\mathrm{Correct}\left(s\right)))))$$

Formalization. D5/S3/Observer/Budget/CaoChenMillerEggDropRefutation.claim (✓ std3).

Source. Repository-derived.

Acknowledgement. Xiangwen Cao and Zongyun Chen and Steven J. Miller (2025). Egg Drop Problems: They Are All They Are Cracked Up To Be!. DOI: 10.48550/arXiv.2511.18330. URL: https://arxiv.org/abs/2511.18330.

Commentary.

For every positive dimension, sufficient egg count, and positive side function, claim asks for some correct strategy within paperBound. This existence statement is weaker than success of a particular named strategy.

Theorem 1.10 (The universal assertion is false).

$$\neg claim$$

Proof. Machine-checked in Lean as D5/S3/Observer/Budget/CaoChenMillerEggDropRefutation.result (✓ std3). ∎

Resolves. Problems/cao-chen-miller-egg-drop-conjecture-one (refuted) by D5/S3/Observer/Budget/CaoChenMillerEggDropRefutation.result.

Source. Repository-derived.

Acknowledgement. Xiangwen Cao and Zongyun Chen and Steven J. Miller (2025). Egg Drop Problems: They Are All They Are Cracked Up To Be!. DOI: 10.48550/arXiv.2511.18330. URL: https://arxiv.org/abs/2511.18330.

Commentary.

At d=4, k=5, and constant side length five, paperBound is nine. Correctness makes paddedTranscript injective, but the hidden-point space has 625 elements and the nine-bit transcript space has 512.

References

• Truth anchor: D5/S3/Observer/Budget/CaoChenMillerEggDropRefutation.Correct
• Truth anchor: D5/S3/Observer/Budget/CaoChenMillerEggDropRefutation.EggStrategy
• Truth anchor: D5/S3/Observer/Budget/CaoChenMillerEggDropRefutation.Point
• Truth anchor: D5/S3/Observer/Budget/CaoChenMillerEggDropRefutation.Query
• Truth anchor: D5/S3/Observer/Budget/CaoChenMillerEggDropRefutation.claim
• Truth anchor: D5/S3/Observer/Budget/CaoChenMillerEggDropRefutation.dropOutcome
• Truth anchor: D5/S3/Observer/Budget/CaoChenMillerEggDropRefutation.paddedTranscript
• Truth anchor: D5/S3/Observer/Budget/CaoChenMillerEggDropRefutation.paperBound
• Truth anchor: D5/S3/Observer/Budget/CaoChenMillerEggDropRefutation.prediction
• Truth anchor: D5/S3/Observer/Budget/CaoChenMillerEggDropRefutation.result