[Merged by Bors] - feat(Counterexamples): disproof of the Aharoni–Korman conjecture by b-mehta · Pull Request #20082 · leanprover-community/mathlib4

b-mehta · 2024-12-19T17:20:13Z

Disprove the Aharoni–Korman conjecture by constructing and verifying Hollom's counterexample. Additionally show this counterexample is countable and scattered.

Zulip thread: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Aharoni.E2.80.93Korman.20conjecture.20formally.20disproved

depends on: [Merged by Bors] - feat(Set/Finite): a set is finite if its image and fibers are finite #20751
depends on: [Merged by Bors] - feat(Order/WellFoundedSet): add convenience constructors for IsWF and IsPWO for WellFoundedLT types #20752
depends on: [Merged by Bors] - feat(Data/Finset/Card): add InjOn and SurjOn versions of finset cardinality lemmas #20753
depends on: [Merged by Bors] - feat(Set/Function): prove surjectivity from composition #20754
depends on: [Merged by Bors] - feat(Order): relate chains to antichains #20756
depends on: [Merged by Bors] - feat(Order/Chain): adapt linear order lemmas to chains #20757
depends on: [Merged by Bors] - feat(Order/Chain): condition for the union of chains to be a chain #20758
depends on: [Merged by Bors] - feat(Order/Interval/Finset): map sectL and sectR on finset intervals #20759

github-actions · 2024-12-19T17:21:06Z

messageFile.md

Counterexamples/AharoniKorman.lean

loefflerd · 2025-01-09T19:37:37Z

Is this ready for review? I guess not, as there is a section marked "to_move", and it's way over the usual length limit for a single PR; but it's appearing in the review queue.

If my guess is correct, could you please mark it as WIP?

These lemmas were present for `Function.Injective` and `Function.Surjective`, but not for their partial versions. Useful from the disproof of the Aharoni–Korman conjecture, #20082.

Counterexamples/AharoniKorman.lean

…20758) Also show that monotone functions preserve chains, and use this lemma to golf another. Useful from the disproof of the Aharoni–Korman conjecture, #20082.

…20759) Useful from the disproof of the Aharoni–Korman conjecture, #20082.

…20751) A useful lemma from the disproof of the Aharoni–Korman conjecture, #20082. Note this does not seem to follow from any of the existing preimage finiteness lemmas.

… IsPWO for WellFoundedLT types (#20752) A useful lemma from the disproof of the Aharoni–Korman conjecture, #20082. While these are easy to inline, they are hard to discover for an end user, since `WellFoundedLT` is never mentioned in this file. As such, this change improves discoverability, especially with `exact?`.

…ardinality lemmas (#20753) These lemmas are useful for dot notation, and help the interface between Set predicates and Finset cardinality. In this PR we: - Add two new lemmas for non-dependent functions, spelled with Set predicates - Use them to golf the dependent versions and improve readability Useful from the disproof of the Aharoni–Korman conjecture, #20082.

Add a series of lemmas for chains in a preorder. Each of these are true in a linear order, but remain true under the weaker assumption that both elements are in a chain. Used in the disproof of the Aharoni–Korman conjecture, #20082.

github-actions · 2025-01-20T14:55:03Z

PR summary 94861e850c

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ C_inter_Icc_large
+ Hollom
+ HollomOrder
+ HollomOrder.trans
+ R
+ R_diff_infinite
+ R_subset_level
+ S
+ S_infinite
+ S_mapsTo_previous
+ S_subset_R
+ S_subset_level
+ SpinalMap
+ add_lt_add_of_lt
+ aharoni_korman_false
+ apply_eq_of_line_eq
+ apply_eq_of_line_eq_aux
+ apply_eq_of_line_eq_step
+ apply_le_of_le
+ apply_lt_of_lt
+ apply_mem_Icc_of_mem_Icc
+ card_C_inter_Icc_eq
+ card_chainBetween
+ chainBetween
+ chainBetween_isChain
+ chainBetween_subset
+ embed
+ embed_apply
+ embed_image_Icc
+ embed_strictMono
+ eq_of_le
+ eq_self_of_mem
+ equivHollom
+ exists_finite_intersection
+ exists_partition_iff_nonempty_spinalMap
+ ext
+ fibre_antichain
+ idempotent
+ image_chainBetween_isChain
+ incomp_apply
+ incomp_of_eq
+ induction
+ induction_on_level
+ injOn_of_isChain
+ instance : Countable Hollom
+ instance : FunLike (SpinalMap C) α α
+ instance : PartialOrder Hollom
+ le_apply_of_le
+ le_of_toHollom_le_toHollom
+ left_or_right_bias
+ level
+ level_eq
+ level_eq_range
+ level_isPWO
+ line
+ line_injOn
+ line_mapsTo
+ line_toHollom
+ lt_apply_of_lt
+ mapsTo_Icc_image
+ mapsTo_Icc_self
+ mem
+ no_infinite_antichain
+ no_infinite_antichain_level
+ no_spinalMap
+ not_R_hits_same
+ not_S_hits_next
+ not_S_mapsTo_previous
+ not_apply_lt
+ not_le_of_eq
+ not_lt_apply
+ not_lt_of_eq
+ ofHollom_toHollom
+ ordConnected_level
+ range_subset
+ scattered
+ square_subset_R
+ square_subset_S
+ square_subset_S_case_1
+ square_subset_S_case_2
+ square_subset_above
+ to
+ toFun_eq_coe
+ toHollom_le_toHollom
+ toHollom_le_toHollom_iff_fixed_right
+ toHollom_mem_level_iff
+ toHollom_ofHollom
+ x0
+ x0_y0_mem
+ x0_y0_min
+ x0y0
+ x0y0_mem
+ x0y0_min
+ y0
+ «exists»
+ «forall»
+ «forall₂»
+ «forall₃»

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

Add a series of lemmas for chains in a preorder. Each of these are true in a linear order, but remain true under the weaker assumption that both elements are in a chain. Used in the disproof of the Aharoni–Korman conjecture, #20082.

Counterexamples/AharoniKorman.lean

riccardobrasca · 2025-02-17T21:40:34Z

apply_eq_of_line_eq_step also seems a little slow. Maybe avoiding Fintype and using Finite can help?

Counterexamples/AharoniKorman.lean

Co-authored-by: Riccardo Brasca <riccardo.brasca@gmail.com>

Counterexamples/AharoniKorman.lean

riccardobrasca · 2025-02-19T09:37:24Z

@b-mehta can you add the reference to references.bib as Eric suggested? The unused variable linter problem is going to be solved/improved so I think this is ready to go.

bors d+

mathlib-bors · 2025-02-19T09:37:28Z

✌️ b-mehta can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

riccardobrasca · 2025-03-02T10:29:33Z

@b-mehta I think you forgot this :) (and we want it in mathlib!). Thanks!

b-mehta · 2025-03-10T11:29:17Z

I did forget, thank you for the reminder!

Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>

b-mehta · 2025-03-10T12:05:31Z

Thank you all for the helpful reviews!

bors merge

) Disprove the Aharoni–Korman conjecture by constructing and verifying Hollom's counterexample. Additionally show this counterexample is countable and scattered. Zulip thread: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Aharoni.E2.80.93Korman.20conjecture.20formally.20disproved Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

Counterexamples/AharoniKorman.lean

mathlib-bors · 2025-03-10T12:57:50Z

Build failed (retrying...):

Build

) Disprove the Aharoni–Korman conjecture by constructing and verifying Hollom's counterexample. Additionally show this counterexample is countable and scattered. Zulip thread: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Aharoni.E2.80.93Korman.20conjecture.20formally.20disproved Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

mathlib-bors · 2025-03-10T13:25:16Z

Build failed:

Build

Co-authored-by: damiano <adomani@gmail.com>

b-mehta · 2025-03-12T15:18:01Z

bors merge

) Disprove the Aharoni–Korman conjecture by constructing and verifying Hollom's counterexample. Additionally show this counterexample is countable and scattered. Zulip thread: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Aharoni.E2.80.93Korman.20conjecture.20formally.20disproved Co-authored-by: Eric Wieser <wieser.eric@gmail.com> Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com>

mathlib-bors · 2025-03-12T16:32:38Z

Pull request successfully merged into master.

Build succeeded:

) Disprove the Aharoni–Korman conjecture by constructing and verifying Hollom's counterexample. Additionally show this counterexample is countable and scattered. Zulip thread: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Aharoni.E2.80.93Korman.20conjecture.20formally.20disproved Co-authored-by: Eric Wieser <wieser.eric@gmail.com> Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com>

…nprover-community#20082) Disprove the Aharoni–Korman conjecture by constructing and verifying Hollom's counterexample. Additionally show this counterexample is countable and scattered. Zulip thread: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Aharoni.E2.80.93Korman.20conjecture.20formally.20disproved Co-authored-by: Eric Wieser <wieser.eric@gmail.com> Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com>

b-mehta added the WIP Work in progress label Dec 19, 2024

trivial1711 reviewed Dec 19, 2024

View reviewed changes

Counterexamples/AharoniKorman.lean Outdated Show resolved Hide resolved

b-mehta added t-order Order theory and removed WIP Work in progress labels Jan 8, 2025

b-mehta added the WIP Work in progress label Jan 9, 2025

mathlib4-dependent-issues-bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Jan 14, 2025

eric-wieser reviewed Jan 15, 2025

View reviewed changes

Counterexamples/AharoniKorman.lean Outdated Show resolved Hide resolved

eric-wieser reviewed Jan 15, 2025

View reviewed changes

Counterexamples/AharoniKorman.lean Show resolved Hide resolved

b-mehta commented Jan 15, 2025

View reviewed changes

Counterexamples/AharoniKorman.lean Outdated Show resolved Hide resolved

mathlib-bors bot pushed a commit that referenced this pull request Jan 15, 2025

feat(Order/Interval/Finset): map sectL and sectR on finset intervals (#…

6815c41

…20759) Useful from the disproof of the Aharoni–Korman conjecture, #20082.

b-mehta force-pushed the fishbone branch 2 times, most recently from c766de0 to 12eaf0a Compare January 21, 2025 18:15

madvorak reviewed Feb 17, 2025

View reviewed changes

Counterexamples/AharoniKorman.lean Show resolved Hide resolved

riccardobrasca reviewed Feb 17, 2025

View reviewed changes

Counterexamples/AharoniKorman.lean Show resolved Hide resolved

riccardobrasca reviewed Feb 17, 2025

View reviewed changes

Counterexamples/AharoniKorman.lean Show resolved Hide resolved

Update Counterexamples/AharoniKorman.lean

e8a083b

Co-authored-by: Riccardo Brasca <riccardo.brasca@gmail.com>

eric-wieser reviewed Feb 17, 2025

View reviewed changes

Counterexamples/AharoniKorman.lean Outdated Show resolved Hide resolved

ghost added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Feb 19, 2025

b-mehta added 2 commits March 10, 2025 11:25

Merge branch 'master' into fishbone

7af263a

add bib reference

92803d0

Update docs/references.bib

1453e8a

Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>

ghost added the ready-to-merge This PR has been sent to bors. label Mar 10, 2025

adomani reviewed Mar 10, 2025

View reviewed changes

Counterexamples/AharoniKorman.lean Outdated Show resolved Hide resolved

Update Counterexamples/AharoniKorman.lean

94861e8

Co-authored-by: damiano <adomani@gmail.com>

mathlib-bors bot changed the title ~~feat(Counterexamples): disproof of the Aharoni–Korman conjecture~~ [Merged by Bors] - feat(Counterexamples): disproof of the Aharoni–Korman conjecture Mar 12, 2025

mathlib-bors bot closed this Mar 12, 2025

mathlib-bors bot deleted the fishbone branch March 12, 2025 16:32

Conversation

b-mehta commented Dec 19, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Dec 19, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Uh oh!

loefflerd commented Jan 9, 2025

Uh oh!

Uh oh!

Uh oh!

Uh oh!

github-actions bot commented Jan 20, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 94861e850c

Import changes for modified files

Declarations diff

Uh oh!

Uh oh!

riccardobrasca commented Feb 17, 2025

Uh oh!

Uh oh!

Uh oh!

Uh oh!

riccardobrasca commented Feb 19, 2025

Uh oh!

mathlib-bors bot commented Feb 19, 2025

Uh oh!

riccardobrasca commented Mar 2, 2025

Uh oh!

b-mehta commented Mar 10, 2025

Uh oh!

b-mehta commented Mar 10, 2025

Uh oh!

Uh oh!

mathlib-bors bot commented Mar 10, 2025

Uh oh!

mathlib-bors bot commented Mar 10, 2025

Uh oh!

b-mehta commented Mar 12, 2025

Uh oh!

mathlib-bors bot commented Mar 12, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

10 participants

b-mehta commented Dec 19, 2024 •

edited

Loading

github-actions bot commented Dec 19, 2024 •

edited

Loading

github-actions bot commented Jan 20, 2025 •

edited

Loading