Concluding the counting argument

In this file, we finish the counting argument.

Main declarations

• ConNF.card_tSet_le: There are at most μ-many t-sets at each level.

theorem ConNF.card_codingFunction [ConNF.Params] [ConNF.Level] [ConNF.CoherentData] (β : ConNF.TypeIndex) [ConNF.LeLevel β] : Cardinal.mk (ConNF.CodingFunction β) < Cardinal.mk ConNF.μ

theorem ConNF.card_supportOrbit [ConNF.Params] [ConNF.Level] [ConNF.CoherentData] (β : ConNF.TypeIndex) [ConNF.LeLevel β] : Cardinal.mk (ConNF.SupportOrbit β) < Cardinal.mk ConNF.μ

theorem ConNF.card_tSet_le [ConNF.Params] [ConNF.Level] [ConNF.CoherentData] (β : ConNF.TypeIndex) [ConNF.LeLevel β] : Cardinal.mk (ConNF.TSet β) ≤ Cardinal.mk ConNF.μ

Note that we cannot prove the reverse implication because all of our hypotheses at this stage are about permutations, not objects.

theorem ConNF.card_tangle_le [ConNF.Params] [ConNF.Level] [ConNF.CoherentData] (β : ConNF.TypeIndex) [ConNF.LeLevel β] : Cardinal.mk (ConNF.Tangle β) ≤ Cardinal.mk ConNF.μ