Coordinate-Deletion Frequency Transport

Abstract

Transport finite-family coordinate frequencies and union closure through coordinate deletion.

Theorem 1.1 (Quantitative and half-frequency transport).

$$\begin{array}{r}\forall \alpha :Type,[\mathrm{DecidableEq}\left(\alpha \right)],\\ F\in \mathrm{Finset}\left(\mathrm{Finset}\left(\alpha \right)\right),D\in \mathrm{Finset}\left(\alpha \right),j\in \alpha ,r\in \mathbb{N},\\ (|D|=r)\wedge \neg (j\in D)\Rightarrow \\ \text{where}G=\mathrm{image}\left(A\mapsto (A\setminus D),F\right),N=|F|,M=|G|,\\ x=|\{A\mid A\in F\wedge j\in A\}|,b=|\{B\mid B\in G\wedge j\in B\}|,\\ ((b+2^r\cdot (M-b))\cdot x\ge b\cdot N)\wedge (2\cdot b\ge M\Rightarrow (2^r+1)\cdot x\ge N).\end{array}$$

Proof. Machine-checked in Lean as D5/S1/Phase/CoordinateDeletionFrequencyTransport.quantitative_and_half_frequency_transport (✓ std3). ∎

Source. Repository-derived.

Commentary.

Let G be the image of F after deleting D, and let N, M, x, and b be the displayed family and coordinate-frequency counts. The first inequality holds without assuming that F is union-closed.

The proof injects each non-j deletion fibre into the powerset of D by sending A to its deleted trace A intersect D. Reconstruction from A minus D and A intersect D gives the fibre bound, while deletion outside j also gives b at most x.

If j occurs in at least half of G, the same two live counting bounds give the stated (2^r+1) frequency bound in F. This is a transport theorem and does not resolve the Frankl union-closed sets conjecture.

Theorem 1.2 (Coordinate deletion preserves union closure).

$$\begin{array}{r}\forall \alpha :Type,[\mathrm{DecidableEq}\left(\alpha \right)],\\ F\in \mathrm{Finset}\left(\mathrm{Finset}\left(\alpha \right)\right),D\in \mathrm{Finset}\left(\alpha \right),\\ (\forall A\in F,\forall B\in F,\mathrm{union}\left(A,B\right)\in F)\Rightarrow \\ \forall A\in \mathrm{image}\left(S\mapsto (S\setminus D),F\right),\forall B\in \mathrm{image}\left(S\mapsto (S\setminus D),F\right),\mathrm{union}\left(A,B\right)\in \mathrm{image}\left(S\mapsto (S\setminus D),F\right).\end{array}$$

Proof. Machine-checked in Lean as D5/S1/Phase/CoordinateDeletionFrequencyTransport.union_closed_after_deletion (✓ std3). ∎

Source. Repository-derived.

Commentary.

For two members represented as A0 minus D and B0 minus D, their union is the deletion image of A0 union B0. This is the bind-only companion for the Frankl coordinate-deletion induction interface.

References

• Truth anchor: D5/S1/Phase/CoordinateDeletionFrequencyTransport.quantitative_and_half_frequency_transport
• Truth anchor: D5/S1/Phase/CoordinateDeletionFrequencyTransport.union_closed_after_deletion