Add verified SOS1 Big-M promotion transform in Lean

lean/OMMXProof.lean

@@ -14,8 +14,15 @@ import OMMXProof.Instance.Transform.IndicatorBigM.Formulation
 import OMMXProof.Instance.Transform.IndicatorBigM.Plan
 import OMMXProof.Instance.Transform.IndicatorBigM.Target
 import OMMXProof.Instance.Transform.SOS1BigM
-import OMMXProof.Instance.Transform.SOS1BigM.Basic
-import OMMXProof.Instance.Transform.SOS1BigM.Formulation
-import OMMXProof.Instance.Transform.SOS1BigM.Plan
-import OMMXProof.Instance.Transform.SOS1BigM.Target
+import OMMXProof.Instance.Transform.SOS1BigM.Lowering
+import OMMXProof.Instance.Transform.SOS1BigM.Lowering.Basic
+import OMMXProof.Instance.Transform.SOS1BigM.Lowering.Plan
+import OMMXProof.Instance.Transform.SOS1BigM.Lowering.Target
+import OMMXProof.Instance.Transform.SOS1BigM.Promotion
+import OMMXProof.Instance.Transform.SOS1BigM.Promotion.Basic
+import OMMXProof.Instance.Transform.SOS1BigM.Promotion.Semantics
+import OMMXProof.Instance.Transform.SOS1BigM.Promotion.Target
+import OMMXProof.Instance.Transform.SOS1BigM.Promotion.Validation
+import OMMXProof.Instance.Transform.SOS1BigM.Promotion.Witness
+import OMMXProof.Instance.Transform.SOS1BigM.SelectorFormulation
 import OMMXProof.State

lean/OMMXProof/Instance/Transform/SOS1BigM.lean

@@ -1,35 +1,40 @@
-import OMMXProof.Instance.Transform.SOS1BigM.Basic
-import OMMXProof.Instance.Transform.SOS1BigM.Formulation
-import OMMXProof.Instance.Transform.SOS1BigM.Plan
-import OMMXProof.Instance.Transform.SOS1BigM.Target
+import OMMXProof.Instance.Transform.SOS1BigM.SelectorFormulation
+import OMMXProof.Instance.Transform.SOS1BigM.Lowering
+import OMMXProof.Instance.Transform.SOS1BigM.Promotion
 
 /-!
-# SOS1 Big-M lowering
-
-This module is the entrypoint for the SDK SOS1 conversion as an actual
-`Instance.Transform`, including the formulation, validated plans, target
-construction, encode/decode maps, and lowering correctness.
-
-## Terminology
-
-- An **SOS1 member** is a source decision-variable component named by the
-  selected SOS1 constraint.
-- A **selector** is the binary value associated with an SOS1 member in the
-  at-most-one formulation. A selector value of zero forces its member to zero;
-  a value of one only permits the member to be nonzero.
-- A **reused selector** is a binary SOS1 member used directly as its own
-  selector.
-- A **fresh selector** is a new binary variable appended to the target instance
-  for a non-binary SOS1 member.
-- The **canonical selector** is the deterministic selector used by `encode`: it
-  is zero exactly when its member is zero.
-- A **link constraint** is a Big-M inequality connecting a non-binary member
-  `vᵢ` to its fresh selector `sᵢ`. For finite bounds `lᵢ ≤ vᵢ ≤ uᵢ`, the
-  generated sides are `vᵢ ≤ uᵢ sᵢ` when `0 < uᵢ` and
-  `lᵢ sᵢ ≤ vᵢ` when `lᵢ < 0`.
-- The **cardinality constraint** is the at-most-one inequality over all reused
-  and fresh selectors.
-- A **plan** selects the occurrence of the source SOS1 constraint to lower. A
-  **validated plan** additionally proves that every member has finite bounds,
-  so all required Big-M coefficients can be constructed.
+# SOS1 Big-M transformations
+
+This module collects both directions of the SOS1 Big-M formulation:
+
+## Shared layers
+
+- `SOS1BigM.SelectorFormulation` defines the direction-independent selector
+  formulation. It owns the abstract mixed reused/fresh selector semantics, the
+  concrete retained-prefix/fresh-selector-suffix layout, and the canonical
+  Big-M link and cardinality rows. It proves both the relation to SOS1 and the
+  equivalence between the generated rows and the abstract semantics.
+
+## Transformation directions
+
+- `SOS1BigM.lowering` replaces one first-class SOS1 constraint with binary
+  selectors, Big-M links, and a selector-cardinality row.
+- `SOS1BigM.promotion` recognizes that standard Big-M layout and replaces it
+  with one first-class SOS1 constraint while preserving existing special
+  constraints which do not reference the removed selectors.
+
+The primary source-to-target interpretations use the shared layers in opposite
+orders, and the reverse feasibility arguments traverse the same bridge backwards:
+
+- Lowering constructs canonical selector semantics from SOS1 and realizes those
+  semantics as target rows. For the reverse feasibility implication, it
+  interprets the target rows and projects the resulting selector semantics to
+  SOS1.
+- Promotion recognizes and interprets the source row suffix, then projects the
+  resulting selector semantics to the promoted SOS1 constraint. Its canonical
+  decoding argument proceeds from SOS1 back to the source rows.
+
+The promotion checker deliberately accepts a conservative sufficient
+condition. Other valid formulations of SOS1 remain outside this Big-M-specific
+transform family.
 -/

lean/OMMXProof/Instance/Transform/SOS1BigM/Lowering.lean

@@ -0,0 +1,10 @@
+import OMMXProof.Instance.Transform.SOS1BigM.Lowering.Basic
+import OMMXProof.Instance.Transform.SOS1BigM.Lowering.Plan
+import OMMXProof.Instance.Transform.SOS1BigM.Lowering.Target
+
+/-!
+# SOS1 Big-M lowering
+
+This module is the entrypoint for complete SOS1 Big-M lowering: plan validation,
+target construction, encode/decode maps, and transformation correctness.
+-/