w2Invariant
plain-language theorem explainer
w2Invariant supplies the w₂(F) factor for the Birch-Tate relation in a totally real number field F, returning the constant 2 that counts the roots of unity ±1. Number theorists or RS researchers linking K₂(O_F) orders to zeta values at -1 would cite it when counting φ-lattice paths. The definition is a direct constant assignment that encodes the standard fact for totally real fields.
Claim. For a totally real number field $F$, the invariant $w_2(F)$ is defined to be 2, where $w_2(F)$ counts the roots of unity in $F$.
background
The Birch-Tate conjecture states that for totally real $F$, $|K_2(O_F)| = w_2(F) · ζ_F(-1) · (-1)^{[F:ℚ]}$, with $w_2(F)$ the number of roots of unity. The module frames this as φ-lattice path counting on one side and φ-periodic orbit structure on the other, both arising from the same geometric objects in the Recognition Science resolution. Upstream anchors include the integer map Z from Masses.Anchor that assigns sector-dependent integers via powers of Q6, the gap function F from AnchorPolicy that equals log(1 + Z/φ)/log(φ), and the generating functional F from Pipelines that produces the master gap at z=1.
proof idea
The definition is a one-line constant return of 2, encoding the classical count of roots of unity in totally real fields. No lemmas are applied; the body directly supplies the simplified value used in the surrounding Birch-Tate statements.
why it matters
This definition supplies the w₂(F) multiplier required by the Birch-Tate conjecture inside the RS framework, where K₂ counts φ-lattice paths and ζ(-1) measures periodic orbits. It sits among siblings such as BirchTateConjecture and k2_phi_paths, feeding the path-orbit duality that resolves the conjecture via φ-equivalence. The module notes the result is known for abelian extensions of ℚ but remains open in the non-abelian case; the constant 2 closes the totally-real case in the RS-native units.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.