abelian_phi_product
plain-language theorem explainer
Abelian extensions of the rationals carry a product decomposition of their phi-lattices into cyclotomic factors. Researchers working on the Birch-Tate conjecture for abelian fields would cite this reduction step. The proof is a one-line trivial discharge that accepts the assertion without further lemmas.
Claim. For an abelian extension $F/mathbb{Q}$, the $phi$-lattice of $F$ decomposes as a product of cyclotomic $phi$-structures.
background
The module treats the Birch-Tate conjecture relating $|K_2(mathcal{O}_F)|$ to $zeta_F(-1)$ for totally real $F$, with the RS resolution that both sides count the same $phi$-geometric objects via lattice paths and periodic orbits. The local setting states that Birch-Tate emerges from $phi$-lattice path counting, with $K_2$ counting paths and zeta measuring orbit structure. Upstream results supply structural 'is' properties from empirical programs, simplicial edge lengths, mechanism design, mock theta constructions, and anchor functions, though the present declaration stands as an independent assertion.
proof idea
The declaration is a term-mode proof consisting of the single tactic 'trivial'. No upstream lemmas are invoked; the statement is accepted outright.
why it matters
This declaration supplies the RS-4 assertion inside the Birch-Tate module, providing the product decomposition of $phi$-lattices required to reduce the conjecture to the abelian case. It aligns with the module's claim that both sides of Birch-Tate count identical $phi$-path objects. The result supports the known abelian resolution (Coates-Lichtenbaum) while the non-abelian case remains open in the framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.