F13 · Effective transcendence · Planning, not proof evidence

Irrationality of (√2)^(√2)

First: ∀ a ∈ ℤ, b > 0, ∃ n : |b uₙ − a| > 2b · 2⁻ⁿ

A carefully bounded, non-LLM-first campaign: exact arithmetic, quadratic norms, finite interpolation and native HA certificates. Full transcendence is the next target, not a completed result.

Open the planned dependency mapRead the target contractLocate G121 in the grand campaign

Definitions first

Proposed mathematical notation

26 dependency-ordered definition contracts. These are proposals, not yet reviewed conservative HA abbreviations.

Inspect the definition plan →

Exact obligations

Lemma-by-lemma contracts

81 irrationality obligations, with prerequisites, induction parameters, automation methods and explicit risks. Expanded kernel formulas remain an execution gate.

Read the planned lemmas →

Focused route

Finite nonvanishing certificates

Follow the primary direct perturbation route. Solver output is a hint until native reconstruction succeeds; no Markov axiom is planned.

Trace the target's planned prerequisites →
Evidence boundary: The full irrationality endpoint is open; there are no new Alpha admissions. Current HA/Lean-checked leaves and solver results · Local conservative definition DAG · Historical pilot baseline. Planned edges are not checked proof dependencies. The existing Alpha/Stable catalogues and historical proof explorers are unchanged.
Zoom between scales: combined 122-goal planning atlas → F13 → irrationality → later transcendence. The original 120-goal snapshot is preserved; G121 and G122 are open additions.
Planning dossier: mathematics, execution waves and budgets · twelve bounded pilot contracts · machine-readable DAG and work queue · deterministic build manifest. Use the browser's print command on the map or an individual contract.