Add verified SOS1 Big-M promotion transform in Lean - #1132

Draft

termoshtt wants to merge 15 commits into

mainfrom

codex/add-sos1-bigm

Commits on Aug 6, 2026

WIP: start SOS1 promotion transform
termoshtt
committed
272723a
Complete SOS1 promotion transform
termoshtt
committed
198b13a
Group SOS1 Big-M transforms by direction
termoshtt
committed
e8b4f0e
Document SOS1 Big-M promotion rules and validation failures
termoshtt
committed
ca28935
Preserve independent special constraints in SOS1 promotion
termoshtt
committed
ea17ca9
Document SOS1 promotion validation contract
termoshtt
committed
012e5ac
Split SOS1 promotion target modules
termoshtt
committed
86cbb1d
Split SOS1 promotion semantics
termoshtt
committed
5de8219
Rename SOS1 promotion reconstruction module
termoshtt
committed
efaa44b
Share canonical SOS1 Big-M rows
termoshtt
committed
80e4b96
Adapt SOS1 Big-M transforms to restructured semantics
termoshtt
committed
91701d9
Adopt mathlib-style SOS1 Big-M modules
termoshtt
committed
ab9d64b

Commits on Aug 17, 2026

Merge remote-tracking branch 'origin/main' into codex/add-sos1-bigm
termoshtt
committed
52f664e
Document SOS1 Big-M shared layers
termoshtt
committed
f46c63a
Consolidate SOS1 Big-M selector formulation
termoshtt
committed
8d3dfb9