ZetaSpecialPoint
plain-language theorem explainer
ZetaSpecialPoint enumerates the five canonical arguments at which the Riemann zeta function takes distinguished closed-form values in the Recognition Science setting. Researchers certifying zeta identities or dimensional configuration counts cite this enumeration when establishing the finite set tied to configDim D equals 5. The definition is a direct inductive type with five named constructors that automatically derives decidable equality and finite cardinality.
Claim. Let $Z$ be the inductive type whose five elements are the points $s = -1, 0, 2, 4, 3$ at which the Riemann zeta function admits canonical values.
background
The module isolates five structurally canonical points of the Riemann zeta function, identified with configDim D = 5: zeta(-1) = -1/12, zeta(0) = -1/2, zeta(2) = pi squared over 6, zeta(4) = pi to the fourth over 90, and zeta(3) the Apery constant. These points are treated as the complete list of distinguished values required for subsequent certification. The sole upstream dependency is the definition of spin 2 (graviton) from SpinStatistics, which supplies the integer label appearing among the five points.
proof idea
The declaration is an inductive definition that introduces exactly five constructors corresponding to the listed arguments. The deriving clause for DecidableEq, Repr, BEq, and Fintype is applied automatically with no separate proof term or tactic steps required.
why it matters
This type supplies the domain for the downstream theorem establishing that its cardinality is exactly five and for the structure ZetaSpecialValuesCert that records the same count. It directly realizes the module statement of five canonical zeta points inside the Recognition Science framework, where the count aligns with the five-dimensional configuration space. The construction closes the enumeration step before any value identities are asserted.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.