feat: add a typeclass for the continuum hypothesis

[eric-wieser]

This allows a proof from the Archive to be promoted to mathlib itself.

The proof strategy of iff_exists_sierpinski_pathological_pred was written almost entirely with public Gemini 3 Thinking, and then manually corrected.

---

[github-actions]

PR summary bc90dd441b

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.SetTheory.Cardinal.ContinuumHypothesis (new file)	1471

---

Declarations diff

+ Cardinal.exists_sierpinski_pathological_partition_of_card_eq_aleph_one
+ Cardinal.exists_sierpinski_pathological_pred_of_card_eq_aleph_one
+ ContinuumHypothesis
+ aleph0_covby_continuum.{u}
+ continuum_eq_aleph_one.{u}
+ iff_aleph0_covby_continuum.{u}
+ iff_continuum_eq_aleph_one.{u}
+ iff_exists_sierpinski_pathological_partition
+ iff_exists_sierpinski_pathological_pred
+ of_aleph0_covby_continuum
+ of_continuum_eq_aleph_one

You can run this locally as follows

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

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

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

---

No changes to technical debt.

You can run this locally as

./scripts/reporting/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).

[vihdzp]

Likewise, I believe this theorem generalizes to:

Suggested change

	ContinuumHypothesis ↔
	∃ f : ℝ → ℝ → Prop, (∀ x, {y | ¬ f x y}.Countable) ∧ ∀ y, {x : ℝ | f x y}.Countable := by
	#α = c ↔
	∃ f : α → α → Prop, (∀ x, #{y | ¬ f x y} < c) ∧ ∀ y, #{x : ℝ | f x y} < c := by

So the continuum hypothesis is truly doing nothing other than giving you the initial rewrite of #ℝ = ℵ₁.

[eric-wieser]

Is one of these being an equality a typo?

[eric-wieser]

Is c here intended to be a bound variable or 𝔠?

[vihdzp]

Bound variable. The same strategy of "take a well-ordering with least order type" should work to prove this.

[plp127]

Would it be desirable to do something like this instead

Suggested change

	theorem iff_continuum_eq_aleph_one.{u} : ContinuumHypothesis ↔ (𝔠 : Cardinal.{u}) = ℵ₁ := by
	rw [iff_continuum_eq_aleph_one', ← Cardinal.lift_continuum.{u, 0}, Cardinal.lift_eq_aleph_one]
	theorem iff_continuum_eq_aleph_one.{u} : ContinuumHypothesis ↔ (𝔠 : Cardinal.{u}) = ℵ₁ :=
	⟨fun ⟨h⟩ => by rw [← lift_continuum.{u, 0}, h, lift_eq_aleph_one],
	fun h => ⟨by rw [← lift_inj.{0, u}, lift_continuum, h, aleph_one_eq_lift]⟩⟩

and remove the primed version?

[eric-wieser]

What's the harm in the primed version? I could also make it private, but maybe that's not possibly with mk_iff.

[mathlib-merge-conflicts]

This pull request has conflicts, please merge master and resolve them.

[vihdzp]

I don't think we should be importing real numbers in the continuum hypothesis file. If there are any theorems about types with cardinality continuum they should be written in that generality.

[vihdzp]

Opened #37965 proving a more general version of the pathological relation theorem.

[mathlib-merge-conflicts]

This pull request has conflicts, please merge master and resolve them.

[felixpernegger]

@eric-wieser do you still plan to work on this? If not I'd be interested in adding some "additional axioms" (CH, GHC and MA)

[eric-wieser]

Closing in favor of #43537, since I am unable to push further changes to this now-protected branch.