refactor: #70 — dissolve CaiGovorov/SimpleOrbitRank into Lovasz + fill legacy sorries (Lovász sorry-free, axiom-clean)#3

Open

cameronfreer wants to merge 8 commits into

70-relocate-caigovorov-stack

Commits on Jul 2, 2026

refactor: #70 — R1: move out_pair_eq' upstream into Lovasz; add CaiGovorov/Pigeonhole imports
cameronfreer
committed
refactor: #70 — R2: dissolve CaiGovorovOrbit.lean into Lovasz.lean (§ CaiGovorovStack)
cameronfreer
committed
feat: #70 — R3: FILL tupleEquivSimple_implies_orbit + orbit_separation_by_simple_graph (−2 sorries, axiom-clean)
cameronfreer
committed
refactor: #70 — R4: move submodule block + rank skeleton into Lovasz (§ RankTheorem); dissolve SimpleOrbitRank.lean
cameronfreer
committed
feat: #70 — R5: FILL toSimple, InTupleSimpleEvalSpan.mul, orbitIndicator_mem_simpleGraphSpan (−3 sorries, axiom-clean)
cameronfreer
committed
feat: #70 — F3: FILL private Lemma 2.4 tupleEquiv_implies_tupleOrbitRel (−1 sorry, axiom-clean)
cameronfreer
committed
feat: #70/#86 — F3: FILL the three multigraph descents; Lovász has ZERO live sorries (−3, axiom-clean)
cameronfreer
committed
feat: #70 — F3: CLOSE the σ-sum parallel-edge frontier Dtr.eval_tupleEquiv_invariant (−1 sorry, axiom-clean)
cameronfreer
committed