Repair Coq + Agda formal verification so it actually checks (axiom-free) - #48

Merged

hyperpolymath merged 4 commits into

mainfrom

fix/coq-mechanization-axiom-free

Jun 15, 2026

Commits on Jun 15, 2026

fix(formal/coq): repair Coq mechanization so the safety core actually checks

hyperpolymath
and
claude
committed
8afc849
feat(formal/coq): discharge totality — Coq formalization now fully proved

hyperpolymath
and
claude
committed
174ecfd
fix(formal/agda): make the intrinsic-typing formalization check under --safe --without-K

hyperpolymath
and
claude
committed
7fa39cd
merge: resolve conflicts in Agda formalization
hyperpolymath
committed
de2bd25