Resolution
plain-language theorem explainer
The Resolution structure packages the assertion that Birch-Tate holds for every totally real number field by equating the order of K2 of its ring of integers to a root-of-unity multiple of the Dedekind zeta value at negative one. Researchers deriving mass ladders or cosmological parameters from phi-lattice counting cite it when they need the conjecture marked resolved. The declaration is introduced as a bare structure definition that simply bundles three propositions with no further reduction.
Claim. Let $F$ be a totally real number field. The structure Resolution consists of the three propositions that the Birch-Tate relation $|K_2(O_F)|=w_2(F)·ζ_F(-1)·(-1)^{[F:ℚ]}$ holds for all such $F$, that an explicit formula expressing this relation in terms of zeta values exists, and that the conjecture is resolved.
background
In the Recognition Science setting the Birch-Tate conjecture is recast as an equality between two counts of the same phi-geometric objects. For a totally real field $F$, $K_2(O_F)$ counts the phi-lattice paths inside the ring of integers while ζ_F(-1) counts the phi-periodic orbits; the module states that these two counts coincide once the J-cost function is calibrated by the ledger factorization. The local theoretical setting is the MC-006 framework in which K-theory is identified with phi-lattice path counting and zeta values with phi-periodic orbit structure, with the abelian case already settled by Coates-Lichtenbaum.
proof idea
The declaration is a structure definition that directly introduces the three fields birchTateHolds, zetaFormula and resolved. No lemmas are invoked and no tactics are executed; the resolved field is simply the constant True.
why it matters
Resolution supplies the resolved status of Birch-Tate that is invoked by the electron-mass, fine-structure, gravitational-constant and proton-electron-ratio theorems as well as by the cosmological-constant derivations. It completes the RS resolution step for the abelian case via phi-path equivalence and thereby feeds the phi-ladder mass formula and the alpha band bounds. The general non-abelian case remains open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.