nucleosideCount
plain-language theorem explainer
There are exactly five canonical nucleosides: adenine, thymine, cytosine, guanine, and uracil. Genetics and config-dimension arguments in the chemistry layer cite this as the discrete count matching configDim = 5 (RNA-inclusive). The proof is a one-line decision procedure on the derived finite enumeration of the inductive type.
Claim. The finite set of canonical nucleosides $\{\text{adenine},\ \text{thymine},\ \text{cytosine},\ \text{guanine},\ \text{uracil}\}$ has cardinality $5$.
background
This module ties nucleoside inventory to configuration dimension in the Recognition Science chemistry layer (B5 / genetics depth). The five canonical types are adenine, thymine, cytosine, guanine, and uracil; the last is the RNA base that replaces thymine. DNA uses four of the five, with Watson–Crick pairing A–T and G–C.
The local claim is that this five-element set is exactly the finite type of nucleosides, so its cardinality is the discrete count that the module identifies with configDim $D = 5$. Downstream, the four DNA bases are further identified with the vector space $\mathbb{F}_2^2$ (two binary axes: purine/pyrimidine and keto/amino).
The inductive enumeration carries a derived Fintype instance, so cardinality is a decidable finite-set fact rather than an analytic estimate.
proof idea
Term-mode proof by the decide tactic. The nucleoside type is an inductive enumeration of five constructors with a derived Fintype instance, so Lean reduces Fintype.card to the literal $5$ and closes the equality by computation. No lemmas beyond the derived finite-type infrastructure are required.
why it matters
This is the five_total field of the nucleoside-structure certificate in the same module, which packages the five-base count, the four-DNA count, and the $\mathbb{F}_2^2$ identification into one certificate object. The module doc frames the five types as configDim $D = 5$ (RNA-inclusive) and the DNA quartet as $2^2$ on two binary chemical axes.
In the broader framework it is a discrete chemistry landmark, not a step of the T0–T8 forcing chain: it records that the canonical nucleoside inventory matches the config-dimension count used in the genetics-depth narrative. Anyone assembling or auditing the nucleoside-structure certificate must discharge this equality first.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.