feat(Counterexamples): disproof of the Aharoni-Korman conjecture

[b-mehta]

---

[github-actions]

PR summary 09f880f2dd

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ C_touches_levelLine
+ Hollom
+ Hollom.«exists»
+ Hollom.«forall»
+ HollomOrder
+ Prod.Ico_map_sectL
+ Prod.Ico_map_sectR
+ Prod.Ioc_map_sectL
+ R
+ R_diff_infinite
+ R_infinite
+ R_maps
+ R_subset_level
+ S
+ S_infinite
+ S_maps
+ S_subset_R
+ S_subset_level
+ Set.finite_of_finite_fibers
+ _root_.IsChain.le_of_not_lt
+ aharoni_korman_false
+ apply_le_of_le
+ apply_mem_interval
+ card_chainBetween
+ card_chainBetweenMem
+ chainBetween
+ chainBetweenMem
+ chainBetweenMem_isChain
+ chainBetweenMem_subset
+ chainBetween_inter
+ chainBetween_isChain
+ chainBetween_subset
+ chain_intersect_antichain
+ embed
+ embed_image_Icc
+ embed_le_embed_iff
+ embed_lt_embed_iff
+ embed_monotone
+ embed_strictMono
+ eqn_1_aux
+ exists_finite_intersection
+ iUnion_levelLine
+ image_chainBetweenMem_isChain
+ image_chainBetween_isChain
+ incomp_apply
+ incomp_of_eq
+ induction
+ injOn_chain
+ instance : LE Hollom := ⟨fun x y ↦ HollomOrder (ofHollom x) (ofHollom y)⟩
+ instance : PartialOrder Hollom
+ isAntichain_levelLine
+ le_apply_of_le
+ le_of_toHollom_le_toHollom
+ left_mem_chainBetween
+ left_or_right_bias
+ level
+ levelLine
+ levelLine_nonempty_of_infinite
+ levelLine_subset_level
+ level_eq
+ level_eq_range
+ level_isPWO
+ mem_R
+ mem_levelLine_iff
+ middle_mem_chainBetweenMem
+ no_infinite_antichain
+ no_infinite_antichain_level
+ not_le_of_eq
+ ofHollom
+ ofHollom_symm_eq
+ ofHollom_toHollom
+ ordConnected_level
+ p
+ p_image_Icc
+ p_image_Ici
+ p_injOn
+ p_le_p
+ p_lt_p
+ p_mem_C
+ p_mem_inter
+ p_strictMonoOn
+ p_uniq
+ p_uniq'
+ p_zero
+ pairwiseDisjoint_level
+ pairwise_disjoint_level
+ partition_iff_function
+ right_mem_chainBetween
+ singleton_p
+ square_subset_R
+ square_subset_S
+ square_subset_S_case_1
+ square_subset_S_case_2
+ square_subset_above
+ surjOn_of_injOn_of_card_le
+ test
+ toHollom
+ toHollom_le_toHollom
+ toHollom_le_toHollom_iff_fixed_right
+ toHollom_mem_levelLine_iff
+ toHollom_mem_level_iff
+ toHollom_ofHollom
+ toHollom_symm_eq
+ univ_isPWO
+ x0
+ x0_y0_mem
+ x0_y0_min
+ x0y0
+ x0y0_mem
+ x0y0_min
+ y0

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).