claimroutineinferred_dep

Pi is irrational

Shows π\pi is irrational: a rational value would be an exact approximation
makes approximation errors nonzero for the pigeonhole step
Claim·§4 Choice of parameters and proof of Theorem~thm:main·inside thmIrrationality exponent of pi is 2

Statement (paper)

The number π\pi is irrational: if π\pi were rational, then exact representations π=p/q\pi=p/q with arbitrarily large denominators qq (unreduced fractions, zero error) would satisfy , which has been excluded for arbitrarily large qq, a contradiction.

In plain English

The number π\pi is irrational, since a rational value π=p/q\pi=p/q would give exact approximations with arbitrarily large denominators, which the preceding argument rules out.

Why it's here

Exact representations (unreduced, with zero error) satisfy the same approximation condition that the previous claim showed cannot hold for arbitrarily large qq, so rationality leads to a contradiction. This lets the later pigeonhole step assume π\pi is irrational, so the approximation errors are nonzero.
Classified routine:
This follows directly from claim-thm-main-4: if π were rational, unreduced fractions would give exact approximations with arbitrarily large denominators, contradicting the preceding exclusion.

Uses

claimCombined error margins contradict determinant comparison

Used by

claimDirichlet pigeonhole gives lower bound exponent 2

Sources

PaperOpen
Section
§4 Choice of parameters and proof of Theorem~thm:main
Page
—
Label
—
Line
sections/conclusion.tex:136
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Exact approximations exclude rationality" rests on claim-thm-main-4