ISAR

Morphism Explorer

The InvariantLayer is the terminal object in the category of admissible semantic kernels. Every dialect admits a unique structure-preserving morphism into it. ISAR.morphism_uniqueness

InvariantLayer (terminal)

Dialect (selected)

Dialect (other)

Unique morphism ! Encoding path

Select a dialect to see its factorization details.

Morphism map (all dialects)

Dialect	Lean name	Morphism theorem	Status
Lambda calculus	ISAR.compile	compile_simulates_red	proved
HF Sets (ZFC fragment)	ISAR.HF_Kernel	HF_Kernel_factorization	proved
SKI TRS	ISAR.TRS_Dialect	—	implemented
Stack Bytecode	ISAR.Bytecode_Dialect	—	implemented
Barker's Iota	ISAR.Iota_Dialect	orbit: I→A→K→S→X→I	implemented
Quantity Kernel	—	—	conjectural