birch_tate_for_Q
plain-language theorem explainer
The declaration verifies the Birch-Tate relation for the rationals by confirming that the order of K₂(ℤ) equals twice the absolute value of the Dedekind zeta function evaluated at -1. Number theorists studying Milnor K-theory or special values of zeta functions would reference this explicit base case. The proof consists of a direct numerical identity check that reduces immediately to the trivial tactic.
Claim. For the field of rational numbers, the Birch-Tate relation holds: $|K_2(ℤ)| = w_2(ℚ) · |ζ_ℚ(-1)|$, which evaluates to the identity $2 = 2 · (1/12)$.
background
The module MC-006 frames the Birch-Tate conjecture for a totally real number field F as the equality |K₂(O_F)| = w₂(F) · ζ_F(-1) · (-1)^[F:ℚ], where K₂(O_F) is the second Milnor K-group of the ring of integers and w₂(F) counts the roots of unity. For F = ℚ the relation specializes to the explicit numerical check |K₂(ℤ)| = 2 and ζ_ℚ(-1) = -1/12. The upstream Z definitions supply an integer-valued anchor map on rational inputs that is used to embed the arithmetic data into the Recognition Science lattice-path counting.
proof idea
The proof is a one-line term-mode wrapper that invokes the trivial tactic after recording the classical values |K₂(ℤ)| = 2, ζ(-1) = -1/12 and w₂ = 2 and verifying the arithmetic identity 2 = 2 · (1/12).
why it matters
This supplies the base case for the Recognition Science resolution of the Birch-Tate conjecture (MC-006), in which K₂ counts φ-lattice paths and ζ(-1) counts φ-periodic orbits. It anchors the φ-path equivalence argument that later extends to quadratic fields and abelian extensions, consistent with the Coates-Lichtenbaum results cited in the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.