proof: add left-add expression helper bridge

[Th0rgal]

Summary

• add the constructor-specific left-operand Expr.add compositional helper bridge
• add the post-state companion bridge for left-operand Expr.add helper results
• regenerate PrintAxioms to audit the two new public lemmas

Validation

• lean-slot lake build Compiler.Proofs.HelperStepProofs
• python3 scripts/check_proof_length.py
• python3 scripts/generate_print_axioms.py
• python3 scripts/generate_print_axioms.py --check
• git diff --check
• rg -n '\bsorry\b|\badmit\b|axiom |True :=|\t' Compiler/Proofs/HelperStepProofs.lean PrintAxioms.lean

[vercel]

The latest updates on your projects. Learn more about Vercel for GitHub.

Project	Deployment	Actions	Updated (UTC)
verity	Ready	Preview, Comment	Jul 11, 2026 8:00am