Methodology

1. A formal result is the exact proposition Lean checked

A result is proved here only as the exact elaborated proposition accepted by the pinned public Lean environment under its transitive assumptions.

Seen in: Full-support Erdős–Borwein irrationality, every integer base b ≥ 2 (eb_full_support).

Limit: Kernel acceptance does not establish intended meaning, relevance, novelty, or claim status.

2. Formal validity and mathematical faithfulness are separate questions

A checked Lean declaration and the intended mathematical statement remain distinct until human mathematical review records their correspondence.

Seen in: Named infinite-support irrationality families toward #257 (support_families).

Recorded boundary: Prove irrationality for every infinite support A, not only the named support families formalised here (remaining_open.universal_257_all_infinite_supports).

Limit: The repository can require and route review; it cannot compute mathematical faithfulness.

3. A public claim crosses representations only through proved transport

A claim may move between coordinates, encodings, normalisations, or models only through a checked implication or equivalence whose direction and losses are explicit.

Seen in: The Mersenne–Lambert ladder identities (mersenne_lambert_ladder).

Recorded boundary: Prove that S = ∑ φ(n)/2ⁿ is irrational, with no bound on a possible rational denominator (remaining_open.erdos_249_irrationality).

Limit: A transport theorem establishes the stated relation; it does not establish that the new representation is useful.

4. A reduction keeps the remaining hypothesis visible

Every conditional theorem, criterion, or reduction names the exact hypothesis or quantifier that remains open.

Seen in: Exact reduction of #249 to finite decidable certificates (certificate_reduction).

Recorded boundary: Produce certified non-integrality witnesses at unbounded parameters. A sufficient one-parameter form is to produce them along the lcm diagonal (remaining_open.unbounded_certificate_supply).

Limit: An exact reduction can expose an open proposition without proving it.

5. Finite verification does not change quantifiers

Finite certificates, bounded searches, and verified initial segments remain finite evidence unless a checked theorem supplies the unbounded or universal step.

Seen in: Initial certified-kill segment and generated certificates (certified_kill_instances).

Recorded boundary: Produce certified non-integrality witnesses at unbounded parameters. A sufficient one-parameter form is to produce them along the lcm diagonal (remaining_open.unbounded_certificate_supply).

Limit: Increasing a checked bound does not change the quantifier of the public claim.

6. A claim of progress names both the theorem and the outstanding obligation

A result advances an open target only when it states which remaining open proposition it proves, narrows, decomposes, re-expresses, or constrains.

Seen in: Unconditional denominator exclusion for the totient constant (denominator_exclusion); Sublogarithmic divisor-coverage zero windows (sublog_zero_windows).

Recorded boundary: This release does not settle Erdős #249 (not_erdos_249_solution).

Limit: The repository checks that the claimed effect is explicit; human review decides whether the effect is mathematically significant.

Lean check

Decides: Whether the declaration elaborates and its proof term is accepted in the pinned environment. The associated axiom audit reports the transitive axioms the declaration depends on.

Does not decide: Whether the proposition expresses the intended mathematics, is relevant to an open problem, or is novel.

Repository check

Decides: Whether identifiers, statuses, source coordinates, routes, projections, and generated files agree.

Does not decide: Whether an informal statement is mathematically faithful or significant.

Human mathematical review

Records a reviewed judgement about: Whether a formal proposition matches the intended statement, how it relates to prior work, what public claim it supports, and what remains open.

Does not decide: Whether the Lean kernel accepts the proof term.

Blinded recovery evaluation

Decides: Whether an agent given the development as it stood before a declaration landed, and a stated subset of the derived layers, reconstructs that declaration’s statement or proof mechanism. The holdout is a git checkout predating the target, so the target is absent by construction rather than by the agent’s restraint.

Does not decide: Whether the recovered statement is novel, significant, or correctly proved; whether the mechanism credited for the recovery is the one the original proof used; or whether a recovery generalises beyond the held-out case.

Mathematical research path

open_target → representation → necessary_consequence → proved_reduction → finite_certificate → lean_declaration → remaining_open_proposition

A route may stop at any intermediate object. In particular, a necessary consequence, reduction, finite certificate, or Lean declaration does not remove the final remaining-open proposition unless a checked theorem actually does so.

Public claim path

lean_declaration → checked_assumptions → reviewed_intended_meaning → public_claim → authored_exposition → generated_projection → public_checkout

This is the authority order for publication. Kernel acceptance precedes assumption review; intended meaning is reviewed before a public claim; authored exposition precedes generated projections; and the public checkout is the final reader-facing surface.

Proving

• Under a hypothetical rational value or counterexample, derive checked structural consequences instead of replacing proof with plausibility.
• A finite checker needs a soundness theorem; calling it exact additionally requires a completeness theorem at the stated parameters.

Publishing

• Every frontier-facing partial result states both its positive conclusion and the exact proposition that survives it.
• Each representation change identifies the checked theorem that transfers the claim and states the direction and any loss.
• A reader using only the public checkout must be able to find the main argument, proof routes, public claim statuses, and remaining open propositions.
• Public claim review checks both ceilings and coverage: prose must not exceed the checked theorem chain, and a source-backed high-value mechanism, exact reformulation, quantitative reduction, or distinct endpoint must be mechanically discoverable when omitting it would materially understate the corpus.

Maintaining

• A failed strategy, counterexample, or disproved finite-state interpretation is retained when it rules out a recurring mathematical route.
• Distinguish proof-body, proposition, assumption, representation, finite-range, claim-status, exposition, and projection changes before deciding what must be updated.
• Lean owns formal validity; humans own intended meaning, significance, and public framing; agents may search, propose, test, and expose consequences without inheriting either authority.
• Update Lean source first, then assumption and meaning review, then claim status, then authored exposition, then generated projections.

An exact reduction that does not close #249

a hypothetical rational value of S = ∑ φ(n)/2ⁿ
→ an integrality constraint on totient tail differences
→ a finite non-integrality certificate at fixed parameters (certifiedKill)
→ an exact conditional reduction (irrational_totient_series_of_lcm_diagonal_certificate_supply)
→ the unbounded supply of such certificates, which remains open

If S were rational, its totient tails would satisfy an integrality constraint. The certifiedKill predicate refutes that constraint at fixed parameters, and the completeness theorem shows the finite computation loses no information at those parameters. The reduction theorem then proves: if certificates occur at unbounded parameters, S is irrational. Producing that unbounded supply is the remaining open proposition; nothing in this repository claims it.

Claims: Exact reduction of #249 to finite decidable certificates (certificate_reduction); Certificate completeness (certificate_completeness).

Remaining open: remaining_open.unbounded_certificate_supply.

Finite verification that stays finite

certifiedKill_all_small and the lcm-diagonal deposits through t = 8 (certifiedKill_periodLcm_diagonal_upto_six and the t = 7 and t = 8 endpoints) are kernel-checked with decide at fixed bounds. Each names a specific bounded region the checker has cleared; together with the generated certificate shards they show the reduction is not vacuous. The claim keeps the status verified finite instance and states its bounded domain. Raising the checked bound changes the stated bound; it does not change the quantifier of any public claim.

Claims: Initial certified-kill segment and generated certificates (certified_kill_instances).

Remaining open: remaining_open.unbounded_certificate_supply.

Necessary structure that does not yet contradict

The carry and zero-window theorems state what a rational series value would force: reciprocal-mass lower bounds, unbounded carry states, and sublogarithmic zero windows in divisor coverage. These are necessary consequences of rationality. They constrain a hypothetical rational value; none of them rules it out, and the universal #257 statement remains open.

Claims: Rationality-forced reciprocal-mass lower bound (reciprocal_mass_bound); Carry states are unbounded over infinite rational-valued supports (unbounded_carry_states); Sublogarithmic divisor-coverage zero windows (sublog_zero_windows).

Remaining open: remaining_open.universal_257_all_infinite_supports.