zeta_def
plain-language theorem explainer
The zeta_def theorem equates the Recognition zeta function to the standard arithmetic zeta function that takes the constant value 1 on positive integers. Number theorists working inside the Recognition framework cite it when they need the basic identification before applying Dirichlet convolution or inversion. The proof is a one-line reflexivity that follows directly from the preceding abbreviation.
Claim. Let $Z$ be the Recognition zeta function. Then $Z$ coincides with the standard arithmetic zeta function, so $Z(n)=1$ for every positive integer $n$.
background
The module supplies thin wrappers around Mathlib arithmetic functions, beginning with the Möbius function and its square-free properties. The upstream abbreviation zeta defines the Recognition zeta as the constant function 1 on positive integers. The declaration also depends on the for structure from UniversalForcingSelfReference, which records the structural properties required for meta-realization certificates.
proof idea
The proof is a one-line term that applies reflexivity to the preceding zeta abbreviation.
why it matters
The equality places the standard zeta function inside the Recognition number-theory layer and prepares the ground for Dirichlet algebra. No direct dependents appear yet, but the declaration supports later inversion formulas and connects to the forcing-chain landmarks by supplying a basic arithmetic tool consistent with the phi-ladder conventions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.