Add verified SOS1 Big-M promotion transform in Lean

[termoshtt]

Summary

• define the mixed reused/fresh selector semantics and a direction-independent canonical Big-M row specification shared by lowering and promotion
• add an untrusted suffix-layout witness and a conservative checker for promoting canonical Big-M rows into a first-class SOS1 constraint
• validate the existing source suffix directly against the shared canonical row specification, including its sense, constant, and every coefficient
• preserve existing OneHot, SOS1, and Indicator constraints when they do not reference removed selector variables
• define promotion as an Instance.Transform and prove reduction, relaxation, objective preservation, and target round-trip properties
• organize the formulation family under SOS1BigM, with separate Lowering and Promotion module trees and focused witness, target, validation, and semantics responsibilities
• add independent handwritten fixtures for accepted formulations, conservative rejection cases, noncanonical source selectors, and sequential recovery of multiple SOS1 constraints

Scope

The promotion checker intentionally supports retained variable and regular-constraint prefixes followed by fresh selector variables and canonical Big-M formulation rows. Existing OneHot and SOS1 constraints must contain only retained members; existing Indicator constraints must have a retained trigger and a body independent of fresh selectors. Rejection means the formulation is outside this sufficient-condition checker, not that no correct SOS1 promotion exists through a broader Big-M recognizer or another formulation.