An exact all-depth modular sieve for GKP carries

For every ternary prefix depth n + 3, powers of two have exact period 2 * 3 ^ (n + 2). In one period, precisely (n + 9) * 2 ^ n exponent classes have fewer than two visible doubling carries. Every other class is an infinite congruence class on which the central binomial coefficient is divisible by nine.

This is an exact infinite family of certified cases. The uncertified classes at each finite depth may acquire carries later; this theorem neither decides them nor proves the universal GKP conjecture.

noncomputable def GKPCarry.twoPowerTernaryUnitWordEquiv (length : ℕ) : Fin (2 * 3 ^ length) ≃ TernaryUnitWords length

One exponent period is equivalent to all fixed-length ternary unit words.

Equations

• GKPCarry.twoPowerTernaryUnitWordEquiv length = (GKPCarry.twoPowerUnitEquiv length).trans (GKPCarry.ternaryUnitWordEquiv length).symm

theorem GKPCarry.ternaryWordValue_twoPowerTernaryUnitWordEquiv_apply (length : ℕ) (exponent : Fin (2 * 3 ^ length)) : ternaryWordValue ↑((twoPowerTernaryUnitWordEquiv length) exponent) = 2 ^ ↑exponent % 3 ^ (length + 1)

The word corresponding to an exponent is the fixed-length ternary expansion of its power-of-two residue.

@[reducible, inline]

abbrev GKPCarry.UncertifiedExponentClasses (n : ℕ) : Type

Exponent classes not yet certified after reading n + 3 ternary digits. They are not counterexamples: later digits may supply the missing carries.

Equations

• GKPCarry.UncertifiedExponentClasses n = { exponent : Fin (2 * 3 ^ (n + 2)) // GKPCarry.ternaryDoubleCarryCount (Nat.digits 3 (2 ^ ↑exponent % 3 ^ (n + 3))) < 2 }

@[reducible, inline]

abbrev GKPCarry.CertifiedExponentClasses (n : ℕ) : Type

Exponent classes certified after reading n + 3 ternary digits.

Equations

• GKPCarry.CertifiedExponentClasses n = { exponent : Fin (2 * 3 ^ (n + 2)) // 2 ≤ GKPCarry.ternaryDoubleCarryCount (Nat.digits 3 (2 ^ ↑exponent % 3 ^ (n + 3))) }

noncomputable def GKPCarry.uncertifiedExponentClassesEquivUnitBadCarryWords (n : ℕ) : UncertifiedExponentClasses n ≃ UnitBadCarryWords (n + 2)

The uncertified exponent classes are exactly the deficient unit words counted by the carry automaton.

Equations

• GKPCarry.uncertifiedExponentClassesEquivUnitBadCarryWords n = (GKPCarry.twoPowerTernaryUnitWordEquiv (n + 2)).subtypeEquiv ⋯

theorem GKPCarry.card_uncertifiedExponentClasses (n : ℕ) : Fintype.card (UncertifiedExponentClasses n) = (n + 9) * 2 ^ n

Exact residual count: after n + 3 digits, precisely (n + 9) * 2 ^ n exponent classes remain uncertified.

theorem GKPCarry.card_certifiedExponentClasses (n : ℕ) : Fintype.card (CertifiedExponentClasses n) = 2 * 3 ^ (n + 2) - (n + 9) * 2 ^ n

The complementary certified set has the corresponding exact size.

Asymptotic strength of the sieve

noncomputable def GKPCarry.uncertifiedClassProportion (n : ℕ) : ℝ

The proportion of exponent classes left uncertified at depth n + 3, written in a form that exposes its geometric decay.

Equations

• GKPCarry.uncertifiedClassProportion n = (↑n + 9) / 18 * (2 / 3) ^ n

theorem GKPCarry.uncertifiedClassProportion_eq_card_ratio (n : ℕ) : uncertifiedClassProportion n = ↑(Fintype.card (UncertifiedExponentClasses n)) / ↑(Fintype.card (Fin (2 * 3 ^ (n + 2))))

The analytic proportion is exactly the ratio of the residual class count to the full exponent period.

theorem GKPCarry.tendsto_uncertifiedClassProportion : Filter.Tendsto uncertifiedClassProportion Filter.atTop (nhds 0)

The proportion of exponent classes left unresolved by the finite-prefix sieve tends to zero as the prefix depth increases.

noncomputable def GKPCarry.certifiedClassProportion (n : ℕ) : ℝ

The complementary proportion of exponent classes certified by the sieve tends to one.

Equations

• GKPCarry.certifiedClassProportion n = 1 - GKPCarry.uncertifiedClassProportion n

theorem GKPCarry.tendsto_certifiedClassProportion : Filter.Tendsto certifiedClassProportion Filter.atTop (nhds 1)

theorem GKPCarry.nine_dvd_centralBinom_two_pow_of_reduced_carry_certificate (n k : ℕ) (hcarry : 2 ≤ ternaryDoubleCarryCount (Nat.digits 3 (2 ^ (k % (2 * 3 ^ (n + 2))) % 3 ^ (n + 3)))) : 9 ∣ (2 ^ k).centralBinom

A certificate for the reduced exponent class propagates to every exponent in that congruence class and proves divisibility by nine.

theorem GKPCarry.nine_dvd_centralBinom_two_pow_of_certified_class (n k : ℕ) (exponentClass : CertifiedExponentClasses n) (hk : k % (2 * 3 ^ (n + 2)) = ↑↑exponentClass) : 9 ∣ (2 ^ k).centralBinom

Every certified class denotes an infinite congruence class of GKP inputs whose central binomial coefficients are divisible by nine.

theorem GKPCarry.badCarryLanguage_two_pow_eq_false_of_certified_class (n k : ℕ) (exponentClass : CertifiedExponentClasses n) (hk : k % (2 * 3 ^ (n + 2)) = ↑↑exponentClass) : badCarryLanguage (Nat.digits 3 (2 ^ k)) = false

The same certified classes avoid the deficient-carry language appearing in the exact GKP characterization.

theorem GKPCarry.gkp_exact_modular_sieve (n : ℕ) : Fintype.card (CertifiedExponentClasses n) = 2 * 3 ^ (n + 2) - (n + 9) * 2 ^ n ∧ ∀ (exponentClass : CertifiedExponentClasses n) (k : ℕ), k % (2 * 3 ^ (n + 2)) = ↑↑exponentClass → 9 ∣ (2 ^ k).centralBinom ∧ badCarryLanguage (Nat.digits 3 (2 ^ k)) = false

Exact all-depth modular GKP sieve. At every depth, the theorem gives the exact number of certified exponent classes and proves the GKP divisibility conclusion on every exponent in each such class.