Source map

Bounded reader route

Start from one mathematical question rather than decoding the complete import graph:

1. Read docs/orientation.json, or its human projection docs/ORIENTATION.md, and select one programme, claim, or exact remaining open proposition.
2. Run one bounded lookup: python3 scripts/query_corpus.py --route <programme_id>, python3 scripts/query_corpus.py --claim <claim_id>, or python3 scripts/query_corpus.py --open <remaining_open.id>.
3. Follow the returned paper label into the authored exposition and its declaration or source handles into the modules grouped below.
4. Read Erdos249257.lean or ErdosProblems.lean only when package topology itself is the question. Those root files now live under lean/. Read docs/reference/WAVE_INDEX.md for chronology, not as the recommended mathematical reading order.

Lean source checked by the pinned Lean kernel is proof authority. This map is authored navigation: it does not strengthen a claim, replace docs/claims.json, or close an exact remaining-open proposition. Erdős #249 and the universal form of #257 remain open.

Source result and Comparator spines

Use the repository-local result selection record for two related reading orders. It records a possible Palomar submission, not an external service decision, claim count, or proof authority. Its source_result_spine leads with the checked finite-prime weighted #257 irrationality criterion, then the formalised Zudilin-region #1049 irrationality theorem (including powers of 31/4), then ani’s degree-seven #1041 counterexample to the exact Formal Conjectures path-image statement. Universal arbitrary-support #257 and rational-base #1049 remain open; correspondence between the #1041 formal statement and the 1958 wording awaits independent human review. The separate candidate_ranking orders Comparator-qualified declarations. The generated verification dossier expands that Comparator spine with exact declarations, mechanisms, and boundaries. These selections are navigation and appraisal, not proof authority or novelty judgements; docs/claims.json and the named Lean sources own the exact claims. Support lemmas and conditional producers stay subordinate.

#1041 / source-current frontier

The current #1041 paper covers the exact Formal Conjectures path-image Hausdorff refutation using ani’s degree-seven polynomial, a separate total-variation counterexample, and Newton-flow results. HausdorffLength is the Lean source for the path-image statement; CatalogueAdapter is the source entry for ani_degree_seven_total_variation_counterexample. docs/claims.json records the exact statements and attribution. Independent review of correspondence with the 1958 wording remains outstanding. For the separate source-only research corpus, start with the dated frontier delta, then use the strongest-result map and the corpus manifest. The frontier delta is the authority for rows refuted after the activation map was generated; do not rebuild those rows merely because they remain in the machine map.

The high-signal reading routes are:

• hub selection and generic closure → GenericSufficiencyClosure: the surviving parent carrier is $\underset{c}{min}L(c)\le 2$ on the ray-separated locus, followed by lower-semicontinuity closure.
• quantitative Fekete stability and radial/angular reduction → degree-five sharpened cuts: the new tools localise the residual, but do not prove the degree-five or unrestricted theorem.
• partial-cluster perimeter identity → tied-fibre moment hierarchy: these are exact geometric/algebraic premises for future selection work, not a completed compatible-root selector.
• new exterior-root product covering and separatrix aggregate reduction: read their explicit hypotheses and refutations before treating either as a parent route.

The current paper links its statements to their Lean declarations. The separate research corpus is not part of docs/claims.json’s reviewed claim authority: its files preserve source-level premises, computations, no-go results, and open boundaries. The exact Formal Conjectures path-image statement is refuted; the historical wording has not been independently adjudicated. The separate research corpus still records open geometric continuations in FRONTIER.md, which must be read before new proof search.

Complete eight-problem return matrix

The per-problem machine index lists module entry points, papers and open obligations. The problem library expands each programme into its papers and transitive Lean source map. Expand each row’s what_is_checked and what_is_not_checked fields before treating one source entry as the whole result inventory: they are the evidence ceiling, not additional claims. This single matrix makes the same route bidirectional: start at a public problem id, reach source entry points and the paper record, then use the exact index handles to resume the open boundary; a paper or source reader can return with the --route command in the second column. Use claim_registration.registered_claim_ids to reach each registered statement’s status and declarations in docs/claims.json. The module or library containing a statement does not determine its review status. Unlisted declarations acquire no public claim status from their neighbours. For #249 and #257, follow the reviewed core routes as well as the problem-owned index.

The exact open boundary each row stops at, as machine handles. A five-column table put these sentences 354px past the rendered column, so they read here:

• #68 — weighted_collision_and_complementary_residue; cofinal_prime_power_amplification; cofinal_lower_endpoint_escape; cofinal_doubled_prime_branch_failure; cramer_residual_nonintegrality
• #243 — unbounded_negative_excursions; derive_negative_part_bound; formalise_the_published_criteria
• #249 — Index: strict_prime_tail_orbit_gap; hankel_denominator_fan_in; euler_sieve_limit_theorem; prime_ray_resultant_supply; stern_brocot_arithmetic_bridge. Family: totient_coprimality_probability; squared_lambert_gcd_moments; stern_brocot_cylinder_law; stern_brocot_run_fibonacci_stability. Reviewed: remaining_open.erdos_249_irrationality; remaining_open.unbounded_certificate_supply
• #251 — prime_gap_cofinal_shift_escape; cofinal_adjacent_small_mismatch. Under a rationality witness, the actual infinite-tail identification is proved in PrimeGapDyadicTail.lean; the cofinal escape and small-shift supplies remain open.
• #257 — Index: arithmetic_rigidity_for_thin_supports; formalise_measure_and_stride_geometry. Reviewed: remaining_open.half_value_membership; remaining_open.twenty_one_permanent_affine_supercapacity; remaining_open.universal_257_all_infinite_supports
• #269 — actual_local_window_residue_escape; nonstationary_analytic_theorem; unbounded_height_certificate. The actual rationality-to-reduced-carry bridge is proved in RationalityCarryBridge.lean; the actual cofinal escape producer remains open.
• #1041 — historical_curve_length_correspondence; repair_or_refute_saddle_block; compact_ray_cut_strip_decomposition; corrected_metric_gluing_for_restricted_families; two_stage_stable_perturbation; relative_global_newton_flow_theorem
• #1049 — three_halves_growing_rank_endpoint_jet_kernel

From a reviewed route, use the registered claim or paper-anchor query to travel back to exact Lean declarations; use the open query for the registered unresolved boundary rather than treating a checked special case as a solution:

python3 scripts/query_corpus.py --claim <claim_id>
python3 scripts/query_corpus.py --paper-anchor <TeX_label_or_source_ref>
python3 scripts/query_corpus.py --open <remaining_open.id>

Build entrypoint

• Erdos249257.lean
• ErdosProblems.lean
• Lake package: erdos249257
• Lean libraries / stable root imports: Erdos249257, ErdosProblems

Erdos249257 is the reviewed #249/#257 corpus. ErdosProblems is the problem-owned expansion surface; unregistered declarations there remain exact Lean propositions rather than reviewed public mathematical claims.

#257 / Erdős–Borwein families

• Erdos249257.CertificateKernel
• Relevant declarations include: irrational_erdosSum_full_support, irrational_erdosBorwein_series, irrational_erdosSum_factorial_support, irrational_erdosSum_two_pow_support, and irrational_erdosSupportSeries_eventuallyPeriodic.

Periodic weighted Lambert series

• Erdos249257.CertificateKernel
• Nonnegative weights: irrational_weightedErdosSeries_periodic, irrational_weightedErdosSeries_eventuallyPeriodic, and irrational_ratWeightSeries_eventuallyPeriodic.
• Signed weights: irrational_or_bpow_mul_eq_intCast_intWeightedErdosSeries_periodic gives the irrational-or-base-terminating dichotomy, while irrational_intWeightedErdosSeries_periodic_of_bpow_mul_ne_intCast consumes an explicit nontermination hypothesis.
• intWeightedCoeff_periodFourSignWeight_eq_zero_of_mod_four_eq_three is the residue-selection obstruction explaining why the signed endpoint is not unconditional irrationality.

#249 / totient denominator exclusions

• Erdos249257.GapFareyBound

• Erdos249257.CertificateKernel

• Visible-coprime lattice mass (totient_visible_coprime_lattice_mass) — tsum_pos_coprime_inv_mersenne_eq_one proves that the positive coprime Mersenne weights on the visible lattice sum exactly to one. This is the rational normalization behind the fair-coin coprimality form of #249, not an irrationality result. Follow the individual-paper explanation or the reviewed claim route python3 scripts/query_corpus.py --claim stern_brocot_cylinder_law; both expose the explanation and reverse source links. The exact boundary is unchanged: this identity does not settle #249.

• All-base totient-kernel reduction, spanning, and conditional rank (all_base_totient_kernel_index_reduction) — TotientKernelConditional.lean gives the unconditional canonical spanning theorem, while finrank_allBaseTotientKernelThroughLevelFamily_eq_of_linearIndependent gives rank $k^e+1$ only under the explicit linear-independence hypothesis. That independence, and Martin’s external positive-density theorem, are not formalised here; this algebraic boundary does not prove irrationality of #249. Retrieve the full claim/source record with python3 scripts/query_corpus.py --claim all_base_totient_kernel_index_reduction, then return to the open problem with python3 scripts/query_corpus.py --route erdos_249.

• Prime-ray cyclotomic support escape (prime_ray_resultant_supply) — PrimeRayCyclotomicCurvature.lean turns bounded-degree order divisibility and eventual nontrivial clean layers into finite-support escape and cofinal unbounded prime divisors. Its bounded order is an existence of an exponent witness, not exact order. The actual totient layer/resultant bridge and the route from unbounded prime support to certificate or carry escape remain open; the Mersenne-only instantiation in CyclotomicAnchoredKill.lean:33-105 does not close #249 or justify novelty.

• Tail-orbit phase-density and natural-prime strict-gap reductions (strict_prime_tail_orbit_gap) — TotientStrictPrimeEscape.lean makes the two producer interfaces explicit: an $11/100$ nonpositive-phase density on arbitrarily late dyadic blocks implies an $89/100$ first-harmonic block saving, while the natural-prime strict-gap predicate gives a pointwise $9/10$ pivot escape through the wrapper Erdos249257.ExternalVerification.irrational_totient_series_of_naturalPrimeTailOrbitStrictGap. The same module records the exact phase update tailOrbitFirstExp_succ: after the integer carry disappears under exponentiation, the first phase evolves by squaring. This is orbit-mechanism evidence only; it supplies none of the density, cofinal prime strict-gap, or uniform-margin hypotheses. The density, cofinal prime strict-gap, and positive truncation-margin producers are unproved for the actual totient orbit. This is conditional certificate/irrationality reduction only: it does not close #249, duplicate the finite first_harmonic_pivot_decomposition or actual_lcm_orbit_separation families, or justify novelty, priority, significance, or external review.

#249 / certificate reductions

• Erdos249257.TotientTailPeriodKiller
• Erdos249257.CarrySurvivorExtinction
• Erdos249257.LcmDiagonalReduction
• Erdos249257.LcmConeFlatness
• Erdos249257.LcmConeNonflat

Supporting ladder modules:

• Erdos249257.MersenneLambertLadder
• Erdos249257.GeometricCoprimality
• Erdos249257.GcdMomentCalculus

#249 / diagonal pincer frontier

Read this band after the certificate reductions above. It sharpens the same open obligation; it does not prove the required unbounded supply.

• Erdos249257.DiagonalPincerDecomposition — exact full-target interval characterisation and the target-avoidance-to-irrationality reduction.
• Erdos249257.SquaredMersenneDiagonalEnclosure — Lambert-projected centre, exact signed square tail, and a sharp separation criterion.
• Erdos249257.DiagonalFreshLossBridge — exact fresh-loss projection and stronger adjacent-suffix supply interfaces.
• Erdos249257.DiagonalPincerCertificates and Erdos249257.DiagonalPincerCertificatesT*, followed by ErdosProblems.Lift and ErdosProblems.Skip — the finite diagonal segment supplies a checked working depth for every natural $t\le 82$; it supplies nothing at $t=83$. This is finite source extraction, not a cofinal or asymptotic result.
• Erdos249257.DiagonalPincerPrimeCertificates.* — finite prime certificate shards used by that assembled segment; read the aggregators first.

Algebraic support for the same band:

• MersenneShadowCyclotomicNoncollapse → MersenneShadowDenominatorGrowth
• RadicalMobiusShadow → RepunitMobiusNumerator → CyclicTensorMobiusShadow
• CyclotomicProjectionOfShadow → PrimePowerJumpDynamics
• RationalDenominatorSurvival, LambertDiagonalEnclosure, and FullTargetPrimeAdjunctionNoGo

Exploratory exact interfaces with explicit conditional boundaries live in PrimitiveRationalGapSupply, PrimitiveSupportBridge, ActualForeignResidueProjection, SternBrocotRunGeometry, and SupportDilationDifferences.

Binary-carry trunk (post-wave carry layer)

Builds on Erdos249257.CertificateKernel; not part of the wave chronology. Reading order: GenericTailOrbitRigidity → GreedyAchievementSet → CampbellShiftSynchronization → BooleanMobiusCarry → RationalSupportCarrySkeleton → DyadicPrefixCompression → SublogDivisorCoverage.

• Erdos249257.GenericTailOrbitRigidity

• Relevant declarations include: temperedBinaryOrbit_eq_scaledTail, binaryCoeffSeries_rational_iff_exists_temperedBinaryOrbit, balancedPulse_fanout_unbounded, balancedPulse_no_autonomous_decoder

• Erdos249257.GreedyAchievementSet

• Relevant declarations include: volume_mersenneAchievementSet, perfect_mersenneAchievementSet, isNowhereDense_mersenneAchievementSet, mem_mersenneAchievementSet_iff_greedy_survival, certifiedGreedyMersenneDeath_not_mem, three_fourths_not_mem_mersenneAchievementSet, rational_member_support_bit_iff, half_mem_mersenneAchievementSet_of_prefixForcingChain (conditional interface only)

• Erdos249257.CampbellShiftSynchronization

• Relevant declarations include: campbellQuarterExponent_periodFreeze_noSync, campbellPhaseFreeze_parameters_impossible, shiftWindowZero_iff_greedyMersenneSkippedSupport_infinite, and shiftWindowZero_iff_half_mem_mersenneAchievementSet. These are a synchronization no-go and an exact endpoint re-expression, not an independent half-membership producer.

• Erdos249257.BooleanMobiusCarry

• Relevant declarations include: erdosSupportSeries_rational_iff_exists_temperedCarry, support_fraction_iff_exists_temperedCarry, exists_normalized_support_fraction_iff_exists_booleanMobiusCarry, mobius_carryQuotient_recovers_support, support_half_iff_affineBinaryOrbit_tempered

• Erdos249257.RationalSupportCarrySkeleton

• Relevant declarations include: sum_doublingResidue_eq_mul_wrapCount, one_div_oddOrder_le_reciprocalMass_of_support_fraction, reciprocalMass_eq_residueMean_add_excessMean, dyadic_support_fraction_reciprocalMass_diverges_or_gt_one, exists_unbounded_shifted_odd_tail_nat_state_of_support_fraction

• Erdos249257.DyadicPrefixCompression

• This is #257 support, not part of the #249 diagonal band. It gives exact finite-fragment dyadic compression inside a hypothetical dyadic-rational support value, reduced/raw block-safety coordinates, primitive-lattice and support-tail-gap equivalences, conditional half-membership consumers, and checked failures of naive induction. Start with finiteFragment_dyadicPrefixCompression, halfGreedyThreeDepthTakeRunExcessBound_iff_skippedExcessBound, greedyHalf_badSkipCapViolation_iff_primitiveLattice, halfGreedyPrefixSupportTailGap_eq_excess_div_denominator, and unsafeSkipGcdOvershootSupply_iff_primitive. No cofinal witness supply is proved.

• Erdos249257.SublogDivisorCoverage

• Relevant declarations include: supportCoeffZeroWindow_length_le_eps_logb_add

Half-value finite-prefix and boundary analysis

This band studies the test value $1/2$ in ordinary finite-prefix language. A greedy prefix is the first $n$ include/skip decisions. A seam is a pair of finite words whose values bracket $1/2$. A cylinder is the set of infinite extensions of one fixed prefix. A producer is an unproved hypothesis that supplies the required seams or return configurations arbitrarily far out.

Read the band in four layers:

1. GreedyAchievementSet → HalfCutLocator defines the achievement set, greedy coding, and the finite cut around $1/2$.
2. HalfCarryReachability → HalfCylinderFiniteShadow translates finite prefixes into integer carry and finite-shadow coordinates.
3. HalfCylinderIntegerGreedy → HalfCylinderConcreteSeamAdapter → HalfCylinderFullShellSeamBridge → HalfCylinderSkippedEndpointClassifier → HalfCylinderFloorErrorReset → HalfCylinderSeamLimit develops the exact boundary arithmetic and limiting seam interface.
4. HalfCylinderFatalGapRightTail → HalfCylinderHalfMembershipClassification → HalfCylinderLastProducerContradiction → HalfCylinderMiddleCarryLowerBound gives the endpoint classification, eliminates the upper and $-3$ middle cases, and isolates the remaining carry-tail inequality for $-2$ and $-1$.

The floor-error and shell modules are supporting arithmetic layers, not separate endpoint theorems. The last layer remains conditional: no producer supplying the required configurations cofinally is proved.

Claim registry

• docs/claims.json — the single owner of release identity, claim statuses, and declaration coordinates (file and line), cross-checked by scripts/check_release.py

Generated finite certificates

• Erdos249257.GeneratedCertificates
• Erdos249257.GeneratedCertificates.*

The complete import graph and every declaration are generated in docs/claims.json::machine_readable_paper.module_graph and docs/declaration_atlas.json; use those surfaces when a grouped route above is not specific enough. Current corpus counts live in the generated docs/ORIENTATION.md, not in this authored route map.