A density-one theorem for the GKP power-of-two condition

The exact modular sieve bounds possible failures in every initial interval. At ternary depth n + 3, each block of 2 * 3 ^ (n + 2) exponents contains at most (n + 9) * 2 ^ n failures. These bounds prove that the proportion of exponents k for which 9 does not divide centralBinom (2 ^ k) tends to zero. Thus the GKP divisibility conclusion holds for a set of exponents of natural density one.

The universal conjecture remains open because a density-zero failure set need not be empty.

@[reducible, inline]

abbrev GKPCarry.GKPFailureExponentsBelow (bound : ℕ) : Type

Possible GKP failures among exponents below bound.

Equations

• GKPCarry.GKPFailureExponentsBelow bound = { exponent : Fin bound // ¬9 ∣ (2 ^ ↑exponent).centralBinom }

@[reducible, inline]

abbrev GKPCarry.GKPSuccessExponentsBelow (bound : ℕ) : Type

Exponents below bound that satisfy the GKP divisibility condition.

Equations

• GKPCarry.GKPSuccessExponentsBelow bound = { exponent : Fin bound // 9 ∣ (2 ^ ↑exponent).centralBinom }

theorem GKPCarry.card_gkpFailureExponentsBelow_le (depth bound : ℕ) : Fintype.card (GKPFailureExponentsBelow bound) ≤ (bound / (2 * 3 ^ (depth + 2)) + 1) * ((depth + 9) * 2 ^ depth)

Quantitative sieve bound in every initial interval.

noncomputable def GKPCarry.gkpFailureProportion (bound : ℕ) : ℝ

Proportion of possible GKP failures among exponents below bound.

Equations

• GKPCarry.gkpFailureProportion bound = ↑(Fintype.card (GKPCarry.GKPFailureExponentsBelow bound)) / ↑bound

theorem GKPCarry.gkpFailureProportion_le (depth bound : ℕ) (hbound : 0 < bound) : gkpFailureProportion bound ≤ uncertifiedClassProportion depth + ↑((depth + 9) * 2 ^ depth) / ↑bound

At any fixed sieve depth, the failure proportion is bounded by the residual periodic proportion plus one incomplete block.

theorem GKPCarry.tendsto_gkpFailureProportion_zero : Filter.Tendsto gkpFailureProportion Filter.atTop (nhds 0)

Density-zero failure theorem. The proportion of exponents below bound that fail the GKP divisibility condition tends to zero.

noncomputable def GKPCarry.gkpSuccessProportion (bound : ℕ) : ℝ

Proportion of exponents below bound satisfying the divisibility condition.

Equations

• GKPCarry.gkpSuccessProportion bound = ↑(Fintype.card (GKPCarry.GKPSuccessExponentsBelow bound)) / ↑bound

theorem GKPCarry.gkpSuccessProportion_eq_one_sub_failure (bound : ℕ) (hbound : 0 < bound) : gkpSuccessProportion bound = 1 - gkpFailureProportion bound

theorem GKPCarry.tendsto_gkpSuccessProportion_one : Filter.Tendsto gkpSuccessProportion Filter.atTop (nhds 1)

Density-one GKP theorem. Powers of two satisfy the divisibility branch of the GKP conjecture for a set of exponents of natural density one.