nucleostructureCert
plain-language theorem explainer
Bundles three finite-counting facts into one certificate: five canonical nucleosides, four DNA bases, and DNA cardinality equal to $2^2$. Genetics-depth and config-dimension arguments cite it as a single witness that the nucleoside inventory matches the $D=5$ / $F_2^2$ picture. Construction is a structure instance that fills each field by an existing `decide` theorem.
Claim. There is a certificate recording three equalities: the number of canonical nucleosides is $5$; the number of DNA nucleosides is $4$; and the DNA nucleoside count equals $2^2$.
background
The module treats nucleoside inventory as a config-dimension fact (B5 / genetics depth). Five canonical nucleosides (adenine, thymine, cytosine, guanine, uracil) match configDim $D=5$, with uracil completing the RNA set. DNA uses four of those five bases (A, T, C, G).
The DNA quartet is identified with the two-bit space $F_2^2$: two binary axes (purine/pyrimidine and keto/amino) give cardinality $2^2=4$. The certificate structure packages exactly those three numerical claims: total nucleoside card $5$, DNA card $4$, and DNA card $=2^2$.
Upstream, each claim is already a closed decide theorem: nucleosideCount, dna_nucleoside_count, and dna_equals_F2sq (doc: "4 = 2² (F₂² at D=2)").
proof idea
One-line structure instance. Field five_total is filled by nucleosideCount (Fintype.card Nucleoside = 5). Field four_dna is filled by dna_nucleoside_count (DNANucleoside.card = 4). Field f2_structure is filled by dna_equals_F2sq (DNANucleoside.card = 2^2). No new reasoning; the definition only assembles the three prior decide proofs into NucleostructureCert.
why it matters
Gives a single named witness that the nucleoside census matches the RS genetics-depth story: five types for configDim $D=5$, and DNA's four bases as $F_2^2$ at effective $D=2$. The module frames this as the canonical $D=3$ spatial setting's combinatorial shadow on base pairing (two binary axes, complement pairs A–T and G–C).
No downstream consumers are recorded yet (used_by empty), so the certificate is presently a terminal packaging lemma inside Chemistry. It does not touch the T0–T8 forcing chain, RCL, or mass ladder; it only locks the discrete inventory that later chemistry or information-theoretic layers can quote without re-proving the three cards.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.