Nucleoside
plain-language theorem explainer
Enumerates the five canonical nucleosides (A, T, C, G, U) as a finite inductive type. Chemists and RS genetics proofs cite it as the discrete carrier for configDim = 5. Deriving Fintype and DecidableEq makes cardinality and membership decidable by computation.
Claim. There is a finite set of five canonical nucleosides: adenine, thymine, cytosine, guanine, and uracil, equipped with decidable equality and a finite-type instance so that its cardinality is computable.
background
In the Recognition Science chemistry layer, nucleoside identity is treated as a discrete configuration space rather than a continuum of molecular geometries. The module frames genetics depth B5: five canonical nucleoside types match configDim $D = 5$ once uracil is included for RNA, while DNA retains four bases.
The four DNA bases are further identified with the vector space $\mathbb{F}_2^2$, whose two binary axes are the classical purine/pyrimidine and keto/amino distinctions. This inductive type is the raw carrier for that counting argument: it names the five residues and supplies the typeclass instances needed for automatic cardinality proofs.
No upstream lemmas are required; the declaration only imports Mathlib for Fintype, DecidableEq, and related infrastructure.
proof idea
Definitional, not a proof. The inductive type lists five nullary constructors and derives DecidableEq, Repr, BEq, and Fintype. Downstream theorems such as nucleosideCount then close Fintype.card = 5 by decide.
why it matters
This type is the discrete substrate for the module's genetics claim that five nucleosides equal configDim $D = 5$, while DNA's four bases equal $2^2$. Downstream, nucleosideCount records the card-5 fact, DNANucleoside carves out the DNA subset ${A,T,C,G}$, and NucleostructureCert packages the triple of equalities (five total, four DNA, four equals $2^2$) into a single certificate structure.
In the broader RS forcing picture the link is configurational rather than dynamical: $D = 3$ spatial dimensions (T8) and the eight-tick octave (T7) sit upstream; here the same discrete-counting style is applied to base identity. The declaration itself is closed (0 sorry, 0 axiom) and only supplies the named finite set those certificates quantify over.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.