zetaDomainCount
plain-language theorem explainer
The declaration proves that the finite type of zeta domains has cardinality five. Researchers formalizing the Riemann zeta function within Recognition Science cite this to confirm the structural decomposition into five canonical regions. The proof proceeds by a single decision tactic that leverages the Fintype instance derived from the inductive definition.
Claim. The set of canonical domains of the Riemann zeta function has cardinality five: $|D| = 5$, where $D$ consists of the region with real part greater than one, the critical strip, the left half-plane, the critical line, and the trivial zeros.
background
The module opens the mathematics section of Recognition Science by defining five canonical domains for the Riemann zeta function. ZetaDomain is an inductive type whose constructors are realPartGtOne, criticalStrip, leftHalfPlane, criticalLine, and trivialZeros; it derives DecidableEq, Repr, BEq, and Fintype. The module states that this construction yields zero sorries and zero axioms.
proof idea
The proof is a one-line wrapper that applies the decide tactic. This tactic computes the cardinality directly from the Fintype instance on the inductive type, which enumerates exactly five constructors.
why it matters
This count populates the five_domains field inside the riemannZetaCert definition, completing the structural certificate for the Riemann zeta function. It forms the C1 mathematics opening that lists the five domains without axioms. The result anchors downstream derivations that connect zeta to the Recognition Science forcing chain and the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.