card_singleton
plain-language theorem explainer
The declaration shows that the cardinality of any singleton Finset equals one. Researchers deriving inductive growth bounds on balls in step relations or computing divisor sums for primes cite this counting fact. The argument reduces immediately to a direct library application on singleton cardinality.
Claim. For any element $x$ of type $α$, the cardinality of the singleton Finset ${x}$ equals 1.
background
The ConeBound module supplies minimal local definitions for ball growth bounds under a bounded-degree step relation, avoiding heavy imports from Mathlib. This singleton cardinality fact is invoked as the base case when inducting on ball radius. The module setting focuses on finite neighborhoods in a causality context where step relations model light-cone propagation.
proof idea
One-line wrapper that applies the library result on the cardinality of singleton Finsets.
why it matters
This result supplies the base case in the induction for ballFS_card_le_geom, which establishes that ball cardinalities grow at most geometrically with radius. It also appears in sigma_zero_prime to evaluate the divisor function at zero for primes. In the Recognition framework it closes the elementary counting step required for cone-bound derivations that feed into the eight-tick octave and spatial dimension D=3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.