LeaTTa 0.4.0

Adds a first, work-in-progress formalization of MeTTa-IL, the MeTTa intermediate language, built from F1R3FLY's MeTTaIL repository (https://github.com/F1R3FLY-io/MeTTaIL).

It is not finished. It models the determinate core and is honest about what is open.

What is checked

• the elaborate, desugar, type-lift, and monomorphize pipeline, pinned by kernel decide against output captured from the real Scala tool on Rholang.module
• the GSLT reduction relation (soundness)
• subject reduction and confluence for SKI and the simply-typed lambda calculus
• the semantic cores of the two papers' calculi (the spice bounded-reachability rule and the mq-calculus Born-rule probability conservation)
• the MeTTa-to-GSLT bridge and the presentation lattice laws with decidable equality

Built with 0 sorry/admit/native_decide/partial/unsafe; the axiom audit shows only the three standard axioms. Full build green, MeTTa differential oracle 270/270.

What is open is listed in the README's MeTTaIL section and in MeTTaIL/SPECIFICATION.md. Formalizing the tool also surfaced five bugs in it, written up for the F1R3FLY team in MeTTaIL/HYPERON_IMPROVEMENTS.md.

The downloadable bundle below is the MeTTa minimal interpreter, unchanged in behavior from 0.3.x. The MeTTaIL work is a Lean formalization and proof library, not part of the binary.