NucleostructureCert
plain-language theorem explainer
Packages three counting facts about the canonical nucleosides: five total types, four DNA bases, and the DNA count equal to 2². Chemists and geneticists working the B5 / Genetics Depth layer cite it as the certificate type for the config-dimension match. It is a pure structure definition; the equalities are discharged by a separate inhabitant.
Claim. A certificate consists of three equalities: the finite type of nucleosides (adenine, thymine, cytosine, guanine, uracil) has cardinality $5$; the DNA subset (excluding uracil) has cardinality $4$; and that DNA cardinality equals $2^2$.
background
The module sits in the B5 / Genetics Depth layer of Recognition Science chemistry. It records that five canonical nucleoside types (adenine, thymine, cytosine, guanine, uracil) match configDim $D = 5$, with uracil included for RNA, while DNA uses four of the five.
Nucleoside is the inductive enumeration of those five bases, deriving Fintype. DNANucleoside is the explicit finset of the four DNA bases, excluding uracil. The module notes that the canonical $D=3$ structure gives four DNA nucleotides as $2^2$, corresponding to two binary axes (purine/pyrimidine and keto/amino), i.e. an $\mathbb{F}_2^2$ labeling.
Lean status of the module is zero sorry and zero axiom; the counting lemmas that fill the certificate fields live as siblings in the same file.
proof idea
No proof body: this is a structure declaration. It only names three fields of type Prop (cardinal equalities). The actual proofs are supplied by the inhabitant nucleostructureCert, which assigns nucleosideCount, dna_nucleoside_count, and dna_equals_F2sq to the three fields respectively.
why it matters
This certificate type is the interface for the nucleoside-structure claim in the Genetics Depth layer. Downstream, nucleostructureCert is the unique packaged witness that the five-base enumeration, the four-base DNA finset, and the $2^2$ identity all hold simultaneously.
In the Recognition framework the five-count is the chemistry-side match to configDim $D = 5$, while the $2^2$ identity records the two binary classification axes on DNA bases. That sits next to the forcing-chain landmark $D = 3$ spatial dimensions (T8) and the eight-tick octave (T7), as a discrete combinatorial shadow rather than a dynamical derivation. The structure itself does not prove those links; it only freezes the three equalities that later genetics arguments can quote as a single object.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.