Normalization for untyped SK combinatory logic

This project gives a dependency-free formalization of untyped SK combinatory logic and establishes that every term reduces to a normal form under the compatible closure of the standard reduction rules.

The theorem has the direct statement

public theorem everyTermHasNormalForm (term : Term) : HasNormalForm term

where HasNormalForm term is an existential normal-form claim.

The development uses impredicative presentations of logical connectives and relation closures so that the complete trusted foundation remains small and directly auditable.

Layout

• SKNormalization/Foundation.lean: minimal logical foundation;
• SKNormalization/Calculus.lean: SK terms, compatible reduction, and normal forms;
• SKNormalization/Proof.lean: internal proof of the normalization result;
• SKNormalization/Main.lean: the public normalization theorem.

Checking

The project is pinned to Lean v4.32.1.

./reproduce.sh

This performs a Lake build, warning-free frontend checks, ordinary and fresh kernel replay of the main module, and Lean's built-in #print axioms check for the theorem.