Kernel-checked bounded C3 certificate

The Boolean certificates cover 27 ≤ m ≤ 6560 in 64-value chunks. Their soundness is transported through proved modular exponentiation and ternary prefix lemmas, yielding the headline carry theorem at the end of this file.

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.