BirchTateConjecture
plain-language theorem explainer
The Birch-Tate conjecture equates the order of the Milnor K-group K₂(O_F) for a totally real number field F to the product of the number of roots of unity w₂(F) and the absolute value of the Dedekind zeta function at -1. Arithmetic geometers and K-theorists cite this when linking special zeta values to algebraic K-theory. The Lean definition implements a simplified placeholder by setting the statement directly to true.
Claim. For a totally real number field $F$, $|K_2(O_F)| = w_2(F) · |ζ_F(-1)|$.
background
The module MC-006 frames the Birch-Tate conjecture as relating the order of K₂(O_F), the second Milnor K-group of the ring of integers, to the special value ζ_F(-1) of the Dedekind zeta function. In the Recognition Science setting this relation is reinterpreted as equality of two counts of φ-lattice paths: K₂(O_F) enumerates the paths while ζ_F(-1) records the periodic orbit structure under the φ-action. Upstream gap functions F supply the logarithmic generator log(1 + z/φ) that defines the underlying φ-lattice metric.
proof idea
The declaration is a one-line definition that directly asserts the equality as the constant True, serving as a simplified placeholder without tactic steps or lemma applications.
why it matters
This definition occupies the Birch-Tate slot inside the RS resolution framework, where K-theory and zeta values are unified by φ-path equivalence. It sits downstream of the forcing chain T0-T8 and the Recognition Composition Law, and is intended to connect to the Birch-Swinnerton-Dyer structure imported by the module. No downstream uses are recorded, leaving open the explicit closure with Lichtenbaum-type conjectures.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.