birch_tate_path_orbit_duality
plain-language theorem explainer
The theorem asserts that the Birch-Tate conjecture holds in Recognition Science as path-orbit duality, with |K₂(O_F)| and ζ_F(-1) counting identical φ-geometric objects for totally real fields F. Researchers linking K-theory to zeta values in discrete φ-lattices would cite it. The proof is a one-line trivial assertion of the duality.
Claim. For a totally real number field $F$, $|K_2(O_F)| = w_2(F) · ζ_F(-1) · (-1)^{[F:ℚ]}$, where the equality is path-orbit duality in the φ-lattice.
background
The module MC-006 frames the Birch-Tate conjecture as relating the order of the Milnor K-group K₂(O_F) to the Dedekind zeta value ζ_F(-1) for totally real F, with the RS resolution interpreting both as counts of φ-geometric objects. K₂(O_F) counts φ-lattice paths while ζ_F(-1) measures φ-periodic orbit structure, so the sides coincide by construction. Upstream results include PhiForcingDerived.of (structure of J-cost) and SpectralEmergence.of (structure forcing SU(3)×SU(2)×U(1) gauge content and three generations from Q₃ face counts).
proof idea
The proof is a term-mode trivial assertion that directly states the path-orbit duality holds, without reduction steps or named lemmas from the depends_on list.
why it matters
This declaration fills RS-3 in the Birch-Tate structure by asserting the conjecture as φ-path equivalence. It connects K-theory path counting to zeta orbit structure per the module documentation and supports the broader RS resolution framework. No downstream uses appear, leaving it as a high-level bridge to the forcing chain landmarks.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.