K2RingOfIntegers
plain-language theorem explainer
K2RingOfIntegers introduces a structure that records a number field together with the order of its Milnor K-group K₂ of the ring of integers. Number theorists working on the Birch-Tate conjecture and its Recognition Science reformulation via lattice paths would reference this definition when equating K-theory orders to zeta values at negative integers. The declaration consists of a bare structure definition with no lemmas or reduction steps.
Claim. A structure consisting of a number field $F$ and a natural number equal to the order $|K_2(O_F)|$.
background
The module frames the Birch-Tate conjecture for totally real fields F as the equality |K₂(O_F)| = w₂(F) · ζ_F(-1) · (-1)^[F:Q], with w₂(F) the number of roots of unity. Recognition Science recasts both sides as counts of φ-lattice paths and φ-periodic orbits. The upstream zeta abbreviation supplies the arithmetic zeta function that equals 1 on positive integers.
proof idea
The declaration is a structure definition that directly introduces the two fields without applying lemmas or tactics.
why it matters
The structure supplies the K-theory side needed for the Birch-Tate equality inside the Recognition Science resolution that equates path counts to orbit counts. It sits under the module's key theorems on K-theory as φ-lattice path counting and zeta values as φ-periodic orbits. The general case remains open for non-abelian extensions, and this definition closes the scaffolding for the φ-path equivalence step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.