Counting cubic AR-labelings
Abstract
Finite partial-injection extension counts and the counting union bound.
Theorem 1.1 (Indexed constraints without a chosen enumeration).
Lean statement: D5/S3/Combinatorics/EdgeLabeling/CubicARGraphCounting.nat_card_equiv_constraints
Proof. Machine-checked in Lean as D5/S3/Combinatorics/EdgeLabeling/CubicARGraphCounting.nat_card_equiv_constraints (✓ std3). ∎
Source. Repository-derived.
Commentary.
The indexed extension count also holds for the natural cardinality of the constraint subtype, independently of its chosen finite enumeration.
Theorem 1.2 (An outcome avoiding every bad event).
Lean statement: D5/S3/Combinatorics/EdgeLabeling/CubicARGraphCounting.exists_avoiding_of_sum_card_lt
Proof. Machine-checked in Lean as D5/S3/Combinatorics/EdgeLabeling/CubicARGraphCounting.exists_avoiding_of_sum_card_lt (✓ std3). ∎
Source. Repository-derived.
Commentary.
If the sum of the cardinalities of a finite family of bad events is smaller than the cardinality of the finite sample space, an outcome lies in none of the bad events. This follows from the cardinality bound for a finite union.