External verification

ErdosProblems.Erdos68.irrational_factorialGapSeries_iff_cofinal_strictFacTopRat_misses

Exact registry keys and Comparator routing are listed separately.

• Factorial carry characterisation
  Exact equivalence between irrationality, cofinally many non-unit carries, and cofinal strict-successor divisibility failures.
  Boundary. An exact reformulation does not supply the required cofinal failures.
  Evidence. locally proved result; novelty unassessed · Lean kernel plus Comparator

• Factorial channel and projection rigidity
  Finite channel congruences, a two-term prime-channel corrector, and endpoint-weighted projection rigidity.
  Boundary. These finite and structural results do not produce a cofinal obstruction.
  Evidence. locally proved result; novelty unassessed · Lean kernel

• Factorial conditional producers
  Cofinal zero-branch or large private-factor hypotheses imply the required irrationality conclusion.
  Boundary. The producer hypotheses are unproved.
  Evidence. conditional reduction · Lean kernel

• Factorial finite certificates
  Lean checks small exact misses; a hash-bound GMP scan reaches index 300000 and yields the corresponding finite denominator exclusion.
  Boundary. Finite computation does not change the cofinal quantifier.
  Evidence. finite computation · Lean finite theorem plus external exact certificate

• Factorial lcm growth
  A paper deduction gives a lower bound for the lcm of factorial-gap denominators using an external multiplicity theorem.
  Boundary. Comparator cannot certify the cited input or authored deduction.
  Evidence. paper plus external theorem · paper argument plus cited theorem

• factorial_carry_characterisation
  Comparator: targeted

• factorial_channel_and_projection_rigidity
  Comparator: represented_by_isolated_headline

• factorial_conditional_producers
  Comparator: not_selected_deep_project_predicate_stack

• factorial_finite_certificates
  Comparator: not_applicable_to_external_execution

• factorial_lcm_growth
  Comparator: not_applicable_not_a_lean_declaration

ErdosProblems.Erdos243.nextTailState_eq_sub_centered

Exact registry keys and Comparator routing are listed separately.

• Centered state dynamics
  Exact update and defect identities, scale equivariance, zero absorption, and eventual recovery of the Sylvester recurrence.
  Boundary. The recovery theorem requires eventual centred-state vanishing.
  Evidence. locally proved result; novelty unassessed · Lean kernel

• Negative orbit no go
  Constant, eventually constant, periodic, and eventually periodic negative-error orbits are excluded in their stated regimes.
  Boundary. The exclusions do not cover arbitrary unbounded negative behaviour.
  Evidence. no-go result · Lean kernel plus Comparator

• Bounded rise coprimality
  A bounded-rise sequence cannot remain coprime to fresh pairwise-coprime moduli; reduced tails inherit this obstruction.
  Boundary. The required bounded-rise input is not automatic for the original sequence.
  Evidence. locally proved result; novelty unassessed · Lean kernel

• Bounded negative exclusion
  Normalised vanishing excludes a cofinally bounded negative part and forces eventual Sylvester behaviour.
  Boundary. Every positivity, dynamics, bounded-rise, and vanishing hypothesis remains explicit.
  Evidence. conditional reduction and no-go result · Lean kernel plus Comparator

• Negative mass recovery
  Finite normalised negative mass forces eventual zero and hence the Sylvester recurrence.
  Boundary. Summability of the negative mass is unproved for the original problem.
  Evidence. conditional reduction · Lean kernel

• centered_state_dynamics
  Comparator: represented_by_selected_boundary_theorems

• negative_orbit_no_go
  Comparator: targeted_representative_periodic_theorem

• bounded_rise_coprimality
  Comparator: represented_by_stronger_selected_boundary_theorem

• bounded_negative_exclusion
  Comparator: targeted

• negative_mass_recovery
  Comparator: not_selected_deep_state_vocabulary

ErdosProblems.Erdos249.irrational_totient_series_of_naturalPrimeTailOrbitStrictGap

Exact registry keys and Comparator routing are listed separately.

• Totient kernel basis
  An explicit odd-core basis and relation normal form for the full dyadic totient kernel.
  Boundary. The basis theorem does not connect rationality of the series to finite kernel rank.
  Evidence. locally proved result; novelty unassessed · Lean kernel plus Comparator

• Totient kernel rank
  An independent constructive proof of exact finite-level dyadic rank 2^e+1, together with a kernel-checked full-kernel infinite-dimensionality corollary already implied by Coons’s non-2-regularity theorem.
  Boundary. Only the finite-level rank is presented as an additional result; full-kernel infinite-dimensionality is prior-art context, and no rationality-to-finite-rank bridge is proved.
  Evidence. mixed local finite-level theorem and formalised prior consequence · Lean kernel plus Comparator

• Totient kernel all base index
  For every base k at least 2, Lean checks the arithmetic reduction, exact nonmultiple-residue coordinates, unconditional canonical spanning, and exact rank k^e+1 conditional on canonical-family linear independence.
  Boundary. Lean does not prove all-base affine-section independence or formalise Martin’s theorem. The unconditional basis and rank conclusions in the paper use that external input.
  Evidence. formalised unconditional spanning and conditional rank with external independence input · Lean kernel for arithmetic, finite indexing, spanning, and the conditional-rank theorem; paper argument plus Martin’s cited theorem for independence

• Totient finite denominator exclusion
  A Farey denominator exclusion through 7.96e34, sharp for its selected window, and diagonal certificates through t=82.
  Boundary. The selected finite window and certificate ceiling do not imply an unbounded producer.
  Evidence. finite computation · Lean kernel and generated finite certificates

• Totient carry rank
  Rationality forces a tempered integral tail orbit with unbounded finite-level carry rank.
  Boundary. This is a necessary consequence, not a contradiction.
  Evidence. conditional reduction · Lean kernel

• Totient lambert coefficients
  The totient series is rewritten as a Lambert series with explicit nonnegative, unbounded prime-power coefficients.
  Boundary. The coefficient identities do not prove irrationality.
  Evidence. locally proved result; novelty unassessed · Lean kernel

• Eventually periodic lambert
  Eventually periodic nonnegative rational weights give an irrational Lambert series.
  Boundary. The totient-derived weights are not eventually periodic.
  Evidence. Lean formalisation of existing result · Lean kernel

• Totient certificate equivalences
  Pointwise, cofinal, lcm-diagonal, and separated-window certificate supplies are exact or sufficient reformulations.
  Boundary. Equivalent producer statements are as hard as the unresolved target.
  Evidence. exact equivalence and conditional reduction · Lean kernel

• totient_kernel_basis
  Comparator: targeted

• totient_kernel_rank
  Comparator: targeted

• totient_kernel_all_base_index
  Comparator: not_selected_external_independence_boundary

• totient_finite_denominator_exclusion
  Comparator: not_selected_finite_family_has_separate_receipt

• totient_carry_rank
  Comparator: not_selected_deep_orbit_vocabulary

• totient_lambert_coefficients
  Comparator: represented_by_basis_and_rank_targets

• eventually_periodic_lambert
  Comparator: not_selected_prior_result

• totient_certificate_equivalences
  Comparator: not_selected_deep_certificate_vocabulary

ErdosProblems.Erdos251.dyadicPartialSumQ_eq_start_add_differences

Exact registry keys and Comparator routing are listed separately.

• Prime gap reformulation
  Exact finite summation by parts, the unconditional infinite prime-gap identity, and irrationality equivalence.
  Boundary. The equivalence does not prove irrationality of either series.
  Evidence. locally proved result; novelty unassessed · Lean kernel plus Comparator

• Integral shift classification
  Block identities and exact denominator criteria classify rationality through integral positive tail shifts.
  Boundary. The concrete prime-gap producer remains missing.
  Evidence. locally proved result; novelty unassessed · Lean kernel

• Totient shift propagation
  Odd rational denominators give totient-length integral shifts, and integrality propagates through the recurrence.
  Boundary. This describes rational states and supplies no contradiction for actual prime gaps.
  Evidence. locally proved result; novelty unassessed · Lean kernel

• Small mismatch criterion
  Cofinal adjacent small mismatches would rule out eventual integral shifts for the prime-gap tail.
  Boundary. The cofinal mismatch producer is unproved.
  Evidence. conditional reduction · Lean kernel

• Coefficient only no go
  Prime gaps are unbounded and non-eventually-periodic, while an explicit nonperiodic unbounded countermodel still has rational sum.
  Boundary. Comparator checks the exact theorem, not the broader methodological interpretation.
  Evidence. no-go result · Lean kernel plus authored synthesis

• prime_gap_reformulation
  Comparator: targeted

• integral_shift_classification
  Comparator: not_selected_abstract_family_represented_in_manifest

• totient_shift_propagation
  Comparator: represented_by_integral_shift_family

• small_mismatch_criterion
  Comparator: not_selected_open_producer_hypothesis

• coefficient_only_no_go
  Comparator: targeted_unboundedness_theorem_only

ErdosProblems.Erdos257.selectedMersenneTail_lt_weight

Exact registry keys and Comparator routing are listed separately.

• Finite period noncollapse
  The multiplicative order of the base modulo a reduced finite-sum denominator is the support lcm, forcing denominator growth.
  Boundary. A finite-support denominator theorem does not settle an infinite-support sum.
  Evidence. locally proved result; novelty unassessed · Lean kernel plus Comparator

• Rational support constraints
  Rational infinite supports force unbounded scaled tails, sublogarithmic zero windows, and reciprocal-mass constraints.
  Boundary. The constraints do not exclude every infinite support.
  Evidence. conditional reduction · Lean kernel

• Known irrational supports
  Full, factorial, power-of-two, multiple, pairwise-coprime, eventually periodic, residue-class, and odd supports are formalised.
  Boundary. Structured known families do not cover arbitrary infinite supports.
  Evidence. Lean formalisation of existing results · Lean kernel plus Comparator for full support

• Squarefree support
  Lean checks squarefree incidence and no-go statements; the irrationality conclusion uses an external analytic theorem in the paper.
  Boundary. Comparator must not badge the paper-plus-external conclusion.
  Evidence. Lean structure plus paper and external theorem · Lean kernel plus paper argument plus cited theorem

• Achievement set geometry
  Compactness, perfectness, total disconnectedness, nowhere density, and measure one for the unrestricted achievement set.
  Boundary. Geometry of the full set does not decide irrationality of every coded point.
  Evidence. mixed prior-art geometry and locally proved metric result; novelty unassessed · Lean kernel plus Comparator

• Restricted achievement sets
  Support-restricted coding is injective and the associated achievement set has exact finite-complement measure or zero for infinite complement.
  Boundary. The measure dichotomy does not classify rational points.
  Evidence. locally proved result; novelty unassessed · Lean kernel plus Comparator

• Half and twenty one frontiers
  Exact greedy characterisations and finite-support exclusions isolate the remaining 1/2 and 1/21 alternatives.
  Boundary. Neither membership question is decided.
  Evidence. conditional reduction and no-go result · Lean kernel

• finite_period_noncollapse
  Comparator: targeted

• rational_support_constraints
  Comparator: not_selected_deep_support_vocabulary

• known_irrational_supports
  Comparator: targeted_full_support_representative

• squarefree_support
  Comparator: not_applicable_to_external_irrationality_input

• achievement_set_geometry
  Comparator: targeted_measure_theorem

• restricted_achievement_sets
  Comparator: targeted_measure_dichotomy

• half_and_twenty_one_frontiers
  Comparator: not_selected_deep_greedy_state_vocabulary

Every two-prime case is settled at transcendence level by a paper argument in the problem note, with Loxton-van der Poorten 1977 (quoted in Bugeaud-Laurent form) as the external engine; the same argument was posted publicly by Steve Fan on the problem’s erdosproblems.com discussion page on 26 June 2026, before the note was finalised, so the note claims no priority. The argument is deliberately not formalised here and no Lean declaration asserts it.

ErdosProblems.Erdos269.smoothPrefixLcm_eq_threePrimeHeight

Exact registry keys and Comparator routing are listed separately.

• Three prime lcm cells
  Exact running-LCM product, logarithmic-cell constancy, coordinate jump ratios, and jump count.
  Boundary. Cell structure alone does not prove irrationality.
  Evidence. locally proved result; novelty unassessed · Lean kernel plus Comparator

• Two prime transcendence
  Both two-prime running-lcm series are proved transcendental by an authored deduction from an external theorem.
  Boundary. Comparator cannot certify the external analytic input.
  Evidence. paper plus external theorem · paper argument plus cited theorem

• Height fibre and shell
  Finite height-fibre normal form and a quadratic smooth-shell multiplicity bound.
  Boundary. The fibre bounds do not provide the missing divisibility bridge.
  Evidence. locally proved result; novelty unassessed · Lean kernel

• Rank two kernel no go
  The 2,3,5 kernel is not rank one and its smallest displayed minor equals -1/15.
  Boundary. Failure of rank one does not itself imply irrationality.
  Evidence. no-go result · Lean kernel plus Comparator

• Dyadic block alphabet
  The exact dyadic block alphabet is 2, 6, 10, and 30.
  Boundary. The finite alphabet does not supply the needed carry escape.
  Evidence. locally proved result; novelty unassessed · Lean kernel

• Conditional carry escape
  Cofinal local-window residue escape would rule out bounded positive carries after an unproved rationality-to-carry bridge.
  Boundary. The producer and actual-series identification are missing.
  Evidence. conditional reduction · Lean kernel

• Three prime finite search
  A local-window checker searches 106666 denominator and start pairs and records small certificates.
  Boundary. Finite search is not a cofinal statement.
  Evidence. finite computation · external exact computation

• three_prime_lcm_cells
  Comparator: targeted_running_lcm_identity

• two_prime_transcendence
  Comparator: not_applicable_not_a_lean_declaration

• height_fibre_and_shell
  Comparator: represented_by_three_prime_structure_target

• rank_two_kernel_no_go
  Comparator: targeted

• dyadic_block_alphabet
  Comparator: represented_by_three_prime_structure_target

• conditional_carry_escape
  Comparator: not_selected_unproved_bridge_and_deep_predicates

• three_prime_finite_search
  Comparator: not_applicable_not_a_lean_theorem

ErdosProblems.Erdos1041.newtonFlow_value_hasDerivAt

Exact registry keys and Comparator routing are listed separately.

• Newton value decay
  The Newton value equation and its exponential first integral are checked exactly.
  Boundary. Value decay alone does not give a short connecting curve.
  Evidence. locally proved result and formalised calculus; novelty unassessed · Lean kernel

• Ray separation
  Distinct positive rays exclude a finite Newton connection.
  Boundary. The result is a route obstruction, not the global theorem.
  Evidence. locally proved result; novelty unassessed · Lean kernel

• Translation avoidance
  Collision translations are parameterised by real affine lines and an arbitrarily small common translation avoids finitely many of them.
  Boundary. The finite-family avoidance theorem does not perform the global topology or metric gluing.
  Evidence. locally proved result; novelty unassessed · Lean kernel plus Comparator

• Root retention
  A quantified small constant perturbation keeps every polynomial root inside the open unit disc.
  Boundary. Root retention is one input to a still-incomplete route.
  Evidence. locally proved result; novelty unassessed · Lean kernel plus Comparator

• Published proof gap
  The paper identifies an invalid local saddle block in a claimed unrestricted proof.
  Boundary. The diagnosis does not prove that no repair exists.
  Evidence. paper diagnosis · authored source analysis

• Lemniscate finite search
  A bounded search records finite geometric evidence.
  Boundary. Finite evidence does not settle the universal problem.
  Evidence. finite computation · external computation

• newton_value_decay
  Comparator: not_selected_compact_calculus_family

• ray_separation
  Comparator: represented_by_translation_avoidance_targets

• translation_avoidance
  Comparator: targeted

• root_retention
  Comparator: targeted

• published_proof_gap
  Comparator: not_applicable_not_a_lean_proposition

• lemniscate_finite_search
  Comparator: not_applicable_not_a_lean_theorem

ErdosProblems.Erdos1049.threeHalves_no_coordinatewiseCorridor

Exact registry keys and Comparator routing are listed separately.

• Scalar content no go
  Integer scalar content changes analytic error and exterior determinant by matching factors, yielding no margin by itself.
  Boundary. The conclusion is scoped to one normalisation strategy.
  Evidence. no-go result · Lean kernel

• Endpoint residues
  Endpoint residues at 2 and 3 exclude a common multiplier under unit-endpoint hypotheses.
  Boundary. Other local or cross-row arithmetic remains possible.
  Evidence. no-go result · Lean kernel

• Four jet collision
  Binary selectors collide in the four-jet signature at the stated rank and depth.
  Boundary. A signed relation is not nonzero analytic data.
  Evidence. locally proved result and no-go result; novelty unassessed · Lean kernel

• Coordinatewise corridor no go
  The coordinatewise corridor forces a power-versus-linear inequality and cannot occur at base 3/2.
  Boundary. This excludes one proof architecture and proves no irrationality statement.
  Evidence. no-go result · Lean kernel plus Comparator

• Rational base tail recurrence
  The exact rational-base cleared-tail recurrence exposes exponential denominator-base forcing absent at integer bases.
  Boundary. The recurrence is not derived from a rationality contradiction.
  Evidence. locally proved result; novelty unassessed · Lean kernel plus Comparator

• Seven halves irrationality
  Irrationality at 7/2 is obtained from an external analytic criterion whose elementary height hypothesis is checked in Lean.
  Boundary. Comparator may check the height inequality, not the cited theorem application.
  Evidence. paper plus external theorem · paper argument plus cited theorem and Lean arithmetic

• Height and pade arithmetic
  Exact height-region inclusions and exclusions, Padé denominator-exponent bounds, and a rectangular Hermite-Padé threshold no-go are checked.
  Boundary. The analytic remainder and nonvanishing input remain untreated.
  Evidence. locally proved result and finite arithmetic; novelty unassessed · Lean kernel

• scalar_content_no_go
  Comparator: represented_by_selected_coordinatewise_no_go

• endpoint_residues
  Comparator: represented_by_selected_coordinatewise_no_go

• four_jet_collision
  Comparator: not_selected_finite_combinatorial_family

• coordinatewise_corridor_no_go
  Comparator: targeted

• rational_base_tail_recurrence
  Comparator: targeted

• seven_halves_irrationality
  Comparator: not_applicable_to_external_irrationality_conclusion

• height_and_pade_arithmetic
  Comparator: not_selected_multiple_scoped_arithmetic_families