NAUX ↔ Coq mapping (L0 core)

Status: current pre-Core-N0 formal subset mapping

This file does not claim that accepted Core-N0 v0.1 or the full compiler is verified. The mapping must be versioned or replaced when the Core-N0 interpreter and schema become executable.

• NAUX Int / Nat ↔ tyNat (Coq TyNat in Syntax.v).
• NAUX Bool ↔ tyBool (TyBool).
• Function ↔ TAbs/TApp (TyArrow).
• let ↔ TLet.
• if ↔ TIf.
• Literals ↔ TNat n, TBool b.
• Subset modeled: L0 = lambda + let + if + nat/bool (mini core).

Commitment: Rust/NAUX semantics for this subset should align with naux-meta-coq definitions (NauxCore.*). Further constructs (pair/list/effects) to be added later. Proof artifacts live in naux-meta-coq/, not required for end users.