ZetaValue
plain-language theorem explainer
ZetaValue packages a number field together with the real number given by its Dedekind zeta function evaluated at -1. Researchers working on the Birch-Tate relation in the Recognition Science setting cite this structure when equating the order of K2 of the ring of integers to a product involving that zeta value. The declaration is a direct record constructor with no computational body or lemmas.
Claim. For a number field $F$, the structure ZetaValue consists of the field $F$ together with the real number $z = ζ_F(-1)$.
background
The module MC-006 states the Birch-Tate conjecture for a totally real number field $F$: $|K_2(O_F)| = w_2(F) · ζ_F(-1) · (-1)^{[F:Q]}$, where $w_2(F)$ is the number of roots of unity. Recognition Science resolves the relation by counting φ-lattice paths on one side and φ-periodic orbits on the other. The single upstream dependency supplies the real-valued spin quantity $s.twice/2$ from the SpinStatistics module.
proof idea
The declaration is a direct structure definition that introduces the record type with two fields: the number field and the real zeta value at -1. No tactics or lemmas are invoked.
why it matters
This definition supplies the zeta side of the Birch-Tate relation inside the RS framework, where ζ_F(-1) measures φ-periodic orbit structure while K2 counts φ-lattice paths. It supports the module's key statements that both sides count the same φ-geometric objects and prepares the ground for the phi-path equivalence that closes the conjecture for abelian extensions of Q.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.