Corpus v3 · Formal theorem
cid005338
FTH0076canonicalv1no_unearned_decimal_diagonal (theorem)
/-- [I.P34] No Unearned Decimal Diagonal: no extractor can have its diagonal avoid all rows. Proof: the avoidance condition diagonal(n) != extract(n, n) directly contradicts diagonal_def which says diagonal(n) = extract(n, n). This is the liar-paradox core of the diagonal argument, and tau blocks it by making diagonal extraction self-referential. -/
Formalization
lean_axiom_freesorries: 0project axioms: 0
Identifiers
Aliases & legacy IDs
no_unearned_decimal_diagonalTauLib.BookI.Sets.CantorRefutation::no_unearned_decimal_diagonalRelease lines
corpus_v2corpus_v3_workingVersion & History
Status disclaimer
A Corpus Item page reports the program's current internal record for this item. It does not imply external verification, scientific consensus, or final proof unless explicitly stated. Read it together with its dependencies, formalization status, and the program's overall stance.