A proof of Geneson's continuous gluing conjecture

Geneson introduced continuous Turán numbers: for a set $R\subseteq\mathbb R^2$ and $n>0$, $\operatorname{opx}(n,R)$ is the supremum of the areas of open subsets of the square $[0,n]^2$ that contain no copy of $R$, where a copy may move the horizontal coordinates of $R$ apart and its vertical coordinates apart, keeping their order, but never closer together. We prove Conjecture 6.3 of Geneson's Continuous Turán numbers: if $P$ and $Q$ share a point $(c,d)$, with $P$ weakly south-west of it and $Q$ weakly north-east of it, then $\operatorname{opx}(n,P\cup Q)\le\operatorname{opx}(n,P)+\operatorname{opx}(n,Q)$ for every $n>0$. The sets $P$ and $Q$ are arbitrary: no finiteness, boundedness or measurability is assumed. Keszegh proved the corresponding inequality for forbidden zero–one matrices joined at opposite corner entries, by partitioning a host matrix according to the possible gluing corners. We carry this partition over to the continuous setting. What we add is compactness of the space of copies in a compact host, which makes the partition measurable, and the inner regularity of Lebesgue measure, which passes from measurable pieces to open sets. The theorem and its proof are formalized in Lean. This work has not yet been reviewed by experts. The proofs, the Lean formalization and the text were produced by AI models (from OpenAI and Anthropic), working under the author's direction. Computer-assisted; not yet reviewed by experts. Produced by AI models under the author's direction.