ZetaSpecialValuesCert
plain-language theorem explainer
The certificate structure records that the inductive enumeration of canonical Riemann zeta points has cardinality exactly five. Researchers linking analytic number theory to Recognition Science constants would cite this when the five-point count must be formally verified. The definition is a structure whose single field directly encodes the Fintype cardinality of the enumerated points.
Claim. Let $P$ be the inductive type whose constructors label the five canonical points of the Riemann zeta function. The certificate is the structure whose field asserts that the cardinality of $P$ equals 5.
background
The module identifies five canonical special values of the Riemann zeta function: zeta(-1) = -1/12, zeta(0) = -1/2, zeta(2) = pi^2/6, zeta(4) = pi^4/90, and zeta(3) (Apery's constant). These are the structurally canonical points where the zeta function takes a well-defined closed form. The inductive type enumerates them via five constructors and derives a Fintype instance, so the certificate simply records that the cardinality is five.
proof idea
The declaration is a structure definition whose single field states the cardinality equality. The equality holds because the inductive type has exactly five constructors and the Fintype instance is derived automatically. No additional lemmas or tactics are applied.
why it matters
The structure is consumed by the downstream definition that builds a concrete instance of the certificate. It formalizes the five-point enumeration stated in the module documentation and supports the Recognition Science identification of configDim D = 5. The count is closed by the inductive definition with no open questions remaining at this step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.