#243 Reciprocal-tail rigidity near the Sylvester recurrence

What is checked in Lean

The exact product-cleared tail dynamics and the defect identity, as identities in the integer state variables.
That a vanishing centred state is absorbing under strict centring, so the state is either eventually zero or nowhere zero.
That eventual vanishing of the centred state, with the next tail state nonvanishing, forces the Sylvester recurrence eventually.
That a nonnegative centred state vanishes eventually, by descent.
That the centred state cannot be eventually constant and negative, at any magnitude and any common scale.
That the negative magnitude cannot be eventually periodic with positive drift, in the regime where each magnitude is below its multiplier.
A coprimality barrier: a sequence tending to infinity with uniformly bounded upward increments cannot permanently avoid infinitely many fresh pairwise coprime moduli.
That a reduced exact tail has pairwise coprime multipliers which its numerator permanently avoids, so no such tail has a divergent numerator with bounded rise.
That the tail gcd stabilises under cofinally bounded negative magnitudes.
Conditionally: exact dynamics, eventual strict centring, an eventually bounded negative part, and normalised vanishing together force the centred state to vanish eventually.
That survival through a fixed number of forced updates depends only on the initial state modulo a factorial of the horizon.

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

conditional reduction and no-go result family: bounded_negative_exclusion

Normalised vanishing and bounded rise exclude a cofinally bounded negative part.

All dynamics, bounded-rise, positivity, and vanishing hypotheses remain explicit.

ErdosProblems.Erdos243.no_cofinallyBoundedNegative_of_normalizedVanishes

no-go result family: negative_orbit_no_go

An eventually periodic negative-error orbit with positive phase growth is impossible.

The theorem does not cover arbitrary unbounded negative behaviour.

ErdosProblems.Erdos243.no_eventuallyPeriodicNegative_orbit

What is not checked

The unrestricted problem.
That eventual strict centring and normalised vanishing follow from the growth hypothesis and rationality. Both are assumed by the final theorem and neither is derived, so that theorem constrains the state system rather than the original sequence.
Any exclusion of negative excursions whose magnitudes are unbounded along a cofinal set.
The criterion of Erdos and Straus and Duverney's conditional characterisation, which are cited rather than formalised and are both stronger than anything checked here.

Open obligations

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

unbounded_negative_excursions Exclude, or construct, an exact orbit whose centred state is negative infinitely often with magnitudes unbounded along that cofinal set. Every checked exclusion consumes some finiteness: a fixed set of prime divisors, a fixed period, or a fixed bound on the negative part.
derive_the_two_analytic_hypotheses Derive eventual strict centring and normalised vanishing from the growth hypothesis and rationality, or show that they do not follow.
formalise_the_published_criteria Kernel-check the Erdos-Straus weighted criterion and Duverney's conditional characterisation under explicit analytic hypotheses.

Finite search evidence

An exact search over initial states below five thousand produced forced prefixes of length seventeen and no longer. It is superseded: the constant-negative template is now excluded outright, for every seed and at every scale.

Lean modules

Module	Lines	Declarations	Theorems
`ErdosProblems.Erdos243.ReciprocalTailRigidity`	2386	77	67
`ErdosProblems.Erdos243.FiniteHorizonResidue`	141	10	7
`ErdosProblems.Erdos243.SparseResetRecovery`	208	6	5
`ErdosProblems.Erdos243.DynamicCancellation`	399	15	15
`ErdosProblems.Erdos243.FeedbackRealizability`	165	7	7
`ErdosProblems.Erdos243.GlobalLcmHeight`	152	13	9
`ErdosProblems.Erdos243.LcmCriticalBoundary`	388	15	14
`ErdosProblems.Erdos243.PrimitivePrefixRigidity`	136	6	4
`ErdosProblems.Erdos243.WeightedCRTRepair`	333	17	11

Comparator review

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

Replayed by the Comparator

Statement and type parity replayed against the pinned toolchain.

Constant, eventually constant, periodic, and eventually periodic negative-error orbits are excluded in their stated regimes.

The exclusions do not cover arbitrary unbounded negative behaviour.

negative_orbit_no_go · targeted_representative_periodic_theorem
Normalised vanishing excludes a cofinally bounded negative part and forces eventual Sylvester behaviour.

Every positivity, dynamics, bounded-rise, and vanishing hypothesis remains explicit.

bounded_negative_exclusion · targeted

Represented indirectly

Covered through a neighbouring selected interface, not replayed one-to-one.

Exact update and defect identities, scale equivariance, zero absorption, and eventual recovery of the Sylvester recurrence.

The recovery theorem requires eventual centred-state vanishing.

centered_state_dynamics · represented_by_selected_boundary_theorems
A bounded-rise sequence cannot remain coprime to fresh pairwise-coprime moduli; reduced tails inherit this obstruction.

The required bounded-rise input is not automatic for the original sequence.

bounded_rise_coprimality · represented_by_stronger_selected_boundary_theorem

Outside the Comparator selection

Stated in the corpus; not part of the replayed interface set.

Finite normalised negative mass forces eventual zero and hence the Sylvester recurrence.

Summability of the negative mass is unproved for the original problem.

negative_mass_recovery · not_selected_deep_state_vocabulary

The paper

Problem note 22 pp

Excluding the Bounded Negative Part

Clearing denominators turns Erdős #243 into rigidity of a centred integer error orbit. Lean excludes eventually negative constant magnitude and positive-drift periodic magnitude, and proves that normalised vanishing plus an eventually bounded negative part forces the error to vanish and the Sylvester recurrence to begin. Eventual strict centring is redundant, while Koizumi supplies normalised vanishing for the canonical orbit. Two of the implications proved here, absorption and descent, are identified with prior lemmas of Koizumi's in canonical coordinates, and no priority is claimed over them. The missing hypothesis is the negative-part bound: any survivor has cofinally unbounded negative excursions and divergent normalised negative mass.

Read it here PDF TeX source