The factorial-denominator series

What is checked in Lean

• The exact integral normal form: the series is irrational if and only if the strict factorial successor Z_m misses divisibility by m cofinally.
• The equivalent carry form: rationality is equivalent to eventual unit carry, so cofinally many non-unit carries imply irrationality.
• Canonical factorial digits, exact remainder recurrences, zero-tail propagation, and the divisor-factorial centre recurrence.
• Integral channel congruences, the lcm tax, the prime unit translator, and factorial-grid Cramer residual identities.
• Weighted projection and factor-split rigidity consumers with their exact modular and Archimedean hypotheses.
• The zero-plateau and first-exit carry dichotomy, prime-power prefix obstructions, and exact doubled-prime branch characterisations.
• A Lean-checked implication from one exact non-unit carry to a rational-denominator lower bound; an independently regenerated exact GMP certificate at m = 300000 supplies the finite input.

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 of the factorial-denominator series.
• A theorem producing cofinally many divisibility misses or non-unit carries.
• Cofinal strict nonintegrality of the factorial-grid Cramer residual.
• The weighted collision-product and complementary-residue estimates needed by the factor-split projection consumer.
• The GMP computation is an exact finite external certificate, not a Lean evaluation and not an unbounded argument.

Open obligations

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

• weighted_collision_and_complementary_residue On an unbounded family of tailored prime blocks, prove both the weighted collision-core product bound and the independent complementary-residue inequality consumed by the exact unit-factor scale split.
• cofinal_prime_power_amplification At infinitely many genuinely nonterminal indices, prove quantitative repeated-support valuation amplification strong enough to meet the checked endpoint inequality.
• cofinal_lower_endpoint_escape For infinitely many primes, force the reduced predecessor gap outside the exact lower unit-carry cylinder.
• cofinal_doubled_prime_branch_failure For infinitely many odd primes, rule out both exact p^2-divisibility branches at index 2p by coupling the carry value to the predecessor residue.
• cramer_residual_nonintegrality Construct an unbounded factorial-grid family whose exact Cramer residual is nonintegral, using a determinant, valuation, cancellation, or gcd-of-minors certificate that controls the finite sign-changing block.

Finite search evidence

An exact GMP recurrence checks the carry sequence through m = 300000 and finds a non-unit carry at that index. The Lean consumer turns that one certificate into q >= 300000 for any hypothetical positive rational denominator; it does not prove a cofinal statement.

Lean modules

Comparator review

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

The paper