Lambert-type series at rational bases

What is checked in Lean

• That a literal coordinatewise transfer of the integer-base clearing argument forces a power-versus-linear inequality, and that this inequality is impossible at base three halves.
• The exact denominator-cleared rational-base tail recurrence, including its forcing term.
• That for every noninteger base with denominator at least two the forcing magnitude grows at least exponentially, while at denominator one it collapses to a bounded expression.
• The complete elementary Archimedean height inequality used by the published Bundschuh-Väänänen criterion at base seven halves; the analytic irrationality theorem itself remains external.
• Polynomial bounds on the doubled denominator exponents in the homogenised Padé construction, together with an exact gap identity.
• The exact exterior-determinant elimination identity, and that rowwise contents scale the Padé errors, exterior determinant, and absolute determinant height by the same factors.
• The exact Heine-Zudilin cone endpoint exponent arithmetic used to identify the bottom and top coefficient endpoints.
• That homogeneous evaluation at (3,2) sees only the constant endpoint modulo three and the top endpoint modulo two, so unit endpoints obstruct common local factors.
• That under unit top and constant endpoint hypotheses, a common multiplier of the two specialised coefficient channels is divisible by neither two nor three; the missing local gain must therefore survive primitive normalisation.
• That vanishing of the higher bottom and top endpoint jets is exactly divisibility by the corresponding powers of three and two.
• That the source integer-base ratio inequality implies a strictly negative scalar product-formula margin at three halves.
• That the four-jet target has exact cardinality (3^R)^2(2^S)^2 and, for positive R, any family with n at least 4R+2S forces two distinct binary selectors to collide; their {-1,0,1} difference cancels all four endpoint jets.
• That the rectangular Hermite-Pade threshold never improves on the classical one in the checked exponent model, with equality characterised exactly.
• The exact 81/200 height region: 31/4 and every positive power lie inside it and outside the earlier Bundschuh-Vaananen region, while 3/2 lies outside both.
• At n = 0, the Amdeberhan-Zeilberger q-Apery operator applied to Van Assche's moving diagonal has residual -p(p-1)^2(p+1)(p^5+2p^4+2p^3+2p^2+2), which is strictly negative and nonzero for every real p > 1.

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 at base three halves, or for any rational base.
• The published analytic height theorem, which is cited and used as an external result and is not formalised here.
• The all-scale Heine-Zudilin coefficient construction at rational base three halves; the primary source assumes an integer base.
• The source analytic irrationality theorem inside the 81/200 height region; only its elementary parameter specialisations are formalised.
• A sufficiently large primitive-normalised, non-collapsed coefficient family meeting the checked n >= 4R+2S threshold at the required quadratic depths.
• That one of the resulting bounded-coefficient collision vectors has a nonzero polynomial pair, lies outside the analytic remainder nullspace, and has sufficient local gain.
• Positivity or decay of the elementary Padé remainder; only its exponent arithmetic is checked.
• Any general recurrence, endpoint, lattice, valuation, denominator, or irrationality conclusion from the n = 0 q-Apery residual; it proves only that the named scalar recurrence does not transfer to Van Assche's diagonal.

Open obligations

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

• three_halves_growing_rank_endpoint_jet_kernel After dividing every coefficient pair by its rowwise common content, at positive quadratic target depths R_n,S_n exhibit at least 4R_n+2S_n primitive coefficient pairs from a genuinely non-collapsed deformation, prove that the required two-adic and three-adic gain survives primitive normalisation, and prove that at least one resulting checked {-1,0,1} collision has a nonzero polynomial pair and lies outside the analytic remainder nullspace; or prove an exact rank obstruction.

Lean modules

Comparator review

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

The paper