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. 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.