External verification

Reader tiers

• Completed direct results: unconditional checked consequences with their scope kept visible.
• Conditional endpoint routes: target-facing routes whose explicit producer or selector remains open.
• Exact endpoint reductions and structural results: results that sharpen the remaining problem without being presented as endpoint theorems.

Source-ranked frontier

1. Finite prime weighted support (Erdos249257.ExternalVerification.divisibilityWeightedClaim; selected)
   • Reader tier. completed direct result
   • Consequence. For every integer base b ≥ 2 it proves irrationality on every infinite positive support of finite prime-weighted mass; a positive host of finite binary weighted mass gives irrationality for every infinite subset at every integer base.
   • Load-bearing mechanism. The source proof builds a concrete weighted dyadic-mean producer with divisibility and scale control, obtains cofinal close returns, and consumes them in the irrationality criterion. The separate fixed-base hereditary theorem restricts the nonnegative weighted summability witness to subsets.
   • Source and evidence. Lean source; The source theorem is Lean-checked in PaperCompleteR8/WeightedReturn.lean:120. This packet includes a separately declared Comparator interface and thin transport. The replay guide’s repository CI record reports a passing weighted-support positive check and deliberate statement-mismatch rejection at commit 7e33a58bb86180013b1fb855cdd8aaff1d7f9057. The recorded CI result applies only to that snapshot. Independent Linux replay remains pending; verification of later commits requires receipts bound to those commits.
   • Boundary. The finite-prime weighted-summability premise is explicit in both clauses. This criterion does not cover every infinite support or settle universal Erdős #257; no novelty, priority, significance, or external human-review claim is made. Overclaim risk. The finite-prime weighted-summability hypothesis and 0 ∉ support condition must stay visible. The theorem does not prove irrationality for arbitrary infinite support, novelty, priority, or external human review.
2. Known irrational supports (Erdos249257.ExternalVerification.irrational_erdosSum_full_support; represented)
   • Reader tier. completed direct result
   • Consequence. Directly settles the canonical full-support member of Erdős #257 for every integer base b >= 2, while leaving universal arbitrary-support irrationality open.
   • Load-bearing mechanism. The source exposes the bounded Bertrand/CRT first-block frame, middle-window divisor-pair averaging with pigeonhole selection, weighted tail bounds, and explicit parameter closure.
   • Source and evidence. Lean source; The exact source theorem is committed at Erdos249257/CertificateKernel.lean:8323-8331 and is transported by the committed Challenge/Solution pair.
   • Boundary. This is the classical full-support theorem, not universal Erdos #257. Overclaim risk. Low only under the stated boundary: this is full support, not all infinite supports, and local proof plus Comparator is not a novelty or human-review claim.
3. Pairwise coprime support (Erdos249257.ExternalVerification.irrational_erdosSupportSeries_pairwise_coprime; represented)
   • Reader tier. completed direct result
   • Consequence. Direct irrationality for every infinite pairwise-coprime support with summable reciprocal mass, but not for arbitrary supports.
   • Load-bearing mechanism. Adaptive CRT weighted coefficient certificates absorb first-block hits and control residue strays through summable reciprocals.
   • Source and evidence. Lean source; The exact source theorem is committed at Erdos249257/CertificateKernel.lean:10768-10782 and is transported by the committed Challenge/Solution pair.
   • Boundary. This is the pairwise-coprime support theorem, not universal Erdos #257; the infinitude, pairwise-coprimality, and summable-reciprocal hypotheses remain explicit. Overclaim risk. Moderate unless infinitude, pairwise coprimality, and summable reciprocal mass stay visible in every projection.
4. Orthogonal petal sunflower reduction (Erdos249257.ExternalVerification.irrational_erdosSupportSeries_of_orthogonalPetalBouquet; represented)
   • Reader tier. conditional endpoint route
   • Consequence. Direct irrationality under the displayed structure, but the structural predicates are not constructed for arbitrary supports.
   • Load-bearing mechanism. The conditional selector is the natural friction; omitting it would turn a reduction into a false unconditional theorem.
   • Source and evidence. Lean source; Exact committed source and Comparator transport are available.
   • Boundary. This is a conditional reduction: the bouquet structure and uniform tail-selection predicate remain hypotheses; neither is constructed for arbitrary supports, so this does not add an unconditional Erdos #257 support family or solve the universal problem. Overclaim risk. High if the bouquet and uniform tail-selection hypotheses are silently treated as automatic.
5. Periodic nonnegative weight irrationality (Erdos249257.ExternalVerification.irrational_ratWeightSeries_eventuallyPeriodic; represented)
   • Reader tier. completed direct result
   • Consequence. Close to the Lambert-series endpoint but not a universal support theorem and not the mixed-sign statement.
   • Load-bearing mechanism. A periodic divisor-orbit sieve and denominator clearing route are visible in the source.
   • Source and evidence. Lean source; Exact committed source and Comparator transport are available.
   • Boundary. This is the nonnegative rational eventually-periodic coefficient theorem; its nonnegativity, eventual periodicity, and positive-tail hypotheses remain explicit, and the broader mixed-sign periodic theorem is not claimed. Overclaim risk. Moderate if the mixed-sign or arbitrary-support cases are inferred.
6. Actual lcm orbit separation (Erdos249257.ExternalVerification.irrational_totientSeries_of_actualLcmOrbitSeparationSupply; represented)
   • Reader tier. conditional endpoint route
   • Consequence. It points directly at the binary totient irrationality endpoint for Erdős #249, conditional on a cofinal separation supply; it does not prove that supply.
   • Load-bearing mechanism. The source carries a raw adjacent-suffix approximation, an explicit error radius, and uniform separation from every integer into a signed-margin producer. The cofinal PowerTwoActualLcmOrbitSeparationSupply is the natural friction and remains a premise.
   • Source and evidence. Lean source; The source definition and implication are committed at Erdos249257/TotientActualLcmOrbitSeparation.lean:305, and the exact wrapper is committed in ExternalVerification/Challenge.lean and ExternalVerification/Solution.lean at the configured declaration.
   • Boundary. The cofinal separation supply is an open premise, stronger than mere non-integrality; this sufficient route is not an equivalence and leaves the punctured/top-edge boundary and the Erdős #249 endpoint open. Overclaim risk. High unless the two cofinal supply clauses stay attached: the implication is source-faithful and checked, but the supply itself is not proved here.
7. First harmonic pivot decomposition (Erdos249257.ExternalVerification.irrational_totient_series_of_pivotResidualDecorrelation; represented)
   • Reader tier. conditional endpoint route
   • Consequence. It points directly at Erdős #249 irrationality from an explicit cofinal analytic producer, independently of the actual-LCM orbit route; that producer remains unproved.
   • Load-bearing mechanism. Supplier fibres, pivot correlation, bad and non-supplier contributions, and the controlled remainder are kept separate. The finite counterexample to global isolation and the missing DTWPivotResidualDecorrelation supply are the natural friction.
   • Source and evidence. Lean source; The source theorem, canonical review family, and exact Comparator endpoint wrapper are committed; the cofinal decorrelation producer is explicitly absent.
   • Boundary. The four-term decomposition and 9X/10 gap remain conditional on the explicit dyadic-room and PivotBudgetAt hypotheses; the cofinal decorrelation producer is unproved. The fibre/image lemmas do not give global supplier-prime isolation or a prime-distribution estimate, and no Erdős #249 irrationality conclusion is claimed. Overclaim risk. High unless DTWPivotResidualDecorrelation remains attached as an unproved cofinal premise; this is not an unconditional #249 result.
8. Strict prime tail orbit gap (Erdos249257.ExternalVerification.irrational_totient_series_of_naturalPrimeTailOrbitStrictGap; represented)
   • Reader tier. conditional endpoint route
   • Consequence. It reaches the Erdős #249 irrationality consumer conditionally and is more than a finite normal form, but neither phase-density nor cofinal-prime producer is proved.
   • Load-bearing mechanism. Unit norm and the complement estimate give the exact 89/100 block bound; a 1/100 truncation budget yields the 9/10 finite gap, while the prime branch uses an adaptive positive margin and exact pivot-fibre membership. The two global producer predicates are the natural friction.
   • Source and evidence. Lean source; The exact source declarations, canonical strict_prime_tail_orbit_gap family, and Comparator representative are committed at Claims ddbe2870 and transport e7a58bb3.
   • Boundary. The phase-density, cofinal natural-prime strict-gap, associated uniform-margin, and cofinal nonpositive-prime-shift producers remain unproved for the actual totient orbit. Exact phase/integrality equivalence, finite dyadic-root exclusion for 1 ≤ h ≤ 16 and k ≤ 14, and non-dyadicity-to-cofinal-nonpositive-phase implications are classification or finite evidence only; they do not supply density or prime alignment, and the source does not prove actual root entry. This is a conditional reduction only: no unconditional Erdős #249 endpoint, novelty, priority, significance, or external-review claim is made. It is distinct from the finite first_harmonic_pivot_decomposition and actual_lcm_orbit_separation families. Overclaim risk. High unless the unproved density, cofinal natural-prime strict-gap, uniform-margin, and cofinal nonpositive-prime-shift producers stay explicit; no unconditional #249, novelty, priority, significance, or external-review claim follows.
9. Factorial carry characterisation (Erdos249257.ExternalVerification.irrational_factorialGapSeries_iff_cofinal_nonunit_carries; subordinate)
   • Reader tier. exact reduction or structural result
   • Consequence. Maximal endpoint proximity for #68, but it does not prove the cofinal producer.
   • Load-bearing mechanism. The carry recurrence is the useful mechanism; the missing cofinal witness is the natural unresolved friction.
   • Source and evidence. Lean source; Exact committed source and Comparator transport are available.
   • Boundary. The equivalence does not supply a cofinal carry producer. Overclaim risk. High if the equivalence is mistaken for a cofinal carry proof.
10. Prime gap reformulation (Erdos249257.ExternalVerification.irrational_tsum_primeDyadicTerm_iff_primeGap; subordinate)

• Reader tier. exact reduction or structural result
• Consequence. Very close to #251’s target but proves neither side irrational and retains a summability premise.
• Load-bearing mechanism. The key mechanism is summation-by-parts normalization; the target irrationality remains open.
• Source and evidence. Lean source; Exact committed source and Comparator transport are available.
• Boundary. The equivalence does not prove irrationality of either series. Overclaim risk. High if equivalence is read as irrationality.

11. Totient carry anti compression (Erdos249257.ExternalVerification.not_irrational_totientSeries_implies_mod_period_and_unbounded_rank; represented)

• Reader tier. exact reduction or structural result
• Consequence. This is an orbit-level necessary consequence of the #249 rational branch, closer to the endpoint than coefficient-side kernel rank alone, but it derives no contradiction.
• Load-bearing mechanism. The theorem couples modular orbit regularity with exponential finite-level anti-compression. Its natural friction is exact: modulo a divisor of the multiplier the forcing can vanish and the carry can become geometric, so periodicity supplies no finite-Q-rank upper bound.
• Source and evidence. Lean source; The exact source theorem, canonical review family, and Comparator representative are committed; the missing finite-rank contradiction is explicit.
• Boundary. This is a necessary consequence of rationality only: it gives no contradiction, no finite-rank upper bound for a rationality-supplied carry, and no irrationality proof for Erdős #249. Modulo a divisor of the multiplier, the forcing disappears and the carry becomes geometric, so quotient periodicity alone supplies no finite-ℚ-rank upper bound. The coefficient-side kernel-rank and certificate-equivalence families are not duplicated, and #249 remains open. Overclaim risk. High if modular periodicity and unbounded canonical-kernel rank are reported as incompatible; the source proves no such upper bound and no #249 irrationality.

12. Half membership seam classification (Erdos249257.ExternalVerification.half_mem_mersenneAchievementSet_iff_unboundedTerminalFalse; represented)

• Reader tier. exact reduction or structural result
• Consequence. It classifies the concrete #257 half-membership endpoint exactly, closer to a usable target than an analytic recovery criterion or source-only certificate normal form, but supplies no occurrence witness.
• Load-bearing mechanism. Finite integer seam construction and terminal-bit normalization expose the global supply condition in interchangeable forms. The natural friction is decisive: none of those forms is proved to occur unboundedly.
• Source and evidence. Lean source; The exact source iff, canonical claims family, and committed Comparator representative are available; the absent occurrence producer is explicit.
• Boundary. This exact endpoint-socket classification does not supply any unbounded terminal-false or upper-or-middle occurrences, cofinal supply, skipped-support producer, or half-membership witness; finite exact rows do not establish the required global supply. It is not an unconditional or universal Erdős #257 result, and no novelty, priority, significance, or external-review claim is made. Overclaim risk. High if an iff is described as a half-membership witness or if finite exact rows are treated as cofinal supply; it proves no universal #257 result.

13. Negative mass recovery (Erdos249257.ExternalVerification.sylvesterNext_eventually_of_summable_negativeRelativeMass; represented)

• Reader tier. conditional endpoint route
• Consequence. It gives a sharp conditional structural conclusion for Erdős #243 and proves that any surviving canonical orbit must evade finite negative mass, but it does not establish the original-orbit hypotheses or reciprocal-tail irrationality.
• Load-bearing mechanism. The tail-growth estimate by 1 + negativeRelativeMass feeds finite-negative-mass stabilization, killing the centered defect. The hard friction is that summability, positivity, strict centering, normalized vanishing, and the exact C/D dynamics are all premises rather than proved properties of the original orbit.
• Source and evidence. Lean source; The exact source theorem, canonical review family, and committed Comparator representative are available at Claims 6bedcde3 and transport 39d0c4bd.
• Boundary. This is a conditional recovery criterion: the source theorem assumes every displayed dynamics, positivity, strict centered-step, normalized-vanishing, and summability hypothesis, and does not prove them for the original Erdős #243 orbit. Any surviving canonical orbit must have divergent normalized negative mass. It supplies no prime-specific producer, unconditional #243 endpoint, or reciprocal-tail irrationality, and makes no novelty, priority, significance, or external-review claim. It is distinct from centered_state_dynamics, which uses a uniform lower-bound hypothesis rather than summability of normalized negative mass. Overclaim risk. High if the conditional summability criterion is reported as applying to the original reciprocal-tail orbit; it proves no unconditional #243 endpoint, prime-specific producer, or reciprocal-tail irrationality.

Natural friction and no-go boundaries

These checked obstructions are an alphabetical, deliberately unranked tier. They show where natural proof friction survives without competing with direct endpoint results for headline position.

• #243 · Bounded negative exclusion (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

• #251 · Coefficient only no go (coefficient_only_no_go)
  The exact finite carry identity and the two non-eventual-periodicity statements expose the coefficient-only barrier: irregularity and growth of a coefficient stream do not by themselves force irrationality, while the synthetic carry stream remains distinct from the actual prime-gap stream.
  Boundary. CoefficientOnlyNoGo checks the exact finite partial-sum identity and the two non-eventual-periodicity statements. It does not assert the infinite limit of the synthetic countermodel, identify its coefficient stream with actual prime gaps, establish a prime-gap tail bridge, prove #251 irrationality, or make novelty, priority, significance, or external-review claims.
  Evidence. coefficient-only barrier; novelty and significance unassessed · Lean kernel plus authored synthesis

• #269 · Conditional carry escape (conditional_carry_escape)
  Under the denominator-dependent cofinal local-window residue-escape predicate, no positive reduced carry can satisfy the exact multiplier recurrence together with its short bound. The load-bearing consumer is no_positive_reducedCarry_of_cofinalLocalWindowEscape; an absorbed nonzero common-factor carry reduces exactly to that consumer. CofinalLocalWindowEscape, windowBase, windowForcing, leastPositiveResidue, and the absorbed-carry bridge are subordinate finite-window mechanism evidence.
  Boundary. The representative assumes b,m : ℕ → ℕ, shortBound : ℕ → ℕ → ℕ, CofinalLocalWindowEscape b m shortBound, and for each positive B coprime to 30 a positive integer-valued d with d(n+1) = (b n : ℤ) d(n) − (B : ℤ) (m n : ℤ) and Int.natAbs (d n) ≤ shortBound B n; it then gives False. The absorbed-carry bridge additionally assumes smoothFactor ≠ 0, c n = smoothFactor * d n, and the corresponding exact absorbed recurrence, then cancels that factor to the same reduced consumer. The representative remains a conditional consumer for arbitrary words. For the actual three-prime word, the rationality-to-reduced-carry bridge is established separately; the source-specific cofinal escape producer is not proved. This is not a #269 endpoint or irrationality proof, and no actual-series identification, novelty, priority, significance, or external-review claim is made. It is one conditional window-carry family, distinct from the finite residue, rank-two, and weighted-phase observer families.
  Evidence. conditional no-go consumer; novelty and significance unassessed · Lean kernel plus Comparator

• #1049 · Coordinatewise corridor no go (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

• #1049 · Endpoint residues (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

• #249 · Fixed precision transport no go (fixed_precision_transport_no_go)
  At every fixed positive precision, every finite word of odd valuation-unit symbols admits a compatible centred carry completion from any incoming integer state; bounded local signatures therefore cannot exclude all finite centred endpoints.
  Boundary. This is a synthetic finite-word construction with unrestricted incoming/high quotient states. It does not impose the actual totient-difference relation or provide growing-precision/global correlation, and it gives no Erdős #249 endpoint or irrationality result. No novelty or priority claim is made. The one-step and finite-word completion theorems are subordinate mechanisms, not separate families.
  Evidence. unconditional synthetic no-go; novelty unassessed · Lean kernel plus Comparator

• #1049 · Four jet collision (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

• #257 · Half and twenty one frontiers (half_and_twenty_one_frontiers)
  Exact greedy characterisations, finite-support exclusions, the odd 2-adic two-thirds-band bound, and two conditional rational-half countermodel frontiers isolate local constraints around the remaining 1/2 and 1/21 alternatives.
  Boundary. Neither membership question is decided; the 2-adic bound is sharp locally, and the two countermodel routes require unconstructed terminal-scaled or cofinal-cylinder antecedents.
  Evidence. conditional reduction and no-go result · Lean kernel plus Comparator

• #1049 · Height and pade arithmetic (height_and_pade_arithmetic)
  For the explicit rectangular two-function exponent model, the cleared gap is nonpositive throughout rho >= 0 and 1 + rho <= sigma, and the threshold is at most 1/2 - 1/pi^2 with equality exactly at rho = 0, sigma = 1. The gap sign and unique-zero mechanism support this sharp threshold no-go within the wider height-and-Padé arithmetic family.
  Boundary. This is a sharp no-go only for the explicit rectangular two-function exponent model under the stated real hypotheses; it constructs no approximating polynomials or remainders and is not a universal Padé or Hermite-Padé no-go. It proves no irrationality at 3/2 or any general rational-base endpoint, and the analytic remainder/nonvanishing input remains untreated. No novelty, priority, significance, external-review, or endpoint claim is made; Erdős #1049 remains open.
  Evidence. locally proved sharp model-specific no-go; novelty unassessed · Lean kernel plus Comparator

• #249 · Lcm factor ideal shift algebra no go (lcm_factor_ideal_shift_algebra_no_go)
  For every t at least 3, a nonzero synthetic dyadic coboundary survives every finite integer shift polynomial while retaining the period-LCM totient factor ideals, exact cleared-prefix cancellation, and uniform state and letter bounds.
  Boundary. The witness is synthetic: it does not assert that its forcing letters are actual totient differences, does not address nonlinear combinations, and leaves the unbounded certificate supply for Erdős #249 open.
  Evidence. unconditional progress · Lean kernel plus Comparator

• #243 · Negative orbit no go (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

• #269 · Rank two kernel no go (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

• #1049 · Scalar content no go (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

Complete inventory, kept subordinate

Every contribution family and the documented statement-isolated interfaces remain queryable in the programme dossiers and the Comparator interface appendix. Subordination is a presentation judgement, not deletion or an adverse mathematical disposition.

Complete serious-result universe

All 76 source-current review families are accounted for here. The categories preserve honest selection reasons while the programme dossiers below retain each family’s exact mechanism and boundary. This inventory is complete but deliberately does not compete with the ranked frontier for attention.

• represented (54). #257 achievement_set_geometry, #249 actual_foreign_residue_projection, #249 actual_lcm_orbit_separation, #257 boolean_mobius_carry, #257 boolean_mobius_exact_row_dynamics, #243 bounded_negative_exclusion, #243 bounded_rise_coprimality, #1049 calibrated_rational_hankel_countermodel, #243 centered_state_dynamics, #251 coefficient_only_no_go, #257 composite_dilation_defect_identity, #269 dyadic_block_alphabet, #251 dyadic_tail_integrality_classification, #249 eventually_periodic_lambert, #68 factorial_carry_characterisation, #68 factorial_channel_and_projection_rigidity, #257 finite_period_noncollapse, #257 finite_prime_weighted_support, #249 first_harmonic_pivot_decomposition, #249 fixed_precision_transport_no_go, #257 half_membership_seam_classification, #1049 height_and_pade_arithmetic, #269 height_fibre_and_shell, #269 independent_clock_channel_relations, #251 integral_shift_classification, #257 known_irrational_supports, #1041 newton_value_decay, #257 orthogonal_petal_sunflower_reduction, #257 pairwise_coprime_support, #257 periodic_nonnegative_weight_irrationality, #251 prime_gap_reformulation, #1049 rational_base_tail_recurrence, #1041 ray_separation, #257 restricted_achievement_sets, #1041 root_retention, #257 separated_cut_algebraic_lambert_transcendence, #257 shifted_odd_tail_state, #249 signed_totient_entire_defect_interpolation, #251 small_mismatch_criterion, #249 squared_lambert_gcd_moments, #249 stern_brocot_cylinder_law, #249 stern_brocot_run_fibonacci_stability, #249 strict_prime_tail_orbit_gap, #269 three_prime_lcm_cells, #249 totient_carry_anti_compression, #249 totient_certificate_equivalences, #249 totient_kernel_all_base_index, #249 totient_kernel_basis, #249 totient_kernel_rank, #249 totient_lambert_coefficients, #251 totient_shift_propagation, #249 totient_visible_coprime_lattice_mass, #1041 translation_avoidance, #269 weighted_phase_carry_observer

• subordinate (7). #269 conditional_carry_escape, #68 factorial_conditional_producers, #1049 four_jet_collision, #257 half_and_twenty_one_frontiers, #243 negative_mass_recovery, #269 selected_staircase_integral_height_boundary, #249 totient_carry_rank

• rejected (6). #1049 coordinatewise_corridor_no_go, #1049 endpoint_residues, #249 lcm_factor_ideal_shift_algebra_no_go, #243 negative_orbit_no_go, #269 rank_two_kernel_no_go, #1049 scalar_content_no_go

• long tail (9). #68 factorial_finite_certificates, #68 factorial_lcm_growth, #1041 lemniscate_finite_search, #1041 published_proof_gap, #1049 seven_halves_irrationality, #257 squarefree_support, #269 three_prime_finite_search, #249 totient_finite_denominator_exclusion, #269 two_prime_transcendence

Programmes. #68: Factorial-denominator series · #243: Reciprocal-tail rigidity near the Sylvester recurrence · #249: Binary totient series · #251: Prime-gap dyadic series · #257: Reciprocal sums over infinite exponent supports · #269: Three-prime running least common multiples · #1041: Short connections inside polynomial lemniscates · #1049: Lambert-type series at rational bases

## #68: Factorial-denominator series

Question. Is the series sum_{n >= 2} 1/(n! - 1) irrational?

Checked frontier. The exact integral normal form: the series is irrational if and only if the strict factorial successor Z_m misses divisibility by m cofinally.

Open boundary. Irrationality of the factorial-denominator series.

Read. Programme paper · Lean source

First-contact mathematical order

This is Palomar’s source-current reader order, not review-matrix or Comparator roster order. Ranked results lead; conditional endpoint leverage, deep mechanisms, natural friction, and supporting rows follow unequally.

1. Factorial carry characterisation (factorial_carry_characterisation; source-ranked frontier; global rank 9; source disposition represented)
   • Why here. Maximal endpoint proximity for #68, but it does not prove the cofinal producer.
   • Source. Erdos249257.ExternalVerification.irrational_factorialGapSeries_iff_cofinal_nonunit_carries in Lean
   • Boundary. The equivalence does not supply a cofinal carry producer.
   • Relation. supports_without_producing factorial_channel_and_projection_rigidity: Finite channel rigidity feeds the carry endpoint route but supplies no cofinal non-unit carry.
2. Factorial conditional producers (factorial_conditional_producers; conditional endpoint leverage; source disposition subordinate)
   • Why here. A single coefficient-free cofinal complementary-tail certificate would imply the #68 endpoint, but the certificate supply is an explicit unproved premise; this is a shorter conditional consumer, not an irrationality proof.
   • Source. Erdos249257.ExternalVerification.irrational_factorialGapSeries_of_cofinal_global_complementaryTail in Lean
   • Boundary. The producer hypotheses are unproved.
3. Factorial channel and projection rigidity (factorial_channel_and_projection_rigidity; deep mechanism and classification; source disposition represented)
   • Why here. The finite channel and projection machinery is the deepest represented #68 mechanism below the endpoint equivalence, but it supplies no cofinal obstruction.
   • Source authority. Canonical review family factorial_channel_and_projection_rigidity in claims
   • Boundary. These finite and structural results do not produce a cofinal obstruction.
   • Relation. supports_without_producing factorial_carry_characterisation: Finite channel rigidity feeds the carry endpoint route but supplies no cofinal non-unit carry.

## #243: Reciprocal-tail rigidity near the Sylvester recurrence

Question. Under a rapid-growth hypothesis on an integer sequence, does rationality of its reciprocal sum force the sequence to satisfy the Sylvester recurrence eventually?

Checked frontier. Lean proves cubic_rate_irrationality_unconditional for positive StrictMono zero-indexed a_n with a_n²/a_(n+1) = 1 + 3/n + o(n^-3). The one-based paper uses a finite-prefix bridge; general #243 remains open.

Open boundary. The unrestricted problem.

Read. Programme paper · Lean source

First-contact mathematical order

This is Palomar’s source-current reader order, not review-matrix or Comparator roster order. Ranked results lead; conditional endpoint leverage, deep mechanisms, natural friction, and supporting rows follow unequally.

1. Bounded negative exclusion (bounded_negative_exclusion; conditional endpoint leverage; source disposition represented)
   • Why here. Excludes a bounded-negative regime only under explicit dynamical hypotheses; it does not decide the unrestricted reciprocal-tail endpoint.
   • Source. Erdos249257.ExternalVerification.no_cofinallyBoundedNegative_of_normalizedVanishes in Lean
   • Boundary. Every positivity, dynamics, bounded-rise, and vanishing hypothesis remains explicit.
   • Relation. mechanism_for centered_state_dynamics: Centered-state descent is the exact dynamics consumed by the bounded-negative exclusion.
2. Negative mass recovery (negative_mass_recovery; source-ranked frontier; global rank 13; source disposition subordinate)
   • Why here. It gives a sharp conditional structural conclusion for Erdős #243 and proves that any surviving canonical orbit must evade finite negative mass, but it does not establish the original-orbit hypotheses or reciprocal-tail irrationality.
   • Source. Erdos249257.ExternalVerification.sylvesterNext_eventually_of_summable_negativeRelativeMass in Lean
   • Boundary. This is a conditional recovery criterion: the source theorem assumes every displayed dynamics, positivity, strict centered-step, normalized-vanishing, and summability hypothesis, and does not prove them for the original Erdős #243 orbit. Any surviving canonical orbit must have divergent normalized negative mass. It supplies no prime-specific producer, unconditional #243 endpoint, or reciprocal-tail irrationality, and makes no novelty, priority, significance, or external-review claim. It is distinct from centered_state_dynamics, which uses a uniform lower-bound hypothesis rather than summability of normalized negative mass.
   • Relation. independent_analytic_recovery_peer centered_state_dynamics: Both recover eventual centered-state zero and Sylvester dynamics only under explicit hypotheses, but negative_mass_recovery uses summability of normalized negative mass whereas centered_state_dynamics uses a uniform lower-bound route; neither supplies the original-orbit premises.
3. Centered state dynamics (centered_state_dynamics; deep mechanism and classification; source disposition represented)
   • Why here. The committed source-faithful representative exposes the signed centered-state recovery theorem with exact natural C/D dynamics, strict centered margin, lower bound, and normalized vanishing; the centered-zero and Sylvester recovery lemmas remain subordinate, and no reciprocal-tail irrationality follows.
   • Source. Erdos249257.ExternalVerification.boundedNegativePart_eventually_zero in Lean
   • Boundary. The signed theorem has a C D : ℕ → ℕ, E : ℕ → ℤ, and B : ℕ with all exact hypotheses explicit: a > 1, C > 0, C(n + 1) + D(n) = a(n) · C(n), D(n + 1) = a(n) · D(n), E is the centered state D − (a − 1)C, |E| < C, a uniform lower bound on E, and division-free normalized vanishing. It excludes persistent bounded negative behaviour and forces eventual centered defect zero; centered-zero plus an eventually nonzero next tail recovers Sylvester, but no reciprocal-tail irrationality follows. The unbounded negative mixed-sign branch and the prime-specific producer remain open. This is distinct from the periodic negative-orbit and cofinally bounded-negative no-go families; no novelty, priority, significance, or external-review claim is made, and no unrestricted #243 solution follows.
   • Relation. mechanism_for bounded_negative_exclusion: Centered-state descent is the exact dynamics consumed by the bounded-negative exclusion.
   • Relation. independent_analytic_recovery_peer negative_mass_recovery: Both recover eventual centered-state zero and Sylvester dynamics only under explicit hypotheses, but negative_mass_recovery uses summability of normalized negative mass whereas centered_state_dynamics uses a uniform lower-bound route; neither supplies the original-orbit premises.
4. Bounded rise coprimality (bounded_rise_coprimality; natural friction and no-go; source disposition represented)
   • Why here. The fresh-modulus obstruction explains why bounded rise would be decisive, but bounded rise is not automatic for the original reciprocal-tail orbit.
   • Source authority. Canonical review family bounded_rise_coprimality in claims
   • Boundary. The required bounded-rise input is not automatic for the original sequence.
5. Negative orbit no go (negative_orbit_no_go; natural friction and no-go; source disposition rejected)
   • Why here. Retires an eventually-periodic negative orbit architecture, but leaves arbitrary unbounded negative behaviour and the #243 target open.
   • Source. Erdos249257.ExternalVerification.no_eventuallyPeriodicNegative_orbit in Lean
   • Boundary. The exclusions do not cover arbitrary unbounded negative behaviour.

## #249: Binary totient series

Question. Is the binary Lambert series sum phi(n)/2^n irrational?

Checked frontier. For every e >= 1, the complete dyadic totient kernel through level e has rational span dimension 2^e+1.

Open boundary. The strict prime-tail orbit gap, which is the unproved producer consumed by the conditional endpoint.

Read. Programme paper · Lean source

First-contact mathematical order

This is Palomar’s source-current reader order, not review-matrix or Comparator roster order. Ranked results lead; conditional endpoint leverage, deep mechanisms, natural friction, and supporting rows follow unequally.

1. Actual lcm orbit separation (actual_lcm_orbit_separation; source-ranked frontier; global rank 6; source disposition represented)
   • Why here. It points directly at the binary totient irrationality endpoint for Erdős #249, conditional on a cofinal separation supply; it does not prove that supply.
   • Source. Erdos249257.ExternalVerification.irrational_totientSeries_of_actualLcmOrbitSeparationSupply in Lean
   • Boundary. The cofinal separation supply is an open premise, stronger than mere non-integrality; this sufficient route is not an equivalence and leaves the punctured/top-edge boundary and the Erdős #249 endpoint open.
   • Relation. independent_conditional_endpoint_peer first_harmonic_pivot_decomposition: Both imply #249 irrationality from different cofinal producers; neither producer is supplied.
   • Relation. conditional_producer_peer strict_prime_tail_orbit_gap: The strict-prime route supplies a phase-density or natural-prime certificate mechanism, while the actual-LCM route instead assumes quantitative orbit separation; all producer predicates remain open.
2. First harmonic pivot decomposition (first_harmonic_pivot_decomposition; source-ranked frontier; global rank 7; source disposition represented)
   • Why here. It points directly at Erdős #249 irrationality from an explicit cofinal analytic producer, independently of the actual-LCM orbit route; that producer remains unproved.
   • Source. Erdos249257.ExternalVerification.irrational_totient_series_of_pivotResidualDecorrelation in Lean
   • Boundary. The four-term decomposition and 9X/10 gap remain conditional on the explicit dyadic-room and PivotBudgetAt hypotheses; the cofinal decorrelation producer is unproved. The fibre/image lemmas do not give global supplier-prime isolation or a prime-distribution estimate, and no Erdős #249 irrationality conclusion is claimed.
   • Relation. independent_conditional_endpoint_peer actual_lcm_orbit_separation: Both imply #249 irrationality from different cofinal producers; neither producer is supplied.
   • Relation. conditional_producer_peer strict_prime_tail_orbit_gap: Both feed the finite first-harmonic certificate socket, but strict-prime uses phase density or adaptive natural-prime escape while the pivot family uses a four-term supplier-fibre budget and residual decorrelation.
3. Strict prime tail orbit gap (strict_prime_tail_orbit_gap; source-ranked frontier; global rank 8; source disposition represented)
   • Why here. It reaches the Erdős #249 irrationality consumer conditionally and is more than a finite normal form, but neither phase-density nor cofinal-prime producer is proved.
   • Source. Erdos249257.ExternalVerification.irrational_totient_series_of_naturalPrimeTailOrbitStrictGap in Lean
   • Boundary. The phase-density, cofinal natural-prime strict-gap, associated uniform-margin, and cofinal nonpositive-prime-shift producers remain unproved for the actual totient orbit. Exact phase/integrality equivalence, finite dyadic-root exclusion for 1 ≤ h ≤ 16 and k ≤ 14, and non-dyadicity-to-cofinal-nonpositive-phase implications are classification or finite evidence only; they do not supply density or prime alignment, and the source does not prove actual root entry. This is a conditional reduction only: no unconditional Erdős #249 endpoint, novelty, priority, significance, or external-review claim is made. It is distinct from the finite first_harmonic_pivot_decomposition and actual_lcm_orbit_separation families.
   • Relation. conditional_producer_peer actual_lcm_orbit_separation: The strict-prime route supplies a phase-density or natural-prime certificate mechanism, while the actual-LCM route instead assumes quantitative orbit separation; all producer predicates remain open.
   • Relation. conditional_producer_peer first_harmonic_pivot_decomposition: Both feed the finite first-harmonic certificate socket, but strict-prime uses phase density or adaptive natural-prime escape while the pivot family uses a four-term supplier-fibre budget and residual decorrelation.
   • Relation. endpoint_normal_form_support_for totient_certificate_equivalences: Certificate completeness identifies the exact finite endpoint socket but cannot manufacture the strict-prime route’s missing phase-density, cofinal-prime, or uniform-margin producer.
4. Totient certificate equivalences (totient_certificate_equivalences; deep mechanism and classification; source disposition represented)
   • Why here. Below the actual-LCM, first-harmonic, and strict-prime producer routes but above medium totient kernel machinery: three exact equivalences expose the endpoint and certificate sockets, while the equivalent lcm-diagonal, period-multiple-kill, and separated-window producers all remain unresolved.
   • Source. Erdos249257.ExternalVerification.exists_clean_binaryCyclotomicAnchor in Lean
   • Boundary. Equivalent producer statements are as hard as the unresolved target.
   • Relation. endpoint_normal_form_support_for strict_prime_tail_orbit_gap: Certificate completeness identifies the exact finite endpoint socket but cannot manufacture the strict-prime route’s missing phase-density, cofinal-prime, or uniform-margin producer.
5. Totient kernel rank (totient_kernel_rank; deep mechanism and classification; source disposition represented)
   • Why here. Exact finite-level dyadic rank growth is strong #249 structure and supports totient_carry_anti_compression, but it is weaker than that orbit-level rationality consequence and provides neither a contradiction nor unbounded certificate supply.
   • Source. Erdos249257.ExternalVerification.finrank_totientKernelThroughLevelFamily_eq in Lean
   • 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.
6. Totient carry anti compression (totient_carry_anti_compression; source-ranked frontier; global rank 11; source disposition represented)
   • Why here. This is an orbit-level necessary consequence of the #249 rational branch, closer to the endpoint than coefficient-side kernel rank alone, but it derives no contradiction.
   • Source. Erdos249257.ExternalVerification.not_irrational_totientSeries_implies_mod_period_and_unbounded_rank in Lean
   • Boundary. This is a necessary consequence of rationality only: it gives no contradiction, no finite-rank upper bound for a rationality-supplied carry, and no irrationality proof for Erdős #249. Modulo a divisor of the multiplier, the forcing disappears and the carry becomes geometric, so quotient periodicity alone supplies no finite-ℚ-rank upper bound. The coefficient-side kernel-rank and certificate-equivalence families are not duplicated, and #249 remains open.
7. Totient kernel all base index (totient_kernel_all_base_index; deep mechanism and classification; source disposition represented)
   • Why here. The rank theorem retains an external linear-independence hypothesis, so it is valuable structural support rather than an unconditional endpoint result.
   • Source. Erdos249257.ExternalVerification.finrank_allBaseTotientKernelThroughLevelFamily_eq_of_linearIndependent in Lean
   • Boundary. This Comparator target reviews the reusable conditional interface. AllBaseTotientKernel.lean separately proves canonical all-base independence and exact rank unconditionally at 25ef6245d15a; it does not formalise Martin’s broader theorem or solve #249.
8. Totient kernel basis (totient_kernel_basis; deep mechanism and classification; source disposition represented)
   • Why here. An explicit basis is useful kernel infrastructure, yet it does not connect finite span structure to the binary totient irrationality endpoint.
   • Source. Erdos249257.ExternalVerification.exists_totientDyadicSectionBasis in Lean
   • Boundary. The basis theorem does not connect rationality of the series to finite kernel rank.
9. Stern brocot run fibonacci stability (stern_brocot_run_fibonacci_stability; deep mechanism and classification; source disposition represented)
   • Why here. A genuine Fibonacci/continuant stability floor, but analytic denominator survival and the #249 endpoint remain unproved.
   • Source. Erdos249257.ExternalVerification.runHeight_defect_fib_sum_lower in Lean
   • Boundary. This exact combinatorial stability floor does not establish analytic denominator survival, irrationality of the binary totient series, or novelty; no #249 endpoint follows.
10. Eventually periodic lambert (eventually_periodic_lambert; deep mechanism and classification; source disposition represented)

• Why here. This is a direct irrationality theorem for an exact structured coefficient class, but the totient-derived coefficients are not eventually periodic, so it is reusable background rather than a #249 frontier.
• Source authority. Canonical review family eventually_periodic_lambert in claims
• Boundary. The totient-derived weights are not eventually periodic.

11. Signed totient entire defect interpolation (signed_totient_entire_defect_interpolation; deep mechanism and classification; source disposition represented)

• Why here. The ordinary proof constructs a sparse signed perturbation with strong defect control for every divergent allowance, but it does not settle the unperturbed totient series or the one-sided prime-gap route; no infinite Lean or Comparator theorem is claimed.
• Source authority. Canonical review family signed_totient_entire_defect_interpolation in claims
• Boundary. The correction is signed, so it does not subsume the one-sided prime-gap theorem. It preserves singularities and prescribed finite jets, not full analytic functions or all Taylor coefficients. The unperturbed totient and prime series remain unresolved.

12. Fixed precision transport no go (fixed_precision_transport_no_go; natural friction and no-go; source disposition represented)

• Why here. The committed representative unconditionally retires fixed-positive-precision local valuation/unit-word escape for every finite odd-unit word through centred completions, while its synthetic unrestricted high-quotient and finite-word scope supplies no actual totient endpoint.
• Source. Erdos249257.ExternalVerification.fixedPrecisionTropicalNoGo in Lean
• Boundary. This is a synthetic finite-word construction with unrestricted incoming/high quotient states. It does not impose the actual totient-difference relation or provide growing-precision/global correlation, and it gives no Erdős #249 endpoint or irrationality result. No novelty or priority claim is made. The one-step and finite-word completion theorems are subordinate mechanisms, not separate families.
• Relation. contrary_evidence_for actual_foreign_residue_projection: Fixed local precision admits synthetic completions, so any successful projection must use growing precision or global correlation.

13. Lcm factor ideal shift algebra no go (lcm_factor_ideal_shift_algebra_no_go; natural friction and no-go; source disposition rejected)

• Why here. A synthetic finite-shift obstruction retires one algebraic route while explicitly leaving actual totient forcing and the unbounded supply open.
• Source. Erdos249257.ExternalVerification.lcm_factorIdeal_finiteRank_shiftAlgebra_not_sufficient in Lean
• Boundary. The witness is synthetic: it does not assert that its forcing letters are actual totient differences, does not address nonlinear combinations, and leaves the unbounded certificate supply for Erdős #249 open.

14. Actual foreign residue projection (actual_foreign_residue_projection; conditional endpoint leverage; source disposition represented)

• Why here. The committed representative exposes the exact finite foreign/divisor partition, geometric tail control, and generic separated-projection consumer for the canonical actual_foreign_residue_projection family; its controlled-projection bridge and unbounded supply remain open, so it is represented conditional evidence rather than a #249 endpoint.
• Source. Erdos249257.ExternalVerification.scaleFullTarget_miss_of_projected_separation in Lean
• Boundary. This is only a finite partition/geometric-majorant reduction feeding a generic complement-noncancellation consumer. The ControlledForeignProjection analytic bridge and any unbounded supply of separated projections remain unproved; no Erdős #249 endpoint, novelty, significance, priority, or external-review claim follows.
• Relation. contrary_evidence_for fixed_precision_transport_no_go: Fixed local precision admits synthetic completions, so any successful projection must use growing precision or global correlation.

15. Totient lambert coefficients (totient_lambert_coefficients; supporting and long tail; source disposition represented)

• Why here. The Lambert rewrite and prime-power coefficient structure orient the programme but provide no irrationality producer.
• Source authority. Canonical review family totient_lambert_coefficients in claims
• Boundary. The coefficient identities do not prove irrationality.

16. Squared lambert gcd moments (squared_lambert_gcd_moments; supporting and long tail; source disposition represented)

• Why here. A precise gcd-moment transfer identity, but it supplies no irrationality conclusion for the binary totient series.
• Source. Erdos249257.ExternalVerification.tsum_totient_div_mersenne_sq_eq_gcd_moment_series in Lean
• Boundary. This exact transfer identity does not prove irrationality of the binary totient series; the cited constant-weight q-Padé result remains external and no #249 endpoint follows.

17. Stern brocot cylinder law (stern_brocot_cylinder_law; supporting and long tail; source disposition represented)

• Why here. Exact Stern–Brocot telescoping is reusable geometry, not an irrationality theorem or novelty claim.
• Source. Erdos249257.ExternalVerification.cylinderMass_split in Lean
• Boundary. This exact telescoping recursion and its geometric interpretation do not prove irrationality of the binary totient series or novelty; the #249 endpoint remains open.

18. Totient visible coprime lattice mass (totient_visible_coprime_lattice_mass; supporting and long tail; source disposition represented)

• Why here. Exact visible-lattice normalization explains a mass term but is rational and does not settle Erdős #249.
• Source. Erdos249257.ExternalVerification.tsum_pos_coprime_inv_mersenne_eq_one in Lean
• Boundary. This rational normalization identity does not prove irrationality of the binary totient series or settle #249.

## #251: Prime-gap dyadic series

Question. Is the dyadic series of consecutive primes irrational? Equivalently, is the corresponding consecutive-prime-gap dyadic series irrational?

Checked frontier. The finite summation-by-parts identity relating the prime dyadic partial sums to the prime-gap dyadic partial sums, with an exact endpoint term and no convergence premise.

Open boundary. The target irrationality.

Read. Programme paper · Lean source

First-contact mathematical order

This is Palomar’s source-current reader order, not review-matrix or Comparator roster order. Ranked results lead; conditional endpoint leverage, deep mechanisms, natural friction, and supporting rows follow unequally.

1. Prime gap reformulation (prime_gap_reformulation; source-ranked frontier; global rank 10; source disposition represented)
   • Why here. Very close to #251’s target but proves neither side irrational and retains a summability premise.
   • Source. Erdos249257.ExternalVerification.irrational_tsum_primeDyadicTerm_iff_primeGap in Lean
   • Boundary. The equivalence does not prove irrationality of either series.
   • Relation. conditional_actual_stream_obstruction_for small_mismatch_criterion: The reformulation gives the exact #251 target language; this fixed-shift actual-prime obstruction identifies what a cofinal adjacent-smallness/mismatch producer would have to destroy. It neither supplies that producer nor turns the reformulation into irrationality.
2. Small mismatch criterion (small_mismatch_criterion; conditional endpoint leverage; source disposition represented)
   • Why here. Below the ranked prime-gap equivalence but above the #269 carry-escape consumer, abstract dyadic-tail classification, and coefficient-only no-go: it is specialized to the actual prime-gap recurrence and identifies the precise cofinal adjacent-smallness producer, while that producer remains unproved.
   • Source. Erdos249257.ExternalVerification.primeGapTailShift_not_eventuallyIntegral_of_cofinal_small_mismatch in Lean
   • Boundary. The representative assumes T : ℕ → ℚ, the DyadicTailRecurrence for the actual prime-gap digits, and for every N₀ an N ≥ N₀ whose adjacent h-shifts both lie strictly in (-1, 1) while the corresponding prime gaps differ. Under that cofinal small-mismatch supply it excludes eventual RatIntegral h-shifts; it does not prove the supply or actual smallness. rationalPrimeGapTail_has_positive_shift_not_eventually_small records the contrary rational-state obstruction for at least one positive shift. This is a conditional reduction only: no #251 irrationality, infinite rational-sum limit, universal producer, novelty, priority, significance, or external-review claim is made; #251 remains open. The actual-prime-gap specialization is distinct from coefficient_only_no_go and does not duplicate prime_gap_reformulation.
   • Relation. normal_form_support_for dyadic_tail_integrality_classification: The abstract shift-integrality normal form explains what the actual-prime cofinal mismatch must destroy.
   • Relation. contrary_evidence_for coefficient_only_no_go: Coefficient irregularity alone is insufficient; the actual-prime adjacent-smallness producer is genuinely additional.
   • Relation. conditional_actual_stream_obstruction_for prime_gap_reformulation: The reformulation gives the exact #251 target language; this fixed-shift actual-prime obstruction identifies what a cofinal adjacent-smallness/mismatch producer would have to destroy. It neither supplies that producer nor turns the reformulation into irrationality.
3. Dyadic tail integrality classification (dyadic_tail_integrality_classification; deep mechanism and classification; source disposition represented)
   • Why here. Below the source-specific conditional endpoint consumers but above negative-method evidence: its exact denominator and all-positive-tail-shift normal forms are deeper and more reusable than a coefficient-only obstruction, while supplying no actual-prime producer.
   • Source. Erdos249257.ExternalVerification.irrational_initial_iff_all_positive_tailShifts_nonintegral in Lean
   • Boundary. These exact statements cover arbitrary integer-digit dyadic tail recurrences with the declared rational and real state types; they classify integrality and give an irrationality normal form but do not supply a cofinal nonintegral shift for the consecutive-prime-gap recurrence. The generic hypotheses therefore do not close the prime-specific producer gap: no prime-gap irrationality, novelty, significance, or external review is claimed, and Erdős #251 remains open. This is one abstract classification family, distinct from prime_gap_reformulation, not a duplicate frontier claim.
   • Relation. normal_form_support_for small_mismatch_criterion: The abstract shift-integrality normal form explains what the actual-prime cofinal mismatch must destroy.
4. Integral shift classification (integral_shift_classification; deep mechanism and classification; source disposition represented)
   • Why here. The block and denominator criteria are reusable rational-state structure below the sharper all-positive-shift normal form and above propagation identities.
   • Source authority. Canonical review family integral_shift_classification in claims
   • Boundary. The concrete prime-gap producer remains missing.
5. Totient shift propagation (totient_shift_propagation; deep mechanism and classification; source disposition represented)
   • Why here. Propagation through totient-length shifts explains rational-state persistence but supplies no contradiction for the actual prime-gap recurrence.
   • Source authority. Canonical review family totient_shift_propagation in claims
   • Boundary. This describes rational states and supplies no contradiction for actual prime gaps.
6. Coefficient only no go (coefficient_only_no_go; natural friction and no-go; source disposition represented)
   • Why here. Below the #251 small-mismatch route and abstract integrality classification: it is valuable natural friction against coefficient-only reasoning, but its synthetic carry stream has no infinite-limit or actual-prime-gap identification bridge.
   • Source. Erdos249257.ExternalVerification.coefficientOnlyNoGo in Lean
   • Boundary. CoefficientOnlyNoGo checks the exact finite partial-sum identity and the two non-eventual-periodicity statements. It does not assert the infinite limit of the synthetic countermodel, identify its coefficient stream with actual prime gaps, establish a prime-gap tail bridge, prove #251 irrationality, or make novelty, priority, significance, or external-review claims.
   • Relation. contrary_evidence_for small_mismatch_criterion: Coefficient irregularity alone is insufficient; the actual-prime adjacent-smallness producer is genuinely additional.

## #257: Reciprocal sums over infinite exponent supports

Question. Is the sum of 1/(2^n-1) over every infinite set of positive exponents irrational?

Checked frontier. Irrationality at every integer base for the classical full support, reciprocal-summable supports, and the finite-prime weighted supports in divisibilityWeightedClaim.

Open boundary. Universal irrationality over all infinite supports, or the proposed rational values 1/2 and 1/21.

Read. Programme paper · Lean source

First-contact mathematical order

This is Palomar’s source-current reader order, not review-matrix or Comparator roster order. Ranked results lead; conditional endpoint leverage, deep mechanisms, natural friction, and supporting rows follow unequally.

1. Finite prime weighted support (finite_prime_weighted_support; source-ranked frontier; global rank 1; source disposition represented)
   • Why here. For every integer base b ≥ 2 it proves irrationality on every infinite positive support of finite prime-weighted mass; a positive host of finite binary weighted mass gives irrationality for every infinite subset at every integer base.
   • Source. Erdos249257.ExternalVerification.divisibilityWeightedClaim in Lean
   • Boundary. The finite-prime weighted-summability premise is explicit in both clauses. This criterion does not cover every infinite support or settle universal Erdős #257; no novelty, priority, significance, or external human-review claim is made.
2. Known irrational supports (known_irrational_supports; source-ranked frontier; global rank 2; source disposition represented)
   • Why here. Directly settles the canonical full-support member of Erdős #257 for every integer base b >= 2, while leaving universal arbitrary-support irrationality open.
   • Source. Erdos249257.ExternalVerification.irrational_erdosSum_full_support in Lean
   • Boundary. This is the classical full-support theorem, not universal Erdos #257.
3. Pairwise coprime support (pairwise_coprime_support; source-ranked frontier; global rank 3; source disposition represented)
   • Why here. Direct irrationality for every infinite pairwise-coprime support with summable reciprocal mass, but not for arbitrary supports.
   • Source. Erdos249257.ExternalVerification.irrational_erdosSupportSeries_pairwise_coprime in Lean
   • Boundary. This is the pairwise-coprime support theorem, not universal Erdos #257; the infinitude, pairwise-coprimality, and summable-reciprocal hypotheses remain explicit.
4. Orthogonal petal sunflower reduction (orthogonal_petal_sunflower_reduction; source-ranked frontier; global rank 4; source disposition represented)
   • Why here. Direct irrationality under the displayed structure, but the structural predicates are not constructed for arbitrary supports.
   • Source. Erdos249257.ExternalVerification.irrational_erdosSupportSeries_of_orthogonalPetalBouquet in Lean
   • Boundary. This is a conditional reduction: the bouquet structure and uniform tail-selection predicate remain hypotheses; neither is constructed for arbitrary supports, so this does not add an unconditional Erdos #257 support family or solve the universal problem.
5. Periodic nonnegative weight irrationality (periodic_nonnegative_weight_irrationality; source-ranked frontier; global rank 5; source disposition represented)
   • Why here. Close to the Lambert-series endpoint but not a universal support theorem and not the mixed-sign statement.
   • Source. Erdos249257.ExternalVerification.irrational_ratWeightSeries_eventuallyPeriodic in Lean
   • Boundary. This is the nonnegative rational eventually-periodic coefficient theorem; its nonnegativity, eventual periodicity, and positive-tail hypotheses remain explicit, and the broader mixed-sign periodic theorem is not claimed.
6. Boolean mobius exact row dynamics (boolean_mobius_exact_row_dynamics; conditional endpoint leverage; source disposition represented)
   • Why here. The committed exact-row representative is one conditional Boolean–Möbius dynamics family: cofinal positive greedy skips yield cofinally many exact local half rows and conditional 1/2-membership, while finite rows do not supply the unproved cofinal premise.
   • Source. Erdos249257.ExternalVerification.half_mem_mersenneAchievementSet_of_positiveHalfGreedySkips in Lean
   • Boundary. CofinalPositiveHalfGreedySkips is an unproved global supply premise: for every N there must be c ≥ max N 4 with a positive greedy remainder below mersenneWeightRat c. Finite exact rows, including one produced by a skipped core, do not establish cofinality. This is a conditional 1/2-membership/counterexample route, not an unconditional Erdős #257 solution; the rank-two, endpoint-defect, and upper-half Boolean-word declarations remain subordinate evidence, and no novelty, priority, significance, or external-review claim is made.
   • Relation. reconstruction_support_for boolean_mobius_carry: The Boolean–Möbius certificate reconstructs support, while exact rows still require a cofinal skip producer.
   • Relation. conditional_producer_for half_membership_seam_classification: Cofinal positive half-greedy skips conditionally give 1/2-membership, which the seam iff classifies as unbounded terminal-false/upper-or-middle supply; finite exact rows supply neither cofinal premise.
7. Half membership seam classification (half_membership_seam_classification; source-ranked frontier; global rank 12; source disposition represented)
   • Why here. It classifies the concrete #257 half-membership endpoint exactly, closer to a usable target than an analytic recovery criterion or source-only certificate normal form, but supplies no occurrence witness.
   • Source. Erdos249257.ExternalVerification.half_mem_mersenneAchievementSet_iff_unboundedTerminalFalse in Lean
   • Boundary. This exact endpoint-socket classification does not supply any unbounded terminal-false or upper-or-middle occurrences, cofinal supply, skipped-support producer, or half-membership witness; finite exact rows do not establish the required global supply. It is not an unconditional or universal Erdős #257 result, and no novelty, priority, significance, or external-review claim is made.
   • Relation. conditional_producer_for boolean_mobius_exact_row_dynamics: Cofinal positive half-greedy skips conditionally give 1/2-membership, which the seam iff classifies as unbounded terminal-false/upper-or-middle supply; finite exact rows supply neither cofinal premise.
8. Shifted odd tail state (shifted_odd_tail_state; conditional endpoint leverage; source disposition represented)
   • Why here. It extracts a modular tail state only from explicit rational-support hypotheses and therefore does not exclude rational infinite supports.
   • Source. Erdos249257.ExternalVerification.exists_shifted_odd_tail_nat_states_of_support_fraction in Lean
   • Boundary. The state-extraction theorem does not exclude rational infinite supports or settle universal Erdős #257; the support and rational-value hypotheses remain explicit.
9. Separated cut algebraic lambert transcendence (separated_cut_algebraic_lambert_transcendence; deep mechanism and classification; source disposition represented)
   • Why here. The ordinary proof transfers algebraic-base transcendence through a separated-cut host and an explicit non-chain example, while full support at 3/2 and unrestricted base-two supports remain open; finite Lean cut lemmas are not its infinite proof.
   • Source authority. Canonical review family separated_cut_algebraic_lambert_transcendence in claims
   • Boundary. The full support at 3/2 and arbitrary infinite supports at base two remain unresolved. Finite cut arithmetic is not a proof of transcendence.
10. Boolean mobius carry (boolean_mobius_carry; deep mechanism and classification; source disposition represented)

• Why here. The committed representative preserves the existence-level quotient certificate, Boolean Möbius support reconstruction, positivity, and square-root bound; it supplies no universal irrationality contradiction or actual-recurrence producer.
• Source. Erdos249257.ExternalVerification.exists_normalized_support_fraction_iff_exists_booleanMobiusCarry in Lean
• Boundary. The equivalence is stated at the existence level with q > 0, 0 ∉ A, and a positive support witness; it gives no contradiction, no universal Erdős #257 irrationality result, and no producer of cofinally nonintegral shifts for the actual recurrence. The generic tempered-orbit theorem and the reciprocal-mass, unbounded-tail, and zero-window results are subordinate consequences, not separate families; the zero-window constant depends on the support and numerator and is not uniform. This does not settle every infinite support, and no novelty, priority, significance, external-review, or unrestricted #257 endpoint claim is made.
• Relation. reconstruction_support_for boolean_mobius_exact_row_dynamics: The Boolean–Möbius certificate reconstructs support, while exact rows still require a cofinal skip producer.

11. Achievement set geometry (achievement_set_geometry; deep mechanism and classification; source disposition represented)

• Why here. The full-measure achievement-set theorem is consequential geometry, but it does not classify rational points or settle infinite-support irrationality.
• Source. Erdos249257.ExternalVerification.volume_mersenneAchievementSet in Lean
• Boundary. Geometry of the full set does not decide irrationality of every coded point.

12. Restricted achievement sets (restricted_achievement_sets; deep mechanism and classification; source disposition represented)

• Why here. The restricted-set measure dichotomy is structurally useful but does not classify rational values or prove universal irrationality.
• Source. Erdos249257.ExternalVerification.volume_supportedMersenneAchievementSet_dichotomy in Lean
• Boundary. The measure dichotomy does not classify rational points.

13. Half and twenty one frontiers (half_and_twenty_one_frontiers; natural friction and no-go; source disposition subordinate)

• Why here. Sharp local 2-adic band arithmetic excludes small odd numerators under stated hypotheses, but does not decide reachability or half-membership.
• Source. Erdos249257.ExternalVerification.seven_le_of_intBand_odd in Lean
• Boundary. Neither membership question is decided; the 2-adic bound is sharp locally, and the two countermodel routes require unconstructed terminal-scaled or cofinal-cylinder antecedents.

14. Composite dilation defect identity (composite_dilation_defect_identity; supporting and long tail; source disposition represented)

• Why here. The exact composite-dilation defect exposes a real obstruction, but it supplies neither a tail selector nor an unconditional irrationality result.
• Source. Erdos249257.ExternalVerification.supportCoeff_mul_eq_add_defect in Lean
• Boundary. The exact defect is not bounded for arbitrary supports and supplies no tail selector or irrationality theorem; the bouquet budget remains conditional on its structural hypotheses.

15. Finite period noncollapse (finite_period_noncollapse; supporting and long tail; source disposition represented)

• Why here. The finite-period order interface is exact denominator infrastructure, but finite support cannot decide an infinite-support sum.
• Source. Erdos249257.ExternalVerification.finite_period_noncollapse_rat_den_interface in Lean
• Boundary. A finite-support denominator theorem does not settle an infinite-support sum.

## #269: Three-prime running least common multiples

Question. For a finite set of at least two primes, is the sum of reciprocals of the running least common multiples of the smooth numbers irrational? This library treats the three-prime case.

Checked frontier. 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.

Open boundary. Irrationality of the repeated sum, or transcendence, in any three-prime case.

Read. Programme paper · Lean source

First-contact mathematical order

This is Palomar’s source-current reader order, not review-matrix or Comparator roster order. Ranked results lead; conditional endpoint leverage, deep mechanisms, natural friction, and supporting rows follow unequally.

1. Conditional carry escape (conditional_carry_escape; conditional endpoint leverage; source disposition subordinate)
   • Why here. Below the #251 small-mismatch route because the source-specific cofinal escape remains unproved, but above medium finite #269 machinery because the exact residue-window contradiction is the endpoint consumer that such machinery must feed. The actual-series reduction is given.
   • Source. Erdos249257.ExternalVerification.no_positive_reducedCarry_of_cofinalLocalWindowEscape in Lean
   • Boundary. The representative assumes b,m : ℕ → ℕ, shortBound : ℕ → ℕ → ℕ, CofinalLocalWindowEscape b m shortBound, and for each positive B coprime to 30 a positive integer-valued d with d(n+1) = (b n : ℤ) d(n) − (B : ℤ) (m n : ℤ) and Int.natAbs (d n) ≤ shortBound B n; it then gives False. The absorbed-carry bridge additionally assumes smoothFactor ≠ 0, c n = smoothFactor * d n, and the corresponding exact absorbed recurrence, then cancels that factor to the same reduced consumer. The representative remains a conditional consumer for arbitrary words. For the actual three-prime word, the rationality-to-reduced-carry bridge is established separately; the source-specific cofinal escape producer is not proved. This is not a #269 endpoint or irrationality proof, and no actual-series identification, novelty, priority, significance, or external-review claim is made. It is one conditional window-carry family, distinct from the finite residue, rank-two, and weighted-phase observer families.
   • Relation. mechanism_support_for weighted_phase_carry_observer: The residue/coboundary split exposes finite carry data but does not supply the cofinal escape.
   • Relation. contrary_evidence_for rank_two_kernel_no_go: The finite kernel is not rank one, ruling out a tempting separable shortcut without producing carry escape.
2. Weighted phase carry observer (weighted_phase_carry_observer; deep mechanism and classification; source disposition represented)
   • Why here. The exact residue-digit/coboundary decomposition is the committed representative of the weighted-phase observer family; it does not transport the separate finite-dimensional factorization or imply the #269 endpoint.
   • Source. Erdos249257.ExternalVerification.carry_eq_residueDigit_add_coboundary in Lean
   • Boundary. The recurrence supplies a finite residue coordinate but leaves an uncontrolled integral quotient coboundary; it proves neither a finite-state quotient nor a literal infinite realised span. Finite realised span requires an explicit factorisation through a finite-dimensional function-faithful observer, and scalar evaluation alone is insufficient. No irrationality conclusion follows from this observer alone. The actual rationality-to-positive-reduced-carry bridge is established separately; cofinal local-window escape remains open.
   • Relation. mechanism_support_for conditional_carry_escape: The residue/coboundary split exposes finite carry data but does not supply the cofinal escape.
3. Rank two kernel no go (rank_two_kernel_no_go; natural friction and no-go; source disposition rejected)
   • Why here. A checked minor obstruction rules out rank one in a displayed finite kernel, but failure of rank one does not imply irrationality.
   • Source. Erdos249257.ExternalVerification.kernel_235_minor_eq_neg_one_fifteen in Lean
   • Boundary. Failure of rank one does not itself imply irrationality.
   • Relation. contrary_evidence_for conditional_carry_escape: The finite kernel is not rank one, ruling out a tempting separable shortcut without producing carry escape.
4. Height fibre and shell (height_fibre_and_shell; deep mechanism and classification; source disposition represented)
   • Why here. The finite height-fibre normal form and smooth-shell bound are substantive three-prime structure, but they do not produce the source-specific cofinal escape. The actual-series reduction is given separately.
   • Source authority. Canonical review family height_fibre_and_shell in claims
   • Boundary. These fibre bounds are counting input, not an escape producer. The separate actual-series divisibility bridge is established.
5. Independent clock channel relations (independent_clock_channel_relations; deep mechanism and classification; source disposition represented)
   • Why here. The ordinary proof classifies rational relations for independent clock channels by a swap-and-lattice mechanism, but it does not establish the needed independence for the original running-LCM rates or its endpoint.
   • Source authority. Canonical review family independent_clock_channel_relations in claims
   • Boundary. No rational independence of the original reciprocal prime logarithms is assumed or proved; the repeated running-LCM endpoint remains open.
6. Dyadic block alphabet (dyadic_block_alphabet; supporting and long tail; source disposition represented)
   • Why here. The exact four-symbol block alphabet is a useful finite interface, subordinate to the carry consumer, weighted observer, and rank obstruction.
   • Source authority. Canonical review family dyadic_block_alphabet in claims
   • Boundary. The finite alphabet does not supply the needed carry escape.
7. Three prime lcm cells (three_prime_lcm_cells; supporting and long tail; source disposition represented)
   • Why here. The smooth-prefix LCM identity is exact three-prime structure, but it does not supply the missing irrationality bridge.
   • Source. Erdos249257.ExternalVerification.smoothPrefixLcm_eq_threePrimeHeight in Lean
   • Boundary. Cell structure alone does not prove irrationality.

## #1041: Short connections inside polynomial lemniscates

Question. Must two roots of a monic polynomial in the open unit disc be joined by a sub-two-length curve inside its unit lemniscate? Ani’s degree-seven example refutes the exact Formal Conjectures statement; correspondence with the 1958 wording awaits human review.

Checked frontier. For ani’s degree-seven polynomial, every preconnected strict-lemniscate set containing two distinct roots has one-dimensional Hausdorff measure above two. Lean refutes the exact Formal Conjectures path-image claim and checks a separate total-variation bound.

Open boundary. The full small-parameter family reported by ani; only one explicit polynomial is formalised.

Read. Programme paper · Lean source

First-contact mathematical order

This is Palomar’s source-current reader order, not review-matrix or Comparator roster order. Ranked results lead; conditional endpoint leverage, deep mechanisms, natural friction, and supporting rows follow unequally.

1. Newton value decay (newton_value_decay; deep mechanism and classification; source disposition represented)
   • Why here. The Newton value equation and exponential first integral are the load-bearing local mechanism, while metric gluing to a short curve remains open.
   • Source. Erdos249257.ExternalVerification.exists_two_roots_dist_sum_le_two_mul_geomMean in Lean
   • Boundary. The cited declarations are pointwise derivative statements. The real-time first integral requires the paper’s interval integration step, and value decay alone does not construct a global trajectory or give a short connecting curve.
   • Relation. mechanism_support_for ray_separation: The exponential first integral confines a Newton trajectory to one value ray, yielding the separation obstruction.
2. Ray separation (ray_separation; natural friction and no-go; source disposition represented)
   • Why here. Distinct value rays exactly obstruct finite Newton connections, a consequential route boundary but not the global lemniscate theorem.
   • Source authority. Canonical review family ray_separation in claims
   • Boundary. The finite-trajectory conclusion retains continuity on the closed interval, differentiability and noncritical Newton evolution on its interior, and the ordinary endpoint passage. It supplies neither global trajectory existence nor geometric length control.
   • Relation. mechanism_support_for newton_value_decay: The exponential first integral confines a Newton trajectory to one value ray, yielding the separation obstruction.
   • Relation. supports_without_closing translation_avoidance: Ray separation motivates avoiding collision lines, but global topology and metric gluing remain open.
3. Translation avoidance (translation_avoidance; supporting and long tail; source disposition represented)
   • Why here. Finite translation avoidance is a useful #1041 input, yet it does not provide the global gluing needed by the target route.
   • Source. Erdos249257.ExternalVerification.exists_small_translation_separating_arguments in Lean
   • Boundary. The finite-family avoidance theorem does not perform the global topology or metric gluing.
   • Relation. supports_without_closing ray_separation: Ray separation motivates avoiding collision lines, but global topology and metric gluing remain open.
4. Root retention (root_retention; supporting and long tail; source disposition represented)
   • Why here. Root retention under small perturbation is an exact local input, not a complete stationarity or minimax conclusion.
   • Source. Erdos249257.ExternalVerification.constant_perturbation_roots_in_unitDisk in Lean
   • Boundary. Root retention is one input to a still-incomplete route.

## #1049: Lambert-type series at rational bases

Question. For which rational bases is the corresponding series irrational? The first resistant explicit base is three halves.

Checked frontier. Lean checks irrationality and the stated irrationality-exponent bound for rational bases in the exact Zudilin contour region, including every positive integral power of 31/4. The contour excludes 3/2.

Open boundary. The universal rational-base conjecture, including the case 3/2, remains open. The checked 31/4 power family settles one region and leaves that conjecture untouched.

Read. Programme paper · Lean source

First-contact mathematical order

This is Palomar’s source-current reader order, not review-matrix or Comparator roster order. Ranked results lead; conditional endpoint leverage, deep mechanisms, natural friction, and supporting rows follow unequally.

1. Rational base tail recurrence (rational_base_tail_recurrence; deep mechanism and classification; source disposition represented)
   • Why here. The cleared-tail recurrence is exact rational-base infrastructure, but no contradiction or irrationality consequence is derived.
   • Source. Erdos249257.ExternalVerification.rationalBaseClearedTailQ_succ in Lean
   • Boundary. The recurrence is not derived from a rationality contradiction.
2. Height and pade arithmetic (height_and_pade_arithmetic; natural friction and no-go; source disposition represented)
   • Why here. The registered representative is the sharp equality characterization for the explicit rectangular two-function exponent model; it is not a universal Hermite-Padé no-go and does not produce irrationality.
   • Source. Erdos249257.ExternalVerification.rectangular_hp_threshold_eq_classical_iff in Lean
   • Boundary. This is a sharp no-go only for the explicit rectangular two-function exponent model under the stated real hypotheses; it constructs no approximating polynomials or remainders and is not a universal Padé or Hermite-Padé no-go. It proves no irrationality at 3/2 or any general rational-base endpoint, and the analytic remainder/nonvanishing input remains untreated. No novelty, priority, significance, external-review, or endpoint claim is made; Erdős #1049 remains open.
   • Relation. stronger_natural_friction_than coordinatewise_corridor_no_go: The sharp rectangular threshold analysis carries deeper model-specific information than the coordinatewise transfer obstruction, while neither proves the endpoint.
3. Coordinatewise corridor no go (coordinatewise_corridor_no_go; natural friction and no-go; source disposition rejected)
   • Why here. It excludes one coordinatewise corridor architecture at base 3/2 and proves no irrationality statement.
   • Source. Erdos249257.ExternalVerification.threeHalves_no_coordinatewiseCorridor in Lean
   • Boundary. This excludes one proof architecture and proves no irrationality statement.
   • Relation. stronger_natural_friction_than height_and_pade_arithmetic: The sharp rectangular threshold analysis carries deeper model-specific information than the coordinatewise transfer obstruction, while neither proves the endpoint.
4. Calibrated rational hankel countermodel (calibrated_rational_hankel_countermodel; natural friction and no-go; source disposition represented)
   • Why here. The ordinary positive-moment countermodel blocks inference from an all-rank Hankel signature alone; these are not Zudilin’s moments, and neither F(3/2) nor the actual arithmetic input is settled.
   • Source authority. Canonical review family calibrated_rational_hankel_countermodel in claims
   • Boundary. These are not Zudilin’s actual moments. They refute an inference from the shared signature alone; they do not settle F(3/2) or refute the attributed divisibility-based criterion.