DNANucleoside
plain-language theorem explainer
The DNA nucleoside set is the four-element subset of the five canonical nucleosides obtained by dropping uracil. RS chemistry and genetics modules cite it when counting DNA bases or matching the DNA alphabet to an F₂² configuration space. The body is a literal finite-set enumeration of adenine, thymine, cytosine, and guanine.
Claim. Let the five canonical nucleosides be adenine, thymine, cytosine, guanine, and uracil. The DNA nucleoside set is the finite set $\{\mathrm{adenine},\,\mathrm{thymine},\,\mathrm{cytosine},\,\mathrm{guanine}\}$ (uracil excluded).
background
The module treats nucleoside structure as a configuration-dimension count (B5 / genetics depth). Five canonical nucleoside types (adenine, thymine, cytosine, guanine, uracil) are identified with configDim $D=5$, the RNA-inclusive alphabet. DNA keeps four of those five, excluding uracil.
The ambient type is the inductive enumeration of those five constructors, with decidable equality and a Fintype instance. Downstream counting therefore reduces to finite-set cardinality on a named subset. The module also records the structural claim that the DNA four-set matches $2^2$, i.e. the vector space $\mathbb{F}_2^2$ at effective dimension two (purine/pyrimidine and keto/amino axes).
proof idea
Pure definition: the value is the four-element Finset literal listing adenine, thymine, cytosine, and guanine. No lemmas or tactics; cardinality facts are discharged later by decide on this concrete set.
why it matters
This set is the carrier for the DNA side of the nucleostructure certificate. It is used by the cardinality theorem that the DNA set has size 4, by the theorem that this size equals $2^2$ ($\mathbb{F}_2^2$ at $D=2$), and by the structure packing five-total, four-DNA, and $f_2$-structure fields together.
In the module narrative, five nucleosides match configDim $D=5$ (RNA-inclusive), while the DNA four-set is the canonical $D=3$ genetics fragment written as a binary configuration space. The definition therefore anchors the combinatorial half of the B5 genetics-depth story without introducing axioms or sorries.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.