zetaSpecialPoint_count
plain-language theorem explainer
The theorem establishes that the inductive type enumerating the five canonical special points of the Riemann zeta function has finite cardinality exactly 5. A researcher verifying the structural count of zeta values under configDim D = 5 in the Recognition Science model would cite this result to anchor the five-point certification. The proof is a one-line decide tactic that exhausts the constructors of the inductive definition.
Claim. The finite set of canonical special points of the Riemann zeta function has cardinality $5$, consisting of the points corresponding to the values at $-1$, $0$, $2$, $4$, and $3$.
background
The module identifies five canonical special values of the zeta function tied to configDim D = 5: ζ(-1) = -1/12, ζ(0) = -1/2, ζ(2) = π²/6, ζ(4) = π⁴/90, and ζ(3) (Apéry). The upstream inductive definition ZetaSpecialPoint introduces exactly these five cases as constructors minusOne, zero, two, four, and three, each equipped with DecidableEq, Repr, BEq, and Fintype instances. This supplies the finite-type structure whose cardinality is asserted in the theorem.
proof idea
The proof is a one-line wrapper that applies the decide tactic. The tactic computes the Fintype.card instance by enumerating the five constructors of ZetaSpecialPoint and confirms the equality holds.
why it matters
This declaration supplies the five_points field inside the downstream zetaSpecialValuesCert definition, which certifies the complete set of special values. It directly implements the module's claim of five structurally canonical points for the zeta function under configDim D = 5, closing the count without reference to the forcing chain or J-uniqueness.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.