Lean Results ↔ AFP theorems

Mapping from lean/Results.lean to Lawrence C. Paulson's AFP entry Euler's Polyhedron Formula (Euler_Formula.thy), vendored under isabelle/afp-Euler_Polyhedron_Formula/.

Lean (`lean/Results.lean`)	AFP (`Euler_Formula.thy`)	Meaning
`results_euler_characteristic`	`Euler_Poincare_full`	Full-dimensional convex polytope: Euler characteristic `1`.
`results_euler_relation_dimension_three`	`Euler_relation`	Euler's formula in dimension 3: `V − E + F = 2`, from the characteristic above.

Supporting AFP substrate (hyperplane arrangements, cell complexes, Euler-char invariance) maps to Lean modules under lean/EulersGem/ — see lean/MATHLIB_SURVEY.md in the repo.

Strategies (credited)

Lineage	Approach	Role here
Paulson AFP / HOL Light (Lawrence)	Hyperplane arrangements, cell complexes, Euler-char invariance	Base (vendored); primary target for Lean
Michal Poly100 (earlier, unfinished)	Tverberg triangulation + induction on facets	Historical + alternate comparison only

Vendored AFP layout

isabelle/
  afp-Euler_Polyhedron_Formula/   # Paulson AFP (BSD)
    Euler_Formula.thy
    ROOT
    LICENSE
    SOURCE_SHA256.txt
    document/
  Poly100.thy                     # historical archive
  Poly100-notes.org
  README.md

Full notes: isabelle/README.md on GitHub.