[ejgallego]

This PR proves that successful production assembly preserves exact statement/proof snapshot membership and that Node.leanDecls contains exactly selected associations or declarations of the accepted payload node. A shared executable name check discharges the erasure-stability premise for both local registration and import replay, rather than assuming Lean producers always supply stable names.

• Prove canonical union, uniqueness, and presence for the production indexed snapshot merge; reuse one fold-membership principle for both facets.
• Reject selected references whose once-erased canonical key changes on a second erasure, including missing references. Preserve complete evidence and existing payload, collision, and priority diagnostic precedence.
• Prove checker exactness, successful-assembly stability, and the revised acceptance contract. Assembly membership theorems no longer require a caller-supplied naming premise.
• Exercise real attribute and statement/proof directive producers, atomic malformed local rejection, malformed imported evidence retention and no resurrection, and collision precedence.
• Build the laws and print dependencies in CI. This verifies checked acceptance, not arbitrary Lean name-resolution APIs; broader payload-frame, environment/index coherence, and completion-status proofs remain separate.