dna_nucleoside_count
plain-language theorem explainer
The DNA nucleoside set (adenine, thymine, cytosine, guanine) has cardinality exactly 4. Genetics and RS chemistry pages cite this as the discrete count feeding the nucleostructure certificate. The proof is a one-line finite-set decision: Lean evaluates the explicit Finset and closes the equality.
Claim. The finite set of DNA nucleosides $\{\mathrm{A},\mathrm{T},\mathrm{C},\mathrm{G}\}$ has cardinality $4$.
background
This module (Nucleoside Structure from ConfigDim, B5 / Genetics Depth) treats the canonical nucleoside inventory as a discrete configuration count. Five named nucleosides (adenine, thymine, cytosine, guanine, uracil) match configDim $D=5$ when RNA is included; DNA drops uracil.
DNANucleoside is the explicit Finset of the four DNA bases. The module links that count to the $D=3$ story: four DNA nucleotides equal $2^2$, i.e. an $\mathbb{F}_2^2$ space on two binary axes (purine/pyrimidine and keto/amino). Upstream, several modules fix spatial dimension $D:=3$ (T8/T9 forcing), which frames why a $2$-bit base coding sits inside the larger recognition geometry.
proof idea
Term-mode proof by decide. The set is a concrete four-element Finset of an inductive enum, so Mathlib's decision procedure computes .card and discharges = 4 with no lemmas or case splits.
why it matters
Fills the four_dna field of nucleostructureCert, the module certificate that packages three facts: five total nucleosides, four DNA bases, and the identification $4=2^2$ ($\mathbb{F}_2^2$ structure). Downstream genetics depth uses that certificate to tie base-pair coding to config-dimension counting rather than an ad-hoc biological list.
In the RS chain this is the chemistry-side echo of forced low dimension: T8 forces $D=3$ spatially, while the DNA count is the $2$-axis binary coding ($2^2=4$) complementary to the five-type RNA/configDim picture. It does not itself force $D$; it records the discrete inventory the certificate needs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.