Kernel-checked bounded C3 certificate

The Boolean certificates cover 27 ≤ m ≤ 6560 over the five ranges on which the ternary length is constant. Within each range, modular residues are advanced by multiplication by four, so only the first power is computed from scratch. Residue tests stop scanning ternary digits as soon as two twos have been found. Their soundness is transported through proved modular exponentiation and ternary prefix lemmas, yielding the headline carry theorem at the end of this file.

@[irreducible]

def GKPCarry.hasAtLeastTernaryTwos (required n : ℕ) : Bool

Test whether the ternary expansion contains at least required twos, stopping as soon as enough have been found.

Equations

• One or more equations did not get rendered due to their size.
• GKPCarry.hasAtLeastTernaryTwos 0 x✝ = true

theorem GKPCarry.hasAtLeastTernaryTwos_eq_true (required n : ℕ) : hasAtLeastTernaryTwos required n = true ↔ required ≤ List.count 2 (Nat.digits 3 n)

The digit scanner is equivalent to counting twos in the canonical ternary expansion.

theorem GKPCarry.four_pow_has_two_ternary_twos_in_finite_range {m : ℕ} (hlower : 27 ≤ m) (hupper : m ≤ 6560) : hasTwoTernaryTwosBelow (6 * ternaryLength m) (4 ^ m)

For every m in the closed interval from 27 through 6560, the first 6 * ternaryLength m little-endian ternary digits of 4 ^ m contain at least two digits equal to 2.

theorem GKPCarry.four_pow_has_two_ternary_twos_of_length_le_eight {m : ℕ} (hlower : 27 ≤ m) (hlength : ternaryLength m ≤ 8) : hasTwoTernaryTwosBelow (6 * ternaryLength m) (4 ^ m)

Equivalent length-indexed form of the bounded ternary-prefix theorem.

theorem GKPCarry.four_pow_prefix_carry_count_ge_two_in_finite_range {m : ℕ} (hlower : 27 ≤ m) (hupper : m ≤ 6560) : 2 ≤ prefixTernaryDoubleCarryCount (6 * ternaryLength m) (4 ^ m)

Bounded C3 carry result: throughout 27 ≤ m ≤ 6560, doubling the selected prefix of the ternary expansion of 4 ^ m produces at least two outgoing carries.