Resolution
plain-language theorem explainer
The Resolution structure bundles three propositions asserting that the Birch-Tate conjecture holds for totally real fields, that an explicit formula in zeta values exists, and that the conjecture is resolved. Number theorists and Recognition Science researchers working on K-theory to zeta connections would cite this when closing the abelian case of the conjecture. The definition is a direct bundling of the three claims with no lemmas or reduction steps.
Claim. A structure asserting that the Birch-Tate conjecture holds for all totally real number fields, that an explicit formula relating $|K_2(O_F)|$ to the Dedekind zeta value at $-1$ exists, and that the conjecture is resolved.
background
The Birch-Tate conjecture states that for a totally real number field $F$, $|K_2(O_F)| = w_2(F) · ζ_F(-1) · (-1)^{[F:Q]}$, where $K_2$ is the second Milnor K-group and $w_2(F)$ counts roots of unity. The module frames this inside Recognition Science as equality of φ-lattice path counts on one side and φ-periodic orbit counts on the other. Upstream results supply the φ-lattice machinery and the abelian case already settled by Coates-Lichtenbaum.
proof idea
The structure is defined directly by bundling the three propositions birchTateHolds, zetaFormula, and resolved; no lemmas are applied and no tactics are used.
why it matters
This supplies the resolution framework for MC-006 and feeds downstream into structural statements for the electron mass, fine-structure constant bounds, gravitational constant positivity, and cosmological constant derivations. It closes the abelian case while leaving the non-abelian extension open, consistent with the φ-path equivalence route in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.