Shipped: Lutar-Lean: Lean 4 formalization of the trust gate

A Lean 4 + Mathlib formalization of the Λ aggregator behind SZL's trust gate: 749 declarations, 14 axioms, 163 tracked sorries, and 8 formulas locked as proven. Λ uniqueness is stated as Conjecture 1, not a theorem. RESEARCH.