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
Open
Conversation
…vorov/Pigeonhole imports out_pair_eq' is Mathlib-only and was the Cai-Govorov stack's sole real dependency on CycleKrylov; moving it upstream (same namespace) keeps all ~24 CycleKrylov call sites resolving through the import chain. Lovasz now imports Graphon.CaiGovorov (Mathlib-only Vandermonde engine) and Mathlib.Combinatorics.Pigeonhole, ready for the R2 stack insertion.
… CaiGovorovStack)
The entire Cai–Govorov stack (test graphs, chunk 3A/4A super-case,
eq. (10), chunks 4B–4G descent, tupleEquivSimple_implies_orbit_general)
moves verbatim into Lovasz.lean as a self-contained section (open
Finset, variable {K}) inserted immediately before
orbit_separation_by_simple_graph — the position its header always
envisioned. Staging file deleted; SimpleOrbitRank now imports
CycleKrylov (transitively Lovasz ⊇ the stack); root module updated.
Zero proof changes; lake build green (2962 jobs).
…n_by_simple_graph (−2 sorries, axiom-clean) The simple-graph Lemma 2.4's 'both non-surjective' branch — the long-standing critical sorry — closes with one line: tupleEquivSimple_implies_orbit_general (the Cai–Govorov descent, now upstream in § CaiGovorovStack). orbit_separation_by_simple_graph is its contrapositive (by_contra + push_neg; tupleEquivSimple is definitionally the simpleEvalAt equality family). Un-taints the whole simple-side chain: k1_orbit_sep_aux, InRootedProfileSpan.of_const_on_orbit, label_unlabeled_square_moment_descends now verify [propext, Classical.choice, Quot.sound] (checked via lean_verify). Docstrings updated to PROVED. Sorry count 20 → 18.
…(§ RankTheorem); dissolve SimpleOrbitRank.lean The CycleKrylov Phase-A/B submodule packaging (simpleEvalSubmodule / multiEvalSubmodule / orbitInvariantSubmodule, membership iffs, inclusions) and the entire rank skeleton + annihilator argument from SimpleOrbitRank.lean now live in Lovasz.lean directly after simpleEvalAt_aut_invariant — every dependency (the Cai–Govorov stack, tupleOrbitIndicator_mem_multiEvalSpan, simpleEvalAt_aut_invariant) is above it. The #70 rank theorem is now available to everything downstream of Lovasz, incl. MatrixDetermination. SimpleOrbitRank.lean deleted; pointer comment in CycleKrylov; Lovasz gains Mathlib.LinearAlgebra.Dual.Lemmas (previously transitive via CycleKrylov's analysis imports). Zero proof changes; lake build green (2961 jobs).
…tor_mem_simpleGraphSpan (−3 sorries, axiom-clean) The three former §3 residues, relocated below § RankTheorem and proved: - InTupleMultiEvalSpan.toSimple (the Hadamard-square residue, Lovász Lemma 2.5 content): direct corollary of the rank collapse — multigraph evals are aut-invariant, orbit-invariant functions lie in the simple-eval span. - InTupleSimpleEvalSpan.mul: hB/hW/htwin added to the signature (as its own docstring always recorded necessary — without them the statement is FALSE via the label-label Hadamard square); proof = (h₁.toMulti.mul hB h₂.toMulti).toSimple hB hW htwin. - orbitIndicator_mem_simpleGraphSpan: list repackaging of tupleOrbitIndicator_mem_simpleEvalSpan (now itself sorry-free) via List.finRange/Fin.sum_univ_def. All lean_verify [propext, Classical.choice, Quot.sound]. Sorry count 18 → 15; Lovasz.lean's remaining 5 = 3 multigraph-descent infra (#86-adjacent) + 2 known-false #77 (frozen).
…el (−1 sorry, axiom-clean) The MatrixDetermination-local Lemma 2.4 (strong induction with the 'both non-surjective' architectural sorry) is replaced by the 10-line bridge to Lovasz.tupleEquivSimple_implies_orbit_via_2_5 (proved via the #70 rank theorem): tupleEquiv is definitionally tupleEquivSimple after unfolding labeledEvalK, and the IsWeightedAutomorphism bodies coincide. Mirrors the already-working multiLabeledEvalK_tupleEquiv_invariant pattern (whose stale 'canonical sorry' docstring is also corrected — it has been proved since the orbit route landed). The Claims 4.1-4.4 intermediate theorems remain as standalone results. lean_verify: [propext, Classical.choice, Quot.sound]. Sorry count 15 → 14.
…RO live sorries (−3, axiom-clean) § CaiGovorovStack moves up (directly after out_pair_eq'/simpleEvalAt_eq_multi, its minimal position); the descent chain (multigraphEval_unlabeled_excess/ label_unlabeled_nonisolated/unlabeled_unlabeled_nonisolated_descends + wrapper + one_doubled + in_simpleProfileClosure + the Lovász multiLabeledEvalK_tupleEquiv_invariant bridge) relocates below it. - The three sorry'd descents are PROVED uniformly: 2 lines each via tupleEquivSimple_implies_orbit_general + multiLabeledEvalK_eq_of_orbit (the structural multiplicity hypotheses and square-moment inputs are no longer needed by the proofs; statements preserved, except hW/htwin ADDED to the UU-nonisolated case, which lacked them). - multiLabeledEvalK_tupleEquiv_invariant rewired from the descent chain to the same 2-line orbit route (h_sq_moment now unused, renamed _). - multigraphEval_in_simpleProfileClosure becomes sorry-free. lean_verify [propext, Classical.choice, Quot.sound]. Sorry count 14 → 11. Lovasz.lean's remaining 2 = the frozen known-false #77 stubs. The #86 descent question is closed as a corollary of #70.
…Equiv_invariant (−1 sorry, axiom-clean) The 'genuine Lovász §3 multigraph frontier' dissolves into multigraph semantics: DecLabeledGraphTr.toMulti packages the σ-sum content (graph edges mult 1 + lu0Mult decorations as label-to-unlabeled-0 multi-edges, multiplicities adding where they coincide); toMulti_sym2_prod splits the Sym2 power product (pow_add + ofSimple-style collapse + prod_pow_eq_pow_sum/prod_comm/prod_ite_eq' + out_pair_eq'); eval_eq_multiEval identifies Dtr.eval = LL-factor × multigraph eval for n > 0; the (proved) bridge multiLabeledEvalK_tupleEquiv_invariant then descends it through tupleEquiv uniformly — no case split on lu0Mult. Theorem relocated below the bridge; hW/htwin added (required by the bridge; the theorem is a leaf). n = 0 case kept direct. Stale 'canonical root'/frontier notes updated. lean_verify: [propext, Classical.choice, Quot.sound]. Sorry count 11 → 10.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Follow-up to #70 (merged as PR #2). Consolidates the Cai–Govorov / simple-orbit
machinery into
Lovasz.leanand fills the remaining legacy sorries left open bythe merged descent + rank theorem.
Net effect: project drops 21 → 15 sorries; Lovász has zero live sorries.
All new proofs verified
#print axioms-clean.Relocation (R1–R5)
out_pair_eq'upstream intoLovasz; addCaiGovorov/Pigeonholeimports.CaiGovorovOrbit.leanintoLovasz.lean(§ CaiGovorovStack).tupleEquivSimple_implies_orbit+orbit_separation_by_simple_graph.Lovasz(§ RankTheorem); dissolveSimpleOrbitRank.lean.toSimple,InTupleSimpleEvalSpan.mul,orbitIndicator_mem_simpleGraphSpan(with
hB/hW/htwinhypotheses — the unhypothesized form is false).Fills (F3)
tupleEquiv_implies_tupleOrbitRel.Dtr.eval_tupleEquiv_invariant.Files
Graphon/CaiGovorovOrbit.lean,Graphon/SimpleOrbitRank.lean— removed (dissolved intoLovasz).Graphon/Lovasz.lean— absorbs both, plus the new proofs.Graphon.lean,CycleKrylov.lean,MatrixDetermination.lean— import/wiring updates.