Three-prime running least common multiples

What is checked in Lean

• That for three pairwise distinct primes the least common multiple of the smooth prefix equals the product of the three maximal pure prime powers below the cutoff.
• That equal logarithmic coordinates give an equal prefix least common multiple, so the running value is constant on logarithmic cells.
• That advancing exactly one logarithmic coordinate multiplies the running value by the corresponding prime.
• That the positive power channels of distinct primes are disjoint, so the first powers in three channels give an exact jump count.
• That a finite smooth lattice sum groups exactly by running height, with the height fibre cardinality as coefficient.
• A quadratic bound on the cardinality of the actual filtered exponent shell.
• That each dyadic block contains at most one internal pure power from each non-dyadic channel, so the compressed {2,3,5} block radix belongs to the exact alphabet {2,6,10,30} and in particular lies between 2 and 30.
• That the smallest {2,3,5} kernel rectangle has determinant exactly -1/15, so its two-by-two matrix has rank two over the rationals and no rank-one separation exists.
• The canonical least-positive-residue interval and congruence facts, including the zero-residue representative.
• The exact local-window identity for an integral carry.
• A denominator-dependent CofinalLocalWindowEscape proposition and the full theorem that it rules out every positive reduced integral carry satisfying the matching bound.
• A bounded-radix dichotomy: under a bounded positive digit alphabet, a nonzero scaled tail must be separated from the integers cofinally.
• Exact three-channel block-nullity as a coboundary condition, and extinction of a bounded carry lift under two independent anchors.
• The exact residue-digit plus coboundary form of an integral carry, together with a function-faithful observer criterion and a finite realised-span consequence.

Main results

Statements and boundaries are copied from the corpus record. Registry status: not_registered; the claim registry does not carry these declarations and kernel checking them does not promote them into reviewed public claims

What is not checked

• Irrationality or transcendence in any three-prime case.
• The derivation of the actual bounded positive carry, including the divisibility required to cancel the absorbed smooth denominator factor, from a hypothetical rational value of the original series.
• CofinalLocalWindowEscape for those actual words; it is an explicit hypothesis of the checked consumer, not a theorem.
• A proof that the actual three-channel word satisfies the block-null, anchor, or factorisation hypotheses of the migrated abstract consumers.
• The infinite limit of the jump expansion; only its finite core is checked.
• Any unbounded denominator exclusion. The finite certificates exclude denominators below an explicit bound and no further.

Open obligations

Prove any one of these and the corresponding reduction above becomes unconditional.

• actual_local_window_residue_escape For every positive B coprime to 30 and every starting index, produce a later actual {2,3,5} window whose least positive forcing residue exceeds the exact denominator-dependent carry bound.
• actual_rational_carry_instantiation Identify the formal radix word with the checked four-symbol dyadic block base, formalize the exact block digit and its link to the original summand multiplicities, and derive the positive reduced carry recurrence and its bound from a hypothetical rational value.
• nonstationary_analytic_theorem Prove a genuinely higher-dimensional analytic theorem for the phase cocycle or the associated contraction.
• unbounded_height_certificate Replace one finite denominator exclusion by a family whose exclusion bound tends to infinity.

Finite search evidence

The integer-only dyadic-window checker reproduces three exact packet certificates and, for all 106,666 pairs with denominator B <= 1000 coprime to 30 and dyadic start 100 <= a <= 500, finds an escaping window of length at most 18; the largest first successful length is 14. This is finite proof-consumer evidence only and proves neither unbounded-denominator nor cofinal escape.

Lean modules

Comparator review

The Comparator replays selected exact interfaces against a pinned toolchain. It never widens what Lean proved.

The paper