Corpus orientation

Release provenance

This checkout is a deliberately curated, independently verifiable public output of a larger ongoing formal-mathematics workflow. No public claim depends on private or unreleased work.

Public evidence of that release workflow: pinned formal-source identity; claim and open-proposition registry; machine-readable argument and module graphs; generated declaration atlas; bounded cold-clone and adversarial checks.

The workflow provenance explains the release discipline; it does not imply hidden proof authority or equivalence with private work.

What a claim status asserts

A status states the exact public evidence claim, not a priority or novelty claim. The authored prior-art record, not this table, is the source for antecedents.

Exact open boundary

• remaining_open.erdos_249_irrationality — Prove that S = ∑ φ(n)/2ⁿ is irrational, with no bound on a possible rational denominator.
• remaining_open.unbounded_certificate_supply — Produce certified non-integrality witnesses at unbounded parameters. A sufficient one-parameter form is to produce them along the lcm diagonal.
• remaining_open.half_value_membership — Decide whether 1/2 lies in the Mersenne achievement set. Yes refutes universal #257; no closes only this route.
• remaining_open.twenty_one_permanent_affine_supercapacity — Decide the exact 1/21 branch: equivalently, exclude the fatal/cofinite/aligned branch, contradict its eventual permanent affine-supercapacity recurrence, prove cofinally bounded scaled greedy remainders, or force an unbounded sequence of closed canonical quotient rows. A positive membership result would refute universal #257; no such producer is proved.
• remaining_open.universal_257_all_infinite_supports — Prove irrationality for every infinite support A, not only the named support families formalised here.

Where the substance is

• Both working records close with a section titled “The wall”: every attempted argument class stopped by a stated bound, recorded with what it does not rule out.
• The mathematics paper closes with “What we need from a mathematician”: four self-contained problems; a refuted route is withdrawn and the refutation credited in the next edition.
• docs/RESULTS.md opens with a ten-minute verdict.

Scale

Navigation inventory, not results. Generated certificate shards are counted as formal source, never as separate mathematical claims.

The exhaustive declaration and import index is docs/declaration_atlas.json.

Mathematical programmes

These are reading routes through the checked corpus, not extra claims. Each route states its mathematical focus and exact public claim ceiling.

• Achievement-set geometry and the rational-target seams (erdos257_half_story)
  • Ceiling: Exact geometry and reductions for the 1/2 and 1/21 branches; neither target membership nor universal Erdős #257 is proved.
• #249 certificate and harmonic interface (erdos249_certificate_story)
  • Ceiling: The certificate formulation is exact and finite instances are checked; the unbounded certificate supply and irrationality of S remain open.
• Classical and structured support irrationality (structured_support_families)
  • Ceiling: These are structured families, coefficient classes, and a conditional bouquet reduction; arbitrary infinite supports in universal Erdős #257 remain open.
• #249 diagonal arithmetic and fresh-loss interfaces (erdos249_diagonal_arithmetic)
  • Ceiling: Each interface sharpens or re-expresses the same supply problem; no unbounded avoidance, slack, or separated-projection supply is proved.
• Boolean Möbius carry and global rationality constraints (boolean_mobius_constraints)
  • Ceiling: These are exact characterisations and necessary consequences of rationality; they do not contradict every hypothetical rational value or settle universal Erdős #257.
• Transport, curvature, phase separation, and no-go results (transport_curvature_programme)
  • Ceiling: The consumers and countermodels are exact, but no cofinal curvature, transport, phase-separation, or anti-reconstruction producer is proved.
• Mersenne–Lambert identities and obstruction interfaces (lambert_obstruction_interfaces)
  • Ceiling: These are exact identities, obstruction theorems, and one conditional rank consequence; they do not form an irrationality criterion for S.
• Coprimality probability, gcd moments, and Stern–Brocot geometry (probabilistic_gcd_geometry)
  • Ceiling: Exact identities, denominator transfer, convergence, and combinatorial stability only; no irrationality or novelty claim.
• Half-carry compactness, windows, seams, and finite propagation (half_carry_compactness_programme)
  • Ceiling: The closure implications, local propagation laws, and bounded stages are exact; no cofinal or coherent unbounded window family is proved, so neither half-membership nor universal Erdős #257 follows.
• Denominator, CRT, moment, and gauge obstructions (arithmetic_obstruction_interfaces)
  • Ceiling: These are exact arithmetic interfaces, finite mechanisms, and obstruction theorems; they do not supply an unbounded certificate family or an irrationality criterion for the totient constant.

Open one programme with python3 scripts/query_corpus.py --route <programme_route_id>. The packet returns the ordered claim handles, exact open boundary, related programmes, and source owners without loading the exhaustive graph.

Principal claim routes

Each row is only an entry handle. Read the claim statement and every attached declaration in docs/claims.json, then follow the paper label into the authored exposition. A conditional reduction or finite instance does not settle the open proposition attached to it.

The first Lean anchor of each claim, in table order, as claim id, declaration name, then source coordinate:

eb_full_support
    irrational_erdosSum_full_support
    Erdos249257/CertificateKernel.lean:8328

eb_constant
    irrational_erdosBorwein_series
    Erdos249257/CertificateKernel.lean:8335

support_families
    erdos257_family_factorial_instance
    Erdos249257/CertificateKernel.lean:6082

denominator_exclusion
    tsum_totient_div_pow_two_ne_ratCast_of_den_le_79639646646701375323355774875831053
    Erdos249257/CertificateKernel.lean:18384

certificate_reduction
    irrational_totient_series_of_certificate_supply
    Erdos249257/TotientTailPeriodKiller.lean:394

certificate_completeness
    exists_certifiedKill_iff_tail_diff_notMem_int
    Erdos249257/LcmConeFlatness.lean:316

certified_kill_instances
    certifiedKill_all_small
    Erdos249257/TotientTailPeriodKiller.lean:404

diagonal_pincer_reduction
    diagonal_int_iff_foreignDiagonalDefect_hits_fullTarget
    Erdos249257/DiagonalPincerDecomposition.lean:215

adelic_height_obstruction
    scalarLocalization_complement_dvd
    Erdos249257/AdelicHeightObstruction.lean:23

all_base_totient_kernel_index_reduction
    totient_pow_mul_eq
    Erdos249257/TotientKernelReduction.lean:60

sublog_zero_windows
    supportCoeffZeroWindow_length_le_eps_logb_add
    Erdos249257/SublogDivisorCoverage.lean:392

greedy_achievement_geometry
    volume_mersenneAchievementSet
    Erdos249257/GreedyAchievementSet.lean:996

Read by intent

• Understand what this repository proves, reduces, cites, leaves open, and how its claims are partitioned. (instant_orientation): docs/orientation.json → SCOPE.md
  • Route: python3 scripts/query_corpus.py --route instant_orientation
• Navigate every committed Lean declaration and exact loaded-root dependency from a cold clone before compiling, then open a receipted workbench session when beginning proof work. (agent_native_corpus_navigation): docs/AGENT_WORKBENCH.md → docs/SEMANTIC_COMPILER.md → docs/semantic/lab/README.md
  • Route: python3 scripts/query_corpus.py --route agent_native_corpus_navigation
• Browse bounded claim handles by exact registry status. (browse_claim_status): docs/orientation.json → SCOPE.md
  • Route: python3 scripts/query_corpus.py --route browse_claim_status
• Trace one mathematical claim from exposition to checked source. (follow_one_claim): docs/orientation.json
  • Route: python3 scripts/query_corpus.py --route follow_one_claim
• See how the #249 reduction, #257 families, carry trunk, and open targets relate. (understand_argument_topology): docs/orientation.json → docs/SOURCE_MAP.md
  • Route: python3 scripts/query_corpus.py --route understand_argument_topology
• Achievement-set geometry and the rational-target seams (erdos257_half_story): docs/orientation.json
  • Intent: Follow the proved #257 achievement-set spine from unique greedy coding through the half-value seam and the exact denominator-21 fatal-branch frontier, without treating finite recurrence data as a solution.
  • Route: python3 scripts/query_corpus.py --route erdos257_half_story
• #249 certificate and harmonic interface (erdos249_certificate_story): docs/orientation.json
  • Intent: Recover the denominator exclusion, exact certificate endpoint, certificate completeness, finite checked instances, first-harmonic consumer, and the still-open unbounded supply.
  • Route: python3 scripts/query_corpus.py --route erdos249_certificate_story
• Classical and structured support irrationality (structured_support_families): docs/orientation.json
  • Intent: Follow the full-support theorem, named infinite-support families, periodic coefficient extensions, the mixed-sign dichotomy, and a conditional orthogonal-petal route.
  • Route: python3 scripts/query_corpus.py --route structured_support_families
• #249 diagonal arithmetic and fresh-loss interfaces (erdos249_diagonal_arithmetic): docs/orientation.json
  • Intent: Follow the exact lcm-diagonal pincer, fresh-loss projection, prime-deficit decomposition, odd-window, bit-lift, slack, and foreign-residue interfaces.
  • Route: python3 scripts/query_corpus.py --route erdos249_diagonal_arithmetic
• Boolean Möbius carry and global rationality constraints (boolean_mobius_constraints): docs/orientation.json
  • Intent: Follow the exact carry-orbit characterisations of rational support-series values and the reciprocal-mass, unbounded-state, and zero-window consequences they force.
  • Route: python3 scripts/query_corpus.py --route boolean_mobius_constraints
• Transport, curvature, phase separation, and no-go results (transport_curvature_programme): docs/orientation.json
  • Intent: Follow exact transport and curvature consumers, affine channel annihilation, checked finite instances, phase-separation producers, and fixed-precision countermodels.
  • Route: python3 scripts/query_corpus.py --route transport_curvature_programme
• Mersenne–Lambert identities and obstruction interfaces (lambert_obstruction_interfaces): docs/orientation.json
  • Intent: Follow the exact Lambert identities around the totient constant and the coordinate, tail-atom, sign-support, and carry-rank obstructions that rule out naive compression strategies.
  • Route: python3 scripts/query_corpus.py --route lambert_obstruction_interfaces
• Coprimality probability, gcd moments, and Stern–Brocot geometry (probabilistic_gcd_geometry): docs/orientation.json
  • Intent: Follow the fair-coin coprimality form of S and its denominator exclusion, squared-Lambert gcd moments, exact Stern–Brocot cylinder convergence, and Fibonacci/continuant stability of induced runs.
  • Route: python3 scripts/query_corpus.py --route probabilistic_gcd_geometry
• Half-carry compactness, windows, seams, and finite propagation (half_carry_compactness_programme): docs/orientation.json
  • Intent: Follow the exact compactness implications from cofinal finite half-carry witnesses to half-membership, and the rewind, seam, suffix-cylinder, and finite-stage results that isolate the missing uniform construction.
  • Route: python3 scripts/query_corpus.py --route half_carry_compactness_programme
• Denominator, CRT, moment, and gauge obstructions (arithmetic_obstruction_interfaces): docs/orientation.json
  • Intent: Follow exact arithmetic enclosures and denominator lower bounds, finite square-CRT suppression, dyadic moment and certificate interfaces, and gauge countermodels that delimit several plausible #249 routes.
  • Route: python3 scripts/query_corpus.py --route arithmetic_obstruction_interfaces
• Understand the cited mathematical sources, their precise relationship to the release, and the priority boundary. (trace_prior_art): docs/PRIOR_ART.md
  • Route: python3 scripts/query_corpus.py --route trace_prior_art
• Understand the mathematical method, the evidence required for claim transitions, and the exact remaining open propositions. (understand_methodology_and_open_boundary): METHODOLOGY.md → SCOPE.md
  • Route: python3 scripts/query_corpus.py --route understand_methodology_and_open_boundary
• Modify a formal or editorial surface without allowing status or source coordinates to drift. (change_or_verify_release): AGENTS.md → CONTRIBUTING.md
  • Route: python3 scripts/query_corpus.py --route change_or_verify_release

Drill down

• Exact statuses, statements, paper anchors, declarations, and argument edges: docs/claims.json
• Source routes by mathematical question: docs/SOURCE_MAP.md
• Development chronology: docs/WAVE_INDEX.md
• Human mathematical account: erdos249-257-main-paper.pdf
• Machine form of this page: docs/orientation.json

External corpus registration

docs/corpus_descriptor.json uses schema erdos249257-corpus-descriptor/5. The release gate keeps it below 64 KB. It carries release identities, content digests, principal claim and declaration handles, and the root module topology. Complete claims, module imports, declaration prose, methodology, both authored papers, and the paper-to-Lean source-sigil crosswalk remain in their digest-bound expansion files. These authored surfaces remain distinct from Lean proof authority.

Query one handle

The read-only query helper returns bounded JSON by default: Module packets include authored roles and both sides of the direct import neighbourhood, with truncation receipts pointing to the exhaustive graph. Claim packets resolve adjacent argument edges into labels, statuses, and relation meanings, so each neighbour can be followed as another handle. Every exact remaining-open proposition ID is itself a typed handle whose packet preserves the open target and lists linked progress claims. Claim paper labels resolve to exact TeX files and lines across both papers; declaration packets add pinned Lean URLs, module context, and attached claims.

python3 scripts/query_corpus.py --format card
python3 scripts/query_corpus.py --claim denominator_exclusion
python3 scripts/query_corpus.py --paper-label res:farey
python3 scripts/query_corpus.py --open remaining_open.unbounded_certificate_supply
python3 scripts/query_corpus.py --declaration irrational_erdosSum_full_support
python3 scripts/query_corpus.py --module Erdos249257/CertificateKernel.lean
python3 scripts/query_corpus.py --module CerKer
python3 scripts/query_corpus.py --route instant_orientation
python3 scripts/query_corpus.py --route erdos249_diagonal_arithmetic
python3 scripts/query_corpus.py --search "what remains open for 257" --limit 5