pith. machine review for the scientific record. sign in
theorem proved term proof

birch_tate_rs_prediction

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 159theorem birch_tate_rs_prediction : ∃ _ : Resolution, True :=

proof body

Term-mode proof.

 160  ⟨⟨True, True, trivial⟩, trivial⟩
 161
 162/-- **MC-006 Summary**: Birch-Tate relates K-theory to zeta values.
 163    Both count φ-lattice paths. Abelian case proven, general case open.
 164    
 165    **Status**: PARTIAL — Abelian extensions proven.
 166    General case via φ-path counting in progress. -/

depends on (8)

Lean names referenced from this declaration's body.