Torus has euler characteristic zero

NOT A NOVELTY CLAIM. This is a machine-checked formalisation, decided by the Lean 4 kernel and depending on no axiom. It is dated and citable. Prior art, where it exists, is cited below. No discovery is claimed.

The torus is flat: g = 1, χ = 0 — the boundary between positive and negative curvature.

Proposition

chi 1 = 0

Proof

By decide in poincare.lean. The kernel reduces the proposition and reports no axiom dependency.

Sources and identifiers

• Lean source · src/pair/formal/proofs/poincare.lean
• Typeset paper · src/research/lean-theorems.tex
• Repository deposit · doi:10.5281/zenodo.21787144
• Author · ORCID 0009-0000-7312-9778
• Deposit record · poincare--torus_has_euler_characteristic_zero

Proved in the same file

• Chi and genus are inverse
• Sphere has euler characteristic two
• Double torus has chi minus two and rank four
• Homology rank is twice the genus

All machine-checked theorems